Add inversion lemmas

theories/Core/Completeness/Consequences/Inversions.v

@@ -0,0 +1,99 @@
+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 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.
+  - (* wf_cumu *)
+    assert (exists j : nat, {{ Γ ⊢ ℕ ≈ Type@i : Type@j }}) as [j contra] by eauto.
+    contradict contra...
+Qed.
+
+Corollary wf_succ_inversion : forall Γ A M,
+    {{ Γ ⊢ succ M : A }} ->
+    {{ Γ ⊢ M : ℕ }} /\ exists i, {{ Γ ⊢ ℕ ≈ A : Type@i }}.
+Proof with mautosolve.
+  intros * H.
+  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.
+  - (* 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 }}.
+Proof with mautosolve 4.
+  intros * H.
+  dependent induction H.
+  - (* wf_fn *)
+    gen_presups.
+    exvar nat ltac:(fun i => assert {{ Γ ⊢ A : Type @ i }} by (eapply lift_exp_max_left; eauto)).
+    exvar nat ltac:(fun i => assert {{ Γ, A ⊢ B : Type @ i }} by (eapply lift_exp_max_right; eauto)).
+    do 2 eexists.
+    repeat split...
+  - (* wf_conv *)
+    specialize (IHwf_exp _ _ eq_refl) as [i0 [? [? []]]].
+    exists (max i i0).
+    eexists.
+    repeat split;
+      mauto 4 using lift_exp_max_right, lift_exp_eq_max_left, lift_exp_eq_max_right.
+  - (* wf_cumu *)
+    specialize (IHwf_exp _ _ eq_refl) as [? [? [? [? contra]]]].
+    contradict contra...
+Qed.

theories/Core/Syntactic/CoreInversions.v

@@ -0,0 +1,150 @@
+From Coq Require Import Setoid.
+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 }}.
+Proof with mautosolve 4.
+  intros * H.
+  pose (A0 := A).
+  dependent induction H;
+    try (specialize (IHwf_exp _ _ _ _ eq_refl); destruct_conjs; repeat split; mautosolve 4).
+  assert {{ Γ ⊢s Id : Γ }} by mauto 3.
+  repeat split...
+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 }}.
+Proof with mautosolve 4.
+  intros * H.
+  dependent induction H;
+    try solve [do 2 eexists; repeat split; mauto 4];
+    specialize (IHwf_exp _ _ eq_refl); destruct_conjs; do 2 eexists; repeat split...
+Qed.
+
+#[export]
+Hint Resolve wf_app_inversion : mcltt.
+
+Lemma wf_vlookup_inversion : forall {Γ x A},
+    {{ Γ ⊢ #x : A }} ->
+    exists A', {{ #x : A' ∈ Γ }} /\ {{ Γ ⊢ A' ⊆ A }}.
+Proof with mautosolve 4.
+  intros * H.
+  dependent induction H;
+    try (specialize (IHwf_exp _ eq_refl); destruct_conjs; eexists; split; mautosolve 4).
+  assert (exists i, {{ Γ ⊢ A : Type@i }}) as []...
+Qed.
+
+#[export]
+Hint Resolve wf_vlookup_inversion : mcltt.
+
+Lemma wf_exp_sub_inversion : forall {Γ M σ A},
+    {{ Γ ⊢ M[σ] : A }} ->
+    exists Δ A', {{ Γ ⊢s σ : Δ }} /\ {{ Δ ⊢ M : A' }} /\ {{ Γ ⊢ A'[σ] ⊆ A }}.
+Proof with mautosolve 4.
+  intros * H.
+  dependent induction H;
+    try (specialize (IHwf_exp _ _ eq_refl); destruct_conjs; do 2 eexists; repeat split; mautosolve 4).
+  gen_presups.
+  do 2 eexists.
+  repeat split...
+Qed.
+
+#[export]
+Hint Resolve wf_exp_sub_inversion : mcltt.
+
+(* [wf_conv] and [wf_cumu] do not give useful inversions *)
+
+Lemma wf_sub_id_inversion : forall Γ Δ,
+    {{ Γ ⊢s Id : Δ }} ->
+    {{ ⊢ Γ ≈ Δ }}.
+Proof.
+  intros * H.
+  dependent induction H; mauto.
+Qed.
+
+#[export]
+Hint Resolve wf_sub_id_inversion : mcltt.
+
+Lemma wf_sub_weaken_inversion : forall {Γ Δ},
+    {{ Γ ⊢s Wk : Δ }} ->
+    exists A, {{ ⊢ Γ ≈ Δ, A }}.
+Proof with mautosolve 4.
+  intros * H.
+  dependent induction H; mauto.
+  specialize (IHwf_sub eq_refl).
+  destruct_conjs.
+  eexists.
+  gen_presups.
+  etransitivity...
+Qed.
+
+#[export]
+Hint Resolve wf_sub_weaken_inversion : mcltt.
+
+Lemma wf_sub_compose_inversion : forall {Γ1 σ1 σ2 Γ3},
+    {{ Γ1 ⊢s σ1 ∘ σ2 : Γ3 }} ->
+    exists Γ2, {{ Γ1 ⊢s σ2 : Γ2 }} /\ {{ Γ2 ⊢s σ1 : Γ3 }}.
+Proof with mautosolve 4.
+  intros * H.
+  dependent induction H; mauto.
+  specialize (IHwf_sub _ _ eq_refl).
+  destruct_conjs.
+  eexists.
+  repeat split; mauto.
+Qed.
+
+#[export]
+Hint Resolve wf_sub_compose_inversion : mcltt.
+
+Lemma wf_sub_extend_inversion : forall {Γ σ M Δ},
+    {{ Γ ⊢s σ,,M : Δ }} ->
+    exists Δ' A', {{ Γ ⊢s σ : Δ' }} /\ {{ Γ ⊢ M : A' }}.
+Proof with mautosolve 4.
+  intros * H.
+  dependent induction H...
+Qed.
+
+#[export]
+Hint Resolve wf_sub_extend_inversion : mcltt.

theories/Core/Syntactic/Corollaries.v

@@ -1,19 +1,8 @@
 From Coq Require Import Setoid.
 From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Export SystemOpt.
+From Mcltt.Core Require Export SystemOpt CoreInversions.
 Import Syntax_Notations.
 
-Corollary invert_id : forall Γ Δ,
-    {{ Γ ⊢s Id : Δ }} ->
-    {{ ⊢ Γ ≈ Δ }}.
-Proof.
-  intros * H.
-  dependent induction H; mauto.
-Qed.
-
-#[export]
-Hint Resolve invert_id : mcltt.
-
 Corollary sub_id_typ : forall Γ M A,
     {{ Γ ⊢ M : A }} ->
     {{ Γ ⊢ M : A [ Id ] }}.
@@ -30,8 +19,8 @@ Corollary invert_sub_id : forall Γ M A,
     {{ Γ ⊢ M [ Id ] : A }} ->
     {{ Γ ⊢ M : A }}.
 Proof.
-  intros * H.
-  dependent induction H; mauto.
+  intros * [? [? [?%wf_sub_id_inversion []]]]%wf_exp_sub_inversion.
+  mauto.
 Qed.
 
 #[export]

theories/Core/Syntactic/CtxEq.v

@@ -107,3 +107,11 @@ Qed.
 
 #[export]
 Hint Resolve ctx_eq_trans : mcltt.
+
+#[export]
+Instance wf_ctx_PER : PER wf_ctx_eq.
+Proof.
+  split.
+  - eauto using ctx_eq_sym.
+  - eauto using ctx_eq_trans.
+Qed.

theories/Core/Syntactic/System/Lemmas.v

@@ -711,6 +711,16 @@ Qed.
 #[export]
 Hint Resolve sub_eq_q_sigma_compose_weak_weak_extend_succ_var_1 : mcltt.
 
+Fact typ_subsumption_refl : forall {Γ A i},
+    {{ Γ ⊢ A : Type@i }} ->
+    {{ Γ ⊢ A ⊆ A }}.
+Proof.
+  mauto.
+Qed.
+
+#[export]
+Hint Resolve typ_subsumption_refl : mcltt.
+
 Lemma typ_subsumption_ge : forall {Γ i j},
     {{ ⊢ Γ }} ->
     i <= j ->

theories/LibTactics.v

@@ -206,6 +206,9 @@ Tactic Notation "mauto" int_or_var(pow) "using" uconstr(use) :=
 Tactic Notation "mauto" int_or_var(pow) "using" uconstr(use1) "," uconstr(use2) :=
   eauto pow using use1, use2 with mcltt core.
 
+Tactic Notation "mauto" int_or_var(pow) "using" uconstr(use1) "," uconstr(use2) "," uconstr(use3) :=
+  eauto pow using use1, use2, use3 with mcltt core.
+
 Tactic Notation "mauto" int_or_var(pow) "using" uconstr(use1) "," uconstr(use2) "," uconstr(use3) "," uconstr(use4) :=
   eauto pow using use1, use2, use3, use4 with mcltt core.
 

theories/_CoqProject

@@ -4,6 +4,7 @@
 
 ./Core/Axioms.v
 ./Core/Base.v
+./Core/Completeness/Consequences/Inversions.v
 ./Core/Completeness/ContextCases.v
 ./Core/Completeness/FunctionCases.v
 ./Core/Completeness/FundamentalTheorem.v
@@ -31,6 +32,7 @@
 ./Core/Semantic/Readback/Lemmas.v
 ./Core/Semantic/Realizability.v
 ./Core/Semantic/NbE.v
+./Core/Syntactic/CoreInversions.v
 ./Core/Syntactic/Corollaries.v
 ./Core/Syntactic/CtxEq.v
 ./Core/Syntactic/Presup.v