Zulip Chat Archive

Stream: new members

Topic: invalid nat.cases_on application


view this post on Zulip 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!

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Oct 28 2019 at 15:27):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Oct 28 2019 at 15:36):

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

view this post on Zulip 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/

view this post on Zulip 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.

view this post on Zulip Reid Barton (Oct 28 2019 at 15:43):

Inequality world DLC

view this post on Zulip 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

view this post on Zulip 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, _)

view this post on Zulip 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

view this post on Zulip Edward Ayers (Oct 28 2019 at 15:46):

(deleted)

view this post on Zulip Kenny Lau (Oct 28 2019 at 15:46):

@Julian Gilbey annotated tactics

view this post on Zulip 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!)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Oct 28 2019 at 15:54):

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

view this post on Zulip 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.

view this post on Zulip 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