Proven closure property for lists.

Author: klinashka

code/Enumerability/EnumerableTypes.v

@@ -1,6 +1,7 @@
 Require Import init.imports.
 Require Import Enumerability.EnumerablePredicates.
 Require Import Decidability.DecidablePredicates.
+Require Import util.NaturalEmbedding.
 Require Import Inductive.Option. 
 Require Import Inductive.Predicates.
 Require Import util.NaturalEmbedding.
@@ -322,6 +323,57 @@ Section ListEnumerability.
     - apply propproperty.
   Qed.
 
+  Local Infix "++" := concatenate. 
+
+  Definition listfun (X : UU) (L : nat → list X) : (nat → (list (list X))). 
+  Proof.
+    intros n; induction n.
+    - exact (cons nil nil).
+    - exact (IHn ++ (map (λ (x : (X×(list X))), (cons (pr1 x) (pr2 x))) (list_prod (cumul L n) IHn))).
+  Defined.
+  
+  Lemma iscumulativelistfun (X : UU) (L : nat → list X) : (iscumulative (listfun X L)).
+  Proof.
+    intros ?; simpl.
+    use (tpair _ (map (λ x : X × list X, cons (pr1 x) (pr2 x)) (list_prod (cumul L n) (listfun X L n)))); apply idpath.
+  Defined. 
+
+  Lemma listlistenumerator (X : UU) (L : nat → list X) : (islistenumerator X L) → (islistenumerator (list X) (listfun X L)).
+  Proof.
+    intros lstenm.
+    use list_ind; cbn beta.
+    - apply hinhpr. use (tpair _ 0). right; apply idpath.
+    - intros.
+      use (squash_to_prop X0 (propproperty _)); intros [n inn1]; clear X0. 
+      use (squash_to_prop (lstenm x) (propproperty _)); intros [m inn2]; clear lstenm.
+      apply hinhpr; use tpair; cbn beta. 
+      + induction (natlthorgeh n m). exact (S m). exact (S n).
+      + induction (natlthorgeh n m); simpl.
+        * induction m. apply fromempty. apply (negnatlthn0 n a). 
+          set (q := (isincumulleh _ _ (iscumulativelistfun _ _) n (S m) (natlthtoleh _ _ a) inn1)).
+          simpl. apply isin_concatenate2. apply (is_inmap (λ (x : X × (list X)), (cons (pr1 x) (pr2 x))) _ (x,, xs)), inn_list_prod1. apply isin_concatenate2. exact inn2.
+          exact q.
+        * induction n. set (q := (nat0gehtois0 m b)). induction (pathsinv0 q). clear q. 
+          apply isin_concatenate2. apply (is_inmap (λ (x : X × (list X)), (cons (pr1 x) (pr2 x))) _ (x,, xs)). apply inn_list_prod1. exact inn2. exact inn1.
+          apply isin_concatenate2. apply (is_inmap (λ (x : X × (list X)), (cons (pr1 x) (pr2 x))) _ (x,, xs)). apply inn_list_prod1. 
+          assert (inn3 : is_in x (cumul L m)) by apply (isinlisincumull _ _ _ inn2).
+          apply (isincumulleh _ _ (iscumulativecumul _) m (S n) b inn3).
+          apply inn1.
+  Defined.  
+          
+  Lemma islistenumerablelist {X : UU} (isenum : islistenumerable X) : (islistenumerable (list X)). 
+  Proof.
+    use squash_to_prop.
+    - exact (listenumerator X).
+    - exact isenum.
+    - apply propproperty.
+    - clear isenum; intros [L isenum]. apply hinhpr.
+      exact ((listfun X L),, (listlistenumerator X L isenum)).
+  Qed.
 
+  Lemma isenumerablelist {X : UU} (isenum : isenumerable X) : (isenumerable (list X)). 
+  Proof.
+    apply weqisenumerableislistenumerable, islistenumerablelist, weqisenumerableislistenumerable. exact isenum.
+  Qed. 
 
 End ListEnumerability. 

code/Inductive/ListProperties.v

@@ -272,30 +272,7 @@ Section Append.
     Example testappendnilright: (append l2 nil) = l2. Proof. apply idpath. Qed. 
 
   End AppendTests. 
-
-  (* Local Notation "l1 ++ l2" := (append l1 l2) (at level 60, left associativity).
-  Lemma appendnil1 {X : UU} (l1 : list X) : (l1 ++ nil) = l1.
-  Proof.
-    revert l1.
-    use list_ind; cbn beta; intros.
-    - apply idpath.
-    - exact (maponpaths (cons x) X0).
-  Qed.
-
-  Lemma appendnil1inv {X : UU} (l1 : list X) : l1 = (l1 ++ nil). 
-  Proof. 
-    apply pathsinv0, appendnil1.
-  Qed.
 
-  Lemma appendnil2 {X : UU} (l1 : list X) : (nil ++ l1) = l1.
-  Proof. apply idpath. Qed.
-  
-  Lemma appendnil2inv {X : UU} (l2 : list X) : l2 = (nil ++ l2).
-  Proof. apply idpath. Qed.
-
-  Lemma appendtrans {X : UU} (l1 l2 l3 : list X) : (l1 ++ l2) ++ l3 = l1 ++ l2 ++ l3. 
-  Proof. *)
-   
   Local Infix "++" := concatenate.
 
   Lemma isin_concatenate1 {X : UU} (l1 l2 : list X) (x : X) : (is_in x l1) → (is_in x (l1 ++ l2)).
@@ -328,12 +305,51 @@ Section Append.
   Defined. 
 End Append. 
 
+Section ListProduct. 
+Local Infix "++" := concatenate. 
+  Definition list_prod {X Y : UU} (l1 : list X) (l2 : list Y) : (list (X × Y)).
+  Proof. 
+    revert l1.
+    use list_ind; cbn beta.  
+    - exact nil.
+    - intros; exact ((map (λ (y : Y), (x,, y)) l2) ++ X0).
+  Defined.
+  
+  Lemma inn_list_prod1 {X Y : UU} (l1 : list X) (l2 : list Y) (x : X) (y : Y) : (is_in x l1) → (is_in y l2) → (is_in (x,, y) (list_prod l1 l2)). 
+  Proof. 
+    revert l1.
+    use list_ind; cbn beta.
+    - exact fromempty.
+    - intros x0 xs IHl inn1 inn2.
+      destruct inn1 as [l | r]. 
+      + apply isin_concatenate2. exact (IHl l inn2).
+      + apply isin_concatenate1. rewrite <- r. clear IHl r x0.
+        revert l2 inn2. use list_ind; cbn beta.
+        * exact (fromempty).
+        * intros y0 ys IHl [l | r]; rewrite -> (mapStep).
+          -- left. exact (IHl l).
+          -- right. rewrite -> r. apply idpath.
+  Defined.           
+End ListProduct. 
+
+Section Map. 
+
+  Lemma is_inmap {X Y : UU} (f : X → Y) (l : list X) (x : X) : (is_in x l) → (is_in (f x) (map f l)).
+  Proof. 
+    revert l. use list_ind; cbn beta.
+    - exact fromempty.
+    - intros x0 xs IHl [l | r].
+      + left. exact (IHl l).
+      + right. apply maponpaths. exact r.
+  Defined.  
+End Map. 
+
 Section CumulativeFunctions.
 
   Local Infix "++" := concatenate. 
-  Definition iscumulative {X : UU} (L : nat → list X) := ∏ (n : nat), ∃ (l : list X), (L (S n) = ((L n) ++ l)).
+  Definition iscumulative {X : UU} (L : nat → list X) := ∏ (n : nat), ∑ (l : list X), (L (S n) = ((L n) ++ l)).
 
-  Lemma cumulativenleqm {X : UU} (L : nat → list X) (iscum : (iscumulative L)) (m n : nat) : n ≤ m → ∃ (l : list X), L m = (L n) ++ l.
+  Lemma cumulativenleqm {X : UU} (L : nat → list X) (iscum : (iscumulative L)) (m n : nat) : n ≤ m → ∑ (l : list X), L m = (L n) ++ l.
   Proof.
     intros nleqm.
     assert (eq : ∑ (k : nat), n + k = m).
@@ -342,11 +358,11 @@ Section CumulativeFunctions.
       + cbn beta. rewrite -> (natpluscomm n (m - n)). apply (minusplusnmm _ _ nleqm).
     - destruct eq as [k eq].
       induction eq; induction k.
-      + rewrite (natpluscomm n 0). apply hinhpr. use (tpair _ nil). simpl. rewrite -> (concatenate_nil (L n)). apply idpath.
-      + rewrite (natplusnsm n k); use (squash_to_prop (iscum (n + k)) (propproperty _)); intros [l eq]; clear iscum.
-        use (squash_to_prop (IHk (natlehnplusnm _ _)) (propproperty _)); intros [l0 neq]; clear IHk; apply hinhpr.
+      + rewrite (natpluscomm n 0). use (tpair _ nil). simpl. rewrite -> (concatenate_nil (L n)). apply idpath.
+      + rewrite (natplusnsm n k); destruct (iscum (n + k)) as [l eq]; clear iscum.
+        destruct (IHk (natlehnplusnm _ _)) as [l0 neq]; clear IHk.
         use (tpair _ (l0 ++ l)). simpl. rewrite -> eq, neq. apply assoc_concatenate.
-  Qed.  
+  Qed.
 
   Definition cumul {X : UU} : (nat → list X) → (nat → list X). 
   Proof.
@@ -359,10 +375,8 @@ Section CumulativeFunctions.
   Lemma iscumulativecumul {X : UU} (L : nat → list X) : (iscumulative (cumul L)).
   Proof.
     intros n; induction n. 
-    - apply hinhpr.
-      use (tpair _ (L 1) (idpath _)).
-    - use (squash_to_prop IHn (propproperty _)); intros IH; clear IHn; apply hinhpr.
-      use (tpair _ (L (S (S n))) (idpath _)). 
+    - use (tpair _ (L 1) (idpath _)).
+    - use (tpair _ (L (S (S n))) (idpath _)). 
   Defined.
 
   Lemma isinlisincumull {X : UU} (L : nat → list X) (x : X) (n : nat) : (is_in x (L n)) → (is_in x (cumul L n)).
@@ -371,7 +385,14 @@ Section CumulativeFunctions.
     induction n.
     - exact inn.
     - simpl. apply isin_concatenate2. exact inn.
-  Defined.        
+  Defined.
+
+  Lemma isincumulleh {X : UU} (L : nat → list X) (x : X) (iscum : iscumulative L) (n m: nat) : (n ≤ m) → (is_in x (L n)) → (is_in x (L m)).
+  Proof. 
+    intros leq inn.
+    set (q := cumulativenleqm L iscum m n leq); destruct q as [l eq]; rewrite -> eq.
+    apply isin_concatenate1. exact inn.
+  Defined.   
 
   Lemma iscumulex {X : UU} (L : nat → list X) (x : X) : (∃ (n : nat), (is_in x (L n))) <-> (∃ (n : nat), (is_in x (cumul L n))).
   Proof.
@@ -383,7 +404,7 @@ Section CumulativeFunctions.
     + induction (isin_concatenate_choice (cumul L n) (L (S n)) x inn).
       * exact (IHn a).
       * exact ((S n),, b).
-  Defined. 
+  Defined.
 
 End CumulativeFunctions.