## Stream: new members

### Topic: Induction over list whose size is guaranteed to be 1?

#### fkefjlwejlfk (Jan 21 2023 at 16:37):

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 (Jan 21 2023 at 16:42):

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

#### fkefjlwejlfk (Jan 21 2023 at 16:44):

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 (Jan 21 2023 at 17:00):

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

#### Kyle Miller (Jan 21 2023 at 17:01):

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

#### fkefjlwejlfk (Jan 21 2023 at 17:17):

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 (Jan 21 2023 at 17:20):

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 (Jan 21 2023 at 17:22):

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 (Jan 21 2023 at 17:25):

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 (Jan 21 2023 at 17:26):

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 (Jan 21 2023 at 17:30):

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 (Jan 21 2023 at 19:59):

Thank you!

Last updated: Dec 20 2023 at 11:08 UTC