PreTalent23.Spl_before_third_session
SimPle Language (SPL)
Inductive expr :=
| Num (n : nat)
| Bool (b : bool)
| ITE (c t f : expr)
| And (e1 e2 : expr)
| Or (e1 e2 : expr)
| Not (e : expr)
| Le (e1 e2 : expr)
| Eq (e1 e2 : expr)
| Add (e1 e2 : expr)
| Sub (e1 e2 : expr)
| Mul (e1 e2 : expr).
Example add23 := Add (Num 2) (Num 3).
Example if3le5 := ITE ((Le (Num 3) (Num 5))) (Num 2) (Num 3).
Example bad_prog := ITE (Num 3) (Num 4) (Num 5).
Example sub74 := Sub (Num 7) (Num 4).
The semantics of SPL
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.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?
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 n : res_typed (BoolRes n) TBool.
Inductive typed : expr → typ → Prop :=
| Num_typed n : typed (Num n) TNum
| Bool_typed b : typed (Bool b) TBool
| ITE_typed c t f tp :
typed c TBool →
typed t tp →
typed f tp →
typed (ITE c t f) tp
| And_typed e1 e2 : typed e1 TBool → typed e2 TBool → typed (And e1 e2) TBool
| Or_typed e1 e2 : typed e1 TBool → typed e2 TBool → typed (Or e1 e2) TBool
| Not_typed e : typed e TBool → typed (Not e) TBool
| Le_typed e1 e2 : typed e1 TNum → typed e2 TNum → typed (Le e1 e2) TBool
| Eq_typed e1 e2 : typed e1 TNum → typed e2 TNum → typed (Eq e1 e2) TBool
| Add_typed e1 e2 : typed e1 TNum → typed e2 TNum → typed (Add e1 e2) TNum
| Sub_typed e1 e2 : typed e1 TNum → typed e2 TNum → typed (Sub e1 e2) TNum
| Mul_typed e1 e2 : typed e1 TNum → typed e2 TNum → typed (Mul e1 e2) TNum.
The eval function respects types
Exercise (in class)
Once the typing relations above are completed, the induction in theorem below will have more cases. Finish the proof.
Local Ltac solve_respects_type :=
repeat match goal with
| |- res_typed (NumRes _) TNum => constructor
| |- res_typed (BoolRes _) TBool => constructor
| |- context [eval ?e >>n= _] => destruct (eval e); simpl
| |- context [eval ?e >>b= _] => destruct (eval e); simpl
| H : res_typed Err _ |- _ => inversion H
| H : res_typed (NumRes _) TBool |- _ => inversion H
| H : res_typed (BoolRes _) TNum |- _ => inversion H
end.
Theorem eval_respects_types (e : expr) (t : typ) : typed e t → res_typed (eval e) t.
Proof.
intros Htp.
induction Htp; simpl; solve_respects_type.
destruct b; auto.
Qed.
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.
intros Htp.
apply eval_respects_types in Htp.
intros He; rewrite He in Htp.
inversion Htp.
Qed.
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.
Prove the following theorem.
Exercise
Prove the following theorem.