From ef41831f9224c5963ee02787cdafc8a6d1f579a5 Mon Sep 17 00:00:00 2001
From: Junyoung/Clare Jang <jjc9310@gmail.com>
Date: Sat, 31 Aug 2024 12:36:33 -0400
Subject: [PATCH] Use existT

---
 theories/Extraction/TypeCheck.v | 46 ++++++++++++---------------------
 1 file changed, 16 insertions(+), 30 deletions(-)

diff --git a/theories/Extraction/TypeCheck.v b/theories/Extraction/TypeCheck.v
index 74d1b95a..c41d978d 100644
--- a/theories/Extraction/TypeCheck.v
+++ b/theories/Extraction/TypeCheck.v
@@ -50,8 +50,8 @@ Section type_check.
   | _               => inright _
   .
 
-  Equations get_subterms_of_pi_nf (A : nf) : { '(B, C) | A = n{{{ Π B C }}} } + { forall B C, A <> n{{{ Π B C }}} } :=
-  | n{{{ Π B C }}} => pureo (exist _ (B, C) _)
+  Equations get_subterms_of_pi_nf (A : nf) : { B & { C | A = n{{{ Π B C }}} } } + { forall B C, A <> n{{{ Π B C }}} } :=
+  | n{{{ Π B C }}} => pureo (existT _ B (exist _ C _))
   | _              => inright _
   .
 
@@ -74,18 +74,13 @@ Section type_check.
   #[local]
   Hint Constructors type_check_order type_infer_order : mcltt.
 
-  Lemma user_exp_to_type_check_order : forall M,
-      user_exp M ->
-      type_check_order M.
-  Proof.
-    induction 1; progressive_inversion; mauto 3.
-  Qed.
-
   Lemma user_exp_to_type_infer_order : forall M,
       user_exp M ->
       type_infer_order M.
   Proof.
-    induction 1; progressive_inversion; mauto using user_exp_to_type_check_order.
+    intros M HM.
+    enough (type_check_order M) as [] by eassumption.
+    induction HM; progressive_inversion; mauto 3.
   Qed.
 
   #[local]
@@ -202,9 +197,9 @@ Section type_check.
         pureo (exist _ n{{{ Π A'' B' }}} _)
     | {{{ M' N' }}} =>
         let*o (exist _ C _) := type_infer G _ M' _ while _ in
-        let*o (exist _ AB _) := get_subterms_of_pi_nf C while _ in
-        let*b->o _ := type_check G (fst AB) _ N' _ while _ in
-        let (B', _) := nbe_ty_impl G {{{ ~(snd AB)[Id,,N'] }}} _ in
+        let*o (existT _ A (exist _ B _)) := get_subterms_of_pi_nf C while _ in
+        let*b->o _ := type_check G A _ N' _ while _ in
+        let (B', _) := nbe_ty_impl G {{{ B[Id,,N'] }}} _ in
         pureo (exist _ B' _)
     | {{{ #x }}} =>
         let*o (exist _ A _) := lookup G _ x while _ in
@@ -304,23 +299,14 @@ Section type_check.
     eexists; mauto 4 using alg_type_infer_sound.
   Qed.
 
-  Next Obligation. (* False *)
-    clear_defs.
-    functional_alg_type_infer_rewrite_clear.
-    progressive_inversion.
-    functional_alg_type_infer_rewrite_clear.
-    autoinjections.
-    congruence.
-  Qed.
-
-  Next Obligation. (* nbe_ty_order G {{{ n0[Id,,N'] }}} *)
+  Next Obligation. (* nbe_ty_order G {{{ s[Id,,N'] }}} *)
     clear_defs.
     functional_alg_type_infer_rewrite_clear.
     progressive_inversion.
-    assert {{ G ⊢ n : ~n{{{ Type@i }}} }} by mauto 4 using alg_type_infer_sound.
-    assert {{ G, ~(n : exp) ⊢ n0 : ~n{{{ Type@j }}} }} by mauto 4 using alg_type_infer_sound.
-    assert {{ G ⊢ N' : n }} by mauto 3 using alg_type_check_sound.
-    assert {{ G ⊢ n0[Id,,N'] : ~n{{{ Type@j }}} }} as [? []]%soundness_ty by mauto 3.
+    assert {{ G ⊢ A : ~n{{{ Type@i }}} }} by mauto 4 using alg_type_infer_sound.
+    assert {{ G, ~(A : exp) ⊢ s : ~n{{{ Type@j }}} }} by mauto 4 using alg_type_infer_sound.
+    assert {{ G ⊢ N' : A }} by mauto 3 using alg_type_check_sound.
+    assert {{ G ⊢ s[Id,,N'] : ~n{{{ Type@j }}} }} as [? []]%soundness_ty by mauto 3.
     mauto 3 using nbe_ty_order_sound.
   Qed.
 
@@ -329,9 +315,9 @@ Section type_check.
     functional_alg_type_infer_rewrite_clear.
     progressive_inversion.
     split; [mauto 3 |].
-    assert {{ G ⊢ n0 : ~n{{{ Type@i }}} }} by mauto 4 using alg_type_infer_sound.
-    assert {{ G, ~(n0 : exp) ⊢ n1 : ~n{{{ Type@j }}} }} by mauto 4 using alg_type_infer_sound.
-    assert {{ G ⊢ n1[Id,,N'] ≈ B' : Type@j }} by (eapply soundness_ty'; mauto 4 using alg_type_check_sound).
+    assert {{ G ⊢ A : ~n{{{ Type@i }}} }} by mauto 4 using alg_type_infer_sound.
+    assert {{ G, ~(A : exp) ⊢ s : ~n{{{ Type@j }}} }} by mauto 4 using alg_type_infer_sound.
+    assert {{ G ⊢ s[Id,,N'] ≈ B' : Type@j }} by (eapply soundness_ty'; mauto 4 using alg_type_check_sound).
     assert (user_exp B') by trivial using user_exp_nf.
     assert (exists k, {{ G ⊢a B' ⟹ Type@k }} /\ k <= j) as [? []] by (gen_presups; mauto 3).
     firstorder.