Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Port consistency #237

Merged
merged 3 commits into from
Oct 2, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
53 changes: 48 additions & 5 deletions theories/Core/Completeness/Consequences/Types.v
Original file line number Diff line number Diff line change
Expand Up @@ -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},
Expand All @@ -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 ->
Expand All @@ -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.

Expand All @@ -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]
Expand Down
152 changes: 141 additions & 11 deletions theories/Core/Semantic/Consequences.v
Original file line number Diff line number Diff line change
Expand Up @@ -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 }} ->
Expand Down Expand Up @@ -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},
Expand All @@ -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.
18 changes: 18 additions & 0 deletions theories/Core/Semantic/NbE.v
Original file line number Diff line number Diff line change
@@ -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.
Expand Down Expand Up @@ -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
Expand Down
22 changes: 22 additions & 0 deletions theories/Core/Syntactic/System/Lemmas.v
Original file line number Diff line number Diff line change
Expand Up @@ -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...
Expand Down Expand Up @@ -1278,3 +1287,16 @@ Lemma presup_exp : forall {Γ M A},
Proof.
mauto 4 using presup_exp_typ.
Qed.

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.