Add a neutral inversion lemma for type well-formedness and use it.

CoqHott · Sep 12, 2023 · 735a6c7 · 735a6c7
1 parent 3b197fe
commit 735a6c7
Show file tree

Hide file tree

Showing 3 changed files with 15 additions and 6 deletions.
diff --git a/theories/BundledAlgorithmicTyping.v b/theories/BundledAlgorithmicTyping.v
@@ -436,14 +436,12 @@ Section BundledConv.
       assert [Γ |-[de] M : U].
       {
         eapply algo_conv_wh in Hconv as [neM neN].
-        inversion HM ; subst ; clear HM.
-        all: solve [now inversion neM| assumption].
+        now eapply neutral_ty_inv.
       }
       assert [Γ |-[de] N : U].
       {
         eapply algo_conv_wh in Hconv as [neM neN].
-        inversion HN ; subst ; clear HN.
-        all: solve [now inversion neN| assumption].
+        now eapply neutral_ty_inv.
       }
       assert (well_typed (ta := de) Γ M) by now eexists.
       assert (well_typed (ta := de) Γ N) by now eexists.

diff --git a/theories/Decidability/Termination.v b/theories/Decidability/Termination.v
@@ -148,8 +148,7 @@ Proof.
     split.
     2: intros [|] ; cbn ; easy.
     eapply (IHM tt A) ; tea.
-    inversion Hty ; subst ; tea.
-    1-6:  inv_whne.
+    apply neutral_ty_inv in Hty; [|tea].
     now exists U.
   - intros * ???? ? ? wu' ?.
     apply compute_domain.

diff --git a/theories/TypeConstructorsInj.v b/theories/TypeConstructorsInj.v
@@ -594,6 +594,18 @@ Proof.
     * prod_splitter; tea; right; now eapply TypeTrans.
 Qed.
 
+Lemma neutral_ty_inv Γ A :
+  [Γ |- A] -> whne A -> [Γ |- A : U].
+Proof.
+  intros Hty Hne.
+  unshelve eapply TypeRefl, ty_conv_inj in Hty.
+  - now constructor.
+  - now constructor.
+  - cbn in *.
+    apply Fundamental in Hty; destruct Hty.
+    now eapply escapeTm.
+Qed.
+
 Lemma prod_ty_inv Γ A B :
   [Γ |- tProd A B] ->
   [Γ |- A] × [Γ,, A |- B].