Commit 1e009e4d authored by charguer's avatar charguer
Browse files

lists

parent aa5e34dc
......@@ -48,6 +48,7 @@ LATER
- make systematic use of || (rm -f $@; exit 1) in cfml calls
- Ltac xcf_core tt should be able to test whether Spec is a top val, and then do rewrite.
DEPRECATED?
......
......@@ -721,10 +721,6 @@ Tactic Notation "xextract" "as" simple_intropattern(I1) simple_intropattern(I2)
[xgc_post] applied to the goal [F H Q] replaces the goal
with [F H ?Q'] and [Q' ===> Q \*+ \GC], which allows to
perform garbage collection.
[xgc_post_if_not_evar] is useful for implementing other tactics;
it applies [xgc_post] only if the post-condition is instantiated;
otherwise, if the post-condition is [?Q], it does nothing.
*)
Ltac xgc_remove_core H :=
......@@ -755,14 +751,13 @@ Tactic Notation "xgc_but" constr(H) :=
Tactic Notation "xgc_post" :=
xgc_post_core.
Ltac xgc_post_if_not_evar_core tt :=
(* DEPRECATED
Ltac xgc_post_if_not_evar_then cont :=
match cfml_postcondition_is_evar tt with
| true => idtac
| false => xgc_post
| true => cont tt
| false => xgc_post; [ cont tt | ]
end.
Tactic Notation "xgc_post_if_not_evar" :=
xgc_post_if_not_evar_core tt.
*)
(* Lemma used by [xgc_all], to remove everything from the
pre-condition *)
......@@ -871,8 +866,7 @@ Tactic Notation "xframes" constr(s1) constr(s2) constr(s3) :=
Ltac xapply_core H cont1 cont2 :=
forwards_nounfold_then H ltac:(fun K =>
xgc_post_if_not_evar;
eapply local_frame; [ xlocal | sapply K | cont1 tt | cont2 tt ]).
eapply local_frame_gc; [ xlocal | sapply K | cont1 tt | cont2 tt ]).
Ltac xapply_base H :=
xextract_check_not_needed tt;
......@@ -1439,7 +1433,8 @@ Tactic Notation "xval_st" constr(P) :=
- [xfun_ind R P] is a shorthand for proving a recursive function
by well-founded induction on the first argument quantified in [P].
It is similar to [xfun_no_simpl P], followed by [intros n] and
[induction_wf IH: R n]. The binary relation [R] needs to be
[induction_wf IH: R n], and then exploiting the characteristic
formula. The binary relation [R] needs to be
shown well-founded. Typical relation includes [downto 0]
and [upto n] for induction on the type [int].
......
......@@ -6,8 +6,6 @@ Require Import Array_ml.
Generalizable Variables A.
Print LibList.append.
(************************************************************)
......@@ -43,7 +41,7 @@ Lemma make_spec_direct : forall A (n:int) (v:A),
n >= 0 ->
app make [n v] \[] (fun l => l ~> Array (LibListZ.make n v)).
Proof using.
intros. xapp~. xsimpl~.
intros. xapp~.
Qed.
Parameter length_spec : curried 1%nat length /\
......
......@@ -11,58 +11,170 @@ Generalizable Variables A.
(** Functions treated directly by CFML *)
Ltac induction_wf_core_then IH E X cont :=
let T := type of E in
let T := eval hnf in T in
pattern X;
match T with
| ?A -> ?A -> Prop =>
first [
applys well_founded_ind E; clear X;
[ change well_founded with wf; auto with wf
| intros X IH; cont tt ]
| fail 2 ]
| _ => applys well_founded_ind E; clear X; intros X IH; cont tt
end.
Ltac xfun_ind_core R P IH ::=
xfun_spec_as_0 P ltac:(fun Hf =>
intro;
let X := get_last_hyp tt in
induction_wf_core_then IH R X ltac:(fun _ =>
intros; apply (proj2 Hf); clear Hf
)).
Tactic Notation "xcf_go" :=
xcf; xgo.
Tactic Notation "xcf_go" "~" :=
xcf_go; xauto~.
Tactic Notation "xcf_go" "*" :=
xcf_go; xauto*.
Ltac xauto_tilde ::= rew_list in *; try math; auto.
Lemma length_spec : forall A (l:list A),
app length [l] \[] \[= (@TLC.LibListZ.length _) l].
Proof using.
xcf.
xfun_ind (downto 0) (fun f => forall n (l:list A),
app f [n l] \[] \[= n + LibListZ.length l]).
(* details:
xfun_no_simpl (fun f => forall n (l:list A),
xcf. xfun_ind (@list_sub A) (fun f => forall (r:list A) n,
app f [n r] \[] \[= n + LibListZ.length r]); xgo~.
Qed.
Hint Extern 1 (RegisterSpec length) => Provide length_spec.
(* Remark: details of the script for length:
xcf. xfun_no_simpl (fun f => forall n (l:list A),
app f [n l] \[] \[= n + LibListZ.length l]).
intros n. induction_wf IH: (downto 0) n.
*)
{ intros. xapp12. xapp3. applys Saux. xspec. intros. xapp. apply Saux.
intros. apply (proj2 Saux). clear Saux.
{ xmatch.
{ xrets~. }
{ xapp~. xsimpl~. } }
{ xapp~. }
*)
Lemma rev_append_spec : forall A (l1 l2:list A),
app rev_append [l1 l2] \[] \[= LibList.rev l1 ++ l2].
Proof using.
intros. gen l2. induction_wf IH: (@list_sub A) l1. xcf_go~.
Qed.
Hint Extern 1 (RegisterSpec rev_append) => Provide rev_append_spec.
pattern n.
applys well_founded_ind (downto 0).
induction_wf IH: (downto 0) n.
applys well_founded_ind lt. apply lt_wf.
Print well_founded_ind.
Ltac xgo_once tt :=
try (xextract; intros); xgo_step tt; instantiate.
P
Ltac xgo_core tt :=
repeat (xgo_once tt).
Ltac xspec_core f ::=
first [ xspec_in_hyps_core f
(* FUTURE: | xspec_in database_spec_credits f *)
| xspec_in_core database_spec f
| xspec_app_in_hyps f
| fail 1 "xspec cannot find specification" ].
Ltac xcf_core tt ::=
intros;
match goal with
| |- spec ?f ?n ?P => first [ xcf_core_spec f | xcf_fallback f | fail 2 ]
| |- curried ?n ?f /\ ?P => first [ xcf_core_spec f | xcf_fallback f | fail 2 ]
| |- app ?f ?xs ?H ?Q => first [ xcf_core_app f | xcf_top_value f | xcf_fallback f | fail 2 ]
| |- tag tag_apply (app ?f ?xs ?H ?Q) => first [ xuntag tag_apply; xcf_core_app f | xcf_fallback f | fail 2 ]
| |- ?f = _ => first [ xcf_top_value f | xcf_fallback f | fail 2 ]
| _ => fail 1 "need to call [xcf f; => H], where [f] is the name of the definition"
end.
Ltac xgo_step tt ::=
match cfml_get_tag tt with
| tag_ret => xret
| tag_apply => xapp
| tag_none_app => xapp
| tag_val => xval
| tag_fun => xfun
| tag_let => xlet
| tag_match => xmatch
| tag_case => xcase
| tag_fail => xfail
| tag_done => xdone
| tag_alias => xalias
| tag_seq => xseq
| tag_if => xif
| tag_for => fail 1
| tag_while => fail 1
| tag_assert => fail 1 (* TODO assert *)
| _ =>
match goal with
| |- _ ==> _ => first [ xsimpl | fail 2 ]
| |- _ ===> _ => first [ xsimpl | fail 2 ]
end
end.
Ltac xcf_top_value f ::=
xcf_find f;
let Sf := fresh "Spec" in
intros Sf;
rewrite Sf;
clear Sf;
try solve_type.
{ xmatch.
{ xgo. rew_list. math. }
{ xapp.
Lemma rev_spec : forall A (l:list A),
app rev [l] \[] \[= (@TLC.LibList.rev _) l].
Proof using.
xcf. xgo.
xcf_go~.
Qed.
Lemma concat_spec : forall A (l:list A),
app concat [l] \[] \[= (@TLC.LibList.concat _) l].
Proof using.
xcf. xgo.
Qed.
Hint Extern 1 (RegisterSpec rev) => Provide rev_spec.
Lemma append_spec : forall A (l1 l2:list A),
app append [l1 l2] \[] \[= (@TLC.LibList.append _) l1 l2].
Proof using.
xcf. xgo.
xcf. xfun_ind (@list_sub A) (fun f => forall (r:list A),
app f [r] \[] \[= r ++ l2]); xgo*.
Qed.
Hint Extern 1 (RegisterSpec length) => Provide length_spec.
Hint Extern 1 (RegisterSpec rev) => Provide rev_spec.
Hint Extern 1 (RegisterSpec concat) => Provide concat_spec.
Hint Extern 1 (RegisterSpec append) => Provide append_spec.
Lemma infix_at__spec : forall A (l1 l2:list A),
app infix_at_ [l1 l2] \[] \[= (@TLC.LibList.append _) l1 l2].
Proof using. xcf_go~. Qed.
Hint Extern 1 (RegisterSpec infix_at_) => Provide infix_at__spec.
Lemma concat_spec : forall A (l:list (list A)),
app concat [l] \[] \[= (@TLC.LibList.concat _) l].
Proof using.
intros. induction_wf IH: (@list_sub (list A)) l. xcf_go*.
Qed.
Hint Extern 1 (RegisterSpec concat) => Provide concat_spec.
(************************************************************)
(** Iterators *)
......
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