Prove 3588 !-> [3862, 3878, 3917, 3955]

We prove this using a proof that is specific to this equation, but designed to be mostly generalizable and perhaps possible to automatically generalize.
teorth · Oct 9, 2024 · 8d52243 · 8d52243
1 parent 68f981f
commit 8d52243
Show file tree

Hide file tree

Showing 2 changed files with 195 additions and 0 deletions.
diff --git a/equational_theories/Confluence.lean b/equational_theories/Confluence.lean
@@ -1,7 +1,9 @@
+import equational_theories.ConfluenceAttr
 import equational_theories.FreeMagma
 import equational_theories.AllEquations
 import equational_theories.FactsSyntax
 import Mathlib.Tactic.NthRewrite
+import Mathlib.Tactic.CasesM
 
 namespace FreeMagma
 
@@ -1011,4 +1013,193 @@ theorem «Facts» : ∃ (G : Type) (_ : Magma G), Facts G [1110] [8, 411, 1629,
 
 end rw1110
 
+
+
+open Lean.Parser.Tactic
+
+attribute [confluence_simps] not_true_eq_false not_false_eq_true false_implies implies_true imp_false false_and and_true and_self not_and and_imp
+attribute [confluence_simps] ite_eq_right_iff
+attribute [confluence_simps] Option.or Option.getD Option.ite_none_right_eq_some Option.some.injEq
+attribute [confluence_simps] forall_apply_eq_imp_iff₂
+attribute [confluence_simps] Fork.injEq
+
+simproc [confluence_simps] confluenceReduceCtorEq (_) := reduceCtorEq
+
+local macro "separate" : tactic => `(tactic| (
+  try intros
+  try repeat
+    simp only [Not.eq_1]
+    try intros
+  try injections
+  try casesm* _ ∨ _, _ ∧ _, Exists _
+  try any_goals
+    try subst_eqs
+    try trivial
+))
+
+local macro "autosplit" : tactic => `(tactic| (
+  try any_goals separate
+  repeat'
+    split at *
+    try any_goals separate
+))
+
+local macro "prove_elim" : tactic => `(tactic| (
+  autosplit
+  all_goals simp_all only [confluence_simps, exists_and_right, exists_eq_right_right', exists_eq_right', false_iff, not_exists]
+  constructor
+  · intro h
+    subst_eqs
+    repeat constructor
+  · autosplit
+))
+
+local macro "prove_elim_not" : tactic => `(tactic| (
+  autosplit
+  all_goals simp_all only [confluence_simps, false_iff, not_exists, not_and, true_iff, forall_eq', forall_apply_eq_imp_iff, true_iff, not_false_eq_true]
+  try separate
+  rename_i h
+  rw [eq_comm]
+  apply h
+  try trivial
+))
+
+local macro "compute" lemmus:simpLemma : tactic => `(tactic| (
+  simp only [$lemmus, ↓reduceIte, and_self]
+))
+
+namespace rw3588
+
+variable [DecidableEq α]
+
+-- 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
+
+-- generated by Knuth-Bendix completion with Vampire or kbcv
+def rule2 : FreeMagma α → Option (FreeMagma α)
+  | ((z1 ⋆ w1) ⋆ (x ⋆ y)) ⋆ (z2 ⋆ w2) =>
+    if z1 = z2 ∧ w1 = w2 then
+      x ⋆ y
+    else
+      none
+  | _ => none
+
+def rule (x: FreeMagma α): FreeMagma α :=
+  ((rule1 x).or (rule2 x)).getD x
+
+def rule_eq_rule21' (x: FreeMagma α):
+  rule x = ((rule2 x).or (rule1 x)).getD x := by
+  simp only [rule, Option.or, Option.getD]
+  autosplit
+  any_goals simp_all only [Option.some.injEq]
+  exfalso
+  simp_all only [rule1, rule2]
+  autosplit
+
+def rule_eq_rule12 (x: FreeMagma α) := by
+  simpa [rule1, rule2, Option.or, Option.getD] using rule.eq_def x
+
+def rule_eq_rule21 {x: FreeMagma α} := by
+  simpa [rule1, rule2, Option.or, Option.getD] using rule_eq_rule21' x
+
+def rule2.elim (e r: FreeMagma α): rule2 e = some r ↔
+  ∃ x y z w, e = ((z ⋆ w) ⋆ (x ⋆ y)) ⋆ (z ⋆ w) ∧ r = x ⋆ y := by
+  simp only [rule2]
+  prove_elim
+
+def rule2.elim_not (e: FreeMagma α): rule2 e = none ↔
+  ¬∃ x y z w, e = ((z ⋆ w) ⋆ (x ⋆ y)) ⋆ (z ⋆ w) := by
+  simp only [rule2]
+  prove_elim_not
+
+def rule1.elim (e r: FreeMagma α): rule1 e = some r ↔
+  ∃ x y z, e = z ⋆ ((x ⋆ y) ⋆ z) ∧ r = x ⋆ y := by
+  simp only [rule1]
+  prove_elim
+
+def rule1.elim_not (e: FreeMagma α): rule1 e = none ↔
+  ¬∃ x y z, e = z ⋆ ((x ⋆ y) ⋆ z) := by
+  simp only [rule1]
+  prove_elim_not
+
+def rule.elim' (x y: FreeMagma α): rule x = y ↔
+  rule1 x = some y ∨ rule2 x = some y ∨ (x = y ∧ rule1 x = none ∧ rule2 x = none) := by
+  constructor
+  · intro h
+    simp only [rule, Option.or, Option.getD] at h
+    autosplit
+    all_goals simp_all
+  · intro h
+    rcases h with h1 | h2 | ⟨h0, h1, h2⟩
+    next h1 => simp only [rule, h1, Option.or, Option.getD]
+    next h2 => simp only [rule_eq_rule21', h2, Option.or, Option.getD]
+    next h' => simp only [rule, ← h0, h1, h2, Option.or, Option.getD]
+
+def rule.elim (e r: FreeMagma α) := by
+  simpa only [rule1.elim, rule2.elim, rule1.elim_not, rule2.elim_not] using rule.elim' e r
+
+instance rule_projection : IsProj (@rule α _) where
+  proj := by
+    intro x
+    simp only [rule, rule1, rule2, Option.or, Option.getD]
+    autosplit
+    · apply SubtermOf.right
+      apply SubtermOf.left
+      rfl
+    · apply SubtermOf.left
+      apply SubtermOf.right
+      rfl
+    · apply SubtermOf.left
+      apply SubtermOf.right
+      rfl
+
+theorem comp1 {α} [DecidableEq α] {x y z : FreeMagma α}:
+    rule (z ⋆ (x ⋆ y ⋆ z)) = x ⋆ y := by
+  compute rule_eq_rule12
+
+theorem comp2 {α} [DecidableEq α] {x y z : FreeMagma α} (hxy: NF rule (x ⋆ y)):
+    rule (z ⋆ rule (x ⋆ y ⋆ z)) = x ⋆ y := by
+  generalize h: rule (x ⋆ y ⋆ z) = e
+  simp only [rule.elim] at h
+  separate
+  · compute rule_eq_rule21
+  · apply rw_eq_self_of_NF rule hxy
+  · exact comp1
+
+theorem comp3 {α} [DecidableEq α] {x y z : FreeMagma α} (hx: NF rule x) (hy: NF rule y):
+    rule (z ⋆ rule (rule (x ⋆ y) ⋆ z)) = rule (x ⋆ y) := by
+  generalize h: rule (x ⋆ y) = e
+  simp only [rule.elim] at h
+  separate
+  all_goals apply comp2
+  · apply Everywhere.left hy
+  · apply Everywhere.right hx
+  · rw [NF, Everywhere]
+    refine ⟨hx, hy, ?_⟩
+    simp only [rule.elim]
+    right
+    right
+    constructorm* _ ∧ _
+    all_goals trivial
+
+@[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 only [Magma.op, bu, hx, hy, hz, buFixed_rw_op]
+    symm
+    congr! 1
+    apply comp3 ((NF_iff_buFixed rule).mpr hx) ((NF_iff_buFixed rule).mpr hy)
+  all_goals refute
+
+end rw3588
+
 end Confluence
diff --git a/equational_theories/ConfluenceAttr.lean b/equational_theories/ConfluenceAttr.lean
@@ -0,0 +1,4 @@
+import Lean.Meta.Tactic.Simp.RegisterCommand
+
+-- doesn't work in the same file where it's declared
+register_simp_attr confluence_simps