Commit 8267241f authored by charguer's avatar charguer

remove_hints

parent f67b5116
......@@ -63,6 +63,20 @@ Qed.
Lemma Rule_val_example_one_ref : forall n,
Triple (val_example_one_ref n)
PRE \[]
POST (fun r => \[r = n+2]).
Proof using.
xcf. xapps. xapps ;=> r. xapp~. xapp~. hsimpl. math.
Qed.
(* ---------------------------------------------------------------------- *)
(** Basic let-binding two ref *)
(** [val_example_two_ref] defined in [ExampleBasicNonlifted.v] *)
Lemma Rule_val_example_two_ref : forall n,
Triple (val_example_two_ref n)
PRE \[]
POST (fun r => \[r = n+1]).
Proof using.
......
......@@ -575,7 +575,7 @@ Proof using.
{ intros p. xpull ;=> Np. xchange~ (@Alloc_to_Record p 0%nat).
{ math_rewrite ((p+0)%nat = p). hsimpl. } (* todo simplify *)
xpull ;=> Ws LWs. fold xs. fold fs.
rewrite (@Subst_new_record_aux fs xs Vs 0%nat n n); try first [ math | auto ].
rewrite (@Subst_new_record_aux n fs xs Vs 0%nat n); try first [ math | auto ].
asserts Lxs: (length xs = n). { subst xs. rewrite~ length_var_seq. }
(*clearbody xs.*) clear HP.
applys local_weaken_post (fun p' => \[p' = p] \* p ~> Record (combine fs Vs));
......@@ -708,11 +708,13 @@ Proof using.
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.
lets (L1'&X'&L2'&E1&E2&E3&E4): map_eq_middle_inv N1. subst.
rewrite length_map. hsimpl~ L1' X' L2'.
do 2 rewrite Array_unlift. hsimpl. }
{ 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~. }
rewrite~ length_map. subst L. rew_listx~. }
Qed.
End ArrayProp.
......@@ -726,12 +728,9 @@ Lemma Rule_alloc_array : forall n,
POST (fun p => Hexists (L:list val), \[length L = n :> int] \* p ~> Array L).
Proof using.
intros. unfold Triple. xapplys~ rule_alloc_array.
intros r x L. intros E N. subst.
unfold Post. hsimpl~ L.
rewrite Array_unlift.
asserts_rewrite (@enc val _ = @id val). (* TODO: map_id extens *)
{ extens. intros v. rewrite~ enc_val_eq. }
rewrite map_id. hsimpl.
intros r x L. intros E N. subst. unfold Post. hsimpl~ L.
rewrite Array_unlift. rewrite map_id_ext. hsimpl.
{ intros v. rewrite~ enc_val_eq. }
Qed.
Import LibListZ.
......@@ -741,17 +740,19 @@ Section ArrayRules.
Context A `{EA:Enc A} `{IA:Inhab A}.
Implicit Types L : list A.
Hint Resolve index_map.
Lemma Rule_array_get : forall p i L,
index L i ->
Triple (val_array_get `p `i)
PRE (p ~> Array L)
PRE (p ~> Array L)
POST (fun (r:A) => \[r = L[i]] \* p ~> Array L).
Proof using.
intros. unfold Triple. rewrite Array_unlift.
xapplys~ rule_array_get. skip. (* todo! index_map *)
intros r E. (* todo: read_map *)
unfold Post. hsimpl.
Admitted.
xapplys~ rule_array_get. intros r E.
lets M: (@read_map A _ val) L. rewrites~ (rm M) in E. (* todo: polish *)
unfold Post. subst. hsimpl*.
Qed.
Hint Extern 1 (Register_Spec val_array_get) => Provide Rule_array_get.
......@@ -762,10 +763,10 @@ Lemma Rule_array_set : forall p i v L,
POST (fun (_:unit) => p ~> Array (L[i:=v])).
Proof using.
intros. unfold Triple. rewrite Array_unlift.
xapplys~ rule_array_set. skip. (* todo! index_map *)
intros r E. (* todo: update_map *)
unfold Post. hsimpl~.
Admitted.
xapplys~ rule_array_set. intros r E.
rewrite~ <- map_update.
unfold Post. subst. rewrite Array_unlift. hsimpl~ tt.
Qed.
Hint Extern 1 (Register_Spec val_array_set) => Provide Rule_array_set.
......@@ -775,16 +776,13 @@ Lemma Rule_array_make : forall n v,
PRE \[]
POST (fun p => Hexists L, \[L = make n v] \* p ~> Array L).
Proof using.
intros. unfold Triple.
xapplys~ rule_array_make.
intros r p L E N. (* todo: update_map *)
unfold Post. hsimpl~ p (make n v).
rewrite Array_unlift. subst L. (* todo: map_make *)
Admitted.
intros. unfold Triple. xapplys~ rule_array_make.
intros r p L E N. unfold Post. hsimpl~ p (make n v).
rewrite Array_unlift. subst L. rewrite map_make; [|math]. hsimpl.
Qed.
Hint Extern 1 (Register_Spec val_array_make) => Provide Rule_array_make.
End ArrayRules.
......@@ -815,10 +813,6 @@ End ArrayRules.
......
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