Commit d62cc173 authored by charguer's avatar charguer

progress

parent 7a0c2004
......@@ -122,11 +122,11 @@ Qed.
End Properties.
Implicit Arguments MList_null_inv [].
Implicit Arguments MList_cons_eq [].
Implicit Arguments MList_cons [].
Implicit Arguments MList_not_null_inv_not_nil [].
Implicit Arguments MList_not_null_inv_cons [].
Arguments MList_null_inv : clear implicits.
Arguments MList_cons_eq : clear implicits.
Arguments MList_cons : clear implicits.
Arguments MList_not_null_inv_not_nil : clear implicits.
Arguments MList_not_null_inv_cons : clear implicits.
Global Opaque MList.
......
......@@ -67,13 +67,13 @@ Proof using.
hchange~ (hfield_not_null p hd). hsimpl~.
Qed.
Implicit Arguments MCell_inv_not_null [].
Arguments MCell_inv_not_null : clear implicits.
Lemma MCell_null_false : forall v q,
(MCell v q null) ==> \[False].
Proof using. intros. hchanges~ (MCell_inv_not_null null). Qed.
Implicit Arguments MCell_null_false [].
Arguments MCell_null_false : clear implicits.
Lemma MCell_hstar_MCell_inv : forall p1 p2 x1 x2 y1 y2,
MCell x1 y1 p1 \* MCell x2 y2 p2 ==+> \[p1 <> p2].
......@@ -299,11 +299,11 @@ Qed.
End MListProperties.
Implicit Arguments MList_null_inv [].
Implicit Arguments MList_cons_eq [].
Implicit Arguments MList_cons [].
Implicit Arguments MList_not_null_inv_cons [].
Implicit Arguments MList_not_null_inv_not_nil [].
Arguments MList_null_inv : clear implicits.
Arguments MList_cons_eq : clear implicits.
Arguments MList_cons : clear implicits.
Arguments MList_not_null_inv_cons : clear implicits.
Arguments MList_not_null_inv_not_nil : clear implicits.
Global Opaque MList.
......@@ -374,7 +374,7 @@ Proof using.
{ applys local_erase. xapplys rule_neq. }
intros X. xpull. intros EX. subst X.
applys local_erase. esplit. splits. eauto.
{ intros C. logics. xchange (MList_not_null_inv_cons p). { auto. }
{ intros C. rew_istrue. xchange (MList_not_null_inv_cons p). { auto. }
xpull. intros p' x L' EL.
applys local_erase. esplit. split.
{ applys local_erase. xapplys rule_get_tl. }
......@@ -384,7 +384,7 @@ Proof using.
{ intros r. xpull. intros Er. xchange (MList_cons p).
subst r L. applys local_erase. xapplys rule_add.
{ intros. subst. rew_length. fequals. math. } } }
{ intros C. logics. applys local_erase. unfolds. inverts C.
{ intros C. rew_istrue. applys local_erase. unfolds. inverts C.
xchange MList_null_inv. hpull. intros EL.
hsimpl. subst~. }
Qed.
......@@ -565,7 +565,7 @@ Qed.
End Properties.
Implicit Arguments MListSeg_then_MCell_inv_neq [].
Arguments MListSeg_then_MCell_inv_neq : clear implicits.
(* ********************************************************************** *)
......@@ -615,7 +615,7 @@ Proof using.
xapps. xapps.
xchanges (MListSeg_then_MCell_inv_neq pf pb) ;=> R.
(* xchange (MListSeg_then_MCell_inv_neq pf pb). xpull ;=> R. *)
xapp. hsimpl. isubst. fequals. logics. rewrite R. iff; congruence.
xapp. hsimpl. isubst. fequals. rew_istrue. rewrite R. iff; congruence.
Qed.
Hint Extern 1 (Register_spec val_is_empty) => Provide rule_is_empty.
......@@ -716,7 +716,7 @@ Lemma rule_transfer : forall p1 p2 L1 L2,
(MQueue L1 p1 \* MQueue L2 p2)
(fun r => \[r = val_unit] \* MQueue (L1 ++ L2) p1 \* MQueue nil p2).
Proof using.
xcf. xapps. xapps. xif ;=> C; fold_bool; logics. (* todo cleanup *)
xcf. xapps. xapps. xif ;=> C; fold_bool; rew_istrue. (* todo cleanup *)
{ unfold MQueue. xpull ;=> pf2 pb2 vx2 vy2 pf1 pb1 vx1 vy1.
destruct L2 as [|x L2']; tryfalse.
rewrite MListSeg_cons_eq. xpull ;=> pf2'.
......
......@@ -168,7 +168,7 @@
r ~> Stack L.
Proof using. intros. xunfolds~ Stack. Qed.
Implicit Arguments Stack_close [].
Arguments Stack_close : clear implicits..
Hint Extern 1 (RegisterOpen (Stack _)) =>
Provide Stack_open.
......
......@@ -51,7 +51,7 @@ Implicit Types T : tree.
(** Inhabited type *)
Instance tree_Inhab : Inhab tree.
Proof using. apply (prove_Inhab Leaf). Qed.
Proof using. apply (Inhab_of_val Leaf). Qed.
(** Well-founded order on trees *)
......@@ -152,8 +152,8 @@ Proof using.
hchange (MTree_node_eq p). hsimpl~.
Qed.
Implicit Arguments MTree_not_null_inv_not_leaf [].
Implicit Arguments MTree_not_null_inv_node [].
Arguments MTree_not_null_inv_not_leaf : clear implicits.
Arguments MTree_not_null_inv_node : clear implicits.
......@@ -251,14 +251,14 @@ Definition MTreeComplete'' (T:tree) (p:loc) : hprop :=
Lemma MTreeComplete'_eq : MTreeComplete' = MTreeComplete.
Proof using.
applys func_ext_2 ;=> T p.
applys fun_ext_2 ;=> T p.
unfold MTreeComplete, MTreeComplete'.
xunfold~ MTreeDepth.
Qed.
Lemma MTreeComplete''_eq : MTreeComplete'' = MTreeComplete.
Proof using.
applys func_ext_2 ;=> T p.
applys fun_ext_2 ;=> T p.
unfold MTreeComplete, MTreeComplete''.
applys himpl_antisym.
{ hpull ;=> (n&E). hsimpl*. }
......@@ -380,13 +380,13 @@ Proof using.
xapps. xif.
xchange focus_tree_null. xextracts. xret.
inverts IE. hsimpl. hchanges unfocus_Leaf.
fold_bool; rew_refl. intros H. set_in H.
fold_bool; rew_istrue. intros H. set_in H.
xchange~ (@focus_tree_not_null p).
xextract as y p1 p2 T1 T2 EQ. subst T.
inverts IE. xapps. xif.
xapps. xapp*. intros b.
hchange (@unfocus_Node p). hsimpl.
subst b. extens; rew_refl. subst E. iff M.
subst b. extens; rew_istrue. subst E. iff M.
eauto.
set_in M.
math.
......@@ -394,7 +394,7 @@ Proof using.
false* foreach_gt_notin H6 C0.
xif. xapps. xapps*. intros b.
hchange (@unfocus_Node p). hsimpl.
subst b. extens; rew_refl. subst E. iff M.
subst b. extens; rew_istrue. subst E. iff M.
rewrite <- for_set_union_empty_r.
repeat rewrite <- for_set_union_assoc.
apply in_union_get_3. assumption.
......
......@@ -127,7 +127,7 @@ Proof using.
{ inverts H2; auto_false. subst y1. applys* IHIH. }
Qed.
Implicit Arguments repr_inj [].
Arguments repr_inj : clear implicits.
Lemma repr_functional : forall L x z1 z2,
repr L x z1 ->
......@@ -219,7 +219,7 @@ Lemma link_related : forall R x y,
R x = R y ->
link R x y = R.
Proof using.
introv E. applys func_ext_1 ;=> i. unfold link. case_if as C.
introv E. applys fun_ext_1 ;=> i. unfold link. case_if as C.
{ destruct~ C. }
{ auto. }
Qed.
......
......@@ -25,7 +25,7 @@ Implicit Types t : trm.
Definition formula := hprop -> (val -> hprop) -> Prop.
Global Instance Inhab_formula : Inhab formula.
Proof using. apply (prove_Inhab (fun _ _ => True)). Qed.
Proof using. apply (Inhab_of_val (fun _ _ => True)). Qed.
(* ********************************************************************** *)
......@@ -114,7 +114,7 @@ Definition cf_def cf (t:trm) :=
Definition cf := FixFun cf_def.
Ltac fixfun_auto := try solve [
try fequals; auto; try apply func_ext_1; auto ].
try fequals; auto; try apply fun_ext_1; auto ].
Lemma cf_unfold_iter : forall n t,
cf t = func_iter n cf_def cf t.
......@@ -124,10 +124,10 @@ Proof using.
destruct t; fequals.
{ fequals~. }
{ fequals~. }
{ fequals~. applys~ func_ext_1. }
{ fequals~. applys~ fun_ext_1. }
{ fequals~. }
{ destruct t1; fequals~. destruct t2; fequals~.
applys~ func_ext_1. }
applys~ fun_ext_1. }
Qed.
Lemma cf_unfold : forall t,
......@@ -304,18 +304,27 @@ Implicit Types n : nat.
Implicit Types F : val.
Implicit Types f x : var.
Definition var_funs_exec (n:nat) (xs:vars) : bool := (* todo: use exec typeclass *)
nat_compare n (List.length xs)
&&& is_not_nil xs (* todo: rename to exec *)
&&& var_distinct xs. (* todo: remove triple &&& *)
(*-- LATER: move to TLC LibNatExec *)
Fixpoint nat_compare (x y : nat) :=
match x, y with
| O, O => true
| S x', S y' => nat_compare x' y'
| _, _ => false
end.
Lemma nat_compare_eq : forall n1 n2,
nat_compare n1 n2 = isTrue (n1 = n2).
Proof using.
intros n1. induction n1; intros; destruct n2; simpl; fold_bool; fold_prop; auto_false.
rewrite IHn1. extens. rew_reflect. math.
intros n1. induction n1; intros; destruct n2; simpl; rew_bool_eq; auto_false.
rewrite IHn1. extens. rew_istrue. math.
Qed.
Definition var_funs_exec (n:nat) (xs:vars) : bool := (* --todo: use exec typeclass *)
nat_compare n (List.length xs)
&& is_not_nil xs (* --todo: rename to exec *)
&& var_distinct xs.
Lemma var_funs_exec_eq : forall n xs,
var_funs_exec n xs = isTrue (var_funs n xs).
Proof using.
......@@ -323,7 +332,7 @@ Proof using.
rewrite nat_compare_eq.
rewrite is_not_nil_eq.
rewrite List_length_eq.
extens. rew_reflect. iff*.
extens. rew_istrue. iff*.
Qed.
Lemma triple_apps_funs_of_cf_iter : forall n F (vs:vals) xs t H Q,
......@@ -332,14 +341,14 @@ Lemma triple_apps_funs_of_cf_iter : forall n F (vs:vals) xs t H Q,
func_iter n cf_def cf (substs xs vs t) H Q ->
triple (trm_apps F vs) H Q.
Proof using.
introv EF N M. rewrite var_funs_exec_eq in N. rew_reflect in N.
introv EF N M. rewrite var_funs_exec_eq in N. rew_istrue in N.
applys* rule_apps_funs. applys* triple_trm_of_cf_iter.
Qed.
Definition var_fixs_exec (f:var) (n:nat) (xs:vars) : bool := (* todo: use exec typeclass *)
nat_compare n (List.length xs)
&&& is_not_nil xs (* todo: rename to exec *)
&&& var_distinct (f::xs). (* todo: remove triple &&& *)
&& is_not_nil xs (* todo: rename to exec *)
&& var_distinct (f::xs).
Lemma var_fixs_exec_eq : forall f n xs,
var_fixs_exec f n xs = isTrue (var_fixs f n xs).
......@@ -348,7 +357,7 @@ Proof using.
rewrite nat_compare_eq.
rewrite is_not_nil_eq.
rewrite List_length_eq.
extens. rew_reflect. iff*.
extens. rew_istrue. iff*.
Qed.
Lemma triple_apps_fixs_of_cf_iter : forall n f F (vs:vals) xs t H Q,
......@@ -357,7 +366,7 @@ Lemma triple_apps_fixs_of_cf_iter : forall n f F (vs:vals) xs t H Q,
func_iter n cf_def cf (subst f F (substs xs vs t)) H Q ->
triple (trm_apps F vs) H Q.
Proof using.
introv EF N M. rewrite var_fixs_exec_eq in N. rew_reflect in N.
introv EF N M. rewrite var_fixs_exec_eq in N. rew_istrue in N.
applys* rule_apps_fixs. applys* triple_trm_of_cf_iter.
Qed.
......@@ -528,7 +537,7 @@ Tactic Notation "xlet" "as" simple_intropattern(X) :=
(* ** Tactic [xif] *)
Ltac xif_post tt :=
logics.
rew_bool_eq.
Ltac xif_core tt :=
applys local_erase; esplit; splits;
......@@ -731,13 +740,13 @@ Ltac xval_template xlet_tactic xval_tactic xlet_cont :=
Ltac xval_basic tt :=
match goal with
| |- local ?F ?H ?Q => is_evar Q; applys local_erase; applys rel_le_refl
| |- local ?F ?H ?Q => is_evar Q; applys local_erase; applys refl_rel_incl'
| _ => applys xval_htop_lemma
end.
Ltac xval_as_basic X EX :=
match goal with
| |- local ?F ?H ?Q => is_evar Q; applys local_erase; applys rel_le_refl
| |- local ?F ?H ?Q => is_evar Q; applys local_erase; applys refl_rel_incl'
| _ => applys xval_htop_as_lemma; intros X EX
end.
......
......@@ -25,7 +25,7 @@ Implicit Types v w : val.
Definition formula := hprop -> (val -> hprop) -> Prop.
Global Instance Inhab_formula : Inhab formula.
Proof using. apply (prove_Inhab (fun _ _ => True)). Qed.
Proof using. apply (Inhab_of_val (fun _ _ => True)). Qed.
(* ********************************************************************** *)
......@@ -100,7 +100,7 @@ Definition cf_def cf (t:trm) :=
Definition cf := FixFun cf_def.
Ltac fixfun_auto := try solve [
try fequals; auto; try apply func_ext_1; auto ].
try fequals; auto; try apply fun_ext_1; auto ].
Lemma cf_unfold_iter : forall n t,
cf t = func_iter n cf_def cf t.
......@@ -109,7 +109,7 @@ Proof using.
intros f1 f2 t IH. unfold cf_def.
destruct t; fequals.
{ fequals~. }
{ fequals~. applys~ func_ext_1. }
{ fequals~. applys~ fun_ext_1. }
Qed.
Lemma cf_unfold : forall t,
......
......@@ -32,7 +32,7 @@ Ltac auto_star ::= jauto.
Definition Formula := forall `{Enc A}, hprop -> (A -> hprop) -> Prop.
Global Instance Inhab_Formula : Inhab Formula.
Proof using. apply (prove_Inhab (fun _ _ _ _ => True)). Qed.
Proof using. apply (Inhab_of_val (fun _ _ _ _ => True)). Qed.
Notation "' F H Q" := ((F:Formula) _ _ H Q)
(at level 65, F at level 0, H at level 0, Q at level 0,
......@@ -53,7 +53,7 @@ Definition Local (F:Formula) := fun A `{EA:Enc A} H Q =>
Lemma local_Local_eq : forall A `{EA:Enc A} (F:Formula),
local (@Local F A EA) = (@Local F A EA).
Proof using.
intros. apply prop_ext_2. intros H Q.
intros. apply pred_ext_2. intros H Q.
unfold Local. rewrite local_local. split~.
Qed.
......@@ -168,11 +168,11 @@ Proof using.
destruct t; fequals.
{ fequals~. }
{ fequals~. }
{ fequals~. applys~ func_ext_dep_3. }
{ fequals~. applys~ fun_ext_dep_3. }
{ fequals~. }
{ destruct t1; fequals~. destruct v0; fequals~.
destruct t2; fequals~. destruct v0; fequals~.
applys~ func_ext_1. }
applys~ fun_ext_1. }
Qed.
Lemma Cf_unfold : forall t,
......@@ -361,7 +361,7 @@ Lemma Triple_apps_funs_of_Cf_iter : forall n F (Vs:dyns) (vs:vals) xs t A `{EA:E
func_iter n Cf_def Cf (Substs xs Vs t) A EA H Q ->
Triple (trm_apps F vs) H Q.
Proof using.
introv EF EV N M. rewrite var_funs_exec_eq in N. rew_reflect in N.
introv EF EV N M. rewrite var_funs_exec_eq in N. rew_istrue in N.
subst. applys* Rule_apps_funs. applys* Triple_trm_of_Cf_iter.
Qed.
......@@ -372,7 +372,7 @@ Lemma Triple_apps_fixs_of_Cf_iter : forall n F f (Vs:dyns) (vs:vals) xs t A `{EA
func_iter n Cf_def Cf (subst f F (Substs xs Vs t)) A EA H Q ->
Triple (trm_apps (val_fixs f xs t) vs) H Q.
Proof using.
introv EF EV N M. rewrite var_fixs_exec_eq in N. rew_reflect in N.
introv EF EV N M. rewrite var_fixs_exec_eq in N. rew_istrue in N.
subst. applys* Rule_apps_fixs. applys* Triple_trm_of_Cf_iter.
Qed.
......@@ -608,7 +608,7 @@ Proof using.
introv E. applys local_erase. exists V. split~. hsimpl~.
Qed.
Implicit Arguments xval_htop_evar [A].
Arguments xval_htop_evar [A].
Lemma xval_htop_lemma : forall A (V:A) (EA:Enc A) v H Q,
v = enc V ->
......@@ -620,7 +620,7 @@ Proof using.
applys local_erase. exists~ V.
Qed.
Implicit Arguments xval_htop_lemma [A].
Arguments xval_htop_lemma [A].
(* TODO; simplify proof of original xval_htop_lemma in LambdaCF *)
......@@ -666,7 +666,7 @@ Ltac xvals_core tt ::=
Ltac xval_as_basic X EX ::=
match goal with
| |- Local ?F ?H ?Q => is_evar Q; applys local_erase; applys rel_le_refl
| |- Local ?F ?H ?Q => is_evar Q; applys local_erase; applys refl_rel_incl'
| _ => applys xval_htop_as_lemma; intros X EX
end.
......@@ -733,7 +733,7 @@ Ltac xlet_core tt ::=
Ltac xif_core tt ::=
applys local_erase;
applys Cf_if_val_bool;
rew_reflect.
rew_istrue.
*)
(* applys Cf_if_val_isTrue ;=> C. *)
......@@ -752,7 +752,7 @@ Ltac xfail_core tt ::=
Ltac xapply_core H cont1 cont2 :=
forwards_nounfold_then H ltac:(fun K =>
match xpostcondition_is_evar tt with
| true => eapply local_frame; [ xlocal | sapply K | cont1 tt | try apply rel_le_refl ]
| true => eapply local_frame; [ xlocal | sapply K | cont1 tt | try apply refl_rel_incl' ]
| false => eapply local_frame_htop; [ xlocal | sapply K | cont1 tt | cont2 tt ]
end).
*)
......@@ -791,7 +791,7 @@ Ltac fast_apply E :=
Ltac xapply_core H cont1 cont2 ::=
forwards_nounfold_then H ltac:(fun K =>
match xpostcondition_is_evar tt with
| true => eapply local_frame; [ xlocal | fast_apply K | cont1 tt | try apply rel_le_refl ]
| true => eapply local_frame; [ xlocal | fast_apply K | cont1 tt | try apply refl_rel_incl' ]
| false => eapply local_frame_htop; [ xlocal | fast_apply K | cont1 tt | cont2 tt ]
end).
......
......@@ -127,7 +127,7 @@ Proof using. intros. auto. Qed.
Lemma hsingle_eq_fun_hfield :
hsingle = (fun l v => (l`.`(0%nat) ~~~> v)).
Proof using.
intros. applys func_ext_2. intros. unfold hfield. fequals.
intros. applys fun_ext_2. intros. unfold hfield. fequals.
Transparent loc. unfold loc. math.
Qed.
......@@ -498,7 +498,7 @@ Lemma Hfield_not_null : forall l f `{EA:Enc A} (V:A),
(l`.`f ~> V) ==> (l`.`f ~> V) \* \[l <> null].
Proof using. intros. applys~ hfield_not_null. Qed.
Implicit Arguments Hfield_not_null [].
Arguments Hfield_not_null : clear implicits.
Definition Hsingle `{EA:Enc A} (l:loc) (V:A) :=
hsingle l (enc V).
......@@ -651,7 +651,7 @@ Open Scope charac.
Definition tag_cf (F:Formula) A `{EA:Enc A} := F A EA.
Implicit Arguments tag_cf [A [EA]].
Arguments tag_cf [A] {EA}.
(*
Notation "'PRE' H 'POST' Q 'CODE' F" :=
......@@ -981,11 +981,11 @@ Ltac hsimpl_remove_head_units tt :=
(* xapp_basic_prepare tt. xapplys Spec_eq_int. *)
(*
forwards_nounfold_then G ltac:(fun K =>
eapply local_frame; [ xlocal | eapply K | hcancel | try apply rel_le_refl ]).
eapply local_frame; [ xlocal | eapply K | hcancel | try apply refl_rel_incl' ]).
forwards_nounfold_then G ltac:(fun K => instantiate;
eapply local_frame; [ xlocal | sapply K | hcancel | try apply rel_le_refl ]).
eapply local_frame; [ xlocal | sapply K | hcancel | try apply refl_rel_incl' ]).
forwards_nounfold_then G ltac:(fun K => pose (X:=K)).
eapply local_frame; [ xlocal | sapply X | hcancel | try apply rel_le_refl ].
eapply local_frame; [ xlocal | sapply X | hcancel | try apply refl_rel_incl' ].
*)
......@@ -1046,15 +1046,15 @@ Ltac xcf_reveal_fun tt :=
xapp_basic_prepare tt. (* xapply @Spec_get. hsimpl.*)
forwards_nounfold_then Spec_get ltac:(fun K =>
eapply local_frame; [ xlocal | eapply K | hcancel | try apply rel_le_refl ]).
eapply local_frame; [ xlocal | eapply K | hcancel | try apply refl_rel_incl' ]).
*)
(* Try in 8.6 to use [notypeclasses refine]
forwards_nounfold_then Spec_get ltac:(fun K =>
eapply local_frame; [ xlocal | notypeclasses refine @K | hcancel | try apply rel_le_refl ]).
eapply local_frame; [ xlocal | notypeclasses refine @K | hcancel | try apply refl_rel_incl' ]).
*)
eapply local_frame; [ xlocal | fast_apply Spec_get | hcancel | try apply rel_le_refl ].
eapply local_frame; [ xlocal | fast_apply Spec_get | hcancel | try apply refl_rel_incl' ].
eapply local_frame.
skip. eapply @Spec_get. hsimpl. hsimpl.
......@@ -1306,9 +1306,9 @@ Proof using. intros. applys~ Rule_set. Qed.
End SpecBasic.
Implicit Arguments Spec_ref [].
Implicit Arguments Spec_get [].
Implicit Arguments Spec_set [].
Arguments Spec_ref : clear implicits.
Arguments Spec_get : clear implicits.
Arguments Spec_set : clear implicits.
Hint Extern 1 (RegisterSpec (val_prim val_ref)) =>
Provide Spec_ref.
......@@ -1935,16 +1935,16 @@ Notation "``[ x1 , x2 , x3 , x4 ]" :=
xspec ;=> G; xapp_basic_prepare tt. xapply G.
forwards_nounfold_then G ltac:(fun K =>
eapply local_frame; [ xlocal | eapply K | hcancel | try apply rel_le_refl ]).
eapply local_frame; [ xlocal | eapply K | hcancel | try apply refl_rel_incl' ]).
(* Problematic backtracking going on *)
(* TODO: why slow?*)
forwards_nounfold_then G ltac:(fun K => instantiate;
eapply local_frame; [ xlocal | sapply K | hcancel | try apply rel_le_refl ]).
eapply local_frame; [ xlocal | sapply K | hcancel | try apply refl_rel_incl' ]).
forwards_nounfold_then G ltac:(fun K => pose (X:=K)).
eapply local_frame; [ xlocal | sapply X | hcancel | try apply rel_le_refl ].
eapply local_frame; [ xlocal | sapply X | hcancel | try apply refl_rel_incl' ].
unfolds Spec, Apps. apply s.
......@@ -1953,7 +1953,7 @@ unfolds Spec, Apps. apply s.
xapply G.
forwards_nounfold_then H ltac:(fun K =>
match xpostcondition_is_evar tt with
| true => eapply local_frame; [ xlocal | sapply K | cont1 tt | try apply rel_le_refl ]
| true => eapply local_frame; [ xlocal | sapply K | cont1 tt | try apply refl_rel_incl' ]
| false => eapply local_frame_htop; [ xlocal | sapply K | cont1 tt | cont2 tt ]
end).
......@@ -1975,7 +1975,7 @@ Lemma Triple_apps_funs_of_Cf_iter : forall n F (Vs:dyns) (vs:vals) xs t A `{EA:E
func_iter n Cf_def Cf (Substs xs Vs t) A EA H Q ->
Triple (trm_apps F vs) H Q.
Proof using.
introv EF EV N M. rewrite var_funs_exec_eq in N. rew_reflect in N.
introv EF EV N M. rewrite var_funs_exec_eq in N. rew_istrue in N.
subst. applys* Rule_apps_funs. applys* Triple_trm_of_Cf_iter.
Qed.
*)
......@@ -2103,7 +2103,7 @@ Lemma Cf_if_val_isTrue : forall (P:Prop) (F1 F2 : formula) H A (EA:Enc A) (Q:A->
(~ P -> 'F2 H Q) ->
'(Cf_if_val (enc (isTrue P)) F1 F2) H Q.
Proof using.
introv M1 M2. applys Cf_if_val_bool; intros; rew_refl in *; auto.
introv M1 M2. applys Cf_if_val_bool; intros; rew_istrue in *; auto.
Qed.
......@@ -2410,7 +2410,7 @@ Proof using.
{ rew_list in *. asserts: (vs' = nil).
{ applys length_zero_inv. math. } subst vs'. clear L.
simpls. applys~ red_app R. applys~ red_fun. }
{ rew_refl in N. destruct N as [F N']. applys~ IHxs' M.
{ rew_istrue in N. destruct N as [F N']. applys~ IHxs' M.
applys~ red_app R. applys~ red_fun.
rewrite~ subst_trm_funs. applys~ red_funs. } }
Qed.
......@@ -2431,7 +2431,7 @@ Proof using.
{ rew_list in *. asserts: (vs' = nil).
{ applys length_zero_inv. math. } subst vs'. clear L.
simpls. applys~ red_app R. applys~ red_fun. }
{ rew_refl in N. destruct N as [F N']. applys~ IHxs' M.
{ rew_istrue in N. destruct N as [F N']. applys~ IHxs' M.
applys~ red_app R. applys~ red_fun.
rewrite~ subst_trm_funs. applys~ red_funs. } }
Qed.
......@@ -2898,8 +2898,8 @@ Notation "'`Fix' F X1 ':=' F1" :=
| trm_func Norec x t1 => local (cf_fun (fun X => cf (subst x X t1)))
| trm_func (Rec f) x t1 => local (cf_fix (fun F X => cf (subst f F (subst x X t1))))
{ destruct r; fequals; fequals.
{ applys~ func_ext_1. }
{ applys~ func_ext_2. } }
{ applys~ fun_ext_1. }
{ applys~ fun_ext_2. } }
destruct r; simpl; applys sound_for_local; intros H Q P.
{ renames v to x. unfolds in P. applys rule_func_val.
hchanges~ P. intros F H' Q' HB. applys~ rule_app_fun. applys~ IH. }
......
......@@ -68,7 +68,7 @@ with trm : Type :=
(** The type of values is inhabited *)
Global Instance Inhab_val : Inhab val.
Proof using. apply (prove_Inhab val_unit). Qed.
Proof using. apply (Inhab_of_val val_unit). Qed.
(* ---------------------------------------------------------------------- *)
......@@ -169,7 +169,7 @@ Inductive red : state -> trm -> state -> val -> Prop :=
red m (val_set (val_loc l) v) m' val_unit
| red_alloc : forall k n ma mb l,
mb = fmap_conseq l k val_unit ->
n = my_Z_of_nat k ->
n = nat_to_Z k ->
l <> null ->
\# ma mb ->
red ma (val_alloc (val_int n)) (mb \+ ma) (val_loc l)
......@@ -654,7 +654,7 @@ Proof using.
{ rew_list in *. asserts: (vs' = nil).
{ applys length_zero_inv. math. } subst vs'. clear L.
simpls. applys~ red_app_arg R. applys~ red_app_fun. }
{ rew_refl in N. destruct N as [F N']. applys~ IHxs' M.
{ rew_istrue in N. destruct N as [F N']. applys~ IHxs' M.
applys~ red_app_arg R. applys~ red_app_fun.
rewrite~ subst_trm_funs. applys~ red_funs. splits~. } }
Qed.
......@@ -703,8 +703,8 @@ Lemma red_app_fixs_val : forall xs vs m1 m2 vf f t r,
Proof using.
introv E M (N&L&P). destruct xs as [|x xs']. { false. }
{ destruct vs as [|v vs']; rew_list in *. { false; math. } clear P.
simpls. case_if*. destruct N as (N1&N2&N3).
subst vf. tests C: (xs' = nil).
simpls. case_if*. rew_istrue in *. destruct N as (N1&N2&N3).
subst vf. tests C':(xs' = nil).
{ rew_list in *. asserts: (vs' = nil).
{ applys length_zero_inv. math. } subst vs'. clear L.