## Stream: new members

### Topic: Sublist contradiction, can't use induction

#### Yakov Pechersky (Jul 14 2022 at 15:32):

Why does induction leave an unprovable goal here?

import data.list.basic

variables {α : Type*}

lemma cons_ne_sublist (x : α) (xs : list α) :
¬ x :: xs <+ xs :=
begin
intro h,
induction h,
{ sorry }, -- what happened here?
{ assumption },
{ assumption }
end

lemma cons_ne_sublist' (x : α) (xs : list α) :
¬ x :: xs <+ xs :=
begin
rintro ⟨⟩,
-- only 2 cases as expected
sorry,
sorry,
end


#### Eric Wieser (Jul 14 2022 at 15:39):

induction' seems ok here

#### Eric Wieser (Jul 14 2022 at 15:40):

cases also works fine

#### Yakov Pechersky (Jul 14 2022 at 15:42):

induction' has the first goal as unprovable I think

#### Eric Rodriguez (Jul 14 2022 at 15:50):

seems induction forgets to check whether slnil is actually a possible introduction... yikes. rintro <> has some extra no_confusion stuff

#### Eric Rodriguez (Jul 14 2022 at 15:53):

is this posdsible to write with the equation compiler? I've been trying and failing at that

#### Eric Rodriguez (Jul 14 2022 at 15:54):

lemma cons_ne_sublist (x : α) (xs : list α) :
¬ x :: xs <+ xs :=
begin
cases xs,
sorry,
intro h,
induction h,
end


shows an even more obvious nonsense

#### Patrick Johnson (Jul 14 2022 at 16:06):

Yakov Pechersky said:

induction' has the first goal as unprovable I think

The goal is provable:

import tactic
import tactic.induction
import data.list.basic

variables {α : Type*}

lemma cons_ne_sublist {x : α} {xs : list α} : ¬x :: xs <+ xs :=
begin
intro h,
induction' h,
{ replace h := h.antisymm (list.sublist_of_cons_sublist (list.sublist_cons _ _)),
apply_fun list.length at h,
simp_rw list.length at h,
change xs.length + 2 = xs.length + 0 at h,
{ assumption },
end


#### Patrick Johnson (Jul 14 2022 at 16:10):

Of course, this is silly because proving the first goal requires proving the original statement, so induction is not the right path here. But the point is that the goal is indeed provable.

#### Yakov Pechersky (Jul 14 2022 at 17:04):

Thanks!

import data.list.basic

variables {α : Type*}

open list

lemma cons_not_sublist (x : α) (xs : list α) :
¬ x :: xs <+ xs :=
begin
intro h,
suffices : x :: xs = xs,
{ exact cons_ne_self _ _ this },
exact h.antisymm (sublist_cons _ _)
end


#### Yakov Pechersky (Jul 14 2022 at 17:05):

Where the magic is in src#list.eq_of_sublist_of_length_eq

Last updated: Dec 20 2023 at 11:08 UTC