Library ex12

Blatt 12 —- Types

SemProg SoSe 2013, Set 12

Based on the material of the online course "Software Foundations" by Pierce et al. Submit your solutions to tadeusz.m.litak at cs.fau.de

Please submit by Jul 23, anywhere on earth.

As we haven't shown so much yet for simply typed lambda calculus, in most of the Blatt we only use the file Types:

Require Export Types.

... and we will only import Stlc for the last exercise. Don't import it earlier to avoid possible clashes, e.g., with the step relation. In Exercises 1-3, we are concerned with the simple language introduced in the Types.v chapter and its operational semantics.

Exercise 1 (preservation_alternative_proof)

In the Types.v lecture, we have shown the type preservation theorem for our simple language by induction on the deriviation of the typing judgement. Now prove the same property again by induction on the evaluation derivation instead of on the typing derivation. Begin by carefully reading and thinking about the first few lines of the above proof to make sure you understand what each one is doing. The set-up for this proof is similar, but not exactly the same.

Theorem preservation_alternative_proof : forall t t' T,
  |- t \in T ->
  t ==> t' ->
  |- t' \in T.
Proof with eauto.
  intros t t' T HT HE. generalize dependent T.
     induction HE.

<- you might want to replace the last dot by semicolon...

Admitted.

☐

Exercise 2: (expansion)/(failure_of_expansion)

Having seen the subject reduction property, it is reasonable to wonder whether the opposity property — subject expansion — also holds. That is, is it always the case that, if t ==> t' and |- t' \in T, then |- t \in T?

If you believe it is true, then show

Theorem expansion : forall t t' T,
  (|- t' \in T) ->
  (t ==> t') ->
  (|- t \in T).
Proof. Admitted.

If you believe it is false, then show

Theorem failure_of_expansion : exists t t' T,
  (|- t' \in T) /\
  (t ==> t') /\
  ~(|- t \in T).
Proof. Admitted.

Exercise 3 (silly step)

Module silly_step.

In this exercise, we consider possible consequences of modifications to the definition of small-step semantics. We will just add one plausible and innocent-looking rule...

Inductive step : tm -> tm -> Prop :=
  | ST_IfTrue : forall t1 t2,
      (tif ttrue t1 t2) ==> t1
  | ST_IfFalse : forall t1 t2,
      (tif tfalse t1 t2) ==> t2
  | ST_If : forall t1 t1' t2 t3,
      t1 ==> t1' ->
      (tif t1 t2 t3) ==> (tif t1' t2 t3)
  | ST_Succ : forall t1 t1',
      t1 ==> t1' ->
      (tsucc t1) ==> (tsucc t1')
  | ST_PredZero :
      (tpred tzero) ==> tzero
  | ST_PredSucc : forall t1,
      nvalue t1 ->
      (tpred (tsucc t1)) ==> t1
  | ST_Pred : forall t1 t1',
      t1 ==> t1' ->
      (tpred t1) ==> (tpred t1')
  | ST_IszeroZero :
      (tiszero tzero) ==> ttrue
  | ST_IszeroSucc : forall t1,
       nvalue t1 ->
      (tiszero (tsucc t1)) ==> tfalse
  | ST_Iszero : forall t1 t1',
      t1 ==> t1' ->
      (tiszero t1) ==> (tiszero t1')
  | ST_IfThenStep : forall t1 t2 t2' t3,
           t2 ==> t2' ->
           (tif t1 t2 t3) ==> (tif t1 t2' t3)

where "t1 '==>' t2" := (step t1 t2).

Tactic Notation "step_cases" tactic(first) ident(c) :=
  first;
  [ Case_aux c "ST_IfTrue" | Case_aux c "ST_IfFalse" | Case_aux c "ST_If"
  | Case_aux c "ST_Succ" | Case_aux c "ST_PredZero"
  | Case_aux c "ST_PredSucc" | Case_aux c "ST_Pred"
  | Case_aux c "ST_IszeroZero" | Case_aux c "ST_IszeroSucc"
  | Case_aux c "ST_Iszero"
| Case_aux c "ST_IfThenStep" ].

Hint Constructors step.

Print step_normal_form.

Definition step_normal_form := normal_form step.

Print step_normal_form.

Is every value still a normal form? If so, then prove

Lemma value_is_nf : forall t,
value t -> step_normal_form t.
Proof. Admitted.

Or perhaps it is not true anymore? Prove then

Lemma not_every_value_nf : exists t,
value t /\ ~ (step_normal_form t).
Proof. Admitted.

Does the step relation remain deterministic? If so, then prove

Theorem step_deterministic:
deterministic step.
Proof. Admitted.

If not, then show

Theorem step_nondeterministic:
exists x y1 y2 : tm, x ==> y1 /\ x ==> y2 /\ ~(y1 = y2).
Proof. Admitted.

☐

End silly_step.

Exercise 4 (substi), (substi_correct)

In this last exercise, we finally consider simply typed lambda calculus...

Require Export Stlc.
Import STLC.

The definition of substitution that we gave in the lecture uses Coq's Fixpoint facility to define substitution as a function. Suppose, instead, we wanted to define substitution as an inductive relation substi. We've begun the definition by providing the Inductive header and one of the constructors; your job is to fill in the rest of the constructors.

Inductive substi (s:tm) (x:id) : tm -> tm -> Prop :=
  | s_var1 :
      substi s x (tvar x) s

.

Hint Constructors substi.

Theorem substi_correct : forall s x t t',
  [x:=s]t = t' <-> substi s x t t'.
Proof.
Admitted.

☐