Library CFML.Stdlib.List_proof

Set Implicit Arguments.
Require Import CFLib.
Require Import Pervasives_ml Pervasives_proof.
Require Export LibListZ.
Require Import List_ml.
Require Import CFTactics.

Generalizable Variables A.

Ltac auto_tilde ::= unfold measure; rew_list in *; try math; auto.

Functions treated directly by CFML

Lemma length_spec : forall A (l:list A),
  app length [l ] \[] \[= (@TLC.LibListZ.length _) l ].
Proof using.
  xcf. xfun_ind (@list_sub A) (fun f => forall (r:list A) n,
    app f [n r ] \[] \[= n + LibListZ.length r ]); xgo~.
Qed.

Hint Extern 1 (RegisterSpec length) => Provide length_spec.

Lemma rev_append_spec : forall A (l1 l2:list A),
  app rev_append [l1 l2 ] \[] \[= LibList.rev l1 ++ l2 ].
Proof using.
  intros. gen l2. induction_wf IH: (@list_sub A) l1. xcf_go~.
Qed.

Hint Extern 1 (RegisterSpec rev_append) => Provide rev_append_spec.

Lemma rev_spec : forall A (l:list A),
  app rev [l ] \[] \[= (@TLC.LibList.rev _) l ].
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.app _) l1 l2 ].
Proof using.
  xcf. xfun_ind (@list_sub A) (fun f => forall (r:list A),
    app f [r ] \[] \[= r ++ l2]); xgo*.
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.app _) l1 l2 ].
Proof using. xcf_go~. Qed.

Hint Extern 1 (RegisterSpec infix_at__) => Provide infix_at_spec.

Lemma concat_spec : forall A (l:list (list A)),
  app concat [l ] \[] \[= (@TLC.LibList.concat _) l ].
Proof using.
  intros. induction_wf IH: (@list_sub (list A)) l. xcf_go*.
Qed.

Hint Extern 1 (RegisterSpec concat) => Provide concat_spec.

Iterators

Lemma iter_spec : forall A (l: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.
  =>> M. cuts G: (forall r t, l = t ++r ->
    app iter [f r ] (I t) (# I l)). { xapp~. }
  => r. induction_wf IH: (@LibList.length A) r. =>> E.
  xcf. xmatch; rew_list in E; inverts E; xgo~.
Qed.

Hint Extern 1 (RegisterSpec iter) => Provide iter_spec.

Alternative spec for iter, with an invariant that depends on the remaining items, rather than depending on the processed items.

Lemma iter_spec_rest : forall A (l:list A) (f:func),
  forall (I:list A ->hprop),
  (forall x t, app f [x ] (I (x ::t)) (# I t)) ->
  app iter [f l ] (I l) (# I nil).
Proof using.
  =>> M. xapp~ (fun k => Hexists r, \[l = k ++ r ] \* I r).
  { =>> E. xpull ;=> r' E'. subst l.
    lets: app_cancel_l E'. subst r'.
    xapp. xsimpl~. }
  { xpull ;=>> E. rewrites (>> self_eq_app_l_inv E). xsimpl~. }
Qed.
Ltac auto_tilde ::= auto_tilde_default.