# Zulip Chat Archive

## 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