Set Implicit Arguments.
Require Export DeepPrinter.
Require Import LibClosure.
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.
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.
Definition val_of_trm t :=
match t with
| trm_val v => Some v
| _ => None
end.
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.
Definition inst := LibEnv.env Var val.
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.
Definition empty_subst : inst := LibEnv.empty.
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.
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.
Section Reduction.
Implicit Types t : trm.
Implicit Types v e : val.
Implicit Types n : int.
Reserved Notation "t1 --> t2" (at level 68).
Inductive red : trm -> trm -> Prop :=
| 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
| 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
| red_val : forall v t,
trm_to_val t = Some v ->
t --> v
| 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)
| 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)
| red_try_exn : forall e1 t2,
('try (exn e1) 'catch t2) --> (t2 ' e1)
| red_try_val : forall v1 t2,
('try v1 'catch t2) --> v1
| 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).
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.
Notation "t1 -->* t2" := (star red t1 t2) (at level 68).
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.
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.
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 reduces t :=
exists t', (t --> t').
Definition diverges t :=
forall tr, (t -->* tr) -> reduces tr.
Section Diverges.
Hint Resolve reds_red reds_refl reds_step.
Lemma reduces_intro : forall t t',
(t --> t') -> reduces t.
Proof. unfolds* reduces. Qed.
Hint Resolve reduces_intro.
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.
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.
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).
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).
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.
Section BehaveReduction.
Implicit Types t : trm.
Hint Resolve reds_red.
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.
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.
Definition bimpl B1 B2 :=
forall t, (t >- B1) -> (t >- B2).
Notation "B1 ==> B2" := (bimpl B1 B2) (at level 68).
Section BImpl.
Hint Constructors behave.
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 ctx := trm -> trm.
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.
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.
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.
Section SpecDef.
Implicit Types A : Type.
Implicit Types f : val.
Definition Spec1 A1 (_A1:code A1) (K:A1->trm->Prop) f :=
forall X1, K X1 (f ' (_A1 X1)).
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 "'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 '//'").
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 '//'").
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 '//'").
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 "'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 '//'").
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 '//'").
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 '//'").
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 '//'").
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.