(**************************************************************************
* Proving functional programs through a deep embedding                    *
* Semantics of the embedded language                                      *
***************************************************************************)

Set Implicit Arguments.
Require Export DeepPrinter.
Require Import LibClosure.


(************************************************************)
(* ** Free variables of a pattern and of a term *)

(** [pat_vars p] returns a list that contains all the 
    variables bound by pattern [p]. This function is used 
    in the definition of capture-avoiding substitution. *)

Fixpoint pat_vars (p:pat) : list var :=
  match p with 
  | pat_var x => x :: nil
  | pat_con c ps => Flatten (List.map pat_vars ps)
  | pat_alias x p1 => x::(pat_vars p1)
  | _ => nil
  end.

(** [trm_vars t] returns a list that contains all the 
    variables occuring in the term [t]. This function is
    used only to defined what closed terms are. *)

Fixpoint trm_vars (t:trm) : list var :=
  match t with
  | trm_var x => x::nil
  | trm_app t1 t2 => trm_vars t1 ++ trm_vars t2
  | trm_try t1 t2 => trm_vars t1 ++ trm_vars t2
  | trm_con c ts => Flatten (List.map trm_vars ts)
  | trm_fix f p t1 t2 => 
      let vs := LibList.removes (pat_vars p) (trm_vars t1) in
       (LibList.remove f (vs ++ trm_vars t2))
  | _ => nil
  end.


(************************************************************)
(* ** Conversion from term to values *)

(** [val_of_trm t] returns [Some v] if the term [t] is
    equal to [trm_val v], and [None] otherwise. *)

Definition val_of_trm t :=
  match t with 
  | trm_val v => Some v
  | _ => None
  end.

(** [trm_to_val t] returns [Some v] if the term [t] 
    corresponds to the representation of a value [v]
    in the syntax of terms, and if [t] is not already a value
    of the form [trm_val v]. 
    It returns [None] otherwise. This function
    is used in the definition of the reduction rule that 
    turns terms into corresponding values when appropriate. *)

Definition trm_to_val (t:trm) : option val :=
  match t with
  | trm_con c ts => 
        LibOption.map_on (map_partial val_of_trm ts) 
                         (fun vs => val_con c vs)
  | trm_fix f p t1 t2 =>
     match trm_vars t with
     | nil => Some (val_fix f p t1 t2)
     | _ => None
     end
  | _ => None
  end.


(************************************************************)
(* ** Capture-avoiding substitution *)

(** [inst] is the type of a finite map from variables 
    to values. Such maps are used both to define the
    result of matching a value against a pattern and
    to define the substitution that follows. *)

Definition inst := LibEnv.env Var val.

(** [subst m t] returns the result of substituting in [t]
    free occurences of variable [xi] with the value [vi] 
    for each binding [(xi,vi)] from map [m]. Because values 
    are closed, substitution need not go through values.
    Substitution is used to implement beta-reduction. *)

Fixpoint subst (m:inst) (t:trm) : trm :=
  match t with
  | trm_var x => match m[x] with None => t | Some v => trm_val v end
  | trm_app t1 t2 => trm_app (subst m t1) (subst m t2)
  | trm_try t1 t2 => trm_try (subst m t1) (subst m t2)
  | trm_con c ts => trm_con c (List.map (subst m) ts)
  | trm_fix f p t1 t2 => 
     let m2 := m \rem (f::nil) in
     let m1 := m2 \rem (pat_vars p) in
     trm_fix f p (subst m1 t1) (subst m2 t2)
  | _ => t
  end.

(** [empty_subst] stands for the empty map. *)

Definition empty_subst : inst := LibEnv.empty.


(************************************************************)
(* ** Comparison of values *)

(** [val_cmp v1 v2] returns [true] if
    - values [v1] and [v2] are identical 
    - values [v1] and [v2] do not contain any closure.
    It returns [false] otherwise.
    This function is used to describe Caml's polymorphic 
    equality, whose behaviour is undefined on closure.
    (Actually it is defined, in terms of physical equality,
     but this property cannot be expressed in a purely 
     functional programming model. *)

Fixpoint val_cmp (v1 v2 : val) {struct v1} : bool :=
  match v1, v2 with
  | val_int n1, val_int n2 => (n1 == n2)
  | val_con c1 vs1, val_con c2 vs2 =>
     let aux := fix aux (ws1 ws2 : list val) {struct ws1} :=
        match ws1,ws2 with
        | nil,nil => true
        | w1::ws1,w2::ws2 => val_cmp w1 w2 && aux ws1 ws2 
        | _,_ => false
        end
       in
     (c1 == c2) && (aux vs1 vs2)    
  | _,_ => false
  end.


(************************************************************)
(* ** Pattern matching *)

(** [matching p v] returns [Some m] if value [v] matches
    pattern [p]. The map [m] returned describes the 
    instantiations given to pattern variables bound in [p].
    The function returns [None] if the value [v] does not 
    match the pattern [p]. *)

Fixpoint matching (p:pat) (v:val) {struct p} : option inst :=
  match p, v with
  | pat_wildcard, _ => Some empty_subst
  | pat_var x, _ => Some (x ~> v)
  | pat_alias x p1, v1 =>
     LibOption.map_on (matching p1 v1) (fun m1 => 
       m1 \U (x ~> v1))
  | pat_int n1, val_int n2 => 
     if (n1 == n2) then Some empty_subst else None
  | pat_con c1 ps1, val_con c2 vs2 =>
     let mat := fix mat (qs1 : list pat) (ws2 : list val) {struct qs1} :=
       match qs1,ws2 with
       | nil, nil => Some empty_subst
       | q1::qs1', w2::ws2' => 
           LibOption.apply_on (matching q1 w2) (fun m =>
              LibOption.map_on (mat qs1' ws2') (fun ms =>
                 m \U ms))
       | _, _ => None
       end in
     if c1 == c2 then mat ps1 vs2 else None
  | _,_ => None
  end.
 

(************************************************************)
(* ** Semantics: small-step *)

Section Reduction.
Implicit Types t : trm.
Implicit Types v e : val.
Implicit Types n : int.

(** Predicate [t1 --> t2] indicates that term [t1] reduces
    in one step into term [t2]. 
    The reduction rules fall in 6 categories:
    - beta-reduction
    - transformation of terms into corresponding values
    - reduction under an evaluation context
    - propagation of exceptions 
    - behaviour of exception handlers
    - reduction rules for primitive operations.  *)

Reserved Notation "t1 --> t2" (at level 68).

Inductive red : trm -> trm -> Prop :=

  (* beta-reduction *)
  | red_beta : forall p t1 t2 v,
     (val_fix novar p t1 t2) ' v --> 
        match matching p v with 
        | None => t2 ' v
        | Some m => subst m t1
        end

  (* beta-reduction for recursive functions *)
  | red_beta_fix : forall f p t1 t2 v F,
     f != novar ->
     F = val_fix f p t1 t2 ->
     F ' v --> match matching p v with 
              | None => (subst (f ~> F) t2) ' v
              | Some m => subst (m \U (f ~> F)) t1
              end

  (* term-to-value-reduction *)
  | red_val : forall v t,
     trm_to_val t = Some v -> 
     t --> v

  (* reduction contexts *)
  | red_app_2 : forall t1 t2 t2r,
     t2 --> t2r ->
     (t1 ' t2) --> (t1 ' t2r)
  | red_app_1 : forall t1 t1r v2,
     t1 --> t1r ->
     (t1 ' v2) --> (t1r ' v2)
  | red_try_1 : forall t1 t1r t2,
     t1 --> t1r ->
     ('try t1 'catch t2) --> ('try t1r 'catch t2)
  | red_con : forall c vs ts t1 t1r,
     t1 --> t1r ->
     (c ## vs++t1++ts) --> (c ## vs++t1r++ts)
  
  (* exception contexts *)
  | red_exn_app_2 : forall e2 t1,
     (t1 ' (exn e2)) --> (exn e2)
  | red_exn_app_1 : forall v2 e1,
     ((exn e1) ' v2) --> (exn e1)
  | red_exn_con : forall c e1 vs ts,
     (c ## vs++(exn e1)++ts) --> (exn e1)

  (* exception handling *)
  | red_try_exn : forall e1 t2,
     ('try (exn e1) 'catch t2) --> (t2 ' e1)
  | red_try_val : forall v1 t2,
     ('try v1 'catch t2) --> v1

  (* primitive operations *)
  | red_throw : forall e1,
     ('throw e1) --> (exn e1)
  | red_add : forall n1 n2,
     ((\ val_builtin builtin_add) ' \#(_Int n1, _Int n2))
     --> _Int (n1 + n2)
  | red_sub : forall n1 n2,
     ((\ val_builtin builtin_sub) ' \#(_Int n1, _Int n2))
     --> _Int (n1 - n2)
  | red_mul : forall n1 n2,
     ((\ val_builtin builtin_mul) ' \#(_Int n1, _Int n2))
     --> _Int (n1 * n2)
  | red_div : forall n1 n2,
     ((\ val_builtin builtin_div) ' \#(_Int n1, _Int n2))
     --> if (n2 == 0) then Exn con_div_by_zero
                      else _Int (exact_div n1 n2)
  | red_equ : forall v1 v2,
     ((\ val_builtin builtin_equ) ' \#(v1, v2))
     --> _Bool (val_cmp v1 v2)
  | red_leq : forall n1 n2,
     ((\ val_builtin builtin_leq) ' \#(_Int n1, _Int n2))
     --> _Bool (n1 <= n2)%I

where "t1 --> t2" := (red t1 t2).

End Reduction.
  
Notation "t1 --> t2" := (red t1 t2) (at level 68).



(************************************************************)
(* ** Reduction is deterministic *)

Section Deterministic.

Lemma value_no_red : forall v t,
  \v --> t -> False.
Proof. introv H. inverts H. discriminate. Qed.

Lemma exn_no_red : forall v t,
  exn v --> t -> False.
Proof. introv H. inverts H. discriminate. Qed.

Definition not_value t := 
  forall v, t = \v -> False.

Lemma not_value_red : forall t tr,
  t --> tr -> not_value t.
Proof. intros_all. subst. apply* value_no_red. Qed.

Lemma not_value_exn : forall v,
  not_value (exn v).
Proof. intros_all. invert H. Qed.

Hint Resolve not_value_red not_value_exn.

Lemma con_eq_inv : forall vs1 t1 ts1 vs2 t2 ts2,
    (map trm_val vs1)++t1::ts1 
  = (map trm_val vs2)++t2::ts2 ->
  not_value t1 -> not_value t2 ->
  vs1 = vs2 /\ t1 = t2 /\ ts1 = ts2.
Proof.
  introv Eq NV1 NV2. gen vs2.
  induction vs1; destruct vs2;
   calc_map; calc_app; intros H; inverts H.
  auto.
  false. rapply* NV1.
  false. rapply* NV2.
  destructs~ 3 (@IHvs1 vs2). splits; congruence.
Qed.

Implicit Arguments con_eq_inv [vs1 t1 ts1 vs2 t2 ts2].

Lemma val_of_trm_inv : forall t v,
  val_of_trm t = Some v -> t = trm_val v.
Proof.
  destruct t; simpl; intros; tryfalse.
  inverts~ H.
Qed.
Implicit Arguments val_of_trm_inv [t v].

Lemma val_of_trm_inv_not_value : forall t v,
  val_of_trm t = Some v -> not_value t -> False. 
Proof. introv Eq Nv. eapply Nv. apply* val_of_trm_inv. Qed.

Lemma constr_not_value_inv : forall vs ts c t1 v,
  trm_to_val (c##vs++t1++ts) = Some v ->
  not_value t1 ->
  False.
Proof.
  introv E0 Nv. lets ws E1 E2: (map_on_inv E0).
  lets F: (map_partial_inv E1). clears v E1. gen ws.
  induction vs; calc_map; calc_app; introv F; inverts F.
    apply* val_of_trm_inv_not_value.
    apply* IHvs. 
Qed.

Lemma constr_red_no_red : forall vs ts c t1 t1r v,
  t1 --> t1r ->
  trm_to_val (c##vs++t1++ts) = Some v ->
  False.
Proof. intros. apply* constr_not_value_inv. Qed.

Lemma constr_exn_no_red : forall vs ts c e1 v,
  trm_to_val (c##vs++(exn e1)++ts) = Some v ->
  False.
Proof. intros. apply* constr_not_value_inv. Qed.

Ltac deter_discr_base := 
  solve [ discriminate |
    match goal with 
    | H: \?v --> ?t |- _ => false (value_no_red H) 
    | H: exn ?v --> ?t |- _ => false (exn_no_red H) 
    end ].

Ltac deter_discr := 
  try solve [ deter_discr_base
            | simpls; deter_discr_base ].

Lemma red_deterministic : forall t tr1 tr2,
  t --> tr1 -> t --> tr2 -> tr1 = tr2.
Proof.
  introv Red1. gen tr2. induction Red1; 
   introv Red2; inversions Red2; deter_discr;
   try solve [ reflexivity | congruence | f_equal~ ].
   inversions~ H3.
   false~.
   inversions~ H2.
   false~.
   inversions~ H5.
   false. apply* constr_red_no_red.
   false. apply* constr_exn_no_red. 
   false. apply* constr_red_no_red. 
   destructs 3 (con_eq_inv H1); eauto. subst.
    rewrite~ (IHRed1 _ H2). 
   false.
    destructs 3 (con_eq_inv H1); eauto. subst.
    apply (exn_no_red Red1).
   false. apply* constr_exn_no_red.
   false.
    destructs 3 (con_eq_inv H1); eauto. subst.
    apply (exn_no_red H2).
   gen vs. induction vs0; destruct vs; simpl;
    calc_map; calc_app; intros H; inversions~ H.
    apply* IHvs0.
Qed.

End Deterministic.


(************************************************************)
(* ** Big-step semantics *)

(** [t1 -->* t2] indicates that term [t1] reduces in zero,
    one, or more steps into the term [t2]. It is defined
    as the reflexive-transitive closure of the one-step
    reduction [-->]. *)

Notation "t1 -->* t2" := (star red t1 t2) (at level 68).

(* The above definition is equivalent to:

  Inductive reds : trm -> trm -> Prop :=
  | reds_refl : forall t,
      t -->* t
  | reds_step : forall t2 t1 t3,
      t1 --> t2 -> 
      t2 -->* t3 -> 
      t1 -->* t3
*)

Section Reds.

Hint Constructors red star.

Lemma reds_refl : forall t,
  t -->* t.
Proof. auto. Qed.

Lemma reds_step : forall t2 t1 t3,
  (t1 --> t2) -> (t2 -->* t3) -> (t1 -->* t3).
Proof. auto*. Qed. 

Lemma reds_red : forall t1 t2,
  (t1 --> t2) -> (t1 -->* t2).
Proof. auto*. Qed.

Hint Resolve reds_red.

Lemma reds_trans : forall t2 t1 t3,
  (t1 -->* t2) -> (t2 -->* t3) -> (t1 -->* t3).
Proof. introv R1 R2. induction* R1. Qed.

End Reds.

(** [red_not t] holds if [t] does not reduce. *)

Definition red_not t := 
  forall t', (t --> t') -> False.

Lemma red_not_val : forall v, red_not (\v).
Proof. intros_all. inversions H. false. Qed.

Lemma red_not_exn : forall v, red_not (exn v).
Proof. intros_all. inversions H. false. Qed.

Hint Resolve red_not_val red_not_exn.

(** The following lemma is used to prove that the language
    is deterministic with respect to big-step evaluation,
    for terminating programs. *)

Lemma reds_deterministic : forall t tf t',
  (t -->* tf) -> (red_not tf) -> (t --> t') -> (t' -->* tf).
Proof. 
  introv RedsT EndTf. gen t'. induction RedsT; introv Redt.
  false. apply* EndTf.
  rewrite* <- (red_deterministic H Redt). 
Qed.


(************************************************************)
(* ** Definition of non-termination *)

(** [reduces t] holds if [t] can take a reduction step *)

Definition reduces t :=
  exists t', (t --> t').

(** [diverges t] holds if [t] diverges, that is, if for
    any finite reduction sequence starting on [t] and
    ending on a term [tr], the term [tr] is reducible. *)

Definition diverges t :=
  forall tr, (t -->* tr) -> reduces tr.

Section Diverges.
Hint Resolve reds_red reds_refl reds_step.

(** Helper lemma to show that a term is reducible *)

Lemma reduces_intro : forall t t',
  (t --> t') -> reduces t.
Proof. unfolds* reduces. Qed.

Hint Resolve reduces_intro.

(** If [t] diverges, then [t] reduces to some [t']
    that also diverges. *)

Lemma diverges_inv : forall t,
  diverges t -> exists t', (t --> t') /\ diverges t'.
Proof.
  introv Div. destruct~ (Div t) as [t' Red1].
  exists t'. split~. introv Reds. destruct* (Div tr).
Qed.

(** If [t] reduces to [t'], then [t] diverges if
    and only if [t'] diverges. *)

Lemma diverges_red_back : forall t t',
  diverges t -> (t --> t') -> diverges t'.
Proof. introv Div Red Reds. apply* (Div tr). Qed.

Lemma diverges_red : forall t t',
  diverges t' -> (t --> t') -> diverges t.
Proof.
  introv Div Red Reds. destruct Reds.
    exists* t'.
    apply Div. rewrite* (red_deterministic Red H).
Qed.

End Diverges.


(************************************************************)
(* ** Definition of behaviours *)

(** We define four behaviours:
    - [ >> _A st P ] for terms that return a value,
    - [ >! _A st P ] for terms throwing exceptions,
    - [ >oo ] for terms that diverge,
    - [ >? ] for terms whose behaviour is unspecified. *)

Inductive behaviour : Type :=
  | Returns : forall (A:Type), 
      (code A) -> (A -> Prop) -> behaviour
  | Throws : con -> behaviour 
  | Diverges : behaviour
  | Unspecified : behaviour.

Notation ">> _A 'st' P" := 
  (Returns _A P) (at level 9, P at level 71).
Notation ">! c" := 
  (Throws c) (at level 9, C at level 71).
Notation ">oo" := 
  (Diverges) (at level 9).
Notation ">?" := 
  (Unspecified) (at level 9). 

Notation ">> '[' x ':' _A ']' 'st' P" := 
  (Returns _A (fun x => P)) 
  (at level 9, P at level 71, x at level 0, only parsing). 


(************************************************************)
(* ** Relation between terms and their behaviour *)

(** The predicate [t >- B] indicates that the term [t]
    admits the behaviour [B]. It is defined using four
    introduction rules, one for each kind of behaviour. *)

Inductive behave : behaviour -> trm -> Prop :=
  | behave_returns : forall A V (_A:code A) (P:A->Prop) t,
      t -->* (_A V) -> P V -> behave (Returns _A P) t
  | behave_throws : forall C t,
      t -->* Exn C -> behave (Throws C) t
  | behave_diverges : forall t, 
      diverges t -> behave Diverges t
  | behave_unspecified : forall t, 
      behave Unspecified t.

Notation ">- B" := (behave B) 
  (at level 10).
Notation "t >- B" := 
  (behave B t) (at level 68, B at level 40). 

(** Notations are:
    - [ t >> _A st P ] if [t] returns a value satisfying [P]
      ("such that P"), encoded through encoder [_A],
    - [ t >! _A st P ] if [t] throws a value satisfying [P]
      ("such that P"), encoded through encoder [_A],
    - [ t >oo ] if [t] diverges,
    - [ t >? ] if [t] is unspecified. *)

Notation "t >> '[' x ':' _A ']' 'st' P" := 
  (behave (>> _A st (fun x => P)) t) 
  (at level 6, P at level 71, x at level 0, only parsing).

Notation "t >> '[' x ',' y ':' _A ']' 'st' P" := 
  (behave (>> _A st (fun r => let (x,y) := r in P)) t) 
  (at level 6, P at level 71, x at level 0, y at level 0, 
   only parsing).
Notation "t >> '[' x ',' y ',' z ':' _A ']' 'st' P" := 
  (behave (>> _A st (fun r => let (x,yz) := r in
                              let (y,z) := yz in P)) t) 
  (at level 6, P at level 71, x at level 0, y at level 0,
   z at level 0, only parsing).

Notation "t >> _A 'st' P" := 
  (behave (>> _A st P) t) (at level 7, P at level 71).
Notation "t >! e" :=
   (behave (>! e) t) (at level 7).
Notation "t >oo" := 
  (behave >oo t) (at level 7).
Notation "t >?" := 
  (behave >? t) (at level 7). 

Lemma behave_returns_inv : forall A (_A:code A) (P:A->Prop) t,
  t >> _A st P -> exists X, t -->* (_A X) /\ P X.
Proof. intros. inverts* H. Qed.


(************************************************************)
(* ** Preservation of behaviour through reductions *)

Section BehaveReduction.
Implicit Types t : trm.
Hint Resolve reds_red.

(** Behaviours are preserved through one-step reduction.  
    More precisely, if [t1] reduces to [t2], then
    [t1] and [t2] admit the same behaviours. *)

Lemma behave_red : forall t2 t1 B, 
  (t2 >- B) -> (t1 --> t2) -> (t1 >- B).
Proof.
  introv Beh Red. destruct Beh.
  apply~ (behave_returns V). apply~ (@reds_trans t).
  apply~ behave_throws. apply~ (@reds_trans t).
  apply~ behave_diverges. apply* diverges_red.
  apply~ behave_unspecified.
Qed.

Lemma behave_red_back : forall t1 t2 B, 
  (t1 >- B) -> (t1 --> t2) -> (t2 >- B).
Proof. 
  introv Beh Red. destruct Beh.
  apply~ (behave_returns V). apply* reds_deterministic. 
  apply~ behave_throws. apply* reds_deterministic. 
  apply~ behave_diverges. apply* diverges_red_back.
  apply~ behave_unspecified.
Qed.

(** Behaviours are preserved through reduction sequences.
    This is just a generalization of the previous lemma. *)

Lemma behave_reds : forall t2 t1 B, 
  (t2 >- B) -> (t1 -->* t2) -> (t1 >- B).
Proof.
  introv Beh Red. induction~ Red. apply~ behave_red. 
Qed.

End BehaveReduction.


(************************************************************)
(* ** Partial order on behaviours *)

(** Predicate [B1 ==> B2] means that the behaviour [B1]
    is stronger than [B2] in the sense that any term [t]
    which admits behaviour [B1] also admits behaviour [B2]. 
    This relation is used in particular when weakening 
    specification of terms (tactic [xweaken]). *)

Definition bimpl B1 B2 := 
  forall t, (t >- B1) -> (t >- B2).

Notation "B1 ==> B2" := (bimpl B1 B2) (at level 68).

Section BImpl.
Hint Constructors behave.

(** The relation [==>] is reflexive, transitive, and 
    admits the unspecified behaviour ([>?]) as bottom. *)

Lemma bimpl_refl : forall B,
  B ==> B.
Proof. intros_all~. Qed.

Lemma bimpl_trans : forall B1 B2 B3,
  B1 ==> B2 -> B2 ==> B3 -> B1 ==> B3.
Proof. intros_all~. Qed.

Lemma bimpl_bottom : forall B,
  B ==> Unspecified.
Proof. intros_all~. Qed.

Lemma bimpl_elim : forall B1 t,
  t >- B1 -> forall B2, B1 ==> B2 -> t >- B2.
Proof. auto. Qed.

End BImpl.


(************************************************************)
(* ** Definition of reduction contexts *)

(** A context is represented as a Coq function from 
    term to terms. If [C] is a context, then [C t] is 
    the instantiation of this context onto the term [t]. *)

Definition ctx := trm -> trm.

(** A reduction context [C] is a context such that
    when a term [t] takes a reduction step the term
    [C t] takes a corresponding reduction step. *)

Definition red_ctx (C : ctx) :=
  forall t t', (t --> t') -> (C t --> C t').

Section RedCtx.
Implicit Types C : ctx.
Implicit Types t : trm.
Implicit Types v : val.

(** All reduction contexts can be built from atomic contexts
    (hole context, left and right branches of applications,
    argument of a try, subterm of a data-constructor)
    plus a context composition operator ([ctx_comp]). *)

Definition ctx_hole : ctx := 
  fun t => t.
Definition ctx_app_2 t1 : ctx := 
  fun t => t1 ' t.
Definition ctx_app_1 v2 : ctx := 
  fun t => t ' v2.
Definition ctx_try t2 : ctx := 
  fun t => 'try t 'catch t2.
Definition ctx_con_1_1 c : ctx := 
  fun t => trm_con c (t::nil).
Definition ctx_con_2_1 c (t2 : trm) : ctx := 
  fun t => trm_con c (t::t2::nil).
Definition ctx_con_2_2 c (v1 : val) : ctx := 
  fun t => trm_con c (\v1::t::nil).
Definition ctx_con_3_1 c (t2 t3 : trm) : ctx := 
  fun t => trm_con c (t::t2::t3::nil).
Definition ctx_con_3_2 c (v1 : val) (t3 : trm) : ctx := 
  fun t => trm_con c (\v1::t::t3::nil).
Definition ctx_con_3_3 c (v1 v2 : val) : ctx := 
  fun t => trm_con c (\v1::\v2::t::nil).

Definition ctx_comp C2 C1 : ctx :=
  fun t => C2 (C1 t).

Hint Constructors red.
Hint Resolve reds_refl reds_red.
Hint Unfold red_ctx.

(** The following lemmas simply establishes the fact that
    the atomic contexts defined above are indeed reduction
    contexts. Furthermore, the composition of two reduction
    contexts is also a reduction context. Tactic [prove_ctx]
    handles the application of these lemmas. *)

Lemma red_ctx_hole :
  red_ctx (ctx_hole).
Proof. unfolds~ ctx_hole. Qed.

Lemma red_ctx_app_2 : forall t1,
  red_ctx (ctx_app_2 t1).
Proof. unfolds~ ctx_app_2. Qed.

Lemma red_ctx_app_1 : forall v2,
  red_ctx (ctx_app_1 v2).
Proof. unfolds~ ctx_app_1. Qed.

Lemma red_ctx_try : forall t2,
  red_ctx (ctx_try t2).
Proof. unfolds~ ctx_try. Qed.

Section RedCtxCon.
Variables (c:con) (v1 v2 v3:val) (t1 t2 t3:trm).
Lemma red_ctx_con_1_1 :
  red_ctx (ctx_con_1_1 c).
Proof.
  introv H. lets K: (@red_con c nil nil _ _ H).
  calc_map in K. auto.
Qed.
Lemma red_ctx_con_2_1 :
  red_ctx (ctx_con_2_1 c t1).
Proof.
  introv H. lets K: (@red_con c nil (t1::nil) _ _ H).
  calc_map in K. auto.
Qed.
Lemma red_ctx_con_2_2 :
  red_ctx (ctx_con_2_2 c v1).
Proof.
  introv H. lets K: (@red_con c (v1::nil) nil _ _ H).
  calc_map in K. auto.
Qed.
Lemma red_ctx_con_3_1 :
  red_ctx (ctx_con_3_1 c t2 t3).
Proof.
  introv H. lets K: (@red_con c nil (t2::t3::nil) _ _ H).
  calc_map in K. auto.
Qed.
Lemma red_ctx_con_3_2 :
  red_ctx (ctx_con_3_2 c v1 t3).
Proof.
  introv H. lets K: (@red_con c (v1::nil) (t3::nil) _ _ H).
  calc_map in K. auto.
Qed.
Lemma red_ctx_con_3_3 :
  red_ctx (ctx_con_3_3 c v1 v2).
Proof.
  introv H. lets K: (@red_con c (v1::v2::nil) nil _ _ H).
  calc_map in K. auto.
Qed.
End RedCtxCon.

Lemma red_ctx_comp : forall C1 C2,
  red_ctx C1 -> 
  red_ctx C2 ->
  red_ctx (ctx_comp C2 C1).
Proof. unfolds~ ctx_comp. Qed.

End RedCtx.

Hint Resolve red_ctx_hole red_ctx_app_1 red_ctx_app_2
  red_ctx_try red_ctx_comp
  red_ctx_con_1_1 red_ctx_con_2_1 red_ctx_con_2_2 
  red_ctx_con_3_1 red_ctx_con_3_2 red_ctx_con_3_3 
  : red_ctx_hints.


(************************************************************)
(* ** Definitions of specifications (predicate Spec) *)

Section SpecDef.
Implicit Types A : Type.
Implicit Types f : val.

(** [Spec1 _A K f] means that for any argument [X] of
    type [A], the proposition [K X t] is true, where
    [t] stands for the application of function [f] to
    the value [_A X] (the encoding of the argument [X]). *)

Definition Spec1 A1 (_A1:code A1) (K:A1->trm->Prop) f := 
  forall X1, K X1 (f ' (_A1 X1)).

(** Predicates [SpecN] describe curried N-ary functions.
    [Spec{N+1} _A1 _A2 .. _A{N+1} f] holds if for any 
    argument [X], the application of [f] to [_A1 X]
    returns a function that satisfies the predicate
    [Spec{N} _A2 .. _A{N+1}]. *)

Definition Spec2 A1 (_A1:code A1) A2 (_A2:code A2) 
  (K:A1->A2->trm->Prop) := 
  Spec1 _A1 (fun X1 => >- >> _Val st Spec1 _A2 (K X1)).

Definition Spec3 A1 (_A1:code A1) A2 (_A2:code A2) 
  A3 (_A3:code A3) (K:A1->A2->A3->trm->Prop) := 
  Spec1 _A1 (fun X1 => >- >> _Val st Spec2 _A2 _A3 (K X1)).

Definition Spec4 A1 (_A1:code A1) A2 (_A2:code A2) 
  A3 (_A3:code A3) A4 (_A4:code A4) 
  (K:A1->A2->A3->A4->trm->Prop) := 
  Spec1 _A1 (fun X1 => >- >> _Val st Spec3 _A2 _A3 _A4 (K X1)).

End SpecDef.


(************************************************************)
(* ** Notation for specifications *)

(** The notation used for [Spec] predicates are:
    - [spec \[x1:_A1\] .. \[xN:_AN\] = t is K] stands
      for [SpecN _A1 _A2 .. _AN (fun x1 .. xN t => K)].
      Variables [xi] and variable [t] are bound in [K].
    - [spec \[x1:_A1\] .. \[xN:_AN\] is B] stands
      for [SpecN _A1 _A2 .. _AN (fun x1 .. xN t => t >- B)].
      Variables [xi] are bound in the behaviour [B]. *)

(** Arity 1 *)

Notation "'spec' f '[' x1 ':' _A1 ']' '=' t 'is' K" := 
  (Spec1 _A1 (fun x1 t => K) f)
  (at level 69, f at level 0, _A1 at level 0, x1 at level 0,
   t at level 0,  K at level 90, format
   "spec  f  [ x1 : _A1 ]  =  t  is  '//'  K  '//'").

Notation "'spec' f '[' x1 ':' _A1 ']' 'is' B" := 
  (Spec1 _A1 (fun x1 t => t >- B) f)
  (at level 69, f at level 0, x1 at level 0, _A1 at level 0, 
   B at next level, format
   "spec  f  [ x1 : _A1 ]  is  '//'  B  '//'").

(** Arity 2 *)

Notation "'spec' f '[' x1 ':' _A1 ']' '[' x2 ':' _A2 ']' '=' t 'is' K" := 
  (Spec2 _A1 _A2 (fun x1 x2 t => K) f)
  (at level 69, f at level 0, _A1 at level 0, _A2 at level 0,
   x1 at level 0, x2 at level 0, t at level 0, K at level 90, format
  "spec  f  [ x1 : _A1 ]  [ x2 : _A2 ]  =  t  is  '//'  K  '//'").

Notation "'spec' f '[' x1 ':' _A1 ']' '[' x2 ':' _A2 ']' 'is' B" := 
  (Spec2 _A1 _A2 (fun x1 x2 t => t >- B) f)
  (at level 69, f at level 0, _A1 at level 0, _A2 at level 0,
   x1 at level 0, x2 at level 0, B at next level, format
   "spec  f  [ x1 : _A1 ]  [ x2 : _A2 ]  is  '//'  B  '//'").

(** Arity 3 *)

Notation "'spec' f '[' x1 ':' _A1 ']' '[' x2 ':' _A2 ']' '[' x3 ':' _A3 ']' '=' t 'is' K" := 
  (Spec3 _A1 _A2 _A3 (fun x1 x2 x3 t => K) f)
  (at level 69, f at level 0, _A1 at level 0, _A2 at level 0, _A3 at level 0,
   x1 at level 0, x2 at level 0, x3 at level 0, t at level 0, K at level 90, format
  "spec  f  [ x1 : _A1 ]  [ x2 : _A2 ]  [ x3 : _A3 ]  =  t  is  '//'  K  '//'").

Notation "'spec' f '[' x1 ':' _A1 ']' '[' x2 ':' _A2 ']' '[' x3 ':' _A3 ']' 'is' B" := 
  (Spec3 _A1 _A2 _A3 (fun x1 x2 x3 t => t >- B) f)
  (at level 69, f at level 0, _A1 at level 0, _A2 at level 0, _A3 at level 0,
   x1 at level 0, x2 at level 0, x3 at level 0, B at next level, format
   "spec  f  [ x1 : _A1 ]  [ x2 : _A2 ]  [ x3 : _A3 ]  is  '//'  B  '//'").

(** Arity 4 *)

Notation "'spec' f '[' x1 ':' _A1 ']' '[' x2 ':' _A2 ']' '[' x3 ':' _A3 ']' '[' x4 ':' _A4 ']' '=' t 'is' K" := 
  (Spec4 _A1 _A2 _A3 _A4 (fun x1 x2 x3 x4 t => K) f)
  (at level 69, f at level 0, _A1 at level 0, _A2 at level 0, _A3 at level 0, _A4 at level 0,
   x1 at level 0, x2 at level 0, x3 at level 0, x4 at level 0, t at level 0,  K at level 90, format
  "spec  f  [ x1 : _A1 ]  [ x2 : _A2 ]  [ x3 : _A3 ]  [ x4 : _A4 ]  =  t  is  '//'  K  '//'").

Notation "'spec' f '[' x1 ':' _A1 ']' '[' x2 ':' _A2 ']' '[' x3 ':' _A3 ']' '[' x4 ':' _A4 ']' 'is' B" := 
  (Spec4 _A1 _A2 _A3 _A4 (fun x1 x2 x3 x4 t => t >- B) f)
  (at level 69, f at level 0, _A1 at level 0, _A2 at level 0, _A3 at level 0, _A4 at level 0,
   x1 at level 0, x2 at level 0, x3 at level 0, x4 at level 0, B at next level, format
   "spec  f  [ x1 : _A1 ]  [ x2 : _A2 ]  [ x3 : _A3 ]  [ x4 : _A4 ]  is  '//'  B  '//'").


(************************************************************)
(* ** Notation for specifications with un-named arguments *)

(** When the result of a function does not depend on the
    value of one of its arguments, we need not bind its
    name, e.g. if the second argument is not used we
    may write [spec \[x1:_A1\] \[__:_A2\] = t is K]. 
    This set of notation is actually necessary for Coq to 
    display specification properly when one argument is 
    unnamed (the notation defined earlier are not recognized 
    when an argument [xi] does not occur in [K]). *)

(** Arity 1 *)

Notation "'spec' f '[' '__' ':' _A1 ']' '=' t 'is' K" := 
  (Spec1 _A1 (fun _ t => K) f)
  (at level 69, f at level 0, _A1 at level 0, 
   t at level 0, K at level 90, format 
   "spec  f  [ __ : _A1 ]  =  t  is  '//'  K  '//'").

(** Arity 2 *)

Notation "'spec' f '[' '__' ':' _A1 ']' '[' x2 ':' _A2 ']' '=' t 'is' K" := 
  (Spec2 _A1 _A2 (fun _ x2 t => K) f)
  (at level 69, f at level 0, _A1 at level 0, _A2 at level 0,
    x2 at level 0, t at level 0, K at level 90, format
  "spec  f  [ __ : _A1 ]  [ x2 : _A2 ]  =  t  is  '//'  K  '//'").

Notation "'spec' f '[' x1 ':' _A1 ']' '[' '__' ':' _A2 ']' '=' t 'is' K" := 
  (Spec2 _A1 _A2 (fun x1 _ t => K) f)
  (at level 69, f at level 0, _A1 at level 0, _A2 at level 0,
   x1 at level 0, t at level 0, K at level 90, format
  "spec  f  [ x1 : _A1 ]  [ __ : _A2 ]  =  t  is  '//'  K  '//'").

(** Arity 3 *)

Notation "'spec' f '[' '__' ':' _A1 ']' '[' x2 ':' _A2 ']' '[' x3 ':' _A3 ']' '=' t 'is' K" := 
  (Spec3 _A1 _A2 _A3 (fun _ x2 x3 t => K) f)
  (at level 69, f at level 0, _A1 at level 0, _A2 at level 0, _A3 at level 0,
   x2 at level 0, x3 at level 0, t at level 0, K at level 90, format
  "spec  f  [ __ : _A1 ]  [ x2 : _A2 ]  [ x3 : _A3 ]  =  t  is  '//'  K  '//'").

Notation "'spec' f '[' x1 ':' _A1 ']' '[' '__' ':' _A2 ']' '[' x3 ':' _A3 ']' '=' t 'is' K" := 
  (Spec3 _A1 _A2 _A3 (fun x1 _ x3 t => K) f)
  (at level 69, f at level 0, _A1 at level 0, _A2 at level 0, _A3 at level 0,
   x1 at level 0, x3 at level 0, t at level 0, K at level 90, format
  "spec  f  [ x1 : _A1 ]  [ __ : _A2 ]  [ x3 : _A3 ]  =  t  is  '//'  K  '//'").

Notation "'spec' f '[' x1 ':' _A1 ']' '[' x2 ':' _A2 ']' '[' '__' ':' _A3 ']' '=' t 'is' K" := 
  (Spec3 _A1 _A2 _A3 (fun x1 x2 _ t => K) f)
  (at level 69, f at level 0, _A1 at level 0, _A2 at level 0, _A3 at level 0,
   x1 at level 0, x2 at level 0, t at level 0, K at level 90, format
  "spec  f  [ x1 : _A1 ]  [ x2 : _A2 ]  [ __ : _A3 ]  =  t  is  '//'  K  '//'").

(** Arity 4 : *)

Notation "'spec' f '[' '__' ':' _A1 ']' '[' x2 ':' _A2 ']' '[' x3 ':' _A3 ']' '[' x4 ':' _A4 ']' '=' t 'is' K" := 
  (Spec4 _A1 _A2 _A3 _A4 (fun _ x2 x3 x4 t => K) f)
  (at level 69, f at level 0, _A1 at level 0, _A2 at level 0, _A3 at level 0, _A4 at level 0,
   x2 at level 0, x3 at level 0, x4 at level 0, t at level 0,  K at level 90, format
  "spec  f  [ __ : _A1 ]  [ x2 : _A2 ]  [ x3 : _A3 ]  [ x4 : _A4 ]  =  t  is  '//'  K  '//'").

Notation "'spec' f '[' x1 ':' _A1 ']' '[' '__' ':' _A2 ']' '[' x3 ':' _A3 ']' '[' x4 ':' _A4 ']' '=' t 'is' K" := 
  (Spec4 _A1 _A2 _A3 _A4 (fun x1 _ x3 x4 t => K) f)
  (at level 69, f at level 0, _A1 at level 0, _A2 at level 0, _A3 at level 0, _A4 at level 0,
   x1 at level 0, x3 at level 0, x4 at level 0, t at level 0,  K at level 90, format
  "spec  f  [ x1 : _A1 ]  [ __ : _A2 ]  [ x3 : _A3 ]  [ x4 : _A4 ]  =  t  is  '//'  K  '//'").

Notation "'spec' f '[' x1 ':' _A1 ']' '[' x2 ':' _A2 ']' '[' '__' ':' _A3 ']' '[' x4 ':' _A4 ']' '=' t 'is' K" := 
  (Spec4 _A1 _A2 _A3 _A4 (fun x1 x2 _ x4 t => K) f)
  (at level 69, f at level 0, _A1 at level 0, _A2 at level 0, _A3 at level 0, _A4 at level 0,
   x1 at level 0, x2 at level 0, x4 at level 0, t at level 0,  K at level 90, format
  "spec  f  [ x1 : _A1 ]  [ x2 : _A2 ]  [ __ : _A3 ]  [ x4 : _A4 ]  =  t  is  '//'  K  '//'").

Notation "'spec' f '[' x1 ':' _A1 ']' '[' x2 ':' _A2 ']' '[' x3 ':' _A3 ']' '[' '__' ':' _A4 ']' '=' t 'is' K" := 
  (Spec4 _A1 _A2 _A3 _A4 (fun x1 x2 x3 _ t => K) f)
  (at level 69, f at level 0, _A1 at level 0, _A2 at level 0, _A3 at level 0, _A4 at level 0,
   x1 at level 0, x2 at level 0, x3 at level 0, t at level 0,  K at level 90, format
  "spec  f  [ x1 : _A1 ]  [ x2 : _A2 ]  [ x3 : _A3 ]  [ __ : _A4 ]  =  t  is  '//'  K  '//'").


(************************************************************)
(* ** Unfolding of definitions of specifications *)

(** Automated proof-search is directed by the statement of 
   the goal and has difficulties working modulo unfolding 
   of definitions. To work around this issue, we state 
   lemmas that paraphrase the definitions of the 
   predicates [SpecN], and add these lemmas to the 
   proof-search hint database. *)

Lemma spec1_from_spec2 :  
  forall (A1 A2:Type) (_A1:code A1) (_A2:code A2) 
         (K:A1->A2->trm->Prop) f,
  Spec2 _A1 _A2 K f ->
  Spec1 _A1 (fun X1 => >- >> _Val st Spec1 _A2 (K X1)) f.
Proof. auto. Qed.

Lemma spec1_from_spec3 :  
  forall (A1 A2 A3:Type) (_A1:code A1) (_A2:code A2)
         (_A3:code A3) (K:A1->A2->A3->trm->Prop) f,
  Spec3 _A1 _A2 _A3 K f ->
  Spec1 _A1 (fun X1 => >- >> _Val st Spec2 _A2 _A3 (K X1)) f.
Proof. auto. Qed.

Lemma spec1_from_spec4 :  
  forall (A1 A2 A3 A4:Type) (_A1:code A1) (_A2:code A2)
         (_A3:code A3) (_A4:code A4) (K:A1->A2->A3->A4->trm->Prop) f,
  Spec4 _A1 _A2 _A3 _A4 K f ->
  Spec1 _A1 (fun X1 => >- >> _Val st Spec3 _A2 _A3 _A4 (K X1)) f.
Proof. auto. Qed.

Hint Resolve spec1_from_spec2 spec1_from_spec3 spec1_from_spec4 : specs.