## Stream: new members

### Topic: simp not resolving an "and.intro rfl rfl"

#### Yakov Pechersky (Oct 29 2020 at 02:02):

I have a tactic state after a simp that looks like:

case list.cons, list.cons, nat.succ
α : Type u_1,
β : Type u_2,
hd : α,
tl : list α,
IH :
∀ {l' : list β} {i : ℕ} (h : i < (tl.zip l').length),
tl.length = l'.length → (tl.zip l').nth_le i h = (tl.nth_le i _, l'.nth_le i _),
hd' : β,
tl' : list β,
i : ℕ,
h : i.succ < ((hd :: tl).zip (hd' :: tl')).length,
hl : tl.length = tl'.length
⊢ tl.nth_le i _ = tl.nth_le i _ ∧ tl'.nth_le i _ = tl'.nth_le i _


#### Yakov Pechersky (Oct 29 2020 at 02:02):

Why doesn't simp resolve the last statement? mwe:

import data.list.basic

open list

namespace list

section list

variables {α β : Type*} (l : list α) (l' : list β) (x : α) (x' : β)

@[simp] lemma zip_nil_left : (@nil α).zip l' = nil := rfl

@[simp] lemma zip_nil_right : l.zip (@nil β) = nil :=
by { induction l; simp only [zip, zip_with] }

@[simp] lemma zip_cons : (x :: l).zip (x' :: l') = (x, x') :: l.zip l' := rfl

@[simp] lemma length_zip : (l.zip l').length = min l.length l'.length :=
begin
induction l with hd tl IH generalizing l',
{ simp only [zip_nil_left, min_eq_left, length, zero_le], },
{ cases l',
{ simp only [zip_nil_right, length, zero_le, min_eq_right] },
end

variables {l l'}

lemma nth_le_zip {i : ℕ} (h : i < (l.zip l').length) (hl : l.length = l'.length) :
(l.zip l').nth_le i h =
(l.nth_le i ((@lt_min_iff _ _ i l.length l'.length).mp (list.length_zip l l' ▸ h)).left,
l'.nth_le i ((@lt_min_iff _ _ i l.length l'.length).mp (list.length_zip l l' ▸ h)).right) :=
begin
induction l with hd tl IH generalizing l' i,
{ simp only [zip_nil_left, length] at h,
exact absurd h (nat.not_lt_zero i) },
{ cases l' with hd' tl',
{ simpa only using h },
{ cases i,
{ simp only [zip_cons, nth_le] },
{ simp only [add_left_inj, length] at hl,
simp [IH, hl],
/-
case list.cons, list.cons, nat.succ
α : Type u_1,
β : Type u_2,
hd : α,
tl : list α,
IH :
∀ {l' : list β} {i : ℕ} (h : i < (tl.zip l').length),
tl.length = l'.length → (tl.zip l').nth_le i h = (tl.nth_le i _, l'.nth_le i _),
hd' : β,
tl' : list β,
i : ℕ,
h : i.succ < ((hd :: tl).zip (hd' :: tl')).length,
hl : tl.length = tl'.length
⊢ tl.nth_le i _ = tl.nth_le i _ ∧ tl'.nth_le i _ = tl'.nth_le i _
-/

exact and.intro rfl rfl,
},
} }
end

end list

end list


Last updated: May 08 2021 at 03:17 UTC