Commit 33801ca2 authored by charguer's avatar charguer

fixes

parent 1cd8e4ea
......@@ -23,7 +23,7 @@ Implicit Types n : int.
(* ---------------------------------------------------------------------- *)
(** Swap function *)
(** [val_swap] defined in [ExampleBasicNonLifted.v] *)
(** [val_swap] defined in [ExampleBasicNonlifted.v] *)
Lemma Rule_swap_neq : forall A1 A2 `{EA1:Enc A1} `{EA2:Enc A2} (v:A1) (w:A2) p q,
Triple (val_swap `p `q)
......@@ -45,7 +45,7 @@ Qed.
(* ---------------------------------------------------------------------- *)
(** Basic two references *)
(** [val_example_let] defined in [ExampleBasicNonLifted.v] *)
(** [val_example_let] defined in [ExampleBasicNonlifted.v] *)
Lemma Rule_val_example_let : forall n,
Triple (val_example_let n)
......@@ -59,10 +59,10 @@ Qed.
(* ---------------------------------------------------------------------- *)
(** Basic let-binding example *)
(** [val_example_ref] defined in [ExampleBasicNonLifted.v] *)
(** [val_example_one_ref] defined in [ExampleBasicNonlifted.v] *)
Lemma Rule_val_example_ref : forall n,
Triple (val_example_ref n)
Lemma Rule_val_example_one_ref : forall n,
Triple (val_example_one_ref n)
PRE \[]
POST (fun r => \[r = n+1]).
Proof using.
......
......@@ -420,8 +420,7 @@ Lemma rule_mlist_length_1 : forall L p,
(MList L p)
(fun r => \[r = val_int (length L)] \* MList L p).
Proof using.
intros L. induction_wf: list_sub_wf L. xcf.
(* TODO URGENT: will be removed soon *) fold val_mlist_length.
intros L. induction_wf: list_sub_wf L. xcf.
xapps. xif ;=> C.
{ xchanges~ (MList_not_null_inv_cons p) ;=> x p' L' EL. subst L.
xapps. xapps~ (IH L').
......
......@@ -107,6 +107,16 @@ Relevant files:
(***********************************************************************)
(** Demo: [hsimpl] *)
(**
H1 \* (r ~~~> n) \* H2 \* H3 ==> H4 \* H5 \* (r ~~~> n) \* H6
(r ~~~> 3) \* (s ~~~> 4) ==> Hexists n, (r ~~~> n) \* (s ~~~> (n+1))
(Hexists n, r ~~~> n \* \[n > 0]) ==> (Hexists m, r ~~~> (m+1) \* \[m >= 0])
*)
(***********************************************************************)
(** Demo: verification of [incr] *)
......@@ -364,7 +374,6 @@ Lemma rule_mlist_length_1 : forall L p,
(fun r => \[r = val_int (length L)] \* MList L p).
Proof using.
intros L. induction_wf: list_sub_wf L. xcf.
(* TODO URGENT: will be removed soon *) fold val_mlist_length.
xapps. xif ;=> C.
{ xchanges~ (MList_not_null_inv_cons p) ;=> x p' L' EL. subst L.
xapps. xapps~ (IH L').
......@@ -730,7 +739,6 @@ Qed.
(** Demo: new cell *)
Definition val_new_cell : val := val_new_record 2%nat.
Lemma Rule_new_cell : forall `{EA:Enc A} (x:A) (q:loc),
Triple (val_new_cell `x `q)
PRE \[]
......
......@@ -477,29 +477,39 @@ Ltac xcf_reveal_fun tt :=
first [ unfold f
| match goal with H: f = _ |- _ => rewrite H end ]).
(* TODO: reimplement using LambdaCFLifted strategy *)
Ltac xcf_post tt :=
simpl.
Ltac xcf_prepare tt :=
intros;
rew_nary;
Ltac xcf_trm n :=
applys triple_trm_of_cf_iter n; [ xcf_post tt ].
Ltac xcf_basic_fun n f' :=
let f := xcf_get_fun tt in
match f with
| val_funs _ _ => (* TODO: use (apply (@..)) instead of applys? same in cflifted *)
applys triple_apps_funs_of_cf_iter n;
[ reflexivity | reflexivity | xcf_post tt ]
| val_fixs _ _ _ =>
applys triple_apps_fixs_of_cf_iter n f';
[ try unfold f'; rew_nary; try reflexivity (* TODO: how in LambdaCF? *)
(* reflexivity *)
| reflexivity
| xcf_post tt ]
end.
Ltac xcf_prepare_args tt :=
rew_nary.
Ltac xcf_fun n :=
xcf_prepare_args tt;
let f' := xcf_get_fun tt in
xcf_reveal_fun tt;
rew_nary;
rew_vals_to_trms.
Ltac xcf_post tt :=
simpl.
rew_vals_to_trms;
xcf_basic_fun n f'.
Ltac xcf_core n :=
xcf_prepare tt;
match goal with |- triple ?t _ _ =>
match t with
| trm_apps (trm_val (val_funs _ _)) _ =>
applys triple_apps_funs_of_cf_iter n; [ reflexivity | reflexivity | xcf_post tt ]
| trm_apps (trm_val (val_fixs _ _ _)) _ =>
applys triple_apps_fixs_of_cf_iter n; [ reflexivity | reflexivity | xcf_post tt ]
| _ =>
applys triple_trm_of_cf_iter n; [ xcf_post tt ]
end end.
intros; first [ xcf_fun n | xcf_trm n ].
Tactic Notation "xcf" :=
xcf_core 100%nat.
......@@ -508,6 +518,7 @@ Tactic Notation "xcf_depth" constr(depth) :=
xcf_core depth.
(* ---------------------------------------------------------------------- *)
(* ** Tactic [xseq] *)
......
......@@ -566,15 +566,13 @@ Ltac xcf_get_fun_from_goal tt ::=
Ltac xcf_post tt ::=
simpl; rew_enc_dyn.
(** TODO URGENT: follow similar strategy to avoid the need to fold in LambdaCF *)
Ltac xcf_trm n :=
Ltac xcf_trm n ::=
applys Triple_trm_of_Cf_iter n; [ xcf_post tt ].
Ltac xcf_basic_fun n f' :=
Ltac xcf_basic_fun n f' ::=
let f := xcf_get_fun tt in
match f with
| val_funs _ _ =>
| val_funs _ _ =>
applys Triple_apps_funs_of_Cf_iter n;
[ reflexivity | try xeq_encs | reflexivity | xcf_post tt ]
| val_fixs _ _ _ =>
......@@ -582,17 +580,9 @@ Ltac xcf_basic_fun n f' :=
[ reflexivity | try xeq_encs | reflexivity | xcf_post tt ]
end.
Ltac xcf_fun n :=
Ltac xcf_prepare_args tt ::=
rew_nary;
try xdecode_args tt;
let f' := xcf_get_fun tt in
xcf_reveal_fun tt;
rew_nary;
rew_vals_to_trms;
xcf_basic_fun n f'.
Ltac xcf_core n ::=
intros; first [ xcf_fun n | xcf_trm n ].
try xdecode_args tt.
(*--------------------------------------------------------*)
......
......@@ -725,7 +725,7 @@ Lemma Rule_sub : forall n1 n2,
(fun n => \[n = n1 - n2]).
Proof using. intros. unfold Triple, Post. xapplys~ rule_sub. Qed.
(* TODO URGENT: add other primitives *)
(* TODO: add other arithmetic primitives *)
Lemma Rule_ptr_add : forall (l:loc) (n:int),
(l:nat) + n >= 0 ->
......
......@@ -613,19 +613,12 @@ Fixpoint Array A `{EA:Enc A} (L:list A) (p:loc) : hprop :=
| x::L' => (p ~~> x) \* (Array L' (S p))
end.
(* TODO: move *)
Lemma repr_eq : forall (A:Type) (S:A->hprop) (x:A),
(x ~> S) = S x.
Proof using. auto. Qed.
Section ArrayProp.
Context A `{EA:Enc A}.
Implicit Types L : list A.
Implicit Types x : A.
Lemma Array_eq_NonLiftedArray : forall L p,
Lemma Array_eq_ArrayNonlifted : forall L p,
Array L p = LambdaStruct.Array (LibList.map enc L) p.
Proof using.
intros L. induction L; intros.
......@@ -635,9 +628,7 @@ Qed.
Lemma Array_unlift : forall L p,
p ~> Array L = LambdaStruct.Array (LibList.map enc L) p.
Proof using. apply Array_eq_NonLiftedArray. Qed.
(* TODO: better exploit factorization with LambdaStruct using lemma above? *)
Proof using. apply Array_eq_ArrayNonlifted. Qed.
Lemma Array_nil_eq : forall p,
p ~> Array (@nil A) = \[].
......@@ -656,47 +647,38 @@ Lemma Array_concat_eq : forall p L1 L2,
Proof using.
intros. repeat rewrite Array_unlift. rew_listx. rewrite Array_concat_eq.
rewrite length_map. auto. (* TODO: add to rew_listx. *)
(*
Transparent loc.
intros. gen p. induction L1; intros; rew_list.
{ rewrite Array_nil_eq. rew_heap. fequals. unfold loc; math. }
{ do 2 rewrite Array_cons_eq. rewrite IHL1. rew_heap. do 3 fequals.
unfold loc; math. }
*)
Qed.
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.
Transparent loc. (* TODO: avoid this using pointer arithmetic operator for p+n *)
Lemma Array_middle_eq' : forall n p L,
(* TODO URGENT: complete proofs below *)
Transparent loc. (* TODO: avoid the need for this by
using pointer arithmetic operator for p+n *)
Lemma Array_middle_eq : forall n p L,
0 <= n < length L ->
(p ~> Array L) = Hexists L1 x L2, \[L = L1++x::L2] \* \[length L1 = n :> int] \*
p ~> Array L1 \* (abs(p+n) ~~> x) \* (p + length L1 + 1)%nat ~> Array L2.
Proof using.
(* TODO: reuse proof from LambdaStruct *)
(*
introv N. applys himpl_antisym.
{ forwards (L1&x&L2&E&HM): list_middle_inv (abs n) L.
asserts (N1&N2): (0 <= abs n /\ (abs n < length L)%Z).
{ split; rewrite abs_nonneg; math. } math.
lets M': eq_int_of_eq_nat HM. rewrite abs_nonneg in M'; [|math].
hsimpl~ (>> L1 x L2). subst L. rewrite Array_concat_eq, Array_cons_eq.
rew_nat. hsimpl. rewrite HM. rewrite~ abs_nat_plus_nonneg. math. }
{ hpull ;=> L1 x L2 HM E. subst n.
subst L. rewrite Array_concat_eq, Array_cons_eq.
rew_nat. hsimpl. applys_eq himpl_refl 1. fequals.
rewrite abs_nat_plus_nonneg; [|math]. rewrite~ abs_nat. }
*)
skip.
intros. repeat rewrite Array_unlift.
rewrites (>> Array_middle_eq n p (map enc L)).
rewrite length_map. auto. (* TODO: add to rew_listx. *)
apply himpl_antisym.
{ hpull ;=> L1 x L2 N1 N2. admit. (* TODO inversion lemma for map *) }
{ hpull ;=> L1 x L2 N1 N2. hsimpl (map enc L1) (enc x) (map enc L2).
repeat rewrite Array_unlift. rewrite length_map. (* todo rew_list *) hsimpl.
rewrite~ length_map.
subst L. rew_listx~. }
Qed.
End ArrayProp.
Global Opaque Array.
Lemma Rule_alloc_array : forall n,
n >= 0 ->
Triple (val_alloc `n)
......
......@@ -14,7 +14,7 @@ COQFLAGS:=-w -notation-overridden,-implicits-in-term
# Compilation.
# Note: double space below is important for export.sh
SRC := TLCbuffer Fmap SepFunctor SepTactics LambdaSemantics LambdaSep LambdaCF LambdaStruct LambdaSepLifted LambdaCFLifted LambdaStructLifted Example ExampleBasicNonlifted ExampleListNonlifted ExampleQueueNonlifted ExampleBasic ExampleTrees ExampleUnionFind ExampleHigherOrder LambdaSepCredits LambdaCFCredits LambdaSepRO ExampleList
SRC := TLCbuffer Fmap SepFunctor SepTactics LambdaSemantics LambdaSep LambdaCF LambdaStruct LambdaSepLifted LambdaCFLifted LambdaStructLifted Example ExampleBasicNonlifted ExampleListNonlifted ExampleQueueNonlifted ExampleBasic ExampleTrees ExampleUnionFind ExampleHigherOrder LambdaSepCredits LambdaCFCredits LambdaSepRO ExampleList
# The official list of files that should be compiled by [make]
......
......@@ -505,6 +505,10 @@ Definition repr (A:Type) (S:A->hprop) (x:A) : hprop :=
Notation "x '~>' S" := (repr S x)
(at level 33, no associativity) : heap_scope.
Lemma repr_eq : forall (A:Type) (S:A->hprop) (x:A),
(x ~> S) = (S x).
Proof using. auto. Qed.
(** [x ~> Id X] holds when [x] is equal to [X] in the empty heap.
[Id] is called the identity representation predicate. *)
......
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