Commit 6bbaa4a7 authored by charguer's avatar charguer
Browse files

xapp

parent 04fd078b
......@@ -2641,3 +2641,36 @@ Tactic Notation "xunfocus" constr(t1) constr(t2) constr(t3) :=
Tactic Notation "xunfocus" constr(t1) constr(t2) constr(t3) constr(t4) :=
xunfocus t1; xunfocus t2 t3 t4.
------------
(* FUTURE
- [xapp_1] is like [xapp1]
- [xapp_2] is like [xapp1; xapp2]
- [xapp_3] is like [xapp1; xapp2; xapp3]
- [xapp_4] is like [xapp1; xapp2; xapp3; xapp4]
- [xapp_5] is like [xapp1; xapp2; xapp3; xapp4; xapp5]
Tactic Notation "xapp_1" := xapp1.
Tactic Notation "xapp_2" := xapp1; xapp2.
Tactic Notation "xapp_2_spec" constr(H) := xapp_1; xapp2_spec H.
Tactic Notation "xapp_3" := xapp_2; xapp3.
Tactic Notation "xapp_3" constr(args) := xapp_2; xapp3 args.
Tactic Notation "xapp_3_spec" constr(H) := xapp_2_spec H; xapp3.
Tactic Notation "xapp_3_spec" constr(H) constr(args) := xapp_2_spec H; xapp3 args.
Tactic Notation "xapp_4" := xapp_3; xapp4.
Tactic Notation "xapp_4" constr(args) := xapp_3 args; xapp4.
Tactic Notation "xapp_4_spec" constr(H) := xapp_spec H; xapp4.
Tactic Notation "xapp_4_spec" constr(H) constr(args) := xapp_3_spec H args; xapp4.
*)
......@@ -9,58 +9,55 @@ Open Scope tag_scope.
(********************************************************************)
(* ** Sequence *)
Axiom ret_unit_spec' : forall A (x:A),
app ret_unit [x] \[] \[= tt]. (* (fun (_:unit) => \[]).*) (* same as (# \[]). *)
Ltac xapp3_common args cont :=
let Sf := get_last_hyp tt in
let K := xapp_instantiate Sf args in
forwards_nounfold_then K cont.
Ltac xapp3_core args ::=
let Sfi := fresh "S" in
xapp3_common args ltac:(fun R =>
generalize R; intros Sfi).
Ltac xapp4_core args ::=
xapp3_common args ltac:(fun R =>
xapply_core R ltac:(fun _ => idtac) ltac:(fun _ => idtac)).
Hint Extern 1 (RegisterSpec ret_unit) => Provide ret_unit_spec'.
Ltac xapp5_core args ::=
xapp3_common args ltac:(fun R =>
xapply_core R ltac:(fun _ => hsimpl) ltac:(fun _ => try xok)).
Lemma seq_ret_unit_spec :
app seq_ret_unit [tt] \[] \[= tt].
Proof using.
xcf.
(* xlet. -- make sure we get a good error here *)
xseq.
xapp1.
xapp2.
dup 3.
{ xapp3_no_apply. apply S. }
{ xapp3_no_simpl. }
{ xapp3. }
dup 4.
{ xseq. xapp. xapp. xsimpl~. }
{ xapp. intro_subst. xapp. xsimpl~. }
{ xapps. xapps. xsimpl~. }
{ xapps. xapps~. }
Qed.
(********************************************************************)
(* ** Let-function *)
Lemma let_fun_poly_id_spec :
app let_fun_poly_id [tt] \[] \[= 3].
Proof using.
xcf. xfun.
xapp1.
xapp2.
dup 3.
{ xapp3. Focus 2. apply S. xret. }
{ xapp3. Focus 2. xapply S.
(* TODO . xsimpl. xsimpl.
apply S. xret. }
{ xapp4.
let args := constr:(>>) in
let Sf := get_last_hyp tt in
let Sfi := fresh "SpecI" in
let K := xapp_instantiate Sf args in
pose K.
forwards R: K.
xapp3.
*)
xcf. xfun. dup 2.
{ xapp. xret. xsimpl~. }
{ xapp1.
xapp2.
dup 5.
{ apply Spec. xret. }
{ xapp3_no_apply. Focus 2. apply S. xret. }
{ xapp3_no_simpl. xret. }
{ xapp3. xret. }
{ xapp. xret. xsimpl~. }
xsimpl~.
Qed.
Lemma let_fun_poly_pair_homogeneous () =
let f (x:'a) (y:'a) = (x,y) in
f 3 3
......@@ -133,25 +130,8 @@ Qed.
(********************************************************************)
(* ** Sequence *)
Axiom ret_unit_spec :
app ret_unit [tt] \[] \[= tt]. (* (fun (_:unit) => \[]).*) (* same as (# \[]). *)
Proof using.
Lemma seq_noop_spec :
app seq_noop [tt] \[] \[= tt].
Proof using.
xcf.
xfun.
xret.
Qed.
......
......@@ -394,3 +394,8 @@ Definition spec (f:func) (n:nat) (P:Prop) :=
(********************************************************************)
(* ** Export opaque *)
Opaque app_def curried.
......@@ -160,6 +160,44 @@ Proof using.
*)
Admitted. (* demo *)
(* ** FUTURE WORK: extend hsimpl to handle \[] ==> ?H1 \* ?H2 *)
(*
Ltac instantiate_right_when_left_empty tt
...
Ltac hsimpl_cleanup tt ::=
try apply hsimpl_stop;
try apply hsimpl_stop;
try apply pred_le_refl;
try hsimpl_hint_remove tt;
try remove_empty_heaps_right tt;
try remove_empty_heaps_left tt;
try instantiate_right_when_left_empty tt.
Lemma hsimpl_demo_6 :
(forall H1 H2, \[] ==> H1 \* H2 -> True) ->
True.
Proof using.
introv M. dup.
(* details *)
eapply M.
hsimpl_setup tt.
hsimpl_step tt.
hsimpl_step tt.
hsimpl_step tt.
try hsimpl_step tt.
hsimpl_cleanup tt.
Admitted. (* demo *)
*)
(********************************************************************)
(** [hclean] *)
Lemma hclean_demo_1 : forall A (x X:A) H1 H2 H3 B (F:~~B) Q,
......
......@@ -34,6 +34,8 @@ Inductive tag_type : Type :=
| tag_pay
| 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_top_trm -- FUTURE *)
......@@ -62,6 +64,8 @@ Ltac cfml_get_tag tt :=
match goal with
| |- @tag ?t _ _ => constr:(t)
| |- @tag ?t _ _ _ _ => constr:(t)
| |- app ?f ?xs ?H ?Q => constr:(tag_none_app)
| |- _ => constr:(tag_none)
end.
(** [cfml_check_not_tagged tt] fails if the head of the goal contains a tag *)
......@@ -80,8 +84,9 @@ Tactic Notation "xuntag" constr(T) :=
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.
(** [xuntag] removes the tag at the head of the goal,
and fails if there is not tag there. *)
......
......@@ -729,11 +729,17 @@ Tactic Notation "xframes" constr(s1) constr(s2) constr(s3) :=
the subgoals.
Hint: call [xgc] prior to [xapply] if you also need a
step of garbage collection. *)
step of garbage collection.
// LATER: make [xapply] support the gc rule, and introduce
// [xapply_no_gc E] is like [xapply] but does not allow
// for the garbage collection rule to be applied.
// In that case, change [xapp_prepare] to not do [xgc];
// but check first that introduce evars later is not an issue.
*)
Ltac xapply_core H cont1 cont2 :=
forwards_nounfold_then H ltac:(fun K =>
eapply local_wframe; [xlocal | sapply K | cont1 tt | cont2 tt]).
eapply local_wframe; [ xlocal | sapply K | cont1 tt | cont2 tt ]).
Ltac xapply_base H :=
xextract_check_not_needed tt;
......@@ -757,6 +763,17 @@ Tactic Notation "xapplys" "~" constr(H) :=
Tactic Notation "xapplys" "*" constr(H) :=
xapplys H; xauto*.
(* -- commented out for faster compilation
Lemma xapply_demo_1 : forall B R H H' (Q:B->hprop),
is_local R ->
R H Q ->
R (H \* H') (Q \*+ H').
Proof using.
introv HR M. dup 2.
{ xapply M. xsimpl. xsimpl. }
{ xapplys M. }
Qed.
*)
(*--------------------------------------------------------*)
(* ** [xchange] *)
......@@ -1097,20 +1114,36 @@ Qed.
Use [xlet Q as y] to do both. *)
Ltac xlet_core cont0 cont1 cont2 :=
xextract_check_not_needed tt;
apply local_erase; cont0 tt; split; [ | cont1 tt; cont2 tt ].
Tactic Notation "xlet_def" tactic(c0) tactic(c1) tactic(c2) :=
xlet_core ltac:(c0) ltac:(c1) ltac:(c2).
Ltac xlet_def cont0 cont1 cont2 :=
xextract_check_not_needed tt;
xuntag tag_let;
xlet_core cont0 cont1 cont2.
Tactic Notation "xlet" constr(Q) "as" simple_intropattern(x) :=
xlet_def (fun _ => exists Q) (fun _ => intros x) (fun _ => try xextract).
xlet_def
ltac:(fun _ => exists Q)
ltac:(fun _ => intros x)
ltac:(fun _ => try xextract).
Tactic Notation "xlet" constr(Q) :=
xlet_def (fun _ => exists Q) (fun _ => intro) (fun _ => try xextract).
xlet_def
ltac:(fun _ => exists Q)
ltac:(fun _ => intro)
ltac:(fun _ => try xextract).
Tactic Notation "xlet" "as" simple_intropattern(x) :=
xlet_def (fun _ => esplit) (fun _ => intros x) (fun _ => idtac).
xlet_def
ltac:(fun _ => esplit)
ltac:(fun _ => intros x)
ltac:(fun _ => idtac).
Tactic Notation "xlet" :=
xlet_def (fun _ => esplit) (fun _ => intro) (fun _ => idtac).
xlet_def
ltac:(fun _ => esplit)
ltac:(fun _ => intro)
ltac:(fun _ => idtac).
Tactic Notation "xlet" "~" := xlet; xauto~.
Tactic Notation "xlet" "~" "as" simple_intropattern(x) := xlet as x; xauto~.
......@@ -1140,13 +1173,39 @@ Tactic Notation "xlets" constr(Q) :=
Use [xseq_no_xextract H'] to prevent [xextract] from being
called automatically after [xseq H']. *)
Tactic Notation "xseq_no_xextract" constr(H) :=
xlet_def (fun _ => first [ exists (#H) | exists H ]) (fun _ => idtac) (fun _ => idtac).
Ltac xseq_pre tt :=
xextract_check_not_needed tt;
xuntag tag_seq.
Ltac xseq_noarg_core tt :=
xseq_pre tt;
xlet_core
ltac:(fun _ => esplit)
ltac:(fun _ => idtac)
ltac:(fun _ => idtac).
Ltac xseq_arg_core H :=
xseq_pre tt;
xlet_core
ltac:(fun _ => first [ exists (#H) | exists H ])
ltac:(fun _ => idtac)
ltac:(fun _ => try xextract).
Ltac xseq_no_xextract_core H :=
xseq_pre tt;
xlet_core
ltac:(fun _ => first [ exists (#H) | exists H ])
ltac:(fun _ => idtac)
ltac:(fun _ => idtac).
Tactic Notation "xseq" :=
xlet_def (fun _ => esplit) (fun _ => idtac) (fun _ => idtac).
xseq_noarg_core tt.
Tactic Notation "xseq" constr(H) :=
xlet_def (fun _ => first [ exists (#H) | exists H ]) (fun _ => idtac) (fun _ => try xextract).
xseq_arg_core H.
Tactic Notation "xseq_no_xextract" constr(H) :=
xseq_no_xextract_core H.
Tactic Notation "xseq" "~" := xseq; xauto~.
Tactic Notation "xseq" "~" constr(H) := xseq H; xauto~.
......@@ -2009,17 +2068,16 @@ Tactic Notation "xspec_in" constr(db) constr(f) :=
Tactic Notation "xspec" constr(f) :=
xspec_core f.
Ltac cfml_apply_xseq_or_xlet_to_see_function cont :=
first [
match cfml_get_tag tt with
| tag_let => xlet; [ cont tt | ]
| tag_seq => xseq; [ cont tt | ]
| _ => cont tt
end
| cont tt ].
Ltac cfml_apply_xseq_or_xlet_to_reveal_app cont :=
match cfml_get_tag tt with
| tag_let => xlet; [ cont tt | ]
| tag_seq => xseq; [ cont tt | ]
| tag_none_app => cont tt
| _ => fail 2 "xspec expects the goal to be an application"
end.
Ltac cfml_apply_xseq_or_xlet_then_process_function cont :=
cfml_apply_xseq_or_xlet_to_see_function ltac:(fun _ =>
cfml_apply_xseq_or_xlet_to_reveal_app ltac:(fun _ =>
let f := cfml_get_goal_fun tt in cont f).
Tactic Notation "xspec_in_hyps" :=
......@@ -2074,24 +2132,29 @@ Tactic Notation "xspec" :=
- [xapp2] looks up the specification for the function and pushes
it into the goal.
[xapp2_spec H] can be used to provide a custom specification.
- [xapp3] exploits the last hypothesis in the goal as a specification
and instantiates it using the tactic [forward].
[xapp3 args] can be used to provide arguments.
At this point, sides conditions should be discarded.
//TODO: [xapp3_skip] can be used to skip all side conditions.
- [xapp2_spec H] can be used to provide a custom specification.
- [xapp4] applies the frame rule, exploiting lemma [local_wframe].
- [xapp12] and [xapp12_spec H] are shorthands for combining the two.
- [xapp5] applies the last hypothesis in the goal to the goal.
From there, [xsimpl] should be called on the other two goals
produced by [xapp4].
- [xapp12] is short for [xapp1; xapp2].
- [xapp3] exploits the last hypothesis in the goal as a specification
to prove the goal, using either [applys] or [xapply], and then
calling [xsimpl] like [xapp] would do.
- [xapp3 Es] can be used to provide arguments to the lemma.
- [xapp45] is short for [xapp4; xapp5].
- [xapp3a], alias [xapp_no_apply] is like [xapp3] but it only shows
the instantiation, without applying it.
- [xapp3b], alias [xapp_no_simpl] is like [xapp3] but it does not
the instantiation, without calling [xsimpl] on the subgoals.
A typical debugging session goes as follows:
- try [xapp12] or [xapp12_spec H]
if this fails, then try [xapp1]
if this fails, then the goal does not have the right shape for [xapp]
else, the specification lemma was not found in the database (see [xspec]).
else continue the script with [xapp3b]
if this fails, replace it with [xapp3a] to see the instantiation
else execute [xapp3], which is like [xapp3b] plus [xsimpl].
*)
(* TODO: xapp_spec_no_simpl *)
......@@ -2122,13 +2185,18 @@ Ltac xapp_use_or_find H Sf :=
Ltac xapp_prepare_goal cont :=
xextract_check_not_needed tt;
match cfml_get_tag tt with
| tag_apply =>
| tag_let => xlet; [ xuntag tag_apply; cont tt | instantiate; xextract ]
| tag_seq => xseq; [ xuntag tag_apply; cont tt | instantiate; xextract ]
| tag_apply =>
match cfml_postcondition_is_meta tt with
| false => xgc; [ xuntag tag_apply; cont tt | ]
| true => xuntag tag_apply; cont tt
end
| tag_let => xlet; [ xuntag tag_apply; cont tt | instantiate; xextract ]
| tag_seq => xseq; [ xuntag tag_apply; cont tt | instantiate; xextract ]
end
| tag_none_app =>
match cfml_postcondition_is_meta tt with
| false => xgc; [ cont tt | ]
| true => cont tt
end
end.
Ltac xapp_instantiate Sf args :=
......@@ -2162,14 +2230,16 @@ Ltac xapp_common H E xapp_core cont :=
(* helper for [xapp] internal implementation *)
Ltac xapp_xapply_generic K cont1 cont2 :=
eapply local_wframe; [ xlocal | sapply K | cont1 tt | cont2 tt ].
Ltac xapp_xapply_with_simpl K :=
xapply_core K ltac:(fun _ => hsimpl) ltac:(fun _ => try xok).
first
[ applys K (* useful for specifications that are CF *)
| xapply_core K ltac:(fun _ => hsimpl) ltac:(fun _ => try xok) ].
(* TODO: make sure that [apply K] does not trigger when not desired *)
Ltac xapp_xapply_no_simpl K :=
xapply_core K ltac:(fun _ => idtac) ltac:(fun _ => idtac).
first
[ applys K
| xapply_core K ltac:(fun _ => idtac) ltac:(fun _ => idtac) ].
(* [xapp] implementation,
with [H] as specification (or [___]),
......@@ -2196,6 +2266,7 @@ Ltac xapps_core H E cont :=
| tag_let => xlet; [ cont1 tt | cont2 tt ]
| tag_seq => xseq; [ cont1 tt | cont2 tt ]
| tag_apply => xapp_core H E cont
| tag_none_app => xapp_core H E cont
end.
(* [xapp as X] implementation *)
......@@ -2219,62 +2290,47 @@ Ltac xapp2_spec_core H :=
let Sf := fresh "Spec" in
xapp_use_or_find H Sf.
Ltac xapp3_core args :=
Ltac xapp3_no_apply_core args :=
let Sf := get_last_hyp tt in
let Sfi := fresh "SpecI" in
let K := xapp_instantiate Sf args in
generalize K; intros Sfi. (* ; clear Sf. *)
forwards_nounfold_then K ltac:(fun R =>
let Sfi := fresh "S" in
generalize R; intros Sfi).
Ltac xapp4_core tt :=
eapply local_wframe; [ xlocal | | | ].
Ltac xapp5_core tt :=
let K := get_last_hyp tt in
xapply_core K ltac:(fun _ => hsimpl) ltac:(fun _ => try xok).
Ltac xapp5_no_simpl_core tt :=
let K := get_last_hyp tt in
xapply_core K ltac:(fun _ => idtac) ltac:(fun _ => idtac).
Ltac xapp3_no_simpl_core args :=
let Sf := get_last_hyp tt in
let K := xapp_instantiate Sf args in
xapp_xapply_no_simpl K.
Ltac xapp45_core tt :=
let K := get_last_hyp tt in
xapp_xapply_generic K ltac:(fun _ => idtac) ltac:(fun _ => idtac).
Ltac xapp3_core args :=
let Sf := get_last_hyp tt in
let K := xapp_instantiate Sf args in
xapp_xapply_with_simpl K.
(* Notation for [xapp] debugging versions *)
Tactic Notation "xapp1" := xapp1_core tt.
Tactic Notation "xapp2" := xapp2_core tt.
Tactic Notation "xapp2_spec" constr(H) := xapp2_spec_core H.
Tactic Notation "xapp12" := xapp1; xapp2_core tt.
Tactic Notation "xapp12_spec" constr(H) := xapp1; xapp2_spec_core H.
Tactic Notation "xapp3_no_apply" := xapp3_no_apply_core (>>).
Tactic Notation "xapp3_no_apply" constr(args) := xapp3_no_apply_core args.
Tactic Notation "xapp3a" := xapp3_no_apply.
Tactic Notation "xapp3a" constr(args) := xapp3_no_apply args.
Tactic Notation "xapp3_no_simpl" := xapp3_no_simpl_core (>>).
Tactic Notation "xapp3_no_simpl" constr(args) := xapp3_no_simpl_core args.
Tactic Notation "xapp3b" := xapp3_no_simpl.
Tactic Notation "xapp3b" constr(args) := xapp3_no_simpl args.
Tactic Notation "xapp3" := xapp3_core (>>).
Tactic Notation "xapp3" constr(args) := xapp3_core args.
Tactic Notation "xapp4" := xapp4_core tt.
Tactic Notation "xapp5" := xapp5_core tt.
Tactic Notation "xapp5_no_simpl" := xapp5_no_simpl_core tt.
Tactic Notation "xapp45" := xapp45_core tt.
(* FUTURE
- [xapp_1] is like [xapp1]
- [xapp_2] is like [xapp1; xapp2]
- [xapp_3] is like [xapp1; xapp2; xapp3]
- [xapp_4] is like [xapp1; xapp2; xapp3; xapp4]
- [xapp_5] is like [xapp1; xapp2; xapp3; xapp4; xapp5]
Tactic Notation "xapp_1" := xapp1.
Tactic Notation "xapp_2" := xapp1; xapp2.
Tactic Notation "xapp_2_spec" constr(H) := xapp_1; xapp2_spec H.
Tactic Notation "xapp_3" := xapp_2; xapp3.
Tactic Notation "xapp_3" constr(args) := xapp_2; xapp3 args.
Tactic Notation "xapp_3_spec" constr(H) := xapp_2_spec H; xapp3.
Tactic Notation "xapp_3_spec" constr(H) constr(args) := xapp_2_spec H; xapp3 args.
Tactic Notation "xapp_4" := xapp_3; xapp4.
Tactic Notation "xapp_4" constr(args) := xapp_3 args; xapp4.
Tactic Notation "xapp_4_spec" constr(H) := xapp_spec H; xapp4.
Tactic Notation "xapp_4_spec" constr(H) constr(args) := xapp_3_spec H args; xapp4.
*)
(* Notation for [xapp] with automation and with hints *)
......
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