From ec1d5131ef1ae4ace627bd3fd674346b7e6e87e4 Mon Sep 17 00:00:00 2001
From: Calin Diacicov <diacicov.calin@gmail.com>
Date: Tue, 24 Dec 2024 00:43:01 +0200
Subject: [PATCH] Implemented embed and unembed inverse proofs.

---
 code/Enumerability/EnumerableTypes.v |  4 +-
 code/util/NaturalEmbedding.v         | 90 +++++++++-------------------
 2 files changed, 30 insertions(+), 64 deletions(-)

diff --git a/code/Enumerability/EnumerableTypes.v b/code/Enumerability/EnumerableTypes.v
index ec2c2d5..de4255b 100644
--- a/code/Enumerability/EnumerableTypes.v
+++ b/code/Enumerability/EnumerableTypes.v
@@ -116,7 +116,7 @@ Section TypePredicateEnumerabilityEquivalence.
   Qed.
   
 End TypePredicateEnumerabilityEquivalence. 
-
+ 
 Section StrongEnumerability. 
 
   Definition isstrongenumerator (X : UU) (f : nat → X) := (issurjective f).
@@ -460,4 +460,4 @@ Section ListEnumerability.
     apply weqisenumerableislistenumerable, islistenumerablelist, weqisenumerableislistenumerable. exact isenum.
   Qed. 
 
-End ListEnumerability. 
\ No newline at end of file
+End ListEnumerability.
\ No newline at end of file
diff --git a/code/util/NaturalEmbedding.v b/code/util/NaturalEmbedding.v
index 6acdaa5..593c65b 100644
--- a/code/util/NaturalEmbedding.v
+++ b/code/util/NaturalEmbedding.v
@@ -40,76 +40,42 @@ Section EmbedNaturals.
   
   (*Proofs that embed and unembed are inverses of each other. *)
 
-  Lemma gauss_sum_sn (n : nat) : (gauss_sum (S n)) = ((S n) + gauss_sum n).
-  Proof.
-    apply idpath.
-  Qed.
-
-  Lemma natplusS (n m : nat) : n + S m = S (n + m). 
+  Lemma embedinv (n : nat) : (embed (unembed n)) = n.
   Proof.
-    induction (pathsinv0 (natpluscomm n (S m))). 
-    induction (pathsinv0 (natpluscomm n m)).
-    apply idpath.
+    induction n as [|n IH]. reflexivity.
+    simpl. revert IH. destruct (unembed n) as [x y]. 
+    case x as [|x]; intro Hx; rewrite <- Hx; unfold embed; simpl.
+    - rewrite natplusr0. apply idpath.
+    - rewrite natpluscomm, (natpluscomm y (S x)).
+      simpl. rewrite (natpluscomm y (S (x + y + gauss_sum (x + y)))). apply maponpaths. simpl. apply maponpaths. rewrite (natpluscomm x y). apply idpath.
   Qed.
   
-    
-  Lemma embedsn (m : nat) : (embed (0,, S m)) = ((S (S m)) + embed (0,, m)).
+  Lemma embed0x (x y : nat) : (embed (S x,, 0) = S (embed (0,, x))).
   Proof.
-    induction m.
-    - apply idpath.
-    - unfold embed. simpl.
-      induction (pathsinv0 (natplusr0 m)).
-      induction (pathsinv0 (natplusS m (S (m + S (m + gauss_sum (m)))))). 
-      apply idpath.
-  Qed.
-    
-  Lemma embedmsn (n m : nat) : (embed (n,, S m)) = ((S (S (n + m)) + embed (n,, m))).
-  Proof.
-    unfold embed. 
-    simpl.
-    induction (pathsinv0 (natplusS m (m + n + gauss_sum (m + n)))). 
-    repeat apply maponpaths.
-    induction (pathsinv0 (natpluscomm n m)).
-    induction ( (natplusassoc m (m + n) (gauss_sum (m + n)))).
-    induction (natplusassoc m m n).
-    induction (natplusassoc (m + n) m (gauss_sum (m + n))).
-    apply (maponpaths (λ x, add x (gauss_sum (m + n)))). 
-    induction (pathsinv0 (natplusassoc m m n)), (pathsinv0 (natplusassoc m n m)).
-    apply (maponpaths (add m)).
-    apply natpluscomm.
+    unfold embed; simpl; rewrite natplusr0. apply idpath.
   Qed.
 
-  Lemma natnmto0 (n m : nat) : n + m = 0 → n = 0. 
+  Lemma embedsxy (x y : nat) : (embed (x,, S y) = S (embed (S x,, y))).
   Proof.
-    intros eq.
-    induction n. 
-    - apply idpath.
-    - apply fromempty.
-      exact (negpathssx0 _ eq).
-  Qed.
-  
-  Lemma embed0 (n : nat × nat) : (embed n) = 0 → n = (0,, 0). 
-  Proof.
-    induction n as [[|?] [|?]].
-    - intros. apply idpath. 
-    - unfold embed. simpl. intros. apply fromempty. exact (negpathssx0 _ X).  
-    - unfold embed. simpl. intros. apply fromempty. exact (negpathssx0 _ X). 
-    - unfold embed. simpl. intros. apply fromempty. exact (negpathssx0 _ X).
-  Defined. 
-        
-  Lemma embedinv (n : nat) : (embed (unembed n)) = n.
-  Proof.
-    assert (eq : ∏ (m : nat × nat), unembed n = m → n = embed m).
-    - admit.  
-    - rewrite <- (eq (unembed n)); apply idpath; apply idpath.
-  Admitted.
-  
-  Lemma unembedinv (n : nat × nat) : (unembed (embed n)) = n. 
-  Proof.
-    (* TODO *)
-  Admitted.
-
+    unfold embed; simpl.
+    rewrite natplusnsm, (natplusnsm y x); simpl.
+    rewrite natplusnsm. apply idpath.
+  Qed.    
 
+  Lemma unembedinv (mn : nat × nat) : (unembed (embed mn)) = mn. 
+  Proof.
+    assert (∏ (n : nat), embed mn = n → unembed n = mn).
+    - intro n. revert mn. induction n as [|n IH].
+      + intros [[|?][|?]]; intro H; inversion H; apply idpath.
+      + intros [x [|y]]; simpl.
+        * case x as [| x]; simpl; intro H.
+            inversion H.
+          rewrite (IH (0,, x)); [reflexivity |].
+          revert H. rewrite embed0x. intros H; apply invmaponpathsS. apply H. exact x.
+        * intro H. rewrite (IH (S x,, y)); [reflexivity| ].
+          apply invmaponpathsS. rewrite <- embedsxy. exact H.
+    - apply X. apply idpath.
+    Qed.
   
 End EmbedNaturals.