implemented ITree.bind

LeanBoogie/Boog.lean

@@ -12,6 +12,7 @@ open Std (HashSet HashMap)
 
 /-- Assigns values to every variable. Ideally you'd want `(v : String) -> v ∈ ValidVars -> Int`. -/
 abbrev BoogieState := String -> Int
+instance : EmptyCollection BoogieState := ⟨fun _ => 0⟩
 
 /-- State monad during execution of boogie programs. Assigns values to every variable. -/
 abbrev Boog : Type -> Type := StateM BoogieState
@@ -25,8 +26,6 @@ def Boog.set (v : String) (e : Boog Int) : Boog Unit := do
   modifyThe BoogieState
       (fun f x => if x = v then val else f x)
 
-#check ite
-
 /-- This is a little ugly, because lean `if` actually takes a (decidable) `Prop`, not a `Bool` -/
 def Boog.ifthenelse (c : Boog Bool) (t e : Boog Unit) : Boog Unit := do
   if <- c then t else e
@@ -61,7 +60,6 @@ theorem bind_eq2 (a: Boog A) (b: A -> Boog B) : (a >>= b : Boog B) = fun s => le
 @[simp]
 theorem ite_bind:
   ∀ [Monad m]
-    [LawfulMonad m]
     {c : Bool}
     {m1 m2 : m a}
     {k : a -> m b},

LeanBoogie/ITree/Examples.lean

@@ -36,6 +36,20 @@ def find (f : Nat -> Int) (K : Int) (a : Nat) : ITree Empty Nat :=
 theorem find_eq1 {f : Nat -> Int} {K : Int} {a : Nat} (h : f a = K) : find f K a = .ret a := sorry
 theorem find_eq2 {f : Nat -> Int} {K : Int} {a : Nat} (h : f a ≠ K) : find f K a = .tau (find f K (a + 1)) := by sorry
 
+/-- Proof by induction on k, i.e. where the searched-for value is. -/
+theorem find_correct_aux (f : Nat -> Int) (K : Int) (k a : Nat) (h_a : a <= k) (solvable : f k = K) : Eutt (find f K a) (.ret k) := by
+  induction k generalizing a with
+  | zero =>
+    have : a = 0 := by omega
+    cases this
+    rw [find_eq1 solvable]
+    exact Eutt.refl _
+  | succ k ih => -- k is still ahead of the current position (a)
+    done
+
+theorem find_correct (f : Nat -> Int) (K : Int) (k : Nat) (solvable : f k = K) : Eutt (find f K 0) (.ret k) :=
+  find_correct_aux f K k 0 (by omega) solvable
+
 /-- Like `find`, but on `Int` instead of `Nat`, and searches in both directions. -/
 def find2 (f : Int -> Int) (K : Int) (a b : Int) : ITree Empty Int :=
   ITree.corec (fun (a, b) =>

LeanBoogie/ITree/ITree.lean

@@ -48,53 +48,59 @@ end Internal
 abbrev Ans : Type := Int
 
 def ITree E A := Internal.ITree Ans E A
+
+namespace ITree
+
 -- QPF gotcha: The parameters to ITree get reordered in the ctors somehow
-def ITree.ret {E A} (r : A) : ITree E A := @Internal.ITree.ret A Ans E r
-def ITree.tau {E A} (t : ITree E A) : ITree E A := @Internal.ITree.tau Ans E A t
-def ITree.vis {E A} (e : E) (k : Ans -> ITree E A) := @Internal.ITree.vis E Ans A e k
+def ret {E A} (r : A) : ITree E A := @Internal.ITree.ret A Ans E r
+def tau {E A} (t : ITree E A) : ITree E A := @Internal.ITree.tau Ans E A t
+def vis {E A} (e : E) (k : Ans -> ITree E A) := @Internal.ITree.vis E Ans A e k
 
-abbrev ITree.Base E A β := Internal.ITree.Base Ans E A β
+abbrev Base E A β := Internal.ITree.Base Ans E A β
 
-def ITree.corec {E A β : Type} (f : β → ITree.Base E A β) (b : β) : ITree E A :=
-  MvQPF.Cofix.corec (n := 2) (F := TypeFun.ofCurried (ITree.Base)) f b
+def corec {E A β : Type} (f : β → ITree.Base E A β) (b : β) : ITree E A
+  := MvQPF.Cofix.corec (n := 2) (α := (Vec.reverse (Vec.nil.append1 A ::: E))) (F := TypeFun.ofCurried (n := 3) (ITree.Base)) f b
 
-/-- Execute a finite amount of steps of a potentially infinite ITree.
-  Returns the events encountered along the way (if any), and the final state (if any).
-  Uses `f` to determine the answer to events. -/
-def ITree.run (t : ITree E A) (f : E -> Ans) : Nat -> (List E) × Option A
-| 0 => ([], none)
-| n+1 => match MvQPF.Cofix.dest t with
-  | .ret a => ([], some a)
-  | .tau t => run t f n
-  | .vis e k => by
-    let t : ITree E A := k (f e)
-    let (evs, ret) := run t f n
-    exact (e :: evs, ret)
+def dest {E A : Type} : ITree E A -> ITree.Base E A (ITree E A)
+  := MvQPF.Cofix.dest
 
 @[cases_eliminator, elab_as_elim]
-def ITree.cases {E A : Type} {motive : ITree E A → Sort u}
+def cases {E A : Type} {motive : ITree E A → Sort u}
     (ret : (r : A) → motive (.ret r))
-    (tau : (x : ITree E A) → motive (ITree.tau x))
+    (tau : (x : ITree E A) → motive (.tau x))
     (vis : (e : E) → (k : Ans → ITree E A) → motive (.vis e k)) :
     ∀ (x : ITree E A), motive x :=
   fun x =>
     match h : MvQPF.Cofix.dest x with
     | .ret r =>
-      have h : x = ITree.ret r := by
+      have h : x = .ret r := by
         apply_fun MvQPF.Cofix.mk at h
         simpa [MvQPF.Cofix.mk_dest] using h
       h ▸ ret r
     | .tau y =>
-      have h : x = ITree.tau y := by
+      have h : x = .tau y := by
         apply_fun MvQPF.Cofix.mk at h
         simpa [MvQPF.Cofix.mk_dest] using h
       h ▸ tau y
     | .vis e k =>
-      have h : x = ITree.vis e k := by
+      have h : x = .vis e k := by
         apply_fun MvQPF.Cofix.mk at h
         simpa [MvQPF.Cofix.mk_dest] using h
       h ▸ vis e k
 
+/-- Execute a finite amount of steps of a potentially infinite
+  Returns the events encountered along the way (if any), and the final state (if any).
+  Uses `f` to determine the answer to events. -/
+def run (t : ITree E A) (f : E -> Ans) : Nat -> (List E) × Option A
+| 0 => ([], none)
+| n+1 => match t.dest with
+  | .ret a => ([], some a)
+  | .tau t => run t f n
+  | .vis e k => by
+    let t : ITree E A := k (f e)
+    let (evs, ret) := run t f n
+    exact (e :: evs, ret)
+
 -- # Experimentation:
 
 namespace WithSigma
@@ -103,8 +109,8 @@ namespace WithSigma
   | tau (t : ι) -- ι = ITree ε ρ
   | vis (e : ν) -- ν = Σ α : Type, ε α × α → ITree ε ρ
 
-  -- qpf F ε ρ ι ν    = (Σ α : Type, ε α × α → ι)
-  -- qpf F (α : Type) ε ρ ι ν    = Sigma G
+  -- qpf F ε ρ ι ν    := (Σ α : Type, ε α × α → ι)
+  -- qpf F (α : Type) ε ρ ι ν    := Sigma G
 
   qpf G (α : Type) (ε : Type → Type) ρ ι ν := ε α × (α → ι)
 

LeanBoogie/ITree/Mem.lean

@@ -22,5 +22,52 @@ abbrev Mem : Type -> Type := ITree MemEv
 def Mem.set (a : String) (b : Int) : Mem Unit := .vis (.write a b) (fun _unit => .ret ())
 def Mem.get (v : String)           : Mem Int  := .vis (.read v) (fun ans => .ret ans)
 
--- TODO: interpreting memory events away into the boogie state monad.
--- def interp (handler : MemEv -> Boog Int) (t : Mem A) : Boog A :=
+abbrev Mem.inc (v : String) : Mem Unit := do
+  let x <- get v
+  set v (x+1)
+
+/-
+  # Interpreting memory
+-/
+
+/-- Transforms memory events into state monad actions. -/
+-- def interp (tm : ITree MemEv A) (s₀ : BoogieState) : ITree Empty (A × BoogieState) :=
+def interp (tm : ITree MemEv A) : StateT BoogieState (ITree Empty) A := fun s₀ =>
+  ITree.corec (fun ⟨tm, s⟩ =>
+    match tm.dest with
+    | .ret a => .ret (a, s)
+    | .tau t => .tau (t, s)
+    | .vis (.read v)      k =>
+      let ⟨val, s'⟩ := Boog.get v s
+      .tau ⟨k val, s'⟩
+    | .vis (.write v val) k =>
+      let ⟨(), s'⟩ := Boog.set v (pure val) s
+      .tau ⟨k (default), s'⟩ -- TODO: Instead of `default : Int`, this should be `() : Unit` once the QPF ITree limitation is gone.
+  ) (tm, s₀)
+
+def writeForever : ITree MemEv Empty
+  := ITree.corec (fun a => .vis (MemEv.write "x" 1) (fun _unit => a) ) 0
+
+-- ? If it terminates, can you extract the state transition function?
+#check fun s₀ => ITree.run (interp (Mem.inc "x") s₀) 0 2 |>.2
+-- #eval ITree.run (interp (Mem.inc "x") {}) 0 2 |>.2
+
+#check interp writeForever
+#check ITree.run (interp writeForever {}) 0 0
+#reduce ITree.run (interp writeForever {}) 0 0
+
+theorem interp_ret : interp (.ret x) s = .ret (x, s) := by
+  rw [interp]
+  sorry
+
+
+section Experiment
+-- ## Crazy idea, what if...
+
+def interp_crazy (t : ITree MemEv A) : ITree Empty (A × (BoogieState -> BoogieState -> Prop)) :=
+  match t.dest with
+  | .ret r => .ret (r, (. = .))
+  | .tau r => sorry
+  | .vis e k => sorry
+
+end Experiment

LeanBoogie/ITree/Monad.lean

@@ -1,45 +1,68 @@
 import LeanBoogie.ITree.ITree
 import LeanBoogie.ITree.Eutt
 
+namespace ITree
+
 /-
   # `ITree` forms a monad
 -/
 
-def ITree.pure (a : A) : ITree E A := .ret a
-
-def ITree.bind (ta : ITree E A) (tb : A -> ITree E B) : ITree E B :=
-  ITree.corec (fun ta => ta.cases
-    (fun (a : A) =>
-      let tb : ITree E B := tb a
-
-      sorry
-    ) -- :(
-    (fun ta => .tau ta)
-    (fun e k => .vis e (fun x => k x))
-  ) ta
+def pure (a : A) : ITree E A := .ret a
+
+def bind (ta : ITree E A) (tb : A -> ITree E B) : ITree E B :=
+  ITree.corec (β := Sum (ITree E A) (ITree E B)) (fun x =>
+    match x with
+    | .inl ta =>
+      match ta.dest with
+      | .ret (a : A) =>
+        let tb : ITree E B := tb a
+        let tbdest : ITree.Base E B (ITree E B) := tb.dest
+        have : TypeFun.ofCurried Base ((Vec.reverse (Vec.nil.append1 B ::: E)).append1 (ITree E B)) = Base E B (ITree E B) := rfl
+        let INR : TypeVec.Arrow
+          ((Vec.reverse (Vec.nil.append1 B ::: E)).append1 (ITree E B))
+          ((Vec.reverse (Vec.nil.append1 B ::: E)).append1 (ITree E A ⊕ ITree E B))
+          := TypeVec.appendFun TypeVec.id Sum.inr
+        let ret : ITree.Base E B (ITree E A ⊕ ITree E B) := MvFunctor.map (F := TypeFun.ofCurried (n := 3) ITree.Base) INR (this ▸ tbdest)
+        ret
+      | .tau t => .tau (.inl t)
+      | .vis e k => .vis e (fun x => .inl (k x))
+    | .inr b =>
+      match b.dest with
+      | .ret (b : B) => .ret b
+      | .tau t => .tau (.inr t)
+      | .vis e k => .vis e (fun x => .inr (k x))
+  ) (Sum.inl ta)
 
 instance : Monad (ITree E) where
-  pure := ITree.pure
-  bind := ITree.bind
-
-#check LawfulMonad
+  pure := pure
+  bind := bind
+
+instance : LawfulFunctor (ITree E) where
+  map_const := sorry
+  id_map := sorry
+  comp_map := sorry
+instance : LawfulMonad (ITree E) where
+  seqLeft_eq := sorry
+  seqRight_eq := sorry
+  pure_seq := sorry
+  bind_pure_comp := sorry
+  bind_map := sorry
+  pure_bind := sorry
+  bind_assoc := sorry
 
 /- ## Helpers for writing imperative programs -/
 
-def ITree.skip : ITree E Unit := .ret ()
-def ITree.spin : ITree E A := ITree.corec (fun n => .tau n) 0
-def ITree.seq (a b : ITree E Unit) : ITree E Unit := bind a (fun () => b)
-def ITree.trigger (e : E) : ITree E Int := .vis e (fun ans => .ret ans)
+def skip : ITree E Unit := .ret ()
+def spin : ITree E A := corec (fun n => .tau n) 0
+def seq (a b : ITree E Unit) : ITree E Unit := bind a (fun () => b)
+def trigger (e : E) : ITree E Int := .vis e (fun ans => .ret ans)
+def ite (c : ITree E Bool) (t e : ITree E Unit) : ITree E Unit := bind c (fun c => if c then t else e)
+abbrev ifthen (c : ITree E Bool) (t : ITree E Unit) : ITree E Unit := ite c t skip
 
-def ITree.ite (c : ITree E Bool) (t e : ITree E Unit) : ITree E Unit
-  := bind c (fun c => if c then t else e)
+def assume (φ : Prop) [Decidable φ] : ITree E Unit := if φ then skip else spin
 
-abbrev ITree.ifthen (c : ITree E Bool) (t : ITree E Unit) : ITree E Unit
-  := ite c t skip
 
-def ITree.assume (φ : Prop) [Decidable φ] : ITree E Unit := if φ then skip else spin
-
-/-
+/- # Iter
   From the ITrees paper, page 12:
   CoFixpoint iter (body : A → itree E (A + B)) : A → itree E B :=
     fun a ⇒ ab <- body a ;;
@@ -57,27 +80,26 @@ def ITree.assume (φ : Prop) [Decidable φ] : ITree E Unit := if φ then skip el
       end) (inr a).
 -/
 
--- -- ! Wait,... we don't have loops. We just have blocks.
--- def loop (step : A -> ITree E (Sum A B)) (a : A) : ITree E B :=
---   sorry
-
--- /--
---         iter step a  : ITree E B
---   step (iter step a) : ITree E B
--- -/
--- def iter (step : A -> ITree E (Sum A B)) (a : A) : ITree E B :=
---   ITree.corec (fun iter_ =>
---     bind (step iter_) (fun
---       | .inl a => step a
---       | .inr b => .ret (.inr b)
---     )
---   ) a
---   -- ITree.corec (fun
---   --   | .inl a => .tau (step a)
---   --   | .inr b => .ret b
---   -- ) (Sum.inl a)
-
---   -- ITree.bind (step a) (fun
---   --   | .inl a => step a
---   --   | .inr b => sorry
---   -- )
+/-- Repeat a computation until it returns `B`. -/
+def iter (body : A -> ITree E (Sum A B)) (a : A) : ITree E B := sorry
+--   ITree.corec (β := Sum A Unit) (fun x =>
+--     match x with
+--     | .inl a =>
+--       let res := bind (body a) (fun ab =>
+--         match ab with
+--         | .inl a => sorry
+--         | .inr b => sorry
+--       )
+--       match res.dest with
+--       | .ret a => sorry
+--       | .tau a => sorry
+--       | .vis e k => sorry
+--       -- | .vis e k => .vis e (fun x => .inl (k x))
+--     | .inr b =>
+--       match b.dest with
+--       | .ret (b : B) => .ret b
+--       | .tau t => .tau (.inr t)
+--       | .vis e k => .vis e (fun x => .inr (k x))
+--   ) (Sum.inl a)
+
+def loop (body : Sum C A -> ITree E (Sum C B)) (a : A) : ITree E B := sorry