3102 does not imply 3176

Stream: Equational

[Johan Commelin]

I found this one in
https://github.com/amirlb/equational_theories/blob/extract_implications_equivalence_creators_data/scripts/equivalence_creators.json
Is it still open? Here is an almost complete sketch of a counterexample:

abbrev M : Type := String

def M.mul (a b : M) : M :=
  if a == b then b else
  if a.endsWith (b ++ b ++ b) then b else a ++ b

infixl:70 " * " => M.mul

theorem M.mul_def (a b : M) : a * b =
  if a == b then b else
  if a.endsWith (b ++ b ++ b) then b else a ++ b := rfl

@[simp]
theorem M.mul_self (a : M) : a * a = a := by
  simp [M.mul_def a a, if_pos]

/-- `M` satisfies 3102 -/
example (x y : M) : x = (((y * x) * x) * x) * x := by
  rw [M.mul_def y x]
  split
  next h => simp
  next h =>
  split
  next h => simp
  rw [M.mul_def (y ++ x) x]
  split
  next h => simp
  next h =>
  split
  next h => simp
  rw [M.mul_def (y ++ x ++ x) x]
  split
  next h => simp
  next h =>
  split
  next h => simp
  rw [M.mul_def _ x]
  split
  next h => simp
  next h =>
  rw [if_pos]
  sorry

/-- `M` does not satisfy 3176 -/
example : ∃ (x y z : M), x ≠ (((y * z) * x) * x) * x := by
  exists "a", "b", "c"
  simp [M.mul_def "b"]
  rw [if_neg ?f]
  case f => decide
  simp [M.mul_def "bc"]
  rw [if_neg ?f]
  case f => decide
  simp [M.mul_def "bca"]
  rw [if_neg ?f]
  case f => sorry
  simp [M.mul_def "bcaa"]
  rw [if_neg ?f]
  case f => sorry
  decide

[Johan Commelin]

Is there an easy interface somewhere to check if a (non)-implication is known already? Or do I need to install some tools?

[David Renshaw]

@Nicholas Carlini's new web page should have that information: https://nicholas.carlini.com/tmp/view.html

[David Renshaw]

that webpage seems to indicate that it is still "unknown"

[Nicholas Carlini]

(I'll try to get this committed soon, so that we can have a better source of truth and not "hope nicholas has fetched recently")

[Johan Commelin]

The same magma also show:

/-- `M` does not satisfy 270 -/
example : ∃ (x y : M), x ≠ ((y * x) * x) * x := by
  exists "a", "b"
  simp [M.mul_def "b"]
  rw [if_neg ?f]
  case f => decide
  simp [M.mul_def "ba"]
  rw [if_neg ?f]
  case f => decide
  simp [M.mul_def "baa"]
  rw [if_neg ?f]
  case f => sorry
  decide

[Nicholas Carlini]

This is a very clever magma... I should try to brute force over ones like this.

[Johan Commelin]

Here's a similar one, which should also lead to a bunch of open counterexamples.

abbrev N : Type := String

def N.mul (a b : N) : N :=
  let x := a.take (a.length / 4)
  if a == (x ++ x ++ x ++ x) then x else a ++ b

infixl:70 " + " => N.mul

theorem N.add_def (a b : N) : a + b =
  let x := a.take (a.length / 4)
  if a == (x ++ x ++ x ++ x) then x else a ++ b := rfl

@[simp]
theorem N.empty_add (b : N) : "" + b = "" := by
  rw [N.add_def, if_pos]
  decide
  decide

/-- `N` satisfies 3051 -/
example (x y : N) : x = (((x + x) + x) + x) + y := by
  by_cases h : x == ""
  · simp_all
  rw [N.add_def x x, if_neg ?f]
  case f => sorry
  rw [N.add_def (x ++ x) x, if_neg ?f]
  case f => sorry
  rw [N.add_def (x ++ x ++ x) x, if_neg ?f]
  case f => sorry
  rw [N.add_def, if_pos ?t]
  case t => sorry
  sorry

[Johan Commelin]

I guess I shouldn't use String but List Nat or something like that...

[Nicholas Carlini]

Johan Commelin said:

I guess I shouldn't use String but List Nat or something like that...

If it works...

[Terence Tao]

I put these magmas into https://teorth.github.io/equational_theories/blueprint/sect0005.html (where they should appear in a few minutes if CI passes; hopefully I have interpreted the Lean code correctly/

[Johan Commelin]

The magma N does not satisfy 3051. I thought the remaining sorries were trivial. But they are actually false.

[Terence Tao]

I guess maybe I should remove that magma from the list of "magmas used to establish counterexamples" portion of the blueprint, then.

[Johan Commelin]

Yes please, sorry for the error

[Johan Commelin]

M still seems fine to me.

[Johan Commelin]

I will try to prove that one formally, later today

[Johan Commelin]

Switched to lists, now sorry-free

import equational_theories.AllEquations

abbrev M : Type := List Nat

def M.mul (a b : M) : M :=
  if a == b then b else
  if (b ++ b ++ b) <:+ a then b else a ++ b

infixl:70 " * " => M.mul

theorem M.mul_def (a b : M) : a * b =
  if a == b then b else
  if (b ++ b ++ b) <:+ a then b else a ++ b := rfl

@[simp]
theorem M.mul_self (a : M) : a * a = a := by
  simp [M.mul_def a a, if_pos]

/-- `M` satisfies 3102 -/
example (x y : M) : x = (((y * x) * x) * x) * x := by
  rw [M.mul_def y x]
  split
  next h => simp
  next h =>
  split
  next h => simp
  rw [M.mul_def (y ++ x) x]
  split
  next h => simp
  next h =>
  split
  next h => simp
  rw [M.mul_def (y ++ x ++ x) x]
  split
  next h => simp
  next h =>
  split
  next h => simp
  rw [M.mul_def _ x]
  split
  next h => simp
  next h =>
  rw [if_pos]
  simp only [List.append_assoc]
  exact List.suffix_append y (x ++ (x ++ x))

/-- `M` does not satisfy 3176 -/
example : ∃ (x y z : M), x ≠ (((y * z) * x) * x) * x := by
  exists [0], [1], [2]

/-- `M` does not satisfy 270 -/
example : ∃ (x y : M), x ≠ ((y * x) * x) * x := by
  exists [0], [1]

[Johan Commelin]

If someone wants to massage this into a PR, that's fine with me. I probably won't have time to do it.

[Terence Tao]

Opened equational#312 for this.

[Terence Tao]

Also opened equational#316 for a more general tool to make it easier for casual project contributors to create proofs of implications or anti-implications in the project format.