Code review / What (things) am I doing wrong

Stream: new members

[Chris Ahn]

I've been trying to write up the structure defined here; more specifically I've almost finished writing up a proof that addition is in fact a commutative monoid except for one case in add_comm (the code is at the bottom of the post).

The main problem I am having is that for some reason simp/rw is unable to find the instances of monoidNPlus2.add_zero even though it seems "obvious" where it should be applied. I have marked the relevant position in code with a sorry.

There are some other things obviously wrong with this: currently I'm using unfold_projs unfold addAux as a bad way of only expanding out the addition of NPlus2, since using simp [HAdd.hAdd] also expands out natural addition, which makes it impossible to apply Nat lemmas. I'm sure there's a more proper way to do this but for some reason I have been unable to find it.

Additionally, I'm unsure about how case based proofs are usually structured in lean: I tried building up the proof with pattern matching but it seemed that lean was unable to deduce basic facts such as a ≠ 0 in certain branches.

If anyone has some time to look over this example I would appreciate it greatly. If there are any other errors/unorthodox constructions apart from those pointed out above I would also appreciate feedback on those. (I am aware the names of lemmas do not exactly follow conventions but as this is more of a personal working draft I have not taken great care in naming them).

import Mathlib.Data.ZMod.Basic
import Mathlib.RingTheory.Subsemiring.Basic
import Mathlib.Algebra.Order.Monoid.Basic
import Mathlib.Algebra.Ring.Basic

inductive NPlus2
  | two'
  | nat: ℕ → NPlus2
  deriving DecidableEq

namespace NPlus2

instance : Zero NPlus2 :=
  ⟨nat 0⟩

instance : One NPlus2 :=
  ⟨nat 1⟩

@[simp]
def aux1 : NPlus2 → ℕ
  | two' => 2
  | nat a => a

instance inhabited : Inhabited NPlus2 :=
  ⟨two'⟩

lemma aux1nat {n: ℕ}: aux1 (nat n) = n := by
  unfold aux1
  simp

@[simp]
lemma zero_eq : 0 = nat Nat.zero := by rfl

@[simp]
lemma one_eq : 1 = nat 1 := by rfl

def addAux: NPlus2 → NPlus2 → NPlus2
  | 0, x => x
  | x, 0 => x
  | a, b => nat (aux1 a + aux1 b)

instance monoidNPlus2 : AddCommMonoid NPlus2 where
  add := addAux
  zero_add a := by
    unfold_projs
    unfold addAux
    simp
  add_zero a := by
    unfold_projs
    unfold addAux
    by_cases ha: a = nat 0 <;> simp [ha]
  add_comm a b := by
    unfold_projs
    unfold addAux
    by_cases ha : a = nat 0 <;> {
      by_cases hb: b = nat 0 <;> {
        simp [ha, hb]
        try { ring }
      }
    }
  add_assoc a b c := by
    have lem1 {n: ℕ} : ¬(nat n = nat 0) ↔ ¬(n = 0) := by simp
    have lem2 {n m: ℕ} : ¬(n = 0) → ¬(n + m = 0) := by cases' m <;> simp
    by_cases ha: a = nat 0
    · unfold_projs
      unfold addAux
      simp [ha]
    · by_cases hb: b = nat 0
      · unfold_projs
        unfold addAux
        simp [hb]
      · by_cases hc: c = nat 0
        · rw [hc, ←zero_eq]
          simp [monoidNPlus2.add_zero]
          sorry
        · unfold_projs
          unfold addAux
          have ne_zero {n m: NPlus2}  (h: ¬(n = nat 0)) : ¬(nat (aux1 n + aux1 m) = nat 0) := by
            cases' n with n n
            · simp
            · simp only [aux1nat]
              rw [lem1] at *
              apply lem2 (m := aux1 m) at h
              exact h
          have ab_ne_zero: ¬(nat (aux1 a + aux1 b ) = nat 0) := ne_zero ha
          have bc_ne_zero: ¬(nat (aux1 b + aux1 c ) = nat 0) := ne_zero hb
          simp only [addAux, ab_ne_zero, bc_ne_zero, aux1nat, Nat.add_assoc]

[Matt Diamond]

What is semiNPlus2? I don't see it defined anywhere

[Chris Ahn]

Matt Diamond said:

What is semiNPlus2? I don't see it defined anywhere

Sorry I made a mistake while copying the code over, it was the old name of the AddCommMonoid instance

[Chris Ahn]

Have edited the post now