# Zulip Chat Archive

## Stream: new members

### Topic: invalid nat.cases_on application

#### Julian Gilbey (Oct 28 2019 at 14:47):

Hi, I'm just getting my head around Lean 3, and working through the Logic and Proof book on the Lean github page. I'm trying to prove that \le is a total order on the naturals, but my code gives an error which I'm struggling to make sense of. Any help would be much appreciated! The code is below. (Yes, I know my coding style is very rudimentary, and I haven't yet learnt how to use rw effectively. I'll get there! Any pointers in that direction would be helpful, but in the meantime, what is this bizarre error? It would be good to have a "minimal example", but I don't know how to trim this one down, I'm afraid.)

The error message reads:

error: invalid 'nat.cases_on' application, elaborator has special support for this kind of application (it is handled as an "eliminator"), but expected type must not contain metavariables ?m_1

and here is my code:

open nat -- we define ≼ to mean less than or equal to, using the following definition -- rather than the inductive definition lean uses; yes, they're equivalent, -- but let's see how this one goes! def leq (a b : nat) := ∃ c : nat, a + c = b infix ` ≼ `:50 := leq theorem ineq_totality : ∀ m n : nat, n ≼ m ∨ m ≼ n := assume m n, nat.rec_on n (have h : 0 + m = m, by rw zero_add, have hi : 0 ≼ m, from exists.intro m h, show 0 ≼ m ∨ m ≼ 0, from or.inl hi) (assume n, assume ih : n ≼ m ∨ m ≼ n, or.elim (assume h1 : n ≼ m, exists.elim h1 $ assume c (hc : n + c = m), nat.cases_on c (have he : succ m = succ n, by calc succ m = succ(n + 0) : by rw eq.subst (eq.symm hc) ... = succ n : rfl, have hi : m ≼ succ n, from exists.intro 1 he, show succ n ≼ m ∨ m ≼ succ n, from or.inr hi) (assume c, have he : succ n + c = m, by calc succ n + c = succ (n + c) : by rw succ_add ... = succ (c + n) : by rw add_symm ... = succ c + n : by rw succ_add ... = n + succ c : by rw add_symm ... = m : by rw hc, have hi : succ n ≼ m, from exists.intro c he, show succ n ≼ m ∨ m ≼ succ n, from or.inl hi)) (assume h1 : m ≼ n, exists.elim h1 $ assume c (hc : m + c = n), have he : m + succ c = succ n, by calc m + succ c = succ (m + c) : by rw succ_add ... = succ n : by rw h, have hi : m ≼ succ n, from exists.intro c he, show succ n ≼ m ∨ m ≼ succ n, from or.inr hi))

Many thanks!

#### Bryan Gin-ge Chen (Oct 28 2019 at 15:15):

The step where you use `or.elim`

looks wrong to me. If I insert `by {}; exact`

before `or.elim`

(a handy trick from @Mario Carneiro to inspect the goal in "term-mode" proofs), I see:

1 goal m n n : ℕ, ih : n ≼ m ∨ m ≼ n ⊢ succ n ≼ m ∨ m ≼ succ n

~~But ~~`or.elim`

has type `∀ {a b c : Prop}, a ∨ b → (a → c) → (b → c) → c`

which doesn't clear something like this. Naïvely, you would want to use `or.inl`

or `or.inr`

instead. But in fact that won't work because you don't know which case you're in. So I think you need to apply classical logic somewhere, maybe `classical.em : ∀ (p : Prop), p ∨ ¬p`

.

~~(Not sure about this, but I think the error appears because Lean introduces a metavariable when trying to unify the ~~`or.elim`

stuff with the goal and these aren't allowed in the goal when you use `nat.cases_on`

.)

**Edit**: whoops, I was way off. Sorry, see the messages below!

#### Kevin Buzzard (Oct 28 2019 at 15:23):

This is just horrible. Beginners writing their proofs with all that have, show, assume stuff. Tactic mode is absolutely the canonical way to prove something like this. This exercise makes a beginner think that using a theorem prover is hell.

#### Kenny Lau (Oct 28 2019 at 15:27):

@Julian Gilbey the line `or.elim`

(L17) should be `or.elim ih`

#### Kevin Buzzard (Oct 28 2019 at 15:27):

import tactic.interactive -- mathlib tactics open nat -- we define ≼ to mean less than or equal to, using the following definition -- rather than the inductive definition lean uses; yes, they're equivalent, -- but let's see how this one goes! def leq (a b : nat) := ∃ c : nat, a + c = b infix ` ≼ `:50 := leq theorem ineq_totality : ∀ m n : nat, n ≼ m ∨ m ≼ n := begin intro m, induction m with d hd, { -- base case intro n, right, use n, simp, }, { -- inductive step, intro n, cases n with n', left, use succ d, simp, cases hd n', left, cases h with e he, use e, simp [he, add_succ], right, cases h with e he, use e, simp [he, add_succ], } end

#### Kevin Buzzard (Oct 28 2019 at 15:27):

@Julian Gilbey the real problem is that the entire thing should be in tactic mode so you can see what you're doing.

#### Kevin Buzzard (Oct 28 2019 at 15:28):

Check out chapter 5 of Theorem Proving In Lean to get you out of this assume, show, have hell.

#### Kenny Lau (Oct 28 2019 at 15:32):

@Julian Gilbey and if you insist using term mode you can use some syntactic sugars to make it look nicer:

open nat -- we define ≼ to mean less than or equal to, using the following definition -- rather than the inductive definition lean uses; yes, they're equivalent, -- but let's see how this one goes! def leq (a b : nat) := ∃ c : nat, a + c = b infix ` ≼ `:50 := leq theorem ineq_totality : ∀ m n : nat, n ≼ m ∨ m ≼ n | m 0 := or.inl ⟨m, nat.zero_add m⟩ | m (n+1) := match ineq_totality m n with | or.inl ⟨0, hc⟩ := or.inr ⟨1, by rw [← hc, nat.add_zero n]⟩ | or.inl ⟨c+1, hc⟩ := or.inl ⟨c, by rw [nat.add_assoc, nat.add_comm 1 c, hc]⟩ | or.inr ⟨c, hc⟩ := or.inr ⟨c+1, by rw [← nat.add_assoc, hc]⟩ end

#### Julian Gilbey (Oct 28 2019 at 15:35):

This is just horrible. Beginners writing their proofs with all that have, show, assume stuff. Tactic mode is absolutely the canonical way to prove something like this. This exercise makes a beginner think that using a theorem prover is hell.

Yes, quite! And I am a complete beginner :rolling_on_the_floor_laughing: So I'm looking forward to learning tactic mode!

#### Julian Gilbey (Oct 28 2019 at 15:35):

Julian Gilbey the line

`or.elim`

(L17) should be`or.elim ih`

Thanks! And then I can correct my remaining errors which now appear...

#### Kevin Buzzard (Oct 28 2019 at 15:35):

In tactic mode you can see all goals at all times and exactly what you are assuming.

#### Kevin Buzzard (Oct 28 2019 at 15:36):

Let me stress that this is not your fault! This is just the method that Avigad uses to teach people, perhaps because it's more suited to the kind of elementary questions that beginner CS people have.

#### Kevin Buzzard (Oct 28 2019 at 15:36):

But you're working on a very natural maths question so you should try tactic mode.

#### Kevin Buzzard (Oct 28 2019 at 15:37):

I think this question is somewhere in world 5 on http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/

#### Kevin Buzzard (Oct 28 2019 at 15:37):

oh no it's not quite there yet. It's coming up in v1.1, to be released this weekend.

#### Reid Barton (Oct 28 2019 at 15:43):

Inequality world DLC

#### Mario Carneiro (Oct 28 2019 at 15:45):

I think the use of this style in Jeremy's proofs reflects influence from the Isar proofs in Isabelle

#### Edward Ayers (Oct 28 2019 at 15:45):

If you really really want to use `cases_on`

: The error comes from the fact that the elaborator can't figure out the motive because it doesn't appear in the type signature. You need to perform `cases_on`

*before* `assume (hc : n + c = m)`

so that `c`

can be replaced by zero or `succ c`

in the two case branches.

assume c, @nat.cases_on (λ c, n + c = m → succ n ≼ m ∨ m ≼ succ n) c (assume h, _) (assume c h, _)

#### Kenny Lau (Oct 28 2019 at 15:46):

import tactic.interactive open nat -- we define ≼ to mean less than or equal to, using the following definition -- rather than the inductive definition lean uses; yes, they're equivalent, -- but let's see how this one goes! def leq (a b : nat) := ∃ c : nat, a + c = b infix ` ≼ `:50 := leq theorem ineq_totality : ∀ m n : nat, n ≼ m ∨ m ≼ n := begin -- The goal is ∀ so we intro everything. intros m n, -- We do induction on n. induction n, -- Now there are two cases. case nat.zero { -- The goal is ∨ and we know that the left one is true. left, -- The goal is 0 ≼ m but is secretly an ∃ so I use m. use m, -- The goal is 0 + m = m which we know is nat.zero_add. exact nat.zero_add m }, -- Now we go to the second case. case nat.succ : n ih { -- We case on ih. cases ih, -- We now have two cases. case or.inl : h1 { -- h1 says n ≼ m but is secretly an ∃ so we cases on it. cases h1 with c hc, -- We case on c instead of induction because we don't need an induction hypothesis. cases c, -- Now we have two cases. case nat.zero { -- The goal is ∨ and the right hand side is true. right, -- The goal is m ≼ succ n but is secretly an ∃. use 1, -- From n + 0 = m we readily derive m + 1 = succ n. rw [← hc, nat.add_zero n] }, -- We proceed to the second case. case nat.succ : c { -- The goal is ∨ and the left hand side is true. left, -- The goal is succ n ≼ m but is secretly an ∃. use c, -- From n + succ c = m we readily derive succ n + c = m. rw [← hc, nat.succ_add] } }, -- We are now in the second case. case or.inr : h1 { -- h1 says m ≼ n but is secretly an ∃. cases h1 with c hc, -- The goal is ∨ and the right hand side is true. right, -- The goal is m ≼ succ n but is secretly and ∃. use c+1, -- From m + c = n we readily derive m + (c + 1) = succ n. rw [← hc, ← nat.add_assoc] } } end

#### Edward Ayers (Oct 28 2019 at 15:46):

(deleted)

#### Kenny Lau (Oct 28 2019 at 15:46):

@Julian Gilbey annotated tactics

#### Julian Gilbey (Oct 28 2019 at 15:50):

Julian Gilbey annotated tactics

Wow, thanks! This will take some getting used to... chapter 5, here I come (or at least once I've finished my marking and the paper I'm drafting!)

#### Kevin Buzzard (Oct 28 2019 at 15:50):

Thanks Kenny! Julian -- I hope this is giving you some indication that this sort of question can actually be worked on in Lean using a much easier-to-use framework than the one you are attempting to use, where 9 times out of 10 the error is "missing comma" and the user never recovers

#### Mario Carneiro (Oct 28 2019 at 15:54):

To counter Kevin's negativity, I would like to say that your initial proof is very nicely formatted

#### Kenny Lau (Oct 28 2019 at 15:54):

Also you can also always see the goals in term mode by using underscores

#### Kevin Buzzard (Oct 28 2019 at 15:55):

All this is true, but it's still completely impossible for a beginner to debug. That's why he's asking the question in the first place.

#### Bryan Gin-ge Chen (Oct 28 2019 at 16:06):

Ah, I answered way too hastily. :face_palm:♂️ Sorry for posting nonsense and thanks to everyone else for jumping in with great explanations!

Last updated: May 11 2021 at 00:31 UTC