blob: e3aa767ccb57182e3b87a87c85495963f91a2ba8 (
plain)
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
|
(**************************************************************************)
(* *)
(* SMTCoq *)
(* Copyright (C) 2011 - 2021 *)
(* *)
(* See file "AUTHORS" for the list of authors *)
(* *)
(* This file is distributed under the terms of the CeCILL-C licence *)
(* *)
(**************************************************************************)
Require Import State SMT_terms.
Require Import List Bool PArray Int63.
Local Open Scope list_scope.
Local Open Scope bool_scope.
Local Open Scope int63_scope.
Set Implicit Arguments.
(* User-friendly interpretation of clauses and of consequences *)
Section Interp_UF.
Fixpoint interp_uf (rho:Valuation.t) (c:C.t) :=
match c with
| nil => false
| l::nil => Lit.interp rho l
| l::c => (Lit.interp rho l) || (interp_uf rho c)
end.
Lemma interp_equiv rho c : C.interp rho c = interp_uf rho c.
Proof.
induction c as [ |l c IHc]; simpl; auto.
rewrite IHc. destruct c as [ |l' c]; simpl; auto.
now rewrite orb_false_r.
Qed.
Fixpoint interp_conseq_uf (rho:Valuation.t) (prem:list C.t) (concl:C.t) :=
match prem with
| nil => is_true (interp_uf rho concl)
| c::prem => is_true (interp_uf rho c) -> interp_conseq_uf rho prem concl
end.
End Interp_UF.
(* Small checker for assumptions *)
Section Checker.
Section Forallb2.
Variables A B : Type.
Variable P : A -> B -> bool.
Fixpoint forallb2 (xs: list A) (ys:list B) {struct xs} : bool :=
match xs, ys with
| nil, nil => true
| x::xs, y::ys => (P x y) && (forallb2 xs ys)
| _, _ => false
end.
End Forallb2.
Definition check_hole (s:S.t) (prem_id:list clause_id) (prem:list C.t) (concl:C.t) : C.t :=
if forallb2 (fun id c => forallb2 (fun i j => i == j) (S.get s id) (S.sort_uniq c)) prem_id prem
then concl
else C._true.
End Checker.
Section Checker_correct.
Variable t_i : array SMT_classes.typ_compdec.
Variable t_func : array (Atom.tval t_i).
Variable t_atom : array Atom.atom.
Variable t_form : array Form.form.
Local Notation rho := (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) (Atom.interp_form_hatom_bv t_i t_func t_atom) t_form).
Variable s : S.t.
Hypothesis Hs : S.valid rho s.
Hypothesis Ht3 : Valuation.wf
(Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom)
(Atom.interp_form_hatom_bv t_i t_func t_atom)
t_form).
Lemma interp_check_clause c1 : forall c2,
forallb2 (fun i j => i == j) c1 c2 -> C.interp rho c1 = C.interp rho c2.
Proof.
induction c1 as [ |l1 c1 IHc1]; simpl; intros [ |l2 c2]; simpl; auto; try discriminate.
unfold is_true. rewrite andb_true_iff. intros [H1 H2].
rewrite Int63.eqb_spec in H1. now rewrite (IHc1 _ H2), H1.
Qed.
Lemma valid_check_clause cid c :
forallb2 (fun i j => i == j) (S.get s cid) (S.sort_uniq c) ->
interp_uf rho c.
Proof.
intro H. rewrite <- interp_equiv, <- S.sort_uniq_correct; auto.
rewrite <- (interp_check_clause _ _ H). now apply Hs.
Qed.
Lemma valid_check_forall_inst (lemma : Prop) :
lemma ->
forall concl,
(lemma -> interp_uf rho concl) ->
C.valid rho concl.
Proof.
intros pl concl applemma.
unfold C.valid. rewrite interp_equiv.
now apply applemma.
Qed.
Variable prem_id : list int.
Variable prem : list C.t.
Variable concl : C.t.
Hypothesis p : interp_conseq_uf
(Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom)
(Atom.interp_form_hatom_bv t_i t_func t_atom)
t_form) prem concl.
Lemma valid_check_hole: C.valid rho (check_hole s prem_id prem concl).
Proof.
unfold check_hole. revert prem p. induction prem_id as [ |pid pids IHpids]; simpl;
intros [ |p ps]; simpl; intro H.
- unfold C.valid. now rewrite interp_equiv.
- now apply C.interp_true.
- now apply C.interp_true.
- case_eq (forallb2 (fun i j => i == j) (S.get s pid) (S.sort_uniq p));
simpl; intro Heq; [ |now apply C.interp_true].
apply IHpids. apply H. apply (valid_check_clause _ _ Heq).
Qed.
End Checker_correct.
Unset Implicit Arguments.
|
