Started implementation on enumerability.

Author: klinashka

code/Decidability/DecidablePredicates.v

@@ -1,4 +1,5 @@
 Require Import init.imports.
+Require Import Inductive.Predicates.
 
 Section Definitions.
 
@@ -108,7 +109,7 @@ End Properties.
 
 Section ClosureProperties.
 
-  Lemma decidabledisj {X : UU} (p q : X → hProp) : (deptypeddecider p) → (deptypeddecider q) → (deptypeddecider (λ (x : X), (p x) ∨ (q x))).
+  Lemma decidabledisj {X : UU} (p q : X → hProp) : (deptypeddecider p) → (deptypeddecider q) → (deptypeddecider (preddisj p q)).
   Proof.
     intros decp decq x.
     induction (decp x).
@@ -125,7 +126,7 @@ Section ClosureProperties.
         * exact (sumofmaps b b0).
   Qed.
 
-  Lemma decidableconj {X : UU} (p q : X → hProp) : (deptypeddecider p) → (deptypeddecider q) → (deptypeddecider (λ (x : X), (p x) ∧ (q x))).
+  Lemma decidableconj {X : UU} (p q : X → hProp) : (deptypeddecider p) → (deptypeddecider q) → (deptypeddecider (predconj p q)).
   Proof.
     intros decp decq x.
     induction (decp x), (decq x).
@@ -135,7 +136,7 @@ Section ClosureProperties.
     - right. intros [pp qq]. exact (b pp).
   Qed.
 
-  Lemma decidableneg {X : UU} (p q : X → hProp) : (deptypeddecider p) → (deptypeddecider (λ (x : X), hneg (p x))).
+  Lemma decidableneg {X : UU} (p : X → hProp) : (deptypeddecider p) → (deptypeddecider (predneg p)).
   Proof.
     intros decp x.
     induction (decp x).
@@ -144,105 +145,3 @@ Section ClosureProperties.
   Qed.
 
 End ClosureProperties.
-
-Section EqualityDeciders.
-
-  Definition iseqdecider (X : UU) (f : X → X → bool) : UU := ∏ (x1 x2 : X), x1 = x2 <-> f x1 x2 = true.
-
-  Definition eqdecider (X : UU) := ∑ (f : X → X → bool), (iseqdecider X f).
-
-  Definition make_eqdecider {X : UU} {f : X → X → bool} : (iseqdecider X f) → eqdecider (X) := (λ is : (iseqdecider X f), (f,, is)).
-
-  Lemma eqdecidertodeptypedeqdecider (X : UU) : (eqdecider X) → (isdeceq X).
-  Proof.
-    intros [f is] x y.
-    destruct (is x y) as [impl1 impl2].
-    induction (f x y).
-    - left; apply impl2; apply idpath.
-    - right. intros eq. apply nopathsfalsetotrue. exact (impl1 eq).
-  Qed.
-
-  Lemma deptypedeqdecidertoeqdecider (X : UU) : (isdeceq X) → (eqdecider X).
-  Proof.
-    intros is.
-    use tpair.
-    - intros x y.
-      induction (is x y).
-      + exact true.
-      + exact false.
-    - intros x y.
-      induction (is x y); simpl; split.
-      + exact (λ a : (x = y), (idpath true)).
-      + exact (λ b : (true = true), a).
-      + intros; apply fromempty; exact (b X0).
-      + intros; apply fromempty; exact (nopathsfalsetotrue X0).
-  Qed.
-
-  Lemma eqdecidertoisapropeq (X : UU) (f : eqdecider X) : ∏ (x y : X) ,(isaprop (x = y)).
-  Proof.
-    intros x.
-    apply isaproppathsfromisolated.
-    intros y.
-    set (dec := eqdecidertodeptypedeqdecider X f).
-    apply (dec x).
-  Qed.
-
-  Lemma isapropiseqdecider (X : UU) (f : X → X → bool) : (isaprop (iseqdecider X f)).
-  Proof.
-    apply isofhlevelsn.
-    intros is.
-    repeat (apply impred_isaprop + intros).
-    apply isapropdirprod; apply isapropimpl.
-    - induction (f t).
-      + apply isapropifcontr.
-        use iscontrloopsifisaset.
-        exact isasetbool.
-      + apply isapropifnegtrue.
-        exact nopathsfalsetotrue.
-    - apply eqdecidertoisapropeq.
-      use make_eqdecider.
-      + exact f.
-      + exact is.
-  Qed.
-
-  Lemma pathseqdeciders (X : UU) (f g : X → X → bool) (isf : iseqdecider X f) (isg : iseqdecider X g) : f = g.
-  Proof.
-    apply funextsec; intros x.
-    apply funextsec; intros y.
-    destruct (isf x y) as [implf1 implf2].
-    destruct (isg x y) as [implg1 implg2].
-    induction (g x y).
-    - apply implf1; apply implg2.
-      apply idpath.
-    - induction (f x y).
-      + apply fromempty, nopathsfalsetotrue, implg1, implf2.
-        exact (idpath true).
-      + exact (idpath false).
-  Qed.
-
-  Lemma isapropeqdecider (X : UU) : (isaprop (eqdecider X)).
-  Proof.
-    apply invproofirrelevance.
-    intros [f isf] [g isg].
-    induction (pathseqdeciders X f g isf isg).
-    assert (eq : isf = isg).
-    - apply proofirrelevance.
-      apply isapropiseqdecider.
-    - induction eq.
-      apply idpath.
-  Qed.
-
-  Lemma weqisdeceqiseqdecider (X : UU) : (isdeceq X) ≃ (eqdecider X).
-  Proof.
-    use make_weq.
-    - exact (deptypedeqdecidertoeqdecider X).
-    - apply isweqimplimpl.
-      + exact (eqdecidertodeptypedeqdecider X).
-      + exact (isapropisdeceq X).
-      + exact (isapropeqdecider X).
-  Qed.
-End EqualityDeciders.
-
-Section ChoiceFunction.
-
-End ChoiceFunction.

code/Enumerability/Definitions.v

@@ -0,0 +1,81 @@
+Require Import init.imports.
+Require Import Inductive.Option.
+
+Definition rangeequiv {X : UU} {Y : UU} (f g : X → Y) := ∏ (y : Y), ∥hfiber f y∥ <-> ∥hfiber g y∥.
+
+Notation "f ≡ᵣ g" := (rangeequiv f g) (at level 50).
+
+Section EmbedNaturals.
+
+  (* Bijective maps from pairs of natural numbers to natural numbers.*)
+  
+  Definition embed (p : nat×nat) : nat :=
+    (pr2 p) + (nat_rec _ 0 (λ i m,  (S i) + m) ((pr2 p) + (pr1 p))).
+
+  Definition unembed (n : nat) : nat × nat :=
+    nat_rec _ (0,, 0) (fun _ a => match (pr1 a) with S x => (x,, S (pr2 a)) | _ => (S (pr2 a),, 0) end) n.
+
+  (*Proofs that embed and unembed are inverses of each other. *)
+
+  Lemma embedinv (n : nat) : (embed (unembed n)) = n.
+  Proof.
+  (*TODO*)  
+  Admitted.
+
+  Lemma unembedinv (n : nat × nat) : (unembed (embed n)) = n. 
+  Proof.
+  (* TODO *)
+  Admitted.  
+End EmbedNaturals.
+
+Section EnumerablePredicates.
+  
+  Definition ispredenum {X : UU} (p : X → hProp) (f : nat → option) := ∏ (x : X), (p x) <-> ∥(hfiber f (some x))∥. 
+
+  Definition predenum {X : UU} (p : X → hProp) := ∑ (f : nat → option), (ispredenum p f).
+
+  Definition isenumerablepred {X : UU} (p : X → hProp) := ∥predenum p∥.
+  
+  Lemma isapropispredenum {X : UU} (p : X → hProp) (f : nat → option) : (isaprop (ispredenum p f)).
+  Proof.
+    apply impred_isaprop.
+    intros t.
+    apply isapropdirprod; apply isapropimpl, propproperty.
+  Qed.
+
+  Lemma rangeequivtohomot {X : UU} (p q : X → hProp) (e1 : (predenum p)) (e2 : (predenum q)) : ((pr1 e1) ≡ᵣ (pr1 e2)) → p ~ q.  
+  Proof.
+    intros req x.
+    destruct e1 as [f ispf].
+    destruct e2 as [g ispg].
+    destruct (req (some x)) as [impl1 impl2].
+    destruct (ispf x) as [if1 if2].
+    destruct (ispg x) as [ig1 ig2].
+    use hPropUnivalence. 
+    - intros px.
+      apply ig2, impl1, if1.
+      exact px.
+    - intros qx.
+      apply if2, impl2, ig1.
+      exact qx. 
+  Qed.
+
+  (* Closure properties *)
+  Lemma enumconj {X : UU} (p q : X → hProp) : (predenum p) → (predenum q) → (predenum (λ x : X, p x ∧ q x)).
+  Admitted.
+
+  Lemma enumdisj {X : UU} (p q : X → hProp) : (predenum p) → (predenum q) → (predenum (λ x : X, p x ∨ q x)). 
+  Admitted.
+
+  Lemma enumdirprod {X Y : UU} (p : X → hProp) (q : Y → hProp) : (predenum p) → (predenum q) → (predenum (λ a, (p (pr1 a)) ∧ (q (pr2 a)))).
+  Proof.
+  Admitted.
+
+  Lemma enumcoprod {X Y : UU} (p : X → hProp) (q : Y → hProp) : (predenum p) → (predenum q) → (predenum (λ a, (
+  
+  
+End EnumerablePredicates.
+
+
+
+

code/Inductive/Predicates.v

@@ -0,0 +1,37 @@
+Require Import init.imports.
+
+(*
+
+This file contains definitions of the used operations on predicates and a number of useful 
+properties. 
+
+*)
+
+
+Section Operations.
+
+  Definition predconj {X : UU} (p q : X → hProp) : X → hProp := (λ x : X, (p x) ∧ (q x)).
+
+  Infix "p ∧ q" := (predconj p q) (at level 25).
+  
+  Definition preddisj {X : UU} (p q : X → hProp) : X → hProp := (λ x : X, (p x) ∨ (q x)).
+
+  Infix "p ∨ q" := (preddisj p q) (at level 25).
+  
+  Definition predneg {X : UU} (p : X → hProp) : X → hProp := (λ x : X, hneg (p x)).
+  
+  Notation "¬ p" := (predneg p) (at level 35).
+
+  Definition preddirprod {X Y : UU} (p : X → hProp) (q : Y → hProp) : (X × Y) → hProp := (λ x : X × Y, (p (pr1 x)) ∧ (q (pr2 x))). 
+
+  Infix "p × q" := (preddirprod p q) (at level 25).
+  
+  Definition predcoprod {X Y : UU} (p : X → hProp) (q : Y → hProp) : (X ⨿ Y) → hProp.
+  Proof.
+    intros x.
+    induction x.
+    - exact (p a).
+    - exact (q b). 
+  Defined.
+  
+End Operations.

code/_CoqProject

@@ -2,11 +2,14 @@ COQC = coqc
 COQDEP = coqdep
 -R . "sem"
 
--o -arg "-w -notation-overridden -type-in-type"
+-arg "-w -notation-overridden -type-in-type"
 
 init/imports.v
 init/all.v
 
+util/range_equiv.v
+
+Inductive/Predicates.v
 Inductive/Option.v
 
 Decidability/DecidablePredicates.v

code/util/range_equiv.v

@@ -0,0 +1,5 @@
+Require Import init.imports.
+
+Definition rangeequiv {X : UU} {Y : UU} (f g : X → Y) := ∏ (y : Y), ∥hfiber f y∥ <-> ∥hfiber g y∥.
+
+Notation "f ≡ᵣ g" := (rangeequiv f g) (at level 50).