Theorem prover lab: applications in programming languages

Lambda the Ultimate SSA: Optimizing Functional Programs in SSA

Numerical packages in lean

https://github.com/leanprover/lean4/blob/master/tests/playground/webserver/Webserver.lean

novice friendly induction tactic https://arxiv.org/pdf/2012.08990.pdf

metaprogramming framework for formal verification https://dl.acm.org/doi/pdf/10.1145/3110278

http://leanprover.github.io/papers/lean4.pdf lean4

“The Lean typeclass resolution procedure can be viewed as a simple λ-Prolog interpreter [8], where the Horn clauses are the user declared instances.” That sounds fun

lean for the curious mathematician 2020

mathlib 4 docs but also std lib docs

lean forward a hitchiker’s guide to formal verification Still on Lean 3 fyi https://github.com/blanchette/logical_verification_2023 2023 version is on lean 4

lean update ipam 2023

lean chat openai codex tranlate natural language to lean statements

https://lean.math.hhu.de/ lean4 web editor lean 4 metaprgramming book metaprogramming in lean 4

https://github.com/yatima-inc hmm. Lean company?

https://github.com/search?q=language%3ALean&type=Repositories&ref=advsearch&l=Lean&l=

lean 4 tagged stuff on github makig lean cli tools - arg parsing and whatnot https://github.com/GaloisInc/reopt-vcg https://github.com/opencompl/lean-mlir

do unchained - a description of the extensions to monad syntax like for, break, mut that lean offer

lean 3 to lean 4 tactic trasnlation cheatsheet

A super position prover for Lean 3

https://github.com/ccodel/verified-encodings

a big twitter thread on lean software verification stuff

mathematics in lean course iris lean

lean 4 hackers

lean 4 released

lean dojo LeanDojo: Theorem Proving with Retrieval-Augmented Language Models

euclidean geometry

learning lean 4

https://lftcm2023.github.io/tutorial/ lean curious mathematician 2023 https://www.slmath.org/summer-schools/1021#schedule_notes

Verification of Combinational and Sequential Circuits in LEAN3

https://github.com/leanprover/lean4-cli https://github.com/EdAyers/ProofWidgets4

A Henkin-style completeness proof for the modal logic S5∗

paper proof proof visualization https://lakesare.brick.do/all-lean-books-and-where-to-find-them-x2nYwjM3AwBQ

How to prove it with lean

lean 4 terry tao

https://www.moogle.ai/ semantic search

https://lean-fro.org/about/roadmap/ learn roadmap for lean focused research organization

Build

elan tool

leanpkg

lake is a new build tool on the horizon. analog of cargo Making a lake project is a way to get the standard lib? https://github.com/leanprover-community/mathlib4/blob/master/lakefile.lean mathlib4 lakefile

require std from git "https://github.com/leanprover/std4" @ "main"
require Qq from git "https://github.com/gebner/quote4" @ "master"
require aesop from git "https://github.com/JLimperg/aesop" @ "master

Using nix is kind of a pain. I haven’t done it.

Ah. I need to open my lake project in it’s own window for vscode to work right resolving paths. That is weird. Hmm.

LEAN_PATH for libraries? Probably I’m fighting the Lake experience which is bad.

[@inline] [@reduced] [@simp]

Lean Src

https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html prelude is interesting

simp tactic

discrimination tree disctree types

Expr

IR - somehow this is what I need to look at to implement new backend?

MIL

-- tactics
rw
use
rintro
ring

have have, show style proofs

Stuff

echo '
def main := IO.println "hello world"
' > /tmp/test.lean
lean --run /tmp/test.lean


def main := IO.println "hello world"

#eval 1 + 1 -- it's a nat
#eval String.append "hello" "world"
#eval if 1 > 2 then "yes" else "no"
#eval (1 + 1 : Int)

/- block comment -/
def hello := "hello"
def Str : Type := String

abbrev N : Type := Nat
#check 1.2

structure Point where
  x : Float
  y : Float
deriving Repr

#check ({x := 1, y := 2} : Point)

inductive MyBool where
  | MyTrue : MyBool
  | MyFalse : MyBool

#check MyBool.MyTrue

#eval Lean.versionString

#check fun (x : Nat) => x
#check λ x => x
#eval let y := 2; y + y

theorem foo : p -> q -> p /\ q :=
  by intros x y
     apply And.intro
     apply x
     apply y
     done

inductive aexp where
    | Plus : aexp -> aexp -> aexp
    | Lit : Nat -> aexp

-- dot notation to go into aexp scope
def interp : aexp -> Nat
    | .Plus x y => interp x + interp y
    | .Lit n => n

#eval interp (aexp.Plus (aexp.Lit 4) (aexp.Lit 3))

#check (("a",1) : Prod String Nat )
#eval (1,(2,34,5)) == (1,2,34,5)


#print axioms Nat.add_comm

#eval ! true || (false && true)
--example : True := by
--    decide

import Std.Data.List.Basic
import Mathlib.Tactic.LibrarySearch
import Mathlib.Tactic.Linarith
import Aesop

-- aesop is an auto tactic
example : α → α :=
  by aesop



theorem foo : 1 = 1 := by
  -- library_search
  exact _root_.trans rfl rfl
#check _root_.trans

theorem bar : x <= 7 + 3*x := by
  linarith

#print bar
def hello := "world"

theorem and_commutative (p q : Prop) : p ∧ q → q ∧ p :=
  fun hpq : p ∧ q =>
  have hp : p := And.left hpq
  have hq : q := And.right hpq
  show q ∧ p from And.intro hq hp


theorem plus_comm : forall a b, a + b + 0 = b + a := by
  intros a b
  have c : a + b = b + a := by exact IsSymmOp.symm_op a b
  rw [c]
  have d : forall x, x + 0 = x := by intros; exact namedPattern rfl rfl rfl
  rw [d]

-- ok, so unification variables can be made by apply, or explicit ?x maybe?
theorem existstry : exists x, x = 11 := by
  apply Exists.intro
  rfl

example : exists x, x = 11 := by
  exists ?x
  exact 11
  rfl

-- simp?

/-

repeat (apply r1 | apply r2 | apply r3 <;> simp)

-/

#check existstry



import Lean.Data.PersistentHashSet
import Lean.Data.PersistentHashMap
import Lean.Data.RBMap
import Lean.Data.RBTree
import Mathlib.Data.List.Basic
import Lean
import Qq
import Lean.Meta.Reduce
import Lean.Meta

import Lean.Meta.DiscrTree
open Lean.PersistentHashSet
open Lean (PHashSet)

#check EmptyCollection
def edge1 : PHashSet Int := insert EmptyCollection.emptyCollection 5
def edge : PHashSet Int := insert empty 6
def toList {α : Type}[BEq α] [Hashable α] 
(s : PHashSet α) : List α := 
  fold (fun a b => b :: a) [] s

#eval toList edge
--#eval (Lean.PersistentHashMap.toList edge)

-- list comprehesion sugar example
-- https://github.com/leanprover/lean4-samples/tree/main/ListComprehension


-- RBTRee vs Persistenthash
-- Lookos like RBTree has more functions on it.
#check ()
#check compare
-- hmm. It takes an ordering in the type. Interesting.
def edge3 : Lean.RBTree Int compare := Lean.RBTree.insert Lean.RBTree.empty 7
#eval Lean.RBTree.toArray edge3

-- Oh Std has HashMap and HashSet


#eval #[1,2,3] -- array notation. Cool.

#check (1,2)
#check List.pure
#synth Monad List -- ok I needed to import mathlib to get monad instance for list
abbrev Rel := List (Prod Int Int)
def run (edge path : Rel) : List (Int × Int) := 
  let r2 := edge
  let r1 := do
    --pure (1,2)
    let (x,y) <- edge
    let (y1,z) <- path
    if y == y1 then
      pure (x,z)
    else
      [] --failure -- List isn't altenrative
  r1 ++ r2

-- The stream type is called many  https://leanprover.github.io/functional_programming_in_lean/monads/arithmetic.html#nondeterministic-search
--#check Many No I can't finds this

#eval run [(1,2), (2,3)] []
  --for (x,y) in edge, (y1,z) in path do
  --  pure (x,z)
  --  for (y1,z) in path do
  --  if y == y1 then pure (x,z) else fail

--def run1 edge path :=  ()
  -- Lean.RBTree. edge #[] (fun (x,y) => )

-- lean as an logic automation framework seems fun
-- don't worry about termination or proving anythihng.
-- just reuse parsers and indexing structures

-- Brzowski derivatives
-- generic automata minimization
-- lean-res / metis
-- datalog -> lambda datalog -> egglog



-- Lean Expr
-- https://leanprover-community.github.io/mathlib4_docs/Lean/Expr.html
#print Lean.Expr
open Lean
def bv0 : Expr := .bvar 0
#eval bv0 
#eval toExpr true
#check Expr.const "foo" []
#check `foo -- Name

#check Expr.const `foo []
#check ``Nat.zero -- checks identifier exists


#check Expr.app
#check mkApp2
#check mkAppN -- takes array

-- #eval mkLambdaEx
-- #eval Q(foo bar biz)
def foo := Expr.const ``Nat.zero [] 
-- trick to convert Expr to it's meaning
elab "foo" : term => return foo
#check foo

open Qq
set_option trace.compiler.ir.result true in

#check (q([2,3]) : Expr)

#check Nat.succ
#print Nat
def mypow (n : Nat)  x :=
 match n with 
 | .zero => 1
 | .succ n' => x * (mypow n' x) 
/-
def mypow' (n : Nat) (x : Expr) : Expr :=
 match n with 
 | .zero => q(1)
 | .succ n' => q($x * $(mypow' n' x)) 
 -/
 -- CoreM
 -- MetaM - metavaraibe generation
 --

-- eval also executes MetaM monad
#eval Lean.Meta.reduce q(1 + 2)
#eval (q(1 + 2 : Nat) : Expr)

-- optParam of functions. Huh. Nice.
-- outParam of typeclasses

elab "#mycommand2" : command =>
  logInfo "Hello World"
#mycommand2 -- Hello World

/-
MetaM moand 




-/


def doo : MetaM Expr := do
  let me <- Lean.Meta.mkFreshExprMVar none
  let m := Lean.Expr.mvarId! me
  Lean.MVarId.assign m (Expr.const ``Nat.zero [])
  Lean.instantiateMVars me

#eval doo

-- what the gell is eval show
--#eval show MetaM Unit from doo


-- Meta Basic file. good to peruse
-- https://leanprover-community.github.io/mathlib4_docs/Lean/Meta/Basic.html

open Lean.Elab.Term in
def whnf' (e : TermElabM Syntax) : TermElabM Format := do
  let e ← elabTermAndSynthesize (← e) none
  Lean.Meta.ppExpr (← Lean.Meta.whnf e)

#eval whnf' `(List.append [1,2] [2,3])

-- lazy evaluation is good for reducing the head lazily for matchig

#check Lean.Meta.isDefEq


#eval show MetaM _ from do
  let e := q([1,2])
  let e' := q([1,2])
  let b <- Lean.Meta.isDefEq e e'
  pure b

#eval show MetaM _ from do
  logInfo "hello wolrd"
  dbg_trace "hi there"


axiom edge2 : Int -> Int -> Prop

#eval show MetaM _ from do
  let m <- Lean.Meta.mkFreshExprMVar none
  let m2 <- Lean.Meta.mkFreshExprMVar none
  _ <- Lean.Meta.instantiateForall q(forall x : Nat, x = x) #[m]
  Lean.Meta.instantiateForall q(forall x y, edge2 x y) #[m,m2]



namespace Discrtree
  -- https://github.com/leanprover/lean4/blob/master/src/Lean/Meta/DiscrTree.lean
  open Lean.Meta.DiscrTree
  --#eval forall x y, edge x y
  #check getMatch
  #check mkConst `foo

  -- ok so we can make discrimination trees. Doesn't actually help us do multipatterns
  #eval show MetaM _ from do
    let fo := mkConst `foo
    let mvar1 ← Lean.Meta.mkFreshExprMVar (Expr.const ``Nat []) (userName := `mvar1)
    let d <- insert (empty : Lean.Meta.DiscrTree _ true) fo 42
    let pat := mvar1
    --getMatch d pat
    getUnify d pat

end Discrtree

open Lean.PersistentHashSet
open Lean (PHashSet)

namespace leanlog2

def run (db : PHashSet Expr) : PHashSet Expr := 
  fold (fun acc b => 
  if let .const `edge _ := b then
    
    fold (fun acc c => insert acc c) acc db
  else acc) empty db


#eval toList (run (List.foldl insert empty [mkConst `foo, mkConst `bar ]))




end leanlog2




-- Brzowksisksis derivatives for regex
-- https://www.ccs.neu.edu/home/turon/re-deriv.pdf
inductive regex where
    | empty : regex
    | eps : regex -- empty string
    | lit : Char -> regex
    | seq : regex -> regex -> regex
    | and : regex -> regex -> regex
    | star : regex -> regex

#check regex.lit 'a'

def null : regex -> regex
    | .empty => .empty
    | .eps => .eps
    | .lit _ => .eps
    | .seq a b => .and (null a) (null b)
    | .and a b => .and (null a) (null b)
    | .star _ => .eps

def deriv a 
    | .empty => .empty
    | .eps => .eps
    | .lit b => if a == b then .eps else .empty 
    | .seq a' b => .alt (.seq (deriv a a') b) (.seq a' (deriv a b))
    | .and a b => .and (null a) (null b)
    | .star _ => .eps
def main : IO Unit := pure ()

Typeclass


-- Use and abuse of instance parameters in the Lean mathematical library
-- https://arxiv.org/pdf/2202.01629.pdf

class GoodNum (n : Int) where

instance : GoodNum 3 where
instance : GoodNum 4 where

#check (inferInstance : GoodNum 4)

-- set_option in

--variable (mylist : Type)
def mylist := Type
--variable (cons : Int -> mylist -> mylist) --(nil : mylist)
--variable (myappend : mylist -> mylist -> mylist -> Prop)
axiom nil : mylist
axiom cons : Int -> mylist -> mylist
class MyAppend (x : Type) (y : Type) (z : Type) where






#check MyAppend Int Int Int 
instance myfoo (x : mylist) : MyAppend nil x x where
instance [MyAppend xs ys zs] : MyAppend (cons x xs) (ys) (cons x zs) where
#check myfoo
#check inferInstance
#check (inferInstance : MyAppend nil nil nil)
#synth (MyAppend nil nil nil)
#check exists x, x
--theorem mytest : (Σ z, MyAppend (cons 7 nil) nil z) := by
--  exists
--  exact inferInstance


--#print mytest

-- instance : MyAppend (cons x xs) (ys) (cons x zs) where

axiom A : Type
axiom B : Type
axiom C : Type
axiom D : Type

class R (a : Type) (b : Type) where

instance I1 : R A B where
instance I2 : R A C where
instance I3 : R C D where
instance I4 {X Y Z : Type} [R X Y] [R Y Z] : R X Z where
#check (inferInstance :  R A D)
set_option trace.Meta.synthInstance true
#synth R A D


class Quant (a : Type) where
class Foo (a : Type) where
class Biz (a : Type) where
-- https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/quantified_constraints.html
instance [Biz a] : Quant a where
instance biz [forall a, [Biz a] : Quant a] : Foo Int where
#check biz
#synth Foo Int

-- unification hints

Minikanren

inductive Term where
  | Var : String -> Term
  | Fn : String -> List Term -> Term

def Subst := List (String × Term)
def walk subst t : Term :=
  match t with
  | Var s => match subst.find (_ == s) with
    | Some t => walk subst t
    | None => t
  | Fn f ts => Fn f (ts.map (walk subst))

def unify t1 t2 subst : Option Subst :=
  match t1,t2 with
  | Var s1, Var s2 => if s1 == s2 then some subst else some ((s1,t2)::subst)

def disj := 
def conj :=

Embedding Logic

We’re (Me) more used to embedding Hoare logics and things because they are disparate from Lean’s logic. But we can also embed prop logic, fol, modal, etc. This can be useful for reflective proving

-- shallow embdding of logic is a usefuk thing to know about
-- []()

inductive Prop' where
  | Atom : String -> Prop' 
  | Impl : Prop' -> Prop'  -> Prop' 
  | Not : Prop'  -> Prop' 
  | False : Prop'

inductive Provable : List Prop' -> Prop' -> Prop where -- [P] |- Q
  --| Modus : forall a b, Provable h(Impl a b) -> Provable a -> Provable b
  -- | Axiom : forall a, Provable a -> Provable a
  | Refl : forall hyps a, Provable (a :: hyps) a
  | Weaken : forall hyps a b,  Provable hyps b -> Provable (a :: hyps) b
  -- | NotI : forall hyps a, Provable (a :: hyps) Prop'.False -> Provable hyps (Prop'.Not a)
  -- | NotE : forall hyps a, Provable hyps (Prop'.Not a) -> ProaProvable hyps Prop'.False
  | ImplI : forall hyps a b, Provable (a :: hyps) b -> Provable hyps (Prop'.Impl a b)
  | ImplE : forall hyps a b, Provable hyps (Prop'.Impl a b) -> Provable hyps a -> Provable hyps b
  | FalseE : forall hyps a, Provable hyps Prop'.False -> Provable hyps a

-- Using lean typeclasses as automation for our proof datatype
instance Inhabited (Provable )
class BackChain
class Invert

-- cody claims that first order logic using explicit names isn't that bad

inductive Term where
  | Var : String -> Term
  | Const : String -> List Term -> Term

inductive FOL where
  | Atom : Term -> FOL
  | Impl : FOL -> FOL -> FOL

IMP

-- From Coq Require Import Arith ZArith Psatz Bool String List Program.Equality.
-- Require Import Sequences.
/-   -/
-- Local Open Scope string_scope.
-- Local Open Scope Z_scope.
-- Local Open Scope list_scope.

-- import home.philip.Documents.lean.std4.Std.Data.Int.Basics

-- import Std.Data.List.Basic
import Std.Data.Int.Basic
import Std.Data.Int.Lemmas

import Std.Data.List.Basic
import Mathlib.Tactic.LibrarySearch
import Mathlib.Tactic.Linarith

#eval Lean.versionString
#eval 1 + 1
#check (1 : Int)
#check "string"

/-
-- /-* * 1. The source language: IMP -/
-/
-- /-* ** 1.1 Arithmetic expressions -/


abbrev ident : Type := String
#check String
-- def mythree : Nat := 3
-- type ident = string

-- /-* The abstract syntax: an arithmetic expression is either... -/
def myid : forall {a :Type}, a -> a := fun x => x
def myid2 : {a :Type} -> a -> a := fun x => x
#check myid

inductive aexp where
  | CONST (n : Int) : aexp --                      /-*r a constant, or -/
  | VAR (x : ident) : aexp --                   /-*r a variable, or -/
  | PLUS (a1 : aexp) (a2 : aexp) : aexp --        /-*r a sum of two expressions, or -/
  | MINUS (a1 : aexp) (a2 : aexp) : aexp --      /-*r a difference of two expressions -/

/- /- * The denotational semantics: an evaluation function that computes
  the integer value denoted by an expression.  It is parameterized by
  a store [s] that associates values to variables. -/
-/


def store : Type := ident -> Int

def aeval (s: store) (a: aexp) : Int :=
  match a with
  | aexp.CONST n => n
  | aexp.VAR x => s x
  | aexp.PLUS a1 a2 => aeval s a1 + aeval s a2
  | aexp.MINUS a1 a2 => aeval s a1 - aeval s a2


--/-* Such evaluation functions / denotational semantics have many uses.
--    First, we can use [aeval] to evaluate a given expression in a given store. -/

#eval (aeval (fun _x => 2) (aexp.PLUS (aexp.VAR "x") (aexp.MINUS (aexp.VAR "x") (aexp.CONST 1))))


-- /-* Result is: [ = 3 : Z ]. -/

-- /-* We can also do partial evaluation with respect to an unknown store -/
open aexp
-- hmm #eval doesn't work. #reduce is a little too aggressive
#reduce (fun s => aeval s (PLUS (VAR "x") (MINUS (CONST 10) (CONST 1))))
-- example : forall s, 42 =  aeval s (PLUS (VAR "x") (MINUS (CONST 10) (CONST 1))) := by
--  intros
--  simp [aeval]

--/-* Result is: [ = fun s : store => s "x" + 9 ]. -/

-- /-* We can prove properties of a given expression. -/

#print Int.lt_succ
--set_option trace.Compiler.
--set_option t.Compiler.simp true 
--set_option trace.Debug.Meta.Tactic.simp true
set_option trace.Meta.Tactic.simp true
--set_option pp.all true
theorem aeval_xplus1 :
  forall (s :store) (x :ident), aeval s (PLUS (VAR x) (CONST 1)) > aeval s (VAR x) := by 
  intros s x
  --simp? [aeval]
  simp only [aeval, gt_iff_lt, lt_add_iff_pos_right]

  --simp [aeval]
  --linarith -- huh merely importing Linarith makes simpe discharge this
  -- library_search
  -- apply Int.lt_succ
-- delta aeval

#check "hi" 

#check 10
#check aeval_xplus1


/-
Proof.
  intros. cbn. lia.
Qed.
-/
/-
/-* Finally, we can prove "meta-properties" that hold for all expressions.
  For example: the value of an expression depends only on the values of its
  free variables.

  Free variables are defined by this recursive predicate:
-/
-/
def free_in_aexp (x: ident) (a: aexp) : Prop :=
  match a with
  | CONST n => False
  | VAR y => y = x
  | PLUS a1 a2 | MINUS a1 a2 => free_in_aexp x a1 \/ free_in_aexp x a2



theorem aeval_free:
  forall s1 s2 a,
  (forall x, free_in_aexp x a -> s1 x = s2 x) ->
  aeval s1 a = aeval s2 a := by
  intros s1 s2 a
  induction a <;> simp [aeval] <;> intros hyp
  -- case CONST n => simp [aeval]
  case VAR x => apply hyp; simp [free_in_aexp]
  -- what a mess
  case PLUS a1 a2 => rw [a1, a2] <;> intros x f <;> apply hyp <;> simp [free_in_aexp]; apply Or.inr; assumption; apply Or.inl; assumption
  case MINUS a1 a2 => rw [a1, a2] <;> intros x f <;> apply hyp <;> simp [free_in_aexp]; apply Or.inr; assumption; apply Or.inl; assumption


#check "hello"
/-
Proof.
  induction a; cbn; intros SAMEFREE.
- /- Case a = CONST n -/
  auto.
- /- Case a = VAR x -/
  apply SAMEFREE. auto.
- /- Case a = PLUS a1 a2 -/
  rewrite IHa1, IHa2. auto. auto. auto.
- /- Case a = MINUS a1 a2 -/
  rewrite IHa1, IHa2; auto.
Qed.

/-* *** Exercise (1 star, recommended). -/
/-* Add support for multiplication in arithmetic expressions.
  Modify the [aexp] type and the [aeval] function accordingly. -/

/-* *** Exercise (2 stars, recommended). -/
/-* Add support for division and for detecting arithmetic overflow.
  With this extension, the evaluation of an expression can produce an
  error: integer division by zero or result that exceeds the range
  [[min_int, max_int]].  You can either change the type of the
  function [aeval] to
<<
  aeval: store -> aexp -> option Z
>>
  with [None] meaning "error" and [Some n] meaning "success with
  result n".  Alternatively, you can define the semantics as a
  relation instead of a function:
<<
  Inductive aeval_rel: store -> aexp -> Z -> Prop := ...
>>
  Some definitions you can use:
-/
-/

#check Int.pow
def min_int := - ((2 : Int) ^ 63)
def max_int := (2 : Int) ^ 63 - 1
def check_for_overflow (n: Int): Option Int :=
  if n < min_int then none else if n > max_int then none else some n

#eval (check_for_overflow 2222222222222222222)

/-
/-* ** 1.3 Boolean expressions -/

/-* The IMP language has conditional statements (if/then/else) and
  loops.  They are controlled by expressions that evaluate to Boolean
  values.  Here is the abstract syntax of Boolean expressions. -/

-/
inductive bexp : Type :=
  | TRUE                         --     /-*r always true -/
  | FALSE                          --   /-*r always false -/
  | EQUAL (a1: aexp) (a2: aexp)     --  /-*r whether [a1 = a2] -/
  | LESSEQUAL (a1: aexp) (a2: aexp) --  /-*r whether [a1 <= a2] -/
  | NOT (b1: bexp)                  --  /-*r Boolean negation -/
  | AND (b1: bexp) (b2: bexp)      --  /-*r Boolean conjunction -/
/-
/-* Just like arithmetic expressions evaluate to integers,
  Boolean expressions evaluate to Boolean values [true] or [false]. -/
-/
open bexp
def beval (s: store) (b: bexp) : Bool :=
  match b with
  | TRUE => true
  | FALSE => false
  | EQUAL a1 a2 => aeval s a1 == aeval s a2
  | LESSEQUAL a1 a2 => aeval s a1 <= aeval s a2
  | NOT b1 => not (beval s b1)
  | AND b1 b2 => beval s b1 && beval s b2

-- /-* There are many useful derived forms. -/

def NOTEQUAL (a1 a2: aexp) : bexp := NOT (EQUAL a1 a2)

def GREATEREQUAL (a1 a2: aexp) : bexp := LESSEQUAL a2 a1

def GREATER (a1 a2: aexp) : bexp := NOT (LESSEQUAL a1 a2)

def LESS (a1 a2: aexp) : bexp := GREATER a2 a1

def OR (b1 b2: bexp) : bexp := NOT (AND (NOT b1) (NOT b2))

-- /- * *** Exercise (1 star, recommended) -/
-- /- * Show the expected semantics for the [OR] derived form: -/

lemma beval_OR :
  forall s b1 b2, beval s (OR b1 b2) = (beval s b1 || beval s b2) := by
  intros s b1 b2
  simp [beval]
  --rw [Bool.not_and]
  --library_search
  cases (beval s b1) <;> cases (beval s b2) <;> simp
  


  
  
/-
Proof.
  intros; cbn.
  /- Hint: do "SearchAbout negb" to see the available lemmas about Boolean negation. -/
  /- Hint: or just do a case analysis on [beval s b1] and [beval s b2], there are
     only 4 cases to consider. -/
  /- FILL IN HERE -/
Abort.
-/
/-* ** 1.4 Commands -/

/-* To complete the definition of the IMP language, here is the
  abstract syntax of commands, also known as statements. -/

inductive com: Type :=
  | SKIP                                     /-*r do nothing -/
  | ASSIGN (x: ident) (a: aexp)              /-*r assignment: [v := a] -/
  | SEQ (c1: com) (c2: com)                  /-*r sequence: [c1; c2] -/
  | IFTHENELSE (b: bexp) (c1: com) (c2: com) /-*r conditional: [if b then c1 else c2] -/
  | WHILE (b: bexp) (c1: com)               /-*r loop: [while b do c1 done] -/

/-* We can write [c1 ;; c2] instead of [SEQ c1 c2], it is easier on the eyes. -/

infixr:80 ";;" => com.SEQ -- (at level 80, right associativity).

/-* Here is an IMP program that performs Euclidean division by
  repeated subtraction.  At the end of the program, "q" contains
  the quotient of "a" by "b", and "r" contains the remainder.
  In pseudocode:
<<
       r := a; q := 0;
       while b <= r do r := r - b; q := q + 1 done
>>
  In abstract syntax:
-/
open com
def Euclidean_division :=
  ASSIGN "r" (VAR "a") ;;
  ASSIGN "q" (CONST 0) ;;
  WHILE (LESSEQUAL (VAR "b") (VAR "r"))
    (ASSIGN "r" (MINUS (VAR "r") (VAR "b")) ;;
     ASSIGN "q" (PLUS (VAR "q") (CONST 1)))

/-* A useful operation over stores:
    [update x v s] is the store that maps [x] to [v] and is equal to [s] for
    all variables other than [x]. -/
#print ident
#print store
def update (x: ident) (v: Int) (s: store) : store :=
  fun y => if x == y then v else s y

/-* A naive approach to giving semantics to commands is to write an
  evaluation function [cexec s c] that runs the command [c] in initial
  store [s] and returns the final store when [c] terminates. -/

-- Lean accepts this deftion with the unsafe keyword
unsafe def cexec' (s: store) (c: com) : store :=
  match c with
  | SKIP => s
  | ASSIGN x a => update x (aeval s a) s
  | SEQ c1 c2 => let s' := cexec' s c1
                 cexec' s' c2
  | IFTHENELSE b c1 c2 => if beval s b then cexec' s c1 else cexec' s c2
  | WHILE b c1 =>
      if beval s b
      then (let s' := cexec' s c1
            cexec' s' (WHILE b c1))
      else s
  

/-* The definition above is rejected by Coq, and rightly so, because
  all Coq functions must terminate, yet the [WHILE] case may not
  terminate.  Consider for example the infinite loop [WHILE TRUE
  SKIP].

  Worse, IMP is Turing-complete, since it has unbounded iteration
  ([WHILE]) plus arbitrary-precision integers.  Hence, there is no
  computable function [cexec s c] that would return [Some s'] if [c]
  terminates with store [s'], and [None] if [c] does not terminate.

  However, instead of computable functions, we can use a relation
  [cexec s c s'] that holds iff command [c], started in state [s],
  terminates with state [s'].  This relation can easily be defined as
  a Coq inductive predicate:
-/

inductive cexec: store -> com -> store -> Prop where
  | cexec_skip: forall s,
      cexec s SKIP s
  | cexec_assign: forall s x a,
      cexec s (ASSIGN x a) (update x (aeval s a) s)
  | cexec_seq: forall c1 c2 s s' s'',
      cexec s c1 s' -> cexec s' c2 s'' ->
      cexec s (SEQ c1 c2) s''
  | cexec_ifthenelse: forall b c1 c2 s s',
      cexec s (if beval s b then c1 else c2) s' ->
      cexec s (IFTHENELSE b c1 c2) s'
  | cexec_while_done: forall b c s,
      beval s b = false ->
      cexec s (WHILE b c) s
  | cexec_while_loop: forall b c s s' s'',
      beval s b = true -> cexec s c s' -> cexec s' (WHILE b c) s'' ->
      cexec s (WHILE b c) s''

/-* This style of semantics is known as natural semantics or big-step
  operational semantics.  The predicate [cexec s c s'] holds iff there
  exists a finite derivation of this conclusion, using the axioms and
  inference rules above.  The structure of the derivation represents
  the computations performed by [c] in a tree-like manner.  The
  finiteness of the derivation guarantees that only terminating
  executions satisfy [cexec].  Indeed, [WHILE TRUE SKIP] does not
  satisfy [cexec]: 
-/


lemma cexec_infinite_loop:
  forall s, ¬ exists s', cexec s (WHILE TRUE SKIP) s':= by
  sorry
  /-
  assert (A: forall s c s', cexec s c s' -> c = WHILE TRUE SKIP -> False).
  { induction 1; intros EQ; inversion EQ.
  - subst b c. cbn in H. discriminate.
  - subst b c. apply IHcexec2. auto.
  }
  intros s (s' & EXEC). apply A with (s := s) (c := WHILE TRUE SKIP) (s' := s'); auto.
Qed.
-/

/-* Our naive idea of an execution function for commands was not
  completely off.  We can define an approximation of such a function
  by bounding a priori the recursion depth, using a [fuel] parameter
  of type [nat].  When the fuel drops to 0, [None] is returned,
  meaning that the final store could not be computed. -/
#check Option
def cexec_bounded (fuel: Nat) (s: store) (c: com) : Option store :=
  match fuel with
  | .zero => none
  | .succ fuel' =>
      match c with
      | SKIP => some s
      | ASSIGN x a => some (update x (aeval s a) s)
      | SEQ c1 c2 =>
          match cexec_bounded fuel' s c1 with
          | none  => none
          | some s' => cexec_bounded fuel' s' c2
          
      | IFTHENELSE b c1 c2 =>
          if beval s b then cexec_bounded fuel' s c1 else cexec_bounded fuel' s c2
      | WHILE b c1 =>
          if beval s b then
            match cexec_bounded fuel' s c1 with
            | none  => none
            | some s' => cexec_bounded fuel' s' (WHILE b c1)
            
          else some s
      
  

/-* This bounded execution function is great for testing programs.
    For example, let's compute the quotient and the remainder of 14 by
    3 using the Euclidean division program above. -/

#eval (let s := update "a" 14 (update "b" 3 (fun _ => 0))
       match cexec_bounded 100 s Euclidean_division with
       | none => none
       | some s' => some (s' "q", s' "r")
   )

/-* *** Exercise (3 stars, optional) -/
/-* Relate the [cexec] relation with the [cexec_bounded] function by
  proving the following two lemmas. -/

lemma cexec_bounded_sound:
  forall fuel s c s', cexec_bounded fuel s c = some s' -> cexec s c s' := by
  induction fuel as [ | fuel ]; cbn; intros.
- discriminate.
- destruct c.
  /- FILL IN HERE -/
Abort.

lemma cexec_bounded_complete:
  forall s c s', cexec s c s' ->
  exists fuel1, forall fuel, (fuel >= fuel1)%nat -> cexec_bounded fuel s c = Some s'.
Proof.
  induction 1.
  /- FILL IN HERE -/
Abort.

/-* * 6. Small-step semantics for IMP -/

/-* * 6.1 Reduction semantics -/

/-* In small-step style, the semantics is presented as a one-step
  reduction relation [ red (c, s) (c', s') ], meaning that the command
  [c], executed in initial state [s], performs one elementary step of
  computation.  [s'] is the updated state after this step.  [c'] is
  the residual command, capturing all the computations that remain to
  be done.  -/

inductive red: com * store -> com * store -> Prop where
  | red_assign: forall x a s,
      red (ASSIGN x a, s) (SKIP, update x (aeval s a) s)
  | red_seq_done: forall c s,
      red (SEQ SKIP c, s) (c, s)
  | red_seq_step: forall c1 c s1 c2 s2,
      red (c1, s1) (c2, s2) ->
      red (SEQ c1 c, s1) (SEQ c2 c, s2)
  | red_ifthenelse: forall b c1 c2 s,
      red (IFTHENELSE b c1 c2, s) ((if beval s b then c1 else c2), s)
  | red_while_done: forall b c s,
      beval s b = false ->
      red (WHILE b c, s) (SKIP, s)
  | red_while_loop: forall b c s,
      beval s b = true ->
      red (WHILE b c, s) (SEQ c (WHILE b c), s).

/-* *** Exercise (2 stars, recommended) -/
/-* Show that Imp programs cannot go wrong.  Hint: first prove the following
  "progress" result for non-[SKIP] commands. -/

lemma red_progress:
  forall c s, c = SKIP \/ exists c', exists s', red (c, s) (c', s').
Proof.
  induction c; intros.
  /- FILL IN HERE -/
Abort.

def goes_wrong (c: com) (s: store) : Prop :=
  exists c', exists s',
  star red (c, s) (c', s') /\ irred red (c', s') /\ c' <> SKIP.

lemma not_goes_wrong:
  forall c s, ~(goes_wrong c s).
Proof.
  intros c s (c' & s' & STAR & IRRED & NOTSKIP).
  /- FILL IN HERE -/
Abort.

/-* Sequences of reductions can go under a sequence context, generalizing
  rule [red_seq_step]. -/

lemma red_seq_steps:
  forall c2 s c s' c',
  star red (c, s) (c', s') -> star red ((c;;c2), s) ((c';;c2), s').
Proof.
  intros. dependent induction H.
- apply star_refl.
- destruct b as [c1 st1].
  apply star_step with (c1;;c2, st1). apply red_seq_step. auto. auto.  
Qed.

/-* We now recall the equivalence result between 
- termination according to the big-step semantics
- existence of a finite sequence of reductions to [SKIP]
  according to the small-step semantics.

We start with the implication big-step ==> small-step, which is
a straightforward induction on the big-step evaluation derivation. -/

Theorem cexec_to_reds:
  forall s c s', cexec s c s' -> star red (c, s) (SKIP, s').
Proof.
  induction 1.
- /- SKIP -/
  apply star_refl.
- /- ASSIGN -/
  apply star_one. apply red_assign. 
- /- SEQ -/
  eapply star_trans. apply red_seq_steps. apply IHcexec1.
  eapply star_step.  apply red_seq_done.  apply IHcexec2.
- /- IFTHENELSE -/
  eapply star_step. apply red_ifthenelse. auto.
- /- WHILE stop -/
  apply star_one. apply red_while_done. auto.
- /- WHILE loop -/
  eapply star_step. apply red_while_loop. auto.
  eapply star_trans. apply red_seq_steps. apply IHcexec1.
  eapply star_step. apply red_seq_done. apply IHcexec2.
Qed.

/-* The reverse implication, from small-step to big-step, is more subtle.
The key lemma is the following, showing that one step of reduction
followed by a big-step evaluation to a final state can be collapsed
into a single big-step evaluation to that final state. -/

lemma red_append_cexec:
  forall c1 s1 c2 s2, red (c1, s1) (c2, s2) ->
  forall s', cexec s2 c2 s' -> cexec s1 c1 s'.
Proof.
  intros until s2; intros STEP. dependent induction STEP; intros.
- /- red_assign -/
  inversion H; subst. apply cexec_assign. 
- /- red_seq_done -/
  apply cexec_seq with s2. apply cexec_skip. auto.
- /- red seq step -/
  inversion H; subst. apply cexec_seq with s'0.
  eapply IHSTEP; eauto.
  auto.
- /- red_ifthenelse -/
  apply cexec_ifthenelse. auto.
- /- red_while_done -/
  inversion H0; subst. apply cexec_while_done. auto.
- /- red while loop -/
  inversion H0; subst. apply cexec_while_loop with s'0; auto.
Qed.

/-* As a consequence, a term that reduces to [SKIP] evaluates in big-step
  with the same final state. -/

Theorem reds_to_cexec:
  forall s c s',
  star red (c, s) (SKIP, s') -> cexec s c s'.
Proof.
  intros. dependent induction H.
- apply cexec_skip.
- destruct b as [c1 s1]. apply red_append_cexec with c1 s1; auto.
Qed.

/-* ** 6.2 Transition semantics with continuations -/

/-* We now introduce an alternate form of small-step semantics
  where the command to be executed is explicitly decomposed into:
- a sub-command under focus, where computation takes place;
- a continuation (or context) describing the position of this sub-command
  in the whole command, or, equivalently, describing the parts of the
  whole command that remain to be reduced once the sub-command is done.

As a consequence, the small-step semantics is presented as a
transition relation between triples (subcommand-under-focus,
continuation, state).  Previously, we had transitions between pairs
(whole-command, state).

The syntax of continuations is as follows:
-/

inductive cont : Type :=
  | Kstop
  | Kseq (c: com) (k: cont)
  | Kwhile (b: bexp) (c: com) (k: cont).

/-* Intuitive meaning of these constructors:
- [Kstop] means that, after the sub-command under focus terminates,
  nothing remains to be done, and execution can stop.  In other words,
  the sub-command under focus is the whole command.
- [Kseq c k] means that, after the sub-command terminates, we still need
  to execute command [c] in sequence, then continue as described by [k].
- [Kwhile b c k] means that, after the sub-command terminates, we still need
  to execute a loop [WHILE b DO c END], then continue as described by [k].
-/

/-* Another way to forge intuitions about continuations is to ponder the following
  [apply_cont k c] function, which takes a sub-command [c] under focus
  and a continuation [k], and rebuilds the whole command.  It simply
  puts [c] in lefmost position in a nest of sequences as described by [k].
-/

def apply_cont (k: cont) (c: com) : com :=
  match k with
  | Kstop => c
  | Kseq c1 k1 => apply_cont k1 (SEQ c c1)
  | Kwhile b1 c1 k1 => apply_cont k1 (SEQ c (WHILE b1 c1))
  

/-* Transitions between (subcommand-under-focus, continuation, state)
  triples perform conceptually different kinds of actions:
- Computation: evaluate an arithmetic expression or boolean expression
  and modify the triple according to the result of the evaluation.
- Focusing: replace the sub-command by a sub-sub-command that is to be
  evaluated next, possibly enriching the continuation as a consequence.
- Resumption: when the sub-command is [SKIP] and therefore fully executed,
  look at the head of the continuation to see what to do next.

Here are the transition rules, classified by the kinds of actions they implement.
-/

inductive step: com * cont * store -> com * cont * store -> Prop :=

  | step_assign: forall x a k s,              /-*r computation for assignments -/
      step (ASSIGN x a, k, s) (SKIP, k, update x (aeval s a) s)

  | step_seq: forall c1 c2 s k,               /-*r focusing for sequence -/
      step (SEQ c1 c2, k, s) (c1, Kseq c2 k, s)

  | step_ifthenelse: forall b c1 c2 k s,      /-*r computation for conditionals -/
      step (IFTHENELSE b c1 c2, k, s) ((if beval s b then c1 else c2), k, s)

  | step_while_done: forall b c k s,          /-*r computation for loops -/
      beval s b = false ->
      step (WHILE b c, k, s) (SKIP, k, s)

  | step_while_true: forall b c k s,          /-*r computation and focusSKIing for loops -/
      beval s b = true ->
      step (WHILE b c, k, s) (c, Kwhile b c k, s)

  | step_skip_seq: forall c k s,              /-*r resumption -/
      step (SKIP, Kseq c k, s) (c, k, s)

  | step_skip_while: forall b c k s,          /-*r resumption -/
      step (SKIP, Kwhile b c k, s) (WHILE b c, k, s).


/-* *** Extensions to other control structures -/

/-* A remarkable feature of continuation semantics is that they extend very easily
  to other control structures besides "if-then-else" and "while" loops.
  Consider for instance the "break" construct of C, C++ and Java, which
  immediately terminates the nearest enclosing "while" loop.  Assume we
  extend the type of commands with a [BREAK] constructor.  Then, all we need
  to give "break" a semantics is to add two resumption rules:
<<
  | step_break_seq: forall c k s,
      step (BREAK, Kseq c k, s) (BREAK, k, s)
  | step_break_while: forall b c k s,
      step (BREAK, Kwhile b c k, s) (SKIP, k, s)
>>
  The first rule says that a [BREAK] statement "floats up" pending sequences,
  skipping over the computations they contain.  Eventually, a [Kwhile]
  continuation is encountered, meaning that the [BREAK] found its enclosing
  loop.  Then, the second rule discards the [Kwhile] continuation and
  turns the [BREAK] into a [SKIP], effectively terminating the loop.
  That's all there is to it!
*-/

/-* *** Exercise (2 stars, recommended) -/
/-* Besides "break", C, C++ and Java also have a "continue" statement
  that terminates the current iteration of the enclosing loop,
  then resumes the loop at its next iteration (instead of stopping
  the loop like "break" does). Give the transition rules
  for the "continue" statement. -/

/-* *** Exercise (3 stars, optional) -/
/-* In Java, loops as well as "break" and "continue" statements carry
  an optional label.  "break" without a label exits out of the immediately
  enclosing loop, but "break lbl" exits out of the first enclosing loop
  that carries the label "lbl".  Similarly for "continue".
  Give the transition rules for "break lbl" and "continue lbl". -/

/-* *** Relating the continuation semantics and the big-step semantics -/

/-* *** Exercise (2 stars, optional) -/
/-* Show that a big-step execution give rise to a sequence of steps to [SKIP].
  You can adapt the proof of theorem [cexec_to_reds] with minor changes. -/

Theorem cexec_to_steps:
  forall s c s', cexec s c s' -> forall k, star step (c, k, s) (SKIP, k, s').
Proof.
  induction 1; intros k.
  /- FILL IN HERE -/
Abort.

/-* *** Exercise (3 stars, optional) -/
/-* Show the converse result: a sequence of steps to [(SKIP, Kstop)] corresponds
  to a big-step execution.  You need a lemma similar to [red_append_cexec],
  but also a notion of big-step execution of a continuation. -/

Theorem steps_to_cexec:
  forall c s s', star step (c, Kstop, s) (SKIP, Kstop, s') -> cexec s c s'.
Proof.
  /- FILL IN HERE -/
Abort.