```(**************************************************************************
* 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.

```