tactics.v 27.8 KB
Newer Older
Michael Sammler's avatar
Michael Sammler committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
From stdpp Require Import fin_maps.
From refinedc.lang Require Export notation.
Set Default Proof Using "Type".

Module W.
(*** Expressions *)
Section expr.
Local Unset Elimination Schemes.
Inductive expr :=
| Var (x : var_name)
| Loc (l : loc)
| Val (v : val)
| UnOp (op : un_op) (ot : op_type) (e : expr)
| BinOp (op : bin_op) (ot1 ot2 : op_type) (e1 e2 : expr)
15
| CopyAllocId (ot1 : op_type) (e1 e2 : expr)
Michael Sammler's avatar
Michael Sammler committed
16
| Deref (o : order) (ot : op_type) (e : expr)
Michael Sammler's avatar
Michael Sammler committed
17
| CAS (ot : op_type) (e1 e2 e3 : expr)
18
| Call (f : expr) (args : list expr)
Michael Sammler's avatar
Michael Sammler committed
19
| Concat (es : list expr)
Michael Sammler's avatar
Michael Sammler committed
20
| IfE (op : op_type) (e1 e2 e3 : expr)
Michael Sammler's avatar
Michael Sammler committed
21
22
23
| SkipE (e : expr)
| StuckE
(* new constructors *)
24
25
| LogicalAnd (ot1 ot2 : op_type) (e1 e2 : expr)
| LogicalOr (ot1 ot2 : op_type) (e1 e2 : expr)
Michael Sammler's avatar
Michael Sammler committed
26
| Use (o : order) (ot : op_type) (e : expr)
Michael Sammler's avatar
Michael Sammler committed
27
| AddrOf (e : expr)
Michael Sammler's avatar
Michael Sammler committed
28
| LValue (e : expr)
Michael Sammler's avatar
Michael Sammler committed
29
30
| GetMember (e : expr) (s : struct_layout) (m : var_name)
| GetMemberUnion (e : expr) (ul : union_layout) (m : var_name)
31
32
| OffsetOf (s : struct_layout) (m : var_name)
| OffsetOfUnion (ul : union_layout) (m : var_name)
Michael Sammler's avatar
Michael Sammler committed
33
34
35
| AnnotExpr (n : nat) {A} (a : A) (e : expr)
| LocInfoE (a : location_info) (e : expr)
| StructInit (ly : struct_layout) (fs : list (string * expr))
Michael Sammler's avatar
Michael Sammler committed
36
| MacroE (m : list lang.expr  lang.expr) (es : list expr) (wf : MacroWfSubst m)
Michael Sammler's avatar
Michael Sammler committed
37
38
39
40
41
42
43
44
45
46
47
(* for opaque expressions*)
| Expr (e : lang.expr)
.
End expr.

Lemma expr_ind (P : expr  Prop) :
  ( (x : var_name), P (Var x)) 
  ( (l : loc), P (Loc l)) 
  ( (v : val), P (Val v)) 
  ( (op : un_op) (ot : op_type) (e : expr), P e  P (UnOp op ot e)) 
  ( (op : bin_op) (ot1 ot2 : op_type) (e1 e2 : expr), P e1  P e2  P (BinOp op ot1 ot2 e1 e2)) 
48
  ( (ot1 : op_type) (e1 e2 : expr), P e1  P e2  P (CopyAllocId ot1 e1 e2)) 
Michael Sammler's avatar
Michael Sammler committed
49
  ( (o : order) (ot : op_type) (e : expr), P e  P (Deref o ot e)) 
Michael Sammler's avatar
Michael Sammler committed
50
  ( (ot : op_type) (e1 e2 e3 : expr), P e1  P e2  P e3  P (CAS ot e1 e2 e3)) 
51
  ( (f : expr) (args : list expr), P f  Forall P args  P (Call f args)) 
Michael Sammler's avatar
Michael Sammler committed
52
  ( (es : list expr), Forall P es  P (Concat es)) 
Michael Sammler's avatar
Michael Sammler committed
53
  ( (ot : op_type) (e1 e2 e3 : expr), P e1  P e2  P e3  P (IfE ot e1 e2 e3)) 
Michael Sammler's avatar
Michael Sammler committed
54
55
  ( (e : expr), P e  P (SkipE e)) 
  (P StuckE) 
56
57
  ( (ot1 ot2 : op_type) (e1 e2 : expr), P e1  P e2  P (LogicalAnd ot1 ot2 e1 e2)) 
  ( (ot1 ot2 : op_type) (e1 e2 : expr), P e1  P e2  P (LogicalOr ot1 ot2 e1 e2)) 
Michael Sammler's avatar
Michael Sammler committed
58
  ( (o : order) (ot : op_type) (e : expr), P e  P (Use o ot e)) 
Michael Sammler's avatar
Michael Sammler committed
59
  ( (e : expr), P e  P (AddrOf e)) 
Michael Sammler's avatar
Michael Sammler committed
60
  ( (e : expr), P e  P (LValue e)) 
Michael Sammler's avatar
Michael Sammler committed
61
62
  ( (e : expr) (s : struct_layout) (m : var_name), P e  P (GetMember e s m)) 
  ( (e : expr) (ul : union_layout) (m : var_name), P e  P (GetMemberUnion e ul m)) 
63
64
  ( (s : struct_layout) (m : var_name), P (OffsetOf s m)) 
  ( (ul : union_layout) (m : var_name), P (OffsetOfUnion ul m)) 
Michael Sammler's avatar
Michael Sammler committed
65
66
  ( (n : nat) (A : Type) (a : A) (e : expr), P e  P (AnnotExpr n a e)) 
  ( (a : location_info) (e : expr), P e  P (LocInfoE a e)) 
Michael Sammler's avatar
Michael Sammler committed
67
68
  ( (ly : struct_layout) (fs : list (string * expr)), Forall P fs.*2  P (StructInit ly fs)) 
  ( (m : list lang.expr  lang.expr) (es : list expr) (wf : MacroWfSubst m), Forall P es  P (MacroE m es wf)) 
Michael Sammler's avatar
Michael Sammler committed
69
70
71
  ( (e : lang.expr), P (Expr e))   (e : expr), P e.
Proof.
  move => *. generalize dependent P => P. match goal with | e : expr |- _ => revert e end.
72
  fix FIX 1. move => [ ^e] => ???????? Hcall Hconcat ?????????????? Hstruct Hmacro ?.
73
74
75
  9: {
    apply Hcall; [ |apply Forall_true => ?]; by apply: FIX.
  }
76
  9: {
Michael Sammler's avatar
Michael Sammler committed
77
78
    apply Hconcat. apply Forall_true => ?. by apply: FIX.
  }
79
  23: {
Michael Sammler's avatar
Michael Sammler committed
80
81
    apply Hstruct. apply Forall_fmap. apply Forall_true => ?. by apply: FIX.
  }
82
  23: {
Michael Sammler's avatar
Michael Sammler committed
83
84
    apply Hmacro. apply Forall_true => ?. by apply: FIX.
  }
Michael Sammler's avatar
Michael Sammler committed
85
86
87
88
89
90
91
92
93
94
  all: auto.
Qed.

Fixpoint to_expr (e : expr) : lang.expr :=
  match e with
  | Val v => v
  | Loc l => val_of_loc l
  | Var x => lang.Var x
  | UnOp op ot e  => lang.UnOp op ot (to_expr e)
  | BinOp op ot1 ot2 e1 e2 => lang.BinOp op ot1 ot2 (to_expr e1) (to_expr e2)
95
  | CopyAllocId ot1 e1 e2 => lang.CopyAllocId ot1 (to_expr e1) (to_expr e2)
Michael Sammler's avatar
Michael Sammler committed
96
  | Deref o ot e => lang.Deref o ot (to_expr e)
Michael Sammler's avatar
Michael Sammler committed
97
  | CAS ot e1 e2 e3 => lang.CAS ot (to_expr e1) (to_expr e2) (to_expr e3)
98
  | Call f args => lang.Call (to_expr f) (to_expr <$> args)
Michael Sammler's avatar
Michael Sammler committed
99
  | Concat es => lang.Concat (to_expr <$> es)
Michael Sammler's avatar
Michael Sammler committed
100
  | IfE ot e1 e2 e3 => lang.IfE ot (to_expr e1) (to_expr e2) (to_expr e3)
Michael Sammler's avatar
Michael Sammler committed
101
102
  | SkipE e => lang.SkipE (to_expr e)
  | StuckE => lang.StuckE
103
104
  | LogicalAnd ot1 ot2 e1 e2 => notation.LogicalAnd ot1 ot2 (to_expr e1) (to_expr e2)
  | LogicalOr ot1 ot2 e1 e2 => notation.LogicalOr ot1 ot2 (to_expr e1) (to_expr e2)
Michael Sammler's avatar
Michael Sammler committed
105
  | Use o ot e => notation.Use o ot (to_expr e)
Michael Sammler's avatar
Michael Sammler committed
106
  | AddrOf e => notation.AddrOf (to_expr e)
Michael Sammler's avatar
Michael Sammler committed
107
  | LValue e => notation.LValue (to_expr e)
Michael Sammler's avatar
Michael Sammler committed
108
109
110
111
112
  | AnnotExpr n a e => notation.AnnotExpr n a (to_expr e)
  | LocInfoE a e => notation.LocInfo a (to_expr e)
  | StructInit ly fs => notation.StructInit ly (prod_map id to_expr <$> fs)
  | GetMember e s m => notation.GetMember (to_expr e) s m
  | GetMemberUnion e ul m => notation.GetMemberUnion (to_expr e) ul m
113
114
  | OffsetOf s m => notation.OffsetOf s m
  | OffsetOfUnion ul m => notation.OffsetOfUnion ul m
Michael Sammler's avatar
Michael Sammler committed
115
  | MacroE m es _ => notation.MacroE m (to_expr <$> es)
Michael Sammler's avatar
Michael Sammler committed
116
117
118
119
120
121
122
123
124
125
126
  | Expr e => e
  end.

Ltac of_expr e :=
  lazymatch e with
  | [] => constr:(@nil expr)
  | ?e :: ?es =>
    let e := of_expr e in
    let es := of_expr es in
    constr:(e :: es)

127
  | lang.Val (val.val_of_loc ?l) => constr:(Loc l)
Michael Sammler's avatar
Michael Sammler committed
128
129
  | notation.AddrOf ?e =>
    let e := of_expr e in constr:(AddrOf e)
Michael Sammler's avatar
Michael Sammler committed
130
131
  | notation.LValue ?e =>
    let e := of_expr e in constr:(LValue e)
Michael Sammler's avatar
Michael Sammler committed
132
133
  | notation.AnnotExpr ?n ?a ?e =>
    let e := of_expr e in constr:(AnnotExpr n a e)
Michael Sammler's avatar
Michael Sammler committed
134
135
  | notation.MacroE ?m ?es =>
    let es := of_expr es in constr:(MacroE m es _)
Michael Sammler's avatar
Michael Sammler committed
136
137
138
139
140
141
142
143
  | notation.LocInfo ?a ?e =>
    let e := of_expr e in constr:(LocInfoE a e)
  | notation.StructInit ?ly ?fs =>
    let fs := of_field_expr fs in constr:(StructInit ly fs)
  | notation.GetMember ?e ?s ?m =>
    let e := of_expr e in constr:(GetMember e s m)
  | notation.GetMemberUnion ?e ?ul ?m =>
    let e := of_expr e in constr:(GetMemberUnion e ul m)
144
145
  | notation.OffsetOf ?s ?m => constr:(OffsetOf s m)
  | notation.OffsetOfUnion ?ul ?m => constr:(OffsetOfUnion ul m)
146
147
148
149
150
151
152
153
  | notation.LogicalAnd ?ot1 ?ot2 ?e1 ?e2 =>
    let e1 := of_expr e1 in
    let e2 := of_expr e2 in
    constr:(LogicalAnd ot1 ot2 e1 e2)
  | notation.LogicalOr ?ot1 ?ot2 ?e1 ?e2 =>
    let e1 := of_expr e1 in
    let e2 := of_expr e2 in
    constr:(LogicalOr ot1 ot2 e1 e2)
Michael Sammler's avatar
Michael Sammler committed
154
155
  | notation.Use ?o ?ot ?e =>
    let e := of_expr e in constr:(Use o ot e)
Michael Sammler's avatar
Michael Sammler committed
156
157
158
159
160
161
  | lang.Val ?x => constr:(Val x)
  | lang.Var ?x => constr:(Var x)
  | lang.UnOp ?op ?ot ?e =>
    let e := of_expr e in constr:(UnOp op ot e)
  | lang.BinOp ?op ?ot1 ?ot2 ?e1 ?e2 =>
    let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(BinOp op ot1 ot2 e1 e2)
162
163
  | lang.CopyAllocId ?ot1 ?e1 ?e2 =>
    let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(CopyAllocId ot1 e1 e2)
Michael Sammler's avatar
Michael Sammler committed
164
165
  | lang.Deref ?o ?ot ?e =>
    let e := of_expr e in constr:(Deref o ot e)
Michael Sammler's avatar
Michael Sammler committed
166
167
  | lang.CAS ?ot ?e1 ?e2 ?e3 =>
    let e1 := of_expr e1 in let e2 := of_expr e2 in let e3 := of_expr e3 in constr:(CAS ot e1 e2 e3)
168
169
170
  | lang.Call ?f ?args =>
    let f := of_expr f in
    let args := of_expr args in constr:(Call f args)
Michael Sammler's avatar
Michael Sammler committed
171
172
  | lang.Concat ?es =>
    let es := of_expr es in constr:(Concat es)
Michael Sammler's avatar
Michael Sammler committed
173
174
175
176
177
  | lang.IfE ?ot ?e1 ?e2 ?e3 =>
    let e1 := of_expr e1 in
    let e2 := of_expr e2 in
    let e3 := of_expr e3 in
    constr:(IfE ot e1 e2 e3)
Michael Sammler's avatar
Michael Sammler committed
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
  | lang.SkipE ?e =>
    let e := of_expr e in constr:(SkipE e)
  | lang.StuckE => constr:(StuckE e)
  | _ => constr:(Expr e)
  end
with of_field_expr fs :=
  lazymatch fs with
  | [] => constr:(@nil (string * expr))
  | (?id, ?e) :: ?fs =>
    let e := of_expr e in
    let fs := of_field_expr fs in
    constr:((id, e) :: fs)
  end.

Inductive ectx_item :=
| UnOpCtx (op : un_op) (ot : op_type)
| BinOpLCtx (op : bin_op) (ot1 ot2 : op_type) (e2 : expr)
| BinOpRCtx (op : bin_op) (ot1 ot2 : op_type) (v1 : val)
196
197
| CopyAllocIdLCtx (ot1 : op_type) (e2 : expr)
| CopyAllocIdRCtx (ot1 : op_type) (v1 : val)
Michael Sammler's avatar
Michael Sammler committed
198
| DerefCtx (o : order) (l : op_type)
Michael Sammler's avatar
Michael Sammler committed
199
200
201
| CASLCtx (ot : op_type) (e2 e3 : expr)
| CASMCtx (ot : op_type) (v1 : val) (e3 : expr)
| CASRCtx (ot : op_type) (v1 v2 : val)
202
203
| CallLCtx (args : list expr)
| CallRCtx (f : val) (vl : list val) (el : list expr)
Michael Sammler's avatar
Michael Sammler committed
204
| ConcatCtx (vs : list val) (es : list expr)
Michael Sammler's avatar
Michael Sammler committed
205
| IfECtx (ot : op_type) (e2 e3 : expr)
Michael Sammler's avatar
Michael Sammler committed
206
207
| SkipECtx
(* new constructors *)
Michael Sammler's avatar
Michael Sammler committed
208
| UseCtx (o : order) (ot : op_type)
Michael Sammler's avatar
Michael Sammler committed
209
| AddrOfCtx
Michael Sammler's avatar
Michael Sammler committed
210
| LValueCtx
Michael Sammler's avatar
Michael Sammler committed
211
212
213
214
215
216
217
218
219
220
221
222
223
| AnnotExprCtx (n : nat) {A} (a : A)
| LocInfoECtx (a : location_info)
(* the following would not work, thus we don't have a context, but prove a specialized bind rule*)
(*| StructInitCtx (ly : struct_layout) (vfs : list (string * val)) (id : string) (efs : list (string * expr))*)
| GetMemberCtx (s : struct_layout) (m : var_name)
| GetMemberUnionCtx (ul : union_layout) (m : var_name)
.

Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
  match Ki with
  | UnOpCtx op ot => UnOp op ot e
  | BinOpLCtx op ot1 ot2 e2 => BinOp op ot1 ot2 e e2
  | BinOpRCtx op ot1 ot2 v1 => BinOp op ot1 ot2 (Val v1) e
224
225
  | CopyAllocIdLCtx ot1 e2 => CopyAllocId ot1 e e2
  | CopyAllocIdRCtx ot1 v1 => CopyAllocId ot1 (Val v1) e
Michael Sammler's avatar
Michael Sammler committed
226
227
228
229
  | DerefCtx o l => Deref o l e
  | CASLCtx ot e2 e3 => CAS ot e e2 e3
  | CASMCtx ot v1 e3 => CAS ot (Val v1) e e3
  | CASRCtx ot v1 v2 => CAS ot (Val v1) (Val v2) e
230
231
  | CallLCtx args => Call e args
  | CallRCtx f vl el => Call (Val f) ((Val <$> vl) ++ e :: el)
Michael Sammler's avatar
Michael Sammler committed
232
  | ConcatCtx vs es => Concat ((Val <$> vs) ++ e :: es)
Michael Sammler's avatar
Michael Sammler committed
233
  | IfECtx ot e2 e3 => IfE ot e e2 e3
Michael Sammler's avatar
Michael Sammler committed
234
235
236
  | SkipECtx => SkipE e
  | UseCtx o l => Use o l e
  | AddrOfCtx => AddrOf e
Michael Sammler's avatar
Michael Sammler committed
237
  | LValueCtx => LValue e
Michael Sammler's avatar
Michael Sammler committed
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
  | AnnotExprCtx n a => AnnotExpr n a e
  | LocInfoECtx a => LocInfoE a e
  | GetMemberCtx s m => GetMember e s m
  | GetMemberUnionCtx ul m => GetMemberUnion e ul m
  end.

Definition fill (K : list ectx_item) (e : expr) : expr := foldl (flip fill_item) e K.
Lemma fill_app (K1 K2 : list ectx_item) e : fill (K1 ++ K2) e = fill K2 (fill K1 e).
Proof. apply foldl_app. Qed.

Fixpoint find_expr_fill (e : expr) (bind_val : bool) : option (list ectx_item * expr) :=
  match e with
  | Var _ => None
  | Val v => if bind_val then Some ([], Val v) else None
  | Loc l => if bind_val then Some ([], Loc l) else None
  | Expr e => Some ([], Expr e)
  | StuckE => Some ([], StuckE)
  | UnOp op ot e1 =>
    if find_expr_fill e1 bind_val is Some (Ks, e') then
      Some (Ks ++ [UnOpCtx op ot], e') else Some ([], e)
  | BinOp op ot1 ot2 e1 e2 =>
    if find_expr_fill e1 bind_val is Some (Ks, e') then
      Some (Ks ++ [BinOpLCtx op ot1 ot2 e2], e')
    else if find_expr_fill e2 bind_val is Some (Ks, e') then
           if e1 is Val v then Some (Ks ++ [BinOpRCtx op ot1 ot2 v], e') else None
         else Some ([], e)
264
  | CopyAllocId ot1 e1 e2 =>
265
    if find_expr_fill e1 bind_val is Some (Ks, e') then
266
      Some (Ks ++ [CopyAllocIdLCtx ot1 e2], e')
267
    else if find_expr_fill e2 bind_val is Some (Ks, e') then
268
           if e1 is Val v then Some (Ks ++ [CopyAllocIdRCtx ot1 v], e') else None
269
         else Some ([], e)
Michael Sammler's avatar
Michael Sammler committed
270
271
272
273
274
275
276
277
  | CAS ot e1 e2 e3 =>
    if find_expr_fill e1 bind_val is Some (Ks, e') then
      Some (Ks ++ [CASLCtx ot e2 e3], e')
    else if find_expr_fill e2 bind_val is Some (Ks, e') then
      if e1 is Val v1 then Some (Ks ++ [CASMCtx ot v1 e3], e') else None
    else if find_expr_fill e3 bind_val is Some (Ks, e') then
      if e1 is Val v1 then if e2 is Val v2 then Some (Ks ++ [CASRCtx ot v1 v2], e') else None else None
    else Some ([], e)
278
279
280
281
  | Call f args =>
    if find_expr_fill f bind_val is Some (Ks, e') then
      Some (Ks ++ [CallLCtx args], e') else
      (* TODO: handle arguments? *) None
282
  | Concat _ | MacroE _ _ _ | OffsetOf _ _ | OffsetOfUnion _ _ | LogicalAnd _ _ _ _ | LogicalOr _ _ _ _ => None
Michael Sammler's avatar
Michael Sammler committed
283
284
285
  | IfE ot e1 e2 e3 =>
    if find_expr_fill e1 bind_val is Some (Ks, e') then
      Some (Ks ++ [IfECtx ot e2 e3], e') else Some ([], e)
Michael Sammler's avatar
Michael Sammler committed
286
287
288
289
290
291
292
293
294
  | SkipE e1 =>
    if find_expr_fill e1 bind_val is Some (Ks, e') then
      Some (Ks ++ [SkipECtx], e') else Some ([], e)
  | Deref o ly e1 => if find_expr_fill e1 bind_val is Some (Ks, e') then
      Some (Ks ++ [DerefCtx o ly], e') else Some ([], e)
  | Use o ly e1 => if find_expr_fill e1 bind_val is Some (Ks, e') then
      Some (Ks ++ [UseCtx o ly], e') else Some ([], e)
  | AddrOf e1 => if find_expr_fill e1 bind_val is Some (Ks, e') then
      Some (Ks ++ [AddrOfCtx], e') else Some ([], e)
Michael Sammler's avatar
Michael Sammler committed
295
296
  | LValue e1 => if find_expr_fill e1 bind_val is Some (Ks, e') then
      Some (Ks ++ [LValueCtx], e') else Some ([], e)
Michael Sammler's avatar
Michael Sammler committed
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
  | AnnotExpr n a e1 => if find_expr_fill e1 bind_val is Some (Ks, e') then
      Some (Ks ++ [AnnotExprCtx n a], e') else Some ([], e)
  | LocInfoE a e1 => if find_expr_fill e1 bind_val is Some (Ks, e') then
      Some (Ks ++ [LocInfoECtx a], e') else Some ([], e)
  | StructInit _ _ => None
  | GetMember e1 s m => if find_expr_fill e1 bind_val is Some (Ks, e') then
      Some (Ks ++ [GetMemberCtx s m], e') else Some ([], e)
  | GetMemberUnion e1 ul m => if find_expr_fill e1 bind_val is Some (Ks, e') then
      Some (Ks ++ [GetMemberUnionCtx ul m], e') else Some ([], e)
  end.

Lemma find_expr_fill_correct b e Ks e':
  find_expr_fill e b = Some (Ks, e')  e = fill Ks e'.
Proof.
  elim: e Ks e' => //= *;
     repeat (try case_match; simpl in *; simplify_eq => /=);
     rewrite ?fill_app /=; f_equal; eauto.
Qed.

Lemma ectx_item_correct Ks:
317
   Ks',  e, to_rtexpr (to_expr (fill Ks e)) = ectxi_language.fill Ks' (to_rtexpr (to_expr e)).
Michael Sammler's avatar
Michael Sammler committed
318
319
320
Proof.
  elim/rev_ind: Ks. by exists [].
  move => K Ks [Ks' IH].
321
322
323
324
325
  eexists (Ks' ++ (ExprCtx <$> ?[K])) => ?. rewrite fill_app ectxi_language.fill_app /= -IH.
  only [K]: (destruct K; [
    apply: [lang.UnOpCtx _ _]|
    apply: [lang.BinOpLCtx _ _ _ _]|
    apply: [lang.BinOpRCtx _ _ _ _]|
326
327
    apply: [lang.CopyAllocIdLCtx _ _]|
    apply: [lang.CopyAllocIdRCtx _ _]|
328
329
330
331
332
333
334
    apply: [lang.DerefCtx _ _]|
    apply: [lang.CASLCtx _ _ _]|
    apply: [lang.CASMCtx _ _ _]|
    apply: [lang.CASRCtx _ _ _]|
    apply: [lang.CallLCtx _]|
    apply: [lang.CallRCtx _ _ _]|
    apply: [lang.ConcatCtx _ _]|
Michael Sammler's avatar
Michael Sammler committed
335
    apply: [lang.IfECtx _ _ _]|
336
337
338
339
340
341
342
343
344
    apply: [lang.SkipECtx]|
    apply: [lang.DerefCtx _ _]|
    apply: []|
    apply: []|
    apply: (replicate n lang.SkipECtx)|
    apply: []|
    apply: [lang.BinOpRCtx _ _ _ _]|
    apply: []|..
  ]).
Michael Sammler's avatar
Michael Sammler committed
345
  move: K => [|||||||||||||||||n|||] * //=.
346
347
348
349
  - (** Call *)
    do 2 f_equal.
    rewrite !fmap_app !fmap_cons. repeat f_equal; eauto.
    rewrite -!list_fmap_compose. by apply: list_fmap_ext.
Michael Sammler's avatar
Michael Sammler committed
350
  - (** Concat *)
351
352
353
    do 2 f_equal.
    rewrite !fmap_app !fmap_cons. repeat f_equal; eauto.
    rewrite -!list_fmap_compose. by apply: list_fmap_ext.
Michael Sammler's avatar
Michael Sammler committed
354
  - (** AnnotExpr *)
355
356
    elim: n; eauto.
    move => n. by rewrite /notation.AnnotExpr replicate_S_end fmap_app ectxi_language.fill_app /= => ->.
Michael Sammler's avatar
Michael Sammler committed
357
358
359
360
361
362
363
364
365
366
367
Qed.

Lemma to_expr_val_list (vl : list val) :
  to_expr <$> (Val <$> vl) = lang.Val <$> vl.
Proof. elim: vl => //; csimpl => *. by f_equal. Qed.

(*** Statements *)

Section stmt.
Local Unset Elimination Schemes.
Inductive stmt :=
368
| Goto (b : label)
Michael Sammler's avatar
Michael Sammler committed
369
| Return (e : expr)
370
| IfS (ot : op_type) (e : expr) (s1 s2 : stmt)
Michael Sammler's avatar
Michael Sammler committed
371
| Switch (it : int_type) (e : expr) (m : gmap Z nat) (bs : list stmt) (def : stmt)
Michael Sammler's avatar
Michael Sammler committed
372
| Assign (o : order) (ot : op_type) (e1 e2 : expr) (s : stmt)
Michael Sammler's avatar
Michael Sammler committed
373
374
375
376
| SkipS (s : stmt)
| StuckS
| ExprS (e : expr) (s : stmt)

377
| Assert (ot : op_type) (e : expr) (s : stmt)
Michael Sammler's avatar
Michael Sammler committed
378
379
380
381
382
383
384
| AnnotStmt (n : nat) {A} (a : A) (s : stmt)
| LocInfoS (a : location_info) (s : stmt)
(* for opaque statements *)
| Stmt (s : lang.stmt).
End stmt.

Lemma stmt_ind (P : stmt  Prop):
385
  ( b : label, P (Goto b)) 
Michael Sammler's avatar
Michael Sammler committed
386
  ( e : expr, P (Return e)) 
387
  ( (ot : op_type) (e : expr) (s1 : stmt), P s1   s2 : stmt, P s2  P (IfS ot e s1 s2)) 
Michael Sammler's avatar
Michael Sammler committed
388
  ( (it : int_type) (e : expr) (m : gmap Z nat) (bs : list stmt) (def : stmt), P def  Forall P bs  P (Switch it e m bs def)) 
Michael Sammler's avatar
Michael Sammler committed
389
  ( (o : order) (ot : op_type) (e1 e2 : expr) (s : stmt), P s  P (Assign o ot e1 e2 s)) 
Michael Sammler's avatar
Michael Sammler committed
390
391
392
  ( s : stmt, P s  P (SkipS s)) 
  (P StuckS) 
  ( (e : expr) (s : stmt), P s  P (ExprS e s)) 
393
  ( (ot : op_type) (e : expr) (s : stmt), P s  P (Assert ot e s)) 
Michael Sammler's avatar
Michael Sammler committed
394
395
396
397
398
  ( (n : nat) (A : Type) (a : A) (s : stmt), P s  P (AnnotStmt n a s)) 
  ( (a : location_info) (s : stmt), P s  P (LocInfoS a s)) 
  ( s : lang.stmt, P (Stmt s))   s : stmt, P s.
Proof.
  move => *. generalize dependent P => P. match goal with | s : stmt |- _ => revert s end.
399
  fix FIX 1. move => [ ^s] ??? Hswitch *. 4: {
Michael Sammler's avatar
Michael Sammler committed
400
401
402
403
404
405
406
407
408
409
    apply Hswitch; first by apply: FIX. elim: sbs; auto.
  }
  all: auto.
Qed.


Fixpoint to_stmt (s : stmt) : lang.stmt :=
  match s with
  | Goto b => lang.Goto b
  | Return e => lang.Return (to_expr e)
410
  | IfS ot e s1 s2 => (if{ot}: to_expr e then to_stmt s1 else to_stmt s2)%E
Michael Sammler's avatar
Michael Sammler committed
411
  | Switch it e m bs def => lang.Switch it (to_expr e) m (to_stmt <$> bs) (to_stmt def)
Michael Sammler's avatar
Michael Sammler committed
412
  | Assign o ot e1 e2 s => lang.Assign o ot (to_expr e1) (to_expr e2) (to_stmt s)
Michael Sammler's avatar
Michael Sammler committed
413
414
415
  | SkipS s => lang.SkipS (to_stmt s)
  | StuckS => lang.StuckS
  | ExprS e s => lang.ExprS (to_expr e) (to_stmt s)
416
  | Assert ot e s => (assert{ot}: to_expr e; to_stmt s)%E
Michael Sammler's avatar
Michael Sammler committed
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
  | AnnotStmt n a s => notation.AnnotStmt n a (to_stmt s)
  | LocInfoS a s => notation.LocInfo a (to_stmt s)
  | Stmt s => s
  end.

Ltac of_stmt s :=
  lazymatch s with
  | [] => constr:(@nil stmt)
  | ?s :: ?ss =>
    let s := of_stmt s in
    let ss := of_stmt ss in
    constr:(s :: ss)

  | notation.AnnotStmt ?n ?a ?s =>
    let s := of_stmt s in
    constr:(AnnotStmt n a s)
  | notation.LocInfo ?a ?s =>
    let s := of_stmt s in
    constr:(LocInfoS a s)
436
  | (assert{?ot}: ?e ; ?s)%E =>
Michael Sammler's avatar
Michael Sammler committed
437
438
    let e := of_expr e in
    let s := of_stmt s in
439
440
    constr:(Assert ot e s)
  | (if{?ot}: ?e then ?s1 else ?s2)%E =>
Michael Sammler's avatar
Michael Sammler committed
441
442
443
    let e := of_expr e in
    let s1 := of_stmt s1 in
    let s2 := of_stmt s2 in
444
    constr:(IfS ot e s1 s2)
Michael Sammler's avatar
Michael Sammler committed
445
446
447
448
449
450
451
452
  | lang.Goto ?b => constr:(Goto b)
  | lang.Return ?e =>
    let e := of_expr e in constr:(Return e)
  | lang.Switch ?it ?e ?m ?bs ?def =>
    let e := of_expr e in
    let bs := of_stmt bs in
    let def := of_stmt def in
    constr:(Switch it e m bs def)
Michael Sammler's avatar
Michael Sammler committed
453
  | lang.Assign ?o ?ot ?e1 ?e2 ?s =>
Michael Sammler's avatar
Michael Sammler committed
454
455
456
    let e1 := of_expr e1 in
    let e2 := of_expr e2 in
    let s := of_stmt s in
Michael Sammler's avatar
Michael Sammler committed
457
    constr:(Assign o ot e1 e2 s)
Michael Sammler's avatar
Michael Sammler committed
458
459
460
461
462
463
464
465
466
467
468
469
  | lang.SkipS ?s =>
    let s := of_stmt s in
    constr:(SkipS s)
  | lang.StuckS => constr:(StuckS s)
  | lang.ExprS ?e ?s =>
    let e := of_expr e in
    let s := of_stmt s in
    constr:(ExprS e s)
  | _ => constr:(Stmt s)
  end.

Inductive stmt_ectx :=
Michael Sammler's avatar
Michael Sammler committed
470
471
| AssignRCtx (o : order) (ot : op_type) (e1 : expr) (s : stmt)
| AssignLCtx (o : order) (ot : op_type) (v2 : val) (s : stmt)
Michael Sammler's avatar
Michael Sammler committed
472
| ReturnCtx
473
| IfSCtx (ot : op_type) (s1 s2 : stmt)
Michael Sammler's avatar
Michael Sammler committed
474
475
| SwitchCtx (it : int_type) (m: gmap Z nat) (bs : list stmt) (def : stmt)
| ExprSCtx (s : stmt)
476
| AssertCtx (ot : op_type) (s : stmt)
Michael Sammler's avatar
Michael Sammler committed
477
478
479
480
.

Definition stmt_fill (Ki : stmt_ectx) (e : expr) : stmt :=
  match Ki with
Michael Sammler's avatar
Michael Sammler committed
481
482
  | AssignRCtx o ot e1 s => Assign o ot e1 e s
  | AssignLCtx o ot v2 s => Assign o ot e (Val v2) s
Michael Sammler's avatar
Michael Sammler committed
483
484
  | ReturnCtx => Return e
  | ExprSCtx s => ExprS e s
485
  | IfSCtx ot s1 s2 => IfS ot e s1 s2
Michael Sammler's avatar
Michael Sammler committed
486
  | SwitchCtx it m bs def => Switch it e m bs def
487
  | AssertCtx ot s => Assert ot e s
Michael Sammler's avatar
Michael Sammler committed
488
489
490
491
492
493
494
  end.

Definition find_stmt_fill (s : stmt) : option (stmt_ectx * expr) :=
  match s with
  | Goto _ | Stmt _ | AnnotStmt _ _ _ | LocInfoS _ _ | SkipS _ | StuckS => None
  | Return e => if e is (Val v) then None else Some (ReturnCtx, e)
  | ExprS e s => if e is (Val v) then None else Some (ExprSCtx s, e)
495
  | IfS ot e s1 s2 => if e is (Val v) then None else Some (IfSCtx ot s1 s2, e)
Michael Sammler's avatar
Michael Sammler committed
496
  | Switch it e m bs def => if e is (Val v) then None else Some (SwitchCtx it m bs def, e)
Michael Sammler's avatar
Michael Sammler committed
497
  | Assign o ot e1 e2 s => if e2 is (Val v) then if e1 is (Val v) then None else Some (AssignLCtx o ot v s, e1) else Some (AssignRCtx o ot e1 s, e2)
498
  | Assert ot e s => if e is (Val v) then None else Some (AssertCtx ot s, e)
Michael Sammler's avatar
Michael Sammler committed
499
500
501
502
503
504
505
506
  end.

Lemma find_stmt_fill_correct s Ks e:
  find_stmt_fill s = Some (Ks, e)  s = stmt_fill Ks e.
Proof.
  destruct s => *; repeat (try case_match; simpl in *; simplify_eq => //).
Qed.

507
508
Lemma stmt_fill_correct Ks rf:
   Ks',  e, to_rtstmt rf (to_stmt (stmt_fill Ks e)) = ectxi_language.fill Ks' (to_rtexpr (to_expr e)).
Michael Sammler's avatar
Michael Sammler committed
509
510
Proof.
  move: Ks => [] *; [
511
512
513
  eexists ([StmtCtx (lang.AssignRCtx _ _ _ _) rf])|
  eexists ([StmtCtx (lang.AssignLCtx _ _ _ _) rf])|
  eexists ([StmtCtx (lang.ReturnCtx) rf])|
514
  eexists ([StmtCtx (lang.IfSCtx _ _ _) rf])|
515
516
  eexists ([StmtCtx (lang.SwitchCtx _ _ _ _) rf])|
  eexists ([StmtCtx (lang.ExprSCtx _) rf])|
517
  eexists ([StmtCtx (lang.IfSCtx _ _ _) rf])|
518
..] => //=.
Michael Sammler's avatar
Michael Sammler committed
519
520
521
Qed.

(*** Substitution *)
Michael Sammler's avatar
Michael Sammler committed
522
Fixpoint subst_l (xs : list (var_name * val)) (e : expr)  : expr :=
Michael Sammler's avatar
Michael Sammler committed
523
  match e with
Michael Sammler's avatar
Michael Sammler committed
524
  | Var y => if list_find (λ x, x.1 = y) xs is Some (_, (_, v)) then Val v else Var y
Michael Sammler's avatar
Michael Sammler committed
525
526
  | Loc l => Loc l
  | Val v => Val v
Michael Sammler's avatar
Michael Sammler committed
527
528
  | UnOp op ot e => UnOp op ot (subst_l xs e)
  | BinOp op ot1 ot2 e1 e2 => BinOp op ot1 ot2 (subst_l xs e1) (subst_l xs e2)
529
  | CopyAllocId ot1 e1 e2 => CopyAllocId ot1 (subst_l xs e1) (subst_l xs e2)
Michael Sammler's avatar
Michael Sammler committed
530
531
532
533
  | Deref o l e => Deref o l (subst_l xs e)
  | CAS ot e1 e2 e3 => CAS ot (subst_l xs e1) (subst_l xs e2) (subst_l xs e3)
  | Call f args => Call (subst_l xs f) (subst_l xs <$> args)
  | Concat es => Concat (subst_l xs <$> es)
Michael Sammler's avatar
Michael Sammler committed
534
  | IfE ot e1 e2 e3 => IfE ot (subst_l xs e1) (subst_l xs e2) (subst_l xs e3)
Michael Sammler's avatar
Michael Sammler committed
535
  | SkipE e => SkipE (subst_l xs e)
Michael Sammler's avatar
Michael Sammler committed
536
  | StuckE => StuckE
537
538
  | LogicalAnd ot1 ot2 e1 e2 => LogicalAnd ot1 ot2 (subst_l xs e1) (subst_l xs e2)
  | LogicalOr ot1 ot2 e1 e2 => LogicalOr ot1 ot2 (subst_l xs e1) (subst_l xs e2)
Michael Sammler's avatar
Michael Sammler committed
539
  | Use o ot e => Use o ot (subst_l xs e)
Michael Sammler's avatar
Michael Sammler committed
540
541
542
543
544
545
546
  | AddrOf e => AddrOf (subst_l xs e)
  | LValue e => LValue (subst_l xs e)
  | AnnotExpr n a e => AnnotExpr n a (subst_l xs e)
  | LocInfoE a e => LocInfoE a (subst_l xs e)
  | StructInit ly fs => StructInit ly (prod_map id (subst_l xs) <$> fs)
  | GetMember e s m => GetMember (subst_l xs e) s m
  | GetMemberUnion e ul m => GetMemberUnion (subst_l xs e) ul m
547
548
  | OffsetOf s m => OffsetOf s m
  | OffsetOfUnion ul m => OffsetOfUnion ul m
Michael Sammler's avatar
Michael Sammler committed
549
550
  | MacroE m es wf => MacroE m (subst_l xs <$> es) wf
  | Expr e => Expr (lang.subst_l xs e)
Michael Sammler's avatar
Michael Sammler committed
551
552
553
  end.

Lemma to_expr_subst x v e :
Michael Sammler's avatar
Michael Sammler committed
554
  to_expr (subst_l [(x, v)] e) = lang.subst x v (to_expr e).
Michael Sammler's avatar
Michael Sammler committed
555
Proof.
Michael Sammler's avatar
Michael Sammler committed
556
  elim: e => *//; cbn -[notation.GetMember]; (repeat case_bool_decide) => //=; f_equal; eauto; try by case_decide.
557
558
  - (** Call *)
    rewrite -!list_fmap_compose. apply list_fmap_ext' => //. by apply Forall_forall.
Michael Sammler's avatar
Michael Sammler committed
559
560
  - (** Concat *)
    rewrite -!list_fmap_compose. apply list_fmap_ext' => //. by apply Forall_forall.
561
562
563
564
  - (** LogicalAnd *)
    rewrite /notation.LogicalAnd/=. do 2 f_equal; eauto.
  - (** LogicalOr *)
    rewrite /notation.LogicalOr/=. do 2 f_equal; eauto.
Michael Sammler's avatar
Michael Sammler committed
565
566
567
568
  - (** GetMember *)
    match goal with
    | _ : ?e1 = ?e2 |- _ => assert (e1 = e2) as -> by assumption
    end; done.
569
570
  - rewrite /notation.OffsetOf/=.
    match goal with | |- context [offset_of ?s ?m] => destruct (offset_of s m) end => //=.
571
    by match goal with | |- context [val_of_Z ?o ?it] => destruct (val_of_Z o it) end.
Michael Sammler's avatar
Michael Sammler committed
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
  - (** AnnotExpr *)
    match goal with
    | |- notation.AnnotExpr ?n _ _ = _ => generalize dependent n
    end.
    by rewrite /notation.AnnotExpr; elim; eauto => /= n ->.
  - (** StructInit *)
    match goal with | H : struct_layout |- _ => rename H into sl end.
    match goal with | H : list (string * expr) |- _ => rename H into fs end.
    rewrite /notation.StructInit; f_equal.
    generalize dependent fs.
    induction (sl_members sl) as [|[f ly] ? IHfs]; first done. move => fs Hf.
    rewrite fmap_cons IHfs //=; clear IHfs; f_equal.
    rewrite [X in _ = X]apply_default /=. f_equal. destruct f as [f|] => //=.
    rewrite !list_to_map_fmap !lookup_fmap. destruct (list_to_map fs !! f) as [e|] eqn:H; simpl; last done.
    f_equal. move: Hf => /Forall_forall IH. apply (IH _).
    simplify_eq. apply elem_of_list_to_map_2 in H. set_solver.
Michael Sammler's avatar
Michael Sammler committed
588
589
590
  - (** MacroE *)
    rewrite /notation.MacroE macro_wf_subst. f_equal.
    rewrite -!list_fmap_compose. apply list_fmap_ext' => //. by apply Forall_forall.
Michael Sammler's avatar
Michael Sammler committed
591
592
Qed.

Michael Sammler's avatar
Michael Sammler committed
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
Lemma Forall_eq_fmap {A B} (xs : list A) (f1 f2 : A  B) :
  Forall (λ x, f1 x = f2 x) xs  f1 <$> xs = f2 <$> xs.
Proof. elim => //. csimpl. congruence. Qed.

Lemma fmap_snd_prod_map {A B C} (l : list (A * B)) (f1 f2 : B  C)  :
  f1 <$> l.*2 = f2 <$> l.*2 
  prod_map id f1 <$> l = prod_map id f2 <$> l.
Proof. elim: l => // -[??] ? IH. csimpl => -[??]. rewrite IH //. congruence. Qed.

Lemma to_expr_subst_l xs e :
  to_expr (subst_l xs e) = lang.subst_l xs (to_expr e).
Proof.
  elim: xs e => //=.
  - elim => //= >; try congruence; try move => ->.
    all: try move => /Forall_eq_fmap; try move/fmap_snd_prod_map.
    all: by move => <-; by rewrite -list_fmap_compose.
  - move => [x v] xs IH e. rewrite -to_expr_subst -IH. f_equal.
    elim: e => //= >; try congruence; try move => ->.
    all: try move => /Forall_eq_fmap; try move/fmap_snd_prod_map.
    all: try by move => ->; by rewrite -list_fmap_compose.
    case_decide => //. rewrite /subst_l.
    by match goal with | |- context [list_find ?f ?xs] => destruct (list_find f xs) as [[?[??]]|] end.
Qed.
Michael Sammler's avatar
Michael Sammler committed
616

Michael Sammler's avatar
Michael Sammler committed
617
Fixpoint subst_stmt (xs : list (var_name * val)) (s : stmt) : stmt :=
Michael Sammler's avatar
Michael Sammler committed
618
619
  match s with
  | Goto b => Goto b
Michael Sammler's avatar
Michael Sammler committed
620
  | Return e => Return (subst_l xs e)
621
  | IfS ot e s1 s2 => IfS ot (subst_l xs e) (subst_stmt xs s1) (subst_stmt xs s2)
Michael Sammler's avatar
Michael Sammler committed
622
  | Switch it e m' bs def => Switch it (subst_l xs e) m' (subst_stmt xs <$> bs) (subst_stmt xs def)
Michael Sammler's avatar
Michael Sammler committed
623
  | Assign o ot e1 e2 s => Assign o ot (subst_l xs e1) (subst_l xs e2) (subst_stmt xs s)
Michael Sammler's avatar
Michael Sammler committed
624
  | SkipS s => SkipS (subst_stmt xs s)
Michael Sammler's avatar
Michael Sammler committed
625
  | StuckS => StuckS
Michael Sammler's avatar
Michael Sammler committed
626
  | ExprS e s => ExprS (subst_l xs e) (subst_stmt xs s)
627
  | Assert ot e s => Assert ot (subst_l xs e) (subst_stmt xs s)
Michael Sammler's avatar
Michael Sammler committed
628
629
630
  | AnnotStmt n a s => AnnotStmt n a (subst_stmt xs s)
  | LocInfoS a s => LocInfoS a (subst_stmt xs s)
  | Stmt s => Stmt (lang.subst_stmt xs s)
Michael Sammler's avatar
Michael Sammler committed
631
632
  end.

Michael Sammler's avatar
Michael Sammler committed
633
634
Lemma to_stmt_subst xs s :
  to_stmt (subst_stmt xs s) = lang.subst_stmt xs (to_stmt s).
Michael Sammler's avatar
Michael Sammler committed
635
636
637
Proof.
  elim: s => * //=; repeat rewrite to_expr_subst_l //; repeat f_equal => //; repeat rewrite -list_fmap_compose.
  - by apply Forall_fmap_ext_1.
638
  - rewrite /notation.Assert. by f_equal.
Michael Sammler's avatar
Michael Sammler committed
639
640
641
642
643
644
645
646
647
  - match goal with
    | |- notation.AnnotStmt ?n _ _ = _ => generalize dependent n
    end.
    by rewrite /notation.AnnotStmt; elim; eauto => /= n ->.
Qed.
End W.

(** Substitution *)
Ltac simpl_subst :=
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
  (* We need to be careful to never call simpl on the goal as that may
  become quite slow. TODO: vm_compute seems to perform a lot better
  than simpl but it reduces to much. Can we somehow still use it?  *)
  repeat (lazymatch goal with
          | |- context C [subst_stmt ?xs ?s] =>
            let s' := W.of_stmt s in
            let P := context C [subst_stmt xs (W.to_stmt s')] in
            change_no_check P; rewrite <-(W.to_stmt_subst xs)
          end);
  repeat (lazymatch goal with
          | |- context C [W.to_stmt (W.subst_stmt ?xs ?s)] =>
            let s' := eval simpl in (W.subst_stmt xs s) in
            let s' := eval unfold W.to_stmt, W.to_expr in (W.to_stmt s') in
            let s' := eval simpl in s' in
            let P := context C [s'] in
            change_no_check P
          end).
Michael Sammler's avatar
Michael Sammler committed
665
666
667
668
669
670
671
Arguments W.to_expr : simpl never.
Arguments W.to_stmt : simpl never.
Arguments subst : simpl never.
Arguments subst_l : simpl never.
Arguments subst_stmt : simpl never.

Ltac inv_stmt_step :=
672
673
674
675
676
677
678
679
680
  repeat match goal with
  | _ => progress simplify_map_eq/= (* simplify memory stuff *)
  | H : to_val _ = Some _ |- _ => apply of_to_val in H
  | H : context [to_val (of_val _)] |- _ => rewrite to_of_val in H
  | H : stmt_step ?e _ _ _ _ _ _ |- _ =>
     try (is_var e; fail 1); (* inversion yields many goals if [e] is a variable *)
(*      and can thus better be avoided. *)
     inversion H; subst; clear H
  end.
Michael Sammler's avatar
Michael Sammler committed
681
682
683
684
685
686
687

Ltac inv_expr_step :=
  repeat match goal with
  | _ => progress simplify_map_eq/= (* simplify memory stuff *)
  | H : to_val _ = Some _ |- _ => apply of_to_val in H
  | H : context [to_val (of_val _)] |- _ => rewrite to_of_val in H
  | H : expr_step ?e _ _ _ _ _ |- _ =>
688
689
     try (is_var e; fail 1); (* inversion yields many goals if [e] is a variable *)
(*      and can thus better be avoided. *)
Michael Sammler's avatar
Michael Sammler committed
690
691
692
     inversion H; subst; clear H
  end.

693
Ltac solve_struct_obligations := done.