Commit f1d447fa authored by MARCHE Claude's avatar MARCHE Claude
Browse files

mise au point preuves

parent b3f27633
......@@ -731,6 +731,17 @@ predicate stmt_writes (s:stmt) (w:Set.set mident) =
eval_fmla sigma pi f
(* hypothese 2: si
sigma, pi |= (forall w, p) /\ (forall w, q)
alors
sigma, pi |= forall w, (f /\ q)
*)
axiom abstract_effects_distrib_conj :
forall s:stmt, p q:fmla, sigma:env, pi:stack.
eval_fmla sigma pi (abstract_effects s p) /\
eval_fmla sigma pi (abstract_effects s q) ->
eval_fmla sigma pi (abstract_effects s (Fand p q))
(* hypothese 3: si
|= p -> q
alors
|= (forall w, p) -> (forall w, q)
......@@ -745,20 +756,6 @@ predicate stmt_writes (s:stmt) (w:Set.set mident) =
mais on n'a
(forall x, true) -> (forall x, x=42)
*)
(*
axiom abstract_effects_monotonic :
forall s:stmt, p q:fmla.
valid_fmla (Fimplies p q) ->
forall sigma:env, pi:stack.
eval_fmla sigma pi (abstract_effects s p) ->
eval_fmla sigma pi (abstract_effects s q)
*)
(*
axiom abstract_effects_monotonic :
forall s:stmt, p:fmla.
valid_fmla p -> valid_fmla (abstract_effects s p)
*)
axiom abstract_effects_monotonic :
forall s:stmt, p q:fmla.
valid_fmla (Fimplies p q) ->
......@@ -766,12 +763,6 @@ predicate stmt_writes (s:stmt) (w:Set.set mident) =
eval_fmla sigma pi (abstract_effects s p) ->
eval_fmla sigma pi (abstract_effects s q)
axiom abstract_effects_distrib_conj :
forall s:stmt, p q:fmla, sigma:env, pi:stack.
eval_fmla sigma pi (abstract_effects s p) /\
eval_fmla sigma pi (abstract_effects s q) ->
eval_fmla sigma pi (abstract_effects s (Fand p q))
function wp (s:stmt) (q:fmla) : fmla =
match s with
| Sskip -> q
......@@ -794,7 +785,7 @@ predicate stmt_writes (s:stmt) (w:Set.set mident) =
end
(* hypothese 3: invariance de la formule "forall w. f"
(* hypothese 4: invariance de la formule "forall w. f"
par les effets de s si w = writes s
*)
axiom abstract_effects_writes :
......@@ -802,11 +793,8 @@ predicate stmt_writes (s:stmt) (w:Set.set mident) =
eval_fmla sigma pi (abstract_effects s q) ->
eval_fmla sigma pi (wp s (abstract_effects s q))
(* lemma wp_subst: *)
(* forall e:expr, q:fmla, id :mident, id':ident. *)
(* fresh_in_stmt id e -> *)
(* subst (wp e q) id id' = wp e (subst q id id') *)
(* ce lemme sert pour prouver distrib_conj, dans le cas de la sequence (et c'est tout !) *)
lemma monotonicity:
forall s:stmt, p q:fmla.
valid_fmla (Fimplies p q)
......@@ -823,6 +811,7 @@ predicate stmt_writes (s:stmt) (w:Set.set mident) =
wp (x := 7) x=42 = 7=42
*)
(* ce lemme sert pour wp_reduction dans le cas du while (et c'est tout !) *)
lemma distrib_conj:
forall s:stmt, sigma:env, pi:stack, p q:fmla.
(eval_fmla sigma pi (wp s p)) /\
......
......@@ -4,7 +4,6 @@ Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require int.MinMax.
Require set.Set.
(* Why3 assumption *)
Inductive list (a:Type) {a_WT:WhyType a} :=
......@@ -576,32 +575,109 @@ Definition total_valid_triple(p:fmla) (s:stmt) (q:fmla): Prop :=
exists pi':(list (ident* value)%type), exists n:Z, (many_steps sigma pi s
sigma' pi' Sskip n) /\ (eval_fmla sigma' pi' q).
Axiom set1 : forall (a:Type) {a_WT:WhyType a}, Type.
Parameter set1_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (set1 a).
Existing Instance set1_WhyType.
Parameter mem1: forall {a:Type} {a_WT:WhyType a}, a -> (set1 a) -> Prop.
(* Why3 assumption *)
Definition infix_eqeq {a:Type} {a_WT:WhyType a}(s1:(set1 a)) (s2:(set1
a)): Prop := forall (x:a), (mem1 x s1) <-> (mem1 x s2).
Axiom extensionality : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set1 a))
(s2:(set1 a)), (infix_eqeq s1 s2) -> (s1 = s2).
(* Why3 assumption *)
Definition subset {a:Type} {a_WT:WhyType a}(s1:(set1 a)) (s2:(set1
a)): Prop := forall (x:a), (mem1 x s1) -> (mem1 x s2).
Axiom subset_trans : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set1 a))
(s2:(set1 a)) (s3:(set1 a)), (subset s1 s2) -> ((subset s2 s3) ->
(subset s1 s3)).
Parameter empty: forall {a:Type} {a_WT:WhyType a}, (set1 a).
(* Why3 assumption *)
Definition is_empty {a:Type} {a_WT:WhyType a}(s:(set1 a)): Prop :=
forall (x:a), ~ (mem1 x s).
Axiom empty_def1 : forall {a:Type} {a_WT:WhyType a}, (is_empty (empty :(set1
a))).
Parameter add: forall {a:Type} {a_WT:WhyType a}, a -> (set1 a) -> (set1 a).
Axiom add_def1 : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a),
forall (s:(set1 a)), (mem1 x (add y s)) <-> ((x = y) \/ (mem1 x s)).
Parameter remove: forall {a:Type} {a_WT:WhyType a}, a -> (set1 a) -> (set1
a).
Axiom remove_def1 : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a)
(s:(set1 a)), (mem1 x (remove y s)) <-> ((~ (x = y)) /\ (mem1 x s)).
Axiom subset_remove : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(set1
a)), (subset (remove x s) s).
Parameter union: forall {a:Type} {a_WT:WhyType a}, (set1 a) -> (set1 a) ->
(set1 a).
Axiom union_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set1 a))
(s2:(set1 a)) (x:a), (mem1 x (union s1 s2)) <-> ((mem1 x s1) \/ (mem1 x
s2)).
Parameter inter: forall {a:Type} {a_WT:WhyType a}, (set1 a) -> (set1 a) ->
(set1 a).
Axiom inter_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set1 a))
(s2:(set1 a)) (x:a), (mem1 x (inter s1 s2)) <-> ((mem1 x s1) /\ (mem1 x
s2)).
Parameter diff: forall {a:Type} {a_WT:WhyType a}, (set1 a) -> (set1 a) ->
(set1 a).
Axiom diff_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set1 a))
(s2:(set1 a)) (x:a), (mem1 x (diff s1 s2)) <-> ((mem1 x s1) /\ ~ (mem1 x
s2)).
Axiom subset_diff : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set1 a))
(s2:(set1 a)), (subset (diff s1 s2) s1).
Parameter choose: forall {a:Type} {a_WT:WhyType a}, (set1 a) -> a.
Axiom choose_def : forall {a:Type} {a_WT:WhyType a}, forall (s:(set1 a)),
(~ (is_empty s)) -> (mem1 (choose s) s).
Parameter all: forall {a:Type} {a_WT:WhyType a}, (set1 a).
Axiom all_def : forall {a:Type} {a_WT:WhyType a}, forall (x:a), (mem1 x
(all :(set1 a))).
(* Why3 assumption *)
Definition assigns(sigma:(map mident value)) (a:(set.Set.set mident))
(sigma':(map mident value)): Prop := forall (i:mident), (~ (set.Set.mem i
a)) -> ((get sigma i) = (get sigma' i)).
Definition assigns(sigma:(map mident value)) (a:(set1 mident)) (sigma':(map
mident value)): Prop := forall (i:mident), (~ (mem1 i a)) -> ((get sigma
i) = (get sigma' i)).
Axiom assigns_refl : forall (sigma:(map mident value)) (a:(set.Set.set
mident)), (assigns sigma a sigma).
Axiom assigns_refl : forall (sigma:(map mident value)) (a:(set1 mident)),
(assigns sigma a sigma).
Axiom assigns_trans : forall (sigma1:(map mident value)) (sigma2:(map mident
value)) (sigma3:(map mident value)) (a:(set.Set.set mident)),
((assigns sigma1 a sigma2) /\ (assigns sigma2 a sigma3)) -> (assigns sigma1
a sigma3).
value)) (sigma3:(map mident value)) (a:(set1 mident)), ((assigns sigma1 a
sigma2) /\ (assigns sigma2 a sigma3)) -> (assigns sigma1 a sigma3).
Axiom assigns_union_left : forall (sigma:(map mident value)) (sigma':(map
mident value)) (s1:(set.Set.set mident)) (s2:(set.Set.set mident)),
(assigns sigma s1 sigma') -> (assigns sigma (set.Set.union s1 s2) sigma').
mident value)) (s1:(set1 mident)) (s2:(set1 mident)), (assigns sigma s1
sigma') -> (assigns sigma (union s1 s2) sigma').
Axiom assigns_union_right : forall (sigma:(map mident value)) (sigma':(map
mident value)) (s1:(set.Set.set mident)) (s2:(set.Set.set mident)),
(assigns sigma s2 sigma') -> (assigns sigma (set.Set.union s1 s2) sigma').
mident value)) (s1:(set1 mident)) (s2:(set1 mident)), (assigns sigma s2
sigma') -> (assigns sigma (union s1 s2) sigma').
(* Why3 assumption *)
Fixpoint stmt_writes(s:stmt) (w:(set.Set.set mident)) {struct s}: Prop :=
Fixpoint stmt_writes(s:stmt) (w:(set1 mident)) {struct s}: Prop :=
match s with
| (Sskip|(Sassert _)) => True
| (Sassign id _) => (set.Set.mem id w)
| (Sassign id _) => (mem1 id w)
| (Sseq s1 s2) => (stmt_writes s1 w) /\ (stmt_writes s2 w)
| (Sif t s1 s2) => (stmt_writes s1 w) /\ (stmt_writes s2 w)
| (Swhile _ _ body) => (stmt_writes body w)
......@@ -617,10 +693,16 @@ Axiom abstract_effects_generalize : forall (sigma:(map mident value))
(pi:(list (ident* value)%type)) (s:stmt) (f:fmla), (eval_fmla sigma pi
(abstract_effects s f)) -> (eval_fmla sigma pi f).
Axiom abstract_effects_monotonic : forall (s:stmt) (f:fmla),
forall (sigma:(map mident value)) (pi:(list (ident* value)%type)),
(eval_fmla sigma pi f) -> forall (sigma1:(map mident value)) (pi1:(list
(ident* value)%type)), (eval_fmla sigma1 pi1 (abstract_effects s f)).
Axiom abstract_effects_distrib_conj : forall (s:stmt) (p:fmla) (q:fmla)
(sigma:(map mident value)) (pi:(list (ident* value)%type)),
((eval_fmla sigma pi (abstract_effects s p)) /\ (eval_fmla sigma pi
(abstract_effects s q))) -> (eval_fmla sigma pi (abstract_effects s (Fand p
q))).
Axiom abstract_effects_monotonic : forall (s:stmt) (p:fmla) (q:fmla),
(valid_fmla (Fimplies p q)) -> forall (sigma:(map mident value)) (pi:(list
(ident* value)%type)), (eval_fmla sigma pi (abstract_effects s p)) ->
(eval_fmla sigma pi (abstract_effects s q)).
(* Why3 assumption *)
Fixpoint wp(s:stmt) (q:fmla) {struct s}: fmla :=
......@@ -677,4 +759,5 @@ intros.
do 3 eexists.
econstructor.
eauto.
Qed.
\ No newline at end of file
Qed.
......@@ -4,7 +4,6 @@ Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require int.MinMax.
Require set.Set.
(* Why3 assumption *)
Inductive list (a:Type) {a_WT:WhyType a} :=
......@@ -576,32 +575,109 @@ Definition total_valid_triple(p:fmla) (s:stmt) (q:fmla): Prop :=
exists pi':(list (ident* value)%type), exists n:Z, (many_steps sigma pi s
sigma' pi' Sskip n) /\ (eval_fmla sigma' pi' q).
Axiom set1 : forall (a:Type) {a_WT:WhyType a}, Type.
Parameter set1_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (set1 a).
Existing Instance set1_WhyType.
Parameter mem1: forall {a:Type} {a_WT:WhyType a}, a -> (set1 a) -> Prop.
(* Why3 assumption *)
Definition infix_eqeq {a:Type} {a_WT:WhyType a}(s1:(set1 a)) (s2:(set1
a)): Prop := forall (x:a), (mem1 x s1) <-> (mem1 x s2).
Axiom extensionality : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set1 a))
(s2:(set1 a)), (infix_eqeq s1 s2) -> (s1 = s2).
(* Why3 assumption *)
Definition subset {a:Type} {a_WT:WhyType a}(s1:(set1 a)) (s2:(set1
a)): Prop := forall (x:a), (mem1 x s1) -> (mem1 x s2).
Axiom subset_trans : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set1 a))
(s2:(set1 a)) (s3:(set1 a)), (subset s1 s2) -> ((subset s2 s3) ->
(subset s1 s3)).
Parameter empty: forall {a:Type} {a_WT:WhyType a}, (set1 a).
(* Why3 assumption *)
Definition assigns(sigma:(map mident value)) (a:(set.Set.set mident))
(sigma':(map mident value)): Prop := forall (i:mident), (~ (set.Set.mem i
a)) -> ((get sigma i) = (get sigma' i)).
Definition is_empty {a:Type} {a_WT:WhyType a}(s:(set1 a)): Prop :=
forall (x:a), ~ (mem1 x s).
Axiom empty_def1 : forall {a:Type} {a_WT:WhyType a}, (is_empty (empty :(set1
a))).
Parameter add: forall {a:Type} {a_WT:WhyType a}, a -> (set1 a) -> (set1 a).
Axiom add_def1 : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a),
forall (s:(set1 a)), (mem1 x (add y s)) <-> ((x = y) \/ (mem1 x s)).
Parameter remove: forall {a:Type} {a_WT:WhyType a}, a -> (set1 a) -> (set1
a).
Axiom remove_def1 : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a)
(s:(set1 a)), (mem1 x (remove y s)) <-> ((~ (x = y)) /\ (mem1 x s)).
Axiom subset_remove : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(set1
a)), (subset (remove x s) s).
Parameter union: forall {a:Type} {a_WT:WhyType a}, (set1 a) -> (set1 a) ->
(set1 a).
Axiom assigns_refl : forall (sigma:(map mident value)) (a:(set.Set.set
mident)), (assigns sigma a sigma).
Axiom union_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set1 a))
(s2:(set1 a)) (x:a), (mem1 x (union s1 s2)) <-> ((mem1 x s1) \/ (mem1 x
s2)).
Parameter inter: forall {a:Type} {a_WT:WhyType a}, (set1 a) -> (set1 a) ->
(set1 a).
Axiom inter_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set1 a))
(s2:(set1 a)) (x:a), (mem1 x (inter s1 s2)) <-> ((mem1 x s1) /\ (mem1 x
s2)).
Parameter diff: forall {a:Type} {a_WT:WhyType a}, (set1 a) -> (set1 a) ->
(set1 a).
Axiom diff_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set1 a))
(s2:(set1 a)) (x:a), (mem1 x (diff s1 s2)) <-> ((mem1 x s1) /\ ~ (mem1 x
s2)).
Axiom subset_diff : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set1 a))
(s2:(set1 a)), (subset (diff s1 s2) s1).
Parameter choose: forall {a:Type} {a_WT:WhyType a}, (set1 a) -> a.
Axiom choose_def : forall {a:Type} {a_WT:WhyType a}, forall (s:(set1 a)),
(~ (is_empty s)) -> (mem1 (choose s) s).
Parameter all: forall {a:Type} {a_WT:WhyType a}, (set1 a).
Axiom all_def : forall {a:Type} {a_WT:WhyType a}, forall (x:a), (mem1 x
(all :(set1 a))).
(* Why3 assumption *)
Definition assigns(sigma:(map mident value)) (a:(set1 mident)) (sigma':(map
mident value)): Prop := forall (i:mident), (~ (mem1 i a)) -> ((get sigma
i) = (get sigma' i)).
Axiom assigns_refl : forall (sigma:(map mident value)) (a:(set1 mident)),
(assigns sigma a sigma).
Axiom assigns_trans : forall (sigma1:(map mident value)) (sigma2:(map mident
value)) (sigma3:(map mident value)) (a:(set.Set.set mident)),
((assigns sigma1 a sigma2) /\ (assigns sigma2 a sigma3)) -> (assigns sigma1
a sigma3).
value)) (sigma3:(map mident value)) (a:(set1 mident)), ((assigns sigma1 a
sigma2) /\ (assigns sigma2 a sigma3)) -> (assigns sigma1 a sigma3).
Axiom assigns_union_left : forall (sigma:(map mident value)) (sigma':(map
mident value)) (s1:(set.Set.set mident)) (s2:(set.Set.set mident)),
(assigns sigma s1 sigma') -> (assigns sigma (set.Set.union s1 s2) sigma').
mident value)) (s1:(set1 mident)) (s2:(set1 mident)), (assigns sigma s1
sigma') -> (assigns sigma (union s1 s2) sigma').
Axiom assigns_union_right : forall (sigma:(map mident value)) (sigma':(map
mident value)) (s1:(set.Set.set mident)) (s2:(set.Set.set mident)),
(assigns sigma s2 sigma') -> (assigns sigma (set.Set.union s1 s2) sigma').
mident value)) (s1:(set1 mident)) (s2:(set1 mident)), (assigns sigma s2
sigma') -> (assigns sigma (union s1 s2) sigma').
(* Why3 assumption *)
Fixpoint stmt_writes(s:stmt) (w:(set.Set.set mident)) {struct s}: Prop :=
Fixpoint stmt_writes(s:stmt) (w:(set1 mident)) {struct s}: Prop :=
match s with
| (Sskip|(Sassert _)) => True
| (Sassign id _) => (set.Set.mem id w)
| (Sassign id _) => (mem1 id w)
| (Sseq s1 s2) => (stmt_writes s1 w) /\ (stmt_writes s2 w)
| (Sif t s1 s2) => (stmt_writes s1 w) /\ (stmt_writes s2 w)
| (Swhile _ _ body) => (stmt_writes body w)
......@@ -617,10 +693,16 @@ Axiom abstract_effects_generalize : forall (sigma:(map mident value))
(pi:(list (ident* value)%type)) (s:stmt) (f:fmla), (eval_fmla sigma pi
(abstract_effects s f)) -> (eval_fmla sigma pi f).
Axiom abstract_effects_monotonic : forall (s:stmt) (f:fmla),
forall (sigma:(map mident value)) (pi:(list (ident* value)%type)),
(eval_fmla sigma pi f) -> forall (sigma1:(map mident value)) (pi1:(list
(ident* value)%type)), (eval_fmla sigma1 pi1 (abstract_effects s f)).
Axiom abstract_effects_distrib_conj : forall (s:stmt) (p:fmla) (q:fmla)
(sigma:(map mident value)) (pi:(list (ident* value)%type)),
((eval_fmla sigma pi (abstract_effects s p)) /\ (eval_fmla sigma pi
(abstract_effects s q))) -> (eval_fmla sigma pi (abstract_effects s (Fand p
q))).
Axiom abstract_effects_monotonic : forall (s:stmt) (p:fmla) (q:fmla),
(valid_fmla (Fimplies p q)) -> forall (sigma:(map mident value)) (pi:(list
(ident* value)%type)), (eval_fmla sigma pi (abstract_effects s p)) ->
(eval_fmla sigma pi (abstract_effects s q)).
(* Why3 assumption *)
Fixpoint wp(s:stmt) (q:fmla) {struct s}: fmla :=
......
......@@ -693,17 +693,18 @@ Axiom abstract_effects_generalize : forall (sigma:(map mident value))
(pi:(list (ident* value)%type)) (s:stmt) (f:fmla), (eval_fmla sigma pi
(abstract_effects s f)) -> (eval_fmla sigma pi f).
Axiom abstract_effects_monotonic : forall (s:stmt) (p:fmla) (q:fmla),
(valid_fmla (Fimplies p q)) -> forall (sigma:(map mident value)) (pi:(list
(ident* value)%type)), (eval_fmla sigma pi (abstract_effects s p)) ->
(eval_fmla sigma pi (abstract_effects s q)).
Axiom abstract_effects_distrib_conj : forall (s:stmt) (p:fmla) (q:fmla)
(sigma:(map mident value)) (pi:(list (ident* value)%type)),
((eval_fmla sigma pi (abstract_effects s p)) /\ (eval_fmla sigma pi
(abstract_effects s q))) -> (eval_fmla sigma pi (abstract_effects s (Fand p
q))).
Axiom abstract_effects_monotonic : forall (s:stmt) (p:fmla) (q:fmla),
(valid_fmla (Fimplies p q)) -> forall (sigma:(map mident value)) (pi:(list
(ident* value)%type)), (eval_fmla sigma pi (abstract_effects s p)) ->
(eval_fmla sigma pi (abstract_effects s q)).
(* Why3 assumption *)
Fixpoint wp(s:stmt) (q:fmla) {struct s}: fmla :=
match s with
......
......@@ -4,7 +4,6 @@ Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require int.MinMax.
Require set.Set.
(* Why3 assumption *)
Inductive list (a:Type) {a_WT:WhyType a} :=
......@@ -576,32 +575,109 @@ Definition total_valid_triple(p:fmla) (s:stmt) (q:fmla): Prop :=
exists pi':(list (ident* value)%type), exists n:Z, (many_steps sigma pi s
sigma' pi' Sskip n) /\ (eval_fmla sigma' pi' q).
Axiom set1 : forall (a:Type) {a_WT:WhyType a}, Type.
Parameter set1_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (set1 a).
Existing Instance set1_WhyType.
Parameter mem1: forall {a:Type} {a_WT:WhyType a}, a -> (set1 a) -> Prop.
(* Why3 assumption *)
Definition infix_eqeq {a:Type} {a_WT:WhyType a}(s1:(set1 a)) (s2:(set1
a)): Prop := forall (x:a), (mem1 x s1) <-> (mem1 x s2).
Axiom extensionality : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set1 a))
(s2:(set1 a)), (infix_eqeq s1 s2) -> (s1 = s2).
(* Why3 assumption *)
Definition subset {a:Type} {a_WT:WhyType a}(s1:(set1 a)) (s2:(set1
a)): Prop := forall (x:a), (mem1 x s1) -> (mem1 x s2).
Axiom subset_trans : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set1 a))
(s2:(set1 a)) (s3:(set1 a)), (subset s1 s2) -> ((subset s2 s3) ->
(subset s1 s3)).
Parameter empty: forall {a:Type} {a_WT:WhyType a}, (set1 a).
(* Why3 assumption *)
Definition is_empty {a:Type} {a_WT:WhyType a}(s:(set1 a)): Prop :=
forall (x:a), ~ (mem1 x s).
Axiom empty_def1 : forall {a:Type} {a_WT:WhyType a}, (is_empty (empty :(set1
a))).
Parameter add: forall {a:Type} {a_WT:WhyType a}, a -> (set1 a) -> (set1 a).
Axiom add_def1 : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a),
forall (s:(set1 a)), (mem1 x (add y s)) <-> ((x = y) \/ (mem1 x s)).
Parameter remove: forall {a:Type} {a_WT:WhyType a}, a -> (set1 a) -> (set1
a).
Axiom remove_def1 : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a)
(s:(set1 a)), (mem1 x (remove y s)) <-> ((~ (x = y)) /\ (mem1 x s)).
Axiom subset_remove : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(set1
a)), (subset (remove x s) s).
Parameter union: forall {a:Type} {a_WT:WhyType a}, (set1 a) -> (set1 a) ->
(set1 a).
Axiom union_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set1 a))
(s2:(set1 a)) (x:a), (mem1 x (union s1 s2)) <-> ((mem1 x s1) \/ (mem1 x
s2)).
Parameter inter: forall {a:Type} {a_WT:WhyType a}, (set1 a) -> (set1 a) ->
(set1 a).
Axiom inter_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set1 a))
(s2:(set1 a)) (x:a), (mem1 x (inter s1 s2)) <-> ((mem1 x s1) /\ (mem1 x
s2)).
Parameter diff: forall {a:Type} {a_WT:WhyType a}, (set1 a) -> (set1 a) ->
(set1 a).
Axiom diff_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set1 a))
(s2:(set1 a)) (x:a), (mem1 x (diff s1 s2)) <-> ((mem1 x s1) /\ ~ (mem1 x
s2)).
Axiom subset_diff : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set1 a))
(s2:(set1 a)), (subset (diff s1 s2) s1).
Parameter choose: forall {a:Type} {a_WT:WhyType a}, (set1 a) -> a.
Axiom choose_def : forall {a:Type} {a_WT:WhyType a}, forall (s:(set1 a)),
(~ (is_empty s)) -> (mem1 (choose s) s).
Parameter all: forall {a:Type} {a_WT:WhyType a}, (set1 a).
Axiom all_def : forall {a:Type} {a_WT:WhyType a}, forall (x:a), (mem1 x
(all :(set1 a))).
(* Why3 assumption *)
Definition assigns(sigma:(map mident value)) (a:(set.Set.set mident))
(sigma':(map mident value)): Prop := forall (i:mident), (~ (set.Set.mem i
a)) -> ((get sigma i) = (get sigma' i)).
Definition assigns(sigma:(map mident value)) (a:(set1 mident)) (sigma':(map
mident value)): Prop := forall (i:mident), (~ (mem1 i a)) -> ((get sigma
i) = (get sigma' i)).
Axiom assigns_refl : forall (sigma:(map mident value)) (a:(set.Set.set
mident)), (assigns sigma a sigma).
Axiom assigns_refl : forall (sigma:(map mident value)) (a:(set1 mident)),
(assigns sigma a sigma).
Axiom assigns_trans : forall (sigma1:(map mident value)) (sigma2:(map mident