# Zulip Chat Archive

## 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,
rw add_right_inj at h,
contradiction },
{ 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