ExampleHigherOrder.v 5.68 KB
 charguer committed May 18, 2017 1 2 ``````(** `````` Jacques-Henri Jourdan committed Feb 07, 2018 3 ``````This file formalizes examples of first-class functions in plain `````` charguer committed May 18, 2017 4 5 6 7 8 9 10 11 ``````Separation Logic, using lifted characteristic formulae. Author: Arthur Charguéraud. License: MIT. *) Set Implicit Arguments. `````` charguer committed Dec 04, 2017 12 ``````From Sep Require Import Example. `````` charguer committed May 18, 2017 13 14 ``````Generalizable Variables A B. `````` charguer committed May 19, 2017 15 ``````Implicit Types p : loc. `````` charguer committed May 18, 2017 16 17 18 ``````Implicit Types n : int. `````` charguer committed May 18, 2017 19 20 21 22 `````` (* ********************************************************************** *) (* * Apply function *) `````` charguer committed Jun 08, 2017 23 ``````Definition val_apply : val := `````` charguer committed Jan 18, 2018 24 `````` ValFun 'f 'x := ('f 'x). `````` charguer committed Jun 08, 2017 25 26 27 `````` Lemma Rule_apply : forall (f:func) `{EA:Enc A} (x:A), forall (H:hprop) `{EB:Enc B} (Q:B->hprop), `````` 28 29 `````` Triple (f ``x) H Q -> Triple (val_apply ``f ``x) H Q. `````` charguer committed Jun 08, 2017 30 31 32 33 34 ``````Proof using. introv M. xcf. (* todo why not simplified? *) unfold Substs; simpl; rew_enc_dyn. xapp. hsimpl~. Qed. `````` charguer committed May 18, 2017 35 `````` `````` charguer committed Jun 08, 2017 36 37 ``````Lemma Rule_apply' : forall (f:func) `{EA:Enc A} (x:A), forall (H:hprop) `{EB:Enc B} (Q:B->hprop), `````` 38 39 `````` Triple (val_apply f ``x) PRE (\[Triple (f ``x) H Q] \* H) `````` charguer committed Jun 08, 2017 40 41 `````` POST Q. Proof using. intros. xpull ;=> M. applys~ Rule_apply. Qed. `````` charguer committed May 18, 2017 42 43 44 45 `````` (* ********************************************************************** *) `````` charguer committed Jun 08, 2017 46 47 48 ``````(* * RefApply function *) Definition val_refapply : val := `````` Jacques-Henri Jourdan committed Feb 07, 2018 49 `````` ValFun 'f 'r := `````` charguer committed Jan 18, 2018 50 51 52 `````` Let 'x := val_get 'r in Let 'y := 'f 'x in val_set 'r 'y. `````` charguer committed Jun 08, 2017 53 54 55 `````` Lemma Rule_refapply_pure : forall (f:func) `{EA:Enc A} (r:loc) (x:A), forall `{EB:Enc B} (P:A->B->Prop), `````` 56 `````` Triple (f ``x) `````` Jacques-Henri Jourdan committed Feb 07, 2018 57 58 `````` PRE \[] POST (fun y => \[P x y]) `````` charguer committed Jun 08, 2017 59 `````` -> `````` 60 `````` Triple (val_refapply ``f ``r) `````` Jacques-Henri Jourdan committed Feb 07, 2018 61 `````` PRE (r ~~> x) `````` charguer committed Jun 08, 2017 62 63 64 65 66 67 68 `````` POST (fun (_:unit) => Hexists y, \[P x y] \* r ~~> y). Proof using. introv M. xcf. xapps. xapp ;=> y E. xapp. hsimpl~. Qed. Lemma Rule_refapply_effect : forall (f:func) `{EA:Enc A} (r:loc) (x:A), forall `{EB:Enc B} (P:A->B->Prop) (H H':hprop), `````` 69 `````` Triple (f ``x) `````` Jacques-Henri Jourdan committed Feb 07, 2018 70 71 `````` PRE H POST (fun y => \[P x y] \* H') `````` charguer committed Jun 08, 2017 72 `````` -> `````` 73 `````` Triple (val_refapply ``f ``r) `````` Jacques-Henri Jourdan committed Feb 07, 2018 74 `````` PRE (r ~~> x \* H) `````` charguer committed Jun 08, 2017 75 76 77 78 79 `````` POST (fun (_:unit) => Hexists y, \[P x y] \* r ~~> y \* H'). Proof using. introv M. xcf. xapps. xapp ;=> y E. xapp. hsimpl~. Qed. `````` charguer committed May 18, 2017 80 81 82 `````` (* ********************************************************************** *) `````` charguer committed Jun 08, 2017 83 ``````(* * Twice function *) `````` charguer committed May 18, 2017 84 `````` `````` charguer committed Jun 08, 2017 85 ``````Definition val_twice : val := `````` Jacques-Henri Jourdan committed Feb 07, 2018 86 `````` ValFun 'f := `````` 87 `````` 'f '() ;;; `````` charguer committed Jan 18, 2018 88 `````` 'f '(). `````` charguer committed May 18, 2017 89 `````` `````` charguer committed Jun 08, 2017 90 ``````Lemma Rule_twice : forall (f:func) (H H':hprop) `{EB:Enc B} (Q:B->hprop), `````` 91 92 93 `````` Triple (f ``tt) H (fun (_:unit) => H') -> Triple (f ``tt) H' Q -> Triple (val_twice ``f) H Q. `````` charguer committed Jun 08, 2017 94 95 96 ``````Proof using. introv M1 M2. xcf. xseq. xapp M1. xapp M2. hsimpl~. Qed. `````` charguer committed May 18, 2017 97 98 99 `````` (* ********************************************************************** *) `````` charguer committed Jun 08, 2017 100 101 102 ``````(* * Repeat function *) Definition val_repeat : val := `````` Jacques-Henri Jourdan committed Feb 07, 2018 103 104 `````` ValFun 'n 'f := For 'i := 1 To 'n Do `````` charguer committed Jan 18, 2018 105 `````` 'f '() `````` charguer committed Jun 08, 2017 106 107 108 109 110 111 `````` Done. Axiom xfor_inv_lemma : forall (I:int->hprop), forall (a:int) (b:int) (F:int->Formula) H H', (a <= b+1) -> (H ==> I a \* H') -> `````` charguer committed Jan 18, 2018 112 113 `````` (forall i, a <= i <= b -> ^(F i) (I i) (fun (_:unit) => I(i+1))) -> ^(Cf_for a b F) H (fun (_:unit) => I (b+1) \* H'). `````` charguer committed Jun 08, 2017 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 `````` Lemma Rule_consequence_post : forall t `{Enc A} (Q':A->hprop) H (Q:A->hprop), Triple t H Q' -> Q' ===> Q -> Triple t H Q. Proof using. introv MH M MQ. applys* Rule_consequence MH. Qed. Lemma xfor_simplify_inequality_lemma : forall (n:int), ((n-1)+1) = n. Proof using. math. Qed. Lemma Rule_repeat : forall (I:int->hprop) (f:func) (n:int), n >= 0 -> (forall i, 0 <= i < n -> `````` 130 `````` Triple (f ``tt) `````` charguer committed Jun 08, 2017 131 132 133 `````` PRE (I i) POST (fun (_:unit) => I (i+1))) -> `````` 134 `````` Triple (val_repeat ``n ``f) `````` charguer committed Jun 08, 2017 135 136 137 138 `````` PRE (I 0) POST (fun (_:unit) => I n). Proof using. introv N M. xcf. `````` 139 `````` asserts_rewrite (``n = val_int n). auto. (* todo: investigate *) `````` charguer committed Jun 08, 2017 140 141 142 143 `````` applys local_weaken_post. xlocal. applys local_erase. applys xfor_inv_lemma (fun i => (I (i-1))). { math. } { hsimpl. } `````` Jacques-Henri Jourdan committed Feb 07, 2018 144 `````` { intros i Hi. xapp. { math. } { math_rewrite (i-1+1=i+1-1). hsimpl. } } `````` charguer committed Jun 08, 2017 145 `````` { math_rewrite (n+1-1=n). hsimpl. } `````` Jacques-Henri Jourdan committed Feb 07, 2018 146 `````` (* todo : avoid math_rewrite, `````` charguer committed Jun 08, 2017 147 148 149 `````` thanks to hsimpl simplification of invariants *) Qed. `````` charguer committed May 18, 2017 150 151 `````` (* ********************************************************************** *) `````` charguer committed Jun 08, 2017 152 ``````(* * Iteration (iter, fold, map, find) on lists: see [ExampleList.v] *) `````` charguer committed May 18, 2017 153 154 `````` `````` charguer committed May 18, 2017 155 156 157 158 159 160 161 162 163 164 165 ``````(* ********************************************************************** *) (* * Counter function *) Implicit Types g : val. (* ---------------------------------------------------------------------- *) (** Representation *) Definition MCount (n:int) (g:val) : hprop := Hexists p, (p ~~> n) \* `````` Jacques-Henri Jourdan committed Feb 07, 2018 166 167 `````` \[ forall n', Triple (g val_unit) (p ~~> n') `````` charguer committed May 18, 2017 168 169 170 171 172 173 174 175 `````` (fun r => \[r = n'+1] \* (p ~~> (n'+1))) ]. (* TODO: fix priority of p ~~> (n'+1) differently *) (* ---------------------------------------------------------------------- *) (** Specification *) `````` charguer committed May 22, 2017 176 `````` `````` charguer committed May 18, 2017 177 ``````Lemma Rule_MCount : forall n g, `````` charguer committed May 22, 2017 178 `````` Triple (g '()) (g ~> MCount n) (fun r => \[ r = n+1 ] \* g ~> MCount (n+1)). `````` charguer committed May 18, 2017 179 ``````Proof using. `````` Jacques-Henri Jourdan committed Feb 07, 2018 180 `````` intros. xunfolds MCount at 1 ;=> p Hg. xapp. `````` charguer committed May 22, 2017 181 `````` hpulls. xunfold MCount. hsimpl~. `````` Jacques-Henri Jourdan committed Feb 07, 2018 182 ``````Qed. `````` charguer committed May 18, 2017 183 184 185 186 187 188 `````` (* ---------------------------------------------------------------------- *) (** Implementation *) Definition val_mkcounter : val := `````` charguer committed Jan 18, 2018 189 190 `````` ValFun 'u := Let 'p := val_ref 0 in `````` 191 `````` (Fun 'v := val_incr 'p ;;; val_get 'p). `````` charguer committed May 18, 2017 192 193 194 195 196 `````` (* ---------------------------------------------------------------------- *) (** Verification *) `````` Jacques-Henri Jourdan committed Feb 07, 2018 197 ``````Lemma Rule_mkcounter : `````` 198 `````` Triple (val_mkcounter ``val_unit) `````` Jacques-Henri Jourdan committed Feb 07, 2018 199 `````` \[] `````` charguer committed May 22, 2017 200 `````` (fun g => g ~> MCount 0). `````` charguer committed May 18, 2017 201 ``````Proof using. `````` charguer committed May 22, 2017 202 203 `````` xcf. xapps ;=> r. xval. xunfold MCount. hsimpl. { intros n'. xcf. xapp~. xapp. hsimpl~. } `````` charguer committed May 18, 2017 204 205 206 207 208 209 210 211 212 ``````Qed. Hint Extern 1 (Register_Spec val_mkcounter) => Provide Rule_mkcounter. (* ---------------------------------------------------------------------- *) (** Demo *) Definition trm_test_mkcounter : trm := `````` charguer committed Jan 18, 2018 213 214 215 216 `````` Let 'c := val_mkcounter '() in Let 'n := 'c '() in Let 'm := 'c '() in val_add 'n 'm. `````` charguer committed May 18, 2017 217 `````` `````` Jacques-Henri Jourdan committed Feb 07, 2018 218 219 220 ``````Lemma rule_test_mkcounter : Triple trm_test_mkcounter \[] `````` charguer committed May 18, 2017 221 `````` (fun r => \[r = 3]). `````` charguer committed May 22, 2017 222 ``````Proof using. `````` charguer committed Feb 27, 2018 223 224 `````` xcf_trm 100%nat. (* todo: make xcf work *) xapp as C. `````` charguer committed May 18, 2017 225 226 `````` xapps Rule_MCount. xapps Rule_MCount. `````` charguer committed May 22, 2017 227 228 `````` xapps. hsimpl~. `````` charguer committed May 18, 2017 229 ``Qed.``