Update inversion theorems (#114)

* Rename a constructor

* Remove duplicated inversion theorems

* Add an inversion theorem unexpectedly syntactic

* Rearrange completeness consequences in a clearer structure

theories/Core/Completeness/Consequences/Inversions.v

@@ -1,39 +1,17 @@
 From Coq Require Import RelationClasses.
 From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import Completeness Completeness.FundamentalTheorem Completeness.LogicalRelation Semantic.Realizability.
+From Mcltt.Core Require Import Completeness Semantic.Realizability Completeness.Consequences.Types.
 From Mcltt.Core Require Export SystemOpt CoreInversions.
 Import Domain_Notations.
 
-Theorem not_exp_eq_typ_nat : forall Γ i j,
-    ~ {{ Γ ⊢ ℕ ≈ Type@i : Type@j }}.
-Proof.
-  intros ** ?.
-  assert {{ Γ ⊨ ℕ ≈ Type@i : Type@j }} as [env_relΓ] by mauto using completeness_fundamental_exp_eq.
-  destruct_conjs.
-  assert (exists p p', initial_env Γ p /\ initial_env Γ p' /\ {{ Dom p ≈ p' ∈ env_relΓ }}) by mauto using per_ctx_then_per_env_initial_env.
-  destruct_conjs.
-  functional_initial_env_rewrite_clear.
-  (on_all_hyp: destruct_rel_by_assumption env_relΓ).
-  destruct_by_head rel_typ.
-  invert_rel_typ_body.
-  destruct_by_head rel_exp.
-  invert_rel_typ_body.
-  destruct_conjs.
-  match_by_head1 per_univ_elem invert_per_univ_elem.
-Qed.
-
-#[export]
-Hint Resolve not_exp_eq_typ_nat : mcltt.
-
 Corollary wf_zero_inversion : forall Γ A,
     {{ Γ ⊢ zero : A }} ->
     exists i, {{ Γ ⊢ ℕ ≈ A : Type@i }}.
 Proof with mautosolve 4.
   intros * H.
   dependent induction H; try mautosolve.
   - (* wf_conv *)
-    assert (exists i : nat, {{ Γ ⊢ ℕ ≈ A : Type@i }}) as [j] by eauto.
-    mauto using lift_exp_eq_max_left, lift_exp_eq_max_right.
+    assert (exists i : nat, {{ Γ ⊢ ℕ ≈ A : Type@i }}) as [j] by eauto...
   - (* wf_cumu *)
     assert (exists j : nat, {{ Γ ⊢ ℕ ≈ Type@i : Type@j }}) as [j contra] by eauto.
     contradict contra...
@@ -47,34 +25,12 @@ Proof with mautosolve.
   dependent induction H; try (split; mautosolve).
   - (* wf_conv *)
     assert ({{ Γ ⊢ M : ℕ }} /\ exists i : nat, {{ Γ ⊢ ℕ ≈ A : Type@i }}) as [] by eauto.
-    destruct_conjs.
-    mauto 6 using lift_exp_eq_max_left, lift_exp_eq_max_right.
+    destruct_conjs...
   - (* wf_cumu *)
     assert ({{ Γ ⊢ M : ℕ }} /\ exists j : nat, {{ Γ ⊢ ℕ ≈ Type@i : Type@j }}) as [? [? contra]] by eauto.
     contradict contra...
 Qed.
 
-Theorem not_exp_eq_typ_pi : forall Γ i A B j,
-    ~ {{ Γ ⊢ Π A B ≈ Type@i : Type@j }}.
-Proof.
-  intros ** ?.
-  assert {{ Γ ⊨ Π A B ≈ Type@i : Type@j }} as [env_relΓ] by mauto using completeness_fundamental_exp_eq.
-  destruct_conjs.
-  assert (exists p p', initial_env Γ p /\ initial_env Γ p' /\ {{ Dom p ≈ p' ∈ env_relΓ }}) by mauto using per_ctx_then_per_env_initial_env.
-  destruct_conjs.
-  functional_initial_env_rewrite_clear.
-  (on_all_hyp: destruct_rel_by_assumption env_relΓ).
-  destruct_by_head rel_typ.
-  invert_rel_typ_body.
-  destruct_by_head rel_exp.
-  invert_rel_typ_body.
-  destruct_conjs.
-  match_by_head1 per_univ_elem invert_per_univ_elem.
-Qed.
-
-#[export]
-Hint Resolve not_exp_eq_typ_pi : mcltt.
-
 Corollary wf_fn_inversion : forall {Γ A M C},
     {{ Γ ⊢ λ A M : C }} ->
     exists i B, {{ Γ ⊢ A : Type@i }} /\ {{ Γ, A ⊢ B : Type@i }} /\ {{ Γ ⊢ Π A B ≈ C : Type@i }}.

theories/Core/Completeness/Consequences/Types.v

@@ -0,0 +1,116 @@
+From Coq Require Import RelationClasses.
+From Mcltt Require Import Base LibTactics.
+From Mcltt.Core Require Import Completeness Completeness.FundamentalTheorem Completeness.LogicalRelation Semantic.Realizability.
+From Mcltt.Core Require Export SystemOpt.
+Import Domain_Notations.
+
+Lemma exp_eq_typ_implies_eq_level : forall {Γ i j k},
+    {{ Γ ⊢ Type@i ≈ Type@j : Type@k }} ->
+    i = j.
+Proof with mautosolve.
+  intros * H.
+  assert {{ Γ ⊨ Type@i ≈ Type@j : Type@k }} as [env_relΓ] by eauto using completeness_fundamental_exp_eq.
+  destruct_conjs.
+  assert (exists p p', initial_env Γ p /\ initial_env Γ p' /\ {{ Dom p ≈ p' ∈ env_relΓ }}) as [p [? [? []]]] by eauto using per_ctx_then_per_env_initial_env.
+  functional_initial_env_rewrite_clear.
+  (on_all_hyp: destruct_rel_by_assumption env_relΓ).
+  destruct_by_head rel_typ.
+  invert_rel_typ_body.
+  destruct_by_head rel_exp.
+  invert_rel_typ_body.
+  destruct_conjs.
+  match_by_head1 per_univ_elem invert_per_univ_elem.
+  reflexivity.
+Qed.
+
+#[export]
+Hint Resolve exp_eq_typ_implies_eq_level : mcltt.
+
+Theorem not_exp_eq_typ_nat : forall Γ i j,
+    ~ {{ Γ ⊢ ℕ ≈ Type@i : Type@j }}.
+Proof.
+  intros ** ?.
+  assert {{ Γ ⊨ ℕ ≈ Type@i : Type@j }} as [env_relΓ] by mauto using completeness_fundamental_exp_eq.
+  destruct_conjs.
+  assert (exists p p', initial_env Γ p /\ initial_env Γ p' /\ {{ Dom p ≈ p' ∈ env_relΓ }}) by mauto using per_ctx_then_per_env_initial_env.
+  destruct_conjs.
+  functional_initial_env_rewrite_clear.
+  (on_all_hyp: destruct_rel_by_assumption env_relΓ).
+  destruct_by_head rel_typ.
+  invert_rel_typ_body.
+  destruct_by_head rel_exp.
+  invert_rel_typ_body.
+  destruct_conjs.
+  match_by_head1 per_univ_elem invert_per_univ_elem.
+Qed.
+
+#[export]
+Hint Resolve not_exp_eq_typ_nat : mcltt.
+
+Theorem not_exp_eq_typ_pi : forall Γ i A B j,
+    ~ {{ Γ ⊢ Π A B ≈ Type@i : Type@j }}.
+Proof.
+  intros ** ?.
+  assert {{ Γ ⊨ Π A B ≈ Type@i : Type@j }} as [env_relΓ] by mauto using completeness_fundamental_exp_eq.
+  destruct_conjs.
+  assert (exists p p', initial_env Γ p /\ initial_env Γ p' /\ {{ Dom p ≈ p' ∈ env_relΓ }}) by mauto using per_ctx_then_per_env_initial_env.
+  destruct_conjs.
+  functional_initial_env_rewrite_clear.
+  (on_all_hyp: destruct_rel_by_assumption env_relΓ).
+  destruct_by_head rel_typ.
+  invert_rel_typ_body.
+  destruct_by_head rel_exp.
+  invert_rel_typ_body.
+  destruct_conjs.
+  match_by_head1 per_univ_elem invert_per_univ_elem.
+Qed.
+
+#[export]
+Hint Resolve not_exp_eq_typ_pi : mcltt.
+
+Lemma typ_subsumption_spec : forall {Γ A A'},
+    {{ Γ ⊢ A ⊆ A' }} ->
+    {{ ⊢ Γ }} /\ exists j, {{ Γ ⊢ A ≈ A' : Type@j }} \/ exists i i', i < i' /\ {{ Γ ⊢ Type@i ≈ A : Type@j }} /\ {{ Γ ⊢ A' ≈ Type@i' : Type@j }}.
+Proof.
+  intros * H.
+  dependent induction H; split; mauto 3.
+  - (* typ_subsumption_typ *)
+    eexists.
+    right.
+    do 2 eexists.
+    repeat split; revgoals; mauto.
+  - (* typ_subsumption_trans *)
+    destruct IHtyp_subsumption1 as [? [? [| [i1 [i1']]]]]; destruct IHtyp_subsumption2 as [? [? [| [i2 [i2']]]]];
+      destruct_conjs;
+      only 1: mautosolve 4;
+      eexists; right; do 2 eexists.
+    + (* left & right *)
+      split; [eassumption |].
+      solve [mauto using lift_exp_eq_max_left].
+    + (* right & left *)
+      split; [eassumption |].
+      solve [mauto using lift_exp_eq_max_right].
+    + exvar nat ltac:(fun j => assert {{ Γ ⊢ Type@i2 ≈ Type@i1' : Type@j }} by mauto).
+      replace i2 with i1' in * by mauto.
+      split; [etransitivity; revgoals; eassumption |].
+      mauto 4 using lift_exp_eq_max_left, lift_exp_eq_max_right.
+Qed.
+
+#[export]
+Hint Resolve typ_subsumption_spec : mcltt.
+
+Lemma typ_subsumption_typ_spec : forall {Γ i i'},
+    {{ Γ ⊢ Type@i ⊆ Type@i' }} ->
+    {{ ⊢ Γ }} /\ i <= i'.
+Proof with mautosolve.
+  intros * [? [j [| [i0 [i0']]]]]%typ_subsumption_spec.
+  - (* when lhs is equivalent to rhs *)
+    replace i with i' in *...
+  - (* when lhs is (strictly) subsumed by rhs *)
+    destruct_conjs.
+    (on_all_hyp: fun H => apply exp_eq_typ_implies_eq_level in H); subst.
+    split; [| lia]...
+Qed.
+
+#[export]
+Hint Resolve typ_subsumption_typ_spec : mcltt.

theories/Core/Syntactic/CoreInversions.v

@@ -3,29 +3,6 @@ From Mcltt Require Import Base LibTactics.
 From Mcltt.Core Require Export SystemOpt.
 Import Syntax_Notations.
 
-Lemma wf_univ_inversion : forall {Γ i A},
-    {{ Γ ⊢ Type@i : A }} ->
-    {{ Γ ⊢ Type@(S i) ⊆ A }}.
-Proof.
-  intros * H.
-  dependent induction H; mautosolve.
-Qed.
-
-#[export]
-Hint Resolve wf_univ_inversion : mcltt.
-
-Lemma wf_nat_inversion : forall Γ A,
-    {{ Γ ⊢ ℕ : A }} ->
-    {{ Γ ⊢ Type@0 ⊆ A }}.
-Proof.
-  intros * H.
-  assert (forall i, 0 <= i) by lia.
-  dependent induction H; mautosolve 4.
-Qed.
-
-#[export]
-Hint Resolve wf_nat_inversion : mcltt.
-
 Lemma wf_natrec_inversion : forall Γ A M A' MZ MS,
     {{ Γ ⊢ rec M return A' | zero -> MZ | succ -> MS end : A }} ->
     {{ Γ ⊢ M : ℕ }} /\ {{ Γ ⊢ MZ : A'[Id,,zero] }} /\ {{ Γ, ℕ, A' ⊢ MS : A'[Wk∘Wk,,succ(#1)] }} /\ {{ Γ ⊢ A'[Id,,M] ⊆ A }}.
@@ -41,18 +18,6 @@ Qed.
 #[export]
 Hint Resolve wf_natrec_inversion : mcltt.
 
-Lemma wf_pi_inversion : forall {Γ A B C},
-    {{ Γ ⊢ Π A B : C }} ->
-    exists i, {{ Γ ⊢ A : Type@i }} /\ {{ Γ, A ⊢ B : Type@i }} /\ {{ Γ ⊢ Type@i ⊆ C }}.
-Proof.
-  intros * H.
-  dependent induction H; assert {{ ⊢ Γ }} by mauto 3; try solve [eexists; mauto 4];
-    specialize (IHwf_exp _ _ eq_refl); destruct_conjs; eexists; repeat split; mauto 3.
-Qed.
-
-#[export]
-Hint Resolve wf_pi_inversion : mcltt.
-
 Lemma wf_app_inversion : forall {Γ M N C},
     {{ Γ ⊢ M N : C }} ->
     exists A B, {{ Γ ⊢ M : Π A B }} /\ {{ Γ ⊢ N : A }} /\ {{ Γ ⊢ B[Id,,N] ⊆ C }}.
@@ -132,7 +97,7 @@ Proof with mautosolve 4.
   specialize (IHwf_sub _ _ eq_refl).
   destruct_conjs.
   eexists.
-  repeat split; mauto.
+  repeat split...
 Qed.
 
 #[export]

theories/Core/Syntactic/CoreTypeInversions.v

@@ -0,0 +1,54 @@
+From Coq Require Import Setoid.
+From Mcltt Require Import Base LibTactics.
+From Mcltt.Core Require Export System.
+Import Syntax_Notations.
+
+Lemma wf_univ_inversion : forall {Γ i A},
+    {{ Γ ⊢ Type@i : A }} ->
+    {{ Γ ⊢ Type@(S i) ⊆ A }}.
+Proof.
+  intros * H.
+  dependent induction H; mautosolve.
+Qed.
+
+#[export]
+Hint Resolve wf_univ_inversion : mcltt.
+
+Lemma wf_nat_inversion : forall Γ A,
+    {{ Γ ⊢ ℕ : A }} ->
+    {{ Γ ⊢ Type@0 ⊆ A }}.
+Proof.
+  intros * H.
+  assert (forall i, 0 <= i) by lia.
+  dependent induction H; mautosolve 4.
+Qed.
+
+#[export]
+Hint Resolve wf_nat_inversion : mcltt.
+
+Lemma wf_pi_inversion : forall {Γ A B C},
+    {{ Γ ⊢ Π A B : C }} ->
+    exists i, {{ Γ ⊢ A : Type@i }} /\ {{ Γ, A ⊢ B : Type@i }} /\ {{ Γ ⊢ Type@i ⊆ C }}.
+Proof.
+  intros * H.
+  dependent induction H; assert {{ ⊢ Γ }} by mauto 3; try solve [eexists; mauto 4];
+    specialize (IHwf_exp _ _ eq_refl); destruct_conjs; eexists; repeat split; mauto 3.
+Qed.
+
+#[export]
+Hint Resolve wf_pi_inversion : mcltt.
+
+Corollary wf_pi_inversion' : forall {Γ A B i},
+    {{ Γ ⊢ Π A B : Type@i }} ->
+    {{ Γ ⊢ A : Type@i }} /\ {{ Γ, A ⊢ B : Type@i }}.
+Proof with mautosolve 4.
+  intros * [j [? []]]%wf_pi_inversion.
+  assert {{ Γ, A ⊢s Wk : Γ }} by mauto 4.
+  assert {{ Γ, A ⊢ Type@j ⊆ Type@j[Wk] }} by mauto 4.
+  assert {{ Γ, A ⊢ Type@j[Wk] ⊆ Type@i[Wk] }} by mauto 4.
+  assert {{ Γ, A ⊢ Type@i[Wk] ⊆ Type@i }} by mauto 4.
+  assert {{ Γ, A ⊢ Type@j ⊆ Type@i }}...
+Qed.
+
+#[export]
+Hint Resolve wf_pi_inversion' : mcltt.

theories/Core/Syntactic/System/Definitions.v

@@ -39,7 +39,7 @@ with wf_ctx_eq : ctx -> ctx -> Prop :=
 where "⊢ Γ ≈ Γ'" := (wf_ctx_eq Γ Γ') (in custom judg) : type_scope
 
 with wf_exp : ctx -> exp -> typ -> Prop :=
-| wf_univ :
+| wf_typ :
   `( {{ ⊢ Γ }} ->
      {{ Γ ⊢ Type@i : Type@(S i) }} )
 | wf_nat :

theories/Core/Syntactic/System/Lemmas.v

@@ -145,14 +145,6 @@ Qed.
 #[export]
 Hint Resolve presup_exp_eq_ctx : mcltt.
 
-Lemma wf_pi_syntactic_inversion : forall {Γ A B C},
-    {{ Γ ⊢ Π A B : C }} ->
-    exists i, {{ Γ ⊢ A : Type@i }} /\ {{ Γ, A ⊢ B : Type@i }}.
-Proof.
-  intros * H.
-  dependent induction H; mauto 4.
-Qed.
-
 Lemma exp_eq_refl : forall {Γ M A}, {{ Γ ⊢ M : A }} -> {{ Γ ⊢ M ≈ M : A }}.
 Proof.
   mauto.
@@ -169,6 +161,19 @@ Qed.
 #[export]
 Hint Resolve sub_eq_refl : mcltt.
 
+Lemma exp_eq_trans_typ_max : forall {Γ i i' A A' A''},
+    {{ Γ ⊢ A ≈ A' : Type@i }} ->
+    {{ Γ ⊢ A' ≈ A'' : Type@i' }} ->
+    {{ Γ ⊢ A ≈ A'' : Type@(max i i') }}.
+Proof with mautosolve 4.
+  intros.
+  assert {{ Γ ⊢ A ≈ A' : Type@(max i i') }} by eauto using lift_exp_eq_max_left.
+  assert {{ Γ ⊢ A' ≈ A'' : Type@(max i i') }} by eauto using lift_exp_eq_max_right...
+Qed.
+
+#[export]
+Hint Resolve exp_eq_trans_typ_max : mcltt.
+
 Lemma exp_sub_typ : forall {Δ Γ A σ i}, {{ Δ ⊢ A : Type@i }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢ A[σ] : Type@i }}.
 Proof.
   mauto.
@@ -711,6 +716,17 @@ Qed.
 #[export]
 Hint Resolve sub_eq_q_sigma_compose_weak_weak_extend_succ_var_1 : mcltt.
 
+Lemma typ_subsumption_wf_ctx : forall {Γ A A'},
+    {{ Γ ⊢ A ⊆ A' }} ->
+    {{ ⊢ Γ }}.
+Proof.
+  intros * H.
+  dependent induction H; mauto.
+Qed.
+
+#[export]
+Hint Resolve typ_subsumption_wf_ctx : mcltt.
+
 Fact typ_subsumption_refl : forall {Γ A i},
     {{ Γ ⊢ A : Type@i }} ->
     {{ Γ ⊢ A ⊆ A }}.
@@ -732,6 +748,22 @@ Qed.
 #[export]
 Hint Resolve typ_subsumption_ge : mcltt.
 
+Lemma typ_subsumption_sub : forall {Γ σ Δ A A'},
+    {{ Γ ⊢s σ : Δ }} ->
+    {{ Δ ⊢ A ⊆ A' }} ->
+    {{ Γ ⊢ A[σ] ⊆ A'[σ] }}.
+Proof.
+  intros * Hsub H.
+  dependent induction H.
+  - etransitivity; [do 2 econstructor; eassumption |].
+    etransitivity; mauto.
+  - mauto.
+  - mauto.
+Qed.
+
+#[export]
+Hint Resolve typ_subsumption_sub : mcltt.
+
 Lemma wf_exp_respects_typ_subsumption : forall {Γ M A A'},
     {{ Γ ⊢ M : A }} ->
     {{ Γ ⊢ A ⊆ A' }} ->