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

Refactoring and optimizing proofs #98

Merged
merged 5 commits into from
Jun 4, 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
7 changes: 0 additions & 7 deletions theories/Core/Semantic/PER/Lemmas.v
Original file line number Diff line number Diff line change
Expand Up @@ -4,13 +4,6 @@ From Mcltt Require Import Base LibTactics.
From Mcltt.Core Require Import Evaluation PER.Definitions PER.CoreTactics Readback.
Import Domain_Notations.

Add Parametric Morphism A : (@all A)
with signature forall_relation (fun (x : A) => iff) ==> iff as all_iff_moprhism'.
Proof.
unfold forall_relation.
split; intros ** ?; intuition.
Qed.

Add Parametric Morphism A : PER
with signature (@relation_equivalence A) ==> iff as PER_morphism.
Proof.
Expand Down
2 changes: 2 additions & 0 deletions theories/Core/Soundness/LogicalRelation/Definitions.v
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,9 @@ Global Open Scope predicate_scope.
Generalizable All Variables.

Notation "'typ_pred'" := (predicate (Tcons ctx (Tcons typ Tnil))).
Notation "'typ_pred_equivalence'" := (@predicate_equivalence (Tcons ctx (Tcons typ Tnil))).
Notation "'glu_pred'" := (predicate (Tcons ctx (Tcons exp (Tcons typ (Tcons domain Tnil))))).
Notation "'glu_pred_equivalence'" := (@predicate_equivalence (Tcons ctx (Tcons exp (Tcons typ (Tcons domain Tnil))))).

Definition univ_typ_pred j i : typ_pred := fun Γ T => {{ Γ ⊢ T ≈ Type@j : Type@i }}.
Arguments univ_typ_pred j i Γ T/.
Expand Down
60 changes: 18 additions & 42 deletions theories/Core/Soundness/LogicalRelation/Lemmas.v
Original file line number Diff line number Diff line change
@@ -1,43 +1,18 @@
From Coq Require Import Morphisms Morphisms_Relations.
From Mcltt Require Import Base LibTactics.
From Mcltt.Core Require Import System.Definitions Presup CtxEq Evaluation Readback PER.
From Mcltt.Core Require Import Evaluation PER Presup Readback Syntactic.Corollaries.

From Mcltt.Core.Soundness Require Import LogicalRelation.Definitions.
From Mcltt.Core.Soundness Require Export Weakening.Lemmas.
Import Domain_Notations.


Lemma glu_nat_per_nat : forall Γ m a,
glu_nat Γ m a ->
per_nat a a.
Proof.
induction 1; mauto.
Qed.

Lemma sub_id_typ : forall Γ M A,
{{ Γ ⊢ M : A }} ->
{{ Γ ⊢ M : A [ Id ] }}.
Proof.
intros. gen_presups. mauto 6.
Qed.

#[export]
Hint Resolve invert_id sub_id_typ : mcltt.

Lemma invert_sub_id : forall Γ M A,
{{ Γ ⊢ M [ Id ] : A }} ->
{{ Γ ⊢ M : A }}.
Proof.
intros. remember {{{ M [ Id ]}}} as M'.
gen M.
induction H; intros; try congruence;
gen_presups;
progressive_inversion;
mauto.
Qed.

#[export]
Hint Resolve invert_sub_id : mcltt.

Lemma glu_nat_escape : forall Γ m a,
glu_nat Γ m a ->
{{ ⊢ Γ }} ->
Expand All @@ -49,14 +24,14 @@ Proof.
end.
assert {{ Γ ⊢w Id : Γ }} by mauto.
specialize (H (length Γ)).
destruct_all.
destruct_conjs.
specialize (H0 _ _ _ H2 H3).
gen_presups.
mauto.
Qed.

#[export]
Hint Resolve glu_nat_escape : mcltt.
Hint Resolve glu_nat_escape : mcltt.

Lemma glu_nat_resp_equiv : forall Γ m a,
glu_nat Γ m a ->
Expand All @@ -67,21 +42,19 @@ Proof.
induction 1; intros; mauto.
econstructor; trivial.
intros.
specialize (H0 _ _ _ H2 H3).
mauto.
transitivity {{{ m[σ] }}}; mauto.
Qed.


Lemma glu_nat_per_top : forall Γ m a,
glu_nat Γ m a ->
per_top d{{{ ⇓ ℕ a }}} d{{{ ⇓ ℕ a }}}.
Proof.
induction 1; unfold per_top in *; intros; mauto.
induction 1; intros s; mauto.
- specialize (IHglu_nat s).
destruct_all.
destruct_conjs.
mauto.
- specialize (H s).
destruct_all.
destruct_conjs.
mauto.
Qed.

Expand All @@ -95,21 +68,24 @@ Proof.
induction 1; intros; progressive_inversion; gen_presups.
- transitivity {{{ zero [ σ ] }}}; mauto.
- specialize (IHglu_nat _ _ _ H1 H5).
transitivity {{{ (succ m') [ σ ]}}}; [mauto |].
transitivity {{{ succ m' [ σ ] }}}; mauto 6.
transitivity {{{ (succ m') [ σ ]}}}; mauto.
transitivity {{{ succ m' [ σ ] }}}; mauto.
- mauto.
Qed.


Lemma glu_univ_elem_univ_lvl : forall i P El A B,
glu_univ_elem i P El A B ->
forall Γ T,
P Γ T ->
{{ Γ ⊢ T : Type@i }}.
Proof with (simpl in *; destruct_all; gen_presups; trivial).
pose proof iff_impl_subrelation.
assert (Proper (typ_pred_equivalence ==> pointwise_relation ctx (pointwise_relation typ iff)) id)
by apply predicate_equivalence_pointwise.
induction 1 using glu_univ_elem_ind; intros.
- apply H1 in H3...
- apply H in H1...
- apply H4 in H6. progressive_invert H6...
- apply H0 in H2...
(* Use [apply_relation_equivalence]-like tactic later *)
- rewrite H3 in H5...
- rewrite H1 in H3...
- rewrite H6 in H8. dir_inversion_by_head pi_typ_pred...
- rewrite H2 in H4...
Qed.
39 changes: 14 additions & 25 deletions theories/Core/Soundness/Weakening/Lemmas.v
Original file line number Diff line number Diff line change
@@ -1,9 +1,9 @@
Require Import Coq.Program.Equality.
From Coq Require Import Program.Equality.

From Mcltt Require Import Base System.Definitions System.Lemmas Weakening.Definition Presup CtxEq LibTactics.
From Mcltt Require Import Base LibTactics.
From Mcltt.Core Require Import CtxEq Presup Syntactic.Corollaries System Weakening.Definition.
Import Syntax_Notations.


Lemma weakening_escape : forall Γ σ Δ,
{{ Γ ⊢w σ : Δ }} ->
{{ Γ ⊢s σ : Δ }}.
Expand All @@ -16,8 +16,7 @@ Proof.
Qed.

#[export]
Hint Resolve weakening_escape : mcltt.

Hint Resolve weakening_escape : mcltt.

Lemma weakening_resp_equiv : forall Γ σ σ' Δ,
{{ Γ ⊢w σ : Δ }} ->
Expand All @@ -27,7 +26,6 @@ Proof.
induction 1; mauto.
Qed.


Lemma ctxeq_weakening : forall Γ σ Δ,
{{ Γ ⊢w σ : Δ }} ->
forall Γ',
Expand All @@ -37,7 +35,6 @@ Proof.
induction 1; mauto.
Qed.


Lemma weakening_conv : forall Γ σ Δ,
{{ Γ ⊢w σ : Δ }} ->
forall Δ',
Expand All @@ -55,33 +52,24 @@ Proof.
Qed.

#[export]
Hint Resolve weakening_conv : mcltt.

Lemma invert_id : forall Γ Δ,
{{ Γ ⊢s Id : Δ }} ->
{{ ⊢ Γ ≈ Δ }}.
Proof.
intros. dependent induction H; intros; try congruence; mauto.
Qed.

Hint Resolve weakening_conv : mcltt.

Lemma weakening_compose : forall Γ' σ' Γ'',
{{ Γ' ⊢w σ' : Γ'' }} ->
forall Γ σ,
{{ Γ ⊢w σ : Γ' }} ->
{{ Γ ⊢w σ' ∘ σ : Γ'' }}.
Proof.
Proof with mautosolve.
induction 1; intros.
- gen_presup H.
apply invert_id in Hτ.
eapply weakening_resp_equiv; [ mauto | ].
transitivity {{{ Id ∘ σ0 }}}; mauto.
assert {{ ⊢ Γ ≈ Δ }} by mauto.
eapply weakening_resp_equiv; [mauto 2 |].
transitivity {{{ Id ∘ σ0 }}}...
- eapply wk_p; [eauto |].
apply weakening_escape in H.
transitivity {{{ Wk ∘ τ ∘ σ0 }}}; mauto.
transitivity {{{ Wk ∘ τ ∘ σ0 }}}; mauto 4.
eapply wf_sub_eq_compose_assoc; revgoals...
Qed.


Lemma weakening_id : forall Γ,
{{ ⊢ Γ }} ->
{{ Γ ⊢w Id : Γ }}.
Expand All @@ -93,8 +81,9 @@ Lemma weakening_wk : forall Γ T,
{{ ⊢ Γ , T }} ->
{{ Γ , T ⊢w Wk : Γ }}.
Proof.
intros. eapply wk_p; mauto.
intros.
econstructor; mautosolve.
Qed.

#[export]
Hint Resolve weakening_id weakening_wk : mcltt.
Hint Resolve weakening_id weakening_wk : mcltt.
37 changes: 37 additions & 0 deletions theories/Core/Syntactic/Corollaries.v
Original file line number Diff line number Diff line change
@@ -0,0 +1,37 @@
From Mcltt Require Import Base LibTactics.
From Mcltt.Core Require Import CtxEq Presup.
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 ] }}.
Proof.
intros.
gen_presups.
mauto 6.
Qed.

#[export]
Hint Resolve sub_id_typ : mcltt.

Corollary invert_sub_id : forall Γ M A,
{{ Γ ⊢ M [ Id ] : A }} ->
{{ Γ ⊢ M : A }}.
Proof.
intros * H.
dependent induction H; mauto.
Qed.

#[export]
Hint Resolve invert_sub_id : mcltt.
14 changes: 9 additions & 5 deletions theories/Core/Syntactic/CtxEq.v
Original file line number Diff line number Diff line change
Expand Up @@ -40,24 +40,26 @@ Module ctxeq_judg.
all: inversion_clear 1;
(on_all_hyp: gen_ctxeq_helper_IH ctxeq_exp_helper ctxeq_exp_eq_helper ctxeq_sub_helper ctxeq_sub_eq_helper);
clear ctxeq_exp_helper ctxeq_exp_eq_helper ctxeq_sub_helper ctxeq_sub_eq_helper;
intros * HΓΔ; destruct (presup_ctx_eq HΓΔ); mauto;
intros * HΓΔ; destruct (presup_ctx_eq HΓΔ); mauto 4;
try (rename B into C); try (rename B' into C'); try (rename A0 into B); try (rename A' into B').
(* ctxeq_exp_helper & ctxeq_exp_eq_helper recursion cases *)
1,6-8: assert {{ ⊢ Γ, ℕ ≈ Δ, ℕ }} by (econstructor; mautosolve);
assert {{ Δ, ℕ ⊢ B : Type@i }} by eauto; econstructor...
(* ctxeq_exp_helper & ctxeq_exp_eq_helper function cases *)
1-3,5-9: assert {{ Δ ⊢ B : Type@i }} by eauto; assert {{ ⊢ Γ, B ≈ Δ, B }} by mauto;
try econstructor; mautosolve.
try econstructor...
(* ctxeq_exp_helper & ctxeq_exp_eq_helper variable cases *)
1-2: assert (exists B i, {{ #x : B ∈ Δ }} /\ {{ Γ ⊢ A ≈ B : Type@i }} /\ {{ Δ ⊢ A ≈ B : Type@i }}); destruct_conjs...
1-2: assert (exists B i, {{ #x : B ∈ Δ }} /\ {{ Γ ⊢ A ≈ B : Type@i }} /\ {{ Δ ⊢ A ≈ B : Type@i }}); destruct_conjs; mautosolve 4.
(* ctxeq_sub_helper & ctxeq_sub_eq_helper weakening cases *)
2-3: inversion_clear HΓΔ; econstructor...
2-3: inversion_clear HΓΔ; econstructor; mautosolve 4.

(* ctxeq_exp_eq_helper variable case *)
inversion_clear HΓΔ as [|? Δ0 ? ? C'].
assert (exists D i', {{ #x : D ∈ Δ0 }} /\ {{ Γ0 ⊢ B ≈ D : Type@i' }} /\ {{ Δ0 ⊢ B ≈ D : Type@i' }}) as [D [i0 ?]] by mauto.
destruct_conjs.
assert {{ Δ0, C' ⊢ B[Wk] ≈ D[Wk] : Type @ i0 }}...
assert {{ ⊢ Δ0, C' }} by mauto.
assert {{ Δ0 ⊢ D ≈ B : Type@i0 }} by mauto.
assert {{ Δ0, C' ⊢ D[Wk] ≈ B[Wk] : Type@i0 }}...
Qed.

Corollary ctxeq_exp : forall {Γ Δ M A}, {{ ⊢ Γ ≈ Δ }} -> {{ Γ ⊢ M : A }} -> {{ Δ ⊢ M : A }}.
Expand Down Expand Up @@ -98,6 +100,8 @@ Proof with mautosolve.
assert {{ Γ2 ⊢ T2 : Type@i }} by mauto using lift_exp_max_right.
assert {{ Γ0 ⊢ T0 ≈ T1 : Type@i }} by mauto using lift_exp_eq_max_left.
assert {{ Γ2 ⊢ T1 ≈ T2 : Type@i }} by mauto using lift_exp_eq_max_right.
assert {{ ⊢ Γ0 ≈ Γ2 }} by mauto.
assert {{ Γ0 ⊢ T0 ≈ T2 : Type@i }} by mauto.
econstructor...
Qed.

Expand Down
Loading
Loading