Skip to content

Commit

Permalink
Prove 3588 !-> [3862, 3878, 3917, 3955]
Browse files Browse the repository at this point in the history
This is unfortunately very slow due to automated case splitting and resolution.
  • Loading branch information
lyphyser committed Oct 9, 2024
1 parent 8b11a32 commit 4dbde64
Showing 1 changed file with 247 additions and 0 deletions.
247 changes: 247 additions & 0 deletions equational_theories/Confluence.lean
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@ import equational_theories.FreeMagma
import equational_theories.AllEquations
import equational_theories.FactsSyntax
import Mathlib.Tactic.NthRewrite
import Mathlib.Tactic.CasesM

namespace FreeMagma

Expand Down Expand Up @@ -1013,4 +1014,250 @@ theorem «Facts» : ∃ (G : Type) (_ : Magma G), Facts G [1110] [8, 411, 1629,

end rw1110




namespace rw3588

variable [DecidableEq α]

def rule2 : FreeMagma α → Option (FreeMagma α)
| ((z1 ⋆ w1) ⋆ (x ⋆ y)) ⋆ (z2 ⋆ w2) =>
if z1 = z2 ∧ w1 = w2 then
x ⋆ y
else
none
| _ => none

-- equation 3588 := x ◇ y = z ◇ ((x ◇ y) ◇ z)
def rule1 : FreeMagma α → Option (FreeMagma α)
| z1 ⋆ ((x ⋆ y) ⋆ z2) =>
if z1 = z2 then
x ⋆ y
else
none
| _ => none

def rule (x: FreeMagma α): FreeMagma α :=
((rule1 x).or (rule2 x)).getD x

syntax "sledgehammer" : tactic

macro_rules
| `(tactic| sledgehammer) => `(tacticSeq|
repeat'
split at *
any_goals
try injections
try cases_type* And
try subst_eqs
try trivial
all_goals
try simp_all
try cases_type* And
try intros
try subst_eqs
)

lemma rule_op_is_op (x y: FreeMagma α): ∃ x' y', rule (x ⋆ y) = x' ⋆ y' := by
simp [rule, rule1, rule2, Option.or, Option.getD]
sledgehammer

def rule_eq_rule21 {x: FreeMagma α}:
rule x = ((rule2 x).or (rule1 x)).getD x := by
simp [rule, rule1, rule2, Option.or, Option.getD]
sledgehammer

instance rule_projection : IsProj (@rule α _) where
proj := by
intro x
simp [rule, rule1, rule2, Option.or, Option.getD]
sledgehammer
· apply SubtermOf.right
apply SubtermOf.left
rfl
· apply SubtermOf.left
apply SubtermOf.right
rfl
· apply SubtermOf.left
apply SubtermOf.right
rfl

theorem not_nf_zxyz {α : Type} [inst : DecidableEq α] {x y z : FreeMagma α}:
¬NF rule (z ⋆ ((x ⋆ y) ⋆ z)) := by
intro h
replace h := rw_eq_self_of_NF rule h
simp [rule, rule1, rule2] at h
cases h
subst_eqs

theorem not_nf_zwxyzw {α : Type} [inst : DecidableEq α] {x y z w : FreeMagma α}:
¬NF rule (((z ⋆ w) ⋆ (x ⋆ y)) ⋆ (z ⋆ w)) := by
intro h
replace h := rw_eq_self_of_NF rule h
simp [rule_eq_rule21, rule1, rule2] at h
cases h
subst_eqs

theorem rule_nz_xyz {n x y z : FreeMagma α}
(hn : NF rule n) (h: rule (n ⋆ z) = x ⋆ y ⋆ z):
x ⋆ y = n := by
nth_rw 1 [rule.eq_def] at h
simp [rule2, Option.or, Option.getD] at h
sledgehammer
· simp_all [rule1]
sledgehammer
· exfalso
apply not_nf_zxyz hn

theorem rule_nzwxy_zw {n x y z w : FreeMagma α}
(hn : NF rule n) (h: rule (n ⋆ (z ⋆ w ⋆ (x ⋆ y))) = z ⋆ w):
x ⋆ y = n := by
simp [rule, rule2, Option.or, Option.getD] at h
sledgehammer
· simp_all [rule1]
· exfalso
apply not_nf_zwxyzw hn

theorem foo1 {n x y z w x' y' w' : FreeMagma α}
(hn: NF rule n) (h: rule (n ⋆ (z ⋆ w ⋆ (x ⋆ y))) = x' ⋆ y' ⋆ w')
(h' : ¬z ⋆ w ⋆ (x ⋆ y) = w')
(h'' : z = x' ⋆ y' → ¬w = w'):
z ⋆ w ⋆ (x ⋆ y) ⋆ (x' ⋆ y' ⋆ w') = n := by
simp [rule, rule2, Option.or, Option.getD] at h
sledgehammer
· simp_all [rule1]

theorem foo2 {x0 y0 n x y z w w' z' : FreeMagma α} (hn: NF rule n)
(h: rule (n ⋆ (z ⋆ w ⋆ (x ⋆ y))) = z' ⋆ w')
(hnf: n = x0 ⋆ y0)
(h': z = z' → ¬w = w')
(h'': ∀ z'' x' y' z''', ¬z ⋆ w ⋆ (x ⋆ y) ⋆ (z' ⋆ w') = z'' ⋆ (x' ⋆ y' ⋆ z''')):
z ⋆ w ⋆ (x ⋆ y) ⋆ (z' ⋆ w') = n := by
unhygienic
simp [rule, rule2, Option.or, Option.getD] at h
sledgehammer
any_goals simp_all [rule1]
· apply h''
any_goals apply Eq.refl _
· exfalso
apply h''
any_goals apply Eq.refl _

theorem foo3 {n x0 y0 z x y z': FreeMagma α}
(hnf: n = x0 ⋆ y0)
(h: rule (n ⋆ z) = x ⋆ y ⋆ z')
(h': ∀ (z1 w1 x y z2 w2 : FreeMagma α), z = z1 ⋆ w1 ⋆ (x ⋆ y) → ¬rule (n ⋆ (z1 ⋆ w1 ⋆ (x ⋆ y))) = z2 ⋆ w2)
(h'': ¬z = z'):
z ⋆ (x ⋆ y ⋆ z') = n := by
unhygienic
simp [rule, rule1, rule2, Option.or, Option.getD] at *
sledgehammer
exfalso
apply h'
any_goals apply Eq.refl _

set_option maxHeartbeats 999999

theorem foo4.inner {x0 y0 z : FreeMagma α}
(hn : NF rule (x0 ⋆ y0))
(h : ∀ (z1 w1 x y z2 w2 : FreeMagma α), z = z1 ⋆ w1 ⋆ (x ⋆ y) → ¬rule (x0 ⋆ y0 ⋆ (z1 ⋆ w1 ⋆ (x ⋆ y))) = z2 ⋆ w2)
(h' : ∀ (x y z2 : FreeMagma α), ¬rule (x0 ⋆ y0 ⋆ z) = x ⋆ y ⋆ z2)
(heq : rule1 (x0 ⋆ y0 ⋆ z) = none)
(x_5 : ∀ (z1 w1 x y z2 w2 : FreeMagma α), x0 = z1 ⋆ w1 → y0 = x ⋆ y → ¬z = z2 ⋆ w2) : False := by
unhygienic
simp [rule1, rule2, Option.or, Option.getD] at *
sledgehammer
· simp [rule, rule1, rule2, Option.or, Option.getD] at h'
sledgehammer
apply x_5
any_goals apply Eq.refl _
· simp [rule, rule1, rule2, Option.or, Option.getD] at h'
sledgehammer
· apply x_2
any_goals apply Eq.refl _
· apply x_5
any_goals apply Eq.refl _
· apply x_5
any_goals apply Eq.refl _


theorem foo4 {x0 y0 n z : FreeMagma α} (hn : NF rule n)
(hnf: n = x0 ⋆ y0)
(h : ∀ (z1 w1 x y z2 w2 : FreeMagma α), z = z1 ⋆ w1 ⋆ (x ⋆ y) → ¬rule (n ⋆ (z1 ⋆ w1 ⋆ (x ⋆ y))) = z2 ⋆ w2)
(h' : ∀ (z1 x y z2 : FreeMagma α), z = z1 → ¬rule (n ⋆ z1) = x ⋆ y ⋆ z2):
z ⋆ rule (n ⋆ z) = n := by
specialize h' z
simp_all
unhygienic
simp [rule, rule2, Option.or, Option.getD]
sledgehammer
· any_goals simp_all [rule1]
sledgehammer
exfalso
apply h
any_goals apply Eq.refl _
simp [rule, rule1, rule2, Option.or, Option.getD]
any_goals constructorm* _ ∧ _
any_goals apply Eq.refl _
· exfalso
simp [rule, rule1, rule2, Option.or, Option.getD] at *
sledgehammer
apply h
any_goals apply Eq.refl _
· exfalso
apply foo4.inner (α := α)
any_goals assumption

theorem rule_zxyz {α} [DecidableEq α] {x y z : FreeMagma α} (hx: NF rule x) (hy: NF rule y):
rule (z ⋆ rule (rule (x ⋆ y) ⋆ z)) = rule (x ⋆ y) := by
unhygienic
have hrxy := NF_rw_op rule hx hy
let rxy := rule (x ⋆ y)
have: rule (x ⋆ y) = rxy := rfl
rw [this]
rw [rule.eq_def]
simp only [rule2, Option.or, Option.getD]
sledgehammer
· simp [rule1] at *
sledgehammer
apply rule_nz_xyz hrxy
assumption
· apply rule_nzwxy_zw hrxy
assumption
· simp [rule1] at *
repeat
split at *
all_goals
injections
try subst_eqs
· apply foo1
any_goals assumption
· have ⟨x0, y0, hrxyf⟩ := rule_op_is_op x y
apply foo2
any_goals assumption

· simp [rule1] at *
sledgehammer
· have ⟨x0, y0, hrxyf⟩ := rule_op_is_op x y
apply foo3
any_goals assumption
· have ⟨x0, y0, hrxyf⟩ := rule_op_is_op x y
apply foo4
any_goals assumption

@[equational_result]
theorem «Facts» :
∃ (G : Type) (_ : Magma G), Facts G [3588] [3862, 3878, 3917, 3955] := by
use ConfMagma (@rule Nat _), inferInstance
repeat' apply And.intro
· rintro ⟨x, hx⟩ ⟨y, hy⟩ ⟨z, hz⟩
simp [Magma.op, bu, hx, hy, hz]
symm
congr! 1
apply rule_zxyz ((NF_iff_buFixed rule).mpr hx) ((NF_iff_buFixed rule).mpr hy)
all_goals refute

end rw3588

end Confluence

0 comments on commit 4dbde64

Please sign in to comment.