Commit 9cadd115 authored by charguer's avatar charguer

stdlib

parent 1e009e4d
......@@ -22,20 +22,40 @@ Ltac forwards_nounfold_skip_sides_then S cont :=
end.
Ltac induction_wf_core IH E X :=
(* [xinduction IH: E X] now accepts for [E] either
- a proof of [wf R] for [R] of type [A->A->Prop]
- a binary relation of type [A->A->Prop]
- a measure of type [A->nat]
*)
Ltac induction_wf_core_then IH E X cont :=
let T := type of E in
let T := eval hnf in T in
pattern X;
let clearX tt :=
first [ clear X | fail 3 "the variable on which the induction is done appears in the hypotheses" ] in
match T with
| ?A -> nat =>
induction_wf_core_then IH (measure_wf E) X cont
(* TODO: error message might not show up in this case *)
| ?A -> ?A -> Prop =>
pattern X;
first [
applys well_founded_ind E; clear X;
applys well_founded_ind E;
clearX tt;
[ change well_founded with wf; auto with wf
| intros X IH ]
| intros X IH; cont tt ]
| fail 2 ]
| _ => applys well_founded_ind E; clear X; intros X IH
| _ =>
pattern X;
applys well_founded_ind E;
clearX tt;
intros X IH;
cont tt
end.
Ltac induction_wf_core IH E X :=
induction_wf_core_then IH E X ltac:(fun _ => idtac).
Tactic Notation "induction_wf" ident(IH) ":" constr(E) ident(X) :=
induction_wf_core IH E X.
Tactic Notation "induction_wf" ":" constr(E) ident(X) :=
......@@ -44,6 +64,14 @@ Tactic Notation "induction_wf" ":" constr(E) ident(X) :=
induction_wf: E X.
(* FOR LibList. v *)
Lemma app_eq_prefix_inv_l : forall A (l1 l2 l2' : list A),
l1 ++ l2 = l1 ++ l2' -> l2 = l2'.
Proof using.
introv E. induction l1; rew_list in *. auto. inverts* E.
Qed.
(*--------------------------------------------------------*)
(* ** [=>] and [=>>] tactics for introduction *)
......@@ -1527,12 +1555,13 @@ Tactic Notation "xfun_no_simpl" constr(P) "as" ident(f) ident(Hf) :=
(* TODO: support higher number of mutually recursive functions. *)
Ltac xfun_ind_core R S IH :=
xfun_no_simpl S; [
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 IH: R x
| ].
let X := get_last_hyp tt in
induction_wf_core_then IH R X ltac:(fun _ =>
intros; apply (proj2 Hf); clear Hf
)).
Tactic Notation "xfun_ind" constr(R) constr(S) "as" ident(IH) :=
xfun_ind_core R S IH.
......@@ -2294,7 +2323,7 @@ Ltac xspec_core f :=
(* FUTURE: | xspec_in database_spec_credits f *)
| xspec_in_core database_spec f
| xspec_app_in_hyps f
| fail 100 "xspec cannot find specification" ].
| fail 1 "xspec cannot find specification" ].
Tactic Notation "xspec_in_hyps" constr(f) :=
xspec_in_hyps_core f.
......@@ -3008,19 +3037,21 @@ Ltac xcf_top_value f :=
let Sf := fresh "Spec" in
intros Sf;
rewrite Sf;
clear Sf.
clear Sf;
try solve_type.
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_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.
Tactic Notation "xcf" :=
xcf_core tt.
......@@ -3182,10 +3213,20 @@ Tactic Notation "xskip_credits" :=
(********************************************************************)
(* ** Tactics for Automation *)
(** EXPERIMENTAL
[xgo] automatically applies the appropriate [xtactic].
This tactic should only be used to conclude simple goals.
[xcf_go] is short for [xcf; xgo].
*)
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
......@@ -3205,13 +3246,18 @@ Ltac xgo_step tt :=
| |- _ ===> _ => first [ xsimpl | fail 2 ]
end
end.
(*
(*
| tag_casewhen => fail 1
| tag_app_curried
| tag_pay*)
Ltac xgo_once tt :=
try (xextract; intros); xgo_step tt; instantiate.
Ltac xgo_core tt :=
repeat (try (xextract; intros); xgo_step tt; instantiate).
repeat (xgo_once tt).
Tactic Notation "xgo" :=
xgo_core tt.
......@@ -3219,3 +3265,10 @@ Tactic Notation "xgo" "~" :=
xgo; xauto~.
Tactic Notation "xgo" "*" :=
xgo; xauto*.
Tactic Notation "xcf_go" :=
xcf; xgo.
Tactic Notation "xcf_go" "~" :=
xcf_go; xauto~.
Tactic Notation "xcf_go" "*" :=
xcf_go; xauto*.
\ No newline at end of file
......@@ -7,46 +7,11 @@ Require Import List_ml.
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
)).
Ltac xauto_tilde ::= unfold measure; rew_list in *; try math; auto.
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.
(************************************************************)
(** Functions treated directly by CFML *)
Lemma length_spec : forall A (l:list A),
app length [l] \[] \[= (@TLC.LibListZ.length _) l].
......@@ -77,76 +42,9 @@ Qed.
Hint Extern 1 (RegisterSpec rev_append) => Provide rev_append_spec.
Ltac xgo_once tt :=
try (xextract; intros); xgo_step tt; instantiate.
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.
Lemma rev_spec : forall A (l:list A),
app rev [l] \[] \[= (@TLC.LibList.rev _) l].
Proof using.
xcf_go~.
Qed.
Proof using. xcf_go~. Qed.
Hint Extern 1 (RegisterSpec rev) => Provide rev_spec.
......@@ -175,30 +73,43 @@ Hint Extern 1 (RegisterSpec concat) => Provide concat_spec.
(************************************************************)
(** Iterators *)
Lemma iter_spec_rest : forall A (l1 l2:list A) (f:func),
Lemma iter_spec : forall A (l:list A) (f:func),
forall (I:list A->hprop),
(forall x t r, (l = t++x::r) ->
app f [x] (I t) (# I (t&x))) ->
app iter [f l] (I nil) (# I l).
Proof using.
xcf. xgo.
=>> M. cuts G: (forall r t, l = t++r ->
app iter [f r] (I t) (# I l)). { xapp~. }
=> r. induction_wf IH: (@LibList.length A) r. =>> E.
xcf. xmatch; rew_list in E; inverts E; xgo~.
Qed.
(* details:
{ xrets~. }
{ xapp~. xapp~. }
*)
Hint Extern 1 (RegisterSpec iter) => Provide iter_spec.
(* LATER
Lemma iter_spec_rest : forall A (l1 l2:list A) (f:func),
(** Alternative spec for [iter], with an invariant that
depends on the remaining items, rather than depending
on the processed items. *)
Lemma iter_spec_rest : forall A (l:list A) (f:func),
forall (I:list A->hprop),
(forall x t, app f [x] (I (x::t)) (# I t)) ->
app iter [f l] (I l) (# I nil).
Proof using.
xcf. xgo.
Qed.
*)
=>> M. xapp~ (fun k => Hexists r, \[l = k ++ r] \* I r).
{ =>> E. xextract ;=> r' E'. subst l.
lets: app_eq_prefix_inv_l E'. subst r'.
xapp. xsimpl~. xsimpl~. }
{ xextract ;=>> E. rewrites (>> app_eq_self_inv_l E). xsimpl~. }
Qed. (* TODO: beautify this proof *)
......
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