Commit 01378833 authored by charguer's avatar charguer

arglist

parent 92771e49
......@@ -14,6 +14,16 @@ let rec search x p =
else true
(**--------------- contest version, C --------------*)
(*
......
......@@ -199,10 +199,8 @@ Lemma search_spec :
Proof using.
xweaken search_spec_ind. simpl. introv M S1. intros.
xchange (@focus_Stree x2). xextract as T1 R1.
xapply S1. eauto. hsimpl.
intros. hextracts.
hchange* (@unfocus_Stree x2).
hsimpl*.
xapply S1. eauto. hsimpl. intros. hextracts.
hchange* (@unfocus_Stree x2). hsimpl*.
Qed.
......@@ -543,7 +541,7 @@ Inductive tree :=
| tree_node : int -> tree -> tree -> tree.
(** Representation predicate form mutable trees *)
o
Fixpoint Tree (T:tree) (t:loc) : hprop :=
match T with
| tree_leaf => \[t = null]
......
......@@ -174,7 +174,7 @@ Hint Extern 1 (RegisterSpec miter) => Provide miter_spec.
Lemma mlength_spec : forall a,
Spec mlength (l:mlist a) |R>> forall A (T:A->a->hprop) (L:list A),
R (l ~> MList T L) (fun (x:_) => \[x = length L]).
(* keep *) R (l ~> MList T L) (fun (x:_) => \[x = length L]).
Proof using.
xcf. intros. xapp. xapp.
xwhile. xgeneralize (forall L (k:int) l,
......@@ -184,10 +184,13 @@ Proof using.
clear l L. intros L. induction_wf IH: (@list_sub_wf A) L; intros.
applys (rm HR). xlet. xapps. xapps. xextracts. xif.
(* case cons *)
Check MList_not_null.
(* TODO xchange (MList_not_null l) as x l' X L' EL. auto *)
xchange_debug (MList_not_null l). auto. hsimpl. xextract. intros x l' X L' EL.
xapps. xapps. xapps. xapp. subst L. xapply~ (>> IH L' l').
hsimpl. intros _. hchanges (MList_uncons l). rew_length. math.
hsimpl. intros _.
Check MList_uncons.
hchanges (MList_uncons l). rew_length. math.
(* case nil *)
subst. xchange MList_null_keep as M. subst.
xrets. rew_length. math.
......
......@@ -33,7 +33,7 @@ Axiom eval : forall A B, func -> A -> heap -> B -> heap -> Prop.
(** The primitive predicate App *)
Definition app_basic (f:func) A B (x:A) (H:hprop) (Q:B->hprop) :=
Definition app_basic (f:func) A (x:A) B (H:hprop) (Q:B->hprop) :=
forall h i, \# h i -> H h ->
exists v' h' g, \# h' g i /\ Q v' h' /\
eval f x (h \+ i) v' (h' \+ g \+ i).
......@@ -41,7 +41,7 @@ Definition app_basic (f:func) A B (x:A) (H:hprop) (Q:B->hprop) :=
(** AppReturns is a local property *)
Lemma app_basic_local : forall A B f (x:A),
is_local (@app_basic f A B x).
is_local (@app_basic f A x B).
Proof using.
(*
asserts Hint1: (forall h1 h2, \# h1 h2 -> \# h2 h1).
......@@ -92,6 +92,69 @@ Proof using. intros. applys* local_wframe. Qed.
(********************************************************************)
(* ** Generic of [app N] *)
Inductive arglist : nat -> Type :=
| arglist_nil : arglist 0
| arglist_cons : forall A (x:A) n, arglist n -> arglist (S n).
Fixpoint app (n : nat) (X : arglist n) (f:func) (B:Type) (H:hprop) (Q:B->hprop) :=
match X with
| arglist_nil => False
| arglist_cons x arglist_nil => app_basic f x H Q
| arglist_cons x xs =>
app_basic f x H
(fun g : func => Hexists H', H' \* \[ app xs g H' Q])
end.
(* [app n xs f B H Q]
: forall n, arglist n -> func -> forall B, hprop -> (B->hprop) -> Prop.
*)
(*---
Definition app
: forall n, arglist n -> func -> forall B, hprop -> (B->hprop) -> Prop.
Proof.
induction 1; intros f B H Q.
(* exact (H ==> Q f). *)
exact True.
exact (app_basic f x H (fun g => Hexists H', H' \* \[
IHX g B H' Q])).
Defined.
Print app.
Definition app
: forall n, func -> arglist n -> forall B, hprop -> (B->hprop) -> Prop.
Proof.
induction n; intros f xs B H Q.
(* exact (H ==> Q f). *)
exact True.
inversion xs.
exact (app_basic f x H (fun g => Hexists H', H' \* \[
IHn g X B H' Q])).
Defined.
Print app.
Definition app
: forall n, func -> arglist n -> forall B, hprop -> (B->hprop) -> Prop.
Proof.
induction n; intros f xs B H Q.
(* exact (H ==> Q f). *)
exact True.
inversion xs. clear n0 H1. rename X into xs'.
exact (app_basic f x H (fun g => Hexists H', H' \* \[
IHn g xs' B H' Q])).
Defined.
Print app.
*)
(*--- TODO: complete
......@@ -478,3 +541,4 @@ 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