Problem with induction hypothesis

Stream: new members

[Marcus Rossel]

I'm using Lean 4 nightly 2022-01-04.

I don't understand the generated induction hypothesis in the following example:

inductive List.forall₂ (R : α → β → Prop) : List α → List β → Prop
  | nil : forall₂ R [] []
  | cons {a b l₁ l₂} : R a b → forall₂ R l₁ l₂ → forall₂ R (a::l₁) (b::l₂)

def f : Nat → List Char := ...
def g₁ : Nat → List String := ...
def g₂ : Nat → List String := ...

def equiv : Char → String → Prop := ...

-- This theorem is supposed to be used in the induction's `cons` case below,
-- to show that the lists' heads are equal.
theorem same_equiv_eq {c : Char} {s₁ s₂ : String} :
  equiv c s₁ → equiv c s₂ → s₁ = s₂ := ...

example
  (h₁ : ∀ i, List.forall₂ equiv (f i) (g₁ i))
  (h₂ : ∀ i, List.forall₂ equiv (f i) (g₂ i)) :
  g₁ = g₂ := by
  funext i
  have h₁ := h₁ i
  have h₂ := h₂ i
  generalize hc : f i = c
  generalize hs₁ : g₁ i = s₁
  generalize hs₂ : g₂ i = s₂
  rw [hc, hs₁] at h₁
  rw [hc, hs₂] at h₂
  induction c
  case h.nil => sorry
  case h.cons hd tl hi =>
    sorry

The goal state is:

h₁✝ : ∀ (i : ℕ), List.forall₂ equiv (f i) (g₁ i)
h₂✝ : ∀ (i : ℕ), List.forall₂ equiv (f i) (g₂ i)
i : ℕ
s₁ : List String
hs₁ : g₁ i = s₁
s₂ : List String
hs₂ : g₂ i = s₂
hd : Char
tl : List Char
hi : f i = tl → List.forall₂ equiv tl s₁ → List.forall₂ equiv tl s₂ → s₁ = s₂
hc : f i = hd :: tl
h₁ : List.forall₂ equiv (hd :: tl) s₁
h₂ : List.forall₂ equiv (hd :: tl) s₂
⊢ s₁ = s₂

I can't use hi since it requires f i = tl, which isn't true by hc.
But I don't understand where this condition is coming from.

[Mario Carneiro]

You probably need a generalizing clause in the induction

[Mario Carneiro]

The f i = tl assumption is related to the hc : f i = c assumption you introduced. Try generalize : f i = c instead

[Marcus Rossel]

Mario Carneiro said:

The f i = tl assumption is related to the hc : f i = c assumption you introduced. Try generalize : f i = c instead

Do you mean like this?:

example (h₁ : ∀ i, List.forall₂ equiv (f i) (g₁ i)) (h₂ : ∀ i, List.forall₂ equiv (f i) (g₂ i)) :
  g₁ = g₂ := by
  funext i
  have h₁ := h₁ i
  have h₂ := h₂ i
  generalize f i = c
  induction c
  case h.nil =>
    sorry
  case h.cons hd tl hi =>
    exact hi

Because in that case the cons case is trivial as hi : g₁ i = g₂ i but the nil case doesn't reflect the nil-ness at all.

[Mario Carneiro]

Oh, it looks like lean 4 generalize does not incorporate the behavior of mathlib's generalize_hyp. The generalize line is supposed to replace f i in the context. Without it, you can still do it with rw like you were doing before, plus clear:

example (h₁ : ∀ i, List.forall₂ equiv (f i) (g₁ i)) (h₂ : ∀ i, List.forall₂ equiv (f i) (g₂ i)) :
  g₁ = g₂ := by
  funext i
  have h₁ := h₁ i
  have h₂ := h₂ i
  generalize hc : f i = c
  generalize hs₁ : g₁ i = s₁
  generalize hs₂ : g₂ i = s₂
  rw [hc, hs₁] at h₁
  rw [hc, hs₂] at h₂
  clear hc hs₁ hs₂
  (induction c generalizing s₁ s₂)
  case nil =>
    sorry
  case h.cons hd tl hi =>
    sorry

The parentheses around induction are due to a precedence bug, cc: @Sebastian Ullrich