Merge pull request #236 from Beluga-lang/pr-consistency

Prove more consequences

theories/Core/Completeness/Consequences/Types.v

@@ -3,6 +3,7 @@ From Mcltt Require Import LibTactics.
 From Mcltt.Core Require Import Base.
 From Mcltt.Core Require Export Completeness.
 From Mcltt.Core.Semantic Require Import Realizability.
+From Mcltt.Core.Syntactic Require Export CoreInversions.
 Import Domain_Notations.
 
 Lemma exp_eq_typ_implies_eq_level : forall {Γ i j k},
@@ -23,18 +24,57 @@ Proof with mautosolve.
   match_by_head1 per_univ_elem invert_per_univ_elem.
   reflexivity.
 Qed.
-
 #[export]
 Hint Resolve exp_eq_typ_implies_eq_level : mcltt.
 
 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 }}}
+| var_is_typ_constr : forall x, is_typ_constr {{{ #x }}}
 .
+#[export]
+Hint Constructors is_typ_constr : mcltt.  
 
+Theorem is_typ_constr_and_exp_eq_var_implies_eq_var : forall Γ A x i,
+    is_typ_constr A ->
+    {{ Γ ⊢ A ≈ #x : Type@i }} ->
+    A = {{{ #x }}}.
+Proof.
+  intros * Histyp ?.
+  assert {{ Γ ⊨ A ≈ #x : Type@i }} 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.
+  gen_presups.
+  assert (exists A, {{ #x : A ∈ Γ }} /\ {{ Γ ⊢ A ⊆ Type@i }}) as [? [? _]] by mauto 2.
+  assert (exists a, ρ x = d{{{ ⇑! a (length Γ - x - 1) }}}) as [? Heq] by mauto 2.
+  destruct Histyp;
+    invert_rel_typ_body;
+    destruct_conjs;
+    rewrite Heq in *;
+    match_by_head1 per_univ_elem invert_per_univ_elem.
+  rename x1 into a0.
+  rename x2 into x1.
+  assert (exists A, {{ #x1 : A ∈ Γ }} /\ {{ Γ ⊢ A ⊆ Type@i }}) as [? [? _]] by mauto 2.
+  assert (exists a, ρ x1 = d{{{ ⇑! a (length Γ - x1 - 1) }}}) as [a1] by mauto 2.
+  assert (x0 < length Γ) by mauto 2.
+  assert (x1 < length Γ) by mauto 2.
+  f_equal.
+  enough (length Γ - x0 - 1 = length Γ - x1 - 1) by lia.
+  replace (ρ x1) with d{{{ ⇑! a1 (length Γ - x1 - 1) }}} in * by intuition.
+  autoinjections.
+  match_by_head1 per_bot ltac:(fun H => destruct (H (length Γ)) as [? []]).
+  match_by_head read_ne ltac:(fun H => directed dependent destruction H).
+  lia.
+Qed.
 #[export]
-Hint Constructors is_typ_constr : mcltt.
+Hint Resolve is_typ_constr_and_exp_eq_var_implies_eq_var : mcltt.
 
 Theorem is_typ_constr_and_exp_eq_typ_implies_eq_typ : forall Γ A i j,
     is_typ_constr A ->
@@ -55,9 +95,10 @@ Proof.
     invert_rel_typ_body;
     destruct_conjs;
     match_by_head1 per_univ_elem invert_per_univ_elem.
-  reflexivity.
+  - reflexivity.
+  - replace {{{ #x0 }}} with {{{ Type@i }}} by mauto 3 using is_typ_constr_and_exp_eq_var_implies_eq_var.
+    reflexivity.
 Qed.
-
 #[export]
 Hint Resolve is_typ_constr_and_exp_eq_typ_implies_eq_typ : mcltt.
 
@@ -80,7 +121,9 @@ Proof.
     invert_rel_typ_body;
     destruct_conjs;
     match_by_head1 per_univ_elem invert_per_univ_elem.
-  reflexivity.
+  - reflexivity.
+  - replace {{{ #x0 }}} with {{{ ℕ }}} by mauto 3 using is_typ_constr_and_exp_eq_var_implies_eq_var.
+    reflexivity.
 Qed.
 
 #[export]

theories/Core/Semantic/Consequences.v

@@ -4,6 +4,20 @@ From Mcltt.Core Require Export Soundness.
 From Mcltt.Core.Completeness.Consequences Require Export Types.
 Import Domain_Notations.
 
+Lemma idempotent_nbe_ty : forall {Γ i A B C},
+    {{ Γ ⊢ A : Type@i }} ->
+    nbe_ty Γ A B ->
+    nbe_ty Γ B C ->
+    B = C.
+Proof.
+  intros.
+  assert {{ Γ ⊢ A ≈ B : Type@i }} as [? []]%completeness_ty by mauto 2 using soundness_ty'.
+  functional_nbe_rewrite_clear.
+  reflexivity.
+Qed.
+#[export]
+Hint Resolve idempotent_nbe_ty : mcltt.
+
 Lemma adjust_exp_eq_level : forall {Γ A A' i j},
     {{ Γ ⊢ A ≈ A' : Type@i }} ->
     {{ Γ ⊢ A : Type@j }} ->
@@ -42,7 +56,8 @@ Proof.
   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.
-  split; mauto.
+  split; [mauto 3 |].
+  etransitivity; mauto 4.
 Qed.
 
 Lemma nf_of_pi : forall {Γ M A B},
@@ -56,18 +71,133 @@ Proof.
   match_by_head1 read_nf ltac:(fun H => inversion_clear H).
   do 2 eexists; mauto.
 Qed.
+#[export]
+Hint Resolve nf_of_pi : mcltt.
 
-Lemma idempotent_nbe_ty : forall {Γ i A B C},
-    {{ Γ ⊢ A : Type@i }} ->
-    nbe_ty Γ A B ->
-    nbe_ty Γ B C ->
-    B = C.
+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.
+#[export]
+Hint Resolve canonical_form_of_pi : mcltt.
+
+Inductive canonical_nat : nf -> Prop :=
+| canonical_nat_zero : canonical_nat n{{{ zero }}}
+| canonical_nat_succ : forall W, canonical_nat W -> canonical_nat n{{{ succ W }}}
+.
+#[export]
+Hint Constructors canonical_nat : mcltt.
+
+Theorem canonical_form_of_nat : forall {M},
+    {{ ⋅ ⊢ M : ℕ }} ->
+    exists W, nbe {{{ ⋅ }}} M {{{ ℕ }}} W /\ canonical_nat W.
+Proof with mautosolve 4.
+  intros * [? []]%soundness.
+  eexists; split; [eassumption |].
+  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...
+Qed.
+#[export]
+Hint Resolve canonical_form_of_nat : 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.
-  intros.
-  assert {{ Γ ⊢ A ≈ B : Type@i }} as [? []]%completeness_ty by mauto 2 using soundness_ty'.
-  functional_nbe_rewrite_clear.
-  reflexivity.
+  induction 1; mauto 3.
+  - destruct_all; firstorder (mauto 3);
+      try (right; right; do 4 eexists; repeat split; mautosolve 3).
+    + right; left.
+      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.
+    + 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
+      | _: {{ Γ ⊢ 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.
+      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.
+  - right; left.
+    do 2 eexists; repeat split; mauto 4; lia.
+  - right; right.
+    do 4 eexists; repeat split; mauto 4.
 Qed.
 
 #[export]
-Hint Resolve idempotent_nbe_ty : mcltt.
+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';
+    try (destruct W; simpl in *; congruence).
+  - destruct W; simpl in *; autoinjections.
+    eapply IHHW4; [| | | | mauto 4]; mauto 3; congruence.
+  - destruct W; simpl in *; autoinjections.
+    eapply IHHW3; [| | | | mauto 4]; mauto 3; congruence.
+  - 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).
+    assert {{ ⋅, Type@i ⊢ Type@i ≈ Π ~_ ~_ : Type@_ }} by mauto 3.
+    assert ({{{ Π ~_ ~_ }}} = {{{ Type@i }}}) by mauto 3.
+    congruence.
+Qed.
+
+Theorem consistency : forall {i} M,
+    ~ {{ ⋅ ⊢ M : Π Type@i #0 }}.
+Proof.
+  intros * HW.
+  assert (exists W1 W2, nbe {{{ ⋅ }}} M {{{ Π Type@i #0 }}} n{{{ λ W1 W2 }}}) as [? [? 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.
+  dependent destruction Hnbe.
+  invert_rel_typ_body.
+  match_by_head read_nf ltac:(fun H => directed dependent destruction H).
+  match_by_head read_typ ltac:(fun H => directed dependent destruction H).
+  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;
+    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 (_ /\ {{ ~_ ⊢ ~_ ≈ #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.
+Qed.

theories/Core/Semantic/NbE.v

@@ -1,6 +1,7 @@
 From Mcltt Require Import LibTactics.
 From Mcltt.Core Require Import Base.
 From Mcltt.Core.Semantic Require Export Domain Evaluation Readback.
+From Mcltt.Core.Syntactic Require Export System.
 Import Domain_Notations.
 
 Generalizable All Variables.
@@ -30,6 +31,23 @@ Qed.
 #[export]
 Hint Resolve functional_initial_env : mcltt.
 
+(** In the following spec, we do not care (for now)
+    whether [a] is the evaluation result of A or not.
+    If we want to specify that as well, we need a generalized
+    version of [drop_env] that can drop [x] elements. *)
+Lemma initial_env_spec : forall x Γ ρ A,
+    initial_env Γ ρ ->
+    {{ #x : A ∈ Γ }} ->
+    exists a, ρ x = d{{{ ⇑! a (length Γ - x - 1) }}}.
+Proof.
+  induction x; intros * Hinit Hlookup;
+    dependent destruction Hlookup; dependent destruction Hinit; simpl; mauto 3.
+  eexists; repeat f_equal; lia.
+Qed.
+
+#[export]
+Hint Resolve initial_env_spec : mcltt.
+
 Ltac functional_initial_env_rewrite_clear1 :=
   let tactic_error o1 o2 := fail 3 "functional_initial_env equality between" o1 "and" o2 "cannot be solved by mauto" in
   match goal with

theories/Core/Syntactic/System/Lemmas.v

@@ -6,6 +6,15 @@ Import Syntax_Notations.
 (** ** Core Presuppositions *)
 
 (** *** Basic inversion *)
+Lemma ctx_lookup_lt : forall {Γ A x},
+    {{ #x : A ∈ Γ }} ->
+    x < length Γ.
+Proof.
+  induction 1; simpl; lia.
+Qed.
+#[export]
+Hint Resolve ctx_lookup_lt : mcltt.
+
 Lemma ctx_decomp : forall {Γ A}, {{ ⊢ Γ , A }} -> {{ ⊢ Γ }} /\ exists i, {{ Γ ⊢ A : Type@i }}.
 Proof with now eauto.
   inversion 1...
@@ -1135,3 +1144,16 @@ Qed.
 
 #[export]
 Hint Resolve ctx_sub_ctx_lookup : mcltt.
+
+Lemma no_closed_neutral : forall {A} {W : ne},
+    ~ {{ ⋅ ⊢ W : A }}.
+Proof.
+  intros * H.
+  dependent induction H; destruct W;
+    try (simpl in *; congruence);
+    autoinjections;
+    intuition.
+  inversion_by_head ctx_lookup.
+Qed.
+#[export]
+Hint Resolve no_closed_neutral : mcltt.