Skip to content

GitLab

Attention une mise à jour du serveur va être effectuée le lundi 17 mai entre 13h et 13h30. Cette mise à jour va générer une interruption du service de quelques minutes.

Commit 4eb4518f authored by MARCHE Claude's avatar MARCHE Claude
Browse files
Options

Set theory a la B, realizations

parent b7a50941
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 1042 additions and 303 deletions
Makefile.in
View file @ 4eb4518f
......@@ -884,13 +884,16 @@ COQLIBS_NUMBER = $(addprefix lib/coq/number/, $(COQLIBS_NUMBER_FILES))
COQLIBS_SET_FILES = Set
COQLIBS_SET = $(addprefix lib/coq/set/, $(COQLIBS_SET_FILES))
COQLIBS_SETTHEORY_FILES = Interval PowerSet Relation Identity Image InverseDomRan Function
COQLIBS_SETTHEORY = $(addprefix lib/coq/settheory/, $(COQLIBS_SETTHEORY_FILES))
ifeq (@enable_coq_fp_libs@,yes)
COQLIBS_FP_FILES = Rounding SingleFormat Single DoubleFormat Double
COQLIBS_FP_ALL_FILES = GenFloat $(COQLIBS_FP_FILES)
COQLIBS_FP = $(addprefix lib/coq/floating_point/, $(COQLIBS_FP_ALL_FILES))
endif
COQLIBS_FILES = lib/coq/BuiltIn $(COQLIBS_INT) $(COQLIBS_REAL) $(COQLIBS_NUMBER) $(COQLIBS_SET) $(COQLIBS_FP)
COQLIBS_FILES = lib/coq/BuiltIn $(COQLIBS_INT) $(COQLIBS_REAL) $(COQLIBS_NUMBER) $(COQLIBS_SET) $(COQLIBS_SETTHEORY) $(COQLIBS_FP)
COQV = $(addsuffix .v, $(COQLIBS_FILES))
COQVO = $(addsuffix .vo, $(COQLIBS_FILES))
......@@ -916,6 +919,8 @@ drivers/coq-realizations.aux: Makefile
echo 'theory number.'"$$f"' meta "realized" "number.'"$$f"'", "" end'; done; \
for f in $(COQLIBS_SET_FILES); do \
echo 'theory set.'"$$f"' meta "realized" "set.'"$$f"'", "" end'; done; \
for f in $(COQLIBS_SETTHEORY_FILES); do \
echo 'theory settheory.'"$$f"' meta "realized" "settheory.'"$$f"'", "" end'; done; \
for f in $(COQLIBS_FP_FILES); do \
echo 'theory floating_point.'"$$f"' meta "realized" "floating_point.'"$$f"'", "" end'; done; \
) > $@
......@@ -933,6 +938,8 @@ install_no_local::
cp $(addsuffix .vo, $(COQLIBS_NUMBER)) $(LIBDIR)/why3/coq/number/
mkdir -p $(LIBDIR)/why3/coq/set
cp $(addsuffix .vo, $(COQLIBS_SET)) $(LIBDIR)/why3/coq/set/
mkdir -p $(LIBDIR)/why3/coq/settheory
cp $(addsuffix .vo, $(COQLIBS_SETTHEORY_FILES)) $(LIBDIR)/why3/coq/settheory/
ifeq (@enable_coq_fp_libs@,yes)
mkdir -p $(LIBDIR)/why3/coq/floating_point
cp $(addsuffix .vo, $(COQLIBS_FP)) $(LIBDIR)/why3/coq/floating_point/
......@@ -957,6 +964,7 @@ update-coq: bin/why3 drivers/coq-realizations.aux
for f in $(COQLIBS_REAL_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/coq-realize.drv -T real.$$f -o lib/coq/real/; done
for f in $(COQLIBS_NUMBER_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/coq-realize.drv -T number.$$f -o lib/coq/number/; done
for f in $(COQLIBS_SET_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/coq-realize.drv -T set.$$f -o lib/coq/set/; done
for f in $(COQLIBS_SETTHEORY_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/coq-realize.drv -T settheory.$$f -o lib/coq/settheory/; done
for f in $(COQLIBS_FP_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/coq-realize.drv -T floating_point.$$f -o lib/coq/floating_point/; done
else
......
examples/hoare_logic/wp2/why3session.xml
View file @ 4eb4518f
This diff is collapsed.
examples/hoare_logic/wp2/wp2_WP_WP_WP_parameter_compute_writes_1.v
View file @ 4eb4518f
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require set.Set.
(* Why3 assumption *)
Definition unit := unit.
Parameter qtmark : Type.
Parameter at1: forall (a:Type), a -> qtmark -> a.
Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
(* Why3 assumption *)
Definition implb(x:bool) (y:bool): bool := match (x,
y) with
| (true, false) => false
| (_, _) => true
end.
(* Why3 assumption *)
Inductive datatype :=
| Tint : datatype
| Tbool : datatype .
Axiom datatype_WhyType : WhyType datatype.
Existing Instance datatype_WhyType.
(* Why3 assumption *)
Inductive operator :=
......@@ -33,6 +21,8 @@ Inductive operator :=
| Ominus : operator
| Omult : operator
| Ole : operator .
Axiom operator_WhyType : WhyType operator.
Existing Instance operator_WhyType.
(* Why3 assumption *)
Definition ident := Z.
......@@ -43,6 +33,8 @@ Inductive term :=
| Tvar : Z -> term
| Tderef : Z -> term
| Tbin : term -> operator -> term -> term .
Axiom term_WhyType : WhyType term.
Existing Instance term_WhyType.
(* Why3 assumption *)
Inductive fmla :=
......@@ -52,35 +44,40 @@ Inductive fmla :=
| Fimplies : fmla -> fmla -> fmla
| Flet : Z -> term -> fmla -> fmla
| Fforall : Z -> datatype -> fmla -> fmla .
Axiom fmla_WhyType : WhyType fmla.
Existing Instance fmla_WhyType.
(* Why3 assumption *)
Inductive value :=
| Vint : Z -> value
| Vbool : bool -> value .
Axiom value_WhyType : WhyType value.
Existing Instance value_WhyType.
Parameter map : forall (a:Type) (b:Type), Type.
Axiom map : forall (a:Type) {a_WT:WhyType a} (b:Type) {b_WT:WhyType b}, Type.
Parameter map_WhyType : forall (a:Type) {a_WT:WhyType a}
(b:Type) {b_WT:WhyType b}, WhyType (map a b).
Existing Instance map_WhyType.
Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
Implicit Arguments get.
Parameter get: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
(map a b) -> a -> b.
Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
Implicit Arguments set.
Parameter set: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
(map a b) -> a -> b -> (map a b).
Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1)
a2) = b1).
Axiom Select_eq : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
forall (m:(map a b)), forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) ->
((get (set m a1 b1) a2) = b1).
Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1)
a2) = (get m a2)).
Axiom Select_neq : forall {a:Type} {a_WT:WhyType a}
{b:Type} {b_WT:WhyType b}, forall (m:(map a b)), forall (a1:a) (a2:a),
forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1) a2) = (get m a2)).
Parameter const: forall (b:Type) (a:Type), b -> (map a b).
Set Contextual Implicit.
Implicit Arguments const.
Unset Contextual Implicit.
Parameter const: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
b -> (map a b).
Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a),
((get (const b1:(map a b)) a1) = b1).
Axiom Const : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
forall (b1:b) (a1:a), ((get (const b1:(map a b)) a1) = b1).
(* Why3 assumption *)
Definition env := (map Z value).
......@@ -101,7 +98,6 @@ Axiom eval_bin_def : forall (x:value) (op:operator) (y:value), match (x,
end.
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint eval_term(sigma:(map Z value)) (pi:(map Z value))
(t:term) {struct t}: value :=
match t with
......@@ -111,10 +107,8 @@ Fixpoint eval_term(sigma:(map Z value)) (pi:(map Z value))
| (Tbin t1 op t2) => (eval_bin (eval_term sigma pi t1) op (eval_term sigma
pi t2))
end.
Unset Implicit Arguments.
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint eval_fmla(sigma:(map Z value)) (pi:(map Z value))
(f:fmla) {struct f}: Prop :=
match f with
......@@ -128,7 +122,6 @@ Fixpoint eval_fmla(sigma:(map Z value)) (pi:(map Z value))
| (Fforall x Tbool f1) => forall (b:bool), (eval_fmla sigma (set pi x
(Vbool b)) f1)
end.
Unset Implicit Arguments.
Parameter subst_term: term -> Z -> Z -> term.
......@@ -143,7 +136,6 @@ Axiom subst_term_def : forall (e:term) (r:Z) (v:Z),
end.
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint fresh_in_term(id:Z) (t:term) {struct t}: Prop :=
match t with
| (Tconst _) => True
......@@ -151,7 +143,6 @@ Fixpoint fresh_in_term(id:Z) (t:term) {struct t}: Prop :=
| (Tderef _) => True
| (Tbin t1 _ t2) => (fresh_in_term id t1) /\ (fresh_in_term id t2)
end.
Unset Implicit Arguments.
Axiom eval_subst_term : forall (sigma:(map Z value)) (pi:(map Z value))
(e:term) (x:Z) (v:Z), (fresh_in_term v e) -> ((eval_term sigma pi
......@@ -162,7 +153,6 @@ Axiom eval_term_change_free : forall (t:term) (sigma:(map Z value)) (pi:(map
(set pi id v) t) = (eval_term sigma pi t)).
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint fresh_in_fmla(id:Z) (f:fmla) {struct f}: Prop :=
match f with
| (Fterm e) => (fresh_in_term id e)
......@@ -173,20 +163,17 @@ Fixpoint fresh_in_fmla(id:Z) (f:fmla) {struct f}: Prop :=
(fresh_in_fmla id f1))
| (Fforall y ty f1) => (~ (id = y)) /\ (fresh_in_fmla id f1)
end.
Unset Implicit Arguments.
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint subst(f:fmla) (x:Z) (v:Z) {struct f}: fmla :=
match f with
| (Fterm e) => (Fterm (subst_term e x v))
| (Fand f1 f2) => (Fand (subst f1 x v) (subst f2 x v))
| (Fnot f1) => (Fnot (subst f1 x v))
| (Fimplies f1 f2) => (Fimplies (subst f1 x v) (subst f2 x v))
| (Flet y t f1) => (Flet y t (subst f1 x v))
| (Flet y t f1) => (Flet y (subst_term t x v) (subst f1 x v))
| (Fforall y ty f1) => (Fforall y ty (subst f1 x v))
end.
Unset Implicit Arguments.
Axiom eval_subst : forall (f:fmla) (sigma:(map Z value)) (pi:(map Z value))
(x:Z) (v:Z), (fresh_in_fmla v f) -> ((eval_fmla sigma pi (subst f x v)) <->
......@@ -209,6 +196,8 @@ Inductive stmt :=
| Sif : term -> stmt -> stmt -> stmt
| Sassert : fmla -> stmt
| Swhile : term -> fmla -> stmt -> stmt .
Axiom stmt_WhyType : WhyType stmt.
Existing Instance stmt_WhyType.
Axiom check_skip : forall (s:stmt), (s = Sskip) \/ ~ (s = Sskip).
......@@ -219,9 +208,9 @@ Inductive one_step : (map Z value) -> (map Z value) -> stmt -> (map Z value)
(e:term), (one_step sigma pi (Sassign x e) (set sigma x
(eval_term sigma pi e)) pi Sskip)
| one_step_seq : forall (sigma:(map Z value)) (pi:(map Z value))
(sigmaqt:(map Z value)) (piqt:(map Z value)) (i1:stmt) (i1qt:stmt)
(i2:stmt), (one_step sigma pi i1 sigmaqt piqt i1qt) -> (one_step sigma
pi (Sseq i1 i2) sigmaqt piqt (Sseq i1qt i2))
(sigma':(map Z value)) (pi':(map Z value)) (i1:stmt) (i1':stmt)
(i2:stmt), (one_step sigma pi i1 sigma' pi' i1') -> (one_step sigma pi
(Sseq i1 i2) sigma' pi' (Sseq i1' i2))
| one_step_seq_skip : forall (sigma:(map Z value)) (pi:(map Z value))
(i:stmt), (one_step sigma pi (Sseq Sskip i) sigma pi i)
| one_step_if_true : forall (sigma:(map Z value)) (pi:(map Z value))
......@@ -272,141 +261,47 @@ Definition valid_fmla(p:fmla): Prop := forall (sigma:(map Z value)) (pi:(map
(* Why3 assumption *)
Definition valid_triple(p:fmla) (i:stmt) (q:fmla): Prop := forall (sigma:(map
Z value)) (pi:(map Z value)), (eval_fmla sigma pi p) ->
forall (sigmaqt:(map Z value)) (piqt:(map Z value)) (n:Z),
(many_steps sigma pi i sigmaqt piqt Sskip n) -> (eval_fmla sigmaqt piqt q).
Axiom skip_rule : forall (q:fmla), (valid_triple q Sskip q).
Axiom assign_rule : forall (q:fmla) (x:Z) (id:Z) (e:term), (fresh_in_fmla id
q) -> (valid_triple (Flet id e (subst q x id)) (Sassign x e) q).
Axiom seq_rule : forall (p:fmla) (q:fmla) (r:fmla) (i1:stmt) (i2:stmt),
((valid_triple p i1 r) /\ (valid_triple r i2 q)) -> (valid_triple p
(Sseq i1 i2) q).
Axiom if_rule : forall (e:term) (p:fmla) (q:fmla) (i1:stmt) (i2:stmt),
((valid_triple (Fand p (Fterm e)) i1 q) /\ (valid_triple (Fand p
(Fnot (Fterm e))) i2 q)) -> (valid_triple p (Sif e i1 i2) q).
Axiom assert_rule : forall (f:fmla) (p:fmla), (valid_fmla (Fimplies p f)) ->
(valid_triple p (Sassert f) p).
Axiom assert_rule_ext : forall (f:fmla) (p:fmla), (valid_triple (Fimplies f
p) (Sassert f) p).
Axiom while_rule : forall (e:term) (inv:fmla) (i:stmt),
(valid_triple (Fand (Fterm e) inv) i inv) -> (valid_triple inv (Swhile e
inv i) (Fand (Fnot (Fterm e)) inv)).
Axiom while_rule_ext : forall (e:term) (inv:fmla) (invqt:fmla) (i:stmt),
(valid_fmla (Fimplies invqt inv)) -> ((valid_triple (Fand (Fterm e) invqt)
i invqt) -> (valid_triple invqt (Swhile e inv i) (Fand (Fnot (Fterm e))
invqt))).
Axiom consequence_rule : forall (p:fmla) (pqt:fmla) (q:fmla) (qqt:fmla)
(i:stmt), (valid_fmla (Fimplies pqt p)) -> ((valid_triple p i q) ->
((valid_fmla (Fimplies q qqt)) -> (valid_triple pqt i qqt))).
Parameter set1 : forall (a:Type), Type.
Parameter mem: forall (a:Type), a -> (set1 a) -> Prop.
Implicit Arguments mem.
(* Why3 assumption *)
Definition infix_eqeq (a:Type)(s1:(set1 a)) (s2:(set1 a)): Prop :=
forall (x:a), (mem x s1) <-> (mem x s2).
Implicit Arguments infix_eqeq.
Axiom extensionality : forall (a:Type), forall (s1:(set1 a)) (s2:(set1 a)),
(infix_eqeq s1 s2) -> (s1 = s2).
(* Why3 assumption *)
Definition subset (a:Type)(s1:(set1 a)) (s2:(set1 a)): Prop := forall (x:a),
(mem x s1) -> (mem x s2).
Implicit Arguments subset.
Axiom subset_trans : forall (a:Type), forall (s1:(set1 a)) (s2:(set1 a))
(s3:(set1 a)), (subset s1 s2) -> ((subset s2 s3) -> (subset s1 s3)).
Parameter empty: forall (a:Type), (set1 a).
Set Contextual Implicit.
Implicit Arguments empty.
Unset Contextual Implicit.
Z value)) (pi:(map Z value)), (eval_fmla sigma pi p) -> forall (sigma':(map
Z value)) (pi':(map Z value)) (n:Z), (many_steps sigma pi i sigma' pi'
Sskip n) -> (eval_fmla sigma' pi' q).
(* Why3 assumption *)
Definition is_empty (a:Type)(s:(set1 a)): Prop := forall (x:a), ~ (mem x s).
Implicit Arguments is_empty.
Axiom empty_def1 : forall (a:Type), (is_empty (empty :(set1 a))).
Parameter add: forall (a:Type), a -> (set1 a) -> (set1 a).
Implicit Arguments add.
Axiom add_def1 : forall (a:Type), forall (x:a) (y:a), forall (s:(set1 a)),
(mem x (add y s)) <-> ((x = y) \/ (mem x s)).
Parameter remove: forall (a:Type), a -> (set1 a) -> (set1 a).
Implicit Arguments remove.
Axiom remove_def1 : forall (a:Type), forall (x:a) (y:a) (s:(set1 a)), (mem x
(remove y s)) <-> ((~ (x = y)) /\ (mem x s)).
Definition assigns(sigma:(map Z value)) (a:(set.Set.set Z)) (sigma':(map Z
value)): Prop := forall (i:Z), (~ (set.Set.mem i a)) -> ((get sigma
i) = (get sigma' i)).
Axiom subset_remove : forall (a:Type), forall (x:a) (s:(set1 a)),
(subset (remove x s) s).
Axiom assigns_refl : forall (sigma:(map Z value)) (a:(set.Set.set Z)),
(assigns sigma a sigma).
Parameter union: forall (a:Type), (set1 a) -> (set1 a) -> (set1 a).
Implicit Arguments union.
Axiom assigns_trans : forall (sigma1:(map Z value)) (sigma2:(map Z value))
(sigma3:(map Z value)) (a:(set.Set.set Z)), ((assigns sigma1 a sigma2) /\
(assigns sigma2 a sigma3)) -> (assigns sigma1 a sigma3).
Axiom union_def1 : forall (a:Type), forall (s1:(set1 a)) (s2:(set1 a)) (x:a),
(mem x (union s1 s2)) <-> ((mem x s1) \/ (mem x s2)).
Axiom assigns_union_left : forall (sigma:(map Z value)) (sigma':(map Z
value)) (s1:(set.Set.set Z)) (s2:(set.Set.set Z)), (assigns sigma s1
sigma') -> (assigns sigma (set.Set.union s1 s2) sigma').
Parameter inter: forall (a:Type), (set1 a) -> (set1 a) -> (set1 a).
Implicit Arguments inter.
Axiom inter_def1 : forall (a:Type), forall (s1:(set1 a)) (s2:(set1 a)) (x:a),
(mem x (inter s1 s2)) <-> ((mem x s1) /\ (mem x s2)).
Parameter diff: forall (a:Type), (set1 a) -> (set1 a) -> (set1 a).
Implicit Arguments diff.
Axiom diff_def1 : forall (a:Type), forall (s1:(set1 a)) (s2:(set1 a)) (x:a),
(mem x (diff s1 s2)) <-> ((mem x s1) /\ ~ (mem x s2)).
Axiom subset_diff : forall (a:Type), forall (s1:(set1 a)) (s2:(set1 a)),
(subset (diff s1 s2) s1).
Parameter all: forall (a:Type), (set1 a).
Set Contextual Implicit.
Implicit Arguments all.
Unset Contextual Implicit.
Axiom all_def : forall (a:Type), forall (x:a), (mem x (all :(set1 a))).
Axiom assigns_union_right : forall (sigma:(map Z value)) (sigma':(map Z
value)) (s1:(set.Set.set Z)) (s2:(set.Set.set Z)), (assigns sigma s2
sigma') -> (assigns sigma (set.Set.union s1 s2) sigma').
(* Why3 assumption *)
Definition assigns(sigma:(map Z value)) (a:(set1 Z)) (sigmaqt:(map Z
value)): Prop := forall (i:Z), (~ (mem i a)) -> ((get sigma
i) = (get sigmaqt i)).
Axiom assigns_empty : forall (sigma:(map Z value)), (assigns sigma
(empty :(set1 Z)) sigma).
Axiom assigns_union_left : forall (sigma:(map Z value)) (sigmaqt:(map Z
value)) (s1:(set1 Z)) (s2:(set1 Z)), (assigns sigma s1 sigmaqt) ->
(assigns sigma (union s1 s2) sigmaqt).
Axiom assigns_union_right : forall (sigma:(map Z value)) (sigmaqt:(map Z
value)) (s1:(set1 Z)) (s2:(set1 Z)), (assigns sigma s2 sigmaqt) ->
(assigns sigma (union s1 s2) sigmaqt).
Fixpoint stmt_writes(i:stmt) (w:(set.Set.set Z)) {struct i}: Prop :=
match i with
| (Sskip|(Sassert _)) => True
| (Sassign id _) => (set.Set.mem id w)
| ((Sseq s1 s2)|(Sif _ s1 s2)) => (stmt_writes s1 w) /\ (stmt_writes s2 w)
| (Swhile _ _ s) => (stmt_writes s w)
end.
(* Why3 goal *)
Theorem WP_parameter_compute_writes : forall (s:stmt),
match s with
| Sskip => True
| (Sassign i _) => forall (sigma:(map Z value)) (pi:(map Z value))
(sigmaqt:(map Z value)) (piqt:(map Z value)) (n:Z), (many_steps sigma
pi s sigmaqt piqt Sskip n) -> (assigns sigma (add i (empty :(set1 Z)))
sigmaqt)
(sigma':(map Z value)) (pi':(map Z value)) (n:Z), (many_steps sigma pi
s sigma' pi' Sskip n) -> (assigns sigma (set.Set.add i
(set.Set.empty :(set.Set.set Z))) sigma')
| (Sseq s1 s2) => True
| (Sif _ s1 s2) => True
| (Swhile _ _ s1) => True
......@@ -417,7 +312,7 @@ red; intros.
inversion H; subst; clear H.
inversion H1; subst; clear H1.
inversion H2; subst; clear H2.
rewrite add_def1 in H0.
rewrite set.Set.add_def1 in H0.
rewrite Select_neq; auto.
inversion H.
Qed.
......
lib/coq/set/Set.v
View file @ 4eb4518f
......@@ -4,31 +4,35 @@ Require Import BuiltIn.
Require BuiltIn.
Require Import ClassicalEpsilon.
Require Import FunctionalExtensionality.
(* "it is folklore that the two are consistent" *)
Variable eq : forall {a:Type} {a_WT:WhyType a}, a -> a -> bool.
Lemma predicate_extensionality:
forall A (P Q : A -> Prop),
(forall x, P x <-> Q x) -> P = Q.
Admitted.
(* "it is folklore that the two are consistent" *)
(*
Hypothesis eq_dec:
forall {a:Type} {a_WT:WhyType a} (x y:a),
if eq x y then x=y else x<>y.
x=y \/ x<>y.
*)
(* Why3 goal *)
Definition set : forall (a:Type) {a_WT:WhyType a}, Type.
intros.
exact (a -> bool).
exact (a -> Prop).
Defined.
Global Instance set_WhyType : forall a {a_WT:WhyType a}, WhyType (set a).
Proof.
intros.
exact (fun _ => true).
exact (fun _ => True).
Qed.
(* Why3 goal *)
Definition mem: forall {a:Type} {a_WT:WhyType a}, a -> (set a) -> Prop.
intros a a_WT x s.
exact (s x = true).
exact (s x).
Defined.
Hint Unfold mem.
......@@ -44,18 +48,21 @@ Notation "x == y" := (infix_eqeq x y) (at level 70, no associativity).
Lemma extensionality : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)), (infix_eqeq s1 s2) -> (s1 = s2).
intros a a_WT s1 s2 h1.
extensionality x.
red in h1.
unfold mem in h1.
generalize (h1 x); clear h1.
intro H.
destruct (s1 x); destruct (s2 x); intuition.
apply predicate_extensionality; intro x.
apply h1.
Qed.
(* Why3 assumption *)
Definition subset {a:Type} {a_WT:WhyType a}(s1:(set a)) (s2:(set a)): Prop :=
forall (x:a), (mem x s1) -> (mem x s2).
(* Why3 goal *)
Lemma subset_refl : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
(subset s s).
intros a a_WT s.
unfold subset; auto.
Qed.
(* Why3 goal *)
Lemma subset_trans : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)) (s3:(set a)), (subset s1 s2) -> ((subset s2 s3) -> (subset s1
......@@ -67,7 +74,7 @@ Qed.
(* Why3 goal *)
Definition empty: forall {a:Type} {a_WT:WhyType a}, (set a).
intros.
exact (fun _ => false).
exact (fun _ => False).
Defined.
(* Why3 assumption *)
......@@ -84,33 +91,27 @@ Qed.
(* Why3 goal *)
Definition add: forall {a:Type} {a_WT:WhyType a}, a -> (set a) -> (set a).
intros a a_WT x s.
exact (fun y => orb (eq x y) (s y)).
exact (fun y => x = y \/ s y).
Defined.
(* Why3 goal *)
Lemma add_def1 : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a),
forall (s:(set a)), (mem x (add y s)) <-> ((x = y) \/ (mem x s)).
intros a a_WT x y s.
unfold add, mem.
generalize (eq_dec y x); intro.
rewrite Bool.orb_true_iff.
destruct (eq y x); intuition.
unfold add, mem; intuition.
Qed.
(* Why3 goal *)
Definition remove: forall {a:Type} {a_WT:WhyType a}, a -> (set a) -> (set a).
intros a a_WT x s.
exact (fun y => andb (negb (eq x y)) (s y)).
exact (fun y => x <> y /\ s y).
Defined.
(* Why3 goal *)
Lemma remove_def1 : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a)
(s:(set a)), (mem x (remove y s)) <-> ((~ (x = y)) /\ (mem x s)).
intros a a_WT x y s.
unfold mem, remove.
generalize (eq_dec y x); intro.
rewrite Bool.andb_true_iff.
destruct (eq y x); intuition.
unfold remove, mem; intuition.
Qed.
(* Why3 goal *)
......@@ -125,50 +126,42 @@ Qed.
Definition union: forall {a:Type} {a_WT:WhyType a}, (set a) -> (set a) ->
(set a).
intros a a_WT s1 s2.
exact (fun x => orb (s1 x) (s2 x)).
exact (fun x => s1 x \/ s2 x).
Defined.