1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
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
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
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
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
|
(**************************************************************************)
(* *)
(* SMTCoq *)
(* Copyright (C) 2011 - 2022 *)
(* *)
(* See file "AUTHORS" for the list of authors *)
(* *)
(* This file is distributed under the terms of the CeCILL-C licence *)
(* *)
(**************************************************************************)
Require Import Bool List Int63 PArray.
Require Import State SMT_terms.
Local Open Scope array_scope.
Local Open Scope int63_scope.
Section certif.
Variable t_form : PArray.array Form.form.
Variable t_atom : PArray.array Atom.atom.
Local Notation get_atom := (PArray.get t_atom) (only parsing).
Local Notation get_form := (PArray.get t_form) (only parsing).
Definition get_eq (x:var) (f : int -> int -> C.t) :=
match get_form x with
| Form.Fatom xa =>
match get_atom xa with
| Atom.Abop (Atom.BO_eq _) a b => f a b
| _ => C._true
end
| _ => C._true
end.
(* Register get_eq as PrimInline. *)
Fixpoint check_trans_aux (t1 t2:int)
(eqs:list _lit) (res:_lit) (clause:C.t) : C.t :=
match eqs with
| nil =>
let xres := Lit.blit res in
get_eq xres (fun t1' t2' =>
if ((t1 == t1') && (t2 == t2')) ||
((t1 == t2') && (t2 == t1')) then
Lit.lit xres :: clause
else C._true)
| leq::eqs =>
let xeq := Lit.blit leq in
get_eq xeq (fun t t' =>
if t2 == t' then
check_trans_aux t1 t eqs res (Lit.nlit xeq :: clause)
else
if t2 == t then
check_trans_aux t1 t' eqs res (Lit.nlit xeq :: clause)
else
if t1 == t' then
check_trans_aux t t2 eqs res (Lit.nlit xeq :: clause)
else
if t1 == t then
check_trans_aux t' t2 eqs res (Lit.nlit xeq :: clause)
else C._true)
end.
Definition check_trans (res:_lit) (eqs:list _lit) : C.t :=
match eqs with
| nil =>
let xres := Lit.blit res in
get_eq xres (fun t1 t2 =>
if t1 == t2 then Lit.lit xres :: nil else C._true)
| leq :: eqs =>
let xeq := Lit.blit leq in
get_eq xeq
(fun t1 t2 => check_trans_aux t1 t2 eqs res (Lit.nlit xeq :: nil))
end.
Fixpoint build_congr (eqs:list (option _lit))
(l r:list int) (c:C.t) {struct eqs} :=
match eqs, l, r with
| nil, nil, nil => c
| eq::eqs, t1::l, t2::r =>
match eq with
| None => if t1 == t2 then build_congr eqs l r c else C._true
| Some leq =>
let xeq := Lit.blit leq in
get_eq xeq (fun t1' t2' =>
if ((t1 == t1') && (t2 == t2')) ||
((t1 == t2') && (t2 == t1')) then
build_congr eqs l r (Lit.nlit xeq :: c)
else C._true)
end
| _, _, _ => C._true
end.
Definition check_congr (leq:_lit) (eqs:list (option _lit)) :=
let xeq := Lit.blit leq in
get_eq xeq (fun t1 t2 =>
match get_atom t1, get_atom t2 with
| Atom.Abop o1 a1 a2, Atom.Abop o2 b1 b2 =>
if Atom.bop_eqb o1 o2 then
build_congr eqs (a1::a2::nil) (b1::b2::nil) (Lit.lit xeq :: nil)
else C._true
| Atom.Auop o1 a, Atom.Auop o2 b =>
if Atom.uop_eqb o1 o2 then
build_congr eqs (a::nil) (b::nil) (Lit.lit xeq :: nil)
else C._true
| Atom.Aapp f1 args1, Atom.Aapp f2 args2 =>
if f1 == f2 then build_congr eqs args1 args2 (Lit.lit xeq :: nil)
else C._true
| _, _ => C._true
end).
Definition check_congr_pred (PA:_lit) (PB:_lit) (eqs:list (option _lit)) :=
let xPA := Lit.blit PA in
let xPB := Lit.blit PB in
match get_form xPA, get_form xPB with
| Form.Fatom pa, Form.Fatom pb =>
match get_atom pa, get_atom pb with
| Atom.Abop o1 a1 a2, Atom.Abop o2 b1 b2 =>
if Atom.bop_eqb o1 o2 then
build_congr eqs
(a1::a2::nil) (b1::b2::nil) (Lit.nlit xPA :: Lit.lit xPB :: nil)
else C._true
| Atom.Auop o1 a, Atom.Auop o2 b =>
if Atom.uop_eqb o1 o2 then
build_congr eqs
(a::nil) (b::nil) (Lit.nlit xPA :: Lit.lit xPB :: nil)
else C._true
| Atom.Aapp p a, Atom.Aapp p' b =>
if p == p' then
build_congr eqs a b (Lit.nlit xPA :: Lit.lit xPB :: nil)
else C._true
| _, _ => C._true
end
| _, _ => C._true
end.
Section Proof.
Variables (t_i : array SMT_classes.typ_compdec)
(t_func : array (Atom.tval t_i))
(ch_atom : Atom.check_atom t_atom)
(ch_form : Form.check_form t_form)
(wt_t_atom : Atom.wt t_i t_func t_atom).
Local Notation interp_hatom :=
(Atom.interp_hatom t_i t_func t_atom).
Local Notation interp_form_hatom :=
(Atom.interp_form_hatom t_i t_func t_atom).
Local Notation interp_form_hatom_bv :=
(Atom.interp_form_hatom_bv t_i t_func t_atom).
Local Notation rho :=
(Form.interp_state_var interp_form_hatom interp_form_hatom_bv t_form).
Let wf_t_atom : Atom.wf t_atom.
Proof. destruct (Atom.check_atom_correct _ ch_atom); auto. Qed.
Let def_t_atom : default t_atom = Atom.Acop Atom.CO_xH.
Proof. destruct (Atom.check_atom_correct _ ch_atom); auto. Qed.
Let def_t_form : default t_form = Form.Ftrue.
Proof.
destruct (Form.check_form_correct interp_form_hatom interp_form_hatom_bv _ ch_form) as [H _]; destruct H; auto.
Qed.
Let wf_t_form : Form.wf t_form.
Proof.
destruct (Form.check_form_correct interp_form_hatom interp_form_hatom_bv _ ch_form) as [H _]; destruct H; auto.
Qed.
Let wf_rho : Valuation.wf rho.
Proof.
destruct (Form.check_form_correct interp_form_hatom interp_form_hatom_bv _ ch_form); auto.
Qed.
Lemma valid_C_true : C.interp rho C._true.
Proof.
apply C.interp_true.
destruct (Form.check_form_correct interp_form_hatom interp_form_hatom_bv _ ch_form);trivial.
Qed.
Hint Resolve valid_C_true : smtcoq_euf.
Local Notation interp := (Atom.interp t_i t_func t_atom).
Lemma wf_interp_form : forall x,
rho x = Form.interp interp_form_hatom interp_form_hatom_bv t_form (t_form.[x]).
Proof.
destruct (Form.check_form_correct interp_form_hatom interp_form_hatom_bv _ ch_form).
destruct H; intros x;rewrite Form.wf_interp_form;trivial.
Qed.
Local Notation get_type :=
(Atom.get_type t_i t_func t_atom).
Local Notation check_type :=
(Atom.check_aux t_i t_func get_type).
Lemma get_eq_interp :
forall (l:_lit) (f:Atom.hatom -> Atom.hatom -> C.t),
(forall xa, t_form.[Lit.blit l] = Form.Fatom xa ->
forall t a b, t_atom.[xa] = Atom.Abop (Atom.BO_eq t) a b ->
rho (Lit.blit l) =
Atom.interp_bool t_i
(Atom.apply_binop t_i t t Typ.Tbool (Typ.i_eqb t_i t)
(interp_hatom a) (interp_hatom b)) ->
Typ.eqb (get_type a) t -> Typ.eqb (get_type b) t ->
C.interp rho (f a b)) ->
C.interp rho (get_eq (Lit.blit l) f).
Proof.
intros l f Hf;unfold get_eq.
case_eq (t_form.[Lit.blit l]);trivial with smtcoq_euf;intros.
case_eq (t_atom.[i]);trivial with smtcoq_euf;intros.
destruct b;trivial with smtcoq_euf.
generalize wt_t_atom;unfold Atom.wt;unfold is_true;
rewrite Misc.aforallbi_spec;intros.
assert (i < length t_atom).
apply PArray.get_not_default_lt.
rewrite H0, def_t_atom;discriminate.
apply H1 in H2;clear H1;rewrite H0 in H2;simpl in H2.
rewrite !andb_true_iff in H2;decompose [and] H2;clear H2.
apply Hf with (2:= H0);trivial.
rewrite wf_interp_form, H;simpl.
unfold Atom.interp_form_hatom, Atom.interp_hatom at 1;simpl.
rewrite Atom.t_interp_wf, H0;simpl;trivial.
Qed.
Let tunicity : forall A T U, Typ.eqb A T -> Typ.eqb A U -> T = U.
Proof. intros A T U; rewrite !Typ.eqb_spec; intros; subst T U; auto. Qed.
Ltac tunicity :=
match goal with
| [ H1 : is_true (Typ.eqb ?a ?t1),
H2 : is_true (Typ.eqb ?a ?t2) |- _ ] =>
assert (W:= tunicity _ _ _ H1 H2)
| _ => idtac
end.
Lemma interp_binop_eqb_sym :
forall u a b,
Atom.apply_binop t_i u u Typ.Tbool (Typ.i_eqb t_i u) a b =
Atom.apply_binop t_i u u Typ.Tbool (Typ.i_eqb t_i u) b a.
Proof.
unfold Atom.apply_binop;simpl;intros u (ta,va) (tb,vb).
destruct (Typ.cast ta u);destruct (Typ.cast tb u);trivial.
apply f_equal; apply eq_true_iff_eq.
match goal with |- ?x = _ <-> ?y = _ =>
change (is_true x <-> is_true y) end.
split; intro; rewrite Typ.i_eqb_sym in H; auto.
Qed.
Lemma interp_binop_eqb_trans:
forall u a b c,
Typ.eqb (get_type a) u -> Typ.eqb (get_type b) u -> Typ.eqb (get_type c) u ->
Atom.interp_bool t_i
(Atom.apply_binop t_i u u Typ.Tbool (Typ.i_eqb t_i u)
(interp_hatom a) (interp_hatom b)) ->
Atom.interp_bool t_i
(Atom.apply_binop t_i u u Typ.Tbool (Typ.i_eqb t_i u)
(interp_hatom b) (interp_hatom c)) ->
Atom.interp_bool t_i
(Atom.apply_binop t_i u u Typ.Tbool (Typ.i_eqb t_i u)
(interp_hatom a) (interp_hatom c)).
Proof.
intros u a b c Ha Hb Hc.
generalize (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom a), (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom b), (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom c). rewrite Typ.eqb_spec in Ha. rewrite Typ.eqb_spec in Hb. rewrite Typ.eqb_spec in Hc. unfold Atom.get_type in Ha, Hb, Hc. rewrite Ha, Hb, Hc. intros [va HHa] [vb HHb] [vc HHc].
unfold Atom.interp_hatom.
rewrite HHa, HHb, HHc;simpl;rewrite Typ.cast_refl.
unfold Atom.interp_bool;simpl.
apply Typ.i_eqb_trans.
Qed.
Lemma check_trans_aux_correct :
forall eqs u t1 t2 res c,
Typ.eqb (get_type t1) u -> Typ.eqb (get_type t2) u ->
Atom.interp_bool t_i (interp (Atom.Abop (Atom.BO_eq u) t1 t2)) \/
C.interp rho c ->
C.interp rho (check_trans_aux t1 t2 eqs res c).
Proof.
induction eqs;simpl;intros.
- apply get_eq_interp;intros.
match goal with |- context [if ?b then _ else _] => case_eq b end;
intros;trivial with smtcoq_euf.
simpl;rewrite Lit.interp_lit;unfold Var.interp.
destruct H1;[ | rewrite H1,orb_true_r;auto with smtcoq_euf smtcoq_core].
rewrite orb_true_iff, !andb_true_iff in H7;destruct H7 as
[[H7 H8] | [H7 H8]].
rewrite eqb_spec in H7. rewrite eqb_spec in H8. subst.
tunicity. subst t. rewrite H4, H1;auto with smtcoq_euf smtcoq_core.
rewrite eqb_spec in H7. rewrite eqb_spec in H8. subst.
tunicity. subst t;rewrite interp_binop_eqb_sym in H1;rewrite H4, H1;auto with smtcoq_euf smtcoq_core.
- apply get_eq_interp;intros.
destruct (Misc.reflect_eqb t2 b);subst;tunicity; try subst t.
+ apply (IHeqs u);trivial.
simpl;unfold is_true;rewrite orb_true_iff.
rewrite Lit.interp_nlit;unfold Var.interp.
(* Warning: here, we use decidability of equality over u *)
case_eq (rho (Lit.blit a));[rewrite H4; intros | simpl;auto].
destruct H1;[left | auto].
apply interp_binop_eqb_trans with (4:= H1);trivial.
rewrite interp_binop_eqb_sym;trivial.
+ destruct (Misc.reflect_eqb t2 a0); subst;tunicity; try subst t.
* apply (IHeqs u);trivial.
simpl;unfold is_true;rewrite orb_true_iff.
rewrite Lit.interp_nlit;unfold Var.interp.
(* Warning: here, we use decidability of equality over u *)
case_eq (rho (Lit.blit a));[rewrite H4; intros | simpl;auto].
destruct H1;[left | auto].
apply interp_binop_eqb_trans with (4:= H1);trivial.
* destruct (Misc.reflect_eqb t1 b);subst;tunicity; try subst t.
-- apply (IHeqs u);trivial.
simpl;unfold is_true;rewrite orb_true_iff.
rewrite Lit.interp_nlit;unfold Var.interp.
(* Warning: here, we use decidability of equality over u *)
case_eq (rho (Lit.blit a));[rewrite H4; intros | simpl;auto].
destruct H1;[left | auto].
apply interp_binop_eqb_trans with (5:= H1);trivial.
-- destruct (Misc.reflect_eqb t1 a0);[subst;tunicity;try subst t|auto with smtcoq_euf smtcoq_core].
apply (IHeqs u);trivial.
simpl;unfold is_true;rewrite orb_true_iff.
rewrite Lit.interp_nlit;unfold Var.interp.
(* Warning: here, we use decidability of equality over u *)
case_eq (rho (Lit.blit a));[rewrite H4; intros | simpl;auto].
destruct H1;[left | auto].
apply interp_binop_eqb_trans with (5:= H1);trivial.
rewrite interp_binop_eqb_sym;trivial.
Qed.
Lemma valid_check_trans :
forall res eqs,
C.interp rho (check_trans res eqs).
Proof.
unfold check_trans;intros res [ | leq eqs].
- apply get_eq_interp;intros.
destruct (Misc.reflect_eqb a b).
+ unfold C.interp; simpl; rewrite orb_false_r.
unfold Lit.interp; simpl; rewrite Lit.is_pos_lit.
unfold Var.interp; simpl; rewrite Lit.blit_lit.
rewrite H1.
unfold Atom.interp_bool; simpl.
rewrite e; simpl.
generalize (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom b). rewrite Typ.eqb_spec in H3. unfold Atom.get_type in H3. rewrite H3. intros [vb HHb].
unfold Atom.interp_hatom.
rewrite HHb;simpl;rewrite Typ.cast_refl;simpl.
apply Typ.i_eqb_refl.
+ auto with smtcoq_euf.
- apply get_eq_interp;intros.
apply check_trans_aux_correct with t;trivial.
simpl;rewrite Lit.interp_nlit;unfold Var.interp. rewrite <- H1.
(* Attention ici on utilise la decidabilit'e de l'egalit'e sur t *)
destruct (rho (Lit.blit leq));auto with smtcoq_core.
Qed.
Inductive Forall2 A B (P:A->B->Prop) : list A -> list B -> Prop :=
| Forall2_nil : Forall2 A B P nil nil
| Forall2_cons :
forall a b la lb, P a b -> Forall2 A B P la lb ->
Forall2 A B P (a::la) (b::lb).
Lemma build_congr_correct : forall lp l r c,
(Forall2 _ _ (fun a b => interp_hatom a = interp_hatom b) l r -> C.interp rho c) ->
C.interp rho (build_congr lp l r c).
Proof.
induction lp;destruct l;destruct r;simpl;trivial with smtcoq_euf smtcoq_core;intros.
apply H;constructor.
destruct a.
apply get_eq_interp;intros.
match goal with |- context [if ?x then _ else _] =>
case_eq x;intros;auto with smtcoq_euf smtcoq_core end.
apply IHlp;simpl;intros.
rewrite Lit.interp_nlit;unfold Var.interp.
case_eq (rho (Lit.blit i1));intros;simpl;[ | auto with smtcoq_euf smtcoq_core].
apply H;constructor;trivial with smtcoq_euf smtcoq_core.
generalize (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom a), (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom b). rewrite Typ.eqb_spec in H3. rewrite Typ.eqb_spec in H4. unfold Atom.get_type in H3, H4. rewrite H3,H4. intros [va HHa] [vb HHb].
revert H7;rewrite H2;unfold Atom.apply_binop; simpl.
unfold Atom.interp_hatom.
rewrite HHa, HHb;simpl;rewrite Typ.cast_refl;simpl.
intros W;change (is_true (Typ.i_eqb t_i t va vb)) in W.
rewrite Typ.i_eqb_spec in W.
rewrite orb_true_iff, !andb_true_iff in H5;destruct H5 as
[ [H5 H7] | [H5 H7]].
rewrite eqb_spec in H5. rewrite eqb_spec in H7. subst.
rewrite HHa, HHb;trivial with smtcoq_euf smtcoq_core.
rewrite eqb_spec in H5. rewrite eqb_spec in H7. subst.
rewrite HHa, HHb;trivial with smtcoq_euf smtcoq_core.
destruct (Misc.reflect_eqb i i0);[subst | auto with smtcoq_euf smtcoq_core].
apply IHlp;intros;apply H;constructor;auto with smtcoq_euf smtcoq_core.
Qed.
Lemma valid_check_congr :
forall leq eqs,
C.interp rho (check_congr leq eqs).
Proof.
unfold check_congr;intros leq eqs;apply get_eq_interp;intros.
case_eq (t_atom .[ a]);intros;auto with smtcoq_euf smtcoq_core;
case_eq (t_atom .[ b]);intros;auto with smtcoq_euf smtcoq_core.
(* uop *)
destruct (Atom.reflect_uop_eqb u u0);[subst | auto with smtcoq_euf smtcoq_core].
apply build_congr_correct;intros.
simpl;rewrite Lit.interp_lit, orb_false_r;unfold Var.interp.
rewrite H1.
generalize (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom a), (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom b). rewrite Typ.eqb_spec in H2. rewrite Typ.eqb_spec in H3. unfold Atom.get_type in H2, H3. rewrite H2,H3. intros [va HHa] [vb HHb].
unfold Atom.apply_binop;unfold Atom.interp_hatom;simpl.
rewrite HHb, HHa. simpl.
rewrite Atom.t_interp_wf in HHa; auto with smtcoq_euf smtcoq_core. rewrite H4 in HHa. simpl in HHa.
rewrite Atom.t_interp_wf in HHb; auto with smtcoq_euf smtcoq_core. rewrite H5 in HHb. simpl in HHb.
rewrite Typ.cast_refl;simpl.
assert (Atom.Bval t_i t va = Atom.Bval t_i t vb).
inversion H6;subst.
unfold Atom.interp_hatom in H10.
rewrite <- HHa; rewrite <- HHb, H10;trivial with smtcoq_euf smtcoq_core.
inversion H7.
apply Eqdep_dec.inj_pair2_eq_dec in H9;trivial with smtcoq_euf smtcoq_core.
rewrite H9.
apply Typ.i_eqb_refl.
intros x y;destruct (Typ.reflect_eqb x y);auto with smtcoq_euf smtcoq_core.
(* bop *)
destruct (Atom.reflect_bop_eqb b0 b1);[subst | auto with smtcoq_euf smtcoq_core].
apply build_congr_correct;intros.
simpl;rewrite Lit.interp_lit, orb_false_r;unfold Var.interp.
rewrite H1.
generalize (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom a), (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom b). rewrite Typ.eqb_spec in H2. rewrite Typ.eqb_spec in H3. unfold Atom.get_type in H2, H3. rewrite H2,H3. intros [va HHa] [vb HHb].
unfold Atom.apply_binop. unfold Atom.interp_hatom;simpl.
rewrite HHb, HHa;simpl.
rewrite Atom.t_interp_wf in HHa; auto with smtcoq_euf smtcoq_core. rewrite H4 in HHa. simpl in HHa.
rewrite Atom.t_interp_wf in HHb; auto with smtcoq_euf smtcoq_core. rewrite H5 in HHb. simpl in HHb.
rewrite Typ.cast_refl;simpl.
assert (Atom.Bval t_i t va = Atom.Bval t_i t vb).
inversion H6;clear H6;subst.
inversion H12;clear H12;subst.
unfold Atom.interp_hatom in H10, H8.
rewrite <- HHa. rewrite <- HHb, H10, H8;trivial with smtcoq_euf smtcoq_core.
inversion H7.
apply Eqdep_dec.inj_pair2_eq_dec in H9;trivial with smtcoq_euf smtcoq_core.
rewrite H9.
apply Typ.i_eqb_refl.
intros x y;destruct (Typ.reflect_eqb x y);auto with smtcoq_euf smtcoq_core.
(* op *)
destruct (Misc.reflect_eqb i i0);[subst | auto with smtcoq_euf smtcoq_core].
apply build_congr_correct;intros.
simpl;rewrite Lit.interp_lit, orb_false_r;unfold Var.interp.
rewrite H1.
generalize (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom a), (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom b). rewrite Typ.eqb_spec in H2. rewrite Typ.eqb_spec in H3. unfold Atom.get_type in H2, H3. rewrite H2,H3. intros [va HHa] [vb HHb].
unfold Atom.apply_binop;unfold Atom.interp_hatom;simpl.
rewrite HHb, HHa;simpl.
rewrite Atom.t_interp_wf in HHa; auto with smtcoq_euf smtcoq_core. rewrite H4 in HHa. simpl in HHa.
rewrite Atom.t_interp_wf in HHb; auto with smtcoq_euf smtcoq_core. rewrite H5 in HHb. simpl in HHb.
rewrite Typ.cast_refl;simpl.
assert (Atom.Bval t_i t va = Atom.Bval t_i t vb).
rewrite <- HHa;rewrite <- HHb;destruct (t_func.[i0]).
apply f_equal;clear HHa HHb va vb H5 H4.
induction H6;simpl;trivial with smtcoq_euf smtcoq_core.
unfold Atom.interp_hatom in H4.
rewrite IHForall2, H4;trivial with smtcoq_euf smtcoq_core.
inversion H7.
apply Eqdep_dec.inj_pair2_eq_dec in H9;trivial with smtcoq_euf smtcoq_core.
rewrite H9.
apply Typ.i_eqb_refl.
intros x y;destruct (Typ.reflect_eqb x y);auto with smtcoq_euf smtcoq_core.
Qed.
Lemma valid_check_congr_pred :
forall lpa lpb eqs,
C.interp rho (check_congr_pred lpa lpb eqs).
Proof.
unfold check_congr_pred;intros.
case_eq (t_form.[Lit.blit lpa]);auto with smtcoq_euf smtcoq_core.
case_eq (t_form.[Lit.blit lpb]);auto with smtcoq_euf smtcoq_core;intros.
case_eq (t_atom.[i0]);auto with smtcoq_euf smtcoq_core; case_eq (t_atom.[i]);auto with smtcoq_euf smtcoq_core;intros.
(* uop *)
destruct (Atom.reflect_uop_eqb u0 u);[subst | auto with smtcoq_euf smtcoq_core].
apply build_congr_correct;simpl;intros.
rewrite orb_false_r, Lit.interp_lit, Lit.interp_nlit;unfold Var.interp.
replace (rho (Lit.blit lpb)) with (rho (Lit.blit lpa)).
destruct (rho (Lit.blit lpa));reflexivity.
rewrite !wf_interp_form, H, H0;simpl.
generalize wt_t_atom;unfold Atom.wt;unfold is_true;
rewrite Misc.aforallbi_spec;intros.
assert (i < length t_atom).
apply PArray.get_not_default_lt.
rewrite H1, def_t_atom;discriminate.
assert (i0 < length t_atom).
apply PArray.get_not_default_lt.
rewrite H2, def_t_atom;discriminate.
apply H4 in H5;apply H4 in H6;clear H4.
unfold Atom.interp_form_hatom, Atom.interp_hatom;simpl.
rewrite !Atom.t_interp_wf, H1, H2;simpl;trivial with smtcoq_euf smtcoq_core.
apply f_equal;apply f_equal.
inversion H3;clear H3;subst;trivial with smtcoq_euf smtcoq_core.
(* bop *)
destruct (Atom.reflect_bop_eqb b0 b);[subst | auto with smtcoq_euf smtcoq_core].
apply build_congr_correct;simpl;intros.
rewrite orb_false_r, Lit.interp_lit, Lit.interp_nlit;unfold Var.interp.
replace (rho (Lit.blit lpb)) with (rho (Lit.blit lpa)).
destruct (rho (Lit.blit lpa));reflexivity.
rewrite !wf_interp_form, H, H0;simpl.
generalize wt_t_atom;unfold Atom.wt;unfold is_true;
rewrite Misc.aforallbi_spec;intros.
assert (i < length t_atom).
apply PArray.get_not_default_lt.
rewrite H1, def_t_atom. discriminate.
assert (i0 < length t_atom).
apply PArray.get_not_default_lt.
rewrite H2, def_t_atom;discriminate.
apply H4 in H5;apply H4 in H6;clear H4.
unfold Atom.interp_form_hatom, Atom.interp_hatom;simpl.
rewrite !Atom.t_interp_wf, H1, H2;simpl;trivial with smtcoq_euf smtcoq_core.
inversion H3;clear H3;subst.
inversion H11;clear H11;subst.
apply f_equal; apply f_equal2;trivial with smtcoq_euf smtcoq_core.
(* op *)
destruct (Misc.reflect_eqb i2 i1);[subst | auto with smtcoq_euf smtcoq_core].
apply build_congr_correct;simpl;intros.
rewrite orb_false_r, Lit.interp_lit, Lit.interp_nlit;unfold Var.interp.
replace (rho (Lit.blit lpb)) with (rho (Lit.blit lpa)).
destruct (rho (Lit.blit lpa));reflexivity.
rewrite !wf_interp_form, H, H0;simpl.
generalize wt_t_atom;unfold Atom.wt;unfold is_true;
rewrite Misc.aforallbi_spec;intros.
assert (i < length t_atom).
apply PArray.get_not_default_lt.
rewrite H1, def_t_atom;discriminate.
assert (i0 < length t_atom).
apply PArray.get_not_default_lt.
rewrite H2, def_t_atom;discriminate.
apply H4 in H5;apply H4 in H6;clear H4.
unfold Atom.interp_form_hatom, Atom.interp_hatom;simpl.
rewrite !Atom.t_interp_wf, H1, H2;simpl;trivial with smtcoq_euf smtcoq_core.
apply f_equal;destruct (t_func.[i1]);apply f_equal.
clear H H0 H1 H2 H5 H6.
induction H3;simpl;trivial with smtcoq_euf smtcoq_core.
unfold Atom.interp_hatom in H;rewrite H, IHForall2;trivial with smtcoq_euf smtcoq_core.
Qed.
End Proof.
End certif.
(*
Local Variables:
coq-load-path: ((rec ".." "SMTCoq"))
End:
*)
|
