README, comments

CsProofs.lean

@@ -9,6 +9,8 @@ open Cslib.Algorithms.Lean
 #eval (TimeM.merge [1,2,3,4,5,6,7] [])
 #eval (TimeM.merge [1,2,3,4,5,6,7] [98])
 
+-- 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 β) :=
   match list with
     | [] => return []
@@ -17,19 +19,22 @@ def myMap {α β : Type } (list: List α ) (fn : (α -> β)):  TimeM (List β) :
       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)
 
+-- Proof that mapping over the empty list takes no time
 lemma timeOfEmptyListIsZero (fn : α -> β) : (myMap [] fn).time = 0
   := by
     unfold myMap
     unfold pure
     rfl
-    /--
+    /-- These invocations of `simp` are another way to do this proof
     simp only [myMap]
     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 α ) :
   have n := xs.length;
   (myMap xs fn).time <= n
@@ -40,8 +45,10 @@ theorem mapIsLinear {α : Type} {fn: α -> β } (xs: List α ) :
         unfold List.length
         unfold myMap
         simp only [Bind.bind, TimeM.bind, TimeM.tick, Pure.pure, TimeM.pure]
+        -- the `omega` tactic does this Nat math automatically
         --omega
         rw [Nat.add_zero]
+        -- `exact?` searches for a tactic and tells you what it is
         --exact?
         exact Nat.add_le_add_right ih 1
 

README.md

@@ -1 +1,4 @@
-# cs-proofs
+# Computer Science Lean Proofs
+
+
+This repo is me using [cslib](https://www.cslib.io/) to prove random, hopefully-useful properties of code.