ExampleHigherOrder.v 5.68 KB
Newer Older
charguer's avatar
charguer committed
1 2
(**

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
3
This file formalizes examples of first-class functions in plain
charguer's avatar
charguer committed
4 5 6 7 8 9 10 11
Separation Logic, using lifted characteristic formulae.

Author: Arthur Charguéraud.
License: MIT.

*)

Set Implicit Arguments.
charguer's avatar
charguer committed
12
From Sep Require Import Example.
charguer's avatar
charguer committed
13 14
Generalizable Variables A B.

charguer's avatar
charguer committed
15
Implicit Types p : loc.
charguer's avatar
charguer committed
16 17 18
Implicit Types n : int.


charguer's avatar
charguer committed
19 20 21 22

(* ********************************************************************** *)
(* * Apply function *)

charguer's avatar
charguer committed
23
Definition val_apply : val :=
charguer's avatar
charguer committed
24
  ValFun 'f 'x := ('f 'x).
charguer's avatar
charguer committed
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's avatar
charguer committed
30 31 32 33 34
Proof using.
  introv M. xcf. (* todo why not simplified? *)
    unfold Substs; simpl; rew_enc_dyn.
  xapp. hsimpl~.
Qed.
charguer's avatar
charguer committed
35

charguer's avatar
charguer committed
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's avatar
charguer committed
40 41
    POST Q.
Proof using. intros. xpull ;=> M. applys~ Rule_apply. Qed.
charguer's avatar
charguer committed
42 43 44 45



(* ********************************************************************** *)
charguer's avatar
charguer committed
46 47 48
(* * RefApply function *)

Definition val_refapply : val :=
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
49
  ValFun 'f 'r :=
charguer's avatar
charguer committed
50 51 52
    Let 'x := val_get 'r in
    Let 'y := 'f 'x in
    val_set 'r 'y.
charguer's avatar
charguer committed
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's avatar
Jacques-Henri Jourdan committed
57 58
    PRE \[]
    POST (fun y => \[P x y])
charguer's avatar
charguer committed
59
  ->
60
  Triple (val_refapply ``f ``r)
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
61
    PRE (r ~~> x)
charguer's avatar
charguer committed
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's avatar
Jacques-Henri Jourdan committed
70 71
    PRE H
    POST (fun y => \[P x y] \* H')
charguer's avatar
charguer committed
72
  ->
73
  Triple (val_refapply ``f ``r)
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
74
    PRE (r ~~> x \* H)
charguer's avatar
charguer committed
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's avatar
charguer committed
80 81 82


(* ********************************************************************** *)
charguer's avatar
charguer committed
83
(* * Twice function *)
charguer's avatar
charguer committed
84

charguer's avatar
charguer committed
85
Definition val_twice : val :=
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
86
  ValFun 'f :=
87
    'f '() ;;;
charguer's avatar
charguer committed
88
    'f '().
charguer's avatar
charguer committed
89

charguer's avatar
charguer committed
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's avatar
charguer committed
94 95 96
Proof using.
  introv M1 M2. xcf. xseq. xapp M1. xapp M2. hsimpl~.
Qed.
charguer's avatar
charguer committed
97 98 99


(* ********************************************************************** *)
charguer's avatar
charguer committed
100 101 102
(* * Repeat function *)

Definition val_repeat : val :=
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
103 104
  ValFun 'n 'f :=
    For 'i := 1 To 'n Do
charguer's avatar
charguer committed
105
      'f '()
charguer's avatar
charguer committed
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's avatar
charguer committed
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's avatar
charguer committed
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's avatar
charguer committed
131 132 133
       PRE (I i)
       POST (fun (_:unit) => I (i+1)))
  ->
134
  Triple (val_repeat ``n ``f)
charguer's avatar
charguer committed
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's avatar
charguer committed
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's avatar
Jacques-Henri Jourdan committed
144
  { intros i Hi. xapp. { math. } { math_rewrite (i-1+1=i+1-1). hsimpl. } }
charguer's avatar
charguer committed
145
  { math_rewrite (n+1-1=n). hsimpl. }
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
146
  (* todo : avoid math_rewrite,
charguer's avatar
charguer committed
147 148 149
     thanks to hsimpl simplification of invariants *)
Qed.

charguer's avatar
charguer committed
150 151

(* ********************************************************************** *)
charguer's avatar
charguer committed
152
(* * Iteration (iter, fold, map, find) on lists: see [ExampleList.v] *)
charguer's avatar
charguer committed
153 154


charguer's avatar
charguer committed
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's avatar
Jacques-Henri Jourdan committed
166 167
    \[ forall n', Triple (g val_unit)
                  (p ~~> n')
charguer's avatar
charguer committed
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's avatar
charguer committed
176

charguer's avatar
charguer committed
177
Lemma Rule_MCount : forall n g,
charguer's avatar
charguer committed
178
  Triple (g '()) (g ~> MCount n) (fun r => \[ r = n+1 ] \* g ~> MCount (n+1)).
charguer's avatar
charguer committed
179
Proof using.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
180
  intros. xunfolds MCount at 1 ;=> p Hg. xapp.
charguer's avatar
charguer committed
181
  hpulls. xunfold MCount. hsimpl~.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
182
Qed.
charguer's avatar
charguer committed
183 184 185 186 187 188


(* ---------------------------------------------------------------------- *)
(** Implementation *)

Definition val_mkcounter : val :=
charguer's avatar
charguer committed
189 190
  ValFun 'u :=
    Let 'p := val_ref 0 in
191
    (Fun 'v := val_incr 'p ;;; val_get 'p).
charguer's avatar
charguer committed
192 193 194 195 196


(* ---------------------------------------------------------------------- *)
(** Verification *)

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
197
Lemma Rule_mkcounter :
198
  Triple (val_mkcounter ``val_unit)
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
199
    \[]
charguer's avatar
charguer committed
200
    (fun g => g ~> MCount 0).
charguer's avatar
charguer committed
201
Proof using.
charguer's avatar
charguer committed
202 203
  xcf. xapps ;=> r. xval. xunfold MCount. hsimpl.
  { intros n'. xcf. xapp~. xapp. hsimpl~. }
charguer's avatar
charguer committed
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's avatar
charguer committed
213 214 215 216
  Let 'c := val_mkcounter '() in
  Let 'n := 'c '() in
  Let 'm := 'c '() in
  val_add 'n 'm.
charguer's avatar
charguer committed
217

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
218 219 220
Lemma rule_test_mkcounter :
  Triple trm_test_mkcounter
    \[]
charguer's avatar
charguer committed
221
    (fun r => \[r = 3]).
charguer's avatar
charguer committed
222
Proof using.
charguer's avatar
charguer committed
223 224
  xcf_trm 100%nat. (* todo: make xcf work *)
  xapp as C.
charguer's avatar
charguer committed
225 226
  xapps Rule_MCount.
  xapps Rule_MCount.
charguer's avatar
charguer committed
227 228
  xapps.
  hsimpl~.
charguer's avatar
charguer committed
229
Qed.