Commit aa5e34dc authored by charguer's avatar charguer
Browse files

cp

parent 61213d3d
......@@ -20,7 +20,7 @@ SANITY
else if name = "exists" then "exists__"
else if name = "forall" then "forall__"
- restriction on not binding "min" and "max" could be a bit restrictive..
......@@ -28,6 +28,10 @@ SANITY
LATER
- prevent rebinding of List
- restriction on not binding "min" and "max" might be a bit restrictive..
- add support for pure records
- in print_tast and print_past, protect with parenth the infix names being bound
......
......@@ -8,7 +8,6 @@ open Pervasives
*)
(********************************************************************)
(* ** Return *)
......@@ -182,6 +181,12 @@ let compare_float () =
(1. <> 0. && 1. <= 2.) || (0. = 1. && 1. >= 2. && 1. < 2. && 2. > 1.)
*)
(********************************************************************)
(* ** List operators *)
let list_ops () =
let x = [1] in
List.length (List.rev (List.concat (List.append [x] [x; x])))
(********************************************************************)
......
......@@ -9,6 +9,23 @@ Require Import Stdlib.
Lemma max_spec' : forall (n m:int),
app max [n m]
PRE \[]
POST \[= Coq.ZArith.BinInt.Zmax n m ].
Abort.
Lemma max_spec'' : forall (n m:int),
app max [n m]
PRE \[]
RET x ST \[x = Coq.ZArith.BinInt.Zmax n m ].
Abort.
......
......@@ -142,6 +142,10 @@ let inlined_primitives_table =
"Pervasives.>=", (Primitive_binary_only_numbers, "(fun x_ y_ : int => TLC.LibReflect.isTrue (@TLC.LibOrder.ge int (@TLC.LibOrder.ge_from_le int TLC.LibInt.le_int_inst) x_ y_))");
"Pervasives.max", (Primitive_binary_only_numbers, "Coq.ZArith.BinInt.Zmax");
"Pervasives.min", (Primitive_binary_only_numbers, "Coq.ZArith.BinInt.Zmin");
"List.length", (Primitive_unary, "(@TLC.LibListZ.length _)");
"List.rev", (Primitive_unary, "(@TLC.LibList.rev _)");
"List.concat", (Primitive_unary, "(@TLC.LibList.concat _)");
"List.append", (Primitive_binary, "(@TLC.LibList.append _)");
]
......
......@@ -35,7 +35,8 @@ Inductive tag_type : Type :=
| tag_top_val
| tag_top_fun
| tag_none_app (* used for tactics when the goal has no tag but is an app *)
| tag_none (* used for tactics when the goal has no tag *)
| tag_none
| tag_goal (* used for tactics when the goal has no tag *)
.
(* | tag_top_trm -- FUTURE *)
......@@ -45,19 +46,6 @@ Definition tag (t:tag_type) (A:Type) (P:A) := P.
Implicit Arguments tag [A].
(** Lemmas and tactics to manipulate tags *)
Lemma add_tag : forall (T:Prop->Prop), (T = fun P:Prop => P) ->
forall (G:Prop), (T G) -> G.
Proof. intros. subst. auto. Qed.
(* DEPRECATED
(** [cfml_add_tag T] adds a tag [T] to the head of the goal *)
Ltac cfml_add_tag T :=
apply (@add_tag T (refl_equal _)).
*)
(** [cfml_get_tag tt] returns the tag at the head of the goal *)
Ltac cfml_get_tag tt :=
......@@ -78,14 +66,23 @@ Ltac cfml_check_not_tagged tt :=
end.
(** [xuntag T] removes the tag [T] at the head of the goal,
and fails if it is not there. *)
and fails if it is not there. The tag [tag_goal] is
treated specially: it is automatically removed on the fly.
To remove only [tag_goal], use [xuntag_goal]. *)
Tactic Notation "xuntag" constr(T) :=
Ltac xuntag_core T :=
match goal with
| |- @tag tag_goal _ _ _ _ => unfold tag at 1
| _ => idtac
end;
match goal with
| |- @tag T _ _ => unfold tag at 1
| |- @tag T _ _ _ _ => unfold tag at 1
| _ => fail 1 "goal does not contain the expected tag: " T
end.
Tactic Notation "xuntag" constr(T) :=
xuntag_core T.
(** [xuntag] removes the tag at the head of the goal,
and fails if there is not tag there. *)
......@@ -99,7 +96,39 @@ Tactic Notation "xuntag" :=
(** [xuntags] removes all tags from everywhere in the goal;
useful for debugging. *)
Tactic Notation "xuntags" := unfold tag in *.
Tactic Notation "xuntags" :=
unfold tag in *.
(** [xtag_goal] adds the tag [tag_goal] to the characteristic
formula at the head of the goal. It does nothing if there
is no such formula, or if the tag [tag_goal] is already
present. *)
Ltac xtag_goal_core tt :=
match goal with
| |- @tag tag_goal _ _ _ _ => idtac
| |- @tag _ _ _ _ _ =>
match goal with |- ?G =>
match get_fun_arg G with (?G1,?Q) =>
match get_fun_arg G1 with (?F,?H) =>
change G with ((@tag tag_goal _ F) H Q) end end end
| _ => idtac
end.
Tactic Notation "xtag_goal" :=
xtag_goal_core tt.
(** [xuntag_goal] removes [tag_goal] from the head of the goal,
or does nothing if there is no such tag. *)
Ltac xuntag_goal_core tt :=
match goal with
| |- @tag tag_goal _ _ _ _ => unfold tag at 1
| _ => idtac
end.
Tactic Notation "xuntag_goal" :=
xuntag_goal_core tt.
(********************************************************************)
......@@ -165,6 +194,25 @@ Notation "'!TopTerm' P" := (tag tag_top_trm (local P))
Local Open Scope tag_scope.
(********************************************************************)
(* ** Notation for applied characteristic formulae [tag_goal] *)
Notation "'PRE' H 'POST' Q 'CODE' F" :=
(@tag tag_goal _ F H Q) (at level 69,
format "'[v' '[' 'PRE' H ']' '/' '[' 'POST' Q ']' '/' '[' 'CODE' F ']' ']'")
: charac.
Notation "F 'PRE' H 'POST' Q" :=
(F H Q)
(at level 69, only parsing) : charac.
Notation "F 'PRE' H 'RET' x 'ST' Qx" :=
(F H (fun x => Qx))
(at level 69, only parsing) : charac.
(********************************************************************)
(** Ret *)
......
......@@ -3,6 +3,48 @@ Require Import LibCore Shared CFHeaps.
Require Export (* LibInt *) CFPrint.
(*--------------------------------------------------------*)
(* ** TODO: move to LibTactics.v *)
Inductive ltac_goal_to_discard := ltac_goal_to_discard_intro.
Ltac forwards_nounfold_skip_sides_then S cont :=
let MARK := fresh in
generalize ltac_goal_to_discard_intro;
intro MARK;
forwards_nounfold_then S ltac:(fun K =>
clear MARK;
cont K);
match goal with
| MARK: ltac_goal_to_discard |- _ => skip
| _ => idtac
end.
Ltac induction_wf_core IH E X :=
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 ]
| fail 2 ]
| _ => applys well_founded_ind E; clear X; intros X IH
end.
Tactic Notation "induction_wf" ident(IH) ":" constr(E) ident(X) :=
induction_wf_core IH E X.
Tactic Notation "induction_wf" ":" constr(E) ident(X) :=
let IH := fresh "IH" in induction_wf IH: E X.
Tactic Notation "induction_wf" ":" constr(E) ident(X) :=
induction_wf: E X.
(*--------------------------------------------------------*)
(* ** [=>] and [=>>] tactics for introduction *)
......@@ -313,6 +355,72 @@ Ltac cfml_get_goal_arity tt :=
end .
(*--------------------------------------------------------*)
(* ** Tools for showing types involved in [app] instances *)
(* [cfml_show_types_dyn_list L] displays the types of the
arguments in the list [L] *)
Ltac cfml_show_types_dyn_list L :=
match L with
| nil => idtac
| (@dyn ?T ?x) :: ?R => idtac T "->"; cfml_show_types_dyn_list R
end.
(* [cfml_get_app_args E] returns the arguments associated with the
[app] in the term [E] provided *)
Ltac cfml_get_app_args E :=
match E with
| app ?f ?xs ?H ?Q => constr:(xs)
| tag tag_apply (app ?f ?xs) ?H ?Q => constr:(xs)
end.
(* [cfml_get_goal_app_args tt] returns the arguments associated with the
[app] at the head of the goal. *)
Ltac cfml_get_goal_app_args tt :=
match goal with |- ?G => cfml_get_app_args G end.
(* [cfml_get_goal_app_ret E] returns the arguments associated with the
[app] in the term [E] provided. *)
Ltac cfml_get_app_ret E :=
match E with
| @app_def ?f ?xs ?B ?H ?Q => constr:(B)
| tag tag_apply (@app_def ?f ?xs ?B) ?H ?Q => constr:(B)
end.
(* [cfml_get_goal_app_ret tt] returns the arguments associated with the
[app] at the head of the goal. *)
Ltac cfml_get_goal_app_ret tt :=
match goal with |- ?G => cfml_get_app_ret G end.
(* [cfml_show_app_type E] displays the type of the
function application in [E] *)
Ltac cfml_show_app_type E :=
let L := cfml_get_app_args E in
cfml_show_types_dyn_list L;
let B := cfml_get_app_ret E in
idtac B.
(* [cfml_show_app_type_goal tt] displays the type of
the function application in the goal.
(calls [intros] if needed. *)
Ltac cfml_show_app_type_goal tt :=
match goal with |- ?G => cfml_show_app_type G end.
(* [cfml_show_app_type_concl S] displays the type of
the function application in the conclusion of [S] *)
Ltac cfml_show_app_type_concl S :=
forwards_nounfold_then S ltac:(fun K =>
cfml_show_app_type K).
(********************************************************************)
(* ** Simplification, Automation, and Cleaning *)
......@@ -1325,13 +1433,22 @@ Tactic Notation "xval_st" constr(P) :=
- [xfun_no_simpl P] is like the above but does not attempt to
automatically exploit the most general specification for
proving the special specification.
proving the special specification. Use [xapp] or [apply]
to continue the proof.
- [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
shown well-founded. Typical relation includes [downto 0]
and [upto n] for induction on the type [int].
- Also available:
[xfun P as f]
[xfun P as f Hf]
[xfun_no_simpl P as f]
[xfun_no_simpl P as f Hf]
[xfun_ind R P as IH]
*)
......@@ -1415,6 +1532,20 @@ 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; [
intro;
let x := get_last_hyp tt in
induction_wf IH: R x
| ].
Tactic Notation "xfun_ind" constr(R) constr(S) "as" ident(IH) :=
xfun_ind_core R S IH.
Tactic Notation "xfun_ind" constr(R) constr(S) :=
let IH := fresh "IH" in xfun_ind R S as IH.
(*--------------------------------------------------------*)
(* ** [xret] and [xret_no_gc] and [xrets] *)
......@@ -2247,6 +2378,8 @@ Tactic Notation "xspec" :=
*)
(** Debugging for [xapp]:
- [xapp_types] show the types involved in the [app] instances.
- [xapp1] sets the goal in the right form for [xapp],
by calling [xseq] or [xlet], or [xgc_post] if applicable
......@@ -2307,6 +2440,11 @@ Ltac xapp_prepare_goal cont :=
match cfml_get_tag tt with
| tag_let => xlet; [ xuntag tag_apply; cont tt | instantiate; xextract ]
| tag_seq => xseq; [ xuntag tag_apply; cont tt | instantiate; xextract ]
| tag_apply => xuntag tag_apply; cont tt
| tag_none_app => cont tt
end.
(* DEPRECATED
| tag_apply =>
match cfml_postcondition_is_evar tt with
| false => xgc_post; [ xuntag tag_apply; cont tt | ]
......@@ -2317,7 +2455,7 @@ Ltac xapp_prepare_goal cont :=
| false => xgc_post; [ cont tt | ]
| true => cont tt
end
end.
*)
Ltac xapp_instantiate Sf args :=
let args := list_boxer_of args in
......@@ -2583,6 +2721,22 @@ Ltac xapp_skip_core tt :=
Tactic Notation "xapp_skip" :=
xapp_prepare_goal ltac:(fun _ => xapp_skip_core tt).
(** [xapp_types] *)
Ltac xapp_types_core_noarg tt :=
xapp_prepare_goal ltac:(fun _ => idtac);
idtac "=== type of app in goal ===";
cfml_show_app_type_goal tt;
idtac "=== type of app in spec === ";
let S := fresh "Spec" in
xapp_use_or_find ___ S;
forwards_nounfold_skip_sides_then S ltac:(fun K =>
let T := type of K in
cfml_show_app_type T);
clear S.
Tactic Notation "xapp_types" :=
xapp_types_core_noarg tt.
......@@ -2804,6 +2958,11 @@ Tactic Notation "xapp_skip" :=
[xcf_show f as H] are similiar but allow providing name of
the assumption.
- [xcf_types] shows the type of the application in the
goal, compared with the one from the specification.
- [xcf_types S] is similar, with [S] the specification lemma.
*)
(* TODO: extend to support partial application *)
......@@ -2844,7 +3003,7 @@ Ltac xcf_core_app f :=
xcf_core_app_exploit H. (* todo: might need sapply here *)
Ltac xcf_fallback f :=
idtac "Warning: could not exploit the specification; maybe the types don't match; if you intend to use the specification manually, call [xcf_show as S].";
idtac "Warning: could not exploit the specification; maybe the types don't match; check them using [xcf_debug]; if you intend to use the specification manually, use [xcf_show as S].";
xcf_find f;
let Sf := fresh "Spec" in
intros Sf.
......@@ -2909,6 +3068,35 @@ Tactic Notation "xcf_show" constr(f) :=
Tactic Notation "xcf" "~" := xcf; xauto_tilde.
Tactic Notation "xcf" "*" := xcf; xauto_star.
Ltac xcf_types_core tt :=
let S := fresh "Spec" in
first [intros [_ S] | intros S];
idtac "=== type of app in goal ===";
cfml_show_app_type_goal tt;
idtac "=== type of app in code === ";
forwards_nounfold_skip_sides_then S ltac:(fun K =>
let T := type of K in
cfml_show_app_type T);
clear S.
Ltac xcf_types_core_noarg tt :=
intros;
let H := fresh in
xcf_show_core H;
revert H;
xcf_types_core tt.
Ltac xcf_types_core_arg S :=
intros;
generalize S;
xcf_types_core tt.
Tactic Notation "xcf_types" :=
xcf_types_core_noarg tt.
Tactic Notation "xcf_types" constr(S) :=
xcf_types_core_arg S.
(********************************************************************)
(* ** Additional tools for proofs *)
......
......@@ -10,7 +10,6 @@ Ltac is_not_evar E :=
| idtac ].
(********************************************************************)
(** Notation for functions expecting tuples as arguments *)
......@@ -58,6 +57,17 @@ Tactic Notation "false" "~" constr(E) :=
(* todo: to work around a coq bug; still needed? *)
(* TODO: move to libtactics *)
Ltac app_evar t A cont ::=
let x := fresh "X" in
evar (x:A);
let t' := constr:(t x) in
let t'' := (eval unfold x in t') in
subst x; cont t''.
(********************************************************************)
(** Treatment of partially-applied equality *)
......
......@@ -6,6 +6,10 @@ Require Import Array_ml.
Generalizable Variables A.
Print LibList.append.
(************************************************************)
(** Builtin *)
......@@ -65,7 +69,6 @@ Hint Extern 1 (RegisterSpec get) => Provide get_spec.
(************************************************************)
(************************************************************)
(************************************************************)
......
Set Implicit Arguments.
Require Import CFLib.
Require Import Pervasives_ml Pervasives_proof.
Require Export LibListZ.
Require Import List_ml.
Generalizable Variables A.
(************************************************************)
(** Lists *)
(** Functions treated directly by CFML *)
Parameter caml_list_iter_spec : forall a,
Spec caml_list_iter f l |R>> forall (I:list a->hprop),
(forall x t, (App f x;) (I (x::t)) (# I t)) ->
R (I l) (# I nil).
Hint Extern 1 (RegisterSpec caml_list_iter) => Provide caml_list_iter_spec.
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),
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.
(*
(************************************************************)
(** Stacks *)
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.
P
{ 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.
Qed.
Lemma concat_spec : forall A (l:list A),
app concat [l] \[] \[= (@TLC.LibList.concat _) l].
Proof using.
xcf. xgo.
Qed.
Lemma append_spec : forall A (l1 l2:list A),
app append [l1 l2] \[] \[= (@TLC.LibList.append _) l1 l2].
Proof using.
xcf. 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.
Module Stack_ml.
Definition t (A:Type) := loc.
End Stack_ml.
Parameter caml_stack_create : func.
Parameter caml_stack_is_empty : func.
Parameter caml_stack_push : func.
Parameter caml_stack_pop : func.
(************************************************************)
(** Iterators *)
Lemma iter_spec_rest : forall A (l1 l2: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.
Qed.
Hint Extern 1 (RegisterSpec iter) => Provide iter_spec.
(* LATER
Lemma iter_spec_rest : forall A (l1 l2:list A) (f:func),
forall (I:list A->hprop),