COMBINATORIAL: Refute 1076 -> 47, 99, 151, 203, 255, 411, 614, 817, 1223, 1426, 1629, 1832, 2035, 2238, 2441, 2644, 2847, 3050, 3253, 3456, 3659, 3862, 4065, 4380

[teorth]

See https://leanprover.zulipchat.com/user_uploads/3121/HjHtBqq50xdgzG5RP6zmLBgh/Equation1076-corrected.pdf for a proof. The tasks are to

• Transfer Equation 1076 from Eqns1000_1999.lean to Equations.lean (leaving a commented out version in the former file);
• Add Equation 1076 to Chapter 2 of the blueprint;
• Add some version of the proof in the above discussion to the Asterix chapter of the blueprint (making a new section header if desired);
• Formalize the statement and proof of the theorem in Lean in the ManuallyProved folder;
• Update ManuallyProved.lean.
• Add the Lean file to the main equational_theories.lean file so that it is compiled by CI; and
• Add \lean and \leanok tags to the blueprint version of the proof.

[madvorak]

claim

[madvorak]

disclaim

[madvorak]

I failed.

Here are some of my unsuccessful attempts:

import Mathlib


-- Daniel Weber thanks!
lemma FreeAbelianGroup.of_inj {α : Type} (a b : α) :
    FreeAbelianGroup.of a = FreeAbelianGroup.of b ↔ a = b :=
  ⟨(FreeAbelianGroup.of_injective ·), congr_arg _⟩


namespace PaceNielsen

abbrev A : Type := FreeAbelianGroup ℤ
abbrev p : A := FreeAbelianGroup.of 0
abbrev q : A := FreeAbelianGroup.of 1
abbrev r : A := FreeAbelianGroup.of 2
abbrev s : A := FreeAbelianGroup.of 3

notation "∅" => (none : WithZero A)
notation "O" => (some 0 : WithZero A)

noncomputable def E₀ : A →₀ WithZero A :=
  fun₀
  | 0 => p
  | p => q
  | -q => r
  | q + r => O
  | q + r - p => s
  | p - q - r + s => - q - r

def ℰ : Set (A →₀ WithZero A) := fun E =>
  ∀ a b c : A, (E a = b ∧ E b = c) →
    ∃ d : A, E (a - c) = d ∧ E (c + d - a) = -a

lemma E₀inℰ : E₀ ∈ ℰ := by
  have hpq : p ≠ q := by simp [FreeAbelianGroup.of_inj]
  have hpr : p ≠ r := by simp [FreeAbelianGroup.of_inj]
  have hps : p ≠ s := by simp [FreeAbelianGroup.of_inj]
  have hqr : q ≠ r := by simp [FreeAbelianGroup.of_inj]
  have hqs : q ≠ s := by simp [FreeAbelianGroup.of_inj]
  have hrs : r ≠ s := by simp [FreeAbelianGroup.of_inj]
  have hp0 : p ≠ 0 := sorry
  have hq0 : q ≠ 0 := sorry
  have hr0 : r ≠ 0 := sorry
  have hs0 : s ≠ 0 := sorry
  intro a b c ⟨hab, hbc⟩
  rw [E₀] at hab
  /-if ha : a = p - q - r + s then
    rw [ha] at hab
    simp at hab
    sorry
  else-/
  if ha0 : a = 0 then
    rw [ha0] at hab
    have : (p : WithZero A) = (b : WithZero A) := by
      rw [←hab]
      clear hab
      --simp [FreeAbelianGroup.of_inj, *]
      sorry
    sorry
  else
    sorry

end PaceNielsen


namespace PaceNielsen_

abbrev A : Type := FreeAbelianGroup ℤ
abbrev p : A := FreeAbelianGroup.of 0
abbrev q : A := FreeAbelianGroup.of 1
abbrev r : A := FreeAbelianGroup.of 2
abbrev s : A := FreeAbelianGroup.of 3

def E₀ : Set (A × A) :=
{
  (0, p),
  (p, q),
  (-q, r),
  (q + r, 0),
  (q + r - p, s),
  (p - q - r + s, - q - r)
}

def isFun (X : Set (A × A)) : Prop :=
  ∀ x y z : A, (x, y) ∈ X ∧ (x, z) ∈ X → y = z

variable [∀ P, Decidable P] -- TODO get rid of

noncomputable def asFun (X : Set (A × A)) : A → Option A :=
  fun a : A => if hb : ∃ b, (a, b) ∈ X then hb.choose else none

lemma asFun_eq {X : Set (A × A)} (hX : isFun X) {a b : A} (hab : (a, b) ∈ X) : asFun X a = b := by
  have hba : ∃ b, (a, b) ∈ X := ⟨b, hab⟩
  simpa [asFun, hba] using hX _ _ _ ⟨hba.choose_spec, hab⟩

def ℰ : Set (Set (A × A)) := fun E =>
  isFun E ∧ E.Finite ∧
  ∀ a b c : A, (asFun E a = b ∧ asFun E b = c) →
    ∃ d : A, asFun E (a - c) = d ∧ asFun E (c + d - a) = some (-a) -- BTW `0-a` needs no `some`

lemma E₀inℰ : E₀ ∈ ℰ := by
  constructor
  · intro x y z ⟨hxy, hxz⟩
    simp [E₀] at *
    have h0p : 0 ≠ p := sorry
    have h0q : 0 ≠ -q := sorry
    have h0qr : 0 ≠ q + r := sorry
    have h0qrp : 0 ≠ q + r - p := sorry
    have h0pqrs : 0 ≠ p - q - r + s := sorry
    have hpq : p ≠ -q := sorry
    have hpqr : p ≠ q + r := sorry
    have hpqrp : p ≠ q + r - p := sorry
    have hppqrs : p ≠ p - q - r + s := sorry
    have hqqr : -q ≠ q + r := sorry
    have hqqrp : -q ≠ q + r - p := sorry
    have hqpqrs : -q ≠ p - q - r + s := sorry
    have hqrqrp : q + r ≠ q + r - p := sorry
    have hqrpqrs : q + r ≠ p - q - r + s := sorry
    have hqrppqrs : q + r - p ≠ p - q - r + s := sorry
    repeat cases' hxy with hxy hxy <;> repeat cases' hxz with hxz hxz <;> cc
  constructor
  · simp only [E₀]
    apply Set.toFinite
  · intro a b c ⟨hab, hac⟩
    simp only [E₀] at *
    simp [asFun] at hab hac
    obtain ⟨b', hab'⟩ := hab.choose -- lost connection between `b` and `b'`
    obtain ⟨c', hac'⟩ := hac.choose -- lost connection between `c` and `c'`
    sorry

/-- For each E ∈ ℰ, for each a ∈ A, there is an extension of E ∈ ℰ where
the function equation for the functional equation for h:=a will hold. -/
theorem theLemma {E : Set (A × A)} (hE : E ∈ ℰ) (a : A) :
    ∃ E' : Set (A × A), E ⊆ E' ∧ (
        ∃ fa : A, asFun E' a = some fa ∧
        ∃ ffa : A, asFun E' fa = some ffa ∧
        ∃ affa : A, asFun E' (a - ffa) = some affa ∧
        asFun E' (affa - (a - ffa)) = some (-a)
    ) := by
  sorry

end PaceNielsen_

Discussions about the first attempted method:
https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Finsupp-like.20partial.20function
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Finsupp.20and.20FreeAbelianGroup

[lyphyser]

claim

So far I managed to do this:

-- use a reasonable version instead of the Mathlib one that uses classical instead of DecidableEq
import equational_theories.Mathlib.Data.Finsupp.Defs
import equational_theories.Mathlib.Data.Finsupp.Notation
import equational_theories.Mathlib.Data.Finsupp.Basic

import Mathlib.Data.Finset.Basic
import Mathlib.Algebra.Group.WithOne.Defs

-- use a reasonable definition instead of the astronautic one in Mathlib
abbrev FreeAbelianGroup α := Finsupp α ℤ
def FreeAbelianGroup.of {α} [DecidableEq α] (x: α): FreeAbelianGroup α := Finsupp.single x 1

lemma FreeAbelianGroup.of_inj {α : Type} [DecidableEq α] (a b : α) :
    FreeAbelianGroup.of a = FreeAbelianGroup.of b ↔ a = b := by
  apply Finsupp.single_left_inj
  exact Int.one_ne_zero

namespace PaceNielsen

abbrev A : Type := FreeAbelianGroup ℤ
abbrev p : A := FreeAbelianGroup.of 0
abbrev q : A := FreeAbelianGroup.of 1
abbrev r : A := FreeAbelianGroup.of 2
abbrev s : A := FreeAbelianGroup.of 3

notation "∅" => (none : WithZero A)
notation "O" => (some 0 : WithZero A)

instance: DecidableEq (WithZero A) := (inferInstance: DecidableEq (Option A))

def f₀ : A →₀ WithZero A :=
  fun₀
  | 0 => p
  | p => q
  | -q => r
  | q + r => O
  | q + r - p => s
  | p - q - r + s => - q - r

def ℰ : Set (A →₀ WithZero A) := fun f =>
  ∀ (a b c : A) (_: f a = b) (_: f b = c),
    ∃ d : A, f (a - c) = d ∧ f (d - (a - c)) = -a

lemma f₀inℰ : f₀ ∈ ℰ := by
  intro a b c hab hbc
  rw [f₀] at hab
  simp only [Finsupp.single, WithZero.coe_ne_zero, ↓reduceIte, Pi.single, Finsupp.coe_update,
    Function.update, eq_rec_constant, Finsupp.coe_mk, Pi.zero_apply, dite_eq_ite] at hab
  repeat' split at hab
  any_goals subst_eqs
  map_tacs [use s; use r]
  all_goals
    simp [f₀, Function.update, Finsupp.single, Pi.single]
    constructor
    all_goals
      repeat' split
      any_goals
        first
        | trivial
        | norm_cast

def foo := 0

instance {α} [Sub α]: Sub (WithZero α) where
  sub := Option.liftOrGet (· - ·)

lemma sub_coe {α} [Sub α] {x y: α}: ((↑x: WithZero α) - (↑y: WithZero α): WithZero α) = ↑(x - y) := by
  rfl

abbrev fup {α} (f: α →₀ WithZero α): WithZero α → WithZero α := λ x: WithZero α ↦
  match x with
  | (0: WithZero α) => (0: WithZero α)
  | Option.some x => f x

@[simp]
lemma fup_coe {α} {f: α →₀ WithZero α} {x: α}: fup f ↑x = f x := by
  unfold fup
  split
  · injections
  · injections
    subst_eqs
    rfl

abbrev feq (f: A →₀ WithZero A) (h: A) :=
  let f := fup f
  f ((f (h - f (f h))) - (h - f (f h))) = -h

def feq_of_mem_ℰ {f: A →₀ WithZero A} (h: f ∈ ℰ) {a b c: A} (ha: f a = b) (hb: f b = c): feq f a := by
  unfold ℰ at h
  rw [Set.mem_def] at h
  obtain ⟨d, h1, h2⟩ := h a b c ha hb
  simp [feq, fup_coe, sub_coe, ha, hb, h1, h2]

/-- For each E ∈ ℰ, for each a ∈ A, there is an extension of E ∈ ℰ where
the function equation for the functional equation for h:=a will hold. -/
theorem theLemma {f} (hf : f ∈ ℰ) (a : A) :
    ∃ f' ∈ ℰ, f.graph ⊆ f'.graph ∧ feq f a := by
  cases ha: (f a)
  next =>
    sorry
  next b =>
    cases hb: (f b)
    next =>
      sorry
    next c => 
      use f
      constructorm* _ ∧ _
      · exact hf
      · rfl
      · apply feq_of_mem_ℰ hf ha hb

[madvorak]

I cannot find:

import equational_theories.Mathlib.Data.Finsupp.Defs
import equational_theories.Mathlib.Data.Finsupp.Notation
import equational_theories.Mathlib.Data.Finsupp.Basic

Do you have a branch I could checkout?

[lyphyser]

It's a copy of the ones in Mathlib that I changed so that functions are computable because it uses DecidableEq instead of classical (which I think is not actually necessary, but I didn't really like having noncomputable everywhere). Another perhaps better alternative could be to equip HashMaps with a group structure. I mode more progress, maybe today or tomorrow I'll finish it.

EDIT: I changed to code to use DFinsupp, which is a far better solution

[teorth]

By the way, if this task is completed, it is likely that the same code can be modified to obtain 39 further anti-implications (80 net anti-implications after duality). Here is the graph of all the conjectural anti-implications stemming from 1076. 3 is the easiest to refute, but the others should be doable also (ones should focus on the conclusions at the top of the Hasse diagram for maximum efficiency).

EDIT: See https://leanprover.zulipchat.com/user_uploads/3121/BhQY4EgOsd2sQ7uWCWJwDR5d/Equation1076.pdf for more details.

[lyphyser]

disclaim

I have formalized everything except the case 1 check and constructing the final function based on extensions, but don't have time to finish. I posted my current progress in #577