Fix inversion lemmas

theories/Core/Completeness/Consequences/Inversions.v

@@ -4,52 +4,32 @@ From Mcltt.Core Require Import Completeness Semantic.Realizability Completeness.
 From Mcltt.Core Require Export SystemOpt CoreInversions.
 Import Domain_Notations.
 
-Corollary wf_zero_inversion : forall Γ A,
+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...
-  - (* wf_cumu *)
-    assert (exists j : nat, {{ Γ ⊢ ℕ ≈ Type@i : Type@j }}) as [j contra] by eauto.
-    contradict contra...
+  intros * []%wf_zero_inversion%typ_subsumption_left_nat...
 Qed.
 
-Corollary wf_succ_inversion : forall Γ A M,
+#[export]
+Hint Resolve wf_zero_inversion' : mcltt.
+
+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...
-  - (* wf_cumu *)
-    assert ({{ Γ ⊢ M : ℕ }} /\ exists j : nat, {{ Γ ⊢ ℕ ≈ Type@i : Type@j }}) as [? [? contra]] by eauto.
-    contradict contra...
+  intros * [? []%typ_subsumption_left_nat]%wf_succ_inversion...
 Qed.
 
-Corollary wf_fn_inversion : forall {Γ A M C},
+#[export]
+Hint Resolve wf_succ_inversion' : 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...
+    exists B, {{ Γ, A ⊢ M : B }} /\ exists i, {{ Γ ⊢ Π A B ≈ C : Type@i }}.
+Proof with mautosolve.
+  intros * [? [? []%typ_subsumption_left_pi]]%wf_fn_inversion...
 Qed.
+
+#[export]
+Hint Resolve wf_fn_inversion' : mcltt.

theories/Core/Completeness/Consequences/Types.v

@@ -26,32 +26,22 @@ 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.
+Inductive is_typ_constr : typ -> Prop :=
+| typ_is_typ_constr : forall i, is_typ_constr {{{ Type@i }}}
+| nat_is_typ_constr : is_typ_constr {{{ ℕ }}}
+| pi_is_typ_constr : forall A B, is_typ_constr {{{ Π A B }}}
+.
 
 #[export]
-Hint Resolve not_exp_eq_typ_nat : mcltt.
+Hint Constructors is_typ_constr : mcltt.
 
-Theorem not_exp_eq_typ_pi : forall Γ i A B j,
-    ~ {{ Γ ⊢ Π A B ≈ Type@i : Type@j }}.
+Theorem is_typ_constr_and_not_typ_implies_not_exp_eq_typ : forall Γ A j k,
+    is_typ_constr A ->
+    (forall i, A <> {{{ Type@i }}}) ->
+    ~ {{ Γ ⊢ A ≈ Type@j : Type@k }}.
 Proof.
-  intros ** ?.
-  assert {{ Γ ⊨ Π A B ≈ Type@i : Type@j }} as [env_relΓ] by mauto using completeness_fundamental_exp_eq.
+  intros * Histyp ? ?.
+  assert {{ Γ ⊨ A ≈ Type@j : Type@k }} 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.
@@ -60,14 +50,18 @@ Proof.
   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.
+  destruct Histyp;
+    invert_rel_typ_body;
+    destruct_conjs;
+    match_by_head1 per_univ_elem invert_per_univ_elem.
+  congruence.
 Qed.
 
 #[export]
-Hint Resolve not_exp_eq_typ_pi : mcltt.
+Hint Resolve is_typ_constr_and_not_typ_implies_not_exp_eq_typ : mcltt.
 
+(* We cannot use this spec as the definition of [typ_subsumption] as
+   then its transitivity requires [exp_eq_typ_implies_eq_level] or a similar semantic lemma *)
 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 }}.
@@ -99,17 +93,64 @@ Qed.
 #[export]
 Hint Resolve typ_subsumption_spec : mcltt.
 
-Lemma typ_subsumption_typ_spec : forall {Γ i i'},
+Lemma not_typ_implies_typ_subsumption_left_typ_constr : forall {Γ A A'},
+    is_typ_constr A ->
+    (forall i, A <> {{{ Type@i }}}) ->
+    {{ Γ ⊢ A ⊆ A' }} ->
+    exists j, {{ Γ ⊢ A ≈ A' : Type@j }}.
+Proof.
+  intros * ? ? H%typ_subsumption_spec.
+  destruct_all; mauto.
+  exfalso.
+  eapply is_typ_constr_and_not_typ_implies_not_exp_eq_typ; mauto 4.
+Qed.
+
+#[export]
+Hint Resolve not_typ_implies_typ_subsumption_left_typ_constr : mcltt.
+
+Corollary typ_subsumption_left_nat : forall {Γ A'},
+    {{ Γ ⊢ ℕ ⊆ A' }} ->
+    exists j, {{ Γ ⊢ ℕ ≈ A' : Type@j }}.
+Proof.
+  intros * H%not_typ_implies_typ_subsumption_left_typ_constr; mauto.
+  congruence.
+Qed.
+
+#[export]
+Hint Resolve typ_subsumption_left_nat : mcltt.
+
+Corollary typ_subsumption_left_pi : forall {Γ A B C'},
+    {{ Γ ⊢ Π A B ⊆ C' }} ->
+    exists j, {{ Γ ⊢ Π A B ≈ C' : Type@j }}.
+Proof.
+  intros * H%not_typ_implies_typ_subsumption_left_typ_constr; mauto.
+  congruence.
+Qed.
+
+#[export]
+Hint Resolve typ_subsumption_left_pi : mcltt.
+
+Lemma typ_subsumption_left_typ : forall {Γ i A'},
+    {{ Γ ⊢ Type@i ⊆ A' }} ->
+    exists j i', i <= i' /\ {{ Γ ⊢ A' ≈ Type@i' : Type@j }}.
+Proof.
+  intros * H%typ_subsumption_spec.
+  destruct_all; mauto.
+  (on_all_hyp: fun H => apply exp_eq_typ_implies_eq_level in H); subst.
+  mauto using PeanoNat.Nat.lt_le_incl.
+Qed.
+
+#[export]
+Hint Resolve typ_subsumption_left_typ : mcltt.
+
+Corollary 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]...
+  intros * H.
+  pose proof (typ_subsumption_left_typ H).
+  destruct_conjs.
+  (on_all_hyp: fun H => apply exp_eq_typ_implies_eq_level in H); subst...
 Qed.
 
 #[export]

theories/Core/Syntactic/CoreInversions.v

@@ -3,29 +3,71 @@ From Mcltt Require Import Base LibTactics.
 From Mcltt.Core Require Export SystemOpt.
 Import Syntax_Notations.
 
+Corollary wf_zero_inversion : forall Γ A,
+    {{ Γ ⊢ zero : A }} ->
+    {{ Γ ⊢ ℕ ⊆ A }}.
+Proof with mautosolve 4.
+  intros * H.
+  dependent induction H;
+    try specialize (IHwf_exp eq_refl)...
+Qed.
+
+#[export]
+Hint Resolve wf_zero_inversion : mcltt.
+
+Corollary wf_succ_inversion : forall Γ A M,
+    {{ Γ ⊢ succ M : A }} ->
+    {{ Γ ⊢ M : ℕ }} /\ {{ Γ ⊢ ℕ ⊆ A }}.
+Proof with mautosolve.
+  intros * H.
+  dependent induction H;
+    try specialize (IHwf_exp _ eq_refl);
+    destruct_conjs...
+Qed.
+
+#[export]
+Hint Resolve wf_succ_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 }}.
+    {{ Γ ⊢ MZ : A'[Id,,zero] }} /\ {{ Γ, ℕ, A' ⊢ MS : A'[Wk∘Wk,,succ(#1)] }} /\ {{ Γ ⊢ M : ℕ }} /\ {{ Γ ⊢ 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...
+    try (specialize (IHwf_exp _ _ _ _ eq_refl));
+    destruct_conjs;
+    assert {{ Γ ⊢s Id : Γ }} by mauto 3;
+    repeat split...
 Qed.
 
 #[export]
 Hint Resolve wf_natrec_inversion : mcltt.
 
+Corollary wf_fn_inversion : forall {Γ A M C},
+    {{ Γ ⊢ λ A M : C }} ->
+    exists B, {{ Γ, A ⊢ M : B }} /\ {{ Γ ⊢ Π A B ⊆ C }}.
+Proof with mautosolve 4.
+  intros * H.
+  dependent induction H;
+    try specialize (IHwf_exp _ _ eq_refl);
+    destruct_conjs;
+    gen_presups;
+    eexists; split...
+Qed.
+
+#[export]
+Hint Resolve wf_fn_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...
+    try specialize (IHwf_exp _ _ eq_refl);
+    destruct_conjs;
+    do 2 eexists; repeat split...
 Qed.
 
 #[export]
@@ -37,8 +79,10 @@ Lemma wf_vlookup_inversion : forall {Γ x 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 []...
+    [assert (exists i, {{ Γ ⊢ A : Type@i }}) as [] by mauto 4 | |];
+    try (specialize (IHwf_exp _ eq_refl));
+    destruct_conjs;
+    eexists; split...
 Qed.
 
 #[export]
@@ -50,10 +94,10 @@ Lemma wf_exp_sub_inversion : forall {Γ M σ 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...
+    try (specialize (IHwf_exp _ _ eq_refl));
+    destruct_conjs;
+    gen_presups;
+    do 2 eexists; split...
 Qed.
 
 #[export]
@@ -66,7 +110,7 @@ Lemma wf_sub_id_inversion : forall Γ Δ,
     {{ ⊢ Γ ≈ Δ }}.
 Proof.
   intros * H.
-  dependent induction H; mauto.
+  dependent induction H; mautosolve.
 Qed.
 
 #[export]
@@ -80,8 +124,8 @@ Proof with mautosolve 4.
   dependent induction H; mauto.
   specialize (IHwf_sub eq_refl).
   destruct_conjs.
-  eexists.
   gen_presups.
+  eexists.
   etransitivity...
 Qed.
 
@@ -105,10 +149,13 @@ Hint Resolve wf_sub_compose_inversion : mcltt.
 
 Lemma wf_sub_extend_inversion : forall {Γ σ M Δ},
     {{ Γ ⊢s σ,,M : Δ }} ->
-    exists Δ' A', {{ Γ ⊢s σ : Δ' }} /\ {{ Γ ⊢ M : A' }}.
+    exists Δ' A', {{ ⊢ Δ ≈ Δ', A' }} /\ {{ Γ ⊢s σ : Δ' }} /\ {{ Γ ⊢ M : A'[σ] }}.
 Proof with mautosolve 4.
   intros * H.
-  dependent induction H...
+  dependent induction H;
+    try specialize (IHwf_sub _ _ eq_refl);
+    destruct_conjs;
+    do 2 eexists; split...
 Qed.
 
 #[export]