Commit a375c221 authored by charguer's avatar charguer

porting2

parent 7383a08b
......@@ -2,7 +2,7 @@ Set Implicit Arguments.
Require Import LibCore LibEpsilon Shared.
Require Import CFHeaps.
Hint Extern 1 (_ ===> _) => apply rel_le_refl.
Hint Extern 1 (_ ===> _) => apply refl_rel_incl'.
(* TODO: make this a local hint? xauto should take care of this. *)
......@@ -88,7 +88,7 @@ Proof using.
intros. rew_disjoint*.
asserts Hint3: (forall h1 h2 h3, \# h1 h2 -> \# h2 h3 -> \# h1 h3 -> \# h1 h2 h3) .
intros. rew_disjoint*.
intros. extens. intros H Q. iff M. apply~ local_erase.
intros. hnf. extens. intros H Q. iff M. apply~ local_erase.
introv Dhi Hh. destruct (M h Hh) as (H1&H2&Q'&D12&N&HQ).
destruct D12 as (h1&h2&?&?&?&?).
destruct~ (N h1 (heap_union i h2)) as (v'&h1'&i'&?&HQ'&E).
......@@ -202,7 +202,7 @@ Lemma app_ge_2_unfold_extens :
= (fun H Q => app_basic f x H
(fun g => Hexists H', H' \* \[ app_def g xs H' Q])).
Proof using.
introv N. applys func_ext_2. intros H Q. rewrite~ app_ge_2_unfold.
introv N. applys fun_ext_2. intros H Q. rewrite~ app_ge_2_unfold.
Qed.
(** Weaken-frame-gc for [app] -- auxiliary lemma for [app_local]. *)
......@@ -328,8 +328,8 @@ Proof using.
rew_list. simpl. destruct ys. rew_list in *. math. auto.
sets_eq xs': (d :: xs). do 2 (rewrite app_ge_2_unfold;
[ | subst; rew_list; auto_false ]).
fequal. apply func_ext_1. intros g.
apply func_equal_1. auto. apply func_ext_1. intros H'.
fequal. apply fun_ext_1. intros g.
apply args_eq_1. auto. apply fun_ext_1. intros H'.
fequal. fequal. apply IHxs. subst. rew_list. math. math.
Qed.
......@@ -341,13 +341,14 @@ Lemma app_over_take : forall n xs f B H (Q:B->hprop),
= app f (take n xs) H (fun g => Hexists H', H' \*
\[ app g (drop n xs) H' Q ]).
Proof using.
introv N.
forwards* (M&E1&E2): take_and_drop n xs. math.
introv N.
forwards* (M&E1&E2): take_app_drop_spec n xs. math.
set (xs' := xs) at 1. change xs with xs' in M. rewrite M.
subst xs'. rewrite app_over_app; try math. auto.
Qed.
(********************************************************************)
(* ** Lemma for partial-applications *)
......@@ -584,8 +585,8 @@ Proof using.
destruct do as [[T v]|]; inverts M.
induction L as [|[f' [D' d']] T']; [false|].
simpl in E.
intros r. do 2 xunfold record_repr at 1. simpl. case_if.
{ inverts E.
intros r. do 2 xunfold record_repr at 1. simpl. case_if in E. (* todo: fix cases_if *)
{ subst. inverts E.
eapply local_frame.
{ apply app_local. auto_false. }
{ apply record_get_spec. }
......@@ -627,8 +628,8 @@ Proof using.
destruct do as [L'|]; inverts M.
gen L'. induction L as [|[f' [T' v']] T]; intros; [false|].
simpl in E.
xunfold record_repr at 1. simpl. case_if.
{ inverts E.
xunfold record_repr at 1. simpl. case_if. (* todo: fix cases_if *)
{ subst. inverts E.
eapply local_frame.
{ apply app_local. auto_false. }
{ apply record_set_spec. }
......
......@@ -2277,7 +2277,7 @@ Ltac hchange_forwards L modif cont1 cont2 :=
match modif with
| __ =>
match type of K with
| _ = _ => hchange_apply (@pred_le_proj1 _ _ _ K) cont1 cont2
| _ = _ => hchange_apply (@pred_incl_proj1 _ _ _ K) cont1 cont2
| _ => hchange_apply K cont1 cont2
end
| _ => hchange_apply (@modif _ _ _ K) cont1 cont2
......@@ -2301,9 +2301,9 @@ Ltac hchange_debug_base E modif :=
Tactic Notation "hchange_debug" constr(E) :=
hchange_debug_base E __.
Tactic Notation "hchange_debug" "->" constr(E) :=
hchange_debug_base E pred_le_proj1.
hchange_debug_base E pred_incl_proj1.
Tactic Notation "hchange_debug" "<-" constr(E) :=
hchange_debug_base pred_le_proj2.
hchange_debug_base pred_incl_proj2.
Ltac hchange_base E modif :=
hchange_core E modif ltac:(hcancel_cont) ltac:(idcont).
......@@ -2311,9 +2311,9 @@ Ltac hchange_base E modif :=
Tactic Notation "hchange" constr(E) :=
hchange_base E __.
Tactic Notation "hchange" "->" constr(E) :=
hchange_base E pred_le_proj1.
hchange_base E pred_incl_proj1.
Tactic Notation "hchange" "<-" constr(E) :=
hchange_base E pred_le_proj2.
hchange_base E pred_incl_proj2.
Tactic Notation "hchange" "~" constr(E) :=
hchange E; auto_tilde.
......@@ -2326,9 +2326,9 @@ Ltac hchanges_base E modif :=
Tactic Notation "hchanges" constr(E) :=
hchanges_base E __.
Tactic Notation "hchanges" "->" constr(E) :=
hchanges_base E pred_le_proj1.
hchanges_base E pred_incl_proj1.
Tactic Notation "hchange" "<-" constr(E) :=
hchanges_base E pred_le_proj2.
hchanges_base E pred_incl_proj2.
Tactic Notation "hchanges" "~" constr(E) :=
hchanges E; auto_tilde.
......
......@@ -47,7 +47,7 @@ Inductive tag_type : Type :=
Definition tag (t:tag_type) (A:Type) (P:A) := P.
Implicit Arguments tag [A].
Arguments tag t [A].
(** [xtag_add T] adds the tag [T] to the head of the goal *)
......@@ -633,7 +633,8 @@ Notation "'Funs' f1 ':=' K1 'and' f2 ':=' K2 'and' f3 ':=' K3 'in' F" :=
Definition cf_let (A B : Type) (F1:~~A) (F2:A->~~B) : ~~ B :=
(fun H Q => exists Q1, F1 H Q1 /\ forall x, F2 x (Q1 x) Q).
Implicit Arguments cf_let [A B].
Arguments cf_let [A] [B].
Notation "'Let' x ':=' F1 'in' F2" :=
(!Let (cf_let F1 (fun x => F2)))
......@@ -852,46 +853,46 @@ Notation "'Case' x '=' p [ x1 x2 x3 x4 x5 x6 x7 ] 'Then' F1 'Else' F2" :=
Notation "'Case' x '=' p 'When' w 'Then' F1 'Else' F2" :=
(!CaseWhen (fun H Q => (x = p -> istrue (w)%bool -> F1 H Q)
/\ (x <> p \/ istrue (!w) -> F2 H Q)))
/\ (x <> p \/ istrue (!w%bool) -> F2 H Q)))
(at level 69, x at level 0) : charac.
Notation "'Case' x '=' p [ x1 ] 'When' w 'Then' F1 'Else' F2" :=
(!CaseWhen (fun H Q => (forall x1, x = p -> istrue w%bool -> F1 H Q)
/\ ((forall x1, x <> p \/ istrue (!w)) -> F2 H Q)))
/\ ((forall x1, x <> p \/ istrue (!w%bool)) -> F2 H Q)))
(at level 69, x at level 0, x1 ident) : charac.
Notation "'Case' x '=' p [ x1 x2 ] 'When' w 'Then' F1 'Else' F2" :=
(!CaseWhen (fun H Q => (forall x1 x2, x = p -> istrue w%bool -> F1 H Q)
/\ ((forall x1 x2, x <> p \/ istrue (!w)) -> F2 H Q)))
/\ ((forall x1 x2, x <> p \/ istrue (!w%bool)) -> F2 H Q)))
(at level 69, x at level 0, x1 ident, x2 ident) : charac.
Notation "'Case' x '=' p [ x1 x2 x3 ] 'When' w 'Then' F1 'Else' F2" :=
(!CaseWhen (fun H Q => (forall x1 x2 x3, x = p -> istrue w%bool -> F1 H Q)
/\ ((forall x1 x2 x3, x <> p \/ istrue (!w)) -> F2 H Q)))
/\ ((forall x1 x2 x3, x <> p \/ istrue (!w%bool)) -> F2 H Q)))
(at level 69, x at level 0, x1 ident, x2 ident,
x3 ident) : charac.
Notation "'Case' x '=' p [ x1 x2 x3 x4 ] 'When' w 'Then' F1 'Else' F2" :=
(!CaseWhen (fun H Q => (forall x1 x2 x3 x4, x = p -> istrue w%bool -> F1 H Q)
/\ ((forall x1 x2 x3 x4, x <> p \/ istrue (!w)) -> F2 H Q)))
/\ ((forall x1 x2 x3 x4, x <> p \/ istrue (!w%bool)) -> F2 H Q)))
(at level 69, x at level 0, x1 ident, x2 ident,
x3 ident, x4 ident) : charac.
Notation "'Case' x '=' p [ x1 x2 x3 x4 x5 ] 'When' w 'Then' F1 'Else' F2" :=
(!CaseWhen (fun H Q => (forall x1 x2 x3 x4 x5, x = p -> istrue w%bool -> F1 H Q)
/\ ((forall x1 x2 x3 x4 x5, x <> p \/ istrue (!w)) -> F2 H Q)))
/\ ((forall x1 x2 x3 x4 x5, x <> p \/ istrue (!w%bool)) -> F2 H Q)))
(at level 69, x at level 0, x1 ident, x2 ident,
x3 ident, x4 ident, x5 ident) : charac.
Notation "'Case' x '=' p [ x1 x2 x3 x4 x5 x6 ] 'When' w 'Then' F1 'Else' F2" :=
(!CaseWhen (fun H Q => (forall x1 x2 x3 x4 x5 x6, x = p -> istrue w%bool -> F1 H Q)
/\ ((forall x1 x2 x3 x4 x5 x6, x <> p \/ istrue (!w)) -> F2 H Q)))
/\ ((forall x1 x2 x3 x4 x5 x6, x <> p \/ istrue (!w%bool)) -> F2 H Q)))
(at level 69, x at level 0, x1 ident, x2 ident,
x3 ident, x4 ident, x5 ident, x6 ident) : charac.
Notation "'Case' x '=' p [ x1 x2 x3 x4 x5 x6 x7 ] 'When' w 'Then' F1 'Else' F2" :=
(!CaseWhen (fun H Q => (forall x1 x2 x3 x4 x5 x6 x7, x = p -> istrue w%bool -> F1 H Q)
/\ ((forall x1 x2 x3 x4 x5 x6 x7, x <> p \/ istrue (!w)) -> F2 H Q)))
/\ ((forall x1 x2 x3 x4 x5 x6 x7, x <> p \/ istrue (!w%bool)) -> F2 H Q)))
(at level 69, x at level 0, x1 ident, x2 ident,
x3 ident, x4 ident, x5 ident, x6 ident, x7 ident) : charac.
......
......@@ -210,7 +210,7 @@ Tactic Notation "xclean" :=
*)
Ltac xok_core cont := (* see [xok] spec further *)
solve [ hnf; apply rel_incl_refl
solve [ hnf; apply refl_rel_incl'
| apply pred_incl_refl
| apply hsimpl_to_qunit; reflexivity
| hsimpl; cont tt ].
......@@ -396,7 +396,7 @@ Ltac xpost_core Q :=
| _ => constr:(Q)
end in
match cfml_postcondition_is_evar tt with
| true => apply (@fix_post _ Q'); [ try xlocal | xtag_pre_post | apply rel_incl_refl ]
| true => apply (@fix_post _ Q'); [ try xlocal | xtag_pre_post | apply refl_rel_incl' ]
| false => apply (@fix_post _ Q'); [ try xlocal | xtag_pre_post | ]
end.
......@@ -1814,13 +1814,13 @@ Tactic Notation "xassert" :=
Ltac xif_post H := (* todo: cleanup *)
calc_partial_eq tt;
try fold_bool; fold_prop;
try rew_isTrue in H; (* try fold_bool; fold_prop; TODO: check change*)
try fix_bool_of_known tt;
try solve [ discriminate | false; congruence ];
first [ subst_hyp H; try fold_bool
first [ subst_hyp H; try rew_isTrue in H (* TODO: try fold_bool *)
| idtac ];
try fix_bool_of_known tt;
try (check_noevar_hyp H; rew_reflect in H; rew_logic in H).
try (check_noevar_hyp H; rew_istrue in H; rew_logic in H).
(* DEPRECATED
......@@ -2185,7 +2185,7 @@ Lemma xwhile_inv_basic_measure_lemma :
(forall m, F2 (I true m) (# Hexists b m', \[0 <= m' < m] \* I b m')) ->
(While F1 Do F2 Done_) H (# Hexists m, I false m).
Proof using.
introv HH HF1 HF2. applys~ xwhile_inv_basic_lemma I (int_downto_wf 0).
introv HH HF1 HF2. applys~ xwhile_inv_basic_lemma I (wf_downto 0).
Qed.
(* for cheaters *)
......
......@@ -379,21 +379,21 @@ Hint Resolve refl_rel_incl'.
Open Scope func.
Lemma pred_le_extens : forall A (H1 H2 : A->Prop),
Lemma pred_incl_extens : forall A (H1 H2 : A->Prop),
H1 ==> H2 -> H2 ==> H1 -> H1 = H2.
Proof. intros. extens*. Qed.
Lemma pred_le_proj1 : forall A (H1 H2 : A->Prop),
Lemma pred_incl_proj1 : forall A (H1 H2 : A->Prop),
H1 = H2 -> H1 ==> H2.
Proof. intros. subst~. Qed.
Lemma pred_le_proj2 : forall A (H1 H2 : A->Prop),
Lemma pred_incl_proj2 : forall A (H1 H2 : A->Prop),
H1 = H2 -> H2 ==> H1.
Proof. intros. subst~. Qed.
Arguments pred_le_proj1 [A] [H1] [H2].
Arguments pred_le_proj2 [A] [H1] [H2].
Arguments pred_le_extens [A] [H1] [H2].
Arguments pred_incl_proj1 [A] [H1] [H2].
Arguments pred_incl_proj2 [A] [H1] [H2].
Arguments pred_incl_extens [A] [H1] [H2].
(********************************************************************)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment