Normalize tactic in NNG

Stream: general

[Kevin Buzzard]

I am thinking about adding some more computation/algorithm stuff to NNG. This won't be needed for my course so there's no urgency, but if it is relatively straightforward to teach people how to write a tactic which turns a NNG 2 into succ (succ 0) then I might be tempted to teach this; perhaps a more advanced tactic could even change 1 + 1 not into succ 0 + succ 0 but into succ (succ 0).

Anyway, all of this is moot right now because I don't have a clue how to do this myself. Here's some code from NNG:

/-- Our copy of the natural numbers called `MyNat`, with notation `ℕ`. -/
inductive MyNat where
| zero : MyNat
| succ : MyNat → MyNat
-- deriving BEq, DecidableEq, Inhabited

@[inherit_doc]
notation (name := MyNatNotation) (priority := 1000000) "ℕ" => MyNat
-- Note: as long as we do not import `Mathlib.Init.Data.Nat.Notation` this is fine.

namespace MyNat

instance : Inhabited MyNat where
  default := MyNat.zero

def myNatFromNat (x : Nat) : MyNat :=
  match x with
  | Nat.zero   => MyNat.zero
  | Nat.succ b => MyNat.succ (myNatFromNat b)

def natFromMyNat (x : MyNat) : Nat :=
  match x with
  | MyNat.zero   => Nat.zero
  | MyNat.succ b => Nat.succ (natFromMyNat b)

instance ofNat {n : Nat} : OfNat MyNat n where
  ofNat := myNatFromNat n

instance : ToString MyNat where
  toString p := toString (natFromMyNat p)

How do I go from here to a normalize tactic which turns a goal 2 + 2 \ne 5 into succ succ 0 + succ succ 0 \ne succ succ ... 0?
Note that I know how to write an instance of decidable equality so I can prove this by decide; but I want to play with some other ideas before I introduce this: once we're in this state then we can finish the goal with

  rw [add_succ, add_succ, add_zero] at h
  repeat apply succ_inj at h
  apply zero_ne_succ at h
  assumption

(at least once you have apply at, which we have in NNG)

[Damiano Testa]

Kevin, I have not yet tried to get this to work with your version of Nat, but that is probably not too hard. Is what is below close to what you are looking for?

import Lean.Elab.Tactic.Basic
import Lean.Meta.Tactic.Replace

open Lean Elab Tactic

def norml : Nat → Expr
  | 0     => .const ``Nat.zero []
  | n + 1 => .app (.const ``Nat.succ []) (norml n)

def litToExpr? : Literal → Option Expr
  | .natVal val => some (norml val)
  | _ => none

def toNorm (e : Expr) : Expr :=
e.replace fun
  | .lit l => litToExpr? l
  | _ => none

elab "normalize" : tactic => do
  replaceMainGoal [← (← getMainGoal).modifyTarget (return toNorm ·)]

open Nat
example : 2 + 2 ≠ 5 := by
  normalize
  /- Goal is
OfNat.ofNat (succ (succ zero)) + OfNat.ofNat (succ (succ zero)) ≠
  OfNat.ofNat (succ (succ (succ (succ (succ zero)))))
  -/
  trivial

If I understand correctly, the OfNats may be undesirable, but hopefully everything else is close and might be a starting point!

[Damiano Testa]

I now wonder if normalize is a typo for normalise :smile:

[Patrick Massot]

Kevin, looking at your code, I see you didn't use my trick of defining MyNat using only axioms so that you don't have accidental rfl. Did you end deciding you'll really teach rfl?

[Kevin Buzzard]

Oh I didn't write any of this stuff, Jon and/or Alex ported the entire game and then I started ripping up the levels but left the underlying infrastructure the same. rfl doesn't prove stuff like a + 0 = a because they somehow disabled it in another way. I don't know the details. I would be fine with making things more axiomatic: I have definitely made a conscious decision not to explain that x + 0 = x can be proved by rfl (and indeed for some reason it can't).

[Patrick Massot]

Maybe they changed a transparency setting.

[Patrick Massot]

Where is the repo again?

[Kevin Buzzard]

Erm...it's called NNG4...I just type that and my computer finds it (I'm in bed now and I can't look)

[Damiano Testa]

https://github.com/hhu-adam/NNG4

[Alexander Bentkamp]

Yes, Jon changed the transparency setting. And we still redefined Nat because the transparency setting alone didn't fully do the job. (Maybe some definitions on Nat are reducible?)