data from constructor

Stream: lean4

[Elisabeth Bonnevier]

I have defined my own natural numbers and ≤ like so:

inductive le : MyNat → MyNat → Prop
  | zero_le : {n : MyNat} → le zero n
  | succ_le : {m n : MyNat} → le m n → le (succ m) (succ n)

I am now trying to prove that succ m ≤ succ n → m ≤ n. In words what I want to say is that succ m ≤ succ n must have been constructed by succ_le and that constructor requires a proof that m ≤ n, which we use as our proof that m ≤ n. How do I say this in Lean4?

[Sky Wilshaw]

You can use induction on your m ≤ n hypothesis.

[Sky Wilshaw]

I think in this case, cases might also work.

[Elisabeth Bonnevier]

I don't have m ≤ n as a hypothesis. That is my goal

[Sky Wilshaw]

Sorry, I meant the succ m ≤ succ n hypothesis.

[Sky Wilshaw]

Applying induction allows you to essentially solve the goal for all of the different ways an object could have been constructed. In your case, there's only one non-contradictory way to construct a proof of succ m ≤ succ n.

[Elisabeth Bonnevier]

It worked with cases. Thank you! :pray:

[Kevin Buzzard]

This was one of the candidate definitions for <= in the natural number game but tests indicated that people found doing induction on inequalities too confusing! I do think it's a beautiful approach but IIRC it was quite hard to verify the standard axioms for <= on nat using it (maybe antisymmetry was hard?)