Commit c4e908e4 authored by charguer's avatar charguer

stdlib_ok

parent 08df47b0
......@@ -11,6 +11,7 @@ Generalizable Variables A.
Ltac auto_tilde ::= unfold measure; rew_list in *; try math; auto.
(* Restored to default at the end of the file *)
(* TODO: find a nicer way to write [@TLC.LibList] *)
(************************************************************)
(** Functions treated directly by CFML *)
......@@ -51,7 +52,7 @@ Proof using. xcf_go~. Qed.
Hint Extern 1 (RegisterSpec rev) => Provide rev_spec.
Lemma append_spec : forall A (l1 l2:list A),
app append [l1 l2] \[] \[= (@TLC.LibList.append _) l1 l2].
app append [l1 l2] \[] \[= (@TLC.LibList.app _) l1 l2].
Proof using.
xcf. xfun_ind (@list_sub A) (fun f => forall (r:list A),
app f [r] \[] \[= r ++ l2]); xgo*.
......@@ -60,7 +61,7 @@ Qed.
Hint Extern 1 (RegisterSpec append) => Provide append_spec.
Lemma infix_at_spec : forall A (l1 l2:list A),
app infix_at__ [l1 l2] \[] \[= (@TLC.LibList.append _) l1 l2].
app infix_at__ [l1 l2] \[] \[= (@TLC.LibList.app _) l1 l2].
Proof using. xcf_go~. Qed.
Hint Extern 1 (RegisterSpec infix_at__) => Provide infix_at_spec.
......@@ -107,9 +108,9 @@ Lemma iter_spec_rest : forall A (l:list A) (f:func),
Proof using.
=>> M. xapp~ (fun k => Hexists r, \[l = k ++ r] \* I r).
{ =>> E. xpull ;=> r' E'. subst l.
lets: app_eq_prefix_inv_l E'. subst r'.
lets: app_cancel_l E'. subst r'.
xapp. xsimpl~. xsimpl~. }
{ xpull ;=>> E. rewrites (>> app_eq_self_inv_l E). xsimpl~. }
{ xpull ;=>> E. rewrites (>> self_eq_app_l_inv 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