cases on list defined by `let`

Stream: general

[Kevin Buzzard]

I've always been a bit freaked out by let. I usually use set and it's fine, but I found an example where I can't use it. I also managed to get the tactic exfalso to fail, which is certainly a first for me.

import data.nat.prime -- or anything which has a function which returns a list

#check nat.factors
-- nat.factors : ℕ → list ℕ

-- I want to do induction on a list which depends on n
example (n : ℕ) : false :=
begin
  set l := n.factors with hl,
  cases l, -- error
/-
induction tactic failed, failed to create new goal
state:
n : ℕ,
l : list ℕ := nat.factors n,
hl : l = nat.factors n
⊢ false
-/
end

example (n : ℕ) : false :=
begin
  let l := n.factors,
  cases l,
  { -- ⊢ (let l : list ℕ := nat.factors n in false) list.nil
    exfalso, -- error
/-
contradiction tactic failed
-/
  },
  sorry
end

example (n : ℕ) : false :=
begin
  cases n.factors,
  -- works but no assumption n.factors = nil in context
end

I was thinking about the prime factor question in #new members and I wanted to do cases on whether the list of factors had 0, 1, or more than 1 element. I tried induction on length but in the case where the length was >= 2 I couldn't extract the first two elements for reasons such as the above. What am I doing wrong?

[Kevin Buzzard]

I know there will be some goofy trick with the equation compiler but what if I'm in the middle of a tactic proof? [added later: actually, I can't even pull off the equation compiler trick, I want to do the old "match on rfl" thing...]

[Donald Sebastian Leung]

For your first example:

import data.nat.prime -- or anything which has a function which returns a list

#check nat.factors
-- nat.factors : ℕ → list ℕ

-- I want to do induction on a list which depends on n
example (n : ℕ) : false :=
begin
  set l := n.factors with hl,
  simp at *,
  cases l, -- error
/-
induction tactic failed, failed to create new goal
state:
n : ℕ,
l : list ℕ := nat.factors n,
hl : l = nat.factors n
⊢ false
-/
end

Adding simp at * before cases l seems to make it go through, but then both subgoals generated by cases have an explicit let binding under the line :sweat_smile: In fact, I don't even think that the generated subgoals are well-typed, e.g. (let l : list ℕ := nat.factors n in false) list.nil in the first subgoal should reduce to false list.nil which doesn't even make sense.

[Mario Carneiro]

The subgoals are probably well typed but the pretty printer is getting confused and not showing something like a lambda with an implicit argument