EECS 762

An introduction to mechanized language semantics using Rocq and Software Foundations.

https://perry.alexander.name/eecs762

Formatted using Markdown and Marp for VS Code

Date: 2026-01-20

Formal Systems

• Syntax - language structure
  • Alphabet - atomic symbols
  • Grammar - rules defining well-formed formulas (wffs)
• Inference system - immediate consequences of wffs
  • Axioms - wffs assumed true without proof
  • Inference Rules - wffs that follow immediately from other wffs
• Semantics - mapping from wffs to their meanings
  • Evaluation Relation - defines wff evaluation
  • Typing Relation - defines wff static typing

All formal Systems ultimately define the semantics of a language

Mechanisms for defining semantics

• Axiomatic - Floyd & Hoare, Gries
  • Pre- and post-conditions and Invariants ($\lbrace Q\rbrace P\lbrace R\rbrace$)
  • Composition with Floyd-Hoare logic
• Denotational Semantics - Scott & Strachey, Schmidt
  • Lambda calculus
  • Domain theory
  • Denotation functions ($\denotes{t}{\sigma}=v$)
• Operational Semantics - Pierce
  • Define evaluation ($t\rightarrow t’$) and typeof ($t:T$) directly
  • Large step (natural) semantics ($t\Downarrow v$)
  • Small step semantics ($t\rightarrow t’$)

What we will learn this semester

• Program Equivalence
  • Bisimulation
• Hoare Logic ($\hoare{Q}{P}{R}$)
  • Hoare triples
• Small Step Operational Semantics ($t \rightarrow t’$)
  • $t$ evaluates to $t’$ in one-step
• Typing relation ($t : T$)
  • $t$ is of type $T$

What we will prove

• Program Equivalence
• Sequencing of Hoare triples
• Loop invariants
• Type Safety = Progress and Preservation
• Correctness of compilers and interpreters

Our Target Language - IMP

The most over-analyzed programming language in existence.

• Classical imperative programming language
• Arithmetic and boolean expressions
• Sequencing
• Mutable variables and assignment
• if and while
• No functions or recursion
• No types
• Turing complete

Example: Sequential Factorial

Z := X;
Y := 1;
while Z <> 0 do
  Y := Y * Z;
  Z := Z - 1
end

• Most IMP features

Un-mechanized Concrete Syntax

a := nat
  | a + a
  | a - a
  | a * a
  | id

b := true
  | false
  | a = a
  | a <> a
  | a <= a
  | a > a
  | ~b
  | b && b

c := skip
  | c ; c
  | v := a
  | if b then c else c end
  | while b do c end

Mechanized in Abstract Syntax in Rocq

Inductive aexp : Type :=
  | ANum (n : nat)
  | AId (x : string)
  | APlus (a1 a2 : aexp)
  | AMinus (a1 a2 : aexp)
  | AMult (a1 a2 : aexp).

Inductive bexp : Type :=
  | BTrue
  | BFalse
  | BEq (a1 a2 : aexp)
  | BNeq (a1 a2 : aexp)
  | BLe (a1 a2 : aexp)
  | BGt (a1 a2 : aexp)
  | BNot (b : bexp)
  | BAnd (b1 b2 : bexp).

Inductive com : Type :=
  | CSkip
  | CAsgn (x : string) (a : aexp)
  | CSeq (c1 c2 : com)
  | CIf (b : bexp) (c1 c2 : com)
  | CWhile (b : bexp) (c : com).

Mechanized Abstract Syntax

• Abstract Syntax captured in an inductive type
• This is a data structure
• We can do things with data structures
• We’d rather not write data structures

Parsing Concrete Syntax

Rocq provides nifty notations for parsing to abstract syntax.

<{ Z := X;
   Y := 1;
   while Z <> 0 do
     Y := Y × Z;
     Z := Z - 1
   end }>

<{ concrete syntax }> -> abstract syntax

Computational Evaluation

Fixpoint aeval (a : aexp) : nat :=
  match a with
  | ANum n => n
  | APlus  a1 a2 => (aeval a1) + (aeval a2)
  | AMinus a1 a2 => (aeval a1) - (aeval a2)
  | AMult  a1 a2 => (aeval a1) * (aeval a2)
  end.

Example Proof

Example test_aeval1:
  aeval (APlus (ANum 2) (ANum 2)) = 4.
Proof. reflexivity. Qed.

Happier Example Proof

Example test_aeval1:
  aeval <{ 2 + 2 }> = 4.
Proof. reflexivity. Qed.

Booleans work the same way

Fixpoint beval (b : bexp) : bool :=
  match b with
  | BTrue       => true
  | BFalse      => false
  | BEq a1 a2   => (aeval a1) =? (aeval a2)
  | BNeq a1 a2  => negb ((aeval a1) =? (aeval a2))
  | BLe a1 a2   => (aeval a1) <=? (aeval a2)
  | BGt a1 a2   => negb ((aeval a1) <=? (aeval a2))
  | BNot b1     => negb (beval b1)
  | BAnd b1 b2  => andb (beval b1) (beval b2)
  end.

• Note that beval calls aeval

Example test_aeval1:
  aeval <{ true && (1 < 3) }> = true.
Proof. reflexivity. Qed.

State

Functional programs transform terms into values

fact n = if n=0 then 1 else n * (fact n-1)

• fact is simply a function that is equal to a mathematical expression
• Simplify fact n to get a value
• Can do this by substitution of n-1 into fact
• We like this when reasoning about programs

but not much code is written functionally

Imperative programs transform state

<{ Z := X;
   Y := 1;
   while Z <> 0 do
     Y := Y × Z;
     Z := Z - 1
   end }>

• Z := X - replaces the value of Z in program state with the value of X
• while Z<>0 do C - checks the value of Z in state and repeats or does not repeat C
• C1 ; C2 - feeds the state resulting from C1 into C2

The only reason for [state] is so that everything does not happen at once Buckaroo Banzai

Programs as State Transformation Systems

• Remember automata theory?
• ceval : State -> State is a next state function over State
• Defining program execution this way is powerful
  • patterns in state sequences
  • reachability
  • preconditions, post-conditions
  • invariants
  • Hoare Logic, Separation Logic, Linear Temporal Logic, …
  • Lots of automated tools
• What’s a program state?

Date: 2026-01-22

Programs as State Transformation Systems (cont)

<{ Z := X; <st = ??>
   Y := 1; <st = ??>
   while Z <> 0 do 
     Y := Y × Z; <st = ??>
     Z := Z - 1  <st = ??>
   end }> <st = ??>

• Can we construct a state machine?
• Can we say anything interesting?
• Will automata theory inform us?

Total Maps - Representing State

• A mapping from strings to values
• In Rocq we have Maps.v given to us

Model maps as a function from string to some type A

Definition total_map (A:Type) := string -> A.`

• The range type for the map is specified as A
• The domain type for the map is string

Empty Maps

An empty map returns the same default value for all inputs.

Definition t_empty {A:Type} (v : A) : total_map A := (fun _ => v)

• Function accepts anything as input
• Returns v, the default value
• A can be inferred from v

Nonempty Maps

Update a map by updating its function

Definition t_update {A:Type} (m : total_map A) (x : string) (v : A) :=
  fun x' => if String.eqb x x' then v else (m x').

• New function constructed from x:string and v:A
• Returns v if x is the input
• Returns m x' if x is not the input

Map Access

Just call the map as a function to access a value

(m x)

• x is the string being accessed
• m is the map function

Program State as Map

Program state is a total map over nat

• State := total_map nat

Initial state is the empty map over 0

• t_empty 0 - initial state

Update state with t_update

• t_update st "name" v - updating state

Access with function call

• st "name" - variable access

Theorems and Notations

Rocq provides some nifty notations:

• __ !-> v - initial mapping with v as default value
• "name" !-> v ; m - update "name" with v in m

Mathematically $(x \mapsto v);m$ or $(x,v);m$

States as Maps

• __|->0 - initial state over 0
• "x" !-> 3 ; __|->0 - assign 3 to “x”
• "y" !-> 4 ; "x" !-> 3 ; __|->0 - assign 3 to “x”, 4 to “y”
• "x" !-> 4 ; "y" !-> 4 ; "x" !-> 3 ; __|->0 - assign 3 to “x”, 4 to “y”, 4 to “x”

Examples Usage

• X = (st "X")
• X := 3 = (X |-> 3 ; st)
• X := X+1 = (X |-> ((st "X") + 1) ; st)

Switch to Rocq and prove some theorems over total maps

Watch for:

• %string directive
• functional_extensionality theorem
• unfolding notations
• finding and using built in theorems

2026-01-27

Now ceval for commands

Fixpoint ceval (st : state) (c : com) : state :=
  match c with
    | <{ skip }> =>
        st
    | <{ x := a }> =>
        (x !-> aeval st a ; st)
    | <{ c1 ; c2 }> =>
        let st' := ceval st c1 in
        ceval st' c2
    | <{ if b then c1 else c2 end}> =>
        if (beval st b)
          then ceval st c1
          else ceval st c2
    | <{ while b do cb end }> =>
        if (beval st b)
           then st
           else (ceval (ceval st cb) c)
  end.

Yay

• Program execution transforms the current state
• Defines a next state function
• With program state as automata state
• And commands as input

In st we execute c resulting in st'

Not Yay

• All functions in Rocq must terminate
  • Rocq will usually figure this out for you
  • Rocq will punish you if it can’t
• Why?
  • Rocq’s logic plus a nonterminating function is inconsistent
  • You can prove false
  • From false you can prove anything

Calling ceval on this program terminates

<{ Z := X;
   Y := 1;
   while Z <> 0 do
     Y := Y * Z;
     Z := Z - 1
   end }>

But this one does not

<{ Z := X;
   Y := 1;
   while Z <> 0 do
     Y := Y * Z;
     Z := Z + 1
   end }>

Evaluating while Badly

• ceval would seem to implement a recursive function just like beval and aeval

    | <{ while b do cb end }> =>
        if (beval st b)
        then st
        else (ceval (ceval st cb) c)

• What’s the difference?

Make ceval Terminate

Fixpoint ceval (fuel: nat) (st : state) (c : com) : state :=
  match fuel with
  | 0 => empty
  | succ fuel' =>
      match c with
        | <{ skip }> =>
            st
        | <{ x := a }> =>
            (x !-> aeval fuel st a ; st)
        | <{ c1 ; c2 }> =>
            let st' := ceval fuel' st c1 in
              ceval fuel' st' c2
        | <{ if b then c1 else c2 end}> =>
            if (beval st b) then ceval fuel' st c1
              else ceval fuel' st c2
        | <{ while b do cb end }> =>
            if (beval st b) then st
              else (ceval fuel' (ceval fuel' st cb) c)
  end
end.

Fuel

• The new fuel parameter gets smaller on every call
• Rocq easily determines this function terminates
  • fuel decreases on every call
  • nat is a recursive type with a bottom
• Kinda cheesy, but effective
  • Common in industrial verification
  • There is always a fuel big enough

Relations

• Evaluation relation rather than an evaluation function.
• An evaluation relation
  • Need not be total
  • Need not terminate
  • Need not be deterministic
• We can define the properties we want and stop

Relations in Math

• A relation $R$ over two sets $X$ and $Y$ is a set of ordered pairs:

• We say $R(x,y)=true$ if $(x,y)\in R$ and $false$ otherwise.
• The notation $xRy \equiv R(x,y)$
• If $X=Y$ then $R$ is homogeneous

• Relations have a ton of properties that we’ll talk about later

• An evaluation relation type might be defined:

Definition Examples

Three ways of saying “given A and B we know C”

$\frac{A,B}{C}$ - Tree style

$A,B \vdash C$ - Flat style

A -> B -> C - Rocq style

Properties of Relations

• Reflexive - $\forall a \cdot a R a$
• Transitive - $\forall a b c \cdot a R b \wedge b R c \Rightarrow a R c$
• Symmetric - $\forall a b \cdot a R b \Rightarrow b R a$
• Antisymmetric - $\forall a b \cdot a R b\wedge b R a \Rightarrow a = b$
• Equivalence - Reflexive, Transitive, and Symmetric
• Partial Order - Reflexive, Transitive, Antisymmetric
• Lots and lots more, usually encoded in the Rocq standard libraries

2026-01-27

Evaluation Relation Examples

forall v, aevalR(ANum(v),v)

forall t1 t2 v1 v2, aevalR(t1,v1) -> aevalR(t2,v2) -> aevalR(t1+t2,v1+v2)

forall t1 t2 v1 v2, aevalR(t1,v1) -> aevalR(t2,v2) -> bevalR(t1=t2,v1=?v2)

forall t1 t2 v1 v2,
  bevalR(t1,v1) -> bevalR(t2,v2) -> bevalR(t1 && t2,(andb v1 v2))

forall c1 c2 st st' st'',
  cevalR(st,c1,st') -> cevalR(st',c2,st'') -> cevalR(st,c1;c2,st'')

Inductive Propositions in Rocq

Inductive aevalR: aexp -> nat -> Prop :=
| aevalNum : forall v : nat, (aevalR (ANum v) v) -> True
| aevalPlus : forall t1 t2 v1 v2,
    (aevalR t1 v1) -> (aevalR t2 v2) -> (aevalR (APlus t1 t2) (v1+v2)) -> True
| aevalTimes : forall t1 t2 v1 v2,
    (aevalR t1 v1) -> (aevalR t2 v2) -> (aevalR (AMult t1 t2) (v1*v2)) -> True
| aevalMinus : forall t1 t2 v1 v2,
    (aevalR t1 v1) -> (aevalR t2 v2) -> v1 <= v2 -> (aevalR (AMinus t1 t2) (v1-v2)) -> True.

• This is an inductive proposition defining big step evaluation
• Each aexp -> nat -> Prop is an evidence constructor defining when an ordered pair is in the relation
• aevalR is the smallest relation satisfying all evidence constructors
• Evidence constructors are also useful as inference rules with apply

Inductive Propositions in Rocq (cont)

Inductive aevalR: aexp -> nat -> Prop :=
| aevalNum : forall v : nat, (aevalR (ANum v) v)
| aevalPlus : forall t1 t2 v1 v2,
    (aevalR t1 v1) -> (aevalR t2 v2) -> (aevalR (APlus t1 t2) (v1+v2))
| aevalTimes : forall t1 t2 v1 v2,
    (aevalR t1 v1) -> (aevalR t2 v2) -> (aevalR (AMult t1 t2) (v1*v2))
| aevalMinus : forall t1 t2 v1 v2,
    (aevalR t1 v1) -> (aevalR t2 v2) -> v1 <= v2 -> (aevalR (AMinus t1 t2) (v1-v2)).

• The True values are redundant.

Reasoning With Apply

Reasoning with Inversion

Adding State to aeval

Fixpoint aeval (st : state) (* <--- NEW *)
               (a : aexp) : nat :=
  match a with
  | ANum n => n
  | AId x => st x                                (* <--- NEW *)
  | <{a1 + a2}> => (aeval st a1) + (aeval st a2)
  | <{a1 - a2}> => (aeval st a1) - (aeval st a2)
  | <{a1 * a2}> => (aeval st a1) * (aeval st a2)
  end.

• Adding state to aeval and beval simple
• AId abstract syntax
• (AId x) dereferencing

Example aeval State

Definition init := (t_empty 0).
Definition st := (t_update init "X" 3).

Example ex4: aeval st (AId X) = 3.
Proof.

Adding State to aevalR

Inductive aevalR: state -> aexp -> nat -> Prop :=
| aevalNum : forall st : state, v : nat, (aevalR st (ANum v) v)
| aevalId : forall st : state, x : string, (aevalR st (AId x) (st x))
| aevalPlus : forall st t1 t2 v1 v2,
    (aevalR st t1 v1) -> (aevalR st t2 v2) -> (aevalR st (APlus t1 t2) (v1+v2))
| aevalTimes : forall st t1 t2 v1 v2,
    (aevalR st t1 v1) -> (aevalR st t2 v2) -> (aevalR st (AMult t1 t2) (v1*v2))
| aevalMinus : forall st t1 t2 v1 v2,
    (aevalR st t1 v1) -> (aevalR st t2 v2) -> v1 <= v2 -> (aevalR (AMinus st t1
    t2) (v1-v2)).

• Again, add state to aevalR and bevalR
• AId definition
• (AId x) dereferencing.

Example aevalR and aeval with State

Switch to Rocq

Let’s Try com

Inductive com : Type :=
  | CSkip
  | CAsgn (x : string) (a : aexp)
  | CSeq (c1 c2 : com)
  | CIf (b : bexp) (c1 c2 : com)
  | CWhile (b : bexp) (c : com).

• aexp and bexp are different from com
• States are transformed to states by com instances

ceval : s -> com -> s'

st=[c]=>st'

Rocq Notation

ceval st c st'  == st=[c]=>st'

• c transforms st into st'

Skip

-----------
st =[SKIP]=> st

• SKIP skips and does nothing

Assign

    aevalR st t v
-------------------------
st =[ x:=t ]=> (x|->v);st

• evaluate t to v
• add x bound to v

Sequence

        st =[c1]=> st'
       st' =[c2]=> st''
--------------------------------
      st =[c1;c2]=> st''

• Evaluate c1 in st to get st'
• Evaluate c2 in st' to get st''

If

        bevalR b true
        st =[c1]=> st'
--------------------------------
st =[if b then c1 else c2]=> st'

        bevalR b false
        st =[c2]=> st'
--------------------------------
st =[if b then c1 else c2]=> st'

• Evaluate b
• Note that b instructions cannot change state
• If true then evaluate c1
• If false then evaluate c2

While True

         bevalR b true
         st =[c]=> st'
st' =[ while b do c end ]=> st''
--------------------------------
   st =[while b do c end]=> st''

• Evaluate b to true
• Evaluate c once
• Evaluating c can change state
• Run the while again

While False

    bevalR b false
-----------------------
st =[while b do c end]=> st

• Evaluate b to false
• Same as SKIP

Some Thoughts on ceval

• How do we know that c1;c2 evaluates in order?
• Can we use aeval and beval instead of aevalR and bevalR?
  • Why or why not?
  • Why would we do this?
• How does while iterate and terminate?
• Is it okay that if has two rules?

Behavioral Equivalence

• If it walks like a duck and quacks like a duck, it’s duck…

“And if she weighs the same as a duck… she’s made of wood… and therefore… A WITCH!”. ~ Sir Bedevere from Monty Python and the Holy Grail

Behavioral Equivalence of Programs

• X + 2 is behaviorally equivalent to 1 + X + 1
• X - X is behaviorally equivalent to 0
• (X - 1) + 1 is not behaviorally equivalent to X

Why?

Some Definitions of Equivalence

Definition aequiv p1 p2 : aexp :=
  forall st : state, aexp st p1 = aexp st p2.

Definition cequiv (c1 c2 : com) : Prop :=
  ∀ (st st' : state),
    (st =[ c1 ]=> st') <-> (st =[ c2 ]=> st').

• Bisimulation - Start in the same state, end in the same state
• Weak Bisimulation - Nothing about what happens between start and stop
• Remember what c1 and c2 are

Examples from Pierce

Theorem skip_left : ∀ c,
  cequiv
    <{ skip; c }>
    c.

• What does this say?
• Can we do the proof?

Examples from Pierce (2)

Theorem skip_left : ∀ c,
  cequiv
    <{ skip; c }>
    c.
Proof.
  (* WORKED IN CLASS *)
  intros c st st'.
  split; intros H.
  - (* -> *)
    inversion H. subst.
    inversion H2. subst.
    assumption.
  - (* <- *)
    apply E_Seq with st.
    + apply E_Skip.
    + assumption.
Qed.

Examples from Pierce (3)

Theorem skip_right : forall c,
  cequiv
    <{ c; skip }>
    c.

Examples from Pierce (4)

Theorem skip_right : forall c,
  cequiv
    <{ c; skip }>
    c.
Proof.
  intros c st st'.
  split; intros H.
  - inversion H. subst.
    inversion H5. subst.
    assumption.
  - apply E_Seq with st'.
    assumption.
    apply E_Skip.
Qed.

Ltac H := inversion H; subst; remove H.

IF Optimization

Theorem if_true_simple : forall c1 c2,
  cequiv
    <{ if true then c1 else c2 end }>
    c1.

• Simple optimization of if
• Is it useful?
• What does it say?

A Stronger if Optimization

Theorem if_true: ∀ b c1 c2,
  bequiv b <{true}> →
  cequiv
    <{ if b then c1 else c2 end }>
    c1.

• What is the difference between this and if_true_simple?
• Is it important to us?

With the Proof

Theorem if_true: ∀ b c1 c2,
  bequiv b <{true}> →
  cequiv
    <{ if b then c1 else c2 end }>
    c1.
Proof.
  intros b c1 c2 Hb.
  split; intros H.
  - (* -> *)
    inversion H; subst.
    + (* b evaluates to true *)
      assumption.
    + (* b evaluates to false (contradiction) *)
      unfold bequiv in Hb. simpl in Hb.
      rewrite Hb in H5.
      discriminate.
  - (* <- *)
    apply E_IfTrue; try assumption.
    unfold bequiv in Hb. simpl in Hb.
    apply Hb. Qed.

And The Other Way

Theorem if_false : ∀ b c1 c2,
  bequiv b <{false}> →
  cequiv
    <{ if b then c1 else c2 end }>
    c2.

With The Proof

Theorem if_false : forall b c1 c2,
  bequiv b <{false}> ->
  cequiv
    <{ if b then c1 else c2 end }>
    c2.
Proof.
  intros b c1 c2. intros Hb.
  split; intros H.
  - inversion H; subst.
  -- unfold bequiv in Hb. simpl in Hb.
     rewrite Hb in H5.
     inversion H5.
  -- assumption.
  - apply E_IfFalse.
  -- unfold bequiv in Hb. simpl in Hb.
     apply Hb.
  -- assumption.
  Qed.

• Nothing Magic Here…

Flip if Cases

Theorem swap_if_branches : forall b c1 c2,

Flip if Cases (theorem)

Theorem swap_if_branches : forall b c1 c2,
  cequiv
    <{ if b   then c1 else c2 end }>
    <{ if ~ b then c2 else c1 end }>.

Flip if Cases (with the proof)

Theorem swap_if_branches : forall b c1 c2,
  cequiv
    <{ if b   then c1 else c2 end }>
    <{ if ~ b then c2 else c1 end }>.

Properties of while

• while false
• while true
• while unfolding

while false

<{while false do c end}>

• Turn this into a theorem

while and Non-termination

<{while true do c end}>

• Turn this into a theorem
• What does it mean not to terminate?

Unfolding while

Theorem loop_unrolling : forall b c,

Unfolding while Theorem

Theorem loop_unrolling : forall b c,
  cequiv
    <{ while b do c end }>
    <{ if b then c ; while b do c end else skip end }>.

• Execute the loop is the same as
  • Take one loop step
  • Execute the loop

Properties of Program Equivalence

• Program equivalence is an equivalence relation
  • Reflexive
  • Transitive
  • Symmetric
• Program equivalence is a congruence relation
  • Congruent parts of congruent triangles are congruent

Program Equivalence is Equivalence

• Jump to Rocq

Program Equivalence as Congruence

                aequiv a a'
         -------------------------
         cequiv (x := a) (x := a')

              cequiv c1 c1'
              cequiv c2 c2'
         --------------------------
         cequiv (c1;c2) (c1';c2')

• Jump to Rocq

Program Assertions

• Assertions are properties over system state

Definition Assertion := state -> Prop.

• fun st => st X = 3
• fun st => True
• fun st => False

Examples

Definition assertion1 : Assertion := fun st ⇒ st X ≤ st Y.
Definition assertion2 : Assertion :=
  fun st ⇒ st X = 3 ∨ st X ≤ st Y.
Definition assertion3 : Assertion :=
  fun st ⇒ st Z × st Z ≤ st X ∧
            ¬ (((S (st Z)) × (S (st Z))) ≤ st X).
Definition assertion4 : Assertion :=
  fun st ⇒ st Z = max (st X) (st Y).

Notations for Assertions

• Using anonymous Rocq functions:

fun st => st X = m

• Using Rocq Notations:

• st is assumed to be defined as a function parameter
• Cap variables are program variables
• Lower variables are Rocq variables

Example Assertions

Definition assertion1 : Assertion := .
Definition assertion2 : Assertion := .
Definition assertion3 : Assertion := .
Definition assertion4 : Assertion := .
Definition assertion5 : Assertion := .
Definition assertion6 : Assertion := .
Definition assertion7 : Assertion := .
Definition assertion8 : Assertion := .
Definition assertion9 : Assertion := .

Assertion Implication

• Functional Extensionality for Assertions

Definition assert_implies (P Q : Assertion) : Prop := forall st, P st -> Q st.

• Notations for assertion implication

P ->> Q
P <<->> Q == P ->> Q /\ Q ->> P

Hoare Triples

• A claim about system state before and after command execution
• Math notation for “if P is true before c then Q is true after”

{P} c {Q}

• The Rocq notation

 c 

m and M

 X := X + 1 

forall m,  X := X + 1 

Hoare Examples

 c 

forall m,  c 

 c 

 c 

forall m,  c 

forall m,  c 

Valid or Not Valid

 X := 5 

 X := X + 1 

 X := 5; Y := 0 

 X := 5 

 skip 

 skip 

 while true do skip end 


  while X = 0 do X := X + 1 end



  while X ≠ 0 do X := X + 1 end

Hoare Triples Defined

• Given P and Q are assertions
• Given st=[c]=>st' a command definition
• Define:
  • if P is true when c executes
  • then Q is true when it’s done

Hoare Triples Defined (2)

forall st st',
  P st ->
  st =[ c ]=> st' ->
  Q st'

Hoare Triples Defined (3)

Definition valid_hoare_triple
  (P : Assertion) (c : com) (Q : Assertion) : Prop :=
    forall st st',
      st =[ c ]=> st' ->
      P st ->
      Q st'.

• Notation for triples is nice to use

 c 

First Hoare Triple Theorems

• Informally, what do they say?

Theorem hoare_post_true : forall (P Q : Assertion) c,
  (forall st, Q st) ->
   c .

Theorem hoare_post_false : forall (P Q : Assertion) c,
  (forall st, not (P st)) ->
   c .

Hoare Proof Rules

• We want to use Hoare Triples to reason about programs
• Define semantics for individual IMP constructions
• Compose individual instructions to build programs
• Compose Hoare Proof Rules to prove properties of program

SKIP

-------------------- [hoare_SKIP]
 SKIP 

Theorem hoare_skip : forall P,
      skip .

Sequence Rule

  c2 
  c1 
-----------------
 c1;c2 

Assignment

• Assignment changes program state
• Its definition is foundational for Hoare Logic
• Its definition is also kind of weird
• It feels backwards…

Assignment (2)

• Running Example from our text

 X := Y 

• What precondition would make X=1 true after X:=Y

Assignment (3)

• There are several things we could use for ???
• The simplest is:

Y = 1

• And the Hoare triple becomes:

 X:=Y 

• How do we find Y=1 mechanically?

Assignment (4)

• Start with the post-condition X=1
• Replace X with Y

Y=1

Assignment (5)

 X:=X+Y 

• Start with the post-condition X=1
• Replace X with X+Y

 X:=X+Y 

Assignment General Rule

• Replace the left-hand side of the assignment statement with the right-hand side in the post-condition

 X := a 

• Using substitution we can define this as:

 X := a 

Seems kind of backwards. We’ll see forwards later, and you won’t like it

Examples from PLF

        (X + 1 <= 5)
  X := X + 1


            (3 = 3)
  X := 3


    (0 <= 3 /\ 3 <= 5)
  X := 3
0

Assertion Substitution

• Pretty clear that substitution is going to do the trick
• We’re replacing terms in an assertion
• Is there a good way to do that?

Assertion Substitution as Environment

• Simply add the substitution to the environment
• Substitution will take care of itself during evaluation

Definition assertion_sub X (a:aexp) (P:Assertion) : Assertion :=
  fun (st : state) =>
    (P%_assertion) (X !-> ((a:Aexp) st); st).

• Is it okay to do this?

Checking a Simple Precondition

(X <= 5) [X !-> 3]
==
fun st =>
  (fun st' => st' X <= 5)
  (X !-> aeval st 3 ; st),
==
fun st =>
  (fun st' => st' X <= 5)
  (X !-> 3 ; st)
==
fun st =>
  ((X !-> 3 ; st) X) <= 5
==
fun st =>
  3 <= 5.

• Rocq will do this for us

Bounce over to Rocq for a couple of examples

Rule of Consequence

• Frequently preconditions and post-conditions are not equal but are logically compatible
• Different syntactic forms that do not unify
• Logically weaker preconditions
• Logically stronger post-conditions

Aside About Weaker/Stronger

• P is weaker than Q if Q->P but ~P->Q
• P is stronger than Q if P->Q but ~Q->P

• P is equivalent to Q if P->Q and Q->P

• I always forget stronger and weaker

Example

 X := 3 ,

• Follows from the assignment rule

 X := 3 

• Does not follow from the Assignment Rule
• Still, the triple is valid
• True and (X = 3) [X |-> 3] are not syntactically equivalent
• True and (X = 3) [X !-> 3] are logically equivalent

Example Equivalence Rule

                 c 
                  P <<->> P'
             ---------------------
                 c 

• If P is equivalent to P' then P can replace P'

Rules of Consequence

• Strengthening the precondition of a valid triple always produces another valid triple.

                 c 
                   P ->> P'
         -----------------------------   (hoare_consequence_pre)
                 c 

• Weakening the post-condition of a valid triple always produces another valid triple.

                 c 
                  Q' ->> Q
         -----------------------------    (hoare_consequence_post)
                 c 

Formal Rules of Consequence

Theorem hoare_consequence_pre : forall (P P' Q : Assertion) c,
   c  ->
  P ->> P' ->
   c .

Theorem hoare_consequence_post : forall (P Q Q' : Assertion) c,
   c  ->
  Q' ->> Q ->
   c .

• Jump to proofs in Rocq

Combined Rule of Consequence

• Informally

                 c 
                   P ->> P'
                   Q' ->> Q
         -----------------------------   (hoare_consequence)
                 c 

• In Rocq

Theorem hoare_consequence : forall (P P' Q Q' : Assertion) c,
   c  ->
  P ->> P' ->
  Q' ->> Q ->
   c .

Proof Automation

• Our proving so far has been pedantic
  • Find a tactic
  • Try the tactic
  • Repeat
• This is not scalable
  • Proofs grow exceptionally large
  • Brittle and difficult to update
• Introduction of existential variables
  • eapply and eauto
• Ltac language of proof

Proof search attempts to build a proof automatically

auto and lia

• auto is a search tool over lemmas and introductions
  • A -> B style lemmas
  • Breadth first search
  • Controlled database
  • Controlled depth
• lia is a decision procedure for linear integer arithmetic (lia)

Motivating Example

• Pop over to Rocq and look at the ceval_deterministic proof

apply and Specific Rules

Example auto_example_1 : forall (P Q R: Prop),
  (P -> Q) -> (Q -> R) -> P -> R.
Proof.
  intros P Q R H1 H2 H3.
  apply H2. apply H1. assumption.
Qed.

• Three apply applications
• Specific rules used in each step
• If anything changes the proof breaks

auto and Databases

Example auto_example_1' : forall (P Q R: Prop),
  (P -> Q) -> (Q -> R) -> P -> R.
Proof.
  auto.
Qed.

• Solves goals using intros and apply
• Searches for an application sequence
• Safe decision procedure

Example auto_example_2 : forall P Q R S T U : Prop,
  (P -> Q) ->
  (P -> R) ->
  (T -> R) ->
  (S -> T -> U) ->
  ((P -> Q) -> (P -> S)) ->
  T ->
  P ->
  U.
Proof. auto. Qed.

• A hint database is a collection of lemmas accessible to auto
• Limits and informs the search
• Building hint databases controls search
• Default hint database contains
  • Lemmas from the antecedent
  • Equality and logic
• Default database contains

Adding Lemmas to auto

auto using lemma_name.

• Adds lemma_name to the default hint database

Limiting Depth

Example auto_example_3 : forall (P Q R S T U: Prop),
  (P -> Q) ->
  (Q -> R) ->
  (R -> S) ->
  (S -> T) ->
  (T -> U) ->
  P ->
  U.
Proof.

• auto will not solve this
  • Search depth is by default 5
• auto 6 will solve this
  • Search depth manually set
• Use auto_info to see what auto is up to

Examples with auto

Building a Hint Database

Hint Resolve T : core

• core is the default hint database
• Adds T to core
• You can define your own hint dastabase

Hint Database Shorthands

Hint Constructors c : core.

• Adds all constructors for type c to core

Hint Unfold d : core.
Hint Transparent d: core.

• Tells auto to unfold d
• Tells auto to look inside d, but not unfold (rarely used)

Example ceval_deterministic Again

• Jump to Rocq and work there on simplifying ceval_deterministic

Ltac

• A Rocq proof scripting language - a DSL for proving
• Tactics like apply and intros are Ltac primitives
• The semicolon is an example of an Ltac command
• Ltac functions define new commands like programming langauge functions
• Pattern matching over goals provides powerful proof reasoning

An Ltac Function

Ltac rwd H1 H2 := rewrite H1 in H2; discriminate

• A contradiction routine
• H1 and H2 are parameters
• Must use ; to sequence commands
• Ltac functions need not be proven to terminate

Goal Matching

Ltac find_rwd :=
  match goal with
    H1: ?E = true, H2: ?E = false |- _
       =>
    rwd H1 H2
  end.

• match goal looks at the current Rocq proof goal
• H1 and H2 name antecents
• In A |- C
  • A matches antecedent
  • C matches the consequent
• ?E is a match variable

Ltac find_rwd :=
  match goal with
    H1: ?E = true, H2: ?E = false |- _
       =>
    rwd H1 H2
  end.

• Find an expression ?E that matches both antecedents
  • ?E = true
  • ?E = false
• If they are found a contradiction exists that can be dischargd with rwd
• If they are not found find_rwd does nothing

find_eqn

Ltac find_eqn :=
  match goal with
    H1: forall x, ?P x -> ?L = ?R,
    H2: ?P ?X
    |- _
    => rewrite (H1 X H2) in *
  end.

• What does this Ltac snippet do?

Existential or Meta Variables

• Rocq proof variables decorated with “?”
• Created during proofs when values are underconstrained
  • A typed value is needed to instantiate an expression
  • Not enough is known to find the value
  • ?X defers knowing until later
• Must have values for a proof to complete
• Sequence is a great example:

 X := 1 ; Y := 2 

• A hidden state exists between the two commands
• Unknown until P evaluates

A Sequence Example

Example ceval_example1:
  empty_st =[
    X := 2;
    if (X <= 1)
      then Y := 3
      else Z := 4
    end
  ]=> (Z !-> 4 ; X !-> 2).
Proof.
  apply E_Seq with (X !-> 2).
  - apply E_Asgn. reflexivity.
  - apply E_IfFalse. reflexivity. apply E_Asgn. reflexivity.
Qed.

• (X !-> 2) is the intermediate state
• We had to provide it

Sequence Subgoals

empty_st =[X:=2]=> (X !-> 2)
(X !-> 2) =[if command]=> (Z!->4;X!->2)

• See the intermediate state we provided?

A Sequence Example (2)

• E_Seq is applied first

st =[c1]=> st' ->
st' =[c2]=> st'' ->
st =[c1;c2]=> st'' 

• We know st and st'' by unification with the goal
• We do not know st' because X := 2 has not been processed
• But we will know st' if Rocq will be patient

eapply

Example ceval'_example1:
  empty_st =[
    X := 2;
    if (X <= 1)
      then Y := 3
      else Z := 4
    end
  ]=> (Z !-> 4 ; X !-> 2).
Proof.
  (* 1 *) eapply E_Seq.
  - (* 2 *) apply E_Asgn.
    (* 3 *) reflexivity.
  - (* 4 *) apply E_IfFalse. reflexivity. apply E_Asgn. reflexivity.
Qed.

• eapply E_Seq introduces ?X and instantiates E_Seq

?X

• Two subgoals are

empty_st =[X:=2]=> ?X

?X =[if command]=> (Z!->4;X!->2)

• Applying E_Asgn constrains ?X to be

(X!->2) ; empty_st == (X!->2)

• Replace ?X with the value we found:

empty_st =[X:=2]=> (X!->2)

(X!->2) =[if command]=> (Z!->4;X!->2)

The e Commands

• eexists - introduces a new existential variable
• eapply - we just saw this
• eauto - uses eapply instead of apply
• info_eauto - uses eapply instead of apply
• econsructor - instantiates a constructor
• several others

Start with eapply and work from there