Commit 02c29695 authored by charguer's avatar charguer

axiom-free

parent 8267241f
......@@ -247,13 +247,9 @@ Proof using.
xapps~. xif ;=> C.
{ xval. subst p. rewrite MList_null_eq. hsimpl~. }
{ xchanges~ (MList_not_null_inv_cons p) ;=> x p1 T1 E. subst.
xapps. xapps. xapp~ as p1'.
(* TODO URGENT xapp.
(* todo: xapp should look for hyp *)
xapps. xapps. xapp~ as p1'. xapp. (* todo: xapp should look for hyp *)
intros p'. do 2 rewrite MList_cons_eq. hsimpl. }
Qed.
*)
Admitted.
Hint Extern 1 (Register_Spec val_mlist_copy) => Provide Rule_mlist_copy.
......
......@@ -222,15 +222,8 @@ Proof using.
{ xval. subst p. rewrite MTree_null_eq. hsimpl~. }
{ xchanges~ (MTree_not_null_inv_node p) ;=> x p1 p2 T1 T2 E. subst.
xapps. xapps. xapps. xapp~ IH as p1'. xapp~ IH as p2'.
(* TODO URGENT: requires fixing records
xapp.
(* todo: xapp should look for hyp *)
intros p'. do 2 rewrite MTree_node_eq. hsimpl. }
xapp. intros p'. do 2 rewrite MTree_node_eq. hsimpl. }
Qed.
*)
Admitted.
(* ********************************************************************** *)
......
......@@ -772,14 +772,10 @@ Proof using.
xapps~. xif ;=> C.
{ xval. subst p. rewrite MList_null_eq. hsimpl~. }
{ xchanges~ (MList_not_null_inv_cons p) ;=> x p1 T1 E. subst.
xapps. xapps. xapp~ as p1'.
(* TODO URGENT xapp.
(* todo: xapp should look for hyp *)
xapps. xapps. xapp~ as p1'. xapp.
intros p'. do 2 rewrite MList_cons_eq. hsimpl. }
(* /SOLUTION *)
Qed.
*)
Admitted.
(***********************************************************************)
......
......@@ -31,7 +31,7 @@ Ltac auto_star ::= jauto.
(** A formula is a binary relation relating a pre-condition
and a post-condition. *)
Definition Formula := forall `{Enc A}, hprop -> (A -> hprop) -> Prop.
Definition Formula := forall A `{Enc A}, hprop -> (A -> hprop) -> Prop.
Global Instance Inhab_Formula : Inhab Formula.
Proof using. apply (Inhab_of_val (fun _ _ _ _ => True)). Qed.
......
......@@ -333,7 +333,7 @@ Qed.
(* ---------------------------------------------------------------------- *)
(* ** Lifting of postconditions *)
Definition Post `{Enc A} (Q:A->hprop) : val->hprop :=
Definition Post A `{Enc A} (Q:A->hprop) : val->hprop :=
fun v => Hexists V, \[v = enc V] \* Q V.
Lemma Post_himpl : forall `{Enc A} Q Q',
......@@ -359,7 +359,7 @@ Local Hint Resolve Post_himpl.
(** Singleton *)
Definition Hsingle `{EA:Enc A} (V:A) (l:loc) :=
Definition Hsingle `{EA:Enc A} (V:A) (l:loc) : hprop :=
hsingle l (enc V).
Notation "l '~~>' v" := (l ~> Hsingle v)
......
......@@ -398,32 +398,6 @@ Ltac xspec_base tt ::=
end.
(* ---------------------------------------------------------------------- *)
(* ** *)
(* TODO :move *)
(** [nat_seq i n] generates a list of variables [x1;x2;..;xn]
with [x1=i] and [xn=i+n-1]. Such lists are useful for
generic programming. *)
(* TODO: move to LibNat *)
Fixpoint nat_seq (start:nat) (nb:nat) :=
match nb with
| O => nil
| S nb' => start :: nat_seq (S start) nb'
end.
Lemma length_nat_seq : forall start nb,
length (nat_seq start nb) = nb.
Proof using.
intros. gen start. induction nb; simpl; intros.
{ auto. } { rew_list. rewrite~ IHnb. }
Qed.
(* ---------------------------------------------------------------------- *)
(* ** Conversion between allocated segments and record representation *)
......@@ -558,17 +532,17 @@ Lemma Rule_new_record : forall (n:nat) (Vs:dyns),
(n > 0)%nat ->
n = length Vs ->
let fs := nat_seq 0%nat n in
let xs := var_seq 0%nat n in
Triple (trm_apps (val_new_record n) (encs Vs))
PRE \[]
POST (fun p => p ~> Record (combine fs Vs)).
Proof using.
introv HP LVs. intros fs xs. applys Rule_apps_funs.
introv HP LVs. intros fs. applys Rule_apps_funs.
{ reflexivity. }
{ subst. applys~ var_funs_var_seq. }
{ asserts EL: (length Vs = length xs). { unfold xs. rewrite~ length_var_seq. }
{ set (xs := var_seq 0 n).
asserts EL: (length Vs = length xs). { unfold xs. rewrite~ length_var_seq. }
rewrite Substs_let; [| applys var_fresh_var_seq_ge; math | auto ].
asserts_rewrite (Substs (var_seq 0 n) Vs (val_alloc n) = val_alloc n).
asserts_rewrite (Substs xs Vs (val_alloc n) = val_alloc n).
{ rewrite~ Substs_app. rewrite~ Substs_val. do 2 rewrite~ Substs_val. }
eapply (@Rule_let _ _ _ _ _ _ _ loc). (* todo: cleanup *)
{ xapplys Rule_alloc_nat. }
......@@ -600,25 +574,11 @@ Proof using.
{ intros p'. rewrite Record_cons. hsimpl~. } } } } }
Qed.
(*
Parameter val_new_record : nat -> val.
Parameter Rule_new_record : forall (n:nat) (Vs:dyns),
(n > 0)%nat ->
n = length Vs ->
let xs := nat_seq 0%nat n in
Triple (trm_apps (val_new_record n) (encs Vs))
PRE \[]
POST (fun p => p ~> Record (combine xs Vs)).
*)
Lemma Rule_new_record' : forall (n:nat) (Vs:dyns) (vs:vals) (Q:loc->hprop),
vs = (encs Vs) ->
(n = List.length Vs)%nat ->
(n > 0)%nat ->
let fs := nat_seq 0%nat n in
let xs := var_seq 0%nat n in
((fun p => p ~> Record (List.combine fs Vs)) ===> Q) ->
Triple (trm_apps (val_new_record n) (vals_to_trms vs)) \[] Q.
Proof using.
......@@ -693,9 +653,6 @@ Lemma Array_last_eq : forall p x L,
p ~> Array (L&x) = p ~> Array L \* ((p + length L)%nat ~~> x).
Proof using. intros. rewrite Array_concat_eq. rewrite~ Array_one_eq. Qed.
(* TODO URGENT: complete proofs below *)
Transparent loc. (* TODO: avoid the need for this by
using pointer arithmetic operator for p+n *)
......
......@@ -61,6 +61,23 @@ Hint Rewrite nat_zero_plus nat_plus_zero nat_plus_succ
nat_minus_same nat_plus_minus_same : rew_nat.
(** [nat_seq i n] generates a list of variables [x1;x2;..;xn]
with [x1=i] and [xn=i+n-1]. Such lists are useful for
generic programming. *)
Fixpoint nat_seq (start:nat) (nb:nat) :=
match nb with
| O => nil
| S nb' => start :: nat_seq (S start) nb'
end.
Lemma length_nat_seq : forall start nb,
length (nat_seq start nb) = nb.
Proof using.
intros. gen start. induction nb; simpl; intros.
{ auto. } { rew_list. rewrite~ IHnb. }
Qed.
(*----------------------*)
......
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