(**************************************************************************
* Proving functional programs through a deep embedding                    *
* Reasoning rules for verifying embedded programs                         *
***************************************************************************)

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

(** This file formalize the definition of behaviours
    and the statements and proofs of reasoning rules.
    The lemmas contained in this file need never be
    used by the end-user: tactics defined in the file
    [DeepTactics.v] are provided to apply reasoning 
    rules conveniently. *)


(************************************************************)
(* ** Proving behaviours of atomic terms *) 

(** The behaviour of a term [\v] is simply to return the
    value [v]. Similarly, the behaviour of an exception
    [exn v] is simply to throw the value [v]. *)

Section BehaviourTerminal.

Lemma prove_returns : forall (A:Type) (_A:code A) (V:A),
  (\_A V) >> _A st = V.
Proof. intros. apply~ behave_returns. apply reds_refl. Qed.

Lemma prove_returns_fun : forall v (P:val->Prop),
  P v -> (\ v) >> _Val st P.
Proof. 
  intros. apply* (behave_returns v). apply~ reds_refl. 
Qed. 

Lemma prove_throws : forall (C:con),
  (Exn C) >! C.
Proof. intros. apply~ behave_throws. apply reds_refl. Qed.

End BehaviourTerminal.


(************************************************************)
(* ** Proving implication between behaviours *)

(** The lemmas in this section can be used to show that a
    behaviour of the form [>> _A1 st P1] is stronger than 
    another one, say [>> _A2 st P2]. There are a number
    of specialization of the main lemma for particular cases:
    - when [_A1 = _A2],
    - when [_A1 = _Val] or [_A2 = _Val],
    - when [P1] or [P2] is of the form [= V].
    No need to worry about which lemma to use in the proof,
    the tactic [ximpl] picks up the appropriate one. *)

Section BImplProve.
Implicit Types A : Type.

(** Weakening with change of type *)

Lemma bimpl_cast : 
  forall A1 (P1:A1->Prop) A2 (P2:A2->Prop)
         (_A1 : code A1) (_A2 : code A2),
  (forall X1, P1 X1 ->
   exists X2, _A1 X1 = _A2 X2 /\ P2 X2) ->
  (>> _A1 st P1) ==> (>> _A2 st P2).
Proof.
  introv Imp Beh.
  destruct (behave_returns_inv Beh) as [x1 [Rx1 Px1]].
  destruct~ (Imp x1) as [x2 [Eq Px2]]. 
  apply (behave_returns x2); congruence.
 Qed.

Lemma bimpl_cast_leq : 
  forall A2 (P2:A2->Prop) A1 V1 V2
         (_A1 : code A1) (_A2 : code A2),
  _A1 V1 = _A2 V2 -> P2 V2 ->
  (>> _A1 st = V1) ==> (>> _A2 st P2).
Proof. intros. apply bimpl_cast. intros. subst*. Qed.

Lemma bimpl_cast_leq_req : 
  forall A2 (P2:A2->Prop) A1 V1 V2
         (_A1 : code A1) (_A2 : code A2),
  _A1 V1 = _A2 V2 ->
  (>> _A1 st = V1) ==> (>> _A2 st = V2).
Proof. intros. apply* bimpl_cast_leq. Qed.

(** Weakening without change of type *)

Lemma bimpl_nocast : 
  forall A (P1:A->Prop) (P2:A->Prop) (_A : code A),
  (forall X, P1 X -> P2 X) ->
  (>> _A st P1) ==> (>> _A st P2).
Proof. intros. apply* bimpl_cast. Qed.

Lemma bimpl_nocast_leq : 
  forall A (P:A->Prop) (_A : code A) V,
  P V ->
  (>> _A st = V) ==> (>> _A st P).
Proof. intros. apply bimpl_nocast. intros. subst~. Qed.

Lemma bimpl_nocast_leq_req : 
  forall A (_A : code A) V1 V2,
  V1 = V2 ->
  (>> _A st = V1) ==> (>> _A st = V2).
Proof. intros. apply* bimpl_nocast_leq. Qed.

(** Specialization for conversion from values *)

Lemma bimpl_cast_lval : 
  forall (P1:val->Prop) A2 (P2:A2->Prop) (_A2 : code A2),
  (forall v1, P1 v1 ->
   exists X2, v1 = _A2 X2 /\ P2 X2) ->
  (>> _Val st P1) ==> (>> _A2 st P2).
Proof. intros. apply* bimpl_cast. Qed.

Lemma bimpl_cast_lval_leq : 
  forall A (P:A->Prop) (_A : code A) V v,
  _A V = v -> P V ->
  (>> _Val st = v) ==> (>> _A st P).
Proof. intros. apply bimpl_cast_lval. intros. subst*. Qed.

Lemma bimpl_cast_lval_leq_req : 
  forall A (_A:code A) v V,
  _A V = v -> 
  (>> _Val st = v) ==> (>> _A st = V).
Proof. intros. apply* bimpl_cast_lval_leq. Qed.

(** Specialization for conversion to values *)

Lemma bimpl_cast_rval : 
  forall A1 (P1:A1->Prop) (P2:val->Prop) (_A1 : code A1),
  (forall V1, P1 V1 -> P2 (_A1 V1)) ->
  (>> _A1 st P1) ==> (>> _Val st P2).
Proof. intros. apply bimpl_cast. intros. unfolds* _Val. Qed.

Lemma bimpl_cast_rval_leq : 
  forall A (P:val->Prop) (_A : code A) V,
  P (_A V) ->
  (>> _A st = V) ==> (>> _Val st P).
Proof. intros. apply bimpl_cast_rval. intros. subst~. Qed.

Lemma bimpl_cast_rval_leq_req : 
  forall A (_A:code A) v V,
  _A V = v -> 
  (>> _A st = V) ==> (>> _Val st = v).
Proof. intros. apply* bimpl_cast_rval_leq. Qed.

End BImplProve.


(************************************************************)
(* ** Big-step reduction in evaluation contexts *)

Section RedCtxBigStep.
Hint Resolve reds_refl reds_step.
Implicit Types t : trm.
Implicit Types C : ctx.

(** If [C] is a reduction context, then [C t] mimics each 
    step and more generally each sequence of step that [t]
    may undertake. *)

Lemma ctx_red_elim : forall C t' t,
  (t --> t') -> red_ctx C -> (C t --> C t').
Proof. auto. Qed.

Lemma ctx_reds_elim : forall C t' t,
  (t -->* t') -> red_ctx C -> (C t -->* C t').
Proof. introv Red Con. induction* Red. Qed.

(** Auxiliary lemmas for working with contexts. *)

Lemma ctx_rewrite : forall (C:ctx) t t' B,
  t = t' -> ((C t') >- B) -> ((C t) >- B).
Proof. intros. subst~. Qed.

Lemma ctx_visible : forall (C:ctx) t t1 B,
  C t1 = t -> ((C t1) >- B) -> (t >- B).
Proof. intros. subst~. Qed.

(** Thereafter, if [t] reduces to [t'], then the behaviour 
    of [C t] is the same as the one of [C t']. *)

Lemma ctx_behave_red : forall C t t' B,
  (t --> t') -> red_ctx C -> (C t' >- B) -> (C t >- B).
Proof. intros. apply* behave_red. Qed.

Lemma ctx_behave_reds : forall C t t' B,
  (t -->* t') -> red_ctx C -> (C t' >- B) -> (C t >- B).
Proof. intros. apply* behave_reds. apply* ctx_reds_elim. Qed.

(** If [t] reduces to [t'], and [C t] reduces to [u],
    then [u] must be equal to [C t']. *)

Lemma red_deterministic_ctx : forall t t' C u,
  (C t --> u) -> (t --> t') -> red_ctx C -> u = C t'.
Proof. intros. apply* red_deterministic. Qed.

End RedCtxBigStep.


(************************************************************)
(* ** Focusing on terms in evaluation context *)

Section RedCtxFocus.
Implicit Types t : trm.
Implicit Types C : ctx.

(** The lemma [ctx_focus] states that to prove a
    behaviour for [C t] one may start by analysing
    the behaviour of [t]. This lemma is used to implement 
    the tactic [xin]. The remaining lemmas in this
    section are used to implement the tactic [xout]. *)

Lemma ctx_focus : forall C t1 B1 B,
  (t1 >- B1) -> 
  (forall t, (t >- B1) -> (C t >- B)) ->
  (C t1 >- B).
Proof. auto. Qed.

(** The next two lemmas allows to replace a goal about
    [C t] with one about [C (_A X)] under the assumption
    [P X] when [t >> _A st P]. *)

Lemma ctx_returns_reds : forall A (_A:code A) (P:A->Prop) t,
  (t >> _A st P) -> forall C, red_ctx C -> 
  exists X, P X /\ (C t -->* C (\_A X)).
Proof.
  introv Ret Con.
  destruct* (behave_returns_inv Ret) as [X [R PX]].
  exists X. split~. apply* ctx_reds_elim. 
Qed.

Lemma ctx_returns : forall A (P:A->Prop) (_A:code A) t,
  (t >> _A st P) -> forall C B, red_ctx C -> 
  (forall X, P X -> C (\_A X) >- B) ->
  (C t >- B).
Proof.
  introv Ret Con Gen.
  destruct (ctx_returns_reds Ret Con) as [X [PX Red]].
  apply* (@behave_reds (C (_A X))).
Qed.

(** The next lemma allows to replace a goal about
    [C t] with one about [C (exn v)] when [t] throws
    the exception [v], i.e. [t >! v]. *)

Lemma ctx_throws : forall c t,
  t >! c -> forall C B,
  red_ctx C -> (C (Exn c) >- B) -> (C t >- B).
Proof.
  introv Beh Con Gen. inversions Beh.
  apply* behave_reds. apply* ctx_reds_elim.
Qed.

(** The next lemma allows to conclude that [C t] diverges
    when [t] diverges. *)

Hint Resolve reduces_intro.

Lemma diverges_ctx : forall C t,
  diverges t -> red_ctx C -> diverges (C t).
Proof.
  introv Div Ctx Reds. gen_eq u: (C t). gen t.
  induction Reds; intros ta Diva Eq; subst;
   lets [tb [Red Divb]]: (diverges_inv Diva).
  auto* (ctx_red_elim Red Ctx).
  auto* (red_deterministic_ctx H Red Ctx).
Qed.

Lemma ctx_diverges : forall C t,
  t >oo -> red_ctx C -> (C t) >oo.
Proof.
  introv Beh Con. inversions Beh.
  apply behave_diverges. apply* diverges_ctx.
Qed.

(** The next lemma allows to conclude that [C t] is
    unspecified whenever [t] is unspecified. This lemma
    is only provided for the sake of uniformity with
    the other behaviours. It is not really needed, since
    any term admit the unspecified behaviour anyway. *)

Lemma ctx_unspecified : forall t,
  t >? -> forall C, (C t) >?.
Proof. intros. apply behave_unspecified. Qed.

End RedCtxFocus.


(************************************************************)
(* Optimized reduction rules *)

(** A reformulation of reduction rule [red_beta], that
    makes introduces an explicit equality for the result.
    This statement eases the application of the 
    beta-reduction rule with respect to unification. *)

Lemma red_beta_explicit : forall r p t1 t2 v F,
     F = val_fix novar p t1 t2 ->
     r = match matching p v with 
              | None => t2 ' v
              | Some m => subst m t1
              end ->
     F ' v --> r.
Proof. intros. subst. apply* red_beta. Qed.

Lemma red_beta_fix_explicit : forall r f p t1 t2 v F,
     f != novar ->
     F = val_fix f p t1 t2 ->
     r = match matching p v with 
              | None => (subst (f ~> F) t2) ' v
              | Some m => subst (m \U (f ~> F)) t1
              end ->
     F ' v --> r.
Proof. intros. subst. apply* red_beta_fix. Qed.

(** Other optimizations *)

Lemma red_beta_fun : forall x t1 t2 v,
  (val_fix novar (pat_var x) t1 t2) ' \v --> subst (x ~> v) t1.
Proof. 
  intros. eapply red_beta_explicit. eauto. auto.
Qed.

Lemma red_beta_pat_fail : forall p t1 t2 v,
  matching p v = None ->
  (val_fix novar p t1 t2) ' \v --> 
  t2 ' v.
Proof.
  intros. eapply red_beta_explicit. eauto. rewrite~ H.
Qed.

Lemma behave_red_beta_fun_val : forall x t1 t2 v B,
  (subst (x ~> v) t1) >- B ->
  (val_fix novar (pat_var x) t1 t2) ' \v >- B.
Proof.
  intros. apply* (@ctx_behave_red ctx_hole).
  apply red_beta_fun. apply red_ctx_hole. auto.
Qed.

Lemma behave_red_beta_fun_trm : forall x t1 t2 v B,
  trm_vars (trm_fix novar (pat_var x) t1 t2) = nil ->
  (subst (x ~> v) t1) >- B ->
  (trm_fix novar (pat_var x) t1 t2) ' \v >- B.
Proof.
  intros. apply* (@ctx_behave_reds ctx_hole).
  apply (@reds_trans ((val_fix novar (pat_var x) t1 t2) ' v)).
  apply reds_red. apply red_app_1. apply red_val.
  cbv delta -[trm_vars] beta. unfolds novar. rewrite~ H.
  apply reds_red. eapply red_beta_fun. apply red_ctx_hole.
  auto. 
Qed.

Lemma behave_red_beta_fail : forall p t1 t2 v B,
  matching p v = None ->
  (t2 ' \v) >- B ->
  (val_fix novar p t1 t2) ' \v >- B.
Proof.
  intros. apply* (@ctx_behave_red ctx_hole).
  apply~ red_beta_pat_fail. apply red_ctx_hole. auto.
Qed.

Lemma behave_red_fix_fail : forall f p t1 t2 v B,
  f != novar ->
  matching p v = None ->
  ((subst (f ~> (val_fix f p t1 t2)) t2) ' \v) >- B ->
  (val_fix f p t1 t2) ' \v >- B.
Proof.
  intros. apply* (@ctx_behave_red ctx_hole).
  eapply red_beta_fix_explicit. eauto. eauto. rewrite~ H0.
  apply red_ctx_hole. auto.
Qed.


(************************************************************)
(* ** Weakening of specifications *)

(** Weakening lemmas are used to weaken specifications of
    functions. For instance, a specification [Spec1 _A1 K1 f] 
    may be weakened into [Spec1 _A1 K2 f] if forall [x] and
    forall [t], the proposition [K1 x t] implies [K2 x t].
    In the particular case where specification are described
    directly in terms of behaviours, we have the following:
    specification [spec f \[x:_A\] is B1] may be weakened
    into [spec f \[x:_A\] is B2] if [forall x, B1 ==> B2].
    These lemmas are exploited by tactic [xweakens]. *)

Lemma spec1_weaken :
  forall (A1:Type)(_A1:code A1),
  forall (K1:A1->trm->Prop) f,
  Spec1 _A1 K1 f -> forall (K2:A1->trm->Prop),
  (forall x t, K1 x t -> K2 x t) ->
  Spec1 _A1 K2 f.
Proof. intros_all~. Qed.

Lemma spec2_weaken : 
  forall (A1 A2:Type) (_A1:code A1) (_A2:code A2), 
  forall (K1:A1->A2->trm->Prop) f,
  Spec2 _A1 _A2 K1 f -> forall (K2:A1->A2->trm->Prop),
  (forall x1 x2 t, K1 x1 x2 t -> K2 x1 x2 t) -> 
  Spec2 _A1 _A2 K2 f.
Proof.
  unfold Spec2. intros. apply* spec1_weaken. intro.
  rapply bimpl_nocast. intros. apply* spec1_weaken.
Qed. 

Lemma spec3_weaken : 
  forall (A1 A2 A3:Type)(_A1:code A1)(_A2:code A2)(_A3:code A3),
  forall (K1:A1->A2->A3->trm->Prop) f,
  Spec3 _A1 _A2 _A3 K1 f -> forall (K2:A1->A2->A3->trm->Prop),
  (forall x1 x2 x3 t, K1 x1 x2 x3 t -> K2 x1 x2 x3 t) -> 
  Spec3 _A1 _A2 _A3 K2 f.
Proof.
  unfold Spec3. intros. apply* spec1_weaken. intro.
  rapply bimpl_nocast. intros. apply* spec2_weaken.
Qed.

Lemma spec4_weaken : 
  forall (A1 A2 A3 A4:Type)(_A1:code A1)(_A2:code A2)(_A3:code A3)
  (_A4:code A4),
  forall (K1:A1->A2->A3->A4->trm->Prop) f,
  Spec4 _A1 _A2 _A3 _A4 K1 f -> forall (K2:A1->A2->A3->A4->trm->Prop),
  (forall x1 x2 x3 x4 t, K1 x1 x2 x3 x4 t -> K2 x1 x2 x3 x4 t) -> 
  Spec4 _A1 _A2 _A3 _A4 K2 f.
Proof.
  unfold Spec4. intros. apply* spec1_weaken. intro.
  rapply bimpl_nocast. intros. apply* spec3_weaken.
Qed.


(************************************************************)
(* ** Curried functions *)

Section curried.
Variables (A1 A2 A3 A4 : Type).
Variables (_A1:code A1) (_A2:code A2) (_A3:code A3) (_A4:code A4).

Definition curried1 :=
  Spec1 _A1 (fun _ _ => True).
Definition curried2 :=
  Spec2 _A1 _A2 (fun _ _ _ => True).
Definition curried3 :=
  Spec3 _A1 _A2 _A3 (fun _ _ _ _ => True).
Definition curried4 :=
  Spec4 _A1 _A2 _A3 _A4 (fun _ _ _ _ _ => True).

End curried.


(************************************************************)
(* ** Predicate describing behaviours *)

Definition descr (P:trm->Prop) :=
  forall t t', (t --> t') -> (P t <-> P t').

Lemma descr_elim : forall P t t',
  descr P -> t -->* t' -> P t -> P t'.
Proof. 
  introv Des Reds. induction Reds as [ t | t2 t1 t3 Red].  
  auto. lets*: (Des t1 t2). 
Qed.

Lemma descr_elim_back : forall P t t',
  descr P -> t -->* t' -> P t' -> P t.
Proof. 
  introv Des Reds. induction Reds as [ t | t2 t1 t3 Red].  
  auto. lets*: (Des t1 t2). 
Qed.

Lemma descr_elim_ctx : forall t P t' C,
  descr P -> red_ctx C -> t -->* t' -> P (C t) -> P (C t').
Proof.
  introv Des Ctx Reds PCt. lets: (ctx_reds_elim Reds Ctx).
  apply* descr_elim. 
Qed.

Lemma descr_elim_ctx_back : forall t P t' C,
  descr P -> red_ctx C -> t -->* t' -> P (C t') -> P (C t).
Proof.
  introv Des Ctx Reds PCt. lets: (ctx_reds_elim Reds Ctx).
  apply* descr_elim_back. 
Qed.


(************************************************************)
(* ** Introduction of specifications *)

(** These lemmas provide with a direct way of proving
    that a specification holds of a function, without
    having to introduce the arguments of the function
    one by one. *)

Lemma spec1_intro :
  forall (A1:Type) (_A1:code A1) (K:A1->trm->Prop) f,
  (curried1 _A1 f) ->
  (forall X1, descr (K X1)) ->
  (forall X1, K X1 (\f ' (_A1 X1))) ->
  (Spec1 _A1 K f).
Proof. intros_all~. Qed.

Lemma spec2_intro :
  forall (A1 A2:Type) (_A1:code A1) (_A2:code A2) 
         (K:A1->A2->trm->Prop) f,
  (curried2 _A1 _A2 f) ->
  (forall X1 X2, descr (K X1 X2)) ->
  (forall X1 X2, K X1 X2 (\f ' (_A1 X1) ' (_A2 X2))) ->
  (Spec2 _A1 _A2 K f).
Proof.
  introv Sf0 RK PK.
  intros X1. apply_in Sf0 X1. apply_in PK X1.
  lets [f1 [Sf1 _]]: (behave_returns_inv Sf0). clear Sf0.
  eapply behave_reds; [ | apply Sf1 ].
  apply prove_returns_fun. intros X2. apply_in PK X2.
  refine (@descr_elim_ctx _ (K X1 X2) _ (ctx_app_1 (_A2 X2)) _ _ _ _).
  eauto. auto with red_ctx_hints. eauto. unfold ctx_app_1. auto.
Qed.

Lemma spec3_intro :
  forall (A1 A2 A3:Type) (_A1:code A1) (_A2:code A2)
         (_A3:code A3) (K:A1->A2->A3->trm->Prop) f,
  (curried3 _A1 _A2 _A3 f) ->
  (forall X1 X2 X3, descr (K X1 X2 X3)) ->
  (forall X1 X2 X3, K X1 X2 X3 (\f ' (_A1 X1) ' (_A2 X2) ' (_A3 X3))) ->
  (Spec3 _A1 _A2 _A3 K f). 
Proof.
  introv Sf0 RK PK.
  intros X1. apply_in Sf0 X1. apply_in PK X1.
  lets [f1 [Sf1 Sf2]]: (behave_returns_inv Sf0). clear Sf0.
  eapply behave_reds; [ | apply Sf1 ].
  apply prove_returns_fun. intros X2.
  apply_in PK X2. apply_in Sf2 X2.
  lets [f2 [Sf1' Sf2']]: (behave_returns_inv Sf2). clear Sf2.
  eapply behave_reds; [ | apply Sf1' ].
  apply prove_returns_fun. intros X3. apply_in PK X3.
  refine (@descr_elim_ctx _ (K X1 X2 X3) _ (ctx_app_1 (_A3 X3)) _ _ _ _).
  eauto. auto with red_ctx_hints. eauto. unfold ctx_app_1. 
  refine (@descr_elim_ctx _ (K X1 X2 X3) _ (ctx_comp (ctx_app_1 (_A3 X3)) (ctx_app_1 (_A2 X2))) _ _ _ _).
  eauto. auto with red_ctx_hints. eauto. unfold ctx_app_1, ctx_comp. auto. 
Qed.

Lemma spec4_intro :
  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,
  (curried4 _A1 _A2 _A3 _A4 f) ->
  (forall X1 X2 X3 X4, descr (K X1 X2 X3 X4)) ->
  (forall X1 X2 X3 X4, K X1 X2 X3 X4 (\f ' (_A1 X1) ' (_A2 X2) ' (_A3 X3) ' (_A4 X4))) ->
  (Spec4 _A1 _A2 _A3 _A4 K f). 
Proof.
  introv Sf0 RK PK.
  intros X1. apply_in Sf0 X1. apply_in PK X1.
  lets [f1 [Sf1 Sf2]]: (behave_returns_inv Sf0). clear Sf0.
  eapply behave_reds; [ | apply Sf1 ].
  apply prove_returns_fun. intros X2.
  apply_in PK X2. apply_in Sf2 X2.
  lets [f2 [Sf1' Sf2']]: (behave_returns_inv Sf2). clear Sf2.
  eapply behave_reds; [ | apply Sf1' ].
  apply prove_returns_fun. intros X3. 
  apply_in PK X3. apply_in Sf2' X3.
  lets [f3 [Sf1'' Sf2'']]: (behave_returns_inv Sf2'). clear Sf2'.
  eapply behave_reds; [ | apply Sf1'' ].
  apply prove_returns_fun. intros X4. 
  refine (@descr_elim_ctx _ (K X1 X2 X3 X4) _ (ctx_app_1 (_A4 X4)) _ _ _ _).
  eauto. auto with red_ctx_hints. eauto. unfold ctx_app_1. 
  refine (@descr_elim_ctx _ (K X1 X2 X3 X4) _ (ctx_comp (ctx_app_1 (_A4 X4)) (ctx_app_1 (_A3 X3))) _ _ _ _).
  eauto. auto with red_ctx_hints. eauto. unfold ctx_app_1, ctx_comp.
  refine (@descr_elim_ctx _ (K X1 X2 X3 X4) _ (ctx_comp (ctx_comp (ctx_app_1 (_A4 X4)) (ctx_app_1 (_A3 X3))) (ctx_app_1 (_A2 X2))) _ _ _ _).
  eauto. auto with red_ctx_hints. eauto. unfold ctx_app_1, ctx_comp. auto.
Qed.


(************************************************************)
(* ** Elimination of specifications *)

Lemma reds_app_1 : forall (t1 t1r : trm) (v2 : val),
   t1 -->* t1r -> t1 ' v2 -->* t1r ' v2.
Proof.
  induction 1. apply reds_refl.
  apply* reds_step. apply* red_app_1.
Qed.

Lemma spec1_elim :
  forall (A1:Type) (_A1:code A1) (K:A1->trm->Prop) f,
  (Spec1 _A1 K f) ->
  (forall X1, descr (K X1)) ->
  (forall X1, K X1 (\f ' (_A1 X1))).
Proof. intros_all~. Qed.

Lemma spec2_elim :
  forall (A1 A2:Type) (_A1:code A1) (_A2:code A2) 
         (K:A1->A2->trm->Prop) f,
  (Spec2 _A1 _A2 K f) ->
  (forall X1 X2, descr (K X1 X2)) ->
  (forall X1 X2, K X1 X2 (\f ' (_A1 X1) ' (_A2 X2))).
Proof.
  introv Sf Des. intros. 
  lets g Reds Sg: (behave_returns_inv (Sf X1)).
  eapply descr_elim_back. 
    auto. 
    apply* reds_app_1.
    apply~ (spec1_elim Sg).  
Qed.

Lemma spec3_elim :
  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) ->
  (forall X1 X2 X3, descr (K X1 X2 X3)) ->
  (forall X1 X2 X3, K X1 X2 X3 (\f ' (_A1 X1) ' (_A2 X2) ' (_A3 X3))).
Proof.
  introv Sf Des. intros. 
  lets g Reds Sg: (behave_returns_inv (Sf X1)).
  eapply descr_elim_back. 
    auto.
    apply reds_app_1. apply reds_app_1. eauto. 
    apply~ (spec2_elim Sg).  
Qed.

Lemma spec4_elim :
  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) ->
  (forall X1 X2 X3 X4, descr (K X1 X2 X3 X4)) ->
  (forall X1 X2 X3 X4, K X1 X2 X3 X4 (\f ' (_A1 X1) ' (_A2 X2) ' (_A3 X3) ' (_A4 X4))).
Proof.
  introv Sf Des. intros. 
  lets g Reds Sg: (behave_returns_inv (Sf X1)).
  eapply descr_elim_back. 
    auto.
    apply reds_app_1. apply reds_app_1. apply reds_app_1. eauto. 
    apply~ (spec3_elim Sg).  
Qed.


(************************************************************)
(* ** Elimination of specifications under contexts *)

(** The first lemma is used to reason on an application 
    of a function [f] to an argument [_A1 V1] under an 
    evaluation context [C], when a specification of the
    form [Spec1 _A1 K f] is known for [f].
    The following lemmas generalize this statement
    to application of greater arity.
    These lemmas are exploited by tactic [xapply]. *)

Lemma spec1_elim_ctx :
  forall C (A1:Type) (_A1:code A1) (K:A1->trm->Prop) f,
  Spec1 _A1 K f -> forall V1 B B1,
  red_ctx C ->
  (forall t, K V1 t -> t >- B1) ->
  (forall t, t >- B1 -> C t >- B) ->
  C (f ' _A1 V1) >- B.
Proof. auto. Qed.

Lemma spec2_elim_ctx :
  forall C (A1 A2:Type) (_A1:code A1) (_A2:code A2) 
         (K:A1->A2->trm->Prop) f,
  Spec2 _A1 _A2 K f -> forall V1 V2 B B1,
  red_ctx C ->
  (forall t, K V1 V2 t -> t >- B1) ->
  (forall t, t >- B1 -> C t >- B) ->
  C (f ' _A1 V1 ' _A2 V2) >- B.
Proof.
  intros. lets_simpl M: (ctx_returns (H V1)).
  refine (M (ctx_comp C (ctx_app_1 _ )) _ _ _).
  auto with red_ctx_hints. intros t S. 
  rapply* (spec1_elim_ctx (C:=C) S).
Qed.

Lemma spec3_elim_ctx :
  forall C (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 -> forall V1 V2 V3 B B1,
  red_ctx C ->
  (forall t, K V1 V2 V3 t -> t >- B1) ->
  (forall t, t >- B1 -> C t >- B) ->
  C (f ' _A1 V1 ' _A2 V2 ' _A3 V3) >- B.
Proof.
  intros. lets_simpl M: (ctx_returns (H V1)).
  refine (M (ctx_comp (ctx_comp C (ctx_app_1 _ )) (ctx_app_1 _ )) _ _ _).
  auto with red_ctx_hints. intros t S. rapply* (spec2_elim_ctx (C:=C) S).
Qed.

Lemma spec4_elim_ctx :
  forall C (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 -> forall V1 V2 V3 V4 B B1,
  red_ctx C ->
  (forall t, K V1 V2 V3 V4 t -> t >- B1) ->
  (forall t, t >- B1 -> C t >- B) ->
  C (f ' _A1 V1 ' _A2 V2 ' _A3 V3 ' _A4 V4) >- B.
Proof.
  intros. lets_simpl M: (ctx_returns (H V1)).
  refine (M (ctx_comp (ctx_comp (ctx_comp C (ctx_app_1 _ )) 
            (ctx_app_1 _ )) (ctx_app_1 _ )) _ _ _).
  auto with red_ctx_hints. intros t S. rapply* (spec3_elim_ctx (C:=C) S).
Qed.


(************************************************************)
(* ** Proving specifications by induction *)

Section SpecInduction.

Ltac prove_red2_with SD :=
  let V1 := fresh in let V2 := fresh in let Red := fresh in
  intros V1 V2; introv Red; destruct* (SD V1 V2 _ _ Red).
Ltac prove_red3_with SD :=
  let V1 := fresh in let V2 := fresh in let V3 := fresh in
  let Red := fresh in
  intros V1 V2 V3; introv Red; destruct* (SD V1 V2 V3 _ _ Red).
Ltac prove_red4_with SD :=
  let V1 := fresh in let V2 := fresh in let V3 := fresh in
  let V4 := fresh in let Red := fresh in
  intros V1 V2 V3 V4; introv Red; destruct* (SD V1 V2 V3 V4 _ _ Red).

Lemma spec1_induction : 
  forall (A1:Type) (lt:A1->A1->Prop) (Wf: well_founded lt)
         f (_A1:code A1) (K:A1->trm->Prop),
  curried1 _A1 f ->
  (forall X1, descr (K X1)) ->
  (spec f [x1:_A1] = t is
     (spec f [x1':_A1] = t' is (lt x1' x1 -> K x1' t')) 
       -> K x1 t) ->
  Spec1 _A1 K f.
Proof.
  introv Wf Cur Des SfIH. intros X1. pattern X1. 
  apply~ (well_founded_ind Wf).
Qed.

Lemma spec2_induction : 
  forall (A1 A2:Type) (lt:(A1*A2)->(A1*A2)->Prop)
         (Wf: well_founded lt)
         f (_A1:code A1) (_A2:code A2) (K:A1->A2->trm->Prop),
  curried2 _A1 _A2 f ->
  (forall X1 X2, descr (K X1 X2)) ->
  (spec f [x1:_A1] [x2:_A2] = t is
     (spec f [x1':_A1] [x2':_A2] = t' is 
        (lt (x1',x2') (x1,x2) -> K x1' x2' t')) 
     -> K x1 x2 t) ->
  Spec2 _A1 _A2 K f.
Proof.
  introv Wf ST SD SfIH.
  apply~ spec2_intro. intros.
  refine (well_founded_ind Wf (fun X12:A1*A2 => 
    match X12 with (X1,X2) =>
       K X1 X2 (f ' _A1 X1 ' _A2 X2) end)
    _ (X1,X2)).
  intros [X1' X2'] IH.
  apply (spec2_elim SfIH). prove_red2_with SD.
  apply spec2_intro. auto. prove_red2_with SD.
  intros V1 V2. apply (IH (V1,V2)).
Qed.

Lemma spec3_induction : 
  forall (A1 A2 A3:Type) (lt:(A1*A2*A3)->(A1*A2*A3)->Prop)
         (Wf: well_founded lt)
         f (_A1:code A1) (_A2:code A2) (_A3:code A3)
         (K:A1->A2->A3->trm->Prop),
  curried3 _A1 _A2 _A3 f ->
  (forall X1 X2 X3, descr (K X1 X2 X3)) ->
  (spec f [x1:_A1] [x2:_A2] [x3:_A3] = t is
     (spec f [x1':_A1] [x2':_A2] [x3':_A3] = t' is 
        (lt (x1',x2',x3') (x1,x2,x3) -> K x1' x2' x3' t')) 
     -> K x1 x2 x3 t) ->
  Spec3 _A1 _A2 _A3 K f.
Proof.
  introv Wf ST SD SfIH.
  apply~ spec3_intro. intros.
  refine (well_founded_ind Wf (fun X123:A1*A2*A3 => 
    match X123 with ((X1,X2),X3) =>
       K X1 X2 X3 (f ' _A1 X1 ' _A2 X2 ' _A3 X3) end)
    _ (X1,X2,X3)).
  intros [[X1' X2'] X3'] IH.
  apply (spec3_elim SfIH). prove_red3_with SD.
  apply spec3_intro. auto. prove_red3_with SD.
  intros V1 V2 V3. apply (IH (V1,V2,V3)).
Qed.

Lemma spec4_induction : 
  forall (A1 A2 A3 A4:Type) (lt:(A1*A2*A3*A4)->(A1*A2*A3*A4)->Prop)
         (Wf: well_founded lt)
         f (_A1:code A1) (_A2:code A2) (_A3:code A3) (_A4:code A4)
         (K:A1->A2->A3->A4->trm->Prop),
  curried4 _A1 _A2 _A3 _A4 f ->
  (forall X1 X2 X3 X4, descr (K X1 X2 X3 X4)) ->
  (spec f [x1:_A1] [x2:_A2] [x3:_A3] [x4:_A4] = t is
     (spec f [x1':_A1] [x2':_A2] [x3':_A3] [x4':_A4] = t' is 
        (lt (x1',x2',x3',x4') (x1,x2,x3,x4) -> K x1' x2' x3' x4' t')) 
     -> K x1 x2 x3 x4 t) ->
  Spec4 _A1 _A2 _A3 _A4 K f.
Proof.
  introv Wf ST SD SfIH.
  apply~ spec4_intro. intros.
  refine (well_founded_ind Wf (fun X1234:A1*A2*A3*A4 => 
    match X1234 with (((X1,X2),X3),X4) =>
       K X1 X2 X3 X4 (f ' _A1 X1 ' _A2 X2 ' _A3 X3 ' _A4 X4) end)
    _ (X1,X2,X3,X4)).
  intros [[[X1' X2'] X3'] X4'] IH.
  apply (spec4_elim SfIH). prove_red4_with SD.
  apply spec4_intro. auto. prove_red4_with SD.
  intros V1 V2 V3 V4. apply (IH (V1,V2,V3,V4)).
Qed.

End SpecInduction.


(*==========================================================*)
(* * Divergence *)
(*==========================================================*)


Section ProveDiverges.

Hint Resolve reds_red reds_refl reds_step reduces_intro
  red_ctx_comp red_ctx_hole.

Inductive reds_plus : trm -> trm -> Prop :=
 | reds_plus_intro : forall x y z,
     x --> y -> y -->* z -> reds_plus x z.
Notation "x -->+ y" := (reds_plus x y) (at level 68).

Lemma reds_plus_to_star : forall x y,
  x -->+ y -> x -->* y.
Proof. intros. destruct* H. Qed.

Lemma prove_diverges : forall (P:trm->Prop),
  (forall t, P t -> exist C t', 
                      red_ctx C /\ P t' /\ t -->+ C t') ->
  (forall t, P t -> t >oo).
Proof.
  introv Unf Pt.
  cuts Ind: (forall T Tr, T -->* Tr ->
    forall C' C u t, (T = C' u) -> (u -->* C t) -> P t ->
    red_ctx C' -> red_ctx C -> reduces Tr). 
    lets [C [t' [Ctx [Pt' Plu]]]]: (Unf t Pt).
    apply_to Plu reds_plus_to_star.
    apply behave_diverges. introv Reds.
    apply* (Ind _ _ Reds ctx_hole C t t'). 
  clears t. introv H. 
  induction H; introv Eq Reds Pt CtxC' CtxC; subst.
  inverts Reds. 
    lets [C1 [t1 [Ctx1 [Pt1 Plu1]]]]: (Unf t Pt).
     inverts Plu1.
     exists (ctx_comp C' C y).
     apply~ (@ctx_red_elim (ctx_comp C' C)).
    rename y into u'.
     exists (C' u'). apply~ ctx_red_elim.
  rename y into T'. rename z into Tr. inverts Reds.
    lets [C1 [t1 [Ctx1 [Pt1 Plu1]]]]: (Unf t Pt).
     inverts Plu1. rename y into t1'.
     apply~ (IHstar (ctx_comp C' C) C1 t1' t1).
     apply~ (@red_deterministic_ctx t).    
    rename y into u'. apply~ (@IHstar C' C u' t). 
     apply~ (@red_deterministic_ctx u).  
Qed.


End ProveDiverges.