diff --git a/theories/set/Set.v b/theories/set/Set.v new file mode 100644 index 0000000000000000000000000000000000000000..8278eba4b50deb5027c43d17fb7dc1c0819eaaa4 --- /dev/null +++ b/theories/set/Set.v @@ -0,0 +1,231 @@ +(* This file is generated by Why3's Coq driver *) +(* Beware! Only edit allowed sections below *) +Require Import ZArith. +Require Import Rbase. +Add Rec LoadPath "/home/cmarche/recherche/why3/share/theories". +Add Rec LoadPath "/home/cmarche/recherche/why3/share/modules". + +Inductive set_ (X:Type) : Type := mk_set: (X -> Prop) -> set_ X. + +Definition set : forall (a:Type), Type. +(* YOU MAY EDIT THE PROOF BELOW *) +exact set_. +(* +(fun (X: Type) => X -> Prop). +*) +Defined. +(* DO NOT EDIT BELOW *) + +Definition mem: forall (a:Type), a -> (set a) -> Prop. +(* YOU MAY EDIT THE PROOF BELOW *) +intros X x s. +destruct s. +exact (P x). +Defined. +(* DO NOT EDIT BELOW *) + +Implicit Arguments mem. + +Definition infix_eqeq (a:Type)(s1:(set a)) (s2:(set a)): Prop := + forall (x:a), (mem x s1) <-> (mem x s2). +Implicit Arguments infix_eqeq. + +(* YOU MAY EDIT THE CONTEXT BELOW *) +Hint Unfold mem. +Notation "x == y" := (infix_eqeq x y) (at level 70, no associativity). +(* +Require FunctionalExtensionality. +Require ProofIrrelevance. +*) +(* DO NOT EDIT BELOW *) + +Lemma extensionality : forall (a:Type), forall (s1:(set a)) (s2:(set a)), + (infix_eqeq s1 s2) -> (s1 = s2). +(* YOU MAY EDIT THE PROOF BELOW *) +admit. +(* +intros. +apply FunctionalExtensionality.functional_extensionality. +red in H. +unfold mem in H. +intro x. +apply ProofIrrelevance.proof_irrelevance. +rewrite H. +; auto. +*) +Qed. +(* DO NOT EDIT BELOW *) + +Definition subset (a:Type)(s1:(set a)) (s2:(set a)): Prop := forall (x:a), + (mem x s1) -> (mem x s2). +Implicit Arguments subset. + +(* YOU MAY EDIT THE CONTEXT BELOW *) +(*Hint Unfold subset.*) +(* DO NOT EDIT BELOW *) + +Lemma subset_trans : forall (a:Type), forall (s1:(set a)) (s2:(set a)) + (s3:(set a)), (subset s1 s2) -> ((subset s2 s3) -> (subset s1 s3)). +(* YOU MAY EDIT THE PROOF BELOW *) +unfold subset; intuition. +Qed. +(* DO NOT EDIT BELOW *) + +Definition empty: forall (a:Type), (set a). +(* YOU MAY EDIT THE PROOF BELOW *) +exact (fun X => mk_set X (fun _ => False)). +Defined. +(* DO NOT EDIT BELOW *) + +Set Contextual Implicit. +Implicit Arguments empty. +Unset Contextual Implicit. + +Definition is_empty (a:Type)(s:(set a)): Prop := forall (x:a), ~ (mem x s). +Implicit Arguments is_empty. + +(* YOU MAY EDIT THE CONTEXT BELOW *) +(*Print Implicit empty.*) +(* DO NOT EDIT BELOW *) + +Lemma empty_def1 : forall (a:Type), (is_empty (empty:(set a))). +(* YOU MAY EDIT THE PROOF BELOW *) +unfold is_empty; intuition. +Qed. +(* DO NOT EDIT BELOW *) + +Definition add: forall (a:Type), a -> (set a) -> (set a). +(* YOU MAY EDIT THE PROOF BELOW *) +intros X x s. +destruct s. +exact (mk_set _ (fun y => P y \/ y=x)). +Defined. +(* DO NOT EDIT BELOW *) + +Implicit Arguments add. + +(* YOU MAY EDIT THE CONTEXT BELOW *) + +(* DO NOT EDIT BELOW *) + +Lemma add_def1 : forall (a:Type), forall (x:a) (y:a), forall (s:(set a)), + (mem x (add y s)) <-> ((x = y) \/ (mem x s)). +(* YOU MAY EDIT THE PROOF BELOW *) +intros; destruct s. +unfold mem,add; intuition. +Qed. +(* DO NOT EDIT BELOW *) + +Definition remove: forall (a:Type), a -> (set a) -> (set a). +(* YOU MAY EDIT THE PROOF BELOW *) +intros X x s. +destruct s. +exact (mk_set _ (fun y => y<>x /\ P y)). +Defined. +(* DO NOT EDIT BELOW *) + +Implicit Arguments remove. + +(* YOU MAY EDIT THE CONTEXT BELOW *) + +(* DO NOT EDIT BELOW *) + +Lemma remove_def1 : forall (a:Type), forall (x:a) (y:a) (s:(set a)), (mem x + (remove y s)) <-> ((~ (x = y)) /\ (mem x s)). +(* YOU MAY EDIT THE PROOF BELOW *) +intros; destruct s. +unfold mem,remove; intuition. +Qed. +(* DO NOT EDIT BELOW *) + +(* YOU MAY EDIT THE CONTEXT BELOW *) + +(* DO NOT EDIT BELOW *) + +Lemma subset_remove : forall (a:Type), forall (x:a) (s:(set a)), + (subset (remove x s) s). +(* YOU MAY EDIT THE PROOF BELOW *) +intros; destruct s. +unfold subset, remove, mem; intuition. +Qed. +(* DO NOT EDIT BELOW *) + +Definition union: forall (a:Type), (set a) -> (set a) -> (set a). +(* YOU MAY EDIT THE PROOF BELOW *) +intros X s1 s2. +destruct s1; destruct s2. +exact (mk_set _ (fun y => P y \/ P0 y)). +Defined. +(* DO NOT EDIT BELOW *) + +Implicit Arguments union. + +(* YOU MAY EDIT THE CONTEXT BELOW *) + +(* DO NOT EDIT BELOW *) + +Lemma union_def1 : forall (a:Type), forall (s1:(set a)) (s2:(set a)) (x:a), + (mem x (union s1 s2)) <-> ((mem x s1) \/ (mem x s2)). +(* YOU MAY EDIT THE PROOF BELOW *) +intros; destruct s1; destruct s2. +unfold union,mem; intuition. +Qed. +(* DO NOT EDIT BELOW *) + +Definition inter: forall (a:Type), (set a) -> (set a) -> (set a). +(* YOU MAY EDIT THE PROOF BELOW *) +intros X s1 s2. +destruct s1; destruct s2. +exact (mk_set _ (fun y => P y /\ P0 y)). +Defined. +(* DO NOT EDIT BELOW *) + +Implicit Arguments inter. + +(* YOU MAY EDIT THE CONTEXT BELOW *) + +(* DO NOT EDIT BELOW *) + +Lemma inter_def1 : forall (a:Type), forall (s1:(set a)) (s2:(set a)) (x:a), + (mem x (inter s1 s2)) <-> ((mem x s1) /\ (mem x s2)). +(* YOU MAY EDIT THE PROOF BELOW *) +intros; destruct s1; destruct s2. +unfold inter, mem; intuition. +Qed. +(* DO NOT EDIT BELOW *) + +Definition diff: forall (a:Type), (set a) -> (set a) -> (set a). +(* YOU MAY EDIT THE PROOF BELOW *) +intros X s1 s2. +destruct s1; destruct s2. +exact (mk_set _ (fun y => P y /\ ~(P0 y))). +Defined. +(* DO NOT EDIT BELOW *) + +Implicit Arguments diff. + +(* YOU MAY EDIT THE CONTEXT BELOW *) + +(* DO NOT EDIT BELOW *) + +Lemma diff_def1 : forall (a:Type), forall (s1:(set a)) (s2:(set a)) (x:a), + (mem x (diff s1 s2)) <-> ((mem x s1) /\ ~ (mem x s2)). +(* YOU MAY EDIT THE PROOF BELOW *) +intros; destruct s1; destruct s2. +unfold diff, mem; intuition. +Qed. +(* DO NOT EDIT BELOW *) + +(* YOU MAY EDIT THE CONTEXT BELOW *) + +(* DO NOT EDIT BELOW *) + +Lemma subset_diff : forall (a:Type), forall (s1:(set a)) (s2:(set a)), + (subset (diff s1 s2) s1). +(* YOU MAY EDIT THE PROOF BELOW *) +intros; destruct s1; destruct s2. +unfold subset, diff, mem; intuition. +Qed. +(* DO NOT EDIT BELOW *) + +