Big-step semantics

Display all goals and responses

Author: Adam Chlipala, Nate Foster, Dario Halilovic
License: No redistribution allowed (usage by permission in CS-428).

A Simple Arithmetic Language, Continued

Last week, we've seen how to define inductive propositions, and even re-defined our evaluation function as an inductive relation. It turns out that this style of defining semantics is quite common, and ieval is an example of what we call big-step semantics.

In this lecture, we introduce big-step semantics by analyzing our first (rudimentary) programming language. For that, we'll again need our beloved arithmetical language from weeks 1 to 4:

Notation var := string.

Inductive arith : Set :=
| Const (n : nat)
| Var (x : var)
| Plus (e1 e2 : arith)
| Minus (e1 e2 : arith)
| Times (e1 e2 : arith).

The following two sentences register Const and Nat as coercions, which allows us to use natural numbers and strings wherever an arithmetical expression is expected.

Coercion Const : nat >-> arith.
Coercion Var : var >-> arith.

Let's simplify our syntax by defining some notations:

Declare Scope arith_scope.
Infix "+" := Plus : arith_scope.
Infix "-" := Minus : arith_scope.
Infix "*" := Times : arith_scope.
Delimit Scope arith_scope with arith.

As in week 3, we can write some small examples of arithmetical expressions, but with less boilerplate:

Example ex1 : arith := 42.
(* This stands for `Const 42` thanks to the coercion. *)

Example ex2 : arith := ("y" + ("x" * 3))%arith.

Finally, we'll need a valuation to determine the value of variables. We use the same definition of valuations that we introduced in week 3, with the usual definitions of get and set.

Definition valuation := var -> option nat.

Definition empty : valuation := fun _ => None.

Definition get (x: var) (v: valuation) : option nat := v x.

Definition set (x: var) (n: nat) (v: valuation) : valuation :=
  fun y =>
    match string_dec x y with
        | left H => Some n
        | right H' => get y v
    end.

The two lemmas below are going to be useful later, when we'll prove the correctness of our interpreter:

Lemma get_set_neq (x y: var) n v :
  x <> y -> get x (set y n v) = get x v.x, y: var
n: nat
v: valuation
x <> y -> get x (set y n v) = get x v
Proof.x, y: var
n: nat
v: valuation
x <> y -> get x (set y n v) = get x v
  unfold set, get; intros.x, y: var
n: nat
v: valuation
H: x <> y
(if string_dec y x then Some n else v x) = v x
  destruct string_dec; congruence.
Qed.

Lemma get_set_eq (x y: var) n v :
  x = y -> get x (set y n v) = Some n.x, y: var
n: nat
v: valuation
x = y -> get x (set y n v) = Some n
Proof.x, y: var
n: nat
v: valuation
x = y -> get x (set y n v) = Some n
  unfold set, get; intros.x, y: var
n: nat
v: valuation
H: x = y
(if string_dec y x then Some n else v x) = Some n
  destruct string_dec; congruence.
Qed.

Recall our use of a recursive function to interpret arithmetical expressions.

Fixpoint interp (e : arith) (v : valuation) : nat :=
  match e with
  | Const n => n
  | Var x =>
    match get x v with
    | None => 0
    | Some n => n
    end
  | Plus e1 e2 => interp e1 v + interp e2 v
  | Minus e1 e2 => interp e1 v - interp e2 v
  | Times e1 e2 => interp e1 v * interp e2 v
  end.

A Small Imperative Language

Now, we're ready to define a small imperative language. Our language will be able to mutate variables, and use basic if and while statements.

To represent booleans, we'll use our arithmetical expressions, where 0 means false, and any other value means true.

Of course, since our arithmetic expressions can contain variables, and our program can mutate them, we can get interesting (non-trivial) programs this way.

Inductive cmd :=
| Skip (* This instruction does nothing (no-op). *)
| Assign (x : var) (e : arith)
| Sequence (c1 c2 : cmd)
| If (e : arith) (then_ else_ : cmd)
| While (e : arith) (body : cmd).

Since our programs can get very hard to read with the default syntax, we define custom notations for legibility purposes. I won't explain every detail of the incantations below, but you get the general idea.

Notation "x <- e" := (Assign x e%arith) (at level 75).
Infix ";;" := Sequence (at level 76).
Notation "'when' e 'then' then_ 'else' else_ 'done'" :=
  (If e%arith then_ else_) (at level 75, e at level 0).Identifier 'when' now a keyword
Identifier 'done' now a keyword
Notation "'while' e 'loop' body 'done'" :=
  (While e%arith body) (at level 75).Identifier 'while' now a keyword
Identifier 'loop' now a keyword

With our syntax, we can define a program to compute the factorial of a number, which is given as an input variable.

Example factorial :=
  "output" <- 1;;
  while "input" loop
    "output" <- "output" * "input";;
    "input" <- "input" - 1
  done.

Big-Step Semantics

Now, how do we interpret our program?

Defining an interpreter won't work here, since our programs may not even terminate due to the general while loops. Instead, in the spirit of last week, we can rely on inductively-defined propositions to say something of the form "program p transforms valuation v to valuation w". In other words, given an initial valuation v, fully executing program p yields valuation w if and only if eval v p w holds, where eval is our evaluation predicate.

But how exactly should we define eval? A natural strategy is to divide-and-conquer: divide the evaluation of the program into subparts, and combine the results of their full evaluation to get the evaluation of the whole program. For example, given the evaluation to completion of program p, it becomes trivial to evaluate if 1 then p else p'.

This strategy is more commonly referred to as big-step semantics (as opposed to small-step semantics, which we'll see next week).

Inductive eval : valuation -> cmd -> valuation -> Prop :=
| EvalSkip : forall v,
    eval v Skip v
| EvalAssign : forall v x e,
    eval v (Assign x e) (set x (interp e v) v)
| EvalSeq : forall v c1 v1 c2 v2,
    eval v c1 v1
    -> eval v1 c2 v2
    -> eval v (Sequence c1 c2) v2
| EvalIfTrue : forall v e then_ else_ v',
    interp e v <> 0
    -> eval v then_ v'
    -> eval v (If e then_ else_) v'
| EvalIfFalse : forall v e then_ else_ v',
    interp e v = 0
    -> eval v else_ v'
    -> eval v (If e then_ else_) v'
| EvalWhileTrue : forall v e body v' v'',
    interp e v <> 0
    -> eval v body v'
    -> eval v' (While e body) v''
    -> eval v (While e body) v''
| EvalWhileFalse : forall v e body,
    interp e v = 0
    -> eval v (While e body) v.

With our definition of eval, let's try to run the factorial program on a few inputs.

Theorem factorial_2 : exists v,
    eval (set "input" 2 empty) factorial v
    /\ get "output" v = Some 2.exists v : valuation,
  eval (set "input" 2 empty) factorial v /\
  get "output" v = Some 2
Proof.exists v : valuation,
  eval (set "input" 2 empty) factorial v /\
  get "output" v = Some 2
  eexists.eval (set "input" 2 empty) factorial ?v /\
get "output" ?v = Some 2
  econstructor.eval (set "input" 2 empty) factorial ?v
get "output" ?v = Some 2
  econstructor.eval (set "input" 2 empty) ("output" <- 1) ?v1
eval ?v1
  (while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?v
get "output" ?v = Some 2
  econstructor.eval
  (set "output" (interp 1 (set "input" 2 empty))
     (set "input" 2 empty))
  (while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?v
get "output" ?v = Some 2
  simpl in *.eval (set "output" 1 (set "input" 2 empty))
  (while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?v
get "output" ?v = Some 2
  econstructor.interp "input" (set "output" 1 (set "input" 2 empty)) <>
0
eval (set "output" 1 (set "input" 2 empty))
  ("output" <- "output" * "input";;
   "input" <- "input" - 1) ?v'
eval ?v'
  (while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?v
get "output" ?v = Some 2
  simpl in *.2 <> 0
eval (set "output" 1 (set "input" 2 empty))
  ("output" <- "output" * "input";;
   "input" <- "input" - 1) ?v'
eval ?v'
  (while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?v
get "output" ?v = Some 2
  lia.eval (set "output" 1 (set "input" 2 empty))
  ("output" <- "output" * "input";;
   "input" <- "input" - 1) ?v'
eval ?v'
  (while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?v
get "output" ?v = Some 2
  econstructor.eval (set "output" 1 (set "input" 2 empty))
  ("output" <- "output" * "input") ?v1
eval ?v1 ("input" <- "input" - 1) ?v'
eval ?v'
  (while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?v
get "output" ?v = Some 2
  econstructor.eval
  (set "output"
     (interp ("output" * "input")%arith
        (set "output" 1 (set "input" 2 empty)))
     (set "output" 1 (set "input" 2 empty)))
  ("input" <- "input" - 1) ?v'
eval ?v'
  (while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?v
get "output" ?v = Some 2
  econstructor.eval
  (set "input"
     (interp ("input" - 1)%arith
        (set "output"
           (interp ("output" * "input")%arith
              (set "output" 1 (set "input" 2 empty)))
           (set "output" 1 (set "input" 2 empty))))
     (set "output"
        (interp ("output" * "input")%arith
           (set "output" 1 (set "input" 2 empty)))
        (set "output" 1 (set "input" 2 empty))))
  (while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?v
get "output" ?v = Some 2
  simpl in *.eval
  (set "input" 1
     (set "output" 2
        (set "output" 1 (set "input" 2 empty))))
  (while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?v
get "output" ?v = Some 2
  econstructor.interp "input"
  (set "input" 1
     (set "output" 2
        (set "output" 1 (set "input" 2 empty)))) <> 0
eval
  (set "input" 1
     (set "output" 2
        (set "output" 1 (set "input" 2 empty))))
  ("output" <- "output" * "input";;
   "input" <- "input" - 1) ?v'
eval ?v'
  (while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?v
get "output" ?v = Some 2
  simpl in *.1 <> 0
eval
  (set "input" 1
     (set "output" 2
        (set "output" 1 (set "input" 2 empty))))
  ("output" <- "output" * "input";;
   "input" <- "input" - 1) ?v'
eval ?v'
  (while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?v
get "output" ?v = Some 2
  lia.eval
  (set "input" 1
     (set "output" 2
        (set "output" 1 (set "input" 2 empty))))
  ("output" <- "output" * "input";;
   "input" <- "input" - 1) ?v'
eval ?v'
  (while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?v
get "output" ?v = Some 2
  econstructor.eval
  (set "input" 1
     (set "output" 2
        (set "output" 1 (set "input" 2 empty))))
  ("output" <- "output" * "input") ?v1
eval ?v1 ("input" <- "input" - 1) ?v'
eval ?v'
  (while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?v
get "output" ?v = Some 2
  econstructor.eval
  (set "output"
     (interp ("output" * "input")%arith
        (set "input" 1
           (set "output" 2
              (set "output" 1 (set "input" 2 empty)))))
     (set "input" 1
        (set "output" 2
           (set "output" 1 (set "input" 2 empty)))))
  ("input" <- "input" - 1) ?v'
eval ?v'
  (while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?v
get "output" ?v = Some 2
  econstructor.eval
  (set "input"
     (interp ("input" - 1)%arith
        (set "output"
           (interp ("output" * "input")%arith
              (set "input" 1
                 (set "output" 2
                    (set "output" 1
                       (set "input" 2 empty)))))
           (set "input" 1
              (set "output" 2
                 (set "output" 1 (set "input" 2 empty))))))
     (set "output"
        (interp ("output" * "input")%arith
           (set "input" 1
              (set "output" 2
                 (set "output" 1 (set "input" 2 empty)))))
        (set "input" 1
           (set "output" 2
              (set "output" 1 (set "input" 2 empty))))))
  (while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?v
get "output" ?v = Some 2
  apply EvalWhileFalse.interp "input"
  (set "input"
     (interp ("input" - 1)%arith
        (set "output"
           (interp ("output" * "input")%arith
              (set "input" 1
                 (set "output" 2
                    (set "output" 1
                       (set "input" 2 empty)))))
           (set "input" 1
              (set "output" 2
                 (set "output" 1 (set "input" 2 empty))))))
     (set "output"
        (interp ("output" * "input")%arith
           (set "input" 1
              (set "output" 2
                 (set "output" 1 (set "input" 2 empty)))))
        (set "input" 1
           (set "output" 2
              (set "output" 1 (set "input" 2 empty)))))) =
0
get "output"
  (set "input"
     (interp ("input" - 1)%arith
        (set "output"
           (interp ("output" * "input")%arith
              (set "input" 1
                 (set "output" 2
                    (set "output" 1
                       (set "input" 2 empty)))))
           (set "input" 1
              (set "output" 2
                 (set "output" 1 (set "input" 2 empty))))))
     (set "output"
        (interp ("output" * "input")%arith
           (set "input" 1
              (set "output" 2
                 (set "output" 1 (set "input" 2 empty)))))
        (set "input" 1
           (set "output" 2
              (set "output" 1 (set "input" 2 empty)))))) =
Some 2
  simpl in *.0 = 0
get "output"
  (set "input"
     (interp ("input" - 1)%arith
        (set "output"
           (interp ("output" * "input")%arith
              (set "input" 1
                 (set "output" 2
                    (set "output" 1
                       (set "input" 2 empty)))))
           (set "input" 1
              (set "output" 2
                 (set "output" 1 (set "input" 2 empty))))))
     (set "output"
        (interp ("output" * "input")%arith
           (set "input" 1
              (set "output" 2
                 (set "output" 1 (set "input" 2 empty)))))
        (set "input" 1
           (set "output" 2
              (set "output" 1 (set "input" 2 empty)))))) =
Some 2
  econstructor.get "output"
  (set "input"
     (interp ("input" - 1)%arith
        (set "output"
           (interp ("output" * "input")%arith
              (set "input" 1
                 (set "output" 2
                    (set "output" 1
                       (set "input" 2 empty)))))
           (set "input" 1
              (set "output" 2
                 (set "output" 1 (set "input" 2 empty))))))
     (set "output"
        (interp ("output" * "input")%arith
           (set "input" 1
              (set "output" 2
                 (set "output" 1 (set "input" 2 empty)))))
        (set "input" 1
           (set "output" 2
              (set "output" 1 (set "input" 2 empty)))))) =
Some 2
  simpl in *.get "output"
  (set "input" 0
     (set "output" 2
        (set "input" 1
           (set "output" 2
              (set "output" 1 (set "input" 2 empty)))))) =
Some 2
  econstructor.
Qed.

Phew! That was rather repetitive. Fortunately, it's easy to automate.

Ltac eval1 :=
  apply EvalSkip || apply EvalAssign || eapply EvalSeq
  || (apply EvalIfTrue; [ simpl in *; lia | ])
  || (apply EvalIfFalse; [ simpl in *; lia | ])
  || (eapply EvalWhileTrue; [ simpl in *; lia | | ])
  || (apply EvalWhileFalse; [ simpl in *; lia ]).

Ltac evaluate := simpl in *; try econstructor; repeat eval1.

Theorem factorial_2_snazzy : exists v,
    eval (set "input" 2 empty) factorial v
    /\ get "output" v = Some 2.exists v : valuation,
  eval (set "input" 2 empty) factorial v /\
  get "output" v = Some 2
Proof.exists v : valuation,
  eval (set "input" 2 empty) factorial v /\
  get "output" v = Some 2
  eexists.eval (set "input" 2 empty) factorial ?v /\
get "output" ?v = Some 2
  evaluate.get "output"
  (set "input"
     (interp ("input" - 1)%arith
        (set "output"
           (interp ("output" * "input")%arith
              (set "input"
                 (interp ("input" - 1)%arith
                    (set "output"
                       (interp
                          ("output" * "input")%arith
                          (set "output"
                             (interp 1
                                (set "input" 2 empty))
                             (set "input" 2 empty)))
                       (set "output"
                          (interp 1
                             (set "input" 2 empty))
                          (set "input" 2 empty))))
                 (set "output"
                    (interp ("output" * "input")%arith
                       (set "output"
                          (interp 1
                             (set "input" 2 empty))
                          (set "input" 2 empty)))
                    (set "output"
                       (interp 1 (set "input" 2 empty))
                       (set "input" 2 empty)))))
           (set "input"
              (interp ("input" - 1)%arith
                 (set "output"
                    (interp ("output" * "input")%arith
                       (set "output"
                          (interp 1
                             (set "input" 2 empty))
                          (set "input" 2 empty)))
                    (set "output"
                       (interp 1 (set "input" 2 empty))
                       (set "input" 2 empty))))
              (set "output"
                 (interp ("output" * "input")%arith
                    (set "output"
                       (interp 1 (set "input" 2 empty))
                       (set "input" 2 empty)))
                 (set "output"
                    (interp 1 (set "input" 2 empty))
                    (set "input" 2 empty))))))
     (set "output"
        (interp ("output" * "input")%arith
           (set "input"
              (interp ("input" - 1)%arith
                 (set "output"
                    (interp ("output" * "input")%arith
                       (set "output"
                          (interp 1
                             (set "input" 2 empty))
                          (set "input" 2 empty)))
                    (set "output"
                       (interp 1 (set "input" 2 empty))
                       (set "input" 2 empty))))
              (set "output"
                 (interp ("output" * "input")%arith
                    (set "output"
                       (interp 1 (set "input" 2 empty))
                       (set "input" 2 empty)))
                 (set "output"
                    (interp 1 (set "input" 2 empty))
                    (set "input" 2 empty)))))
        (set "input"
           (interp ("input" - 1)%arith
              (set "output"
                 (interp ("output" * "input")%arith
                    (set "output"
                       (interp 1 (set "input" 2 empty))
                       (set "input" 2 empty)))
                 (set "output"
                    (interp 1 (set "input" 2 empty))
                    (set "input" 2 empty))))
           (set "output"
              (interp ("output" * "input")%arith
                 (set "output"
                    (interp 1 (set "input" 2 empty))
                    (set "input" 2 empty)))
              (set "output"
                 (interp 1 (set "input" 2 empty))
                 (set "input" 2 empty)))))) = Some 2
  evaluate.
Qed.

Theorem factorial_3 : exists v,
    eval (set "input" 3 empty) factorial v
    /\ get "output" v = Some 6.exists v : valuation,
  eval (set "input" 3 empty) factorial v /\
  get "output" v = Some 6
Proof.exists v : valuation,
  eval (set "input" 3 empty) factorial v /\
  get "output" v = Some 6
  eexists.eval (set "input" 3 empty) factorial ?v /\
get "output" ?v = Some 6
  evaluate.get "output"
  (set "input"
     (interp ("input" - 1)%arith
        (set "output"
           (interp ("output" * "input")%arith
              (set "input"
                 (interp ("input" - 1)%arith
                    (set "output"
                       (interp
                          ("output" * "input")%arith
                          (set "input"
                             (interp
                                ("input" - 1)%arith
                                (set "output"
                                   (interp (...)%arith
                                      (...))
                                   (set "output" (...)
                                      (...))))
                             (set "output"
                                (interp
                                   ("output" * "input")%arith
                                   (set "output" (...)
                                      (...)))
                                (set "output"
                                   (interp 1 (...))
                                   (set "input" 3
                                      empty)))))
                       (set "input"
                          (interp ("input" - 1)%arith
                             (set "output"
                                (interp
                                   ("output" * "input")%arith
                                   (set "output" (...)
                                      (...)))
                                (set "output"
                                   (interp 1 (...))
                                   (set "input" 3
                                      empty))))
                          (set "output"
                             (interp
                                ("output" * "input")%arith
                                (set "output"
                                   (interp 1 (...))
                                   (set "input" 3
                                      empty)))
                             (set "output"
                                (interp 1
                                   (set "input" 3
                                      empty))
                                (set "input" 3 empty))))))
                 (set "output"
                    (interp ("output" * "input")%arith
                       (set "input"
                          (interp ("input" - 1)%arith
                             (set "output"
                                (interp
                                   ("output" * "input")%arith
                                   (set "output" (...)
                                      (...)))
                                (set "output"
                                   (interp 1 (...))
                                   (set "input" 3
                                      empty))))
                          (set "output"
                             (interp
                                ("output" * "input")%arith
                                (set "output"
                                   (interp 1 (...))
                                   (set "input" 3
                                      empty)))
                             (set "output"
                                (interp 1
                                   (set "input" 3
                                      empty))
                                (set "input" 3 empty)))))
                    (set "input"
                       (interp ("input" - 1)%arith
                          (set "output"
                             (interp
                                ("output" * "input")%arith
                                (set "output"
                                   (interp 1 (...))
                                   (set "input" 3
                                      empty)))
                             (set "output"
                                (interp 1
                                   (set "input" 3
                                      empty))
                                (set "input" 3 empty))))
                       (set "output"
                          (interp
                             ("output" * "input")%arith
                             (set "output"
                                (interp 1
                                   (set "input" 3
                                      empty))
                                (set "input" 3 empty)))
                          (set "output"
                             (interp 1
                                (set "input" 3 empty))
                             (set "input" 3 empty)))))))
           (set "input"
              (interp ("input" - 1)%arith
                 (set "output"
                    (interp ("output" * "input")%arith
                       (set "input"
                          (interp ("input" - 1)%arith
                             (set "output"
                                (interp
                                   ("output" * "input")%arith
                                   (set "output" (...)
                                      (...)))
                                (set "output"
                                   (interp 1 (...))
                                   (set "input" 3
                                      empty))))
                          (set "output"
                             (interp
                                ("output" * "input")%arith
                                (set "output"
                                   (interp 1 (...))
                                   (set "input" 3
                                      empty)))
                             (set "output"
                                (interp 1
                                   (set "input" 3
                                      empty))
                                (set "input" 3 empty)))))
                    (set "input"
                       (interp ("input" - 1)%arith
                          (set "output"
                             (interp
                                ("output" * "input")%arith
                                (set "output"
                                   (interp 1 (...))
                                   (set "input" 3
                                      empty)))
                             (set "output"
                                (interp 1
                                   (set "input" 3
                                      empty))
                                (set "input" 3 empty))))
                       (set "output"
                          (interp
                             ("output" * "input")%arith
                             (set "output"
                                (interp 1
                                   (set "input" 3
                                      empty))
                                (set "input" 3 empty)))
                          (set "output"
                             (interp 1
                                (set "input" 3 empty))
                             (set "input" 3 empty))))))
              (set "output"
                 (interp ("output" * "input")%arith
                    (set "input"
                       (interp ("input" - 1)%arith
                          (set "output"
                             (interp
                                ("output" * "input")%arith
                                (set "output"
                                   (interp 1 (...))
                                   (set "input" 3
                                      empty)))
                             (set "output"
                                (interp 1
                                   (set "input" 3
                                      empty))
                                (set "input" 3 empty))))
                       (set "output"
                          (interp
                             ("output" * "input")%arith
                             (set "output"
                                (interp 1
                                   (set "input" 3
                                      empty))
                                (set "input" 3 empty)))
                          (set "output"
                             (interp 1
                                (set "input" 3 empty))
                             (set "input" 3 empty)))))
                 (set "input"
                    (interp ("input" - 1)%arith
                       (set "output"
                          (interp
                             ("output" * "input")%arith
                             (set "output"
                                (interp 1
                                   (set "input" 3
                                      empty))
                                (set "input" 3 empty)))
                          (set "output"
                             (interp 1
                                (set "input" 3 empty))
                             (set "input" 3 empty))))
                    (set "output"
                       (interp
                          ("output" * "input")%arith
                          (set "output"
                             (interp 1
                                (set "input" 3 empty))
                             (set "input" 3 empty)))
                       (set "output"
                          (interp 1
                             (set "input" 3 empty))
                          (set "input" 3 empty))))))))
     (set "output"
        (interp ("output" * "input")%arith
           (set "input"
              (interp ("input" - 1)%arith
                 (set "output"
                    (interp ("output" * "input")%arith
                       (set "input"
                          (interp ("input" - 1)%arith
                             (set "output"
                                (interp
                                   ("output" * "input")%arith
                                   (set "output" (...)
                                      (...)))
                                (set "output"
                                   (interp 1 (...))
                                   (set "input" 3
                                      empty))))
                          (set "output"
                             (interp
                                ("output" * "input")%arith
                                (set "output"
                                   (interp 1 (...))
                                   (set "input" 3
                                      empty)))
                             (set "output"
                                (interp 1
                                   (set "input" 3
                                      empty))
                                (set "input" 3 empty)))))
                    (set "input"
                       (interp ("input" - 1)%arith
                          (set "output"
                             (interp
                                ("output" * "input")%arith
                                (set "output"
                                   (interp 1 (...))
                                   (set "input" 3
                                      empty)))
                             (set "output"
                                (interp 1
                                   (set "input" 3
                                      empty))
                                (set "input" 3 empty))))
                       (set "output"
                          (interp
                             ("output" * "input")%arith
                             (set "output"
                                (interp 1
                                   (set "input" 3
                                      empty))
                                (set "input" 3 empty)))
                          (set "output"
                             (interp 1
                                (set "input" 3 empty))
                             (set "input" 3 empty))))))
              (set "output"
                 (interp ("output" * "input")%arith
                    (set "input"
                       (interp ("input" - 1)%arith
                          (set "output"
                             (interp
                                ("output" * "input")%arith
                                (set "output"
                                   (interp 1 (...))
                                   (set "input" 3
                                      empty)))
                             (set "output"
                                (interp 1
                                   (set "input" 3
                                      empty))
                                (set "input" 3 empty))))
                       (set "output"
                          (interp
                             ("output" * "input")%arith
                             (set "output"
                                (interp 1
                                   (set "input" 3
                                      empty))
                                (set "input" 3 empty)))
                          (set "output"
                             (interp 1
                                (set "input" 3 empty))
                             (set "input" 3 empty)))))
                 (set "input"
                    (interp ("input" - 1)%arith
                       (set "output"
                          (interp
                             ("output" * "input")%arith
                             (set "output"
                                (interp 1
                                   (set "input" 3
                                      empty))
                                (set "input" 3 empty)))
                          (set "output"
                             (interp 1
                                (set "input" 3 empty))
                             (set "input" 3 empty))))
                    (set "output"
                       (interp
                          ("output" * "input")%arith
                          (set "output"
                             (interp 1
                                (set "input" 3 empty))
                             (set "input" 3 empty)))
                       (set "output"
                          (interp 1
                             (set "input" 3 empty))
                          (set "input" 3 empty)))))))
        (set "input"
           (interp ("input" - 1)%arith
              (set "output"
                 (interp ("output" * "input")%arith
                    (set "input"
                       (interp ("input" - 1)%arith
                          (set "output"
                             (interp
                                ("output" * "input")%arith
                                (set "output"
                                   (interp 1 (...))
                                   (set "input" 3
                                      empty)))
                             (set "output"
                                (interp 1
                                   (set "input" 3
                                      empty))
                                (set "input" 3 empty))))
                       (set "output"
                          (interp
                             ("output" * "input")%arith
                             (set "output"
                                (interp 1
                                   (set "input" 3
                                      empty))
                                (set "input" 3 empty)))
                          (set "output"
                             (interp 1
                                (set "input" 3 empty))
                             (set "input" 3 empty)))))
                 (set "input"
                    (interp ("input" - 1)%arith
                       (set "output"
                          (interp
                             ("output" * "input")%arith
                             (set "output"
                                (interp 1
                                   (set "input" 3
                                      empty))
                                (set "input" 3 empty)))
                          (set "output"
                             (interp 1
                                (set "input" 3 empty))
                             (set "input" 3 empty))))
                    (set "output"
                       (interp
                          ("output" * "input")%arith
                          (set "output"
                             (interp 1
                                (set "input" 3 empty))
                             (set "input" 3 empty)))
                       (set "output"
                          (interp 1
                             (set "input" 3 empty))
                          (set "input" 3 empty))))))
           (set "output"
              (interp ("output" * "input")%arith
                 (set "input"
                    (interp ("input" - 1)%arith
                       (set "output"
                          (interp
                             ("output" * "input")%arith
                             (set "output"
                                (interp 1
                                   (set "input" 3
                                      empty))
                                (set "input" 3 empty)))
                          (set "output"
                             (interp 1
                                (set "input" 3 empty))
                             (set "input" 3 empty))))
                    (set "output"
                       (interp
                          ("output" * "input")%arith
                          (set "output"
                             (interp 1
                                (set "input" 3 empty))
                             (set "input" 3 empty)))
                       (set "output"
                          (interp 1
                             (set "input" 3 empty))
                          (set "input" 3 empty)))))
              (set "input"
                 (interp ("input" - 1)%arith
                    (set "output"
                       (interp
                          ("output" * "input")%arith
                          (set "output"
                             (interp 1
                                (set "input" 3 empty))
                             (set "input" 3 empty)))
                       (set "output"
                          (interp 1
                             (set "input" 3 empty))
                          (set "input" 3 empty))))
                 (set "output"
                    (interp ("output" * "input")%arith
                       (set "output"
                          (interp 1
                             (set "input" 3 empty))
                          (set "input" 3 empty)))
                    (set "output"
                       (interp 1 (set "input" 3 empty))
                       (set "input" 3 empty)))))))) =
Some 6
  evaluate.
Qed.

Proving correctness of factorial

Instead of chugging through these relatively slow individual executions, let's prove once and for all that factorial is correct by comparing it to the mathematical definition.

Fixpoint fact (n : nat) : nat :=
  match n with
  | O => 1
  | S n' => n * fact n'
  end.

To analyze the factorial program, we first prove the corectness of its core loop.

Example factorial_loop :=
  while "input" loop
    "output" <- "output" * "input";;
    "input" <- "input" - 1
  done.

Lemma factorial_loop_correct : forall n v out,
    get "input" v = Some n
    -> get "output" v = Some out
    -> exists v',
        eval v factorial_loop v'
        /\ get "output" v' = Some (fact n * out).forall (n : nat) (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
  eval v factorial_loop v' /\
  get "output" v' = Some (fact n * out)
Proof.forall (n : nat) (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
  eval v factorial_loop v' /\
  get "output" v' = Some (fact n * out)
  induction n; simpl in *; intros.v: valuation
out: nat
H: get "input" v = Some 0
H0: get "output" v = Some out
exists v' : valuation,
  eval v factorial_loop v' /\
  get "output" v' = Some (out + 0)
n: nat
IHn: forall (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
eval v factorial_loop v' /\ get "output" v' = Some (fact n * out)
v: valuation
out: nat
H: get "input" v = Some (S n)
H0: get "output" v = Some out
exists v' : valuation,
  eval v factorial_loop v' /\
  get "output" v' = Some ((fact n + n * fact n) * out)
  eexists.v: valuation
out: nat
H: get "input" v = Some 0
H0: get "output" v = Some out
eval v factorial_loop ?v' /\
get "output" ?v' = Some (out + 0)
n: nat
IHn: forall (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
eval v factorial_loop v' /\ get "output" v' = Some (fact n * out)
v: valuation
out: nat
H: get "input" v = Some (S n)
H0: get "output" v = Some out
exists v' : valuation,
  eval v factorial_loop v' /\
  get "output" v' = Some ((fact n + n * fact n) * out)
  econstructor.v: valuation
out: nat
H: get "input" v = Some 0
H0: get "output" v = Some out
eval v factorial_loop ?v'
v: valuation
out: nat
H: get "input" v = Some 0
H0: get "output" v = Some out
get "output" ?v' = Some (out + 0)
n: nat
IHn: forall (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
eval v factorial_loop v' /\ get "output" v' = Some (fact n * out)
v: valuation
out: nat
H: get "input" v = Some (S n)
H0: get "output" v = Some out
exists v' : valuation,
  eval v factorial_loop v' /\
  get "output" v' = Some ((fact n + n * fact n) * out)
  apply EvalWhileFalse.v: valuation
out: nat
H: get "input" v = Some 0
H0: get "output" v = Some out
interp "input" v = 0
v: valuation
out: nat
H: get "input" v = Some 0
H0: get "output" v = Some out
get "output" v = Some (out + 0)
n: nat
IHn: forall (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
eval v factorial_loop v' /\ get "output" v' = Some (fact n * out)
v: valuation
out: nat
H: get "input" v = Some (S n)
H0: get "output" v = Some out
exists v' : valuation,
  eval v factorial_loop v' /\
  get "output" v' = Some ((fact n + n * fact n) * out)
  simpl in *.v: valuation
out: nat
H: get "input" v = Some 0
H0: get "output" v = Some out
match get "input" v with
| Some n => n
| None => 0
end = 0
v: valuation
out: nat
H: get "input" v = Some 0
H0: get "output" v = Some out
get "output" v = Some (out + 0)
n: nat
IHn: forall (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
eval v factorial_loop v' /\ get "output" v' = Some (fact n * out)
v: valuation
out: nat
H: get "input" v = Some (S n)
H0: get "output" v = Some out
exists v' : valuation,
  eval v factorial_loop v' /\
  get "output" v' = Some ((fact n + n * fact n) * out)
  rewrite H.v: valuation
out: nat
H: get "input" v = Some 0
H0: get "output" v = Some out
0 = 0
v: valuation
out: nat
H: get "input" v = Some 0
H0: get "output" v = Some out
get "output" v = Some (out + 0)
n: nat
IHn: forall (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
eval v factorial_loop v' /\ get "output" v' = Some (fact n * out)
v: valuation
out: nat
H: get "input" v = Some (S n)
H0: get "output" v = Some out
exists v' : valuation,
  eval v factorial_loop v' /\
  get "output" v' = Some ((fact n + n * fact n) * out)
  reflexivity.v: valuation
out: nat
H: get "input" v = Some 0
H0: get "output" v = Some out
get "output" v = Some (out + 0)
n: nat
IHn: forall (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
eval v factorial_loop v' /\ get "output" v' = Some (fact n * out)
v: valuation
out: nat
H: get "input" v = Some (S n)
H0: get "output" v = Some out
exists v' : valuation,
  eval v factorial_loop v' /\
  get "output" v' = Some ((fact n + n * fact n) * out)
  rewrite H0.v: valuation
out: nat
H: get "input" v = Some 0
H0: get "output" v = Some out
Some out = Some (out + 0)
n: nat
IHn: forall (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
eval v factorial_loop v' /\ get "output" v' = Some (fact n * out)
v: valuation
out: nat
H: get "input" v = Some (S n)
H0: get "output" v = Some out
exists v' : valuation,
  eval v factorial_loop v' /\
  get "output" v' = Some ((fact n + n * fact n) * out)
  f_equal.v: valuation
out: nat
H: get "input" v = Some 0
H0: get "output" v = Some out
out = out + 0
n: nat
IHn: forall (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
eval v factorial_loop v' /\ get "output" v' = Some (fact n * out)
v: valuation
out: nat
H: get "input" v = Some (S n)
H0: get "output" v = Some out
exists v' : valuation,
  eval v factorial_loop v' /\
  get "output" v' = Some ((fact n + n * fact n) * out)
  ring.n: nat
IHn: forall (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
eval v factorial_loop v' /\ get "output" v' = Some (fact n * out)
v: valuation
out: nat
H: get "input" v = Some (S n)
H0: get "output" v = Some out
exists v' : valuation,
  eval v factorial_loop v' /\
  get "output" v' = Some ((fact n + n * fact n) * out)
  assert (exists v',
             eval (set "input" n (set "output" (out * S n) v))
               factorial_loop v'
             /\ get "output" v' = Some (fact n * (out * S n))).n: nat
IHn: forall (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
eval v factorial_loop v' /\ get "output" v' = Some (fact n * out)
v: valuation
out: nat
H: get "input" v = Some (S n)
H0: get "output" v = Some out
exists v' : valuation,
  eval (set "input" n (set "output" (out * S n) v))
    factorial_loop v' /\
  get "output" v' = Some (fact n * (out * S n))
n: nat
IHn: forall (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
eval v factorial_loop v' /\ get "output" v' = Some (fact n * out)
v: valuation
out: nat
H: get "input" v = Some (S n)
H0: get "output" v = Some out
H1: exists v' : valuation,
  eval
    (set "input" n (set "output" (out * S n) v))
    factorial_loop v' /\
  get "output" v' = Some (fact n * (out * S n))
exists v' : valuation,
  eval v factorial_loop v' /\
  get "output" v' = Some ((fact n + n * fact n) * out)
  apply IHn.n: nat
IHn: forall (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
eval v factorial_loop v' /\ get "output" v' = Some (fact n * out)
v: valuation
out: nat
H: get "input" v = Some (S n)
H0: get "output" v = Some out
get "input"
  (set "input" n (set "output" (out * S n) v)) =
Some n
n: nat
IHn: forall (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
eval v factorial_loop v' /\ get "output" v' = Some (fact n * out)
v: valuation
out: nat
H: get "input" v = Some (S n)
H0: get "output" v = Some out
get "output"
  (set "input" n (set "output" (out * S n) v)) =
Some (out * S n)
n: nat
IHn: forall (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
eval v factorial_loop v' /\ get "output" v' = Some (fact n * out)
v: valuation
out: nat
H: get "input" v = Some (S n)
H0: get "output" v = Some out
H1: exists v' : valuation,
  eval
    (set "input" n (set "output" (out * S n) v))
    factorial_loop v' /\
  get "output" v' = Some (fact n * (out * S n))
exists v' : valuation,
  eval v factorial_loop v' /\
  get "output" v' = Some ((fact n + n * fact n) * out)
  reflexivity.n: nat
IHn: forall (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
eval v factorial_loop v' /\ get "output" v' = Some (fact n * out)
v: valuation
out: nat
H: get "input" v = Some (S n)
H0: get "output" v = Some out
get "output"
  (set "input" n (set "output" (out * S n) v)) =
Some (out * S n)
n: nat
IHn: forall (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
eval v factorial_loop v' /\ get "output" v' = Some (fact n * out)
v: valuation
out: nat
H: get "input" v = Some (S n)
H0: get "output" v = Some out
H1: exists v' : valuation,
  eval
    (set "input" n (set "output" (out * S n) v))
    factorial_loop v' /\
  get "output" v' = Some (fact n * (out * S n))
exists v' : valuation,
  eval v factorial_loop v' /\
  get "output" v' = Some ((fact n + n * fact n) * out)
  reflexivity.n: nat
IHn: forall (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
eval v factorial_loop v' /\ get "output" v' = Some (fact n * out)
v: valuation
out: nat
H: get "input" v = Some (S n)
H0: get "output" v = Some out
H1: exists v' : valuation,
  eval
    (set "input" n (set "output" (out * S n) v))
    factorial_loop v' /\
  get "output" v' = Some (fact n * (out * S n))
exists v' : valuation,
  eval v factorial_loop v' /\
  get "output" v' = Some ((fact n + n * fact n) * out)
  firstorder.n: nat
IHn: forall (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
eval v factorial_loop v' /\ get "output" v' = Some (fact n * out)
v: valuation
out: nat
H: get "input" v = Some (S n)
H0: get "output" v = Some out
x: valuation
H1: eval (set "input" n (set "output" (out * S n) v))
  factorial_loop x
H2: get "output" x = Some (fact n * (out * S n))
exists v' : valuation,
  eval v factorial_loop v' /\
  get "output" v' = Some ((fact n + n * fact n) * out)
  eexists; firstorder.n: nat
IHn: forall (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
eval v factorial_loop v' /\ get "output" v' = Some (fact n * out)
v: valuation
out: nat
H: get "input" v = Some (S n)
H0: get "output" v = Some out
x: valuation
H1: eval (set "input" n (set "output" (out * S n) v))
  factorial_loop x
H2: get "output" x = Some (fact n * (out * S n))
eval v factorial_loop ?v'
n: nat
IHn: forall (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
eval v factorial_loop v' /\ get "output" v' = Some (fact n * out)
v: valuation
out: nat
H: get "input" v = Some (S n)
H0: get "output" v = Some out
x: valuation
H1: eval (set "input" n (set "output" (out * S n) v))
  factorial_loop x
H2: get "output" x = Some (fact n * (out * S n))
get "output" ?v' = Some ((fact n + n * fact n) * out)
  econstructor.n: nat
IHn: forall (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
eval v factorial_loop v' /\ get "output" v' = Some (fact n * out)
v: valuation
out: nat
H: get "input" v = Some (S n)
H0: get "output" v = Some out
x: valuation
H1: eval (set "input" n (set "output" (out * S n) v))
  factorial_loop x
H2: get "output" x = Some (fact n * (out * S n))
interp "input" v <> 0
n: nat
IHn: forall (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
eval v factorial_loop v' /\ get "output" v' = Some (fact n * out)
v: valuation
out: nat
H: get "input" v = Some (S n)
H0: get "output" v = Some out
x: valuation
H1: eval (set "input" n (set "output" (out * S n) v))
  factorial_loop x
H2: get "output" x = Some (fact n * (out * S n))
eval v
  ("output" <- "output" * "input";;
   "input" <- "input" - 1) ?v'0
n: nat
IHn: forall (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
eval v factorial_loop v' /\ get "output" v' = Some (fact n * out)
v: valuation
out: nat
H: get "input" v = Some (S n)
H0: get "output" v = Some out
x: valuation
H1: eval (set "input" n (set "output" (out * S n) v))
  factorial_loop x
H2: get "output" x = Some (fact n * (out * S n))
eval ?v'0
  (while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?v'
n: nat
IHn: forall (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
eval v factorial_loop v' /\ get "output" v' = Some (fact n * out)
v: valuation
out: nat
H: get "input" v = Some (S n)
H0: get "output" v = Some out
x: valuation
H1: eval (set "input" n (set "output" (out * S n) v))
  factorial_loop x
H2: get "output" x = Some (fact n * (out * S n))
get "output" ?v' = Some ((fact n + n * fact n) * out)
  simpl.n: nat
IHn: forall (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
eval v factorial_loop v' /\ get "output" v' = Some (fact n * out)
v: valuation
out: nat
H: get "input" v = Some (S n)
H0: get "output" v = Some out
x: valuation
H1: eval (set "input" n (set "output" (out * S n) v))
  factorial_loop x
H2: get "output" x = Some (fact n * (out * S n))
match get "input" v with
| Some n => n
| None => 0
end <> 0
n: nat
IHn: forall (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
eval v factorial_loop v' /\ get "output" v' = Some (fact n * out)
v: valuation
out: nat
H: get "input" v = Some (S n)
H0: get "output" v = Some out
x: valuation
H1: eval (set "input" n (set "output" (out * S n) v))
  factorial_loop x
H2: get "output" x = Some (fact n * (out * S n))
eval v
  ("output" <- "output" * "input";;
   "input" <- "input" - 1) ?v'0
n: nat
IHn: forall (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
eval v factorial_loop v' /\ get "output" v' = Some (fact n * out)
v: valuation
out: nat
H: get "input" v = Some (S n)
H0: get "output" v = Some out
x: valuation
H1: eval (set "input" n (set "output" (out * S n) v))
  factorial_loop x
H2: get "output" x = Some (fact n * (out * S n))
eval ?v'0
  (while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?v'
n: nat
IHn: forall (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
eval v factorial_loop v' /\ get "output" v' = Some (fact n * out)
v: valuation
out: nat
H: get "input" v = Some (S n)
H0: get "output" v = Some out
x: valuation
H1: eval (set "input" n (set "output" (out * S n) v))
  factorial_loop x
H2: get "output" x = Some (fact n * (out * S n))
get "output" ?v' = Some ((fact n + n * fact n) * out)
  rewrite H.n: nat
IHn: forall (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
eval v factorial_loop v' /\ get "output" v' = Some (fact n * out)
v: valuation
out: nat
H: get "input" v = Some (S n)
H0: get "output" v = Some out
x: valuation
H1: eval (set "input" n (set "output" (out * S n) v))
  factorial_loop x
H2: get "output" x = Some (fact n * (out * S n))
S n <> 0
n: nat
IHn: forall (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
eval v factorial_loop v' /\ get "output" v' = Some (fact n * out)
v: valuation
out: nat
H: get "input" v = Some (S n)
H0: get "output" v = Some out
x: valuation
H1: eval (set "input" n (set "output" (out * S n) v))
  factorial_loop x
H2: get "output" x = Some (fact n * (out * S n))
eval v
  ("output" <- "output" * "input";;
   "input" <- "input" - 1) ?v'0
n: nat
IHn: forall (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
eval v factorial_loop v' /\ get "output" v' = Some (fact n * out)
v: valuation
out: nat
H: get "input" v = Some (S n)
H0: get "output" v = Some out
x: valuation
H1: eval (set "input" n (set "output" (out * S n) v))
  factorial_loop x
H2: get "output" x = Some (fact n * (out * S n))
eval ?v'0
  (while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?v'
n: nat
IHn: forall (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
eval v factorial_loop v' /\ get "output" v' = Some (fact n * out)
v: valuation
out: nat
H: get "input" v = Some (S n)
H0: get "output" v = Some out
x: valuation
H1: eval (set "input" n (set "output" (out * S n) v))
  factorial_loop x
H2: get "output" x = Some (fact n * (out * S n))
get "output" ?v' = Some ((fact n + n * fact n) * out)
  congruence.n: nat
IHn: forall (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
eval v factorial_loop v' /\ get "output" v' = Some (fact n * out)
v: valuation
out: nat
H: get "input" v = Some (S n)
H0: get "output" v = Some out
x: valuation
H1: eval (set "input" n (set "output" (out * S n) v))
  factorial_loop x
H2: get "output" x = Some (fact n * (out * S n))
eval v
  ("output" <- "output" * "input";;
   "input" <- "input" - 1) ?v'0
n: nat
IHn: forall (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
eval v factorial_loop v' /\ get "output" v' = Some (fact n * out)
v: valuation
out: nat
H: get "input" v = Some (S n)
H0: get "output" v = Some out
x: valuation
H1: eval (set "input" n (set "output" (out * S n) v))
  factorial_loop x
H2: get "output" x = Some (fact n * (out * S n))
eval ?v'0
  (while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?v'
n: nat
IHn: forall (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
eval v factorial_loop v' /\ get "output" v' = Some (fact n * out)
v: valuation
out: nat
H: get "input" v = Some (S n)
H0: get "output" v = Some out
x: valuation
H1: eval (set "input" n (set "output" (out * S n) v))
  factorial_loop x
H2: get "output" x = Some (fact n * (out * S n))
get "output" ?v' = Some ((fact n + n * fact n) * out)
  econstructor.n: nat
IHn: forall (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
eval v factorial_loop v' /\ get "output" v' = Some (fact n * out)
v: valuation
out: nat
H: get "input" v = Some (S n)
H0: get "output" v = Some out
x: valuation
H1: eval (set "input" n (set "output" (out * S n) v))
  factorial_loop x
H2: get "output" x = Some (fact n * (out * S n))
eval v ("output" <- "output" * "input") ?v1
n: nat
IHn: forall (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
eval v factorial_loop v' /\ get "output" v' = Some (fact n * out)
v: valuation
out: nat
H: get "input" v = Some (S n)
H0: get "output" v = Some out
x: valuation
H1: eval (set "input" n (set "output" (out * S n) v))
  factorial_loop x
H2: get "output" x = Some (fact n * (out * S n))
eval ?v1 ("input" <- "input" - 1) ?v'0
n: nat
IHn: forall (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
eval v factorial_loop v' /\ get "output" v' = Some (fact n * out)
v: valuation
out: nat
H: get "input" v = Some (S n)
H0: get "output" v = Some out
x: valuation
H1: eval (set "input" n (set "output" (out * S n) v))
  factorial_loop x
H2: get "output" x = Some (fact n * (out * S n))
eval ?v'0
  (while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?v'
n: nat
IHn: forall (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
eval v factorial_loop v' /\ get "output" v' = Some (fact n * out)
v: valuation
out: nat
H: get "input" v = Some (S n)
H0: get "output" v = Some out
x: valuation
H1: eval (set "input" n (set "output" (out * S n) v))
  factorial_loop x
H2: get "output" x = Some (fact n * (out * S n))
get "output" ?v' = Some ((fact n + n * fact n) * out)
  econstructor.n: nat
IHn: forall (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
eval v factorial_loop v' /\ get "output" v' = Some (fact n * out)
v: valuation
out: nat
H: get "input" v = Some (S n)
H0: get "output" v = Some out
x: valuation
H1: eval (set "input" n (set "output" (out * S n) v))
  factorial_loop x
H2: get "output" x = Some (fact n * (out * S n))
eval
  (set "output" (interp ("output" * "input")%arith v)
     v) ("input" <- "input" - 1) ?v'0
n: nat
IHn: forall (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
eval v factorial_loop v' /\ get "output" v' = Some (fact n * out)
v: valuation
out: nat
H: get "input" v = Some (S n)
H0: get "output" v = Some out
x: valuation
H1: eval (set "input" n (set "output" (out * S n) v))
  factorial_loop x
H2: get "output" x = Some (fact n * (out * S n))
eval ?v'0
  (while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?v'
n: nat
IHn: forall (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
eval v factorial_loop v' /\ get "output" v' = Some (fact n * out)
v: valuation
out: nat
H: get "input" v = Some (S n)
H0: get "output" v = Some out
x: valuation
H1: eval (set "input" n (set "output" (out * S n) v))
  factorial_loop x
H2: get "output" x = Some (fact n * (out * S n))
get "output" ?v' = Some ((fact n + n * fact n) * out)
  econstructor.n: nat
IHn: forall (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
eval v factorial_loop v' /\ get "output" v' = Some (fact n * out)
v: valuation
out: nat
H: get "input" v = Some (S n)
H0: get "output" v = Some out
x: valuation
H1: eval (set "input" n (set "output" (out * S n) v))
  factorial_loop x
H2: get "output" x = Some (fact n * (out * S n))
eval
  (set "input"
     (interp ("input" - 1)%arith
        (set "output"
           (interp ("output" * "input")%arith v) v))
     (set "output"
        (interp ("output" * "input")%arith v) v))
  (while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?v'
n: nat
IHn: forall (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
eval v factorial_loop v' /\ get "output" v' = Some (fact n * out)
v: valuation
out: nat
H: get "input" v = Some (S n)
H0: get "output" v = Some out
x: valuation
H1: eval (set "input" n (set "output" (out * S n) v))
  factorial_loop x
H2: get "output" x = Some (fact n * (out * S n))
get "output" ?v' = Some ((fact n + n * fact n) * out)
  simpl.n: nat
IHn: forall (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
eval v factorial_loop v' /\ get "output" v' = Some (fact n * out)
v: valuation
out: nat
H: get "input" v = Some (S n)
H0: get "output" v = Some out
x: valuation
H1: eval (set "input" n (set "output" (out * S n) v))
  factorial_loop x
H2: get "output" x = Some (fact n * (out * S n))
eval
  (set "input"
     (match
        get "input"
          (set "output"
             (match get "output" v with
              | Some n => n
              | None => 0
              end *
              match get "input" v with
              | Some n => n
              | None => 0
              end) v)
      with
      | Some n => n
      | None => 0
      end - 1)
     (set "output"
        (match get "output" v with
         | Some n => n
         | None => 0
         end *
         match get "input" v with
         | Some n => n
         | None => 0
         end) v))
  (while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?v'
n: nat
IHn: forall (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
eval v factorial_loop v' /\ get "output" v' = Some (fact n * out)
v: valuation
out: nat
H: get "input" v = Some (S n)
H0: get "output" v = Some out
x: valuation
H1: eval (set "input" n (set "output" (out * S n) v))
  factorial_loop x
H2: get "output" x = Some (fact n * (out * S n))
get "output" ?v' = Some ((fact n + n * fact n) * out)
  rewrite H, H0, get_set_neq, H by congruence.n: nat
IHn: forall (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
eval v factorial_loop v' /\ get "output" v' = Some (fact n * out)
v: valuation
out: nat
H: get "input" v = Some (S n)
H0: get "output" v = Some out
x: valuation
H1: eval (set "input" n (set "output" (out * S n) v))
  factorial_loop x
H2: get "output" x = Some (fact n * (out * S n))
eval
  (set "input" (S n - 1) (set "output" (out * S n) v))
  (while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?v'
n: nat
IHn: forall (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
eval v factorial_loop v' /\ get "output" v' = Some (fact n * out)
v: valuation
out: nat
H: get "input" v = Some (S n)
H0: get "output" v = Some out
x: valuation
H1: eval (set "input" n (set "output" (out * S n) v))
  factorial_loop x
H2: get "output" x = Some (fact n * (out * S n))
get "output" ?v' = Some ((fact n + n * fact n) * out)
  replace (S n - 1) with n by lia.n: nat
IHn: forall (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
eval v factorial_loop v' /\ get "output" v' = Some (fact n * out)
v: valuation
out: nat
H: get "input" v = Some (S n)
H0: get "output" v = Some out
x: valuation
H1: eval (set "input" n (set "output" (out * S n) v))
  factorial_loop x
H2: get "output" x = Some (fact n * (out * S n))
eval (set "input" n (set "output" (out * S n) v))
  (while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?v'
n: nat
IHn: forall (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
eval v factorial_loop v' /\ get "output" v' = Some (fact n * out)
v: valuation
out: nat
H: get "input" v = Some (S n)
H0: get "output" v = Some out
x: valuation
H1: eval (set "input" n (set "output" (out * S n) v))
  factorial_loop x
H2: get "output" x = Some (fact n * (out * S n))
get "output" ?v' = Some ((fact n + n * fact n) * out)
  (* [replace e1 with e2 by tac]:
       replace occurrences of [e1] with [e2], proving
       [e2 = e1] with tactic [tac]. *)
  apply H1.n: nat
IHn: forall (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
eval v factorial_loop v' /\ get "output" v' = Some (fact n * out)
v: valuation
out: nat
H: get "input" v = Some (S n)
H0: get "output" v = Some out
x: valuation
H1: eval (set "input" n (set "output" (out * S n) v))
  factorial_loop x
H2: get "output" x = Some (fact n * (out * S n))
get "output" x = Some ((fact n + n * fact n) * out)
  rewrite H2.n: nat
IHn: forall (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
eval v factorial_loop v' /\ get "output" v' = Some (fact n * out)
v: valuation
out: nat
H: get "input" v = Some (S n)
H0: get "output" v = Some out
x: valuation
H1: eval (set "input" n (set "output" (out * S n) v))
  factorial_loop x
H2: get "output" x = Some (fact n * (out * S n))
Some (fact n * (out * S n)) =
Some ((fact n + n * fact n) * out)
  f_equal.n: nat
IHn: forall (v : valuation) (out : nat),
get "input" v = Some n ->
get "output" v = Some out ->
exists v' : valuation,
eval v factorial_loop v' /\ get "output" v' = Some (fact n * out)
v: valuation
out: nat
H: get "input" v = Some (S n)
H0: get "output" v = Some out
x: valuation
H1: eval (set "input" n (set "output" (out * S n) v))
  factorial_loop x
H2: get "output" x = Some (fact n * (out * S n))
fact n * (out * S n) = (fact n + n * fact n) * out
  ring.
Qed.

We then prove the correctness of the full program using the above lemma.

Theorem factorial_correct : forall n v,
    get "input" v = Some n
    -> exists v',
      eval v factorial v'
      /\ get "output" v' = Some (fact n).forall (n : nat) (v : valuation),
get "input" v = Some n ->
exists v' : valuation,
  eval v factorial v' /\
  get "output" v' = Some (fact n)
Proof.forall (n : nat) (v : valuation),
get "input" v = Some n ->
exists v' : valuation,
  eval v factorial v' /\
  get "output" v' = Some (fact n)
  intros.n: nat
v: valuation
H: get "input" v = Some n
exists v' : valuation,
  eval v factorial v' /\
  get "output" v' = Some (fact n)
  assert (exists v',
             eval (set "output" 1 v) factorial_loop v'
             /\ get "output" v' = Some (fact n * 1)).n: nat
v: valuation
H: get "input" v = Some n
exists v' : valuation,
  eval (set "output" 1 v) factorial_loop v' /\
  get "output" v' = Some (fact n * 1)
n: nat
v: valuation
H: get "input" v = Some n
H0: exists v' : valuation,
  eval (set "output" 1 v) factorial_loop v' /\
  get "output" v' = Some (fact n * 1)
exists v' : valuation,
  eval v factorial v' /\
  get "output" v' = Some (fact n)
  apply factorial_loop_correct.n: nat
v: valuation
H: get "input" v = Some n
get "input" (set "output" 1 v) = Some n
n: nat
v: valuation
H: get "input" v = Some n
get "output" (set "output" 1 v) = Some 1
n: nat
v: valuation
H: get "input" v = Some n
H0: exists v' : valuation,
  eval (set "output" 1 v) factorial_loop v' /\
  get "output" v' = Some (fact n * 1)
exists v' : valuation,
  eval v factorial v' /\
  get "output" v' = Some (fact n)
  rewrite get_set_neq; congruence.n: nat
v: valuation
H: get "input" v = Some n
get "output" (set "output" 1 v) = Some 1
n: nat
v: valuation
H: get "input" v = Some n
H0: exists v' : valuation,
  eval (set "output" 1 v) factorial_loop v' /\
  get "output" v' = Some (fact n * 1)
exists v' : valuation,
  eval v factorial v' /\
  get "output" v' = Some (fact n)
  rewrite get_set_eq; congruence.n: nat
v: valuation
H: get "input" v = Some n
H0: exists v' : valuation,
  eval (set "output" 1 v) factorial_loop v' /\
  get "output" v' = Some (fact n * 1)
exists v' : valuation,
  eval v factorial v' /\
  get "output" v' = Some (fact n)
  destruct H0 as (v' & ? & ?).n: nat
v: valuation
H: get "input" v = Some n
v': valuation
H0: eval (set "output" 1 v) factorial_loop v'
H1: get "output" v' = Some (fact n * 1)
exists v' : valuation,
  eval v factorial v' /\
  get "output" v' = Some (fact n)
  eexists; split.n: nat
v: valuation
H: get "input" v = Some n
v': valuation
H0: eval (set "output" 1 v) factorial_loop v'
H1: get "output" v' = Some (fact n * 1)
eval v factorial ?v'
n: nat
v: valuation
H: get "input" v = Some n
v': valuation
H0: eval (set "output" 1 v) factorial_loop v'
H1: get "output" v' = Some (fact n * 1)
get "output" ?v' = Some (fact n)
  econstructor.n: nat
v: valuation
H: get "input" v = Some n
v': valuation
H0: eval (set "output" 1 v) factorial_loop v'
H1: get "output" v' = Some (fact n * 1)
eval v ("output" <- 1) ?v1
n: nat
v: valuation
H: get "input" v = Some n
v': valuation
H0: eval (set "output" 1 v) factorial_loop v'
H1: get "output" v' = Some (fact n * 1)
eval ?v1
  (while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?v'
n: nat
v: valuation
H: get "input" v = Some n
v': valuation
H0: eval (set "output" 1 v) factorial_loop v'
H1: get "output" v' = Some (fact n * 1)
get "output" ?v' = Some (fact n)
  econstructor.n: nat
v: valuation
H: get "input" v = Some n
v': valuation
H0: eval (set "output" 1 v) factorial_loop v'
H1: get "output" v' = Some (fact n * 1)
eval (set "output" (interp 1 v) v)
  (while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?v'
n: nat
v: valuation
H: get "input" v = Some n
v': valuation
H0: eval (set "output" 1 v) factorial_loop v'
H1: get "output" v' = Some (fact n * 1)
get "output" ?v' = Some (fact n)
  simpl.n: nat
v: valuation
H: get "input" v = Some n
v': valuation
H0: eval (set "output" 1 v) factorial_loop v'
H1: get "output" v' = Some (fact n * 1)
eval (set "output" 1 v)
  (while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?v'
n: nat
v: valuation
H: get "input" v = Some n
v': valuation
H0: eval (set "output" 1 v) factorial_loop v'
H1: get "output" v' = Some (fact n * 1)
get "output" ?v' = Some (fact n)
  apply H0.n: nat
v: valuation
H: get "input" v = Some n
v': valuation
H0: eval (set "output" 1 v) factorial_loop v'
H1: get "output" v' = Some (fact n * 1)
get "output" v' = Some (fact n)
  rewrite H1.n: nat
v: valuation
H: get "input" v = Some n
v': valuation
H0: eval (set "output" 1 v) factorial_loop v'
H1: get "output" v' = Some (fact n * 1)
Some (fact n * 1) = Some (fact n)
  f_equal.n: nat
v: valuation
H: get "input" v = Some n
v': valuation
H0: eval (set "output" 1 v) factorial_loop v'
H1: get "output" v' = Some (fact n * 1)
fact n * 1 = fact n
  ring.
Qed.