Commit 473adf47 authored by MARCHE Claude's avatar MARCHE Claude

realization of Sets

Circumvent problem with implicits
parent 47bb41d1
(* 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 *)
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment