Update semantic consequences a bit (#247)

theories/Core/Semantic/Consequences.v

@@ -24,15 +24,15 @@ Lemma adjust_exp_eq_level : forall {Γ A A' i j},
     {{ Γ ⊢ A' : Type@j }} ->
     {{ Γ ⊢ A ≈ A' : Type@j }}.
 Proof.
-  intros * ?%completeness ?%soundness ?%soundness.
+  intros * ?%completeness_ty ?%soundness ?%soundness.
   destruct_conjs.
-  inversion_by_head nbe; subst.
-  match_by_head eval_exp ltac:(fun H => directed inversion H; subst; clear H).
-  match_by_head read_nf ltac:(fun H => directed inversion H; subst; clear H).
+  dir_inversion_by_head nbe; dir_inversion_by_head nbe_ty; subst.
+  match_by_head eval_exp ltac:(fun H => progressive_invert H).
+  match_by_head read_nf ltac:(fun H => progressive_invert H).
   functional_initial_env_rewrite_clear.
   functional_eval_rewrite_clear.
   functional_read_rewrite_clear.
-  etransitivity; [symmetry|]; mautosolve.
+  etransitivity; [| symmetry]; eauto.
 Qed.
 
 Lemma exp_eq_pi_inversion : forall {Γ A B A' B' i},
@@ -42,42 +42,42 @@ Proof.
   intros * H.
   gen_presups.
   (on_all_hyp: fun H => apply wf_pi_inversion' in H; destruct H).
-  (on_all_hyp: fun H => apply completeness in H).
+  (on_all_hyp: fun H => apply completeness_ty in H).
   (on_all_hyp: fun H => pose proof (soundness H)).
   destruct_conjs.
   dir_inversion_clear_by_head nbe.
+  dir_inversion_clear_by_head nbe_ty.
   dir_inversion_by_head initial_env; subst.
   functional_initial_env_rewrite_clear.
   invert_rel_typ_body.
   dir_inversion_clear_by_head read_nf.
   dir_inversion_by_head read_typ; subst.
   functional_eval_rewrite_clear.
   functional_read_rewrite_clear.
-  match_by_head (@eq nf) ltac:(fun H => directed inversion H; subst; clear H).
-  assert {{ Γ ⊢ A ≈ A' : Type@i }} by mauto.
-  assert {{ ⊢ Γ, A ≈ Γ, A' }} by mauto.
+  autoinjections.
+  assert {{ Γ ⊢ A' ≈ A : Type@i }} by mauto 3.
+  assert {{ ⊢ Γ, A' ≈ Γ, A }} by mauto 3.
   split; [mauto 3 |].
-  etransitivity; mauto 4.
+  etransitivity; [| symmetry]; mauto 2.
 Qed.
 
 Lemma nf_of_pi : forall {Γ M A B},
     {{ Γ ⊢ M : Π A B }} ->
     exists W1 W2, nbe Γ M {{{ Π A B }}} n{{{ λ W1 W2 }}}.
 Proof.
-  intros * ?%soundness.
-  destruct_conjs.
-  inversion_clear_by_head nbe.
+  intros * [? []]%soundness.
+  dir_inversion_clear_by_head nbe.
   invert_rel_typ_body.
-  match_by_head1 read_nf ltac:(fun H => inversion_clear H).
-  do 2 eexists; mauto.
+  dir_inversion_clear_by_head read_nf.
+  do 2 eexists; mauto 4.
 Qed.
 #[export]
 Hint Resolve nf_of_pi : mcltt.
 
 Theorem canonical_form_of_pi : forall {M A B},
     {{ ⋅ ⊢ M : Π A B }} ->
     exists W1 W2, nbe {{{ ⋅ }}} M {{{ Π A B }}} n{{{ λ W1 W2 }}}.
-Proof. mauto. Qed.
+Proof. mauto 3. Qed.
 #[export]
 Hint Resolve canonical_form_of_pi : mcltt.
 
@@ -94,90 +94,105 @@ Theorem canonical_form_of_nat : forall {M},
 Proof with mautosolve 4.
   intros * [? []]%soundness.
   eexists; split; [eassumption |].
-  inversion_clear_by_head nbe.
+  dir_inversion_clear_by_head nbe.
   invert_rel_typ_body.
   match_by_head1 eval_exp ltac:(fun H => clear H).
   gen M.
   match_by_head1 read_nf ltac:(fun H => dependent induction H);
     intros; mauto 3;
     gen_presups.
-  - assert ({{ ⋅ ⊢ M : ℕ }} /\ {{ ⋅ ⊢ ℕ ⊆ ℕ }}) as [? _]...
-  - exfalso.
-    eapply no_closed_neutral...
+  - eassert ({{ ⋅ ⊢ ^_ : ℕ }} /\ {{ ⋅ ⊢ ℕ ⊆ ℕ }}) as [? _]...
+  - match_by_head1 (wf_exp {{{ ⋅ }}} {{{ ℕ }}}) ltac:(fun H => contradict H)...
 Qed.
 #[export]
 Hint Resolve canonical_form_of_nat : mcltt.
 
+Theorem canonical_form_of_typ : forall {i M},
+    {{ ⋅ ⊢ M : Type@i }} ->
+    exists W, nbe {{{ ⋅ }}} M {{{ Type@i }}} W /\ is_typ_constr W /\ (forall V, W <> n{{{ ⇑ V }}}).
+Proof with mautosolve 4.
+  intros * [? []]%soundness.
+  eexists; split; [eassumption |].
+  dir_inversion_clear_by_head nbe.
+  invert_rel_typ_body.
+  match_by_head1 eval_exp ltac:(fun H => clear H).
+  gen M.
+  dir_inversion_clear_by_head read_nf.
+  match_by_head1 read_typ ltac:(fun H => dependent induction H);
+    intros; split; intros; mauto 3; try congruence;
+    gen_presups;
+    match_by_head1 (wf_exp {{{ ⋅ }}} {{{ Type@i }}}) ltac:(fun H => contradict H)...
+Qed.
+#[export]
+Hint Resolve canonical_form_of_typ : mcltt.
+
 Lemma subtyp_spec : forall {Γ A B},
     {{ Γ ⊢ A ⊆ B }} ->
     (exists k, {{ Γ ⊢ A ≈ B : Type@k }}) \/
       (exists i j, (exists k, {{ Γ ⊢ A ≈ Type@i : Type@k }}) /\ (exists k, {{ Γ ⊢ Type@j ≈ B : Type@k }}) /\ i <= j) \/
       (exists A1 A2 B1 B2, (exists k, {{ Γ ⊢ A ≈ Π A1 A2 : Type@k }}) /\ (exists k, {{ Γ ⊢ Π B1 B2 ≈ B : Type@k }}) /\ (exists k, {{ Γ ⊢ A1 ≈ B1 : Type@k }}) /\ {{ Γ, B1 ⊢ A2 ⊆ B2 }}).
-Proof.
+Proof with (congruence + firstorder (mautosolve 4 + lia)).
   induction 1; mauto 3.
   - destruct_all; firstorder (mauto 3);
-      try (right; right; do 4 eexists; repeat split; mautosolve 3).
-    + right; left.
-      match goal with
+      try (right; right; do 4 eexists; firstorder mautosolve 3).
+    + match goal with
       | _: {{ Γ ⊢ M' ≈ Type@?i : Type@_ }},
           _: {{ Γ ⊢ Type@?j ≈ M' : Type@_ }} |- _ =>
           assert {{ Γ ⊢ Type@j ≈ Type@i : Type@_ }} by mauto 3;
           assert (j = i) as -> by mauto 3
-      end.
-      do 2 eexists; repeat split; mauto 3; lia.
+      end...
+    + assert {{ Γ ⊢ Π ^_ ^_ ≈ Type@_ : Type@_ }} by mauto 3.
+      assert ({{{ Π ^_ ^_ }}} = {{{ Type@_ }}}) by mauto 3...
     + assert {{ Γ ⊢ Π ^_ ^_ ≈ Type@_ : Type@_ }} by mauto 3.
-      assert ({{{ Π ^_ ^_ }}} = {{{ Type@_ }}}) by mauto 3; congruence.
-    + right; left.
-      assert {{ Γ ⊢ Π ^_ ^_ ≈ Type@_ : Type@_ }} by mauto 3.
-      assert ({{{ Π ^_ ^_ }}} = {{{ Type@_ }}}) by mauto 3; congruence.
-    + right; right.
-      match goal with
+      assert ({{{ Π ^_ ^_ }}} = {{{ Type@_ }}}) by mauto 3...
+    + match goal with
       | _: {{ Γ ⊢ M' ≈ Π ^?A1 ^?A2 : Type@_ }},
           _: {{ Γ ⊢ Π ^?B1 ^?B2 ≈ M' : Type@_ }} |- _ =>
           assert {{ Γ ⊢ Π A1 A2 ≈ Π B1 B2 : Type@_ }} by mauto 3;
           assert ({{ Γ ⊢ A1 ≈ B1 : Type@_ }} /\ {{ Γ, A1 ⊢ A2 ≈ B2 : Type@_ }}) as [] by mauto 3 using exp_eq_pi_inversion
       end.
+      assert {{ ⊢ Γ ≈ Γ }} by mauto 3.
+      right; right.
       do 4 eexists; repeat split; mauto 3.
-      * eexists; mauto 4.
-      * etransitivity; mauto 3.
-        etransitivity; eapply ctxeq_subtyp; mauto 3; eapply wf_ctx_eq_extend'; mauto 3.
+      * eexists; eapply exp_eq_trans_typ_max...
+      * etransitivity; [| eassumption].
+        etransitivity; eapply ctxeq_subtyp...
   - right; left.
-    do 2 eexists; repeat split; mauto 4; lia.
+    do 2 eexists...
   - right; right.
-    do 4 eexists; repeat split; mauto 4.
+    do 4 eexists...
 Qed.
 
 #[export]
 Hint Resolve subtyp_spec : mcltt.
 
-Lemma consistency_ne_helper : forall {i T T'} {W : ne},
-    is_typ_constr T' ->
-    (forall j, T' <> {{{ Type@j }}}) ->
-    {{ ⋅, Type@i ⊢ T ⊆ T' }} ->
-    ~ {{ ⋅, Type@i ⊢ W : T }}.
-Proof.
-  intros * HT' HT'eq Heq HW. gen T'.
-  dependent induction HW; intros; mauto 3; try directed dependent destruction HT';
+Lemma consistency_ne_helper : forall {i A A'} {W : ne},
+    is_typ_constr A' ->
+    (forall j, A' <> {{{ Type@j }}}) ->
+    {{ ⋅, Type@i ⊢ A ⊆ A' }} ->
+    ~ {{ ⋅, Type@i ⊢ W : A }}.
+Proof with (congruence + mautosolve 3).
+  intros * HA' HA'eq Heq HW. gen A'.
+  dependent induction HW; intros; mauto 3; try directed dependent destruction HA';
     try (destruct W; simpl in *; congruence).
   - destruct W; simpl in *; autoinjections.
-    eapply IHHW4; [| | | | mauto 4]; mauto 3; congruence.
+    eapply IHHW4; [| | | | mauto 4]...
   - destruct W; simpl in *; autoinjections.
-    eapply IHHW3; [| | | | mauto 4]; mauto 3; congruence.
+    eapply IHHW3; [| | | | mauto 4]...
   - destruct W; simpl in *; autoinjections.
     do 2 match_by_head ctx_lookup ltac:(fun H => dependent destruction H).
     assert {{ ⋅, Type@i ⊢ Type@i[Wk] ≈ Type@i : Type@(S i) }} by mauto 3.
     eapply subtyp_spec in Heq as [| []]; destruct_conjs;
-      try (eapply HT'eq; mautosolve 4).
+      try (eapply HA'eq; mautosolve 4).
     assert {{ ⋅, Type@i ⊢ Type@i ≈ Π ^_ ^_ : Type@_ }} by mauto 3.
-    assert ({{{ Π ^_ ^_ }}} = {{{ Type@i }}}) by mauto 3.
-    congruence.
+    assert ({{{ Π ^_ ^_ }}} = {{{ Type@i }}}) by mauto 3...
 Qed.
 
 Theorem consistency : forall {i} M,
     ~ {{ ⋅ ⊢ M : Π Type@i #0 }}.
-Proof.
+Proof with (congruence + mautosolve 3).
   intros * HW.
-  assert (exists W1 W2, nbe {{{ ⋅ }}} M {{{ Π Type@i #0 }}} n{{{ λ W1 W2 }}}) as [? [? Hnbe]] by mauto 3.
+  assert (exists W1 W2, nbe {{{ ⋅ }}} M {{{ Π Type@i #0 }}} n{{{ λ W1 W2 }}}) as [W1 [W2 Hnbe]] by mauto 3.
   assert (exists W, nbe {{{ ⋅ }}} M {{{ Π Type@i #0 }}} W /\ {{ ⋅ ⊢ M ≈ W : Π Type@i #0 }}) as [? []] by mauto 3 using soundness.
   gen_presups.
   functional_nbe_rewrite_clear.
@@ -188,16 +203,14 @@ Proof.
   invert_rel_typ_body.
   match_by_head read_nf ltac:(fun H => directed dependent destruction H).
   simpl in *.
-  assert (exists B, {{ ⋅, Type@i ⊢ M0 : B }} /\ {{ ⋅ ⊢ Π Type@i B ⊆ Π Type@i #0 }}) as [? [? [| []]%subtyp_spec]] by mauto 3;
+  assert (exists B, {{ ⋅, Type@i ⊢ M0 : B }} /\ {{ ⋅ ⊢ Π Type@i B ⊆ Π Type@i #0 }}) as [B [? [| [|]]%subtyp_spec]] by mauto 3;
     destruct_conjs;
     try assert ({{{ Π ^_ ^_ }}} = {{{ Type@_ }}}) by mauto 3;
     try congruence.
-  - assert (_ /\ {{ ⋅, Type@i ⊢ ^_ ≈ #0 : ^_ }}) as [_ ?] by mauto 3 using exp_eq_pi_inversion.
-    eapply consistency_ne_helper; mauto 3.
-    congruence.
-  - assert (_ /\ {{ ^_ ⊢ x ≈ ^_ : ^_ }}) as [_ ?] by mauto 3 using exp_eq_pi_inversion.
+  - assert (_ /\ {{ ^_ ⊢ B ≈ #0 : ^_ }}) as [_ ?] by mauto 3 using exp_eq_pi_inversion.
+    eapply consistency_ne_helper...
+  - assert (_ /\ {{ ^_ ⊢ B ≈ ^_ : ^_ }}) as [_ ?] by mauto 3 using exp_eq_pi_inversion.
     assert (_ /\ {{ ^_ ⊢ ^_ ≈ #0 : ^_ }}) as [? ?] by mauto 3 using exp_eq_pi_inversion.
-    assert {{ ⋅, Type@i ⊢ x ⊆ #0 }} by (etransitivity; [| eapply ctxeq_subtyp]; mauto 4).
-    eapply consistency_ne_helper; mauto 3.
-    congruence.
+    assert {{ ^_ ⊢ B ⊆ #0 }} by (etransitivity; [| eapply ctxeq_subtyp]; mauto 4).
+    eapply consistency_ne_helper...
 Qed.