Lean
- Logic and Mechanical Reasoning Logic and Mechanized Reasoning
- Theorem proving in lean4
- functional programming in lean Christianson
Theorem prover lab: applications in programming languages
Lambda the Ultimate SSA: Optimizing Functional Programs in SSA
Numerical packages in lean
- numlean
- lean karray
- https://github.com/lecopivo/SciLean Webserver example. Custom syntax 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 4 Advent of Code 2021
- lean4 raytracer
- balance car
- lean 4 manual
- theorme prover lab
- MA 208: Proof and Programs
- lean learning group Aesop (Automated Extensible Search for Obvious Proofs) i
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
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
https://github.com/ccodel/verified-encodings
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
discrimination tree disctree types
IR - somehow this is what I need to look at to implement new backend?
Stuff
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
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.