Unexpected behavior of simp

Stream: lean4

[Brandon Brown]

I don't understand why the simplifier works on the first example but not the second.

inductive int : Type where
| zero : int
| succ : int → int
| pred : int → int
open int
@[simp] axiom e1 : {a : int} → succ (pred a) = a

example (a : int) : succ (pred a) = a := by simp -- this works
example : succ (pred zero) = zero := by simp -- error

In Lean3 the equivalent code works just fine

[Daniel Selsam]

The error is just that it has reduced your goal to False (your axiom is unsound)

[Brandon Brown]

But then why does it work in Lean3? I just want to stipulate that succ (pred a) = a for my type int

[Daniel Selsam]

What do you mean by 'work'? Lean4's simplifier is doing you a favor by reducing the goal to False:

example (h : succ (pred zero) = zero) : False := by simp at h

[Daniel Selsam]

@[simp] axiom e1 (a : int) : succ (pred a) = a
example : False := by have h := e1 zero; simp at h

[Yakov Pechersky]

You have to make a new quotient type where succ (pred a) ≈ a

[David Renshaw]

#check (Eq.mp (eqFalse' fun (h : succ (pred zero) = zero) => int.noConfusion h) (@e1 zero))

False

[Brandon Brown]

Interesting. So Lean3 is just not telling me my axiom is inconsistent and Lean4 is being more helpful in this case? Regarding quotient type, in this case I don't want a quotient type, I just want int with a stipulation that succ (pred a) = a by definition so that anywhere i have an int I can simplify it. I can do this by

inductive int : Type where
| zero : int
| succ : int → int
| pred : int → int
open int

variable (e1 : {a : int} → succ (pred a) = a)

example (a : int) : int.succ (int.pred a) = a := by rw [e1]
example : int.succ (int.pred int.zero) = int.zero := by rw [e1]

But then I can't tag a variable with @[simp]

[Scott Morrison]

I think you're just confused about what it means to "stipulate" something here. succ (pred a) = a lets you prove false, whether you get it as an axiom or a hypothesis. You need quotient types to do this.

[Daniel Selsam]

^ or to represent your type so that every int has a unique syntactic representation, and then define succ and pred on top of that

[Brandon Brown]

I see - yes I misunderstood; thanks. So my real interest was in trying to emulate a higher-inductive type because there's an elegant (appearing) definition of the integers a higher inductive type, where it appears you just get to define the equalities within the inductive type definition. But I guess there's no way emulate that.