Skip to content

Optimize GL syntax proof elaboration without changing declarations #620

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

Merged
Vilin97 merged 1 commit into from
Oct 10, 2026
Merged

Optimize GL syntax proof elaboration without changing declarations #620

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
44 changes: 27 additions & 17 deletions LeanPool/Lean4GlCoalgebras/Logic/Syntax.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ module
public import Mathlib.Data.Finset.Max
public import Mathlib.Algebra.BigOperators.Group.Finset.Defs
public import Mathlib.Data.Finset.Union
public meta import Mathlib.Tactic.Basic
public meta import Mathlib.Tactic.Basic -- shake: keep
public meta import Mathlib.Tactic.ToAdditive
import Mathlib.Algebra.Order.BigOperators.Group.Finset
import Mathlib.CategoryTheory.Category.Init
Expand Down Expand Up @@ -335,11 +335,13 @@ def FL : SplitFormula → SplitSequent

lemma FL_SplitFormula_left_eq_FL_Formula_map (φ : Formula) :
FL (Sum.inl φ) = φ.FL.map ⟨Sum.inl, Sum.inl_injective⟩ := by
induction φ <;> simp_all [FL, Formula.FL, Finset.map_union]
induction φ <;>
simp only [FL, Formula.FL, Finset.map_union, Finset.map_singleton, *] <;> rfl

lemma FL_SplitFormula_right_eq_FL_Formula_map (φ : Formula) :
FL (Sum.inr φ) = φ.FL.map ⟨Sum.inr, Sum.inr_injective⟩ := by
induction φ <;> simp_all [FL, Formula.FL, Finset.map_union]
induction φ <;>
simp only [FL, Formula.FL, Finset.map_union, Finset.map_singleton, *] <;> rfl

lemma in_FL_SplitFormula_left {φ : Formula} {ψ : SplitFormula}
(ψ_sub_φ : ψ ∈ FL (Sum.inl φ)) : ψ.isLeft := by
Expand Down Expand Up @@ -481,7 +483,9 @@ def single (n : Nat) (ψ : Formula) : Formula → Formula

/- Single substitution preserves negation. -/
lemma single_neg (n : Nat) (φ ψ : Formula) : single n ψ (~φ) = (~ (single n ψ φ)) := by
induction φ <;> simp [Formula.neg, single] <;> aesop
induction φ <;>
simp only [single, Formula.neg, apply_ite, Formula.neg_neg_eq, *] <;>
split <;> simp_all only

/- Single substitution preserves implication. -/
lemma single_imp (n : Nat) (C D E : Formula) :
Expand Down Expand Up @@ -561,7 +565,17 @@ lemma in_single_voc (m n : Nat) (φ ψ : Formula) :
lemma not_in_single_voc (n : Nat) (φ ψ : Formula) :
n ∉ φ.vocab → (single n ψ φ) = φ := by
intro h
induction φ <;> simp_all [single, Formula.vocab] <;> aesop
induction φ with
| bottom | top => rfl
| atom k | negAtom k =>
have hk : (k == n) = false := beq_eq_false_iff_ne.mpr
(Ne.symm (Finset.notMem_singleton.mp h))
simp only [single, hk, Bool.false_eq_true, ite_false]
| and φ χ ihφ ihχ | or φ χ ihφ ihχ =>
have components := Finset.notMem_union.mp h
simp only [single, ihφ components.1, ihχ components.2]
| box φ ih | diamond φ ih =>
simp only [single, ih h]

lemma not_in_single_top_voc (n : ℕ) (φ : Formula) : n ∉ (single n ⊤ φ).vocab := by
apply in_single_voc n n ⊤ φ
Expand Down Expand Up @@ -596,17 +610,13 @@ lemma lt_and_le_imp_add_lt {a b c : ℕ} : b ≤ a → c < b → (a - b) + c < a
lemma Finset.sum_diff_singleton_lt {α : Type} [DecidableEq α] {A C : Finset α} {b : α} {f : α → Nat}
: b ∈ A → C.sum f < f b → Finset.sum ((A \ {b}) ∪ C) f < Finset.sum A f := by
intro b_in_A C_lt_B
have union_sum : ((A \ {b}) ∪ C).sum f + ((A \ {b}) ∩ C).sum f =
(A \ {b}).sum f + C.sum f := Finset.sum_union_inter
have remaining_sum : (A \ {b}).sum f + f b = A.sum f := by
simpa only [Finset.sum_singleton] using
(@Finset.sum_sdiff α Nat {b} A _ f _ (Finset.singleton_subset_iff.2 b_in_A))
calc
_ ≤ Finset.sum (A \ {b}) f + Finset.sum C f := by
simp [sub_add_left <| @Finset.sum_union_inter _ _ (A \ {b}) C _ f _]
_ = Finset.sum A f - Finset.sum {b} f + Finset.sum C f := by
have singleton_subset : {b} ⊆ A := Finset.singleton_subset_iff.2 b_in_A
simp [sub_add_left <| @Finset.sum_sdiff α Nat {b} A _ f _ singleton_subset]
_ < Finset.sum A f := by
apply lt_and_le_imp_add_lt
· exact
Finset.sum_le_sum_of_subset_of_nonneg
(Finset.singleton_subset_iff.2 b_in_A)
(by simp)
· exact C_lt_B
_ ≤ (A \ {b}).sum f + C.sum f := (Nat.le_add_right _ _).trans_eq union_sum
_ < (A \ {b}).sum f + f b := Nat.add_lt_add_left C_lt_B _
_ = A.sum f := remaining_sum
end Lean4GlCoalgebras
Loading