## Stream: new members

### Topic: Problem with induction hypothesis

#### Marcus Rossel (Jan 06 2022 at 10:04):

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 (Jan 06 2022 at 10:23):

You probably need a generalizing clause in the induction

#### Mario Carneiro (Jan 06 2022 at 10:25):

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

#### Marcus Rossel (Jan 06 2022 at 11:44):

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 (Jan 07 2022 at 03:14):

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

Last updated: Dec 20 2023 at 11:08 UTC