854 formalization experiment

Stream: Equational

[Michael Bucko]

I wrote this lemma today - for 854. @Mario Carneiro kindly reviewed the proof (thank you for that!), and says it's correct.

import Mathlib
import Lean

universe u
variable {α : Type u}
variable (op : α → α → α)

def associativity : Prop :=
  ∀ a b c : α, op a (op b c) = op (op a b) c

def idempotence : Prop :=
  ∀ a : α, op a a = a

def commutativity : Prop :=
  ∀ a b : α, op a b = op b a

lemma op_self_left (h_assoc : associativity op) (h_idem : idempotence op) :
  ∀ a b : α, op a (op a b) = op a b :=
λ a b =>
  calc
    op a (op a b) = op (op a a) b := by rw [←h_assoc a a b]
            _ = op a b          := by rw [h_idem a]

lemma op_self_right (h_assoc : associativity op) (h_idem : idempotence op) :
  ∀ a b : α, op (op a b) b = op a b :=
λ a b =>
  calc
    op (op a b) b = op a (op b b) := by rw [h_assoc a b b]
            _ = op a b          := by rw [h_idem b]

lemma op_cancel_right (h_assoc : associativity op) (h_idem : idempotence op) (h_comm : commutativity op) :
  ∀ x z : α, op z (op x z) = op x z :=
λ x z =>
  calc
    op z (op x z) = op z (op z x) := by rw [h_comm x z]
            _ = op (op z z) x := by rw [h_assoc z z x]
            _ = op z x         := by rw [h_idem z]
            _ = op x z         := by rw [h_comm z x]

lemma op_nested_eq (h_assoc : associativity op) (h_idem : idempotence op) (h_comm : commutativity op) :
  ∀ x y z : α, op (op y z) (op x z) = op (op x y) z :=
λ x y z =>
  calc
    op (op y z) (op x z) = op y (op z (op x z)) := by rw [h_assoc y z (op x z)]
            _ = op y (op x z)          := by rw [op_cancel_right op h_assoc h_idem h_comm x z]
            _ = op (op y x) z          := by rw [h_assoc y x z]
            _ = op (op x y) z          := by rw [h_comm y x]

lemma simplify_op_expression (h_assoc : associativity op) (h_idem : idempotence op) (h_comm : commutativity op) :
  ∀ x y z : α, op x (op (op y z) (op x z)) = op (op x y) z :=
λ x y z =>
  calc
    op x (op (op y z) (op x z)) = op x (op (op x y) z) := by rw [op_nested_eq op h_assoc h_idem h_comm x y z]
            _ = op (op x (op x y)) z         := by rw [h_assoc x (op x y) z]
            _ = op (op x y) z                 := by rw [op_self_left op h_assoc h_idem x y]

[Michael Bucko]

Naming is probably wrong and the simp tag is missing (perhaps more), but the proof works.

import Mathlib

lemma ramanujan_1729_one_mul_one_mul_self
  {α : Type u}
  (op : α → α → α)
  (e x y : α)
  (h_id : ∀ a, op e a = a ∧ op a e = a)
  (heq : e = y) :
  x = op y (op (op y x) y) := by
  have h_id_y : ∀ a, op y a = a ∧ op a y = a := by
    intro a
    rw [← heq]
    exact h_id a
  have hyx : op y x = x := (h_id_y x).1
  have hxy : op x y = x := (h_id_y x).2
  have h1 : op (op y x) y = x := by
    rw [hyx]
    rw [hxy]
  have h2 : op y (op (op y x) y) = x := by
    rw [h1]
    rw [hyx]
  exact h2.symm