invalid nat.cases_on application

Stream: new members

[Julian Gilbey]

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]

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]

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]

@Julian Gilbey the line or.elim (L17) should be or.elim ih

[Kevin Buzzard]

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]

@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]

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

[Kenny Lau]

@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]

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]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Reid Barton]

Inequality world DLC

[Mario Carneiro]

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

[Edward Ayers]

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]

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]

(deleted)

[Kenny Lau]

@Julian Gilbey annotated tactics

[Julian Gilbey]

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]

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]

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

[Kenny Lau]

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

[Kevin Buzzard]

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]

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