PreTalent23.Spl_in_class

From PreTalent23 Require Import Overture.

SimPle Language (SPL)

We define the syntax (Abstract Syntax Trees) of SPL as an inductive type. (Note how we are not giving the universe for this type and Coq correctly guesses it; use the Print expr command to see this.)

This simple language only features natural numbers and booleans and allows one to write simple programs (no functions, loops, etc.) for basic computations.

The semantics of SPL

We define semantics of SPL using a definitional interpreter. That is, we define a function eval, an interpreter, that given an SPL program computes the end result of that program.

We will first define the type of the results, result, that a computation might produce.

Inductive result :=
| NumRes (n : nat)
| BoolRes (b : bool)
| Err.

Discuss in class

Why does this type also include an Err constructor?

Useful functions for working with results

We define two functions on result for computing one result based on an earlier result. The function when_num takes an r and function f that applies when the input is a number. If r is indeed a number, we get the result of f applied to that number. Otherwise, we get an error. The function when_bool is defined similarly.

The functions when_num and when_bool provide a layer of abstraction and hide the case analysis that would otherwise clutter the definition of the eval function.

Definition when_num (r : result) (f : nat → result) : result :=
  match r with
  | NumRes n => f n
  | _ => Err
  end.

Notation "r >>n= f" := (when_num r f) (at level 60, right associativity).

Lemma when_num_not_Err r f : r >>n = f ≠ Err → r ≠ Err.
Proof. intros Hr ->; apply Hr; trivial. Qed.

Lemma when_num_correct1 r f : r >>n = f ≠ Err → ∃ n , r = NumRes n.
Proof. destruct r; [eauto|simpl; congruence|simpl; congruence]. Qed.

Lemma when_num_correct2 r f :
  r >>n = f = Err → r = Err ∨ (∃ b , r = BoolRes b ) ∨ ∃ n , r = NumRes n ∧ f n = Err.
Proof. destruct r; eauto. Qed.

Definition when_bool (r : result) (f : bool → result) : result :=
  match r with
  | BoolRes b => f b
  | _ => Err
  end.

Notation "r >>b= f" := (when_bool r f) (at level 60, right associativity).

Lemma when_bool_not_Err r f : r >>b = f ≠ Err → r ≠ Err.
Proof. intros Hr ->; apply Hr; trivial. Qed.

Lemma when_bool_correct1 r f : r >>b = f ≠ Err → ∃ b , r = BoolRes b.
Proof. destruct r; [simpl; congruence|eauto|simpl; congruence]. Qed.

Lemma when_bool_correct2 r f :
  r >>b = f = Err → r = Err ∨ (∃ n , r = NumRes n ) ∨ ∃ b , r = BoolRes b ∧ f b = Err.
Proof. destruct r; eauto. Qed.

The eval function

We define the eval function as follows:

Exercise (in class)

Complete the [eval] function below:

Fixpoint eval (e : expr) : result :=
  match e with
  | Num n => NumRes n
  | Bool b => BoolRes b
  | ITE c t f =>
      eval c >>b = (λ b , if b then eval t else eval f)
  | And e1 e2 => eval e1 >>b = (λ b1 , eval e2 >>b = (λ b2 , BoolRes (b1 && b2)))
  | Or e1 e2 => eval e1 >>b = (λ b1 , eval e2 >>b = (λ b2 , BoolRes (b1 || b2)))
  | Not e => eval e >>b = (λ b , BoolRes (negb b))
  | Le e1 e2 => eval e1 >>n = (λ n1 , eval e2 >>n = (λ n2 , BoolRes (Nat.leb n1 n2)))
  | Eq e1 e2 => eval e1 >>n = (λ n1 , eval e2 >>n = (λ n2 , BoolRes (Nat.eqb n1 n2)))
  | Add e1 e2 => eval e1 >>n = (λ n1 , eval e2 >>n = (λ n2 , NumRes (n1 + n2)))
  | Sub e1 e2 => eval e1 >>n = (λ n1 , eval e2 >>n = (λ n2 , NumRes (n1 - n2)))
  | Mul e1 e2 => eval e1 >>n = (λ n1 , eval e2 >>n = (λ n2 , NumRes (n1 * n2)))
  end.

Eval compute in eval add23. (* Should print: NumRes 5 *)

Eval compute in eval if3le5. (* Should print: NumRes 2 *)

Eval compute in eval bad_prog. (* Should print: Err *)

Eval compute in eval sub74. (* Should print: NumRes 3 *)

What goes wrong when we get an error in evaluating SPL programs?

The issue seems to be a typing issue: the bad_prog above is ill-typed! Let us put this hypothesis to test: we will define types and the typing relation for SPL programs and try to prove that all well-typed programs do not result in error.

Inductive typ :=
| TNum
| TBool.

Exercise (in class)

Complete the following typing relations for expressions and results:

Inductive res_typed : result → typ → Prop :=
| NumRes_typed n : res_typed (NumRes n) TNum
| BoolRes_typed b : res_typed (BoolRes b) TBool.

Inductive typed : expr → typ → Prop :=
| Num_typed n : typed (Num n) TNum
| Bool_typed b : typed (Bool b) TBool
| IFE_typed c t f typ :
  typed c TBool →
  typed t typ →
  typed f typ →
  typed (ITE c t f) typ
| And_typed e1 e2 :
  typed e1 TBool →
  typed e2 TBool →
  typed (And e1 e2) TBool
| Le_typed e1 e2 :
  typed e1 TNum →
  typed e2 TNum →
  typed (Le e1 e2) TBool.

The eval function respects types

The following theorem states that if an SPL program is well-typed then the result obtained by the eval function has the same type.

Exercise (in class)

Once the typing relations above are completed, the induction in theorem below will have more cases. Finish the proof.

Theorem eval_respects_types (e : expr) (t : typ) : typed e t → res_typed (eval e) t.
Proof.
  intros Htp.
  induction Htp.
  - constructor.
  - constructor.
  - simpl.
    destruct (eval c).
    + inversion IHHtp1.
    + simpl.
      destruct b; trivial.
    + inversion IHHtp1.
  - simpl.
    destruct (eval e1).
    + inversion IHHtp1.
    + simpl.
      destruct (eval e2).
      * inversion IHHtp2.
      * simpl. constructor.
      * inversion IHHtp2.
    + inversion IHHtp1.
  -
Abort.

Type soundness

The following theorem is usually referred to as the type safety or type soundness theorem. It states that well-typed programs do not result in an error. The type soundness theorem is one of the main properties that we usually prove about typed programming languages. In our settings, type soundness is a corollary of the theorem above, eval_respects_types.

Exercise

Prove the following corollary.

Corollary typed_soundness e t : typed e t → eval e ≠ Err.
Proof.
Abort.

In addition to soundness of a type system, one can ask whether it is complete or not. That is, is it the case that any program that does not result in an error is well-typed according to our typing relation? The answer very often, if not always, is no, and SPL is no exception. In fact, in SPL there are programs that do not result in an error but are also not well-typed.

Exercise

Prove the following theorem.

Theorem typing_not_complete : ∃ e , eval e ≠ Err ∧ ∀ t , typed e t → False.
Proof.
(* hint: use inversion on the typed relation. *)
Abort.