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

Metatheorem resolving all consequences of Equation1571 #341

Merged
merged 16 commits into from
Oct 7, 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
4 changes: 2 additions & 2 deletions equational_theories/AllEquations.lean
Original file line number Diff line number Diff line change
Expand Up @@ -3185,7 +3185,7 @@ equation 3163 := x = (((y ◇ y) ◇ z) ◇ y) ◇ x
equation 3164 := x = (((y ◇ y) ◇ z) ◇ y) ◇ y
equation 3165 := x = (((y ◇ y) ◇ z) ◇ y) ◇ z
equation 3166 := x = (((y ◇ y) ◇ z) ◇ y) ◇ w
equation 3167 := x = (((y ◇ y) ◇ z) ◇ z) ◇ x
-- equation 3167 := x = (((y ◇ y) ◇ z) ◇ z) ◇ x
equation 3168 := x = (((y ◇ y) ◇ z) ◇ z) ◇ y
equation 3169 := x = (((y ◇ y) ◇ z) ◇ z) ◇ z
equation 3170 := x = (((y ◇ y) ◇ z) ◇ z) ◇ w
Expand Down Expand Up @@ -4674,7 +4674,7 @@ equation 4652 := (x ◇ y) ◇ x = (z ◇ w) ◇ w
equation 4653 := (x ◇ y) ◇ x = (z ◇ w) ◇ u
equation 4654 := (x ◇ y) ◇ y = (x ◇ y) ◇ z
equation 4655 := (x ◇ y) ◇ y = (x ◇ z) ◇ y
equation 4656 := (x ◇ y) ◇ y = (x ◇ z) ◇ z
-- equation 4656 := (x ◇ y) ◇ y = (x ◇ z) ◇ z
equation 4657 := (x ◇ y) ◇ y = (x ◇ z) ◇ w
equation 4658 := (x ◇ y) ◇ y = (y ◇ x) ◇ x
equation 4659 := (x ◇ y) ◇ y = (y ◇ x) ◇ z
Expand Down
3 changes: 3 additions & 0 deletions equational_theories/Equations.lean
Original file line number Diff line number Diff line change
Expand Up @@ -90,6 +90,8 @@ equation 1689 := x = (y ◇ x) ◇ ((x ◇ z) ◇ z)

equation 2662 := x = ((x ◇ y) ◇ (x ◇ y)) ◇ x

abbrev Equation3167 (G: Type _) [Magma G] := ∀ x y z : G, x = (((y ◇ y) ◇ z) ◇ z) ◇ x

/-- From Putnam 1978, Problem A4, part (a) -/
equation 3722 := x ◇ y = (x ◇ y) ◇ (x ◇ y)

Expand All @@ -114,6 +116,7 @@ equation 4579 := x ◇ (y ◇ z) = (w ◇ u) ◇ z
/-- all products of three values are the same, regardless bracketing -/
equation 4582 := x ◇ (y ◇ z) = (w ◇ u) ◇ v

abbrev Equation4656 (G: Type _) [Magma G] := ∀ x y z : G, (x ◇ y) ◇ y = (x ◇ z) ◇ z

/- Some order 5 laws -/

Expand Down
194 changes: 194 additions & 0 deletions equational_theories/FreeSemigroup.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1,194 @@
import Mathlib.Logic.Basic

import equational_theories.Equations
import equational_theories.FreeMagma
import equational_theories.Homomorphisms
import equational_theories.MagmaLaw

open FreeMagma
open Law

def treeConcat {α : Type _} (t : FreeMagma α) : List α :=
match t with
| Lf a => [a]
| (tl ⋆ tr) => treeConcat tl ++ treeConcat tr

def rightJoinTrees {α : Type _} (t1 t2 : FreeMagma α) : FreeMagma α :=
match t1 with
| Lf a => Lf a ⋆ t2
| (tl ⋆ tr) => tl ⋆ (rightJoinTrees tr t2)

def rightAssociateTree {α : Type _} (t : FreeMagma α) : FreeMagma α :=
match t with
| Lf a => Lf a
| (tl ⋆ tr) => rightJoinTrees (rightAssociateTree tl) (rightAssociateTree tr)

theorem AssocImpliesForkEquivRightJoin {α : Type _} {G : Type _} [Magma G]
(assoc : Equation4512 G) (f : α → G) (tl tr : FreeMagma α)
: evalInMagma f (tl ⋆ tr) = evalInMagma f (rightJoinTrees tl tr) :=
match tl with
| Lf _ => Eq.refl _
| (tl1 ⋆ tl2) => Eq.trans
(Eq.symm $ assoc (evalInMagma f tl1) (evalInMagma f tl2) (evalInMagma f tr))
(congrArg (fun t ↦ (evalInMagma f tl1) ◇ t) (AssocImpliesForkEquivRightJoin assoc f tl2 tr))

/- Associativity allows us to fully right-associate an entire operation tree -/
theorem AssocFullyRightAssociate {α : Type _} {G : Type _} [Magma G]
(assoc : Equation4512 G) (f : α → G) (t : FreeMagma α)
: evalInMagma f t = evalInMagma f (rightAssociateTree t) :=
match t with
| Lf _ => Eq.refl _
| (tl ⋆ tr) => Eq.trans
(congrArg (fun s ↦ s ◇ (evalInMagma f tr)) (AssocFullyRightAssociate assoc f tl)) $ Eq.trans
(congrArg (fun s ↦ (evalInMagma f (rightAssociateTree tl)) ◇ s) (AssocFullyRightAssociate assoc f tr))
(AssocImpliesForkEquivRightJoin assoc f (rightAssociateTree tl) (rightAssociateTree tr))

/-- Example usage of AssocFullyRightAssociate -/
theorem Assoc4 {G : Type _} [Magma G] (assoc : Equation4512 G)
: ∀ x y z w : G, ((x ◇ y) ◇ z) ◇ w = x ◇ (y ◇ (z ◇ w)) :=
fun x y z w ↦ AssocFullyRightAssociate
assoc
(fun | 0 => x | 1 => y | 2 => z | 3 => w : Fin 4 → G)
(((Lf 0 ⋆ Lf 1) ⋆ Lf 2) ⋆ Lf 3)

inductive FreeSemigroup (α : Type _)
| Singleton : α → FreeSemigroup α
| Cons : α → FreeSemigroup α → FreeSemigroup α

local postfix:61 ".+" => FreeSemigroup.Singleton
local infixr:60 " ,+ " => FreeSemigroup.Cons

def semigroupConcat {α : Type _} (s1 s2 : FreeSemigroup α) : FreeSemigroup α :=
match s1 with
| a .+ => a ,+ s2
| a ,+ s1tail => a ,+ (semigroupConcat s1tail s2)

instance (α : Type _) : Magma (FreeSemigroup α) where
op := semigroupConcat

theorem FreeSgrAssoc {α : Type} : Equation4512 (FreeSemigroup α) :=
fun ls1 ls2 ls3 ↦ match ls1 with
| _ .+ => Eq.refl _
| a ,+ ls1' => congrArg (fun ls ↦ a ,+ ls) (FreeSgrAssoc ls1' ls2 ls3)

/- "Flatten" a FreeMagma tree expression into its semigroup representation -/
def freeMagmaToFreeSgr {α : Type _} : MagmaHom (FreeMagma α) (FreeSemigroup α) where
toFun := fun t ↦ evalInMagma FreeSemigroup.Singleton t
map_op' := fun s _ ↦ match s with
| Lf _ => Eq.refl _
| _ ⋆ _ => Eq.refl _

local postfix:70 " ↠Sgr " => freeMagmaToFreeSgr.toFun

def evalInSgr {α : Type _} {G : Type _} [Magma G] (f : α → G) (ls : FreeSemigroup α) : G :=
match ls with
| a .+ => f a
| a ,+ lstail => f a ◇ evalInSgr f lstail

def evalInSgrHom {α : Type _} {G : Type _} [Magma G] (assoc : Equation4512 G) (f : α → G) : MagmaHom (FreeSemigroup α) G where
toFun := evalInSgr f
map_op' := let rec mapper : ∀ ls1 ls2 : FreeSemigroup α, evalInSgr f (ls1 ◇ ls2) = evalInSgr f ls1 ◇ evalInSgr f ls2 :=
fun ls1 ls2 ↦ match ls1 with
| _ .+ => Eq.refl _
| a ,+ ls1' => Eq.trans
(congrArg (fun x ↦ f a ◇ x) (mapper ls1' ls2))
(assoc (f a) (evalInSgr f ls1') (evalInSgr f ls2))
mapper

def foldFreeSemigroup {G : Type _} [Magma G] (ls : FreeSemigroup G) : G :=
match ls with
| a .+ => a
| a ,+ lstail => a ◇ (foldFreeSemigroup lstail)

/- When evaluating in an associative structure, we may reduce a FreeMagma tree to a FreeSemigroup list -/
theorem AssocImpliesSgrProjFaithful {α : Type _} {G : Type _} [Magma G] (assoc : Equation4512 G) (f : α → G) (t : FreeMagma α)
: evalInMagma f t = evalInSgr f (freeMagmaToFreeSgr t) :=
match t with
| Lf a => Eq.refl _
| Lf a ⋆ tr => congrArg (fun y ↦ (f a) ◇ y) (AssocImpliesSgrProjFaithful assoc f tr)
| (tl1 ⋆ tl2) ⋆ tr => by
apply Eq.symm
apply Eq.trans $ congrArg (evalInSgr f) $ freeMagmaToFreeSgr.map_op' (tl1 ⋆ tl2) tr
apply Eq.trans $ congrArg (fun s ↦ evalInSgr f (s ◇ tr ↠Sgr)) $ freeMagmaToFreeSgr.map_op' tl1 tl2
apply Eq.trans $ (evalInSgrHom assoc f).map_op' (tl1 ↠Sgr ◇ tl2 ↠Sgr) (tr ↠Sgr)
apply Eq.trans $ congrArg (fun s ↦ s ◇ (evalInSgr f (tr ↠Sgr))) $ (evalInSgrHom assoc f).map_op' (tl1 ↠Sgr) (tl2 ↠Sgr)
apply Eq.symm
apply Eq.trans $ congrArg (fun s ↦ _ ◇ s) (AssocImpliesSgrProjFaithful assoc f tr)
apply Eq.trans $ congrArg (fun s ↦ (s ◇ _) ◇ _) (AssocImpliesSgrProjFaithful assoc f tl1)
apply Eq.trans $ congrArg (fun s ↦ (_ ◇ s) ◇ _) (AssocImpliesSgrProjFaithful assoc f tl2)
trivial

def insertSgrSorted {n : Nat} (i : Fin n) (ls : FreeSemigroup (Fin n)) : FreeSemigroup (Fin n) :=
match ls with
| j .+ => if i ≤ j then i ,+ j .+ else j ,+ i .+
| j ,+ lstail => if i ≤ j then i ,+ j ,+ lstail else j ,+ i ,+ lstail

def insertionSortSgr {n : Nat} (ls : FreeSemigroup (Fin n)) : FreeSemigroup (Fin n) :=
match ls with
| i .+ => i .+
| i ,+ lstail => insertSgrSorted i (insertionSortSgr lstail)

theorem CommSgrImpliesInsertSortedFaithful {n : Nat} {G : Type _} [Magma G] (assoc : Equation4512 G) (comm : Equation43 G) (f : Fin n → G)
: ∀ i : Fin n, ∀ ls : FreeSemigroup (Fin n), evalInSgr f (insertSgrSorted i ls) = (f i) ◇ evalInSgr f ls :=
fun i ls ↦ match ls with
| j .+ => by
have eqor := ite_eq_or_eq (i ≤ j) (i ,+ j .+) (j ,+ i .+)
cases eqor with
| inl eq1 => apply Eq.trans (congrArg (evalInSgr f) eq1); exact Eq.refl _
| inr eq2 => apply Eq.trans (congrArg (evalInSgr f) eq2); exact comm (f j) (f i)
| j ,+ lstail => by
have eqor := ite_eq_or_eq (i ≤ j) (i ,+ j ,+ lstail) (j ,+ i ,+ lstail)
cases eqor with
| inl eq1 =>
apply Eq.trans (congrArg (evalInSgr f) eq1);
exact Eq.refl _
| inr eq2 =>
apply Eq.trans (congrArg (evalInSgr f) eq2);
apply Eq.trans $ assoc (f j) (f i) _;
rw [comm (f j) (f i)];
exact Eq.symm $ assoc (f i) (f j) _

theorem CommSgrImpliesInsertionSortFaithful {n : Nat} {G : Type _} [Magma G] (assoc : Equation4512 G) (comm : Equation43 G) (f : Fin n → G)
: ∀ ls : FreeSemigroup (Fin n), evalInSgr f ls = evalInSgr f (insertionSortSgr ls)
| _ .+ => Eq.refl _
| i ,+ lstail => Eq.trans
(congrArg (fun s ↦ (f i) ◇ s) (CommSgrImpliesInsertionSortFaithful assoc comm f lstail))
(Eq.symm $ CommSgrImpliesInsertSortedFaithful assoc comm f i (insertionSortSgr lstail))

def involutionReduce {α : Type _} [DecidableEq α] (ls : FreeSemigroup α) : FreeSemigroup α :=
match ls with
| a .+ => a .+
| a ,+ b .+ => a ,+ b .+
| a ,+ b ,+ lstail => if (a = b) then involutionReduce lstail else a ,+ involutionReduce (b ,+ lstail)

def InvolutiveImpliesInvolutionReduceFaithful {α : Type _} [DecidableEq α] {G : Type _} [Magma G] (ls : FreeSemigroup α) (invol : Equation16 G) (f : α → G)
: evalInSgr f ls = evalInSgr f (involutionReduce ls) :=
match ls with
| a .+ => Eq.refl _
| a ,+ b .+ => Eq.refl _
| a ,+ b ,+ lstail => by
have eqor := dite_eq_or_eq (P := a = b) (A := fun _ ↦ involutionReduce lstail) (B := fun _ ↦ a ,+ involutionReduce (b ,+ lstail))
cases eqor with
| inl eqcase =>
apply Eq.trans $ congrArg (fun s ↦ (f s) ◇ (f b ◇ (evalInSgr f lstail))) eqcase.1
apply Eq.trans $ Eq.symm $ invol (evalInSgr f lstail) (f b)
apply Eq.trans $ InvolutiveImpliesInvolutionReduceFaithful lstail invol f
exact Eq.symm $ congrArg (evalInSgr f) eqcase.2
| inr neqcase =>
apply Eq.symm
apply Eq.trans $ congrArg (evalInSgr f) neqcase.2
exact congrArg (fun s ↦ f a ◇ s) $ Eq.symm $ InvolutiveImpliesInvolutionReduceFaithful (b ,+ lstail) invol f

def equation1571Reducer {n : Nat} (t : FreeMagma (Fin (n+1))) : FreeSemigroup (Fin (n+1)) :=
involutionReduce $ insertionSortSgr $ freeMagmaToFreeSgr (t ⋆ (Lf (Fin.last n) ⋆ Lf (Fin.last n)))

def AbGrpPow2ImpliesEquation1571ReducerFaithful {n : Nat} {G : Type _} [Magma G] (t : FreeMagma (Fin (n+1))) (f : Fin (n+1) → G)
(assoc : Equation4512 G) (comm : Equation43 G) (invol : Equation16 G)
: evalInMagma f t = evalInSgr f (equation1571Reducer t) := by
apply Eq.symm
apply Eq.trans $ Eq.symm $ InvolutiveImpliesInvolutionReduceFaithful _ invol f
apply Eq.trans $ Eq.symm $ CommSgrImpliesInsertionSortFaithful assoc comm f _
apply Eq.trans $ Eq.symm $ AssocImpliesSgrProjFaithful assoc f _
apply Eq.trans $ comm (evalInMagma f t) _
apply Eq.trans $ Eq.symm $ assoc _ _ _
exact Eq.symm $ invol (evalInMagma f t) (f $ Fin.last n)
60 changes: 43 additions & 17 deletions equational_theories/Subgraph.lean
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,8 @@ import equational_theories.EquationalResult
import equational_theories.Closure
import equational_theories.Equations
import equational_theories.FactsSyntax
import equational_theories.FreeSemigroup
import equational_theories.MagmaLaw

/- This is a subproject of the main project to completely describe a small subgraph of the entire
implication graph. The list of equations under consideration can be found at https://teorth.github.io/equational_theories/blueprint/subgraph-eq.html
Expand Down Expand Up @@ -282,44 +284,68 @@ theorem Lemma_eq1689_implies_h8 (G: Type*) [Magma G] (h: Equation1689 G) : ∀ a

/-- The below results for Equation1571 are out of order because early ones are lemmas for later ones -/
@[equational_result]
theorem Equation1571_implies_Equation2662 (G: Type*) [Magma G] (h: Equation1571 G) : Equation2662 G :=
fun _ _ ↦ (h _ _ _).trans (congrArg _ (h _ _ _).symm)
theorem Equation1571_implies_Equation2662 (G: Type _) [Magma G] (h: Equation1571 G) : Equation2662 G :=
fun x y ↦ Eq.trans (h x (x ◇ y) (x ◇ y)) (congrArg (fun z ↦ ((x ◇ y) ◇ (x ◇ y)) ◇ z)
(Eq.symm $ h x x y))

@[equational_result]
theorem Equation1571_implies_Equation40 (G: Type*) [Magma G] (h: Equation1571 G) : Equation40 G := by
have sqRotate (x y z : G) : (x ◇ y) ◇ (x ◇ y) = (y ◇ z) ◇ (y ◇ z) :=
(congrArg (fun w ↦ (x ◇ y) ◇ (x ◇ w)) (Equation1571_implies_Equation2662 G h _ _)).trans
(h _ _ _).symm
exact fun x y ↦ h x x x ▸ h y y y ▸ (sqRotate _ _ _).trans (sqRotate _ _ _)
theorem Equation1571_implies_Equation40 (G: Type _) [Magma G] (h: Equation1571 G) : Equation40 G := by
have sqRotate : ∀ x y z : G, (x ◇ y) ◇ (x ◇ y) = (y ◇ z) ◇ (y ◇ z) :=
fun x y z ↦ Eq.trans (congrArg (fun w ↦ (x ◇ y) ◇ (x ◇ w))
(Equation1571_implies_Equation2662 G h y z)) (Eq.symm $ h ((y ◇ z) ◇ (y ◇ z)) x y)
have sqConstInImage : ∀ x y z w : G, (x ◇ y) ◇ (x ◇ y) = (z ◇ w) ◇ (z ◇ w) :=
fun x y z w ↦ Eq.trans (sqRotate x y z) (sqRotate y z w)
exact fun x y ↦ h x x x ▸ h y y y ▸ sqConstInImage (x ◇ x) (x ◇ (x ◇ x)) (y ◇ y) (y ◇ (y ◇ y))

@[equational_result]
theorem Equation1571_implies_Equation23 (G: Type*) [Magma G] (h: Equation1571 G) : Equation23 G := by
theorem Equation1571_implies_Equation23 (G: Type _) [Magma G] (h: Equation1571 G) : Equation23 G := by
refine fun x ↦ (h x (x ◇ x) (x ◇ x)).trans ?_
rw [← h x x x, ← Equation1571_implies_Equation40 G h x (x ◇ x)]

@[equational_result]
theorem Equation1571_implies_Equation8 (G: Type*) [Magma G] (h: Equation1571 G) : Equation8 G :=
fun x ↦ (h x x x).trans ((congrArg (· ◇ (x ◇ (x ◇ x))) (Equation1571_implies_Equation40 G h x
(x ◇ (x ◇ x)))).trans (Equation1571_implies_Equation23 G h (x ◇ (x ◇ x))).symm)
theorem Equation1571_implies_Equation8 (G: Type _) [Magma G] (h: Equation1571 G) : Equation8 G :=
fun x ↦ Eq.trans (h x x x) (((congrArg (fun a ↦ a ◇ (x ◇ (x ◇ x))))
(Equation1571_implies_Equation40 G h x (x ◇ (x ◇ x)))).trans
(((Equation1571_implies_Equation23 G h (x ◇ (x ◇ x))).symm).trans rfl))

@[equational_result]
theorem Equation1571_implies_Equation16 (G: Type*) [Magma G] (h: Equation1571 G) : Equation16 G :=
theorem Equation1571_implies_Equation16 (G: Type _) [Magma G] (h: Equation1571 G) : Equation16 G :=
fun x y ↦ ((congrArg (fun w ↦ y ◇ (y ◇ w)) (Equation1571_implies_Equation8 G h x)).trans
(Equation1571_implies_Equation40 G h x y ▸ ((congrArg (· ◇ (y ◇ (x ◇ (y ◇ y)))))
(Equation1571_implies_Equation8 G h y)).trans (h x y (y ◇ y)).symm)).symm
((Equation1571_implies_Equation40 G h x y ▸ ((congrArg (fun w ↦ w ◇ (y ◇ (x ◇ (y ◇ y)))))
(Equation1571_implies_Equation8 G h y)).trans (h x y (y ◇ y)).symm))).symm

@[equational_result]
theorem Equation1571_implies_Equation43 (G: Type*) [Magma G] (h: Equation1571 G) : Equation43 G := by
theorem Equation1571_implies_Equation43 (G: Type _) [Magma G] (h: Equation1571 G) : Equation43 G := by
refine fun x y ↦ (h _ (x ◇ x) (x ◇ (x ◇ y))).trans ?_
rw [← h x x y, ← Equation1571_implies_Equation23 G h x, ← Equation1571_implies_Equation16 G h y x,
Equation1571_implies_Equation40 G h x y, ← Equation1571_implies_Equation23 G h y]

@[equational_result]
theorem Equation1571_implies_Equation4512 (G: Type*) [Magma G] (h: Equation1571 G) : Equation4512 G := by
theorem Equation1571_implies_Equation4512 (G: Type _) [Magma G] (h: Equation1571 G) : Equation4512 G := by
refine fun x y z ↦ (h (x ◇ (y ◇ z)) y x).trans ?_
rw [Equation1571_implies_Equation43 G h (x ◇ (y ◇ z)) x,
← Equation1571_implies_Equation16 G h (y ◇ z) x, ← Equation1571_implies_Equation16 G h z y,
Equation1571_implies_Equation43 G h y x]
Equation1571_implies_Equation43 G h y x]

theorem ProveEquation1571Consequence {n : Nat} {G : Type _} [Magma G] (eq1571 : Equation1571 G)
(law : Law.MagmaLaw (Fin (n+1))) (eq : equation1571Reducer law.lhs = equation1571Reducer law.rhs)
: G ⊧ law :=
fun _ ↦ (AbGrpPow2ImpliesEquation1571ReducerFaithful law.lhs _
(Equation1571_implies_Equation4512 G eq1571) (Equation1571_implies_Equation43 G eq1571)
(Equation1571_implies_Equation16 G eq1571)).trans ((congrArg (evalInSgr _) eq).trans
(AbGrpPow2ImpliesEquation1571ReducerFaithful law.rhs _
(Equation1571_implies_Equation4512 G eq1571) (Equation1571_implies_Equation43 G eq1571)
(Equation1571_implies_Equation16 G eq1571)).symm)

/- Example usage of the general-purpose prover ProveEquation1571Consequence -/
theorem Equation1571_implies_Equation3167 {G : Type} [Magma G] (h : Equation1571 G) : Equation3167 G :=
fun x y z ↦ ProveEquation1571Consequence (n := 2) h
{lhs := Lf 0, rhs := (((Lf 1 ⋆ Lf 1) ⋆ Lf 2) ⋆ Lf 2) ⋆ Lf 0} rfl fun | 0 => x | 1 => y | 2 => z

/- Example usage of the general-purpose prover ProveEquation1571Consequence -/
theorem Equation1571_implies_Equation4656 {G : Type} [Magma G] (h : Equation1571 G) : Equation4656 G :=
fun x y z ↦ ProveEquation1571Consequence (n := 2) h
{lhs := (Lf 0 ⋆ Lf 1) ⋆ Lf 1, rhs := (Lf 0 ⋆ Lf 2) ⋆ Lf 2} rfl fun | 0 => x | 1 => y | 2 => z

/-- This result was first obtained by Kisielewicz in 1997 via computer assistance. -/
@[equational_result]
Expand Down