diff options
| -rw-r--r-- | src/SMT_terms.v | 2 | ||||
| -rw-r--r-- | src/bva/BVList.v | 8 | ||||
| -rw-r--r-- | src/classes/SMT_classes.v | 2 | ||||
| -rw-r--r-- | src/classes/SMT_classes_instances.v | 2 | ||||
| -rw-r--r-- | src/lia/Lia.v | 206 |
5 files changed, 133 insertions, 87 deletions
diff --git a/src/SMT_terms.v b/src/SMT_terms.v index f88c0c4..b3df896 100644 --- a/src/SMT_terms.v +++ b/src/SMT_terms.v @@ -18,7 +18,7 @@ Local Open Scope list_scope. Local Open Scope array_scope. Local Open Scope int63_scope. -Hint Unfold is_true : smtcoq_core. +#[export] Hint Unfold is_true : smtcoq_core. (* Remark: I use Notation instead of Definition du eliminate conversion check during the type checking *) diff --git a/src/bva/BVList.v b/src/bva/BVList.v index 91a110d..9e22f98 100644 --- a/src/bva/BVList.v +++ b/src/bva/BVList.v @@ -589,7 +589,7 @@ Definition ult_list (x y: list bool) := (ult_list_big_endian (List.rev x) (List.rev y)). -Fixpoint slt_list_big_endian (x y: list bool) := +Definition slt_list_big_endian (x y: list bool) := match x, y with | nil, _ => false | _ , nil => false @@ -2103,7 +2103,7 @@ Proof. intro a. induction a as [ | xa xsa IHa ]. - intros. simpl. easy. - intros. - case b in *. simpl. rewrite IHa. simpl. omega. + case b in *. simpl. rewrite IHa. simpl. lia. simpl. case (k - 1 <? 0)%Z; simpl; now rewrite IHa. Qed. @@ -2117,8 +2117,8 @@ Lemma prop_mult_bool_step: forall k' a b res k, length (mult_bool_step a b res k k') = (length res)%nat. Proof. intro k'. induction k'. - - intros. simpl. rewrite prop_mult_bool_step_k_h_len. simpl. omega. - - intros. simpl. rewrite IHk'. rewrite prop_mult_bool_step_k_h_len. simpl; omega. + - intros. simpl. rewrite prop_mult_bool_step_k_h_len. simpl. lia. + - intros. simpl. rewrite IHk'. rewrite prop_mult_bool_step_k_h_len. simpl; lia. Qed. Lemma and_with_bool_len: forall a b, length (and_with_bool a (nth 0 b false)) = length a. diff --git a/src/classes/SMT_classes.v b/src/classes/SMT_classes.v index 53d5dcc..49729db 100644 --- a/src/classes/SMT_classes.v +++ b/src/classes/SMT_classes.v @@ -98,8 +98,6 @@ Class OrdType T := { lt_not_eq : forall x y : T, lt x y -> x <> y }. -Hint Resolve lt_not_eq lt_trans. - Global Instance StrictOrder_OrdType T `(OrdType T) : StrictOrder (lt : T -> T -> Prop). diff --git a/src/classes/SMT_classes_instances.v b/src/classes/SMT_classes_instances.v index a2831cf..ae8f9d6 100644 --- a/src/classes/SMT_classes_instances.v +++ b/src/classes/SMT_classes_instances.v @@ -681,4 +681,4 @@ Section list. End list. -Hint Resolve unit_compdec bool_compdec Z_compdec Nat_compdec Positive_compdec BV_compdec FArray_compdec int63_compdec option_compdec list_compdec : typeclass_instances. +#[export] Hint Resolve unit_compdec bool_compdec Z_compdec Nat_compdec Positive_compdec BV_compdec FArray_compdec int63_compdec option_compdec list_compdec : typeclass_instances. diff --git a/src/lia/Lia.v b/src/lia/Lia.v index f3c3ada..145acd3 100644 --- a/src/lia/Lia.v +++ b/src/lia/Lia.v @@ -157,44 +157,44 @@ Section certif. Section Build_form. Definition build_not2 i f := - fold (fun f' : BFormula (Formula Z) => N (N f')) 1 i f. + fold (fun f' : BFormula (Formula Z) isProp => NOT (NOT f')) 1 i f. - Variable build_var : vmap -> var -> option (vmap*BFormula (Formula Z)). + Variable build_var : vmap -> var -> option (vmap*(BFormula (Formula Z) isProp)). - Definition build_hform vm f : option (vmap*BFormula (Formula Z)) := + Definition build_hform vm f : option (vmap*(BFormula (Formula Z) isProp)) := match f with | Form.Fatom h => match build_formula vm h with - | Some (vm,f) => Some (vm, A f tt) + | Some (vm,f) => Some (vm, A isProp f tt) | None => None end - | Form.Ftrue => Some (vm, TT) - | Form.Ffalse => Some (vm, FF) + | Form.Ftrue => Some (vm, TT isProp) + | Form.Ffalse => Some (vm, FF isProp) | Form.Fnot2 i l => match build_var vm (Lit.blit l) with | Some (vm, f) => let f' := build_not2 i f in - let f'' := if Lit.is_pos l then f' else N f' in + let f'' := if Lit.is_pos l then f' else NOT f' in Some (vm,f'') | None => None end | Form.Fand args => let n := length args in - if n == 0 then Some (vm,TT) + if n == 0 then Some (vm,TT isProp) else - foldi (fun i f1 => match f1 with | Some(vm',f1') => let l := (args.[i]) in match build_var vm' (Lit.blit l) with | Some(vm2,f2) => let f2' := if Lit.is_pos l then f2 else N f2 in Some(vm2,Cj f1' f2') | None => None end | None => None end) 1 (n-1) (let l := args.[0] in + foldi (fun i f1 => match f1 with | Some(vm',f1') => let l := (args.[i]) in match build_var vm' (Lit.blit l) with | Some(vm2,f2) => let f2' := if Lit.is_pos l then f2 else NOT f2 in Some(vm2,AND f1' f2') | None => None end | None => None end) 1 (n-1) (let l := args.[0] in match build_var vm (Lit.blit l) with - | Some (vm',f) => if Lit.is_pos l then Some (vm',f) else Some (vm',N f) + | Some (vm',f) => if Lit.is_pos l then Some (vm',f) else Some (vm',NOT f) | None => None end) | Form.For args => let n := length args in - if n == 0 then Some (vm,FF) + if n == 0 then Some (vm,FF isProp) else - foldi (fun i f1 => match f1 with | Some(vm',f1') => let l := (args.[i]) in match build_var vm' (Lit.blit l) with | Some(vm2,f2) => let f2' := if Lit.is_pos l then f2 else N f2 in Some(vm2,D f1' f2') | None => None end | None => None end) 1 (n-1) (let l := args.[0] in + foldi (fun i f1 => match f1 with | Some(vm',f1') => let l := (args.[i]) in match build_var vm' (Lit.blit l) with | Some(vm2,f2) => let f2' := if Lit.is_pos l then f2 else NOT f2 in Some(vm2,OR f1' f2') | None => None end | None => None end) 1 (n-1) (let l := args.[0] in match build_var vm (Lit.blit l) with - | Some (vm',f) => if Lit.is_pos l then Some (vm',f) else Some (vm',N f) + | Some (vm',f) => if Lit.is_pos l then Some (vm',f) else Some (vm',NOT f) | None => None end) | Form.Fxor a b => @@ -202,26 +202,26 @@ Section certif. | Some (vm1, f1) => match build_var vm1 (Lit.blit b) with | Some (vm2, f2) => - let f1' := if Lit.is_pos a then f1 else N f1 in - let f2' := if Lit.is_pos b then f2 else N f2 in - Some (vm2, Cj (D f1' f2') (D (N f1') (N f2'))) + let f1' := if Lit.is_pos a then f1 else NOT f1 in + let f2' := if Lit.is_pos b then f2 else NOT f2 in + Some (vm2, AND (OR f1' f2') (OR (NOT f1') (NOT f2'))) | None => None end | None => None end | Form.Fimp args => let n := length args in - if n == 0 then Some (vm,TT) + if n == 0 then Some (vm,TT isProp) else if n <= 1 then let l := args.[0] in match build_var vm (Lit.blit l) with - | Some (vm',f) => if Lit.is_pos l then Some (vm',f) else Some (vm',N f) + | Some (vm',f) => if Lit.is_pos l then Some (vm',f) else Some (vm',NOT f) | None => None end else - foldi_down (fun i f1 => match f1 with | Some(vm',f1') => let l := (args.[i]) in match build_var vm' (Lit.blit l) with | Some(vm2,f2) => let f2' := if Lit.is_pos l then f2 else N f2 in Some(vm2,I f2' None f1') | None => None end | None => None end) (n-2) 0 (let l := args.[n-1] in + foldi_down (fun i f1 => match f1 with | Some(vm',f1') => let l := (args.[i]) in match build_var vm' (Lit.blit l) with | Some(vm2,f2) => let f2' := if Lit.is_pos l then f2 else NOT f2 in Some(vm2,IMPL f2' None f1') | None => None end | None => None end) (n-2) 0 (let l := args.[n-1] in match build_var vm (Lit.blit l) with - | Some (vm',f) => if Lit.is_pos l then Some (vm',f) else Some (vm',N f) + | Some (vm',f) => if Lit.is_pos l then Some (vm',f) else Some (vm',NOT f) | None => None end) | Form.Fiff a b => @@ -229,9 +229,9 @@ Section certif. | Some (vm1, f1) => match build_var vm1 (Lit.blit b) with | Some (vm2, f2) => - let f1' := if Lit.is_pos a then f1 else N f1 in - let f2' := if Lit.is_pos b then f2 else N f2 in - Some (vm2, Cj (D f1' (N f2')) (D (N f1') f2')) + let f1' := if Lit.is_pos a then f1 else NOT f1 in + let f2' := if Lit.is_pos b then f2 else NOT f2 in + Some (vm2, AND (OR f1' (NOT f2')) (OR (NOT f1') f2')) | None => None end | None => None @@ -243,10 +243,10 @@ Section certif. | Some (vm2, f2) => match build_var vm2 (Lit.blit c) with | Some (vm3, f3) => - let f1' := if Lit.is_pos a then f1 else N f1 in - let f2' := if Lit.is_pos b then f2 else N f2 in - let f3' := if Lit.is_pos c then f3 else N f3 in - Some (vm3, D (Cj f1' f2') (Cj (N f1') f3')) + let f1' := if Lit.is_pos a then f1 else NOT f1 in + let f2' := if Lit.is_pos b then f2 else NOT f2 in + let f3' := if Lit.is_pos c then f3 else NOT f3 in + Some (vm3, OR (AND f1' f2') (AND (NOT f1') f3')) | None => None end | None => None @@ -271,14 +271,14 @@ Section certif. let l := Lit.neg l in match build_form vm (get_form (Lit.blit l)) with | Some (vm,f) => - let f := if Lit.is_pos l then f else N f in + let f := if Lit.is_pos l then f else NOT f in Some (vm,f) | None => None end. Fixpoint build_clause_aux vm (cl:list _lit) {struct cl} : - option (vmap * BFormula (Formula Z)) := + option (vmap * BFormula (Formula Z) isProp) := match cl with | nil => None | l::nil => build_nlit vm l @@ -286,7 +286,7 @@ Section certif. match build_nlit vm l with | Some (vm,bf1) => match build_clause_aux vm cl with - | Some (vm,bf2) => Some (vm, Cj bf1 bf2) + | Some (vm,bf2) => Some (vm, AND bf1 bf2) | _ => None end | None => None @@ -295,7 +295,7 @@ Section certif. Definition build_clause vm cl := match build_clause_aux vm cl with - | Some (vm, bf) => Some (vm, I bf None FF) + | Some (vm, bf) => Some (vm, IMPL bf None (FF isProp)) | None => None end. @@ -477,14 +477,16 @@ Section certif. Definition bounded_formula (p:positive) (f:Formula Z) := bounded_pexpr p (f.(Flhs)) && bounded_pexpr p (f.(Frhs)). - Fixpoint bounded_bformula (p:positive) (bf:BFormula (Formula Z)) := + Fixpoint bounded_bformula (p:positive) {k:kind} (bf:BFormula (Formula Z) k) : bool := match bf with - | @TT _ | @FF _ | @X _ _ _ _ _ => true - | A f _ => bounded_formula p f - | Cj bf1 bf2 - | D bf1 bf2 - | I bf1 _ bf2 => bounded_bformula p bf1 && bounded_bformula p bf2 - | N bf => bounded_bformula p bf + | @TT _ _ _ _ _ | @FF _ _ _ _ _ | @X _ _ _ _ _ _ => true + | A _ f _ => bounded_formula p f + | AND bf1 bf2 + | OR bf1 bf2 + | IMPL bf1 _ bf2 => bounded_bformula p bf1 && bounded_bformula p bf2 + | NOT bf => bounded_bformula p bf + | IFF bf1 bf2 => bounded_bformula p bf1 && bounded_bformula p bf2 + | EQ bf1 bf2 => bounded_bformula p bf1 && bounded_bformula p bf2 end. Definition interp_vmap (vm:vmap) p := @@ -958,7 +960,7 @@ Transparent build_z_atom. nth_error (snd vm) (nat_of_P (fst vm - p) - 1) = nth_error (snd vm')(nat_of_P (fst vm' - p) - 1)) /\ bounded_formula (fst vm') f /\ - (interp_bool t_i (interp_atom a) <->Zeval_formula (interp_vmap vm') f). + (interp_bool t_i (interp_atom a) <->Zeval_formula (interp_vmap vm') isProp f). Proof. intros a vm vm' f t. destruct a;simpl;try discriminate. @@ -1011,7 +1013,7 @@ Transparent build_z_atom. nth_error (snd vm) (nat_of_P (fst vm - p) - 1) = nth_error (snd vm')(nat_of_P (fst vm' - p) - 1)) /\ bounded_formula (fst vm') f /\ - (interp_form_hatom h' <-> Zeval_formula (interp_vmap vm') f). + (interp_form_hatom h' <-> Zeval_formula (interp_vmap vm') isProp f). Proof. unfold build_formula;intros h. unfold Atom.interp_form_hatom, Atom.interp_hatom. @@ -1026,14 +1028,14 @@ Transparent build_z_atom. Qed. - Local Notation eval_f := (eval_f (fun x => x)). + Local Notation eval_f := (eval_f (fun k x => x)). - Lemma build_not2_pos_correct : forall vm f l i, + Lemma build_not2_pos_correct : forall vm (f:GFormula isProp) l i, bounded_bformula (fst vm) f -> (rho (Lit.blit l) <-> eval_f (Zeval_formula (interp_vmap vm)) f) -> Lit.is_pos l -> bounded_bformula (fst vm) (build_not2 i f) /\ (Form.interp interp_form_hatom interp_form_hatom_bv t_form (Form.Fnot2 i l) <-> eval_f (Zeval_formula (interp_vmap vm)) (build_not2 i f)). Proof. simpl; intros vm f l i H1 H2 H3; split; unfold build_not2. apply fold_ind; auto. - apply (fold_ind2 _ _ (fun b f' => b = true <-> eval_f (Zeval_formula (interp_vmap vm)) f')). + apply (fold_ind2 _ _ (fun b (f':GFormula isProp) => b = true <-> eval_f (Zeval_formula (interp_vmap vm)) f')). unfold Lit.interp; rewrite H3; auto. intros b f' H4; rewrite negb_involutive; simpl; split. intros Hb H5; apply H5; rewrite <- H4; auto. @@ -1041,12 +1043,12 @@ Transparent build_z_atom. Qed. - Lemma build_not2_neg_correct : forall vm f l i, - bounded_bformula (fst vm) f -> (rho (Lit.blit l) <-> eval_f (Zeval_formula (interp_vmap vm)) f) -> Lit.is_pos l = false -> bounded_bformula (fst vm) (N (build_not2 i f)) /\ (Form.interp interp_form_hatom interp_form_hatom_bv t_form (Form.Fnot2 i l) <-> eval_f (Zeval_formula (interp_vmap vm)) (N (build_not2 i f))). + Lemma build_not2_neg_correct : forall vm (f:GFormula isProp) l i, + bounded_bformula (fst vm) f -> (rho (Lit.blit l) <-> eval_f (Zeval_formula (interp_vmap vm)) f) -> Lit.is_pos l = false -> bounded_bformula (fst vm) (NOT (build_not2 i f)) /\ (Form.interp interp_form_hatom interp_form_hatom_bv t_form (Form.Fnot2 i l) <-> eval_f (Zeval_formula (interp_vmap vm)) (NOT (build_not2 i f))). Proof. simpl; intros vm f l i H1 H2 H3; split; unfold build_not2. apply fold_ind; auto. - apply (fold_ind2 _ _ (fun b f' => b = true <-> ~ eval_f (Zeval_formula (interp_vmap vm)) f')). + apply (fold_ind2 _ _ (fun b (f':GFormula isProp) => b = true <-> ~ eval_f (Zeval_formula (interp_vmap vm)) f')). unfold Lit.interp; rewrite H3; unfold Var.interp; split. intros H4 H5; rewrite <- H2 in H5; rewrite H5 in H4; discriminate. intro H4; case_eq (rho (Lit.blit l)); auto; intro H5; elim H4; rewrite <- H2; auto. @@ -1059,42 +1061,73 @@ Transparent build_z_atom. Lemma bounded_bformula_le : forall p p', (nat_of_P p <= nat_of_P p')%nat -> - forall bf, + forall (bf:BFormula (Formula Z) isProp), bounded_bformula p bf -> bounded_bformula p' bf. Proof. unfold is_true;induction bf;simpl;trivial. - destruct a;unfold bounded_formula;simpl. - rewrite andb_true_iff;intros (H1, H2). - rewrite (bounded_pexpr_le _ _ H _ H1), (bounded_pexpr_le _ _ H _ H2);trivial. - rewrite !andb_true_iff;intros (H1, H2);auto. - rewrite !andb_true_iff;intros (H1, H2);auto. - rewrite !andb_true_iff;intros (H1, H2);auto. + - destruct a;unfold bounded_formula;simpl. + rewrite andb_true_iff;intros (H1, H2). + rewrite (bounded_pexpr_le _ _ H _ H1), (bounded_pexpr_le _ _ H _ H2);trivial. + - rewrite !andb_true_iff;intros (H1, H2);auto. + - rewrite !andb_true_iff;intros (H1, H2);auto. + - rewrite !andb_true_iff;intros (H1, H2);auto. + - rewrite !andb_true_iff;intros (H1, H2);auto. + - rewrite !andb_true_iff;intros (H1, H2);auto. Qed. - Lemma interp_bformula_le : - forall vm vm', - (forall (p : positive), - (nat_of_P p < nat_of_P (fst vm))%nat -> - nth_error (snd vm) (nat_of_P (fst vm - p) - 1) = - nth_error (snd vm') (nat_of_P (fst vm' - p) - 1)) -> - forall bf, - bounded_bformula (fst vm) bf -> - (eval_f (Zeval_formula (interp_vmap vm)) bf <-> - eval_f (Zeval_formula (interp_vmap vm')) bf). - Proof. - intros vm vm' Hnth. - unfold is_true;induction bf;simpl;try tauto. - destruct t;unfold bounded_formula;simpl. - rewrite andb_true_iff;intros (H1, H2). - rewrite !(interp_pexpr_le _ _ Hnth);tauto. - rewrite andb_true_iff;intros (H1,H2);rewrite IHbf1, IHbf2;tauto. - rewrite andb_true_iff;intros (H1,H2);rewrite IHbf1, IHbf2;tauto. - rewrite andb_true_iff;intros (H1,H2);rewrite IHbf1, IHbf2;tauto. - Qed. + Section Interp_bformula. + + Variables vm vm' : positive * list atom. + Variable Hnth : forall p : positive, + (Pos.to_nat p < Pos.to_nat (fst vm))%nat -> + nth_error (snd vm) (Pos.to_nat (fst vm - p) - 1) = + nth_error (snd vm') (Pos.to_nat (fst vm' - p) - 1). + + Definition P k : GFormula k -> Prop := + match k as k return GFormula k -> Prop with + | isProp => fun (bf:BFormula (Formula Z) isProp) => + bounded_bformula (fst vm) bf -> + (eval_f (Zeval_formula (interp_vmap vm)) bf <-> + eval_f (Zeval_formula (interp_vmap vm')) bf) + | isBool => fun (bf:BFormula (Formula Z) isBool) => + bounded_bformula (fst vm) bf -> + (eval_f (Zeval_formula (interp_vmap vm)) bf = + eval_f (Zeval_formula (interp_vmap vm')) bf) + end. + + Lemma interp_bformula_le_gen : forall k f, P k f. + Proof. + intro k. induction f as [k|k|k t|k t a|k f1 IHf1 f2 IHf2|k f1 IHf1 f2 IHf2|k f1 IHf1|k f1 IHf1 o f2 IHf2|k f1 IHf1 f2 IHf2|f1 IHf1 f2 IHf2]; unfold P in *; + try (destruct k; simpl; tauto); + try (destruct k; simpl; unfold is_true;rewrite andb_true_iff;intros (H1,H2);rewrite IHf1, IHf2;tauto). + - destruct k; simpl; + destruct t;unfold bounded_formula;simpl; + unfold is_true;rewrite andb_true_iff;intros (H1, H2); + rewrite !(interp_pexpr_le _ _ Hnth);tauto. + - destruct k; simpl; intro H; now rewrite IHf1. + - destruct k; simpl. + + unfold is_true;rewrite andb_true_iff;intros (H1, H2). + split. + * intros H3 H4. rewrite <- IHf2; auto. apply H3. now rewrite IHf1. + * intros H3 H4. rewrite IHf2; auto. apply H3. now rewrite <- IHf1. + + unfold is_true;rewrite andb_true_iff;intros (H1, H2). + now rewrite IHf1, IHf2. + - simpl. unfold is_true;rewrite andb_true_iff;intros (H1, H2). + now rewrite IHf1, IHf2. + Qed. + + Lemma interp_bformula_le : + forall (bf:BFormula (Formula Z) isProp), + bounded_bformula (fst vm) bf -> + (eval_f (Zeval_formula (interp_vmap vm)) bf <-> + eval_f (Zeval_formula (interp_vmap vm')) bf). + Proof. exact (interp_bformula_le_gen isProp). Qed. + + End Interp_bformula. Lemma build_hform_correct : - forall (build_var : vmap -> var -> option (vmap*BFormula (Formula Z))), + forall (build_var : vmap -> var -> option (vmap*BFormula (Formula Z) isProp)), (forall v vm vm' bf, build_var vm v = Some (vm', bf) -> wf_vmap vm -> @@ -1130,7 +1163,7 @@ Transparent build_z_atom. (* Fand *) simpl; unfold afold_left; case (length l == 0). intro H; inversion H; subst vm'; subst bf; simpl; intro H1; split; auto with smtcoq_core; split; [lia| ]; do 3 (split; auto with smtcoq_core). - revert vm' bf; apply (foldi_ind2 _ _ (fun f1 b => forall vm' bf, f1 = Some (vm', bf) -> wf_vmap vm -> wf_vmap vm' /\ (Pos.to_nat (fst vm) <= Pos.to_nat (fst vm'))%nat /\ (forall p : positive, (Pos.to_nat p < Pos.to_nat (fst vm))%nat -> nth_error (snd vm) (Pos.to_nat (fst vm - p) - 1) = nth_error (snd vm') (Pos.to_nat (fst vm' - p) - 1)) /\ bounded_bformula (fst vm') bf /\ (b = true <-> eval_f (Zeval_formula (interp_vmap vm')) bf))). + revert vm' bf; apply (foldi_ind2 _ _ (fun f1 b => forall vm' (bf:BFormula (Formula Z) isProp), f1 = Some (vm', bf) -> wf_vmap vm -> wf_vmap vm' /\ (Pos.to_nat (fst vm) <= Pos.to_nat (fst vm'))%nat /\ (forall p : positive, (Pos.to_nat p < Pos.to_nat (fst vm))%nat -> nth_error (snd vm) (Pos.to_nat (fst vm - p) - 1) = nth_error (snd vm') (Pos.to_nat (fst vm' - p) - 1)) /\ bounded_bformula (fst vm') bf /\ (b = true <-> eval_f (Zeval_formula (interp_vmap vm')) bf))). intros vm' bf; case_eq (build_var vm (Lit.blit (l .[ 0]))); try discriminate; intros [vm0 f] Heq; case_eq (Lit.is_pos (l .[ 0])); intros Heq2 H1 H2; inversion H1; subst vm'; subst bf; destruct (Hbv _ _ _ _ Heq H2) as [H10 [H11 [H12 [H13 H14]]]]; do 4 (split; auto); unfold Lit.interp; rewrite Heq2; auto; simpl; split. intros H3 H4; rewrite <- H14 in H4; rewrite H4 in H3; discriminate. intro H3; case_eq (Var.interp rho (Lit.blit (l .[ 0]))); auto; intro H4; elim H3; rewrite <- H14; auto. @@ -1142,7 +1175,7 @@ Transparent build_z_atom. (* For *) simpl; unfold afold_left; case (length l == 0). intro H; inversion H; subst vm'; subst bf; simpl; intro H1; split; auto with smtcoq_core; split; [lia| ]; do 3 (split; auto with smtcoq_core); discriminate. - revert vm' bf; apply (foldi_ind2 _ _ (fun f1 b => forall vm' bf, f1 = Some (vm', bf) -> wf_vmap vm -> wf_vmap vm' /\ (Pos.to_nat (fst vm) <= Pos.to_nat (fst vm'))%nat /\ (forall p : positive, (Pos.to_nat p < Pos.to_nat (fst vm))%nat -> nth_error (snd vm) (Pos.to_nat (fst vm - p) - 1) = nth_error (snd vm') (Pos.to_nat (fst vm' - p) - 1)) /\ bounded_bformula (fst vm') bf /\ (b = true <-> eval_f (Zeval_formula (interp_vmap vm')) bf))). + revert vm' bf; apply (foldi_ind2 _ _ (fun f1 b => forall vm' (bf:BFormula (Formula Z) isProp), f1 = Some (vm', bf) -> wf_vmap vm -> wf_vmap vm' /\ (Pos.to_nat (fst vm) <= Pos.to_nat (fst vm'))%nat /\ (forall p : positive, (Pos.to_nat p < Pos.to_nat (fst vm))%nat -> nth_error (snd vm) (Pos.to_nat (fst vm - p) - 1) = nth_error (snd vm') (Pos.to_nat (fst vm' - p) - 1)) /\ bounded_bformula (fst vm') bf /\ (b = true <-> eval_f (Zeval_formula (interp_vmap vm')) bf))). intros vm' bf; case_eq (build_var vm (Lit.blit (l .[ 0]))); try discriminate; intros [vm0 f] Heq; case_eq (Lit.is_pos (l .[ 0])); intros Heq2 H1 H2; inversion H1; subst vm'; subst bf; destruct (Hbv _ _ _ _ Heq H2) as [H10 [H11 [H12 [H13 H14]]]]; do 4 (split; auto with smtcoq_core); unfold Lit.interp; rewrite Heq2; auto with smtcoq_core; simpl; split. intros H3 H4; rewrite <- H14 in H4; rewrite H4 in H3; discriminate. intro H3; case_eq (Var.interp rho (Lit.blit (l .[ 0]))); auto with smtcoq_core; intro H4; elim H3; rewrite <- H14; auto with smtcoq_core. @@ -1152,13 +1185,14 @@ Transparent build_z_atom. simpl; rewrite (bounded_bformula_le _ _ H11 _ H8); case (Lit.is_pos (l .[ i])); rewrite H13; auto with smtcoq_core. simpl; rewrite (interp_bformula_le _ _ H12 _ H8) in H9; rewrite <- H9; case_eq (Lit.is_pos (l .[ i])); intro Heq2; simpl; rewrite <- H14; unfold Lit.interp; rewrite Heq2; split; case (Var.interp rho (Lit.blit (l .[ i]))); try rewrite orb_false_r; try rewrite orb_true_r; auto with smtcoq_core; try (intros [H20|H20]; auto with smtcoq_core; discriminate); right; intro H20; discriminate. (* Fimp *) + { simpl; unfold afold_right; case (length l == 0). intro H; inversion H; subst vm'; subst bf; simpl; intro H1; split; auto with smtcoq_core; split; [lia| ]; do 3 (split; auto with smtcoq_core). case (length l <= 1). case_eq (build_var vm (Lit.blit (l .[ 0]))); try discriminate; intros [vm0 f] Heq; case_eq (Lit.is_pos (l .[ 0])); intros Heq2 H1 H2; inversion H1; subst vm'; subst bf; destruct (Hbv _ _ _ _ Heq H2) as [H3 [H4 [H5 [H6 H7]]]]; do 4 (split; auto with smtcoq_core); unfold Lit.interp; rewrite Heq2; auto with smtcoq_core; simpl; split. intros H8 H9; rewrite <- H7 in H9; rewrite H9 in H8; discriminate. intro H8; case_eq (Var.interp rho (Lit.blit (l .[ 0]))); auto with smtcoq_core; intro H9; rewrite H7 in H9; elim H8; auto with smtcoq_core. - revert vm' bf; apply (foldi_down_ind2 _ _ (fun f1 b => forall vm' bf, f1 = Some (vm', bf) -> wf_vmap vm -> wf_vmap vm' /\ (Pos.to_nat (fst vm) <= Pos.to_nat (fst vm'))%nat /\ (forall p : positive, (Pos.to_nat p < Pos.to_nat (fst vm))%nat -> nth_error (snd vm) (Pos.to_nat (fst vm - p) - 1) = nth_error (snd vm') (Pos.to_nat (fst vm' - p) - 1)) /\ bounded_bformula (fst vm') bf /\ (b = true <-> eval_f (Zeval_formula (interp_vmap vm')) bf))). + revert vm' bf; apply (foldi_down_ind2 _ _ (fun f1 b => forall vm' (bf:BFormula (Formula Z) isProp), f1 = Some (vm', bf) -> wf_vmap vm -> wf_vmap vm' /\ (Pos.to_nat (fst vm) <= Pos.to_nat (fst vm'))%nat /\ (forall p : positive, (Pos.to_nat p < Pos.to_nat (fst vm))%nat -> nth_error (snd vm) (Pos.to_nat (fst vm - p) - 1) = nth_error (snd vm') (Pos.to_nat (fst vm' - p) - 1)) /\ bounded_bformula (fst vm') bf /\ (b = true <-> eval_f (Zeval_formula (interp_vmap vm')) bf))). intros vm' bf; case_eq (build_var vm (Lit.blit (l .[ length l - 1]))); try discriminate; intros [vm0 f] Heq; case_eq (Lit.is_pos (l .[ length l - 1])); intros Heq2 H1 H2; inversion H1; subst vm'; subst bf; destruct (Hbv _ _ _ _ Heq H2) as [H10 [H11 [H12 [H13 H14]]]]; do 4 (split; auto with smtcoq_core); unfold Lit.interp; rewrite Heq2; auto with smtcoq_core; simpl; split. intros H3 H4; rewrite <- H14 in H4; rewrite H4 in H3; discriminate. intro H3; case_eq (Var.interp rho (Lit.blit (l .[ length l - 1]))); auto with smtcoq_core; intro H4; elim H3; rewrite <- H14; auto with smtcoq_core. @@ -1166,7 +1200,21 @@ Transparent build_z_atom. intros p H15; rewrite H7; auto with smtcoq_core; apply H12; eauto with smtcoq_core arith. split. simpl; rewrite (bounded_bformula_le _ _ H11 _ H8); case (Lit.is_pos (l .[ i])); rewrite H13; auto with smtcoq_core. - simpl; rewrite (interp_bformula_le _ _ H12 _ H8) in H9; rewrite <- H9; case_eq (Lit.is_pos (l .[ i])); intro Heq2; simpl; rewrite <- H14; unfold Lit.interp; rewrite Heq2; split; case (Var.interp rho (Lit.blit (l .[ i]))); auto with smtcoq_core; try discriminate; simpl; intro H; apply H; discriminate. + simpl; rewrite (interp_bformula_le _ _ H12 _ H8) in H9. + case_eq (Lit.is_pos (l .[ i])); intro Heq2; simpl. + - unfold Lit.interp. rewrite Heq2. split. + + revert H14. case (Var.interp rho (Lit.blit (l .[ i]))); simpl. + * intros H101 H102 H103. now rewrite <- H9. + * intros H101 H102 H103. rewrite <- H101 in H103. discriminate. + + revert H14. case (Var.interp rho (Lit.blit (l .[ i]))); simpl; auto. + intros H101 H102. rewrite H9. apply H102. now rewrite <- H101. + - unfold Lit.interp. rewrite Heq2. split. + + revert H14. case (Var.interp rho (Lit.blit (l .[ i]))); simpl. + * intros H101 H102 H103. elim H103. now rewrite <- H101. + * intros H101 H102 H103. now rewrite <- H9. + + revert H14. case (Var.interp rho (Lit.blit (l .[ i]))); simpl; auto. + intros H101 H102. rewrite H9. apply H102. now rewrite <- H101. + } (* Fxor *) simpl; case_eq (build_var vm (Lit.blit a)); try discriminate; intros [vm1 f1] Heq1; case_eq (build_var vm1 (Lit.blit b)); try discriminate; intros [vm2 f2] Heq2 H1 H2; inversion H1; subst vm'; subst bf; destruct (Hbv _ _ _ _ Heq1 H2) as [H3 [H4 [H5 [H6 H7]]]]; destruct (Hbv _ _ _ _ Heq2 H3) as [H8 [H9 [H10 [H11 H12]]]]; split; auto with smtcoq_core; split; [eauto with smtcoq_core arith| ]; split. intros p H18; rewrite H5; auto with smtcoq_core; rewrite H10; eauto with smtcoq_core arith. @@ -1293,7 +1341,7 @@ Transparent build_z_atom. ( match build_nlit vm a with | Some (vm0, bf1) => match build_clause_aux vm0 (i::l) with - | Some (vm1, bf2) => Some (vm1, Cj bf1 bf2) + | Some (vm1, bf2) => Some (vm1, AND bf1 bf2) | None => None end | None => None |