accessing the source case during induction

Stream: Is there code for X?

[Jared green]

im trying to do induction over length of a list.

variable (p : List a -> Prop)
theorem t  (n : List a) (hn : n ≠ []): p n :=
  let m := n.length
  induction' m with m m' ih
  --i should be able to get a contradiction here
  ...

i could have done this another way, but p calls head n hn in my code so hn has to be a variable

[Etienne Marion]

Your code does not work in the playground, please post a #mwe.

[Aaron Liu]

Do you want something like this?

def List.recNeNil {α : Type u} {motive : (l : List α) → l ≠ [] → Sort v}
    (singleton : ∀ x, motive [x] (List.cons_ne_nil x []))
    (cons : ∀ x xs hxs, motive xs hxs → motive (x :: xs) (List.cons_ne_nil x xs))
    (l : List α) (hl : l ≠ []) : motive l hl :=
  match l with
  | [x] => singleton x
  | x :: y :: xs =>
    cons x (y :: xs) (List.cons_ne_nil y xs)
      (List.recNeNil singleton cons (y :: xs) (List.cons_ne_nil y xs))

variable (p : List a → Prop)
example (n : List a) (hn : n ≠ []) : p n := by
  induction n, hn using List.recNeNil with
  | singleton x => sorry
  | cons x xs hxs ih => sorry

[Riccardo Brasca]

This is basically the same as Aaron's answer, but depending on what you are doing precisely you can use directly strucutral induction, without introducing a new theorem.

import Mathlib

variable {a : Type*} (p : List a -> Prop)

theorem t  (n : List a) (hn : n ≠ []): p n :=
match n, hn with
| x::L, _ => by
  by_cases hL : L = []
  · simp [hL] --singleton case
    sorry
  have := t L hL --now `this` is a proof of `p L` and you have to prove `p (x::L)`
  sorry

[Giacomo Stevanato]

Jared green said:

theorem t (n : List a) (hn : n ≠ []): p n

This is saying that if you have a list, and it's not empty, then any property holds for it. This seems clearly false to me, so you probably won't be able to find a proof for it.

[Jared green]

it would be more like this

variable (p q : List a -> Prop)
theorem t  (n : List a) (hn : n ≠ []): (n.length > 1 -> q n -> ∃ l : List a, l.length = n.length - 1 ∧ q l ∧ (p l -> p n) ) -> (length n = 1 -> q n -> p n) -> q n -> p n :=
  let m := n.length
  induction' m with m m' ih
  --i should be able to get a contradiction here
  ...

[Jared green]

and, l is not necessarily (tail n)

[Kyle Miller]

With your original example, you can give n.length as an induction target directly. Using let causes it to not know that m is the length.

You can also use h : syntax to introduce the necessary hypothesis to make use of n.length in each case.

variable (p : List a -> Prop)
theorem t  (n : List a) (hn : n ≠ []): p n := by
  induction' h : n.length with m m' ih
  · cases n <;> simp_all
  · sorry -- induction step

(The h : syntax should work with the let variable too.)

[suhr]

Two more versions of the same thing:

import Mathlib

variable (p : List a -> Prop)
example (n : List a) (hn : n ≠ []): p n := by
  suffices h: ∀l, n.length = l → p n from h n.length rfl
  intro l
  induction l with
  | zero => sorry       -- ⊢ n.length = 0 → p n
  | succ l ih => sorry  -- ⊢ n.length = l + 1 → p n

example (n : List a) (hn : n ≠ []): p n := by
  suffices h: ∀l, n.length = l → p n from h n.length rfl
  refine λl => l.recOn
    (λh: n.length = 0 => ?zero)
    (λl (ih: n.length = l → p n)(h: n.length = l.succ) => ?succ)
  case zero => cases n <;> simp_all
  case succ => sorry

Note that the last version does not require you to know much about tactics... If you mastered terms, you always find a way.

[Kyle Miller]

@suhr Can I ask why you are preferring to write suffices/intro instead of generalize?

import Mathlib

variable (p : List a -> Prop)
example (n : List a) (hn : n ≠ []): p n := by
  generalize h : n.length = l
  induction l with
  | zero => sorry       -- h : n.length = 0 ⊢ p n
  | succ l ih => sorry  -- h : n.length = l + 1 ⊢ p n

(Note: in the next lean release, we will be able to write induction h : n.length with to have the same effect.)

[suhr]

I often write proofs in term mode, and suffices is both a term and a tactic. And I just forgot that generalize exists.
The proof indeed looks nicer with generalize.