Induction over list whose size is guaranteed to be 1?

Stream: new members

[fkefjlwejlfk]

hey all,

I want to keep this question high level because a #mwe would still get quite extensive.
Somewhere in one of my proofs, I want to perform induction on a list that is generate by method foo. This base case will be list.nil. However, say that I have a lemma that proves foo will never generate an emtpy list, but always a list of at least size one. I want my base case to not be the empty list, but a list of size one. Is there a way to do this?

[Kyle Miller]

You could do cases on the list first before doing induction on its tail in the second case.

[fkefjlwejlfk]

Kyle Miller said:

You could do cases on the list first before doing induction on its tail in the second case.

But if I do this, I also must provide a proof for the first case where the list is equal to nil. In my example this proof is not possible. I have a lemma that proves this base case will never happen.

[Kyle Miller]

Yeah, in the first goal that cases produces, you provide that proof

[Kyle Miller]

This cases/induction pair sets up an induction hypothesis where the list is non-nil.

[fkefjlwejlfk]

Kyle Miller said:

Yeah, in the first goal that cases produces, you provide that proof

Maybe I am misunderstanding. Say xs is the list generated by foo. When I perform cases on foo, I then expect a hypothesis of x = list.nil to appear in my environment. If it did, I could use my lemma to proof by contradiction. However, x = list.nil never appears in my environement. Is there something im missing?

[Kyle Miller]

A #mwe would be really helpful here. If you need that equality, then just so you know there is cases h : xs and induction h : xs syntax

[Kyle Miller]

You can also use something like tactic#set to set up an equality before you start your cases. (Edit: no, I forgot it creates a let binding so that doesn't work here tactic#generalize is fine though.)

[Kyle Miller]

Here's my attempt at a #mwe given your description, but if it doesn't apply to your situation maybe you could tweak it.

import tactic

def foo : list ℕ := [37]

lemma foo_ne_empty : foo ≠ [] := by { intro h, cases h }

lemma baz (p : Prop) : p :=
begin
  generalize h : foo = xs,
  cases xs with x xs,
  { exfalso, exact foo_ne_empty h },
  induction xs,
  -- and so on
end

[Kyle Miller]

I have baz proving an arbitrary p just to have a goal that can't be proved, which means I have to handle the first case in a realistic way.

[Kyle Miller]

That generalize can be merged into the cases syntax:

lemma baz (p : Prop) : p :=
begin
  cases h : foo with x xs,
  { exfalso, exact foo_ne_empty h },
  induction xs,
  -- and so on
end

[fkefjlwejlfk]

Thank you!