Commit 04fd078b authored by charguer's avatar charguer
Browse files

progress_xapp

parent 77d73257
......@@ -9,6 +9,28 @@ Open Scope tag_scope.
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)).
Ltac xapp5_core args ::=
xapp3_common args ltac:(fun R =>
xapply_core R ltac:(fun _ => hsimpl) ltac:(fun _ => try xok)).
(********************************************************************)
(* ** Let-function *)
......@@ -16,7 +38,27 @@ Open Scope tag_scope.
Lemma let_fun_poly_id_spec :
app let_fun_poly_id [tt] \[] \[= 3].
Proof using.
xcf. xfun. xapp.
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.
*)
Qed.
Lemma let_fun_poly_pair_homogeneous () =
......@@ -432,6 +474,13 @@ Qed.
*)
(********************************************************************)
(********************************************************************)
(********************************************************************)
(* TODO: xgc demo *)
(********************************************************************)
(********************************************************************)
(********************************************************************)
......@@ -688,4 +737,6 @@ Proof using. intros. xcf. xval as p Hp. subst p. xrets. auto. Qed.
*
\ No newline at end of file
......@@ -297,7 +297,7 @@ Ltac cfml_get_goal_fun tt :=
match goal with
| |- spec ?f ?n ?P => constr:(f)
| |- app ?f ?xs ?H ?Q => constr:(f)
| |- tag tag_apply (app ?f ?xs ?H ?Q) => constr:(f)
| |- tag tag_apply (app ?f ?xs) ?H ?Q => constr:(f)
end.
(* [cfml_get_goal_arity] returns the arity associated with the
......@@ -448,12 +448,15 @@ Tactic Notation "hsimpl" "~" constr(X1) constr(X2) constr(X3) :=
Ltac xlocal_core tt ::=
first [ assumption
| apply app_local; (* then prove [xs <> nil] *)
let E := fresh in intro E; discriminate E
| apply local_is_local
(*| apply app_local_pred --TODO fix *)
| match goal with H: is_local_pred ?S |- is_local (?S _) => apply H end ].
(********************************************************************)
(* ** Tactics for Structural Rules *)
......@@ -1979,7 +1982,10 @@ Tactic Notation "xmatch" constr(Q) :=
Ltac xspec_in_hyps_core f :=
match goal with
| H: spec f _ _ |- _ => generalize H
| H: spec f _ _ |- _ =>
generalize (proj2 H)
| H: @tag tag_app_curried Prop (curried _ f /\ _) |- _ =>
generalize (proj2 H)
end.
Ltac xspec_app_in_hyps f :=
......@@ -2004,11 +2010,13 @@ Tactic Notation "xspec" constr(f) :=
xspec_core f.
Ltac cfml_apply_xseq_or_xlet_to_see_function cont :=
match cfml_get_tag tt with
| tag_let => xlet; [ cont tt | ]
| tag_seq => xseq; [ cont tt | ]
| _ => cont tt
end.
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_then_process_function cont :=
cfml_apply_xseq_or_xlet_to_see_function ltac:(fun _ =>
......@@ -2097,17 +2105,18 @@ Ltac xapp_extract_app_from_spec_as Sf :=
| |- (_) -> _ => intros Sf
end.
(* [xapp_use_of_find H Sf] creates an hypothesis [Sf]
(* [xapp_use_or_find H Sf] creates an hypothesis [Sf]
that is equal to [H] if [H] is not [___], else
finds a spec for the current function, and names it [Sf]. *)
Ltac xapp_use_of_find H Sf :=
Ltac xapp_use_or_find H Sf :=
match H with
| ___ => xspec
| ___ => first [ xspec | fail 2 "could not find specification" ]
| _ => generalize H
end;
xapp_extract_app_from_spec_as Sf.
(* [xapp_prepare_goal] tactic for settings things up *)
Ltac xapp_prepare_goal cont :=
......@@ -2148,7 +2157,7 @@ Ltac xapp_instantiate_and_apply Sf args xapp_core cont :=
Ltac xapp_common H E xapp_core cont :=
xapp_prepare_goal ltac:(fun _ =>
let Sf := fresh "Spec" in
xapp_use_of_find H Sf;
xapp_use_or_find H Sf;
xapp_instantiate_and_apply Sf E xapp_core cont).
(* helper for [xapp] internal implementation *)
......@@ -2204,11 +2213,11 @@ Ltac xapp1_core tt :=
Ltac xapp2_core tt :=
let Sf := fresh "Spec" in
xapp_use_of_find ___ Sf.
xapp_use_or_find ___ Sf.
Ltac xapp2_spec_core H :=
let Sf := fresh "Spec" in
xapp_use_of_find H Sf.
xapp_use_or_find H Sf.
Ltac xapp3_core args :=
let Sf := get_last_hyp tt in
......@@ -2221,7 +2230,11 @@ Ltac xapp4_core tt :=
Ltac xapp5_core tt :=
let K := get_last_hyp tt in
sapply K.
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 xapp45_core tt :=
let K := get_last_hyp tt in
......@@ -2239,6 +2252,7 @@ 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
......
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