From 922419255d4e95251c32c234f274c06d7160f58c Mon Sep 17 00:00:00 2001 From: "Junyoung/\"Clare\" Jang" Date: Sat, 14 Sep 2024 20:10:13 -0400 Subject: [PATCH 1/3] Optimizing proofs (#201) --- theories/Core/Semantic/PER/CoreTactics.v | 3 +-- theories/Core/Semantic/PER/Lemmas.v | 4 ++-- theories/Core/Soundness/FunctionCases.v | 2 +- .../Soundness/LogicalRelation/CoreLemmas.v | 10 ++++----- .../Soundness/LogicalRelation/CoreTactics.v | 3 +-- .../Core/Soundness/LogicalRelation/Lemmas.v | 3 ++- theories/Core/Soundness/SubstitutionCases.v | 2 +- theories/LibTactics.v | 22 +++++++------------ 8 files changed, 21 insertions(+), 28 deletions(-) diff --git a/theories/Core/Semantic/PER/CoreTactics.v b/theories/Core/Semantic/PER/CoreTactics.v index 597b40c6..b61de31d 100644 --- a/theories/Core/Semantic/PER/CoreTactics.v +++ b/theories/Core/Semantic/PER/CoreTactics.v @@ -46,8 +46,7 @@ Ltac destruct_rel_typ := Ltac basic_invert_per_univ_elem H := progress simp per_univ_elem in H; - inversion H; - subst; + dependent destruction H; try rewrite <- per_univ_elem_equation_1 in *. Ltac basic_per_univ_elem_econstructor := diff --git a/theories/Core/Semantic/PER/Lemmas.v b/theories/Core/Semantic/PER/Lemmas.v index 826c36ea..f742ff19 100644 --- a/theories/Core/Semantic/PER/Lemmas.v +++ b/theories/Core/Semantic/PER/Lemmas.v @@ -446,10 +446,10 @@ Lemma per_univ_elem_trans : forall i R a1 a2, R m1 m2 -> R m2 m3 -> R m1 m3). -Proof with (basic_per_univ_elem_econstructor; mautosolve). +Proof with (basic_per_univ_elem_econstructor; mautosolve 4). induction 1 using per_univ_elem_ind; [> split; - [ intros * HT2; basic_invert_per_univ_elem HT2; clear HT2 + [ intros * HT2; basic_invert_per_univ_elem HT2 | intros * HTR1 HTR2; apply_relation_equivalence ] ..]; mauto. - (* univ case *) subst. diff --git a/theories/Core/Soundness/FunctionCases.v b/theories/Core/Soundness/FunctionCases.v index 8134cf2c..c0b463ce 100644 --- a/theories/Core/Soundness/FunctionCases.v +++ b/theories/Core/Soundness/FunctionCases.v @@ -364,7 +364,7 @@ Proof. assert {{ Γ ⊩ A : Type@(max i j) }} by mauto 3. assert {{ ⊩ Γ, A }} by mauto 2. assert (i <= max i j) by lia. - assert {{ Γ, A ⊢ Type@i ⊆ Type@(max i j) }} by mauto 3. + assert {{ Γ, A ⊢ Type@i ⊆ Type@(max i j) }} by mauto 4. assert {{ Γ, A ⊩ B : Type@(max i j) }} by mauto 3. mauto 2 using glu_rel_exp_app_helper. Qed. diff --git a/theories/Core/Soundness/LogicalRelation/CoreLemmas.v b/theories/Core/Soundness/LogicalRelation/CoreLemmas.v index 976d2247..515bdafa 100644 --- a/theories/Core/Soundness/LogicalRelation/CoreLemmas.v +++ b/theories/Core/Soundness/LogicalRelation/CoreLemmas.v @@ -59,7 +59,7 @@ Lemma glu_nat_resp_exp_eq : forall Γ M a, {{ Γ ⊢ M ≈ M' : ℕ }} -> glu_nat Γ M' a. Proof. - induction 1; intros; mauto. + induction 1; intros; mauto 4. econstructor; trivial. intros. transitivity {{{ M[σ] }}}; mauto. @@ -82,11 +82,11 @@ Lemma glu_nat_readback : forall Γ M a, {{ Δ ⊢ M[σ] ≈ M' : ℕ }}. Proof. induction 1; intros; progressive_inversion; gen_presups. - - transitivity {{{ zero[σ] }}}; mauto. - - assert {{ Δ ⊢ M'[σ] ≈ M0 : ℕ }} by mauto. + - transitivity {{{ zero[σ] }}}; mauto 4. + - assert {{ Δ ⊢ M'[σ] ≈ M0 : ℕ }} by mauto 4. transitivity {{{ (succ M')[σ] }}}; mauto 3. transitivity {{{ succ M'[σ] }}}; mauto 4. - - mauto. + - mauto 4. Qed. #[global] @@ -270,7 +270,7 @@ Lemma glu_univ_elem_per_elem : forall i P El a, Proof. simpl. induction 1 using glu_univ_elem_ind; intros; - try do 2 match_by_head1 per_univ_elem invert_per_univ_elem; + match_by_head per_univ_elem ltac:(fun H => directed invert_per_univ_elem H); simpl_glu_rel; try fold (per_univ j m m); mauto 4. diff --git a/theories/Core/Soundness/LogicalRelation/CoreTactics.v b/theories/Core/Soundness/LogicalRelation/CoreTactics.v index 2b85a547..34bd7691 100644 --- a/theories/Core/Soundness/LogicalRelation/CoreTactics.v +++ b/theories/Core/Soundness/LogicalRelation/CoreTactics.v @@ -5,8 +5,7 @@ From Mcltt.Core.Soundness Require Import LogicalRelation.Definitions. Ltac basic_invert_glu_univ_elem H := progress simp glu_univ_elem in H; - inversion H; - subst; + dependent destruction H; try rewrite <- glu_univ_elem_equation_1 in *. Ltac basic_glu_univ_elem_econstructor := diff --git a/theories/Core/Soundness/LogicalRelation/Lemmas.v b/theories/Core/Soundness/LogicalRelation/Lemmas.v index df1780b4..dd432266 100644 --- a/theories/Core/Soundness/LogicalRelation/Lemmas.v +++ b/theories/Core/Soundness/LogicalRelation/Lemmas.v @@ -405,6 +405,7 @@ Proof. assert {{ Γ ⊢ A'[Id] ≈ V : Type@i }} as -> by mauto 4. eapply wf_subtyp_refl'. mauto 4. + - bulky_rewrite. - bulky_rewrite. mauto 3. - destruct_by_head pi_glu_typ_pred. @@ -916,7 +917,7 @@ Qed. Ltac invert_glu_ctx_env H := (unshelve eapply (glu_ctx_env_cons_clean_inversion _) in H; shelve_unifiable; [eassumption |]; destruct H as [? [? []]]) - + (inversion H; subst). + + dependent destruction H. Lemma glu_ctx_env_subtyp_sub_if : forall Γ Γ' Sb Sb' Δ σ ρ, {{ ⊢ Γ ⊆ Γ' }} -> diff --git a/theories/Core/Soundness/SubstitutionCases.v b/theories/Core/Soundness/SubstitutionCases.v index 5fd963f7..8858e558 100644 --- a/theories/Core/Soundness/SubstitutionCases.v +++ b/theories/Core/Soundness/SubstitutionCases.v @@ -59,7 +59,7 @@ Proof. intros * [SbΓA]. match_by_head1 glu_ctx_env invert_glu_ctx_env. handle_functional_glu_ctx_env. - do 2 eexists; repeat split; mauto. + do 2 eexists; repeat split; [econstructor | |]; try reflexivity; mauto. intros. destruct_by_head cons_glu_sub_pred. econstructor; mauto. diff --git a/theories/LibTactics.v b/theories/LibTactics.v index af0b538d..4944dbf2 100644 --- a/theories/LibTactics.v +++ b/theories/LibTactics.v @@ -229,22 +229,16 @@ Tactic Notation "mautosolve" int_or_var(pow) := mautosolve_impl pow. (* Improve type class resolution *) #[export] - Hint Extern 1 => eassumption : typeclass_instances. - -Ltac predicate_resolve := - lazymatch goal with - | |- @Reflexive _ (@predicate_equivalence _) => - simple apply @Equivalence_Reflexive - | |- @Symmetric _ (@predicate_equivalence _) => - simple apply @Equivalence_Symmetric - | |- @Transitive _ (@predicate_equivalence _) => - simple apply @Equivalence_Transitive - | |- @Transitive _ (@predicate_implication _) => - simple apply @PreOrder_Transitive - end. +Hint Extern 1 => eassumption : typeclass_instances. #[export] -Hint Extern 1 => predicate_resolve : typeclass_instances. +Hint Extern 1 (@Reflexive _ (@predicate_equivalence _)) => simple apply @Equivalence_Reflexive : typeclass_instances. +#[export] +Hint Extern 1 (@Symmetric _ (@predicate_equivalence _)) => simple apply @Equivalence_Symmetric : typeclass_instances. +#[export] +Hint Extern 1 (@Transitive _ (@predicate_equivalence _)) => simple apply @Equivalence_Transitive : typeclass_instances. +#[export] +Hint Extern 1 (@Transitive _ (@predicate_implication _)) => simple apply @PreOrder_Transitive : typeclass_instances. (* intuition tactic default setting *) From c9df2e23ae3b838486623f51c87da1038623da36 Mon Sep 17 00:00:00 2001 From: Jason Hu Date: Sat, 14 Sep 2024 20:36:08 -0400 Subject: [PATCH 2/3] Update README.md (#203) --- README.md | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/README.md b/README.md index ff2f507d..931ff3e2 100644 --- a/README.md +++ b/README.md @@ -92,3 +92,10 @@ cd theories make ``` +## Branches + +The Github repo includes the following special branches: + +1. `main`: the main branch that is used to generate this homepage and Coqdoc; +2. `ext/*`: branches in this pattern are variations of `main` that implements various extensions. They are often used to implement extensions that require non-trivial workload and are aimed to be merged to `main` eventually; +3. `gh-pages`: the branch to host the homepage. From d0f658fedf46e92844a7e86a17160edd1aea5576 Mon Sep 17 00:00:00 2001 From: Jason Hu Date: Sat, 14 Sep 2024 20:38:20 -0400 Subject: [PATCH 3/3] Update ci_build.yaml (#204) --- .github/workflows/ci_build.yaml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.github/workflows/ci_build.yaml b/.github/workflows/ci_build.yaml index 27cefd0b..b53c0407 100644 --- a/.github/workflows/ci_build.yaml +++ b/.github/workflows/ci_build.yaml @@ -3,9 +3,11 @@ on: push: branches: - main + - ext/** pull_request: branches: - main + - ext/** workflow_dispatch: permissions: