(*|
==================
Big-step semantics
==================

:status: hidden

Author
  `Adam Chlipala <http://adam.chlipala.net/frap/>`__,
  Nate Foster,
  Dario Halilovic

License
  No redistribution allowed (usage by permission in CS-428).

.. contents::

.. coq:: none
|*)

Require Import String List Arith Lia.
Import ListNotations.
Open Scope list_scope.
Open Scope string_scope.

Set Implicit Arguments.

(*|
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.
Proof.
  unfold set, get; intros. (* .unfold *)
  destruct string_dec; congruence.
Qed.

Lemma get_set_eq (x y: var) n v :
  x = y -> get x (set y n v) = Some n.
Proof.
  unfold set, get; intros. (* .unfold *)
  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).
Notation "'while' e 'loop' body 'done'" :=
  (While e%arith body) (at level 75).

(*|
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.
Proof.
  eexists.
  econstructor.
  econstructor.
  econstructor.
  simpl in *.
  econstructor.
  simpl in *.
  lia.
  econstructor.
  econstructor.
  econstructor.
  simpl in *.
  econstructor.
  simpl in *.
  lia.
  econstructor.
  econstructor.
  econstructor.
  apply EvalWhileFalse.
  simpl in *.
  econstructor.
  simpl in *.
  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.
Proof.
  eexists.
  evaluate.
  evaluate.
Qed.

Theorem factorial_3 : exists v,
    eval (set "input" 3 empty) factorial v
    /\ get "output" v = Some 6.
Proof.
  eexists.
  evaluate.
  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).
Proof.
  induction n; simpl in *; intros. (* .unfold *)
  eexists.
  econstructor.
  apply EvalWhileFalse.
  simpl in *.
  rewrite H.
  reflexivity.
  rewrite H0.
  f_equal.
  ring.
  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))).
  apply IHn.
  reflexivity.
  reflexivity.
  firstorder.
  eexists; firstorder.
  econstructor.
  simpl.
  rewrite H.
  congruence.
  econstructor.
  econstructor.
  econstructor.
  simpl.
  rewrite H, H0, get_set_neq, H by congruence.
  replace (S n - 1) with n by lia.
  (* [replace e1 with e2 by tac]:
       replace occurrences of [e1] with [e2], proving
       [e2 = e1] with tactic [tac]. *)
  apply H1.
  rewrite H2.
  f_equal.
  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).
Proof.
  intros.
  assert (exists v',
             eval (set "output" 1 v) factorial_loop v'
             /\ get "output" v' = Some (fact n * 1)).
  apply factorial_loop_correct.
  rewrite get_set_neq; congruence.
  rewrite get_set_eq; congruence.
  destruct H0 as (v' & ? & ?).
  eexists; split.
  econstructor.
  econstructor.
  simpl.
  apply H0.
  rewrite H1.
  f_equal.
  ring.
Qed.