Module FUN

From Coq Require Import Bool String List Program.Equality.
From CDF Require Import Sequences.

Local Open Scope string_scope.
Local Open Scope list_scope.

7. The functional language FUN


7.1. Syntax and semantics


The FUN language is lambda-calculus (variables, function abstractions, function applications) extended with Booleans: constants Const true and Const false, and a conditional Cond a ifso ifnot (that is, if a then ifso else ifnot).
 
Inductive term: Type :=
  | Var (x: string)
  | Abs (x: string) (a: term)
  | App (a1: term) (a2: term)
  | Const (b: bool)
  | Cond (a: term) (ifso: term) (ifnot: term).

Values are function abstractions and Boolean constants.

Inductive isvalue: term -> Prop :=
  | V_Abs: forall x a,
      isvalue (Abs x a)
  | V_Const: forall b,
      isvalue (Const b).

subst a x c is the term a where the term c is substituted for variable x, also written a [x ← c] in the lecture.

The substitution below is wrong in general, because it can capture variables that are free in c. We shall use it only when c is a closed term, without free variables. This corresponds to the reduction of whole programs, without free variables. The type system in section 7.2 guarantees that this is the case.

Fixpoint subst (a: term) (x: string) (c: term) : term :=
  match a with
  | Var y => if string_dec x y then c else Var y
  | Abs y a => if string_dec x y then Abs y a else Abs y (subst a x c)
  | App a1 a2 => App (subst a1 x c) (subst a2 x c)
  | Const b => Const b
  | Cond a ifso ifnot => Cond (subst a x c) (subst ifso x c) (subst ifnot x c)
  end.

The reduction semantics: red a a' means that a reduces in one step to a'. We choose a call-by-value semantics, with applications being evaluated from left to right.

Inductive red: term -> term -> Prop :=
  | red_beta: forall x a v, (* call-by-value beta reduction *)
      isvalue v ->
      red (App (Abs x a) v) (subst a x v)
  | red_cond: forall b ifso ifnot, (* reduction for conditionals *)
      red (Cond (Const b) ifso ifnot) (if b then ifso else ifnot)
  | red_app_1: forall a1 a2 a1', (* reduction to the left of an application *)
      red a1 a1' ->
      red (App a1 a2) (App a1' a2)
  | red_app_2: forall v a2 a2', (* reduction to the right of an application *)
      isvalue v -> red a2 a2' ->
      red (App v a2) (App v a2')
  | red_cond_1: forall a a' ifso ifnot, (* reduction under a Cond *)
      red a a' ->
      red (Cond a ifso ifnot) (Cond a' ifso ifnot).

Exercise (1 star)

Modify red to obtain a call-by-name semantics. What is the impact of this change on the results in the remainder of this module?

Exercise (2 stars)

Extend the syntax and the semantics of FUN with one or several of the features mentioned in the lecture: Peano integers, products, sums, fixed points.

Another presentation of the reduction semantics, in the style popularized by Wright and Felleisen. First we define head reductions.

Inductive head_red: term -> term -> Prop :=
  | head_red_beta: forall x a v,
      isvalue v ->
      head_red (App (Abs x a) v) (subst a x v)
  | head_red_cond: forall b ifso ifnot,
      head_red (Cond (Const b) ifso ifnot) (if b then ifso else ifnot).

Then we define the reduction contexts. Contexts are represented by functions C: term -> term. The inductive predicate iscontext C defines which functions are valid reduction contexts.

Inductive iscontext: (term -> term) -> Prop :=
  | iscontext_hole: (* at the top *)
      iscontext (fun a => a)
  | iscontext_app_1: forall a C, (* to the left of an application *)
      iscontext C -> iscontext (fun x => App (C x) a)
  | iscontext_app_2: forall v C, (* to the right of an application *)
      isvalue v -> iscontext C -> iscontext (fun x => App v (C x))
  | iscontext_cond: forall C ifso ifnot, (* under a conditional *)
      iscontext C -> iscontext (fun x => Cond (C x) ifso ifnot).

Finally, we define reductions under a context.

Inductive ctx_red: term -> term -> Prop :=
  | ctx_red_intro: forall a a' C,
      head_red a a' -> iscontext C ->
      ctx_red (C a) (C a').

Equivalence with the previous definition red.

Lemma ctx_red_to_red:
  forall a a', ctx_red a a' -> red a a'.
Proof.
  assert (REC: forall a a', head_red a a' ->
               forall C, iscontext C ->
               red (C a) (C a')).
  { intros a a' HR; induction 1.
  - inversion HR; subst; constructor; auto.
  - apply red_app_1; auto.
  - apply red_app_2; auto.
  - apply red_cond_1; auto. }
  destruct 1. apply REC; auto.
Qed.

Lemma red_to_ctx_red:
  forall a a', red a a' -> ctx_red a a'.
Proof.
  induction 1.
- apply ctx_red_intro with (C := fun x => x).
  apply head_red_beta; auto.
  constructor.
- apply ctx_red_intro with (C := fun x => x).
  apply head_red_cond; auto.
  constructor.
- destruct IHred. apply ctx_red_intro with (C := fun x => App (C x) a2); auto using iscontext.
- destruct IHred. apply ctx_red_intro with (C := fun x => App v (C x)); auto using iscontext.
- destruct IHred. apply ctx_red_intro with (C := fun x => Cond (C x) ifso ifnot); auto using iscontext.
Qed.

The natural semantics.

Inductive eval: term -> term -> Prop :=
  | eval_abs: forall x a,
      eval (Abs x a) (Abs x a)
  | eval_app: forall a1 a2 x a v2 v,
      eval a1 (Abs x a) -> eval a2 v2 -> eval (subst a x v2) v ->
      eval (App a1 a2) v
  | eval_const: forall b,
      eval (Const b) (Const b)
  | eval_cond: forall a ifso ifnot b v,
      eval a (Const b) -> eval (if b then ifso else ifnot) v ->
      eval (Cond a ifso ifnot) v.

Lemma eval_isvalue:
  forall a v, eval a v -> isvalue v.
Proof.
  induction 1; auto using isvalue.
Qed.

Lemma isvalue_eval:
  forall v, isvalue v -> eval v v.
Proof.
  destruct 1; eauto using eval.
Qed.

Equivalence between natural semantics eval a v and reduction semantics (there exists a sequence of reductions from term a to value v).

Lemma eval_reds:
  forall a v, eval a v -> star red a v.
Proof.
  induction 1.
- apply star_refl.
- apply star_trans with (App (Abs x a) a2).
  revert IHeval1. generalize a1, (Abs x a). induction 1; eauto using star, red_app_1.
  apply star_trans with (App (Abs x a) v2).
  revert IHeval2. generalize a2, v2. induction 1; eauto using star, red_app_2, isvalue.
  eapply star_step. apply red_beta. eapply eval_isvalue; eauto.
  apply IHeval3.
- apply star_refl.
- apply star_trans with (Cond (Const b) ifso ifnot).
  revert IHeval1. generalize a, (Const b). induction 1; eauto using star, red_cond_1.
  eapply star_step. apply red_cond.
  apply IHeval2.
Qed.

Lemma red_eval_eval:
  forall a1 a2, red a1 a2 -> forall v, eval a2 v -> eval a1 v.
Proof.
  induction 1; intros v' E.
- eauto using eval, isvalue_eval.
- eauto using eval.
- inversion E; subst; eauto using eval.
- inversion E; subst; eauto using eval, isvalue_eval.
- inversion E; subst; eauto using eval.
Qed.

Lemma reds_eval:
  forall a v, star red a v -> isvalue v -> eval a v.
Proof.
  induction 1; intros.
- apply isvalue_eval; auto.
- apply red_eval_eval with b; auto.
Qed.

7.2. Simple types


The type algebra.

Inductive type: Type :=
  | Bool (* the type of Booleans *)
  | Fun (t1: type) (t2: type). (* the type of functions from t1 to t2 *)

Notation " t1 --> t2 " := (Fun t1 t2) (right associativity, at level 55).

Typing contexts associate a type to each free variable.

Definition context := list (string * type).

Fixpoint lookup {A: Type} (x: string) (l: list (string * A)) : option A :=
  match l with
  | nil => None
  | (y, a) :: l => if string_dec x y then Some a else lookup x l
  end.

The typing rules.

Reserved Notation "E '⊢' a '∈' t" (at level 40).

Inductive has_type : context -> term -> type -> Prop :=
  | T_Var: forall E x t,
      lookup x E = Some t ->
      E ⊢ Var x ∈ t
  | T_Abs : forall E x a t t',
      ((x, t) :: E) ⊢ a ∈ t' ->
      E ⊢ Abs x a ∈ Fun t t'
  | T_App : forall E a1 a2 t t',
      E ⊢ a1 ∈ Fun t t' -> E ⊢ a2 ∈ t ->
      E ⊢ App a1 a2 ∈ t'
  | T_Const : forall E b,
      E ⊢ Const b ∈ Bool
  | T_Cond : forall E a ifso ifnot t,
      E ⊢ a ∈ Bool -> E ⊢ ifso ∈ t -> E ⊢ ifnot ∈ t ->
      E ⊢ Cond a ifso ifnot ∈ t

where "E '⊢' a '∈' t" := (has_type E a t).

The main properties of the typing judgment. First, the weakening property.

Lemma weakening:
  forall E a t,
  E ⊢ a ∈ t ->
  forall E',
  (forall x tx, lookup x E = Some tx -> lookup x E' = Some tx) ->
  E' ⊢ a ∈ t.
Proof.
  induction 1; intros E' W; eauto using has_type.
- (* Abs *)
  apply T_Abs. apply IHhas_type.
  cbn; intros. destruct (string_dec x0 x); auto.
Qed.

Weakening is stated in an unusual manner. Usually, it is stated with a syntactic concatenation of contexts: if E ⊢ a ∈ t, then E' ++ E ⊢ a ∈ t. However, this statement is false if E' can bound variables that are already bound in E. On paper, we implicitly assume that a context never binds the same variable twice, a constraint that can always be satisfied by renaming some variables. In our Coq development, we have no renaming nor constraints over contexts. Instead, we use two arbitrary contexts E and E', connected by the hypothesis "any variable that is given a type by E is given the same type in E'".

The next property is stability of typing under substitution. It uses the same trick to connect Moreover, the lemma requires that c is typed in the empty environment, guaranteeing that c is closed and that the substitution subst a x c avoids variable capture.

Lemma substitution_preserves_typing:
  forall E a t,
  E ⊢ a ∈ t ->
  forall x c t' E',
  nil ⊢ c ∈ t' ->
  lookup x E = Some t' ->
  (forall y ty, y <> x -> lookup y E = Some ty -> lookup y E' = Some ty) ->
  E' ⊢ subst a x c ∈ t.
Proof.
  induction 1; intros until E'; intros TYC TYX TYE; cbn.
- (* Var *)
  destruct (string_dec x0 x).
  + (* Var x *)
    replace t with t' by congruence.
    apply weakening with (E := nil); auto.
    cbn; intros; discriminate.
  + (* Var y, y <> x *)
    apply T_Var. apply TYE; auto.
- (* Abs *)
  destruct (string_dec x0 x).
  + (* Abs x a *)
    subst x0.
    apply T_Abs. apply weakening with (E := (x, t) :: E); auto.
    cbn; intros. destruct (string_dec x0 x); auto.
  + (* Abs y a, y <> x *)
    apply T_Abs. eapply IHhas_type; eauto.
    cbn. destruct (string_dec x0 x); congruence.
    cbn; intros. destruct (string_dec y x); auto.
- (* App *)
  apply T_App with t; eauto.
- (* Const *)
  apply T_Const.
- (* Cond *)
  apply T_Cond; eauto.
Qed.

Finally, here is the "canonical forms" lemma, showing that the type of a closed value determines its shape.

Lemma canonical_forms:
  forall v t,
  nil ⊢ v ∈ t -> isvalue v ->
  match t with
  | Bool => exists b, v = Const b
  | Fun t1 t2 => exists x a, v = Abs x a
  end.
Proof.
  intros v t TY VAL. inversion VAL; subst; inversion TY; subst.
- (* Fun type *)
  exists x, a; auto.
- (* Bool type *)
  exists b; auto.
Qed.

We can, then, prove the two crucial properties that connect typing with reductions: preservation and progress.

Theorem reduction_preserves_typing:
  forall a a',
  red a a' ->
  forall t,
  nil ⊢ a ∈ t -> nil ⊢ a' ∈ t.
Proof.
  induction 1; intros t TY.
- (* red_beta *)
  inversion TY; subst. inversion H3; subst.
  eapply substitution_preserves_typing; eauto.
  cbn. destruct (string_dec x x); congruence.
  cbn; intros. destruct (string_dec y x); congruence.
- (* red_cond *)
  inversion TY; subst.
  destruct b; auto.
- (* red_app_1 *)
  inversion TY; subst. apply T_App with t0; eauto.
- (* red_app_2 *)
  inversion TY; subst. apply T_App with t0; eauto.
- (* red_cond_1 *)
  inversion TY; subst. apply T_Cond; eauto.
Qed.

Theorem progress:
  forall a t,
  nil ⊢ a ∈ t -> isvalue a \/ exists a', red a a'.
Proof.
  intros a t TY; dependent induction TY.
- (* Abs x a *)
  left; apply V_Abs.
- (* App a1 a2 *)
  destruct IHTY1 as [ISVAL1 | (a1' & RED1)]; auto.
  + destruct IHTY2 as [ISVAL2 | (a2' & RED2)]; auto.
    * (* a1 et a2 sont des valeurs *)
      destruct (canonical_forms a1 (Fun t t')) as (x & a & E); auto.
      subst a1. right; exists (subst a x a2). apply red_beta; auto.
    * (* a1 est une valeur, a2 se réduit *)
      right; exists (App a1 a2'). apply red_app_2; auto.
  + (* a1 se réduit *)
    right; exists (App a1' a2). apply red_app_1; auto.
- (* Const b *)
  left; apply V_Const.
- (* Cond a ifso ifnot *)
  destruct IHTY1 as [ISVAL1 | (a' & RED1)]; auto.
  + (* a est une valeur *)
    destruct (canonical_forms a Bool) as (b & E); auto.
    subst a. right; exists (if b then ifso else ifnot). apply red_cond.
  + (* a se réduit *)
    right; exists (Cond a' ifso ifnot). apply red_cond_1; auto.
Qed.

Type soundness follows: a well-typed closed term does not go wrong.

Definition goes_wrong (a: term) : Prop :=
  exists a', star red a a' /\ irred red a' /\ ~isvalue a'.

Theorem well_typed_programs_do_not_go_wrong:
  forall a t,
  nil ⊢ a ∈ t -> ~ goes_wrong a.
Proof.
  intros a t TY (a' & REDS & IRRED & NOTVAL).
  assert (TY': nil ⊢ a' ∈ t).
  { clear IRRED NOTVAL. revert a a' REDS TY.
    induction 1; eauto using reduction_preserves_typing. }
  destruct (progress a' t TY') as [ISVAL | (a'' & RED)].
  - apply NOTVAL. auto.
  - apply IRRED with a''. auto.
Qed.

A more positive presentation of the type soundness result. We define coinductively the predicate safe a, meaning "a executes without going wrong". It covers both the case where the reduction of a terminates on a value, and the case where the reduction of a diverges.

CoInductive safe: term -> Prop :=
  | safe_value: forall v,
      isvalue v ->
      safe v
  | safe_red: forall a a',
      red a a' -> safe a' ->
      safe a.

Theorem well_typed_programs_are_safe:
  forall a t,
  nil ⊢ a ∈ t -> safe a.
Proof.
  cofix CIH; intros.
  destruct (progress a t H) as [ISVAL | (a' & RED)].
- apply safe_value; auto.
- apply safe_red with a'; auto.
  apply CIH with t. apply reduction_preserves_typing with a; auto.
Qed.

Exercise (2 or 3 stars)

Extend the type system with one or several of the features mentioned in the lecture: Peano integers, products, sums, fixed points. Update the proof of type soundness accordingly.

Exercise (3 stars)

In the definition of the type algebra, replace Inductive type ... by CoInductive type .... This makes it possible to work with infinite type expressions such as Bool --> Bool --> ... --> Bool --> ....

Remark type_Y: forall t,
  let D := Abs "x" (App (Var "f") (App (Var "x") (Var "x"))) in
  let Y := Abs "f" (App D D) in
  nil ⊢ Y ∈ ((t --> t) --> t).
Proof.
  intros t D Y.
  (* FILL IN HERE *)
Abort.

Exercise (3 stars)

Write a type-checker for our type system with simple types. It's a function context -> term -> option type that checks whether a term is well-typed in a given context. If yes, the type of the term is returned; if not, None is returned. Prove that this type-checker is sound and complete with respect to the typing rules.

Fixpoint typecheck (E: context) (a: term) : option type :=
None.

Lemma typecheck_sound:
  forall E a t, typecheck E a = Some t -> has_type E a t.
Proof.
  intros E a; revert a E; induction a; cbn; intros E t T.
  (* FILL IN HERE *)
Abort.

Lemma typecheck_complete:
  forall E a t, has_type E a t -> typecheck E a = Some t.
Proof.
  induction 1; cbn.
  (* FILL IN HERE *)
Abort.

7.3. Subtyping


Module Subtyping.

We extend the type algebra with Top, the universal type of all values.

Inductive type: Type :=
  | Top (* universal type *)
  | Bool (* type of Booleans *)
  | Fun (t1: type) (t2: type). (* type of functions from t1 to t2 *)

Reserved Notation "t '<:' s" (at level 40).

The subtyping relation. Intuitively, t is subtype of s if every value of type t can be used with type s.

Inductive subtype: type -> type -> Prop :=
  | subtype_top: forall t,
      t <: Top
  | subtype_bool:
      Bool <: Bool
  | subtype_fun: forall s1 t1 s2 t2,
      s2 <: s1 -> t1 <: t2 ->
      Fun s1 t1 <: Fun s2 t2

where "t '<:' s" := (subtype t s).

Every type is subtype of itself.

Lemma subtype_refl:
  forall t, t <: t.
Proof.
  induction t; auto using subtype.
Qed.

The subtyping relation is transitive.

Lemma subtype_trans:
  forall t1 t2 t3, t1 <: t2 -> t2 <: t3 -> t1 <: t3.
Proof.
  intros t1 t2; revert t2 t1.
  induction t2; intros t1 t3 S1 S2;
  inversion S1; inversion S2; subst; eauto using subtype.
Qed.

We extend the type system with a subsumption rule T_Sub that allows us to use a term with a super-type of its type.

Definition context := list (string * type).

Inductive has_type : context -> term -> type -> Prop :=
  | T_Var: forall E x t,
      lookup x E = Some t ->
      E ⊢ Var x ∈ t
  | T_Abs : forall E x a t t',
      ((x, t) :: E) ⊢ a ∈ t' ->
      E ⊢ Abs x a ∈ Fun t t'
  | T_App : forall E a1 a2 t t',
      E ⊢ a1 ∈ Fun t t' -> E ⊢ a2 ∈ t ->
      E ⊢ App a1 a2 ∈ t'
  | T_Const : forall E b,
      E ⊢ Const b ∈ Bool
  | T_Cond : forall E a ifso ifnot t,
      E ⊢ a ∈ Bool -> E ⊢ ifso ∈ t -> E ⊢ ifnot ∈ t ->
      E ⊢ Cond a ifso ifnot ∈ t
  | T_Sub: forall E a s t, (* <-- new! *)
      E ⊢ a ∈ s -> s <: t ->
      E ⊢ a ∈ t

where "E '⊢' a '∈' t" := (has_type E a t).

Exercise (3 stars)

Prove type soundness for this type system with subtyping. The proof in section 7.2 can be reused with very few changes. However, it is necessary to use the following inversion lemmas.

Lemma T_Abs_inv:
  forall E x a t,
  E ⊢ Abs x a ∈ t -> exists t1 t2, ((x, t1) :: E) ⊢ a ∈ t2 /\ Fun t1 t2 <: t.
Proof.
  intros until t; intros TY; dependent induction TY.
- exists t, t'; auto using subtype_refl.
- edestruct IHTY as (t1 & t2 & P & Q); eauto.
  exists t1, t2; split. auto. apply subtype_trans with s; auto.
Qed.

Lemma T_App_inv:
  forall E a1 a2 t,
  E ⊢ App a1 a2 ∈ t -> exists t1 t2, E ⊢ a1 ∈ Fun t1 t2 /\ E ⊢ a2 ∈ t1 /\ t2 <: t.
Proof.
  intros until t; intros TY; dependent induction TY.
- exists t, t'; auto using subtype_refl.
- edestruct IHTY as (t1 & t2 & P & Q & R); eauto.
  exists t1, t2; split. auto. split. auto. apply subtype_trans with s; auto.
Qed.

Lemma T_Cond_inv:
  forall E a ifso ifnot t,
  E ⊢ Cond a ifso ifnot ∈ t -> exists t', E ⊢ a ∈ Bool /\ E ⊢ ifso ∈ t' /\ E ⊢ ifnot ∈ t' /\ t' <: t.
Proof.
  intros until t; intros TY; dependent induction TY.
- exists t; auto using subtype_refl.
- edestruct IHTY as (t' & P & Q & R & S); eauto.
  exists t'; intuition auto. apply subtype_trans with s; auto.
Qed.

Theorem well_typed_programs_are_safe:
  forall a t,
  nil ⊢ a ∈ t -> safe a.
Proof.
  (* FILL IN HERE *)
Abort.

End Subtyping.

7.4. Intrinsically-typed terms


From Coq Require Import FunctionalExtensionality.

Module Intrinsic.

We now develop an abstract syntax for FUN where terms are indexed by their types and the contexts in which they are typed.

A context lists the free variables that can occur in the term, along with their types. We use a positional notation (de Bruijn indices) for variables. Consequently, the context is just a list of types: t1 :: ... :: tN :: nil is the context that assigns type ti to the variable having index i, for i ranging from 1 to N.

Definition context := list type.

var E t is the type of variables that can be used in context E with type t.

Inductive var: context -> type -> Type :=
  | V1: forall {E: context} {t: type}, var (t :: E) t
  | VS: forall {E: context} {t t': type}, var E t' -> var (t :: E) t'.

Examples of variables.

Definition V2 {E: context} {t1 t2: type}: var (t1 :: t2 :: E) t2 := VS V1.
Definition V3 {E: context} {t1 t2 t3: type}: var (t1 :: t2 :: t3 :: E) t3 := VS V2.

term E t is the type of terms having type t in context E.

Inductive term: context -> type -> Type :=
  | Var: forall {E: context} {t: type},
         var E t ->
         term E t
  | Abs: forall {E: context} {t t': type},
         term (t :: E) t' ->
         term E (Fun t t')
  | App: forall {E: context} {t t': type},
         term E (Fun t t') -> term E t ->
         term E t'
  | Const: forall {E: context} (b: bool),
         term E Bool
  | Cond: forall {E: context} {t: type},
         term E Bool -> term E t -> term E t ->
         term E t.

Examples of terms.

The term fun b => if b then false else true.
Definition t_negation : term nil (Bool --> Bool) :=
  Abs (Cond (Var V1) (Const false) (Const true)).

The term fun f => fun g => fun x => g (f x).
Definition t_compose (t1 t2 t3: type) :
               term nil ((t1 --> t2) --> (t2 --> t3) --> (t1 --> t3)) :=
  Abs (Abs (Abs (App (Var V2) (App (Var V3) (Var V1))))).

An ill-typed term that, consequently, cannot be expressed.
Fail Definition t_error : term nil Bool :=
  Cond (Abs (Var V1)) (Const false) (Const true).

We interpret a FUN type expression by a Coq type. It's the type of Coq values that match this FUN type.

Fixpoint dtype (t: type) : Type :=
  match t with
  | Bool => bool
  | Fun t1 t2 => dtype t1 -> dtype t2
  end.

Likewise, we interpret a typing context by a Coq type. It is the type of evaluation environments corresponding to this context: an heterogeneous list of the values associated to the variables.

Fixpoint dcontext (E: context) : Type :=
  match E with
  | nil => unit
  | t :: E => dtype t * dcontext E
  end.

The denotational semantics of a variable. It is the value associated to the variable in the evaluation environment.

Fixpoint dvar {E: context} {t: type} (v: var E t): dcontext E -> dtype t :=
  match v with
  | V1 => (fun e => fst e)
  | VS v => (fun e => dvar v (snd e))
  end.

The denotational semantics of a term. It is a function from evaluation environments, dcontext E, to Coq values matching the type of the expression, dtype t.

Fixpoint dterm {E: context} {t: type} (a: term E t) : dcontext E -> dtype t :=
  match a with
  | Var v => dvar v
  | Abs a => (fun e => (fun v => dterm a (v, e)))
  | App a1 a2 => (fun e => dterm a1 e (dterm a2 e))
  | Const b => (fun e => b)
  | Cond a ifso ifnot => (fun e => if dterm a e then dterm ifso e else dterm ifnot e)
  end.

The semantics of a beta-redex App (Abs a) b is just that of the binding let 1 = b in a: we evaluate a after binding the variable of index 1 to the value of b.

Lemma dbeta: forall (E: context) (t t': type) (a: term (t :: E) t') (b: term E t),
  forall e, dterm (App (Abs a) b) e = dterm a (dterm b e, e).
Proof.
  reflexivity.
Qed.

In preparation for a reduction semantics, we now build a substitution function over intrinsically-typed terms. The substitution of b for variable of index 1 in a has type 
   subst1 {t': type} {E: context} {t: type} (a: term (t' :: E) t) (b: term E t') : term E t
and satisfies the equation dterm (subst1 a b) e = dterm a (dterm b e, e).

Definiting the substitution function is difficult:

Lifting.

Fixpoint unlift_env (E': context) (t': type) (E: context) : dcontext (E' ++ t' :: E) -> dcontext (E' ++ E) :=
  match E' with
  | nil => fun e => snd e
  | t :: E' => fun e => (fst e, unlift_env E' t' E (snd e))
  end.

Definition lift_var (E': context) (t': type) {E: context} {t: type} (v: var (E' ++ E) t) :
           { w : var (E' ++ t' :: E) t
           | forall e, dvar w e = dvar v (unlift_env E' t' E e)}.
Proof.
  revert E' t' E t v. induction E' as [ | t0 E' ]; cbn.
- intros. exists (VS v). auto.
- intros. dependent destruction v.
  + exists V1. auto.
  + destruct (IHE' t' _ _ v) as (w & W). exists (VS w). intros; cbn. rewrite W; auto.
Defined.

Definition lift (E': context) (t': type) {E: context} {t: type} (a: term (E' ++ E) t) :
           { b : term (E' ++ t' :: E) t
           | forall e, dterm b e = dterm a (unlift_env E' t' E e) }.
Proof.
  dependent induction a.
- destruct (lift_var E' t' v) as (w & W). exists (Var w). auto.
- destruct (IHa (t::E') _ a) as (b & B); auto.
  exists (Abs b). intros. apply functional_extensionality; intros. cbn. rewrite B. auto.
- destruct (IHa1 E' _ a1) as (b1 & B1); auto.
  destruct (IHa2 E' _ a2) as (b2 & B2); auto.
  exists (App b1 b2). cbn; intros. rewrite B1, B2. auto.
- exists (Const b); auto.
- destruct (IHa1 E' _ a1) as (b1 & B1); auto.
  destruct (IHa2 E' _ a2) as (b2 & B2); auto.
  destruct (IHa3 E' _ a3) as (b3 & B3); auto.
  exists (Cond b1 b2 b3). intros; cbn. rewrite B1, B2, B3; auto.
Defined.

Definition lift1 (t': type) {E: context} {t: type} (a: term E t) :
           { b : term (t' :: E) t
           | forall e, dterm b e = dterm a (snd e) }.
Proof.
  apply lift with (E' := nil).
Defined.

Substitution.

Fixpoint proj_env (E': context) (E: context) : dcontext (E' ++ E) -> dcontext E :=
  match E' with
  | nil => fun e => e
  | t :: E' => fun e => proj_env E' E (snd e)
  end.

Fixpoint unsubst_env (E': context) (t': type) (E: context) : dcontext (E' ++ E) -> dtype t' -> dcontext (E' ++ t' :: E) :=
  match E' with
  | nil => fun e v => (v, e)
  | t :: E' => fun e v => (fst e, unsubst_env E' t' E (snd e) v)
  end.

Definition subst_var (E': context) (t': type) {E: context} {t: type} (v: var (E' ++ t' :: E) t) (b: term E t') :
           { c : term (E' ++ E) t
           | forall e, dterm c e = dvar v (unsubst_env E' t' E e (dterm b (proj_env E' E e))) }.
Proof.
  induction E' as [ | t0 E' ]; simpl.
- dependent destruction v; simpl.
  + exists b; auto.
  + exists (Var v); auto.
- dependent destruction v; simpl.
  + exists (Var V1); auto.
  + destruct (IHE' v) as (c & C). destruct (lift1 t0 c) as (c' & C'). exists c'.
    simpl; intros. rewrite C', C. auto.
Defined.

Definition subst (E': context) (t': type) {E: context} {t: type} (a: term (E' ++ t' :: E) t) (b: term E t') :
           { c : term (E' ++ E) t
           | forall e, dterm c e = dterm a (unsubst_env E' t' E e (dterm b (proj_env E' E e))) }.
Proof.
  dependent induction a.
- apply subst_var.
- edestruct (IHa (t :: E') t' E a) as (c & C); eauto.
  exists (Abs c). intros. apply functional_extensionality. intros v; simpl.
  rewrite C. simpl. eauto.
- edestruct (IHa1 E' t' E a1) as (c1 & C1); eauto.
  edestruct (IHa2 E' t' E a2) as (c2 & C2); eauto.
  exists (App c1 c2). simpl; intros. rewrite C1, C2. eauto.
- exists (Const b). simpl; auto.
- edestruct (IHa1 E' t' E a1) as (c1 & C1); eauto.
  edestruct (IHa2 E' t' E a2) as (c2 & C2); eauto.
  edestruct (IHa3 E' t' E a3) as (c3 & C3); eauto.
  exists (Cond c1 c2 c3). simpl; intros. rewrite C1, C2, C3. eauto.
Defined.

Definition subst1 {t': type} {E: context} {t: type} (a: term (t' :: E) t) (b: term E t') : term E t :=
  proj1_sig (subst nil t' a b).

Lemma dterm_subst1:
  forall {t': type} {E: context} {t: type} (a: term (t' :: E) t) (b: term E t') e,
  dterm (subst1 a b) e = dterm a (dterm b e, e).
Proof.
  intros. unfold subst1. destruct (subst nil t' a b) as (c & C). apply C.
Qed.

The reduction semantics.

Inductive isvalue: forall (E: context) (t: type), term E t -> Prop :=
  | V_Abs: forall E t1 t2 (a: term (t1 :: E) t2),
      isvalue E (Fun t1 t2) (Abs a)
  | V_Const: forall E b,
      isvalue E Bool (Const b).

Inductive red: forall E t, term E t -> term E t -> Prop :=
  | red_beta: forall E t1 t2 (a: term (t1 :: E) t2) (v: term E t1),
      isvalue E t1 v ->
      red E t2 (App (Abs a) v) (subst1 a v)
  | red_cond: forall E t (b: bool) (ifso ifnot: term E t),
      red E t (Cond (Const b) ifso ifnot) (if b then ifso else ifnot)
  | red_app_1: forall E t t' (a1 a1': term E (Fun t t')) (a2: term E t),
      red E (Fun t t') a1 a1' ->
      red E t' (App a1 a2) (App a1' a2)
  | red_app_2: forall E t t' (v: term E (Fun t t')) (a2 a2': term E t),
      isvalue E (Fun t t') v -> red E t a2 a2' ->
      red E t' (App v a2) (App v a2')
  | red_cond_1: forall E t (a a': term E Bool) (ifso ifnot: term E t),
      red E Bool a a' ->
      red E t (Cond a ifso ifnot) (Cond a' ifso ifnot).

Reductions are compatible with the denotational semantics.

Theorem red_denot:
  forall E t a1 a2, red E t a1 a2 -> forall e, dterm a1 e = dterm a2 e.
Proof.
  induction 1; simpl; intros.
- rewrite dterm_subst1; auto.
- destruct b; auto.
- rewrite IHred; auto.
- rewrite IHred; auto.
- rewrite IHred; auto.
Qed.

End Intrinsic.
Generated by coq2html