Set Implicit Arguments.
Require Export DeepSemantics.
Require Import LibClosure.
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.
Section BImplProve.
Implicit Types A : 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.
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.
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.
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.
Section RedCtxBigStep.
Hint Resolve reds_refl reds_step.
Implicit Types t : trm.
Implicit Types C : ctx.
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.
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.
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.
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.
Section RedCtxFocus.
Implicit Types t : trm.
Implicit Types C : ctx.
Lemma ctx_focus : forall C t1 B1 B,
(t1 >- B1) ->
(forall t, (t >- B1) -> (C t >- B)) ->
(C t1 >- B).
Proof. auto. Qed.
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.
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.
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.
Lemma ctx_unspecified : forall t,
t >? -> forall C, (C t) >?.
Proof. intros. apply behave_unspecified. Qed.
End RedCtxFocus.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.