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.

Sign up for GitHub

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

Streamline some syntactic proofs #55

Merged
merged 1 commit into from
May 6, 2024
+38 −47
Merged

Streamline some syntactic proofs #55

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
2 changes: 2 additions & 0 deletions theories/Core/Syntactic/Presup.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
From Mcltt Require Import Base CtxEquiv LibTactics Relations Syntax System SystemLemmas.

#[local]
Ltac gen_presup_ctx H :=
match type of H with
| {{ ⊢ ~?Γ ≈ ~?Δ }} =>
Expand All @@ -13,6 +14,7 @@ Ltac gen_presup_ctx H :=
| _ => idtac
end.

#[local]
Ltac gen_presup_IH presup_exp presup_exp_eq presup_sub_eq H :=
match type of H with
| {{ ~?Γ ⊢ ~?M : ~?A }} =>
Expand Down
22 changes: 11 additions & 11 deletions theories/Core/Syntactic/Relations.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,27 +1,27 @@
From Coq Require Import Setoid.

From Mcltt Require Import Base CtxEquiv LibTactics Syntax System SystemLemmas.

Lemma ctx_eq_refl : forall {Γ}, {{ ⊢ Γ }} -> {{ ⊢ Γ ≈ Γ }}.
Proof with mauto.
intros * HΓ.
induction HΓ...
Proof with solve [mauto].
induction 1...
Qed.

#[export]
Hint Resolve ctx_eq_refl : mcltt.

Lemma ctx_eq_trans : forall {Γ0 Γ1 Γ2}, {{ ⊢ Γ0 ≈ Γ1 }} -> {{ ⊢ Γ1 ≈ Γ2 }} -> {{ ⊢ Γ0 ≈ Γ2 }}.
Proof with mauto.
Proof with solve [mauto].
intros * HΓ01 HΓ12.
gen Γ2.
induction HΓ01 as [|? ? ? i01 * HΓ01 IHΓ01 HΓ0T0 _ HΓ0T01 _]; intros...
induction HΓ01 as [|Γ0 ? T0 i01 T1]; intros; mauto.
rename HΓ12 into HT1Γ12.
inversion_clear HT1Γ12 as [|? ? ? i12 * HΓ12' _ HΓ2'T2 _ HΓ2'T12].
pose proof (lift_exp_max_left i12 HΓ0T0).
pose proof (lift_exp_max_right i01 HΓ2'T2).
pose proof (lift_exp_eq_max_left i12 HΓ0T01).
pose proof (lift_exp_eq_max_right i01 HΓ2'T12).
inversion_clear HT1Γ12 as [|? Γ2' ? i12 T2].
clear Γ2; rename Γ2' into Γ2.
set (i := max i01 i12).
assert {{ Γ0 ⊢ T0 : Type@i }} by mauto using lift_exp_max_left.
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.
econstructor...
Qed.

Expand Down
61 changes: 25 additions & 36 deletions theories/Core/Syntactic/SystemLemmas.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,22 +2,21 @@ From Mcltt Require Import Base LibTactics System Syntax.

Lemma ctx_decomp : forall {Γ A}, {{ ⊢ Γ , A }} -> {{ ⊢ Γ }} /\ exists i, {{ Γ ⊢ A : Type@i }}.
Proof with solve [mauto].
intros * HAΓ.
inversion HAΓ; subst...
inversion 1; subst...
Qed.

#[export]
Hint Resolve ctx_decomp : mcltt.

Lemma ctx_decomp_left : forall {Γ A}, {{ ⊢ Γ , A }} -> {{ ⊢ Γ }}.
Proof with solve [eauto].
intros * HAΓ.
intros.
eapply proj1, ctx_decomp...
Qed.

Lemma ctx_decomp_right : forall {Γ A}, {{ ⊢ Γ , A }} -> exists i, {{ Γ ⊢ A : Type@i }}.
Proof with solve [eauto].
intros * HAΓ.
intros.
eapply proj2, ctx_decomp...
Qed.

Expand All @@ -26,8 +25,7 @@ Hint Resolve ctx_decomp_left ctx_decomp_right : mcltt.

Lemma lift_exp_ge : forall {Γ A n m}, n <= m -> {{ Γ ⊢ A : Type@n }} -> {{ Γ ⊢ A : Type@m }}.
Proof with solve [mauto].
intros * Hnm HA.
induction Hnm...
induction 1...
Qed.

#[export]
Expand All @@ -47,8 +45,7 @@ Qed.

Lemma lift_exp_eq_ge : forall {Γ A A' n m}, n <= m -> {{ Γ ⊢ A ≈ A': Type@n }} -> {{ Γ ⊢ A ≈ A' : Type@m }}.
Proof with solve [mauto].
intros * Hnm HAA'.
induction Hnm; subst...
induction 1; subst...
Qed.

#[export]
Expand All @@ -68,19 +65,18 @@ Qed.

Lemma presup_ctx_eq : forall {Γ Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ ⊢ Γ }} /\ {{ ⊢ Δ }}.
Proof with solve [mauto].
intros * HΓΔ.
induction HΓΔ as [|* ? []]...
induction 1 as [|* ? []]...
Qed.

Lemma presup_ctx_eq_left : forall {Γ Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ ⊢ Γ }}.
Proof with solve [eauto].
intros * HΓΔ.
intros.
eapply proj1, presup_ctx_eq...
Qed.

Lemma presup_ctx_eq_right : forall {Γ Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ ⊢ Δ }}.
Proof with solve [eauto].
intros * HΓΔ.
intros.
eapply proj2, presup_ctx_eq...
Qed.

Expand All @@ -89,19 +85,18 @@ Hint Resolve presup_ctx_eq presup_ctx_eq_left presup_ctx_eq_right : mcltt.

Lemma presup_sub_ctx : forall {Γ Δ σ}, {{ Γ ⊢s σ : Δ }} -> {{ ⊢ Γ }} /\ {{ ⊢ Δ }}.
Proof with solve [mauto].
intros * Hσ.
induction Hσ; repeat destruct_one_pair...
induction 1; repeat destruct_one_pair...
Qed.

Lemma presup_sub_ctx_left : forall {Γ Δ σ}, {{ Γ ⊢s σ : Δ }} -> {{ ⊢ Γ }}.
Proof with solve [eauto].
intros * Hσ.
intros.
eapply proj1, presup_sub_ctx...
Qed.

Lemma presup_sub_ctx_right : forall {Γ Δ σ}, {{ Γ ⊢s σ : Δ }} -> {{ ⊢ Δ }}.
Proof with solve [eauto].
intros * Hσ.
intros.
eapply proj2, presup_sub_ctx...
Qed.

Expand All @@ -110,28 +105,26 @@ Hint Resolve presup_sub_ctx presup_sub_ctx_left presup_sub_ctx_right : mcltt.

Lemma presup_exp_ctx : forall {Γ M A}, {{ Γ ⊢ M : A }} -> {{ ⊢ Γ }}.
Proof with solve [mauto].
intros * HM.
induction HM...
induction 1...
Qed.

#[export]
Hint Resolve presup_exp_ctx : mcltt.

Lemma presup_sub_eq_ctx : forall {Γ Δ σ σ'}, {{ Γ ⊢s σ ≈ σ' : Δ }} -> {{ ⊢ Γ }} /\ {{ ⊢ Δ }}.
Proof with solve [mauto].
intros * Hσσ'.
induction Hσσ'; repeat destruct_one_pair...
induction 1; repeat destruct_one_pair...
Qed.

Lemma presup_sub_eq_ctx_left : forall {Γ Δ σ σ'}, {{ Γ ⊢s σ ≈ σ' : Δ }} -> {{ ⊢ Γ }}.
Proof with solve [eauto].
intros * Hσσ'.
intros.
eapply proj1, presup_sub_eq_ctx...
Qed.

Lemma presup_sub_eq_ctx_right : forall {Γ Δ σ σ'}, {{ Γ ⊢s σ ≈ σ' : Δ }} -> {{ ⊢ Δ }}.
Proof with solve [eauto].
intros * Hσσ'.
intros.
eapply proj2, presup_sub_eq_ctx...
Qed.

Expand All @@ -140,8 +133,7 @@ Hint Resolve presup_sub_eq_ctx presup_sub_eq_ctx_left presup_sub_eq_ctx_right :

Lemma presup_exp_eq_ctx : forall {Γ M M' A}, {{ Γ ⊢ M ≈ M' : A }} -> {{ ⊢ Γ }}.
Proof with solve [mauto].
intros * HMM'.
induction HMM'...
induction 1...
Unshelve.
all: constructor.
Qed.
Expand All @@ -167,8 +159,7 @@ Hint Resolve sub_eq_refl : mcltt.

Lemma ctx_eq_sym : forall {Γ Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ ⊢ Δ ≈ Γ }}.
Proof with solve [mauto].
intros * HΓΔ.
induction HΓΔ...
induction 1...
Qed.

#[export]
Expand Down Expand Up @@ -240,8 +231,7 @@ Qed.

Lemma exp_eq_var_1_sub_typ : forall {Γ σ Δ A i M j}, {{ Γ ⊢s σ : Δ }} -> {{ Δ ⊢ A : Type@i }} -> {{ Γ ⊢ M : A[σ] }} -> {{ #0 : Type@j[Wk] ∈ Δ }} -> {{ Γ ⊢ #1[σ ,, M] ≈ #0[σ] : Type@j }}.
Proof with solve [mauto].
intros * ? ? ? Hvar0.
inversion Hvar0 as [? Δ'|]; subst.
inversion 4 as [? Δ'|]; subst.
assert {{ ⊢ Δ' }} by mauto.
eapply wf_exp_eq_conv...
Qed.
Expand All @@ -251,9 +241,9 @@ Hint Resolve exp_eq_var_0_sub_typ exp_eq_var_1_sub_typ : mcltt.

Lemma exp_eq_var_0_weaken_typ : forall {Γ A i}, {{ ⊢ Γ , A }} -> {{ #0 : Type@i[Wk] ∈ Γ }} -> {{ Γ , A ⊢ #0[Wk] ≈ #1 : Type@i }}.
Proof with solve [mauto].
intros * ? Hvar0.
intros * ?.
assert {{ ⊢ Γ }} by mauto.
inversion Hvar0 as [? Γ'|]; subst.
inversion 1 as [? Γ'|]; subst.
assert {{ ⊢ Γ' }} by mauto.
eapply wf_exp_eq_conv; only 1: solve [mauto].
eapply exp_eq_typ_sub_sub; [|solve [mauto]]...
Expand Down Expand Up @@ -394,8 +384,7 @@ Qed.

Lemma exp_eq_var_1_sub_nat : forall {Γ σ Δ A i M}, {{ Γ ⊢s σ : Δ }} -> {{ Δ ⊢ A : Type@i }} -> {{ Γ ⊢ M : A[σ] }} -> {{ #0 : ℕ[Wk] ∈ Δ }} -> {{ Γ ⊢ #1[σ ,, M] ≈ #0[σ] : ℕ }}.
Proof with solve [mauto].
intros * ? ? ? Hvar0.
inversion Hvar0 as [? Δ'|]; subst.
inversion 4 as [? Δ'|]; subst.
assert {{ ⊢ Δ' }} by mauto.
assert {{ Γ ⊢ #1[σ,, M] ≈ #0[σ] : ℕ[Wk][σ] }}...
Unshelve.
Expand All @@ -407,9 +396,9 @@ Hint Resolve exp_eq_var_0_sub_nat exp_eq_var_1_sub_nat : mcltt.

Lemma exp_eq_var_0_weaken_nat : forall {Γ A}, {{ ⊢ Γ , A }} -> {{ #0 : ℕ[Wk] ∈ Γ }} -> {{ Γ , A ⊢ #0[Wk] ≈ #1 : ℕ }}.
Proof with solve [mauto].
intros * ? Hvar0.
intros * ?.
assert {{ ⊢ Γ }} by mauto.
inversion Hvar0 as [? Γ'|]; subst.
inversion 1 as [? Γ'|]; subst.
assert {{ ⊢ Γ' }} by mauto.
assert {{ Γ', ℕ, A ⊢ #0[Wk] ≈ # 1 : ℕ[Wk][Wk] }}...
Unshelve.
Expand Down Expand Up @@ -485,8 +474,8 @@ Hint Resolve exp_eq_sub_sub_compose_cong : mcltt.

Lemma ctx_lookup_wf : forall {Γ A x}, {{ ⊢ Γ }} -> {{ #x : A ∈ Γ }} -> exists i, {{ Γ ⊢ A : Type@i }}.
Proof with solve [mauto].
intros * HΓ Hx.
induction Hx; inversion_clear HΓ; [|assert (exists i, {{ Γ ⊢ A : Type@i }}) as [] by eauto]...
intros * HΓ.
induction 1; inversion_clear HΓ; [|assert (exists i, {{ Γ ⊢ A : Type@i }}) as [] by eauto]...
Qed.

#[export]
Expand Down
Loading