Sublist contradiction, can't use induction

Stream: new members

[Yakov Pechersky]

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]

induction' seems ok here

[Eric Wieser]

cases also works fine

[Yakov Pechersky]

induction' has the first goal as unprovable I think

[Eric Rodriguez]

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

[Eric Rodriguez]

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

[Eric Rodriguez]

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]

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]

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]

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]

Where the magic is in src#list.eq_of_sublist_of_length_eq