Commit 4e4d805f authored by charguer's avatar charguer
Browse files

xlet

parent 6bbaa4a7
......@@ -9,131 +9,6 @@ Open Scope tag_scope.
(********************************************************************)
(* ** Sequence *)
Axiom ret_unit_spec' : forall A (x:A),
app ret_unit [x] \[] \[= tt]. (* (fun (_:unit) => \[]).*) (* same as (# \[]). *)
Hint Extern 1 (RegisterSpec ret_unit) => Provide ret_unit_spec'.
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. 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
Proof using.
xcf.
Qed.
Lemma let_fun_on_the_fly () =
(fun x f -> f x) 3 (fun x -> x+1)
Proof using.
xcf.
Qed.
Lemma let_fun_const_spec :
app let_fun_const [tt] \[] \[= 3].
Proof using.
xcf. dup 9.
{ xfun. apply Sf. xrets~. }
{ xfun as g. apply Sg. skip. }
{ xfun as g G. apply G. skip. }
{ xfun_no_simpl (fun g => app g [tt] \[] \[=3]).
{ apply Sf. skip. }
{ apply Sf. } }
{ xfun_no_simpl (fun g => app g [tt] \[] \[=3]) as h.
{ apply Sh. skip. }
{ apply Sh. } }
{ xfun_no_simpl (fun g => app g [tt] \[] \[=3]) as h H.
{ apply H. skip. }
{ apply H. } }
{ xfun (fun g => app g [tt] \[] \[=3]).
{ xrets~. }
{ apply Sf. } }
{ xfun (fun g => app g [tt] \[] \[=3]) as h.
{ skip. }
{ skip. } }
{ xfun (fun g => app g [tt] \[] \[=3]) as h H.
{ skip. }
{ skip. } }
Qed.
(********************************************************************)
(* ** Let-term *)
Lemma let_term_nested_id_calls () =
let f x = x in
let a = f (f (f 2)) in
a
Proof using.
xcf.
Qed.
Lemma let_term_nested_pairs_calls () =
let f x y = (x,y) in
let a = f (f 1 2) (f 3 (f 4 5)) in
a
Proof using.
xcf.
Qed.
(********************************************************************)
(********************************************************************)
......@@ -199,6 +74,34 @@ Lemma ret_poly_spec : forall A,
Proof using. xcf. xrets*. Qed.
(********************************************************************)
(* ** Sequence *)
Axiom ret_unit_spec' : forall A (x:A),
app ret_unit [x] \[] \[= tt]. (* (fun (_:unit) => \[]).*) (* same as (# \[]). *)
Hint Extern 1 (RegisterSpec ret_unit) => Provide ret_unit_spec'.
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-value *)
......@@ -231,6 +134,101 @@ Proof using.
Qed.
(********************************************************************)
(* ** Let-function *)
Lemma let_fun_const_spec :
app let_fun_const [tt] \[] \[= 3].
Proof using.
xcf. dup 9.
{ xfun. apply Sf. xrets~. }
{ xfun as g. apply Sg. skip. }
{ xfun as g G. apply G. skip. }
{ xfun_no_simpl (fun g => app g [tt] \[] \[=3]).
{ apply Sf. skip. }
{ apply Sf. } }
{ xfun_no_simpl (fun g => app g [tt] \[] \[=3]) as h.
{ apply Sh. skip. }
{ apply Sh. } }
{ xfun_no_simpl (fun g => app g [tt] \[] \[=3]) as h H.
{ apply H. skip. }
{ apply H. } }
{ xfun (fun g => app g [tt] \[] \[=3]).
{ xrets~. }
{ apply Sf. } }
{ xfun (fun g => app g [tt] \[] \[=3]) as h.
{ skip. }
{ skip. } }
{ xfun (fun g => app g [tt] \[] \[=3]) as h H.
{ skip. }
{ skip. } }
Qed.
Lemma let_fun_poly_id_spec :
app let_fun_poly_id [tt] \[] \[= 3].
Proof using.
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_spec :
app let_fun_poly_pair_homogeneous [tt] \[] \[= (3,3)].
Proof using.
xcf.
xfun.
xapp.
xret.
xsimpl~.
Qed.
Lemma let_fun_on_the_fly_spec :
app let_fun_on_the_fly [tt] \[] \[= 4].
Proof using.
xcf.
xfun.
xfun.
xapp.
xapp.
xret.
xsimpl~.
Qed.
(********************************************************************)
(* ** Let-term *)
Lemma let_term_nested_id_calls_spec :
app let_term_nested_id_calls [tt] \[] \[= 2].
Proof using.
xcf.
xfun (fun f => forall (x:int), app f [x] \[] \[= x]). { xret~. }
xapps.
xapps.
xapps.
xrets~.
Qed.
Lemma let_term_nested_pairs_calls_spec :
app let_term_nested_pairs_calls [tt] \[] \[= ((1,2),(3,(4,5))) ].
Proof using.
xcf.
xfun (fun f => forall A B (x:A) (y:B), app f [x y] \[] \[= (x,y)]). { xret~. }
xapps.
xapps.
xapps.
xapps.
xrets~.
Qed.
(********************************************************************)
(* ** Pattern-matching *)
......
......@@ -397,5 +397,5 @@ Definition spec (f:func) (n:nat) (P:Prop) :=
(********************************************************************)
(* ** Export opaque *)
Opaque app_def curried.
Global Opaque app_def curried.
......@@ -1295,6 +1295,8 @@ Tactic Notation "xval_st" constr(P) :=
- [xfun P] can be used to give a specification for [f], proved
with respect to the most-general specification. Here, [P]
should take the form [fun f => spec_of_f].
When this tactic fails, try
[xfun_no_simpl P as f Sf. intros. apply Sf.]
- [xfun_no_simpl P] is like the above but does not attempt to
automatically exploit the most general specification for
......@@ -1305,9 +1307,6 @@ Tactic Notation "xval_st" constr(P) :=
[xfun P as f Hf]
[xfun_no_simpl P as f]
[xfun_no_simpl P as f Hf]
*)
......@@ -1342,7 +1341,7 @@ Ltac xfun_spec_as f P Hf cont1 :=
let H := fresh "B" f in
assert (H: P f);
[ cont1 Hf
| clear Hf; rename H into Hf ].
| clear Hf; rename H into Hf; hnf in Hf ].
Ltac xfun_spec_as_0 P cont :=
xfun_pre tt;
......@@ -1369,7 +1368,7 @@ Ltac xfun_spec_as_2 P f Hf cont :=
and it exploits [Hf] then clears it in order to prove the goal. *)
Ltac xfun_simpl Hf :=
eapply Hf; clear Hf. (* hnf first? *)
intros; eapply Hf; clear Hf. (* hnf first? *)
Tactic Notation "xfun" constr(P) :=
xfun_spec_as_0 P ltac:(fun Hf => xfun_simpl Hf).
......@@ -2640,11 +2639,15 @@ Tactic Notation "xapp" "*" constr(E) "as" simple_intropattern(X) :=
(*--------------------------------------------------------*)
(* ** [xcf] *)
(** [xcf] applies to a goal of the form
(** [xcf] applies to a goal with a conclusion of the form
[spec f n K] or [app f xs H Q].
It looks up the characteristic formula associated with [f]
in the database "database_cf", and exploits it to start
proving the goal.
proving the goal. Note that [xcf] first step is to call [intros].
When [xcf] fails to apply, it is (most usually) because the number
of arguments, or the types of the arguments, or the return type,
does not match.
Variants:
......
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