Setup for finite sets library.

FiniteSets/_CoqProject

@@ -0,0 +1,5 @@
+-R . "" COQC = hoqc COQDEP = hoqdep
+
+definition.v
+operations.v
+properties.v

FiniteSets/definition.v

@@ -0,0 +1,207 @@
+Require Import HoTT.
+Require Export HoTT.
+
+Module Export definition.
+ 
+Section FSet.
+Variable A : Type.
+
+Private Inductive FSet : Type :=
+  | E : FSet
+  | L : A -> FSet
+  | U : FSet -> FSet -> FSet.
+
+Notation "{| x |}" :=  (L x).
+Infix "∪" := U (at level 8, right associativity).
+Notation "∅" := E.
+
+Axiom assoc : forall (x y z : FSet ),
+  x ∪ (y ∪ z) = (x ∪ y) ∪ z.
+
+Axiom comm : forall (x y : FSet),
+  x ∪ y = y ∪ x.
+
+Axiom nl : forall (x : FSet),
+  ∅ ∪ x = x.
+
+Axiom nr : forall (x : FSet),
+  x ∪ ∅ = x.
+
+Axiom idem : forall (x : A),
+  {| x |} ∪ {|x|} = {|x|}.
+
+Axiom trunc : IsHSet FSet.
+
+Fixpoint FSet_rec
+  (P : Type)
+  (H: IsHSet P)
+  (e : P)
+  (l : A -> P)
+  (u : P -> P -> P)
+  (assocP : forall (x y z : P), u x (u y z) = u (u x y) z)
+  (commP : forall (x y : P), u x y = u y x)
+  (nlP : forall (x : P), u e x = x)
+  (nrP : forall (x : P), u x e = x)
+  (idemP : forall (x : A), u (l x) (l x) = l x)
+  (x : FSet)
+  {struct x}
+  : P
+  := (match x return _ -> _ -> _ -> _ -> _ -> _ -> P with
+        | E => fun _ => fun _ => fun _ => fun _ => fun _ => fun _ => e
+        | L a => fun _ => fun _ => fun _ => fun _ => fun _ => fun _ => l a
+        | U y z => fun _ => fun _ => fun _ => fun _ => fun _ => fun _ => u 
+           (FSet_rec P H e l u assocP commP nlP nrP idemP y)
+           (FSet_rec P H e l u assocP commP nlP nrP idemP z)
+      end) assocP commP nlP nrP idemP H.
+
+Axiom FSet_rec_beta_assoc : forall
+  (P : Type)
+  (H: IsHSet P)
+  (e : P)
+  (l : A -> P)
+  (u : P -> P -> P)
+  (assocP : forall (x y z : P), u x (u y z) = u (u x y) z)
+  (commP : forall (x y : P), u x y = u y x)
+  (nlP : forall (x : P), u e x = x)
+  (nrP : forall (x : P), u x e = x)
+  (idemP : forall (x : A), u (l x) (l x) = l x)
+  (x y z : FSet),
+  ap (FSet_rec P H e l u assocP commP nlP nrP idemP) (assoc x y z) 
+  =
+  (assocP (FSet_rec P H e l u assocP commP nlP nrP idemP x)
+          (FSet_rec P H e l u assocP commP nlP nrP idemP y)
+          (FSet_rec P H e l u assocP commP nlP nrP idemP z)
+  ).
+
+Axiom FSet_rec_beta_comm : forall
+  (P : Type)
+  (H: IsHSet P)
+  (e : P)
+  (l : A -> P)
+  (u : P -> P -> P)
+  (assocP : forall (x y z : P), u x (u y z) = u (u x y) z)
+  (commP : forall (x y : P), u x y = u y x)
+  (nlP : forall (x : P), u e x = x)
+  (nrP : forall (x : P), u x e = x)
+  (idemP : forall (x : A), u (l x) (l x) = l x)
+  (x y : FSet),
+  ap (FSet_rec P H e l u assocP commP nlP nrP idemP) (comm x y)
+  =
+  (commP (FSet_rec P H e l u assocP commP nlP nrP idemP x)
+         (FSet_rec P H e l u assocP commP nlP nrP idemP y)
+  ).
+
+Axiom FSet_rec_beta_nl : forall
+  (P : Type)
+  (H: IsHSet P)
+  (e : P)
+  (l : A -> P)
+  (u : P -> P -> P)
+  (assocP : forall (x y z : P), u x (u y z) = u (u x y) z)
+  (commP : forall (x y : P), u x y = u y x)
+  (nlP : forall (x : P), u e x = x)
+  (nrP : forall (x : P), u x e = x)
+  (idemP : forall (x : A), u (l x) (l x) = l x)
+  (x : FSet),
+  ap (FSet_rec P H e l u assocP commP nlP nrP idemP) (nl x)
+  =
+  (nlP (FSet_rec P H e l u assocP commP nlP nrP idemP x)
+  ).
+
+Axiom FSet_rec_beta_nr : forall
+  (P : Type)
+  (H: IsHSet P)
+  (e : P)
+  (l : A -> P)
+  (u : P -> P -> P)
+  (assocP : forall (x y z : P), u x (u y z) = u (u x y) z)
+  (commP : forall (x y : P), u x y = u y x)
+  (nlP : forall (x : P), u e x = x)
+  (nrP : forall (x : P), u x e = x)
+  (idemP : forall (x : A), u (l x) (l x) = l x)
+  (x : FSet),
+  ap (FSet_rec P H e l u assocP commP nlP nrP idemP) (nr x)
+  =
+  (nrP (FSet_rec P H e l u assocP commP nlP nrP idemP x)
+  ).
+
+Axiom FSet_rec_beta_idem : forall
+  (P : Type)
+  (H: IsHSet P)
+  (e : P)
+  (l : A -> P)
+  (u : P -> P -> P)
+  (assocP : forall (x y z : P), u x (u y z) = u (u x y) z)
+  (commP : forall (x y : P), u x y = u y x)
+  (nlP : forall (x : P), u e x = x)
+  (nrP : forall (x : P), u x e = x)
+  (idemP : forall (x : A), u (l x) (l x) = l x)
+  (x : A),
+  ap (FSet_rec P H e l u assocP commP nlP nrP idemP) (idem x)
+  =
+  idemP x.
+
+End FSet.
+Section FSet_induction.
+Arguments E {_}.
+Arguments U {_} _ _.
+Arguments L {_} _.
+Arguments assoc {_} _ _ _.
+Arguments comm {_} _ _.
+Arguments nl {_} _.
+Arguments nr {_} _.
+Arguments idem {_} _.
+Variable A: Type.
+Variable  (P : FSet A -> Type).
+Variable  (H :  forall a : FSet A, IsHSet (P a)).
+Variable  (eP : P E).
+Variable  (lP : forall a: A, P (L a)).
+Variable  (uP : forall (x y: FSet A), P x -> P y -> P (U x y)).
+Variable  (assocP : forall (x y z : FSet A) 
+                   (px: P x) (py: P y) (pz: P z),
+  assoc x y z #
+   (uP      x    (U y z)          px        (uP y z py pz)) 
+  = 
+   (uP   (U x y)    z       (uP x y px py)          pz)).
+Variable  (commP : forall (x y: FSet A) (px: P x) (py: P y),
+  comm x y #
+  uP x y px py = uP y x py px).
+Variable  (nlP : forall (x : FSet A) (px: P x), 
+  nl x # uP E x eP px = px).
+Variable  (nrP : forall (x : FSet A) (px: P x), 
+  nr x # uP x E px eP = px).
+Variable  (idemP : forall (x : A), 
+  idem x # uP (L x) (L x) (lP x) (lP x) = lP x).
+
+(* Induction principle *)
+Fixpoint FSet_ind
+  (x : FSet A)
+  {struct x}
+  : P x
+  := (match x return _ -> _ -> _ -> _ -> _ -> _ -> P x with
+        | E => fun _ => fun _ => fun _ => fun _ => fun _ => fun _ => eP
+        | L a => fun _ => fun _ => fun _ => fun _ => fun _ => fun _ => lP a
+        | U y z => fun _ => fun _ => fun _ => fun _ => fun _ => fun _ => uP y z
+           (FSet_ind y)
+           (FSet_ind z)
+      end) H assocP commP nlP nrP idemP.
+
+
+Axiom FSet_ind_beta_assoc : forall (x y z : FSet A),
+  apD FSet_ind (assoc x y z) =
+  (assocP x y z (FSet_ind x)  (FSet_ind y) (FSet_ind z)).
+
+Axiom FSet_ind_beta_comm : forall (x y : FSet A),
+  apD FSet_ind (comm x y) = (commP x y (FSet_ind x) (FSet_ind y)).
+
+Axiom FSet_ind_beta_nl : forall (x : FSet A),
+  apD FSet_ind (nl x) = (nlP x (FSet_ind x)).
+
+Axiom FSet_ind_beta_nr : forall (x : FSet A),
+  apD FSet_ind (nr x) = (nrP x (FSet_ind x)).
+
+Axiom FSet_ind_beta_idem : forall (x : A), apD FSet_ind (idem x) = idemP x.
+
+
+End FSet_induction.
+End definition.

FiniteSets/operations.v

@@ -0,0 +1,63 @@
+Require Import HoTT.
+Require Export HoTT.
+Require Import definition.
+(*Set Implicit Arguments.*)
+Arguments E {_}.
+Arguments U {_} _ _.
+Arguments L {_} _.
+Arguments assoc {_} _ _ _.
+Arguments comm {_} _ _.
+Arguments nl {_} _.
+Arguments nr {_} _.
+Arguments idem {_} _.
+
+Section operations.
+
+Variable A : Type.
+Parameter A_eqdec : forall (x y : A), Decidable (x = y).
+Definition deceq (x y : A) :=
+  if dec (x = y) then true else false.
+
+Definition isIn : A -> FSet A -> Bool.
+Proof.
+intros a.
+simple refine (FSet_rec A _ _ _ _ _ _ _ _ _ _).
+- exact false.
+- intro a'. apply (deceq a a').
+- apply orb. 
+- intros x y z. destruct x; reflexivity.
+- intros x y. destruct x, y; reflexivity.
+- intros x. reflexivity. 
+- intros x. destruct x; reflexivity.
+- intros a'. destruct (deceq a a'); reflexivity.
+Defined.
+
+Infix "∈" := isIn (at level 9, right associativity).
+
+Definition comprehension : 
+  (A -> Bool) -> FSet A -> FSet A.
+Proof.
+intros P.
+simple refine (FSet_rec A _ _ _ _ _ _ _ _ _ _).
+- apply E.
+- intro a.
+  refine (if (P a) then L a else E).
+- apply U.
+- intros. cbv. apply assoc.
+- intros. cbv. apply comm.
+- intros. cbv. apply nl.
+- intros. cbv. apply nr.
+- intros. cbv. 
+  destruct (P x); simpl.
+  + apply idem.
+  + apply nl.
+Defined.
+
+Definition intersection : 
+  FSet A -> FSet A -> FSet A.
+Proof.
+intros X Y.
+apply (comprehension (fun (a : A) => isIn a X) Y).
+Defined.
+
+End operations.

FiniteSets/properties.v

@@ -0,0 +1,271 @@
+Require Import HoTT.
+Require Export HoTT.
+Require Import definition.
+Require Import operations.
+Section properties.
+
+Arguments E {_}.
+Arguments U {_} _ _.
+Arguments L {_} _.
+Arguments assoc {_} _ _ _.
+Arguments comm {_} _ _.
+Arguments nl {_} _.
+Arguments nr {_} _.
+Arguments idem {_} _.
+Arguments isIn {_} _ _.
+Arguments comprehension {_} _ _.
+Arguments intersection {_} _ _.
+
+Variable A : Type.
+Parameter A_eqdec : forall (x y : A), Decidable (x = y).
+Definition deceq (x y : A) :=
+  if dec (x = y) then true else false.
+  
+Theorem deceq_sym : forall x y, deceq x y = deceq y x.
+Proof.
+intros x y.
+unfold deceq.
+destruct (dec (x = y)) ; destruct (dec (y = x)) ; cbn.
+- reflexivity. 
+- pose (n (p^)) ; contradiction.
+- pose (n (p^)) ; contradiction.
+- reflexivity.
+Defined.
+  
+ 
+Lemma comprehension_false: forall Y: FSet A, 
+	    comprehension (fun a => isIn a E) Y = E.
+Proof.
+simple refine (FSet_ind _ _ _ _ _ _ _ _ _ _ _); 
+try (intros; apply set_path2).
+- cbn. reflexivity.
+- cbn. reflexivity.
+- intros x y IHa IHb.
+  cbn.
+  rewrite IHa.
+  rewrite IHb.
+  rewrite nl.
+  reflexivity.
+Defined.
+
+
+Lemma isIn_singleton_eq (a b: A) : isIn a  (L b) = true -> a = b.
+Proof. unfold isIn. simpl. unfold operations.deceq.
+destruct (dec (a = b)). intro. apply p.
+intro X. 
+contradiction (false_ne_true X).
+Defined.
+
+Lemma isIn_empty_false (a: A) : isIn a E = true -> Empty.
+Proof. 
+cbv. intro X.
+contradiction (false_ne_true X). 
+Defined.
+
+Lemma isIn_union (a: A) (X Y: FSet A) : 
+	    isIn a (U X Y) = (isIn a X || isIn a Y)%Bool.
+Proof. reflexivity. Qed. 
+
+
+Theorem comprehension_or : forall ϕ ψ (x: FSet A),
+    comprehension (fun a => orb (ϕ a) (ψ a)) x = U (comprehension ϕ x) 
+    (comprehension ψ x).
+Proof.
+intros ϕ ψ.
+simple refine (FSet_ind A _ _ _ _ _ _ _ _ _ _) ; try (intros ; apply set_path2). 
+- cbn. symmetry ; apply nl.
+- cbn. intros.
+  destruct (ϕ a) ; destruct (ψ a) ; symmetry.
+  * apply idem.
+  * apply nr. 
+  * apply nl.
+  * apply nl.
+- simpl. intros x y P Q.
+  cbn. 
+  rewrite P.
+  rewrite Q.
+  rewrite <- assoc.
+  rewrite (assoc  (comprehension ψ x)).
+  rewrite (comm  (comprehension ψ x) (comprehension ϕ y)).
+  rewrite <- assoc.
+  rewrite <- assoc.
+  reflexivity.
+Defined.
+
+Theorem intersection_isIn : forall a (x y: FSet A),
+    isIn a (intersection x y) = andb (isIn a x) (isIn a y).
+Proof.
+Admitted.
+(*
+intros a.
+simple refine (FSet_ind A _ _ _ _ _ _ _ _ _ _) ; cbn.
+- intros y.
+  rewrite intersection_E.
+  reflexivity.
+- intros b y.
+  rewrite intersection_La.
+  unfold deceq.
+  destruct (dec (a = b)) ; cbn.
+  * rewrite p.
+    destruct (isIn b y).
+    + cbn.
+      unfold deceq.
+      destruct (dec (b = b)).
+      { reflexivity. }
+      { pose (n idpath). contradiction. }
+    + reflexivity.
+  * destruct (isIn b y).
+    + cbn.
+      unfold deceq.
+      destruct (dec (a = b)).
+      { pose (n p). contradiction. }
+      { reflexivity. }
+    + reflexivity.
+- intros x y P Q z.
+  enough (intersection (U x y) z = U (intersection x z) (intersection y z)).
+  rewrite X.
+  cbn.
+  rewrite P.
+  rewrite Q.
+  destruct (isIn a x) ; destruct (isIn a y) ; destruct (isIn a z) ; reflexivity.
+  admit.
+Admitted.
+*)
+
+
+Theorem union_idem : forall x: FSet A, U x x = x.
+Proof.
+simple refine (FSet_ind A _ _ _ _ _ _ _ _ _ _) ; 
+try (intros ; apply set_path2) ; cbn.
+- apply nl.
+- apply idem.
+- intros x y P Q.
+  rewrite assoc.
+  rewrite (comm x y).
+  rewrite <- (assoc y x x).
+  rewrite P.
+  rewrite (comm y x).
+  rewrite <- (assoc x y y).
+  rewrite Q.
+  reflexivity.
+Defined.
+
+Lemma intersection_0l: forall X: FSet A, intersection E X = E.
+Proof.       
+simple refine (FSet_ind A _ _ _ _ _ _ _ _ _ _) ; 
+try (intros ; apply set_path2).
+- reflexivity.
+- intro a.
+  reflexivity.
+- unfold intersection.
+  intros x y P Q.
+  cbn.
+  rewrite P.
+  rewrite Q.
+  apply nl.
+Defined.
+
+Definition intersection_0r (X: FSet A): intersection X E = E := idpath.
+
+
+     
+
+Lemma intersection_comm (X Y: FSet A): intersection X Y = intersection Y X.
+Proof.
+(*
+simple refine (FSet_ind A _ _ _ _ _ _ _ _ _ _ X) ;  
+try (intros; apply set_path2).
+- cbn. unfold intersection. apply comprehension_false.
+- cbn. unfold intersection. intros a.
+  hrecursion Y; try (intros; apply set_path2).
+  + cbn. reflexivity.
+  + cbn. intros.
+  		destruct  (dec (a0 = a)). 
+  		rewrite p. destruct (dec (a=a)).
+  		reflexivity.
+  		contradiction n. 
+  		reflexivity. 
+		destruct  (dec (a = a0)).
+		contradiction n. apply p^. reflexivity.
+ 	+ cbn -[isIn]. intros Y1 Y2 IH1 IH2.
+ 	 	rewrite IH1. 
+ 	 	rewrite IH2. 	 	
+ 	 	apply 	(comprehension_union (L a)).
+- intros X1 X2 IH1 IH2.
+  cbn.
+  unfold intersection in *.
+  rewrite <- IH1.
+  rewrite <- IH2. symmetry.
+	apply comprehension_union.
+Defined.*)
+Admitted.
+
+Lemma comprehension_union (X Y Z: FSet A) : 
+	U (comprehension (fun a => isIn a Y) X)
+	  (comprehension (fun a => isIn a Z) X) =
+	  comprehension (fun a => isIn a (U Y Z)) X.
+Proof.
+Admitted.
+(*
+hrecursion X; try (intros; apply set_path2).
+- cbn. apply nl.
+- cbn. intro a. 
+		destruct (isIn a Y); simpl;
+		destruct (isIn a Z); simpl.
+		apply idem.
+		apply nr.
+		apply nl.
+		apply nl.
+- cbn. intros X1 X2 IH1 IH2.
+	rewrite assoc.
+	rewrite (comm _ (comprehension (fun a : A => isIn a Y) X1) 
+				  (comprehension (fun a : A => isIn a Y) X2)).
+  rewrite <- (assoc _   
+  				  (comprehension (fun a : A => isIn a Y) X2)
+       		 (comprehension (fun a : A => isIn a Y) X1)
+       		 (comprehension (fun a : A => isIn a Z) X1)
+       		 ).
+  rewrite IH1.
+  rewrite comm.
+  rewrite assoc. 
+  rewrite (comm _ (comprehension (fun a : A => isIn a Z) X2) _).
+  rewrite IH2.
+  apply comm.
+Defined.*)
+
+Theorem intersection_assoc : forall (x y z: FSet A),
+    intersection x (intersection y z) = intersection (intersection x y) z.
+Admitted.
+(*
+simple refine (FSet_ind A _ _ _ _ _ _ _ _ _ _) ; try (intros ; apply set_path2).
+- intros y z.
+  cbn.
+  rewrite intersection_E.
+  rewrite intersection_E.
+  rewrite intersection_E.
+  reflexivity.
+- intros a y z.
+  cbn.
+  rewrite intersection_La.
+  rewrite intersection_La.
+  rewrite intersection_isIn.
+  destruct (isIn a y).
+  * rewrite intersection_La.
+    destruct (isIn a z).
+    + reflexivity.
+    + reflexivity.
+  * rewrite intersection_E.
+    reflexivity.      
+- unfold intersection. cbn.
+  intros x y P Q z z'.
+  rewrite comprehension_or.
+  rewrite P.
+  rewrite Q.
+  rewrite comprehension_or.
+  cbn.
+  rewrite comprehension_or.
+  reflexivity.
+*)
+
+End properties.
+