From cab3217b05cd8e9fcbe1bd17edae4f4dece90b8a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 14 Mar 2022 11:50:47 -0700 Subject: [PATCH] feat: add `forIn'_eq_forIn` theorem for lists --- src/Init/Data/List/Control.lean | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/Init/Data/List/Control.lean b/src/Init/Data/List/Control.lean index 14aeaa5814..d31a4008fa 100644 --- a/src/Init/Data/List/Control.lean +++ b/src/Init/Data/List/Control.lean @@ -176,6 +176,15 @@ instance : ForIn m (List α) α where instance : ForIn' m (List α) α inferInstance where forIn' := List.forIn' +@[simp] theorem forIn'_eq_forIn {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : List α) (init : β) (f : α → β → m (ForInStep β)) : forIn' as init (fun a _ b => f a b) = forIn as init f := by + simp [forIn', forIn, List.forIn, List.forIn'] + have : ∀ cs h, List.forIn'.loop cs (fun a x b => f a b) as init h = List.forIn.loop f as init := by + intro cs h + induction as generalizing cs init with + | nil => intros; rfl + | cons a as ih => intros; simp [List.forIn.loop, List.forIn'.loop, ih] + apply this + instance : ForM m (List α) α where forM := List.forM