Equivalence to List.map

CsProofs.lean

@@ -11,39 +11,39 @@ open Cslib.Algorithms.Lean
 
 -- Define a local version of the standard functional programming map function
 -- This uses the cslib TimeM monad, for proving properties about time complexity
-def myMap {α β : Type } (list: List α ) (fn : (α -> β)):  TimeM (List β) :=
+def timedMap {α β : Type } (list: List α ) (fn : (α -> β)):  TimeM (List β) :=
   match list with
     | [] => return []
     | (List.cons item rest) => do 
-      let rest' <- myMap rest fn
+      let rest' <- timedMap rest fn
       let this' <- TimeM.tick (fn item)
       return this' :: rest'
 
--- `myMap` works how you'd expect
-#eval myMap [8445, 1,2,3] (fun x => x + 500)
+-- `timedMap` works how you'd expect
+#eval timedMap [8445, 1,2,3] (fun x => x + 500)
 
 -- Proof that mapping over the empty list takes no time
-lemma timeOfEmptyListIsZero (fn : α -> β) : (myMap [] fn).time = 0
+lemma timeOfEmptyListIsZero (fn : α -> β) : (timedMap [] fn).time = 0
   := by
-    unfold myMap
+    unfold timedMap
     unfold pure
     rfl
-    /-- These invocations of `simp` are another way to do this proof
-    simp only [myMap]
+    /- These invocations of `simp` are another way to do this proof
+    simp only [timedMap]
     simp only [pure]
     simp only [TimeM.pure]
-    --/
+    -/
 
--- full proof that `myMap` is linear in the length of the list
-theorem mapIsLinear {α : Type} {fn: α -> β } (xs: List α ) :
+-- full proof that `timedMap` is linear in the length of the list
+theorem timedMapIsLinear {α : Type} {fn: α -> β } (xs: List α ) :
   have n := xs.length;
-  (myMap xs fn).time <= n
+  (timedMap xs fn).time <= n
   := by
     induction xs with
     | nil => simp [timeOfEmptyListIsZero]
     | cons head tail ih =>
         unfold List.length
-        unfold myMap
+        unfold timedMap
         simp only [Bind.bind, TimeM.bind, TimeM.tick, Pure.pure, TimeM.pure]
         -- the `omega` tactic does this Nat math automatically
         --omega
@@ -52,3 +52,14 @@ theorem mapIsLinear {α : Type} {fn: α -> β } (xs: List α ) :
         --exact?
         exact Nat.add_le_add_right ih 1
 
+
+-- prove that timedMap is equivalent to List.map
+theorem timedMap_eq_map { α β : Type } (xs: List α ) (fn : α -> β ) :
+    (timedMap xs fn).ret = (xs.map fn) := by
+      induction xs with
+      | nil => rfl
+      | cons head tail ih => 
+        simp [timedMap, ih]
+
+
+