From 3a7670d3520f3e452d656db09c61bc111aa335cf Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Thu, 23 Jan 2025 02:15:03 +0100 Subject: [PATCH] chore: golf `Definability` (#1060) --- equational_theories/Definability/Basic.lean | 43 ++++++++----------- equational_theories/Definability/Simple.lean | 27 +++--------- .../Definability/Tarski543.lean | 11 ++--- 3 files changed, 29 insertions(+), 52 deletions(-) diff --git a/equational_theories/Definability/Basic.lean b/equational_theories/Definability/Basic.lean index 62e13c218..4b3c7e379 100644 --- a/equational_theories/Definability/Basic.lean +++ b/equational_theories/Definability/Basic.lean @@ -209,9 +209,8 @@ theorem definable_of_structural (h : L'.StructuralFrom L) : L'.DefinableFrom L : /-- If law L' is term-definable from L, then L' is definable from L. -/ theorem definable_of_termDefinable (h : L'.TermDefinableFrom L) : L'.DefinableFrom L := by intro G M hGL - obtain ⟨M',h2,h3⟩ := h M hGL - use M', h2 - exact h3.Definable (inst := M.FOStructure) + obtain ⟨M', h2, h3⟩ := h M hGL + exact ⟨M', h2, h3.Definable (inst := M.FOStructure)⟩ end hierarchy @@ -229,15 +228,16 @@ theorem TermDefinable.trans_aux {G : Type} {M M₂ M₃ : Magma G} intro n f by_cases hn : n = 2 · subst hn - simp - eta_reduce - convert h₁ + simp only [realize_functions, Magma.FOStructure_funMap'] + exact h₁ by_cases hn₂ : n = 0 · subst hn₂ - simp [MagmaLanguage, Language.withConstants, Language.sum] at f + simp only [withConstants, Language.sum, MagmaLanguage, constantsOn_Functions, constantsOnFunc, + constantsOn_Relations, OfNat.zero_ne_ofNat, ↓reduceIte] at f exact (isEmptyElim f) · exact isEmptyElim (show _ by - simp [MagmaLanguage, hn, hn₂, Language.withConstants, Language.sum] at f + simp only [withConstants, Language.sum, MagmaLanguage, constantsOn_Functions, constantsOnFunc, + constantsOn_Relations, hn, ↓reduceIte] at f exact f.elim id fun h ↦ (Equiv.equivEmpty _) ((Nat.succ_pred_eq_of_ne_zero hn₂) ▸ h) ) @@ -246,18 +246,14 @@ theorem TermDefinable.trans (h₁₂ : L₂.TermDefinableFrom L₁) (h₂₃ : L intro G M hGL₁ obtain ⟨M₂,hGL₂,hA⟩ := h₁₂ M hGL₁ obtain ⟨M₃,hGL₃,hB⟩ := h₂₃ M₂ hGL₂ - use M₃, hGL₃ - exact trans_aux hA hB + exact ⟨M₃, hGL₃, trans_aux hA hB⟩ theorem TermStructural.trans (h₁₂ : L₂.TermStructuralFrom L₁) (h₂₃ : L₃.TermStructuralFrom L₂) : L₃.TermStructuralFrom L₁ := by intro G M hGL₁ obtain ⟨M₂,hGL₂,hA1,hA2⟩ := h₁₂ M hGL₁ obtain ⟨M₃,hGL₃,hB1,hB2⟩ := h₂₃ M₂ hGL₂ - use M₃, hGL₃ - constructor - · exact TermDefinable.trans_aux hA1 hB1 - · exact TermDefinable.trans_aux hB2 hA2 + exact ⟨M₃, hGL₃, TermDefinable.trans_aux hA1 hB1, TermDefinable.trans_aux hB2 hA2⟩ theorem Definable.trans_aux {G : Type} {M M₂ M₃ : Magma G} (h₁ : @Set.Definable _ (∅:Set _) MagmaLanguage M.FOStructure _ M₂.FinArityOp.arityGraph) @@ -268,15 +264,16 @@ theorem Definable.trans_aux {G : Type} {M M₂ M₃ : Magma G} intro n f by_cases hn : n = 2 · subst hn - simp - eta_reduce - convert h₁ + simp only [realize_functions, Magma.FOStructure_funMap'] + exact h₁ by_cases hn₂ : n = 0 · subst hn₂ - simp [MagmaLanguage, Language.withConstants, Language.sum] at f + simp only [withConstants, Language.sum, MagmaLanguage, constantsOn_Functions, constantsOnFunc, + constantsOn_Relations, OfNat.zero_ne_ofNat, ↓reduceIte] at f exact (isEmptyElim f) · exact isEmptyElim (show _ by - simp [MagmaLanguage, hn, hn₂, Language.withConstants, Language.sum] at f + simp only [withConstants, Language.sum, MagmaLanguage, constantsOn_Functions, constantsOnFunc, + constantsOn_Relations, hn, ↓reduceIte] at f exact f.elim id fun h ↦ (Equiv.equivEmpty _) ((Nat.succ_pred_eq_of_ne_zero hn₂) ▸ h) ) @@ -285,18 +282,14 @@ theorem Definable.trans (h₁₂ : L₂.DefinableFrom L₁) (h₂₃ : L₃.Defi intro G M hGL₁ obtain ⟨M₂,hGL₂,hA⟩ := h₁₂ M hGL₁ obtain ⟨M₃,hGL₃,hB⟩ := h₂₃ M₂ hGL₂ - use M₃, hGL₃ - exact trans_aux hA hB + exact ⟨M₃, hGL₃, trans_aux hA hB⟩ theorem Structural.trans (h₁₂ : L₂.StructuralFrom L₁) (h₂₃ : L₃.StructuralFrom L₂) : L₃.StructuralFrom L₁ := by intro G M hGL₁ obtain ⟨M₂,hGL₂,hA1,hA2⟩ := h₁₂ M hGL₁ obtain ⟨M₃,hGL₃,hB1,hB2⟩ := h₂₃ M₂ hGL₂ - use M₃, hGL₃ - constructor - · exact Definable.trans_aux hA1 hB1 - · exact Definable.trans_aux hB2 hA2 + exact ⟨M₃, hGL₃, Definable.trans_aux hA1 hB1, Definable.trans_aux hB2 hA2⟩ @[simp] theorem TermStructural.refl : L₁.TermStructuralFrom L₁ := diff --git a/equational_theories/Definability/Simple.lean b/equational_theories/Definability/Simple.lean index 5aeb183ad..677ee0e32 100644 --- a/equational_theories/Definability/Simple.lean +++ b/equational_theories/Definability/Simple.lean @@ -25,43 +25,30 @@ theorem FreeMagma.toTerm_realize {α M} (t : FreeMagma α) /-- Every law is TermStructural from its dual. -/ theorem TermStructural_dual (L : NatMagmaLaw) : L.TermStructuralFrom L.dual := by intro G M hGL - use ⟨fun x y ↦ M.op y x⟩ - constructor + refine ⟨⟨fun x y ↦ M.op y x⟩, ?_, ?_⟩ · rw [← law_dual_dual L] exact @satisfies_dual_dual _ _ ⟨_⟩ _ hGL - constructor <;> - { - use Functions.apply₂ (Sum.inl ()) (Term.var 1) (Term.var 0) - funext - rfl - } + · constructor <;> exact ⟨Functions.apply₂ (Sum.inl ()) (Term.var 1) (Term.var 0), rfl⟩ /-- The identity law x=x is TermDefinable from anything. This is a direct consequence of the fact that anything implies Eq1. -/ theorem Equation1_termDefinableFrom_all (L : NatMagmaLaw) : Law1.TermDefinableFrom L := by - apply termDefinable_of_termStructural - apply termStructural_of_implies - intro + refine termDefinable_of_termStructural (termStructural_of_implies fun _ ↦ ?_) simp [Law1.models_iff, Equation1] /-- Anything is TermDefinable from Eq2. This is a direct consequence of the fact that Eq2 implies anything. -/ theorem all_termDefinableFrom_Equation2 (L : NatMagmaLaw) : L.TermDefinableFrom Law2 := by - apply termDefinable_of_termStructural - apply termStructural_of_implies + refine termDefinable_of_termStructural (termStructural_of_implies ?_) simpa [implies] using Equation2_implies L /-- The left projection law is TermDefinable from anything. -/ theorem Equation4_termDefinableFrom_all (L : NatMagmaLaw) : Law4.TermDefinableFrom L := by intro G M hGL - use ⟨fun x _ ↦ x⟩ - constructor + refine ⟨⟨fun x _ ↦ x⟩, ?_, ?_⟩ · rw [@Law4.models_iff] - intro x y - rfl - · use Term.var 0 - funext - rfl + exact fun _ _ => rfl + · exact ⟨Term.var 0, rfl⟩ /-- The right projection law is TermDefinable from anything. -/ theorem Equation5_termDefinableFrom_all (L : NatMagmaLaw) : Law5.TermDefinableFrom L := diff --git a/equational_theories/Definability/Tarski543.lean b/equational_theories/Definability/Tarski543.lean index 84d216328..57e1d6b04 100644 --- a/equational_theories/Definability/Tarski543.lean +++ b/equational_theories/Definability/Tarski543.lean @@ -62,8 +62,7 @@ def CommSemigroupOf543 [Magma M] (h : Equation543 M) : CommSemigroup M := have h4369 : ∀_,_ := Equation543_implies_Equation4369 h -- (1.3) have h11 : ∀_,_ := Equation543_implies_Equation11 h have h40 : ∀_,_ := Equation543_implies_Equation40 h - have hcomm' (x y : M) : x ◇ ((x ◇ x) ◇ y) = y ◇ ((y ◇ y) ◇ x) := by - rw [← h4369, h40] + have hcomm' (x y : M) : x ◇ ((x ◇ x) ◇ y) = y ◇ ((y ◇ y) ◇ x) := by rw [← h4369, h40] have hcomm (x y : M) : x * y = y * x := hcomm' x y { @@ -144,11 +143,9 @@ private lemma groupDef {M : Type*} [op : Magma M] (h : Equation543 M) : have h16 : ∀_,_ := Equation543_implies_Equation16 h have h3823 : ∀_,_ := Equation543_implies_Equation3823 h have h4369 : ∀_,_ := Equation543_implies_Equation4369 h - constructor - · intro h1 - rw [← h1, ← h3823, ← h16] - · intro h1 - rw [h16 y (z ◇ z), h1, h4369, ← h3823, h4369, h4369 _ _ y, ← h16, ← h3823, ← h11] + constructor <;> intro h1 + · rw [← h1, ← h3823, ← h16] + · rw [h16 y (z ◇ z), h1, h4369, ← h3823, h4369, h4369 _ _ y, ← h16, ← h3823, ← h11] /-- Commuative structure, Equation 43, is given by a term from any magma obeying Tarski's one-equation abelian group subtraction law, Equation 543. -/