List_proof.v 4.9 KB
Newer Older
charguer's avatar
cp  
charguer committed
1 2 3 4 5
Set Implicit Arguments.
Require Import CFLib.
Require Import Pervasives_ml Pervasives_proof.
Require Export LibListZ.
Require Import List_ml.
charguer's avatar
charguer committed
6
Require Import CFTactics.
charguer's avatar
cp  
charguer committed
7 8 9

Generalizable Variables A.

charguer's avatar
charguer committed
10

charguer's avatar
array  
charguer committed
11 12
Ltac auto_tilde ::= unfold measure; rew_list in *; try math; auto.
  (* Restored to default at the end of the file *)
charguer's avatar
lists  
charguer committed
13

charguer's avatar
charguer committed
14
(* TODO: find a nicer way to write [@TLC.LibList] *)
charguer's avatar
lists  
charguer committed
15

charguer's avatar
stdlib  
charguer committed
16 17
(************************************************************)
(** Functions treated directly by CFML *)
charguer's avatar
charguer committed
18

charguer's avatar
cp  
charguer committed
19 20 21
Lemma length_spec : forall A (l:list A), 
  app length [l] \[] \[= (@TLC.LibListZ.length _) l].
Proof using.
charguer's avatar
lists  
charguer committed
22 23 24 25 26
  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.
charguer's avatar
charguer committed
27

charguer's avatar
lists  
charguer committed
28
(* Remark: details of the script for length:
charguer's avatar
charguer committed
29

charguer's avatar
lists  
charguer committed
30 31 32 33 34 35 36 37 38 39 40 41 42 43 44
  xcf. xfun_no_simpl (fun f => forall n (l:list A),
    app f [n l] \[] \[= n + LibListZ.length l]).
  intros n. induction_wf IH: (downto 0) n.  
  intros. apply (proj2 Saux). clear Saux.
  { xmatch.  
    { xrets~. } 
    { xapp~. xsimpl~. } }
  { xapp~. }
*)

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.
charguer's avatar
cp  
charguer committed
45

charguer's avatar
lists  
charguer committed
46 47
Hint Extern 1 (RegisterSpec rev_append) => Provide rev_append_spec.

charguer's avatar
cp  
charguer committed
48 49
Lemma rev_spec : forall A (l:list A), 
  app rev [l] \[] \[= (@TLC.LibList.rev _) l].
charguer's avatar
stdlib  
charguer committed
50
Proof using. xcf_go~. Qed.
charguer's avatar
cp  
charguer committed
51

charguer's avatar
lists  
charguer committed
52
Hint Extern 1 (RegisterSpec rev) => Provide rev_spec.
charguer's avatar
cp  
charguer committed
53 54

Lemma append_spec : forall A (l1 l2:list A), 
charguer's avatar
charguer committed
55
  app append [l1 l2] \[] \[= (@TLC.LibList.app _) l1 l2].
charguer's avatar
cp  
charguer committed
56
Proof using.
charguer's avatar
lists  
charguer committed
57 58
  xcf. xfun_ind (@list_sub A) (fun f => forall (r:list A),
    app f [r] \[] \[= r ++ l2]); xgo*.
charguer's avatar
cp  
charguer committed
59 60 61
Qed.

Hint Extern 1 (RegisterSpec append) => Provide append_spec.
charguer's avatar
charguer committed
62

charguer's avatar
charguer committed
63
Lemma infix_at_spec : forall A (l1 l2:list A), 
charguer's avatar
charguer committed
64
  app infix_at__ [l1 l2] \[] \[= (@TLC.LibList.app _) l1 l2].
charguer's avatar
lists  
charguer committed
65 66
Proof using. xcf_go~. Qed.

charguer's avatar
charguer committed
67
Hint Extern 1 (RegisterSpec infix_at__) => Provide infix_at_spec.
charguer's avatar
lists  
charguer committed
68 69 70 71 72 73 74 75 76 77 78

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.



charguer's avatar
cp  
charguer committed
79 80 81
(************************************************************)
(** Iterators *)

charguer's avatar
stdlib  
charguer committed
82
Lemma iter_spec : forall A (l:list A) (f:func),
charguer's avatar
cp  
charguer committed
83 84 85 86 87
  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.
charguer's avatar
stdlib  
charguer committed
88 89 90 91
  =>> 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~.
charguer's avatar
cp  
charguer committed
92
Qed.
charguer's avatar
stdlib  
charguer committed
93 94 95 96
(* details:
  { xrets~. }
  { xapp~. xapp~. }
  *)
charguer's avatar
charguer committed
97

charguer's avatar
cp  
charguer committed
98
Hint Extern 1 (RegisterSpec iter) => Provide iter_spec.
charguer's avatar
charguer committed
99

charguer's avatar
stdlib  
charguer committed
100 101 102 103 104
(** 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),
charguer's avatar
cp  
charguer committed
105 106 107 108
  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.
charguer's avatar
stdlib  
charguer committed
109
  =>> M. xapp~ (fun k => Hexists r, \[l = k ++ r] \* I r).
charguer's avatar
toutbon  
charguer committed
110
  { =>> E. xpull ;=> r' E'. subst l.
111 112
    lets: app_cancel_l E'. subst r'.
    xapp. xsimpl~. }
charguer's avatar
charguer committed
113
  { xpull ;=>> E. rewrites (>> self_eq_app_l_inv E). xsimpl~. }
charguer's avatar
stdlib  
charguer committed
114 115
Qed. (* TODO: beautify this proof *)

charguer's avatar
charguer committed
116 117


charguer's avatar
cp  
charguer committed
118 119 120 121 122 123






charguer's avatar
array  
charguer committed
124
Ltac auto_tilde ::= auto_tilde_default.
charguer's avatar
cp  
charguer committed
125 126 127 128 129 130 131 132 133 134 135







(************************************************************)
(************************************************************)
(************************************************************)
(* FUTURE
charguer's avatar
charguer committed
136 137 138

Fixpoint List A a (T:A->a->hprop) (L:list A) (l:list a) : hprop :=
  match L,l with
charguer's avatar
cp  
charguer committed
139
  | nil, nil => \[l = nil] 
charguer's avatar
charguer committed
140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180
  | X::L', x::l' => x ~> T X \* l' ~> List T L'
  | _,_=> \[False]
  end.

Lemma focus_nil : forall A a (T:A->a->hprop),
  \[] ==> nil ~> List T nil.
Proof. intros. simpl. hdata_simpl. hsimpl~. Qed.

Lemma unfocus_nil : forall a (l:list a) A (T:A->a->hprop),
  l ~> List T nil ==> \[l = nil].
Proof. intros. simpl. hdata_simpl. destruct l. auto. hsimpl. Qed.

Lemma unfocus_nil' : forall A (L:list A) a (T:A->a->hprop),
  nil ~> List T L ==> \[L = nil].
Proof.
  intros. destruct L.
  simpl. hdata_simpl. hsimpl~.
  simpl. hdata_simpl. hsimpl.
Qed.

Lemma focus_cons : forall a (l:list a) A (X:A) (L':list A) (T:A->a->hprop),
  (l ~> List T (X::L')) ==>
  Hexists x l', (x ~> T X) \* (l' ~> List T L') \* \[l = x::l'].
Proof.
  intros. simpl. hdata_simpl. destruct l as [|x l'].
  hsimpl.
  hsimpl~ x l'.
Qed.

Lemma focus_cons' : forall a (x:a) (l:list a) A (L:list A) (T:A->a->hprop),
  (x::l) ~> List T L ==> 
  Hexists X L', \[L = X::L'] \* (x ~> T X) \* (l ~> List T L').
Proof. intros. destruct L; simpl; hdata_simpl; hsimpl~. Qed.

Lemma unfocus_cons : forall a (x:a) (l:list a) A (X:A) (L:list A) (T:A->a->hprop),
  (x ~> T X) \* (l ~> List T L) ==> 
  ((x::l) ~> List T (X::L)).
Proof. intros. simpl. hdata_simpl. hsimpl. Qed.

Global Opaque List.

charguer's avatar
cp  
charguer committed
181
*)