diff options
Diffstat (limited to 'src/lia/Lia.v')
| -rw-r--r-- | src/lia/Lia.v | 1611 |
1 files changed, 1611 insertions, 0 deletions
diff --git a/src/lia/Lia.v b/src/lia/Lia.v new file mode 100644 index 0000000..0969db0 --- /dev/null +++ b/src/lia/Lia.v @@ -0,0 +1,1611 @@ +(**************************************************************************) +(* *) +(* SMTCoq *) +(* Copyright (C) 2011 - 2015 *) +(* *) +(* Michaël Armand *) +(* Benjamin Grégoire *) +(* Chantal Keller *) +(* *) +(* Inria - École Polytechnique - MSR-Inria Joint Lab *) +(* *) +(* This file is distributed under the terms of the CeCILL-C licence *) +(* *) +(**************************************************************************) + +Require Import Bool. +Require Import List. +Require Import Int63. +Require Import PArray. +Require Import RingMicromega. +Require Import ZMicromega. +Require Import Tauto. +Require Import Psatz. +(* Add LoadPath ".." as SMTCoq. *) + +Require Import Misc State. +Require Import SMT_terms. +Require Import SMTCoq.euf.Euf. + +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). + + Import EnvRing Atom. + + Register option_map as PrimInline. + + Section BuildPositive. + Variable build_positive : hatom -> option positive. + + Definition build_positive_atom_aux (a:atom) : option positive := + match a with + | Acop CO_xH => Some xH + | Auop UO_xO a => option_map xO (build_positive a) + | Auop UO_xI a => option_map xI (build_positive a) + | _ => None + end. + + End BuildPositive. + + Definition build_positive := + foldi_down_cont + (fun i cont h => + build_positive_atom_aux cont (get_atom h)) + (PArray.length t_atom) 0 (fun _ => None). + + Definition build_positive_atom := build_positive_atom_aux build_positive. + Register build_positive_atom as PrimInline. + + Section BuildZ. + + Definition build_z_atom_aux a := + match a with + | Auop UO_Zpos a => option_map Zpos (build_positive a) + | Acop CO_Z0 => Some Z0 + | Auop UO_Zneg a => option_map Zneg (build_positive a) + | _ => None + end. + + End BuildZ. + + Definition build_z h := build_z_atom_aux (get_atom h). + + Definition build_z_atom := build_z_atom_aux. + + Definition vmap := (positive * list Atom.atom)%type. + + Fixpoint find_var_aux h p (l:list Atom.atom) := + match l with + | nil => None + | h' :: l => + let p := Ppred p in + if Atom.eqb h h' then Some p else find_var_aux h p l + end. + + Definition find_var (vm:vmap) h := + let (count,map) := vm in + match find_var_aux h count map with + | Some p => (vm, p) + | None => ((Psucc count,h::map), count) + end. + + Definition empty_vmap : vmap := (1%positive, nil). + + Section BuildPExpr. + + Variable build_pexpr : vmap -> hatom -> (vmap * PExpr Z). + + Definition build_pexpr_atom_aux (vm:vmap) (h:atom) : vmap * PExpr Z := + match h with + | Abop BO_Zplus a1 a2 => + let (vm, pe1) := build_pexpr vm a1 in + let (vm, pe2) := build_pexpr vm a2 in + (vm, PEadd pe1 pe2) + | Abop BO_Zminus a1 a2 => + let (vm, pe1) := build_pexpr vm a1 in + let (vm, pe2) := build_pexpr vm a2 in + (vm, PEsub pe1 pe2) + | Abop BO_Zmult a1 a2 => + let (vm, pe1) := build_pexpr vm a1 in + let (vm, pe2) := build_pexpr vm a2 in + (vm, PEmul pe1 pe2) + | Auop UO_Zopp a => + let (vm, pe) := build_pexpr vm a in + (vm, PEopp pe) + | _ => + match build_z_atom h with + | Some z => (vm, PEc z) + | None => + let (vm,p) := find_var vm h in + (vm,PEX Z p) + end + end. + + End BuildPExpr. + + Definition build_pexpr := + foldi_down_cont + (fun i cont vm h => build_pexpr_atom_aux cont vm (get_atom h)) + (PArray.length t_atom) 0 (fun vm _ => (vm,PEc 0%Z)). + + Definition build_pexpr_atom := build_pexpr_atom_aux build_pexpr. + + (* Remark: We do not use OpNeq *) + Definition build_op2 op := + match op with + | (BO_eq Typ.TZ) => Some OpEq + | BO_Zle => Some OpLe + | BO_Zge => Some OpGe + | BO_Zlt => Some OpLt + | BO_Zgt => Some OpGt + | _ => None + end. + + Definition build_formula_atom vm (a:atom) := + match a with + | Abop op a1 a2 => + match build_op2 op with + | Some o => + let (vm,pe1) := build_pexpr vm a1 in + let (vm,pe2) := build_pexpr vm a2 in + Some (vm, Build_Formula pe1 o pe2) + | None => None + end + | _ => None + end. + + Definition build_formula vm h := + build_formula_atom vm (get_atom h). + + + Section Build_form. + + Definition build_not2 i f := + fold (fun f' => N (N (A:=Formula Z) f')) 1 i f. + + Variable build_var : vmap -> var -> option (vmap*BFormula (Formula Z)). + + + Definition build_hform vm f : option (vmap*BFormula (Formula Z)) := + match f with + | Form.Fatom h => + match build_formula vm h with + | Some (vm,f) => Some (vm, A f) + | None => None + end + | Form.Ftrue => Some (vm, TT (Formula Z)) + | Form.Ffalse => Some (vm, FF (Formula Z)) + | 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 + Some (vm,f'') + | None => None + end + | Form.Fand args => + let n := length args in + if n == 0 then Some (vm,TT (Formula Z)) + 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 + 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) + | None => None + end) + | Form.For args => + let n := length args in + if n == 0 then Some (vm,FF (Formula Z)) + 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 + 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) + | None => None + end) + | Form.Fxor a b => + match build_var vm (Lit.blit a) with + | 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'))) + | None => None + end + | None => None + end + | Form.Fimp args => + let n := length args in + if n == 0 then Some (vm,TT (Formula Z)) + 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) + | 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' 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) + | None => None + end) + | Form.Fiff a b => + match build_var vm (Lit.blit a) with + | 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')) + | None => None + end + | None => None + end + | Form.Fite a b c => + match build_var vm (Lit.blit a) with + | Some (vm1, f1) => + match build_var vm1 (Lit.blit b) with + | 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')) + | None => None + end + | None => None + end + | None => None + end + end. + + End Build_form. + + + Definition build_var := + foldi_down_cont + (fun i cont vm h => build_hform cont vm (get_form h)) + (PArray.length t_form) 0 (fun _ _ => None). + + Definition build_form := build_hform build_var. + + + Definition build_nlit vm l := + 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 + Some (vm,f) + | None => None + end. + + + Fixpoint build_clause_aux vm (cl:list _lit) {struct cl} : + option (vmap * BFormula (Formula Z)) := + match cl with + | nil => None + | l::nil => build_nlit vm l + | l::cl => + match build_nlit vm l with + | Some (vm,bf1) => + match build_clause_aux vm cl with + | Some (vm,bf2) => Some (vm, Cj bf1 bf2) + | _ => None + end + | None => None + end + end. + + Definition build_clause vm cl := + match build_clause_aux vm cl with + | Some (vm, bf) => Some (vm, I bf (FF _)) + | None => None + end. + + Definition get_eq (l:_lit) (f : Atom.hatom -> Atom.hatom -> C.t) := + if Lit.is_pos l then + match get_form (Lit.blit l) 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 + else C._true. + Register get_eq as PrimInline. + + Definition get_not_le (l:_lit) (f : Atom.hatom -> Atom.hatom -> C.t) := + if negb (Lit.is_pos l) then + match get_form (Lit.blit l) with + | Form.Fatom xa => + match get_atom xa with + | Atom.Abop (Atom.BO_Zle) a b => f a b + | _ => C._true + end + | _ => C._true + end + else C._true. + Register get_not_le as PrimInline. + + Definition check_micromega cl c : C.t := + match build_clause empty_vmap cl with + | Some (_, bf) => + if ZTautoChecker bf c then cl + else C._true + | None => C._true + end. + + Definition check_diseq l : C.t := + match get_form (Lit.blit l) with + |Form.For a => + if PArray.length a == 3 then + let a_eq_b := a.[0] in + let not_a_le_b := a.[1] in + let not_b_le_a := a.[2] in + get_eq a_eq_b (fun a b => get_not_le not_a_le_b (fun a' b' => get_not_le not_b_le_a (fun b'' a'' => + if (a == a') && (a == a'') && (b == b') && (b == b'') + then (Lit.lit (Lit.blit l))::nil + else + if (a == b') && (a == b'') && (b == a') && (b == a'') + then (Lit.lit (Lit.blit l))::nil + else C._true))) + else C._true + | _ => C._true + end. + + + Section Proof. + + Variables (t_i : array typ_eqb) + (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 check_atom := + (check_aux t_i t_func (get_type t_i t_func t_atom)). + + Local Notation interp_form_hatom := + (Atom.interp_form_hatom t_i t_func t_atom). + + Local Notation rho := + (Form.interp_state_var interp_form_hatom t_form). + + Local Notation t_interp := (t_interp t_i t_func t_atom). + + Local Notation interp_atom := + (interp_aux t_i t_func (get t_interp)). + + 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 _ 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 _ ch_form) as [H _]; destruct H; auto. + Qed. + + Let wf_rho : Valuation.wf rho. + Proof. + destruct (Form.check_form_correct interp_form_hatom _ ch_form); auto. + Qed. + + Lemma build_positive_atom_aux_correct : + forall (build_positive : hatom -> option positive), + (forall (h : hatom) p, + build_positive h = Some p -> + t_interp.[h] = Bval t_i Typ.Tpositive p) -> + forall (a:atom) (p:positive), + build_positive_atom_aux build_positive a = Some p -> + interp_atom a = Bval t_i Typ.Tpositive p. + Proof. + intros build_positive Hbuild a; case a; simpl; try discriminate; auto. + destruct c; simpl; try discriminate; intros p H1; inversion_clear H1; auto. + destruct u; simpl; try discriminate; + intros i p; case_eq (build_positive i); simpl; try discriminate; intros q H1 H2; inversion_clear H2; rewrite (Hbuild _ _ H1); auto. + Qed. + + Lemma build_positive_correct : forall h p, + build_positive h = Some p -> + t_interp.[h] = Bval t_i Typ.Tpositive p. + Proof. + unfold build_positive. + apply foldi_down_cont_ind;intros;try discriminate. + rewrite t_interp_wf;trivial. + apply build_positive_atom_aux_correct with cont;trivial. + Qed. + + Lemma build_positive_atom_correct : + forall (a:atom) (p:positive), + build_positive_atom a = Some p -> + interp_atom a = Bval t_i Typ.Tpositive p. + Proof. + apply build_positive_atom_aux_correct;apply build_positive_correct. + Qed. + + Lemma build_z_atom_aux_correct : + forall a z, + build_z_atom_aux a = Some z -> + interp_atom a = Bval t_i Typ.TZ z. + Proof. + intros a z. + destruct a;simpl;try discriminate;auto. + destruct c;[discriminate | intros Heq;inversion Heq;trivial]. + destruct u;try discriminate; + case_eq (build_positive i);try discriminate; + intros p Hp Heq;inversion Heq;clear Heq;subst; + rewrite (build_positive_correct _ _ Hp);trivial. + Qed. + + Lemma build_z_correct : + forall h z, build_z h = Some z -> t_interp.[h] = Bval t_i Typ.TZ z. + Proof. + unfold build_z;intros h z;rewrite t_interp_wf;trivial. + apply build_z_atom_aux_correct;discriminate. + Qed. + + Lemma build_z_atom_correct : + forall a z, build_z_atom a = Some z -> + interp_atom a = Bval t_i Typ.TZ z. + Proof. + apply build_z_atom_aux_correct. + Qed. + + Definition wf_vmap (vm:vmap) := + (List.length (snd vm) = nat_of_P (fst vm) - 1)%nat /\ + List.forallb (fun h => check_atom h Typ.TZ) (snd vm). + + Fixpoint bounded_pexpr (p:positive) (pe:PExpr Z) := + match pe with + | PEc _ => true + | PEX x => Zlt_bool (Zpos x) (Zpos p) + | PEadd pe1 pe2 + | PEsub pe1 pe2 + | PEmul pe1 pe2 => bounded_pexpr p pe1 && bounded_pexpr p pe2 + | PEopp pe => bounded_pexpr p pe + | PEpow pe _ => bounded_pexpr p pe + end. + + 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)) := + 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 + end. + + Definition interp_vmap (vm:vmap) p := + match nth_error (snd vm) (nat_of_P (fst vm - p) - 1)%nat with + | Some a => + let (t,v) := interp_atom a in + match Typ.cast t Typ.TZ with + | Typ.Cast k => k (Typ.interp t_i) v + | _ => 0%Z + end + | _ => 0%Z + end. + + Lemma find_var_aux_lt : + forall h p lvm pvm, + find_var_aux h pvm lvm = Some p -> + Datatypes.length lvm = (nat_of_P pvm - 1)%nat -> + (nat_of_P p < nat_of_P pvm)%nat. + Proof. + induction lvm;simpl;try discriminate. + intros pvm Heq1 Heq. + assert (1 < pvm)%positive. + rewrite Plt_lt;change (nat_of_P 1) with 1%nat ;omega. + assert (Datatypes.length lvm = nat_of_P (Ppred pvm) - 1)%nat. + rewrite Ppred_minus, Pminus_minus;trivial. + change (nat_of_P 1) with 1%nat ;try omega. + revert Heq1. + destruct (Atom.reflect_eqb h a);subst. + intros Heq1;inversion Heq1;clear Heq1;subst;omega. + intros Heq1;apply IHlvm in Heq1;trivial. + apply lt_trans with (1:= Heq1);omega. + Qed. + + Lemma build_pexpr_atom_aux_correct_z : + forall (h : atom) (vm vm' : vmap) (pe : PExpr Z), + check_atom h Typ.TZ -> + match build_z_atom h with + | Some z => (vm, PEc z) + | None => let (vm0, p) := find_var vm h in (vm0, PEX Z p) + end = (vm', pe) -> + wf_vmap vm -> + wf_vmap vm' /\ + (nat_of_P (fst vm) <= nat_of_P (fst vm'))%nat /\ + (forall p, + (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)) /\ + bounded_pexpr (fst vm') pe /\ + interp_atom h = Bval t_i Typ.TZ (Zeval_expr (interp_vmap vm') pe). + Proof. + intros h vm vm' pe Hh. + case_eq (build_z_atom h). + intros z Hb Heq;inversion Heq;clear Heq;subst. + intros (Hwf1, Hwf2). + repeat split;auto with zarith. + rewrite (build_z_atom_correct _ _ Hb);trivial. + intros _;unfold find_var;destruct vm as (pvm,lvm). + case_eq (find_var_aux h pvm lvm). + intros p Hf Heq;inversion Heq;clear Heq;subst. + intros (Hwf1, Hwf2);repeat split;auto with zarith. + simpl; unfold is_true;rewrite <- Zlt_is_lt_bool. + rewrite <- !Z_of_nat_of_P; apply inj_lt;simpl in Hwf1. + apply find_var_aux_lt with (1:= Hf);trivial. + revert lvm pvm p Hf Hwf1 Hwf2. + unfold interp_vmap;simpl. + induction lvm;simpl;try discriminate. + intros pvm p Heq1 Heq. + assert (1 < pvm)%positive. + rewrite Plt_lt;change (nat_of_P 1) with 1%nat ;omega. + assert (Datatypes.length lvm = nat_of_P (Ppred pvm) - 1)%nat. + rewrite Ppred_minus, Pminus_minus;trivial. + change (nat_of_P 1) with 1%nat ;try omega. + revert Heq1. + destruct (Atom.reflect_eqb h a);subst. + intros Heq1;inversion Heq1;clear Heq1;subst. + unfold is_true;rewrite andb_true_iff;intros (H1,H2). + assert (1 < nat_of_P pvm)%nat by (rewrite Plt_lt in H;trivial). + assert (W:=nat_of_P_pos (Ppred pvm)). + assert (nat_of_P (pvm - Ppred pvm) - 1 = 0)%nat. + rewrite Pminus_minus;try omega. + apply Plt_lt;omega. + rewrite H4;simpl. + destruct (check_aux_interp_aux _ _ _ wf_t_atom _ _ H1) as (z,Hz). + rewrite Hz;trivial. + unfold is_true;rewrite andb_true_iff;intros Heq1 (H1,H2). + assert (W:= find_var_aux_lt _ _ _ _ Heq1 H0). + assert (nat_of_P (pvm - p) - 1 = S (nat_of_P (Ppred pvm - p) - 1))%nat. + assert (W1:= W);rewrite <- Plt_lt in W. + rewrite !Pminus_minus;trivial. + assert (W2:=nat_of_P_pos (Ppred pvm)). + omega. + rewrite Plt_lt. + apply lt_trans with (1:= W1);omega. + rewrite H3;simpl;apply IHlvm;trivial. + intros _ Heq;inversion Heq;clear Heq;subst;unfold wf_vmap; + simpl;intros (Hwf1, Hwf2);repeat split;simpl. + rewrite Psucc_S; assert (W:= nat_of_P_pos pvm);omega. + rewrite Hh;trivial. + rewrite Psucc_S;omega. + intros p Hlt; + assert (nat_of_P (Psucc pvm - p) - 1 = S (nat_of_P (pvm - p) - 1))%nat. + assert (W1:= Hlt);rewrite <- Plt_lt in W1. + rewrite !Pminus_minus;trivial. + rewrite Psucc_S;omega. + rewrite Plt_lt, Psucc_S;omega. + rewrite H;trivial. + unfold is_true;rewrite <- Zlt_is_lt_bool. + rewrite Zpos_succ_morphism;omega. + destruct (check_aux_interp_aux _ _ _ wf_t_atom _ _ Hh) as (z,Hz). + rewrite Hz;unfold interp_vmap;simpl. + assert (nat_of_P (Psucc pvm - pvm) = 1%nat). + rewrite Pplus_one_succ_l, Pminus_minus, Pplus_plus. + change (nat_of_P 1) with 1%nat;omega. + rewrite Plt_lt, Pplus_plus. + change (nat_of_P 1) with 1%nat;omega. + rewrite H;simpl;rewrite Hz;trivial. + Qed. + + Lemma bounded_pexpr_le : + forall p p', + (nat_of_P p <= nat_of_P p')%nat -> + forall pe, + bounded_pexpr p pe -> bounded_pexpr p' pe. + Proof. + unfold is_true;induction pe;simpl;trivial. + rewrite <- !Zlt_is_lt_bool; rewrite <- Ple_le in H. + intros H1;apply Zlt_le_trans with (1:= H1);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. + Qed. + + Lemma interp_pexpr_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 pe, + bounded_pexpr (fst vm) pe -> + Zeval_expr (interp_vmap vm) pe = Zeval_expr (interp_vmap vm') pe. + Proof. + intros vm vm' Hnth. + unfold is_true;induction pe;simpl;trivial. + unfold interp_vmap, is_true;rewrite <- Zlt_is_lt_bool. + intros Hlt;rewrite Hnth;trivial. + rewrite <- Plt_lt;trivial. + rewrite andb_true_iff;intros (H1,H2);rewrite IHpe1, IHpe2;trivial. + rewrite andb_true_iff;intros (H1,H2);rewrite IHpe1, IHpe2;trivial. + rewrite andb_true_iff;intros (H1,H2);rewrite IHpe1, IHpe2;trivial. + intros H1;rewrite IHpe;trivial. + intros H1;rewrite IHpe;trivial. + Qed. + + Lemma build_pexpr_atom_aux_correct : + forall (build_pexpr : vmap -> hatom -> vmap * PExpr Z) h i, + (forall h' vm vm' pe, + h' < h -> + Typ.eqb (get_type t_i t_func t_atom h') Typ.TZ -> + build_pexpr vm h' = (vm',pe) -> + wf_vmap vm -> + wf_vmap vm' /\ + (nat_of_P (fst vm) <= nat_of_P (fst vm'))%nat /\ + (forall p, + (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)) /\ + bounded_pexpr (fst vm') pe /\ + t_interp.[h'] = Bval t_i Typ.TZ (Zeval_expr (interp_vmap vm') pe))-> + forall a vm vm' pe, + h < i -> + lt_atom h a -> + check_atom a Typ.TZ -> + build_pexpr_atom_aux build_pexpr vm a = (vm',pe) -> + wf_vmap vm -> + wf_vmap vm' /\ + (nat_of_P (fst vm) <= nat_of_P (fst vm'))%nat /\ + (forall p, + (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)) /\ + bounded_pexpr (fst vm') pe /\ + interp_atom a = Bval t_i Typ.TZ (Zeval_expr (interp_vmap vm') pe). + Proof. + intros build_pexpr h i Hb a. +Opaque build_z_atom interp_aux. + case a;simpl; + try (intros;apply build_pexpr_atom_aux_correct_z;trivial;fail). + + intros u; destruct u; intros j vm vm' pe _H_ Hlt Ht; + try (intros;apply build_pexpr_atom_aux_correct_z;trivial;fail). + generalize (Hb j vm vm'). + destruct (build_pexpr vm j) as (vm0, pe0); intro W1. + intros Heq Hwf;inversion Heq;clear Heq;subst. + assert (W:= W1 pe0 Hlt Ht (refl_equal _) Hwf). + decompose [and] W;clear W W1. + destruct H;repeat split;trivial. +Transparent interp_aux. + simpl;rewrite H4;trivial. + + intro b; destruct b; intros j k vm vm' pe HH Hlt Ht; + try (intros;apply build_pexpr_atom_aux_correct_z;trivial;fail). + + generalize (Hb j vm). destruct (build_pexpr vm j) as (vm0,pe0). intro IH. + generalize (Hb k vm0). destruct (build_pexpr vm0 k) as (vm1,pe1). intro IH'. + simpl in Ht;unfold is_true in Ht;rewrite !andb_true_iff in Ht; + decompose [and] Ht;clear Ht. + unfold is_true in Hlt;rewrite andb_true_iff in Hlt;destruct Hlt as (Hlt1, Hlt2). + intros Heq Hwf;inversion Heq;clear Heq;subst. + assert (W:= IH _ _ Hlt1 H (refl_equal _) Hwf);clear IH. + decompose [and] W;clear W. + assert (W:= IH' _ _ Hlt2 H0 (refl_equal _) H1);clear IH'. + decompose [and] W;clear W. + destruct H5;repeat split;trivial. + apply le_trans with (1:= H3);trivial. + intros p Hlt;rewrite H2, H7;trivial. + apply lt_le_trans with (1:=Hlt);trivial. + simpl;rewrite H9, andb_true_r. + apply (bounded_pexpr_le (fst vm0));auto with arith. + simpl;rewrite H6, H11;simpl. + rewrite (interp_pexpr_le _ _ H7 _ H4);trivial. + + generalize (Hb j vm). destruct (build_pexpr vm j) as (vm0,pe0); intro IH. + generalize (Hb k vm0). destruct (build_pexpr vm0 k) as (vm1,pe1). intro IH'. + simpl in Ht;unfold is_true in Ht;rewrite !andb_true_iff in Ht; + decompose [and] Ht;clear Ht. + unfold is_true in Hlt;rewrite andb_true_iff in Hlt;destruct Hlt as (Hlt1, Hlt2). + intros Heq Hwf;inversion Heq;clear Heq;subst. + assert (W:= IH _ _ Hlt1 H (refl_equal _) Hwf);clear IH. + decompose [and] W;clear W. + assert (W:= IH' _ _ Hlt2 H0 (refl_equal _) H1);clear IH'. + decompose [and] W;clear W. + destruct H5;repeat split;trivial. + apply le_trans with (1:= H3);trivial. + intros p Hlt;rewrite H2, H7;trivial. + apply lt_le_trans with (1:=Hlt);trivial. + simpl;rewrite H9, andb_true_r. + apply (bounded_pexpr_le (fst vm0));auto with arith. + simpl;rewrite H6, H11;simpl. + rewrite (interp_pexpr_le _ _ H7 _ H4);trivial. + + generalize (Hb j vm). destruct (build_pexpr vm j) as (vm0,pe0); intro IH. + generalize (Hb k vm0). destruct (build_pexpr vm0 k) as (vm1,pe1). intro IH'. + simpl in Ht;unfold is_true in Ht;rewrite !andb_true_iff in Ht; + decompose [and] Ht;clear Ht. + unfold is_true in Hlt;rewrite andb_true_iff in Hlt;destruct Hlt as (Hlt1, Hlt2). + intros Heq Hwf;inversion Heq;clear Heq;subst. + assert (W:= IH _ _ Hlt1 H (refl_equal _) Hwf);clear IH. + decompose [and] W;clear W. + assert (W:= IH' _ _ Hlt2 H0 (refl_equal _) H1);clear IH'. + decompose [and] W;clear W. + destruct H5;repeat split;trivial. + apply le_trans with (1:= H3);trivial. + intros p Hlt;rewrite H2, H7;trivial. + apply lt_le_trans with (1:=Hlt);trivial. + simpl;rewrite H9, andb_true_r. + apply (bounded_pexpr_le (fst vm0));auto with arith. + simpl;rewrite H6, H11;simpl. + rewrite (interp_pexpr_le _ _ H7 _ H4);trivial. + Qed. +Transparent build_z_atom. + + Lemma build_pexpr_atom_aux_correct' : + forall (build_pexpr : vmap -> hatom -> vmap * PExpr Z), + (forall h' vm vm' pe, + Typ.eqb (get_type t_i t_func t_atom h') Typ.TZ -> + build_pexpr vm h' = (vm',pe) -> + wf_vmap vm -> + wf_vmap vm' /\ + (nat_of_P (fst vm) <= nat_of_P (fst vm'))%nat /\ + (forall p, + (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)) /\ + bounded_pexpr (fst vm') pe /\ + t_interp.[h'] = Bval t_i Typ.TZ (Zeval_expr (interp_vmap vm') pe))-> + forall a vm vm' pe, + check_atom a Typ.TZ -> + build_pexpr_atom_aux build_pexpr vm a = (vm',pe) -> + wf_vmap vm -> + wf_vmap vm' /\ + (nat_of_P (fst vm) <= nat_of_P (fst vm'))%nat /\ + (forall p, + (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)) /\ + bounded_pexpr (fst vm') pe /\ + interp_atom a = Bval t_i Typ.TZ (Zeval_expr (interp_vmap vm') pe). + Proof. + intros build_pexpr Hb a. +Opaque build_z_atom interp_aux. + case a;simpl; + try (intros;apply build_pexpr_atom_aux_correct_z;trivial;fail). + intro u; destruct u; intros i vm vm' pe Ht; + try (intros;apply build_pexpr_atom_aux_correct_z;trivial;fail). + generalize (Hb i vm); clear Hb. + destruct (build_pexpr vm i) as (vm0,pe0); intro IH. + intros Heq Hwf;inversion Heq;clear Heq;subst. + assert (W:= IH vm' pe0 Ht (refl_equal _) Hwf). + decompose [and] W;clear W IH. + destruct H;repeat split;trivial. +Transparent interp_aux. + simpl;rewrite H4;trivial. + + intro b; destruct b; intros j k vm vm' pe Ht; + try (intros;apply build_pexpr_atom_aux_correct_z;trivial;fail). + generalize (Hb j vm). + destruct (build_pexpr vm j) as (vm0,pe0); intro IH. + generalize (Hb k vm0); clear Hb. + destruct (build_pexpr vm0 k) as (vm1,pe1); intro IH'. + simpl in Ht;unfold is_true in Ht;rewrite !andb_true_iff in Ht; + decompose [and] Ht;clear Ht. + intros Heq Hwf;inversion Heq;clear Heq;subst. + assert (W:= IH _ _ H (refl_equal _) Hwf);clear IH. + decompose [and] W;clear W. + assert (W:= IH' _ _ H0 (refl_equal _) H1);clear IH'. + decompose [and] W;clear W. + destruct H5;repeat split;trivial. + apply le_trans with (1:= H3);trivial. + intros p Hlt;rewrite H2, H7;trivial. + apply lt_le_trans with (1:=Hlt);trivial. + simpl;rewrite H9, andb_true_r. + apply (bounded_pexpr_le (fst vm0));auto with arith. + simpl;rewrite H6, H11;simpl. + rewrite (interp_pexpr_le _ _ H7 _ H4);trivial. + + generalize (Hb j vm). + destruct (build_pexpr vm j) as (vm0,pe0); intro IH. + generalize (Hb k vm0); clear Hb. + destruct (build_pexpr vm0 k) as (vm1,pe1); intro IH'. + simpl in Ht;unfold is_true in Ht;rewrite !andb_true_iff in Ht; + decompose [and] Ht;clear Ht. + intros Heq Hwf;inversion Heq;clear Heq;subst. + assert (W:= IH _ _ H (refl_equal _) Hwf);clear IH. + decompose [and] W;clear W. + assert (W:= IH' _ _ H0 (refl_equal _) H1);clear IH'. + decompose [and] W;clear W. + destruct H5;repeat split;trivial. + apply le_trans with (1:= H3);trivial. + intros p Hlt;rewrite H2, H7;trivial. + apply lt_le_trans with (1:=Hlt);trivial. + simpl;rewrite H9, andb_true_r. + apply (bounded_pexpr_le (fst vm0));auto with arith. + simpl;rewrite H6, H11;simpl. + rewrite (interp_pexpr_le _ _ H7 _ H4);trivial. + + generalize (Hb j vm). + destruct (build_pexpr vm j) as (vm0,pe0); intro IH. + generalize (Hb k vm0); clear Hb. + destruct (build_pexpr vm0 k) as (vm1,pe1); intro IH'. + simpl in Ht;unfold is_true in Ht;rewrite !andb_true_iff in Ht; + decompose [and] Ht;clear Ht. + intros Heq Hwf;inversion Heq;clear Heq;subst. + assert (W:= IH _ _ H (refl_equal _) Hwf);clear IH. + decompose [and] W;clear W. + assert (W:= IH' _ _ H0 (refl_equal _) H1);clear IH'. + decompose [and] W;clear W. + destruct H5;repeat split;trivial. + apply le_trans with (1:= H3);trivial. + intros p Hlt;rewrite H2, H7;trivial. + apply lt_le_trans with (1:=Hlt);trivial. + simpl;rewrite H9, andb_true_r. + apply (bounded_pexpr_le (fst vm0));auto with arith. + simpl;rewrite H6, H11;simpl. + rewrite (interp_pexpr_le _ _ H7 _ H4);trivial. +Qed. +Transparent build_z_atom. + + Lemma build_pexpr_correct_aux : + forall h vm vm' pe, + (to_Z h < to_Z (length t_atom))%Z -> + Typ.eqb (get_type t_i t_func t_atom h) Typ.TZ -> + build_pexpr vm h = (vm',pe) -> + wf_vmap vm -> + wf_vmap vm' /\ + (nat_of_P (fst vm) <= nat_of_P (fst vm'))%nat /\ + (forall p, + (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)) /\ + bounded_pexpr (fst vm') pe /\ + t_interp.[h] = Bval t_i Typ.TZ (Zeval_expr (interp_vmap vm') pe). + Proof. + unfold build_pexpr. + apply foldi_down_cont_ZInd. + intros z Hz h vm vm' pe Hh. + assert (W:=to_Z_bounded h);rewrite to_Z_0 in Hz. + elimtype False;omega. + intros i cont Hpos Hlen Hrec. + intros h vm vm' pe;unfold is_true;rewrite <-ltb_spec;intros. + rewrite t_interp_wf;trivial. + apply build_pexpr_atom_aux_correct with cont h i;trivial. + intros;apply Hrec;auto. + unfold is_true in H3;rewrite ltb_spec in H, H3;omega. + unfold wf, is_true in wf_t_atom. + rewrite forallbi_spec in wf_t_atom. + apply wf_t_atom. + rewrite ltb_spec in H;rewrite leb_spec in Hlen;rewrite ltb_spec;omega. + unfold wt, is_true in wt_t_atom. + rewrite forallbi_spec in wt_t_atom. + change (is_true(Typ.eqb (get_type t_i t_func t_atom h) Typ.TZ)) in H0. + rewrite Typ.eqb_spec in H0;rewrite <- H0. + apply wt_t_atom. + rewrite ltb_spec in H;rewrite leb_spec in Hlen;rewrite ltb_spec;omega. + Qed. + + Lemma build_pexpr_correct : + forall h vm vm' pe, + Typ.eqb (get_type t_i t_func t_atom h) Typ.TZ -> + build_pexpr vm h = (vm',pe) -> + wf_vmap vm -> + wf_vmap vm' /\ + (nat_of_P (fst vm) <= nat_of_P (fst vm'))%nat /\ + (forall p, + (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)) /\ + bounded_pexpr (fst vm') pe /\ + t_interp.[h] = Bval t_i Typ.TZ (Zeval_expr (interp_vmap vm') pe). + Proof. + intros. + case_eq (h < length t_atom);intros. + apply build_pexpr_correct_aux;trivial. + rewrite <- ltb_spec;trivial. + revert H;unfold get_type,get_type'. + rewrite PArray.get_outofbound, default_t_interp. + revert H0. + unfold build_pexpr. + case_eq (0 < length t_atom);intros Heq. + rewrite foldi_down_cont_gt;trivial. + rewrite PArray.get_outofbound;trivial. + Opaque build_z_atom. + rewrite def_t_atom;simpl. + intros HH H;revert HH H1;apply build_pexpr_atom_aux_correct_z;trivial. + rewrite foldi_down_cont_eq;trivial. + rewrite PArray.get_outofbound;trivial. + rewrite def_t_atom;simpl. + intros HH H;revert HH H1;apply build_pexpr_atom_aux_correct_z;trivial. + rewrite <- not_true_iff_false, ltb_spec, to_Z_0 in Heq. + assert (W:= to_Z_bounded (length t_atom)). + apply to_Z_inj;rewrite to_Z_0;omega. + rewrite length_t_interp;trivial. + Qed. +Transparent build_z_atom. + + Lemma build_pexpr_atom_correct : + forall a vm vm' pe, + check_atom a Typ.TZ -> + build_pexpr_atom_aux build_pexpr vm a = (vm',pe) -> + wf_vmap vm -> + wf_vmap vm' /\ + (nat_of_P (fst vm) <= nat_of_P (fst vm'))%nat /\ + (forall p, + (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)) /\ + bounded_pexpr (fst vm') pe /\ + interp_atom a = Bval t_i Typ.TZ (Zeval_expr (interp_vmap vm') pe). + Proof. + apply build_pexpr_atom_aux_correct';apply build_pexpr_correct. + Qed. + + Lemma build_formula_atom_correct : + forall a vm vm' f t, + check_atom a t -> + build_formula_atom vm a = Some (vm',f) -> + wf_vmap vm -> + wf_vmap vm' /\ + (nat_of_P (fst vm) <= nat_of_P (fst vm'))%nat /\ + (forall p, + (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)) /\ + bounded_formula (fst vm') f /\ + (interp_bool t_i (interp_atom a) <->Zeval_formula (interp_vmap vm') f). + Proof. + intros a vm vm' f t. + destruct a;simpl;try discriminate. + case_eq (build_op2 b);try discriminate. + intros o Heq Ht. + assert (Typ.eqb Typ.Tbool t && Typ.eqb (get_type t_i t_func t_atom i) Typ.TZ && Typ.eqb (get_type t_i t_func t_atom i0) Typ.TZ). + destruct b;try discriminate;trivial. + destruct t0;try discriminate;trivial. + unfold is_true in H;rewrite !andb_true_iff in H;decompose [and] H;clear H. + case_eq (build_pexpr vm i);intros vm0 pe1 Heq1. + case_eq (build_pexpr vm0 i0);intros vm1 pe2 Heq2. + intros H Hwf;inversion H;clear H;subst. + assert (W1:= build_pexpr_correct _ _ _ _ H3 Heq1 Hwf). + decompose [and] W1;clear W1. + assert (W1:= build_pexpr_correct _ _ _ _ H1 Heq2 H). + decompose [and] W1;clear W1. + split;trivial. + split;[ apply le_trans with (1:= H4);trivial | ]. + split. + intros p Hlt;rewrite H0, H8;trivial. + apply lt_le_trans with (1:= Hlt);trivial. + split. + unfold bounded_formula;simpl;rewrite H10, andb_true_r. + apply (bounded_pexpr_le (fst vm0));auto with arith. + rewrite (interp_pexpr_le _ _ H8 _ H5) in H7. + rewrite H7,H12;destruct b;try discriminate;simpl in Heq |- *; + inversion Heq;clear Heq;subst;simpl. + symmetry;apply Zlt_is_lt_bool. + rewrite Zle_is_le_bool;tauto. + rewrite Zge_iff_le. + unfold Zge_bool;rewrite <- Zcompare_antisym. + rewrite Zle_is_le_bool;unfold Zle_bool. + destruct + (Zeval_expr (interp_vmap vm') pe2 ?= Zeval_expr (interp_vmap vm') pe1)%Z; + simpl;tauto. + symmetry;apply Zgt_is_gt_bool. + destruct t0;inversion H13;clear H13;subst. + simpl. + symmetry;apply (Zeq_is_eq_bool (Zeval_expr (interp_vmap vm') pe1) (Zeval_expr (interp_vmap vm') pe2)). + Qed. + + Lemma build_formula_correct : + forall h' vm vm' f, + build_formula vm h' = Some (vm',f) -> + wf_vmap vm -> + wf_vmap vm' /\ + (nat_of_P (fst vm) <= nat_of_P (fst vm'))%nat /\ + (forall p, + (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)) /\ + bounded_formula (fst vm') f /\ + (interp_form_hatom h' <-> Zeval_formula (interp_vmap vm') f). + Proof. + unfold build_formula;intros h. + unfold Atom.interp_form_hatom, Atom.interp_hatom. + rewrite t_interp_wf;trivial. + intros;apply build_formula_atom_correct with + (get_type t_i t_func t_atom h);trivial. + unfold wt, is_true in wt_t_atom;rewrite forallbi_spec in wt_t_atom. + case_eq (h < length t_atom);intros Heq;unfold get_type;auto. + unfold get_type'. + rewrite !PArray.get_outofbound, default_t_interp, def_t_atom;trivial; try reflexivity. + rewrite length_t_interp;trivial. + Qed. + + + Lemma build_not2_pos_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 -> bounded_bformula (fst vm) (build_not2 i f) /\ (Form.interp interp_form_hatom 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')). + unfold Lit.interp; rewrite H3; auto. + intros b f' H4; rewrite negb_involutive; simpl; split. + intros Hb H5; apply H5; rewrite <- H4; auto. + intro H5; case_eq b; auto; intro H6; elim H5; intro H7; rewrite <- H4 in H7; rewrite H7 in H6; discriminate. + 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 t_form (Form.Fnot2 i l) <-> eval_f (Zeval_formula (interp_vmap vm)) (N (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')). + 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. + intros b f' H4; rewrite negb_involutive; simpl; split. + intros Hb H5; apply H5; rewrite <- H4; auto. + intro H5; case_eq b; auto; intro H6; elim H5; intro H7; rewrite <- H4 in H7; rewrite H7 in H6; discriminate. + Qed. + + + Lemma bounded_bformula_le : + forall p p', + (nat_of_P p <= nat_of_P p')%nat -> + forall bf, + 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. + 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 a;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. + + + Lemma build_hform_correct : + forall (build_var : vmap -> var -> option (vmap*BFormula (Formula Z))), + (forall v vm vm' bf, + build_var vm v = Some (vm', bf) -> + wf_vmap vm -> + wf_vmap vm' /\ + (nat_of_P (fst vm) <= nat_of_P (fst vm'))%nat /\ + (forall p, + (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)) /\ + bounded_bformula (fst vm') bf /\ + (Var.interp rho v <-> eval_f (Zeval_formula (interp_vmap vm')) bf)) -> + forall f vm vm' bf, + build_hform build_var vm f = Some (vm', bf) -> + wf_vmap vm -> + wf_vmap vm' /\ + (nat_of_P (fst vm) <= nat_of_P (fst vm'))%nat /\ + (forall p, + (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)) /\ + bounded_bformula (fst vm') bf /\ + (Form.interp interp_form_hatom t_form f <-> eval_f (Zeval_formula (interp_vmap vm')) bf). + Proof. + unfold build_hform; intros build_var Hbv [h| | |i l|l|l|l|a b|a b|a b c] vm vm' bf; try discriminate. + (* Fatom *) + case_eq (build_formula vm h); try discriminate; intros [vm0 f] Heq H1 H2; inversion H1; subst vm0; subst bf; apply build_formula_correct; auto. + (* Ftrue *) + intros H H1; inversion H; subst vm'; subst bf; split; auto; split; [omega| ]; do 4 split; auto. + (* Ffalse *) + intros H H1; inversion H; subst vm'; subst bf; split; auto; split; [omega| ]; do 3 (split; auto); discriminate. + (* Fnot2 *) + case_eq (build_var vm (Lit.blit l)); try discriminate; intros [vm0 f] Heq H H1; inversion H; subst vm0; subst bf; destruct (Hbv _ _ _ _ Heq H1) as [H2 [H3 [H4 [H5 H6]]]]; do 3 (split; auto); case_eq (Lit.is_pos l); [apply build_not2_pos_correct|apply build_not2_neg_correct]; auto. + (* Fand *) + simpl; unfold afold_left; case (length l == 0). + intro H; inversion H; subst vm'; subst bf; simpl; intro H1; split; auto; split; [omega| ]; do 3 (split; auto). + 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))). + 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. + intros i a b _ H1; case a; try discriminate; intros [vm0 f0] IH vm' bf; case_eq (build_var vm0 (Lit.blit (l .[ i]))); try discriminate; intros [vm1 f1] Heq H2 H3; inversion H2; subst vm'; subst bf; destruct (IH _ _ (refl_equal (Some (vm0, f0))) H3) as [H5 [H6 [H7 [H8 H9]]]]; destruct (Hbv _ _ _ _ Heq H5) as [H10 [H11 [H12 [H13 H14]]]]; split; auto; split; [eauto with arith| ]; split. + intros p H15; rewrite H7; auto; apply H12; eauto with arith. + split. + simpl; rewrite (bounded_bformula_le _ _ H11 _ H8); case (Lit.is_pos (l .[ i])); rewrite H13; auto. + 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 andb_true_r; try rewrite andb_false_r; try (intros; split; auto); try discriminate; intros [H20 H21]; auto. + (* For *) + simpl; unfold afold_left; case (length l == 0). + intro H; inversion H; subst vm'; subst bf; simpl; intro H1; split; auto; split; [omega| ]; do 3 (split; auto); 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))). + 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. + intros i a b _ H1; case a; try discriminate; intros [vm0 f0] IH vm' bf; case_eq (build_var vm0 (Lit.blit (l .[ i]))); try discriminate; intros [vm1 f1] Heq H2 H3; inversion H2; subst vm'; subst bf; destruct (IH _ _ (refl_equal (Some (vm0, f0))) H3) as [H5 [H6 [H7 [H8 H9]]]]; destruct (Hbv _ _ _ _ Heq H5) as [H10 [H11 [H12 [H13 H14]]]]; split; auto; split; [eauto with arith| ]; split. + intros p H15; rewrite H7; auto; apply H12; eauto with arith. + split. + simpl; rewrite (bounded_bformula_le _ _ H11 _ H8); case (Lit.is_pos (l .[ i])); rewrite H13; auto. + 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; try (intros [H20|H20]; auto; 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; split; [omega| ]; do 3 (split; auto). + 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); unfold Lit.interp; rewrite Heq2; auto; 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; intro H9; rewrite H7 in H9; elim H8; auto. + 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))). + 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); 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 .[ length l - 1]))); auto; intro H4; elim H3; rewrite <- H14; auto. + intros i a b _ H1; case a; try discriminate; intros [vm0 f0] IH vm' bf; case_eq (build_var vm0 (Lit.blit (l .[ i]))); try discriminate; intros [vm1 f1] Heq H2 H3; inversion H2; subst vm'; subst bf; destruct (IH _ _ (refl_equal (Some (vm0, f0))) H3) as [H5 [H6 [H7 [H8 H9]]]]; destruct (Hbv _ _ _ _ Heq H5) as [H10 [H11 [H12 [H13 H14]]]]; split; auto; split; [eauto with arith| ]; split. + intros p H15; rewrite H7; auto; apply H12; eauto with arith. + split. + simpl; rewrite (bounded_bformula_le _ _ H11 _ H8); case (Lit.is_pos (l .[ i])); rewrite H13; auto. + 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; try discriminate; simpl; intro H; apply H; discriminate. + (* 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; split; [eauto with arith| ]; split. + intros p H18; rewrite H5; auto; rewrite H10; eauto with arith. + split. + case (Lit.is_pos a); case (Lit.is_pos b); simpl; rewrite H11; rewrite (bounded_bformula_le _ _ H9 _ H6); auto. + simpl; rewrite (interp_bformula_le _ _ H10 _ H6) in H7; case_eq (Lit.is_pos a); intro Ha; case_eq (Lit.is_pos b); intro Hb; unfold Lit.interp; rewrite Ha, Hb; simpl; rewrite <- H12; rewrite <- H7; (case (Var.interp rho (Lit.blit a)); case (Var.interp rho (Lit.blit b))); split; auto; try discriminate; simpl. + intros [_ [H20|H20]]; elim H20; reflexivity. + intros _; split; [left; reflexivity|right; intro H20; discriminate]. + intros _; split; [right; reflexivity|left; intro H20; discriminate]. + intros [[H20|H20] _]; discriminate. + intros [_ [H20|H20]]; elim H20; [reflexivity|discriminate]. + intros [[H20|H20] _]; [discriminate|elim H20; reflexivity]. + intros _; split; [right|left]; discriminate. + intros [[H20|H20] _]; [elim H20; reflexivity|discriminate]. + intros [_ [H20|H20]]; elim H20; [discriminate|reflexivity]. + intros _; split; [left|right]; discriminate. + intros [[H20|H20] _]; elim H20; reflexivity. + intros _; split; [right; discriminate|left; intro H21; apply H21; reflexivity]. + intros _; split; [left; discriminate|right; intro H21; apply H21; reflexivity]. + intros [_ [H20|H20]]; elim H20; discriminate. + (* Fiff *) + 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; split; [eauto with arith| ]; split. + intros p H18; rewrite H5; auto; rewrite H10; eauto with arith. + split. + case (Lit.is_pos a); case (Lit.is_pos b); simpl; rewrite H11; rewrite (bounded_bformula_le _ _ H9 _ H6); auto. + simpl; rewrite (interp_bformula_le _ _ H10 _ H6) in H7; case_eq (Lit.is_pos a); intro Ha; case_eq (Lit.is_pos b); intro Hb; unfold Lit.interp; rewrite Ha, Hb; simpl; rewrite <- H12; rewrite <- H7; (case (Var.interp rho (Lit.blit a)); case (Var.interp rho (Lit.blit b))); split; auto; try discriminate; simpl. + intros [_ [H20|H20]]; [elim H20; reflexivity|discriminate]. + intros [[H20|H20] _]; [discriminate|elim H20; reflexivity]. + intros _; split; [right|left]; discriminate. + intros [_ [H20|H20]]; elim H20; reflexivity. + intros _; split; [left; reflexivity|right; discriminate]. + intros _; split; [right; intro H20; apply H20; reflexivity|left; discriminate]. + intros [[H20|H20] _]; [ |elim H20]; discriminate. + intros [[H20|H20] _]; elim H20; reflexivity. + intros _; split; [right; discriminate|left; intro H20; apply H20; reflexivity]. + intros _; split; [left; discriminate|right; reflexivity]. + intros [_ [H20|H20]]; [elim H20| ]; discriminate. + intros [[H20|H20] _]; elim H20; [reflexivity|discriminate]. + intros [_ [H20|H20]]; elim H20; [discriminate|reflexivity]. + intros _; split; [left|right]; discriminate. + (* Fite *) + 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; case_eq (build_var vm2 (Lit.blit c)); try discriminate; intros [vm3 f3] Heq3 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]]]]; destruct (Hbv _ _ _ _ Heq3 H8) as [H13 [H14 [H15 [H16 H17]]]]; split; auto; split; [eauto with arith| ]; split. + intros p H18; rewrite H5; auto; rewrite H10; eauto with arith. + assert (H18: (Pos.to_nat (fst vm1) <= Pos.to_nat (fst vm3))%nat) by eauto with arith. + split. + case (Lit.is_pos a); case (Lit.is_pos b); case (Lit.is_pos c); simpl; rewrite H16; rewrite (bounded_bformula_le _ _ H14 _ H11); rewrite (bounded_bformula_le _ _ H18 _ H6); auto. + simpl; rewrite (interp_bformula_le _ _ H15 _ H11) in H12; rewrite (interp_bformula_le _ vm3) in H7; [ |intros p Hp; rewrite H10; eauto with arith|auto]; case_eq (Lit.is_pos a); intro Ha; case_eq (Lit.is_pos b); intro Hb; case_eq (Lit.is_pos c); intro Hc; unfold Lit.interp; rewrite Ha, Hb, Hc; simpl; rewrite <- H17; rewrite <- H12; rewrite <- H7; (case (Var.interp rho (Lit.blit a)); [case (Var.interp rho (Lit.blit b))|case (Var.interp rho (Lit.blit c))]); split; auto; try discriminate; try (intros [[H20 H21]|[H20 H21]]; auto); try (intros _; left; split; auto; discriminate); try (intros _; right; split; auto; discriminate); try (elim H20; discriminate); try (elim H21; discriminate); try (simpl; intro H; left; split; auto; discriminate); try (revert H; case (Var.interp rho (Lit.blit c)); discriminate); try (revert H; case (Var.interp rho (Lit.blit b)); discriminate); try (intro H20; rewrite H20 in H; discriminate); simpl. + intro H; right; split; auto. + intro H; right; split; auto. + intro H; right; split; auto. + intro H20; rewrite H20 in H; discriminate. + revert H21; case (Var.interp rho (Lit.blit c)); auto. + right; split; auto; intro H20; rewrite H20 in H; discriminate. + revert H21; case (Var.interp rho (Lit.blit c)); auto. + intro H; right; split; auto. + intro H; right; split; auto. + intro H; left; split; try discriminate; revert H; case (Var.interp rho (Lit.blit b)); discriminate. + revert H21; case (Var.interp rho (Lit.blit b)); auto. + intro H; left; split; try discriminate; revert H; case (Var.interp rho (Lit.blit b)); discriminate. + revert H21; case (Var.interp rho (Lit.blit b)); auto. + intro H; right; split; auto; revert H; case (Var.interp rho (Lit.blit c)); discriminate. + revert H21; case (Var.interp rho (Lit.blit c)); auto. + intro H; right; split; auto; revert H; case (Var.interp rho (Lit.blit c)); discriminate. + revert H21; case (Var.interp rho (Lit.blit c)); auto. + intro H; left; split; auto; revert H; case (Var.interp rho (Lit.blit b)); discriminate. + revert H21; case (Var.interp rho (Lit.blit b)); auto. + intro H; left; split; auto; revert H; case (Var.interp rho (Lit.blit b)); discriminate. + revert H21; case (Var.interp rho (Lit.blit b)); auto. + Qed. + + + Lemma build_var_correct : forall v vm vm' bf, + build_var vm v = Some (vm', bf) -> + wf_vmap vm -> + wf_vmap vm' /\ + (nat_of_P (fst vm) <= nat_of_P (fst vm'))%nat /\ + (forall p, + (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)) /\ + bounded_bformula (fst vm') bf /\ + (Var.interp rho v <-> eval_f (Zeval_formula (interp_vmap vm')) bf). + Proof. + unfold build_var; apply foldi_down_cont_ind; try discriminate. + intros i cont _ Hlen Hrec v vm vm' bf; unfold is_true; intros H1 H2; replace (Var.interp rho v) with (Form.interp interp_form_hatom t_form (t_form.[v])). + apply (build_hform_correct cont); auto. + unfold Var.interp; rewrite <- wf_interp_form; auto. + Qed. + + + Lemma build_form_correct : forall f vm vm' bf, + build_form vm f = Some (vm', bf) -> + wf_vmap vm -> + wf_vmap vm' /\ + (nat_of_P (fst vm) <= nat_of_P (fst vm'))%nat /\ + (forall p, + (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)) /\ + bounded_bformula (fst vm') bf /\ + (Form.interp interp_form_hatom t_form f <-> eval_f (Zeval_formula (interp_vmap vm')) bf). + Proof. apply build_hform_correct; apply build_var_correct. Qed. + + + Lemma build_nlit_correct : forall l vm vm' bf, + build_nlit vm l = Some (vm', bf) -> + wf_vmap vm -> + wf_vmap vm' /\ + (nat_of_P (fst vm) <= nat_of_P (fst vm'))%nat /\ + (forall p, + (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)) /\ + bounded_bformula (fst vm') bf /\ + (negb (Lit.interp rho l) <-> eval_f (Zeval_formula (interp_vmap vm')) bf). + Proof. + unfold build_nlit; intros l vm vm' bf; case_eq (build_form vm (t_form .[ Lit.blit (Lit.neg l)])); try discriminate. + intros [vm1 f] Heq H1 H2; inversion H1; subst vm1; subst bf; case_eq (Lit.is_pos (Lit.neg l)); intro Heq2. + replace (negb (Lit.interp rho l)) with (Form.interp interp_form_hatom t_form (t_form .[ Lit.blit (Lit.neg l)])). + apply build_form_correct; auto. + unfold Lit.interp; replace (Lit.is_pos l) with false. + rewrite negb_involutive; unfold Var.interp; rewrite <- wf_interp_form; auto; rewrite Lit.blit_neg; auto. + rewrite Lit.is_pos_neg in Heq2; case_eq (Lit.is_pos l); auto; intro H; rewrite H in Heq2; discriminate. + simpl; destruct (build_form_correct (t_form .[ Lit.blit (Lit.neg l)]) vm vm' f Heq H2) as [H3 [H4 [H5 [H6 [H7 H8]]]]]; do 4 (split; auto); split. + intros H9 H10; pose (H11 := H8 H10); unfold Lit.interp in H9; replace (Lit.is_pos l) with true in H9. + unfold Var.interp in H9; rewrite <- wf_interp_form in H11; auto; rewrite Lit.blit_neg in H11; rewrite H11 in H9; discriminate. + rewrite Lit.is_pos_neg in Heq2; case_eq (Lit.is_pos l); auto; intro H; rewrite H in Heq2; discriminate. + intro H9; case_eq (Lit.interp rho l); intro Heq3; auto; elim H9; apply H7; unfold Lit.interp in Heq3; replace (Lit.is_pos l) with true in Heq3. + unfold Var.interp in Heq3; rewrite <- wf_interp_form; auto; rewrite Lit.blit_neg; auto. + rewrite Lit.is_pos_neg in Heq2; case_eq (Lit.is_pos l); auto; intro H; rewrite H in Heq2; discriminate. + Qed. + + + Lemma build_clause_aux_correct : + forall cl vm vm' bf, + build_clause_aux vm cl = Some (vm',bf) -> + wf_vmap vm -> + wf_vmap vm' /\ + (nat_of_P (fst vm) <= nat_of_P (fst vm'))%nat /\ + (forall p, + (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)) /\ + bounded_bformula (fst vm') bf /\ + (negb (C.interp rho cl) <-> eval_f (Zeval_formula (interp_vmap vm')) bf). + Proof. + induction cl;try discriminate. + case_eq cl. + intros _; simpl;intros;rewrite orb_false_r;apply build_nlit_correct;trivial. + intros i l Heq vm vm' bf;rewrite <- Heq at 2. + change (build_clause_aux vm (a :: i :: l) ) with + ( 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) + | None => None + end + | None => None + end). + case_eq (build_nlit vm a);try discriminate. + intros (vm0, bf1) Heq1 Heq2 Hwf. + rewrite <- Heq in Heq2. + assert (W:= build_nlit_correct _ _ _ _ Heq1 Hwf). + decompose [and] W;clear W. + revert Heq2; case_eq (build_clause_aux vm0 cl);try discriminate. + intros (vm1, fb2) Heq2 W;inversion W;clear W Heq;subst. + assert (W:= IHcl _ _ _ Heq2 H);decompose [and] W;clear W. + split;trivial. + split. + apply le_trans with (1:= H1);trivial. + split. + intros p Hlt;rewrite H0, H5;trivial. + apply lt_le_trans with (1:= Hlt);trivial. + split. + simpl;rewrite H7, andb_true_r. + apply bounded_bformula_le with (2:= H2);trivial. + simpl. + unfold is_true; + rewrite <- (interp_bformula_le _ _ H5), <- H4, <- H9, negb_orb,andb_true_iff; + tauto. + Qed. + + Lemma build_clause_correct : + forall cl vm vm' bf, + build_clause vm cl = Some (vm',bf) -> + wf_vmap vm -> + wf_vmap vm' /\ + (nat_of_P (fst vm) <= nat_of_P (fst vm'))%nat /\ + (forall p, + (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)) /\ + bounded_bformula (fst vm') bf /\ + (C.interp rho cl <-> eval_f (Zeval_formula (interp_vmap vm')) bf). + Proof. + unfold build_clause;intros cl vm vm' bf. + case_eq (build_clause_aux vm cl);try discriminate. + intros (vm1, bf1) Heq W Hwf;inversion W;clear W;subst. + assert (W:= build_clause_aux_correct _ _ _ _ Heq Hwf). + decompose [and] W;clear W. + repeat (split;[trivial;fail | ]). + split;simpl. + rewrite H2;reflexivity. + unfold is_true in *; + destruct (C.interp rho cl);split;simpl;trivial;try discriminate; + try tauto. + intros _ HH;destruct H4. + apply H4 in HH;discriminate. + Qed. + + Local Notation hinterp := (Atom.interp_hatom t_i t_func t_atom). + Local Notation interp := (Atom.interp t_i t_func t_atom). + + 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 -> + Lit.is_pos l -> + rho (Lit.blit l) = + Atom.interp_bool t_i + (Atom.apply_binop t_i t t Typ.Tbool (Typ.i_eqb t_i t) + (hinterp a) (hinterp b)) -> + Typ.eqb (get_type t_i t_func t_atom a) t -> Typ.eqb (get_type t_i t_func t_atom b) t -> + C.interp rho (f a b)) -> + C.interp rho (get_eq l f). + Proof. + intros l f Hf;unfold get_eq. + destruct (Lit.is_pos l); case_eq (t_form.[Lit.blit l]);trivial;intros; + try(case_eq (t_atom.[i]);trivial;intros); try (apply valid_C_true; trivial). + destruct b; try (apply valid_C_true; trivial). + generalize wt_t_atom;unfold Atom.wt;unfold is_true; + rewrite PArray.forallbi_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. auto. + 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. + trivial. + Qed. + + Lemma get_not_le_interp : + forall (l:_lit) (f:Atom.hatom -> Atom.hatom -> C.t), + (forall xa, t_form.[Lit.blit l] = Form.Fatom xa -> + forall a b, t_atom.[xa] = Atom.Abop Atom.BO_Zle a b -> + negb (Lit.is_pos l) -> + rho (Lit.blit l) = + Atom.interp_bool t_i + (Atom.apply_binop t_i Typ.TZ Typ.TZ Typ.Tbool Zle_bool + (hinterp a) (hinterp b)) -> + Typ.eqb (get_type t_i t_func t_atom a) Typ.TZ -> Typ.eqb (get_type t_i t_func t_atom b) Typ.TZ -> + C.interp rho (f a b)) -> + C.interp rho (get_not_le l f). + Proof. + intros l f Hf;unfold get_not_le. + destruct (Lit.is_pos l); case_eq (t_form.[Lit.blit l]);trivial;intros; + try(case_eq (t_atom.[i]);trivial;intros); try (apply valid_C_true; trivial). + destruct b; try (apply valid_C_true; trivial). + generalize wt_t_atom;unfold Atom.wt;unfold is_true; + rewrite PArray.forallbi_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. + simpl; apply Hf with (2:= H0);trivial. auto. + 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. + trivial. + Qed. + + + Lemma interp_binop_eqb_antisym: + forall a b va vb, + interp_atom a = Bval t_i Typ.TZ va -> interp_atom b = Bval t_i Typ.TZ vb -> + (interp_bool t_i + (apply_binop t_i Typ.TZ Typ.TZ Typ.Tbool (Typ.i_eqb t_i Typ.TZ) + (interp a) (interp b)) = false) -> + negb + (interp_bool t_i + (apply_binop t_i Typ.TZ Typ.TZ Typ.Tbool Z.leb + (interp a) (interp b))) = false -> + negb + (interp_bool t_i + (apply_binop t_i Typ.TZ Typ.TZ Typ.Tbool Z.leb + (interp b) (interp a))) = false -> + False. + Proof. + intros a b va vb HHa HHb. + unfold Atom.interp, Atom.interp_hatom. + rewrite HHa, HHb; simpl. + intros. + case_eq (va <=? vb); intros; subst. + case_eq (vb <=? va); intros; subst. + apply Zle_bool_imp_le in H2. + apply Zle_bool_imp_le in H3. + apply Zeq_bool_neq in H. + (*pour la beauté du geste!*) lia. + rewrite H3 in H1; simpl in H1; elim diff_true_false; trivial. + rewrite H2 in H0; simpl in H1; elim diff_true_false; trivial. + Qed. + + + Lemma valid_check_micromega : + forall cl c, C.valid rho (check_micromega cl c). + Proof. + unfold check_micromega; intros cl c. + case_eq (build_clause empty_vmap cl). + intros (vm1, bf) Heq. + destruct (build_clause_correct _ _ _ _ Heq). + red;simpl;auto. + decompose [and] H0. + case_eq (ZTautoChecker bf c);intros Heq2. + unfold C.valid;rewrite H5. + apply ZTautoChecker_sound with c;trivial. + apply C.interp_true. + destruct (Form.check_form_correct interp_form_hatom _ ch_form);trivial. + intros _;apply C.interp_true. + destruct (Form.check_form_correct interp_form_hatom _ ch_form);trivial. + Qed. + + + Lemma valid_check_diseq : + forall c, C.valid rho (check_diseq c). + Proof. + unfold check_diseq; intro c. + case_eq (t_form.[Lit.blit c]);intros;subst; try (unfold C.valid; apply valid_C_true; trivial). + case_eq ((length a) == 3); intros; try (unfold C.valid; apply valid_C_true; trivial). + apply eqb_correct in H0. + apply get_eq_interp; intros. + apply get_not_le_interp; intros. + apply get_not_le_interp; intros. + case_eq ((a0 == a1) && (a0 == b1) && (b == b0) && (b == a2)); intros; subst; + try (unfold C.valid; apply valid_C_true; trivial). + repeat(apply andb_prop in H19; destruct H19). + apply Int63Properties.eqb_spec in H19;apply Int63Properties.eqb_spec in H20;apply Int63Properties.eqb_spec in H21;apply Int63Properties.eqb_spec in H22;subst. + unfold C.interp; simpl; rewrite orb_false_r. + unfold Lit.interp; rewrite Lit.is_pos_lit. + unfold Var.interp; rewrite Lit.blit_lit. + rewrite wf_interp_form, H;simpl. + case_eq (Lit.interp rho (a.[0]) || Lit.interp rho (a.[1]) || Lit.interp rho (a.[2])). + intros;repeat (rewrite orb_true_iff in H19);destruct H19. destruct H19. + apply (afold_left_orb_true int 0); subst; auto. + apply ltb_spec;rewrite H0;compute;trivial. + apply (afold_left_orb_true int 1); auto. + apply ltb_spec;rewrite H0;compute;trivial. + apply (afold_left_orb_true int 2); auto. + apply ltb_spec;rewrite H0;compute;trivial. + intros; repeat (rewrite orb_false_iff in H19);destruct H19. destruct H19. + unfold Lit.interp in H19. + rewrite H3 in H19; unfold Var.interp in H19; rewrite H4 in H19. + unfold Lit.interp in H21. + pose (H24 := H15). apply negb_true_iff in H24. + rewrite H24 in H21. + unfold Var.interp in H21; rewrite H16 in H21. + unfold Lit.interp in H23. + pose (H25 := H9). apply negb_true_iff in H25. + rewrite H25 in H23. + unfold Var.interp in H23; rewrite H10 in H23. + assert (t = Typ.TZ). + generalize H12. clear H12. + destruct (Typ.reflect_eqb (get_type t_i t_func t_atom b0) Typ.TZ) as [H12|H12]; [intros _|discriminate]. + generalize H6. clear H6. + destruct (Typ.reflect_eqb (get_type t_i t_func t_atom b0) t) as [H6|H6]; [intros _|discriminate]. + rewrite <- H6. auto. + rewrite H26 in H19. + case_eq (interp_atom (t_atom .[ b1])); intros t1 v1 Heq1. + assert (H50: t1 = Typ.TZ). + unfold get_type, get_type' in H18. rewrite t_interp_wf in H18; trivial. rewrite Heq1 in H18. simpl in H18. rewrite Typ.eqb_spec in H18. assumption. + subst t1. + case_eq (interp_atom (t_atom .[ a2])); intros t2 v2 Heq2. + assert (H50: t2 = Typ.TZ). + unfold get_type, get_type' in H17. rewrite t_interp_wf in H17; trivial. rewrite Heq2 in H17. simpl in H17. rewrite Typ.eqb_spec in H17. assumption. + subst t2. + subst;elim (interp_binop_eqb_antisym (t_atom.[b1]) (t_atom.[a2]) v1 v2);trivial. + unfold interp_hatom in H19; do 2 rewrite t_interp_wf in H19; trivial. + unfold interp_hatom in H23; do 2 rewrite t_interp_wf in H23; trivial. + unfold interp_hatom in H21; do 2 rewrite t_interp_wf in H21; trivial. + trivial. + destruct H19. + case_eq ((a0 == b0) && (a0 == a2) && (b == a1) && (b == b1)); intros; subst; + try (unfold C.valid; apply valid_C_true; trivial). + repeat(apply andb_prop in H19; destruct H19). + apply Int63Properties.eqb_spec in H19;apply Int63Properties.eqb_spec in H20;apply Int63Properties.eqb_spec in H21;apply Int63Properties.eqb_spec in H22;subst. + unfold C.interp; simpl; rewrite orb_false_r. + unfold Lit.interp; rewrite Lit.is_pos_lit. + unfold Var.interp; rewrite Lit.blit_lit. + rewrite wf_interp_form, H;simpl. + case_eq (Lit.interp rho (a.[0]) || Lit.interp rho (a.[1]) || Lit.interp rho (a.[2])). + intros;repeat (rewrite orb_true_iff in H19);destruct H19. destruct H19. + apply (afold_left_orb_true int 0); auto. + apply ltb_spec;rewrite H0;compute;trivial. + apply (afold_left_orb_true int 1); auto. + apply ltb_spec;rewrite H0;compute;trivial. + apply (afold_left_orb_true int 2); auto. + apply ltb_spec;rewrite H0;compute;trivial. + intros; repeat (rewrite orb_false_iff in H19);destruct H19. destruct H19. + unfold Lit.interp in H19. + rewrite H3 in H19; unfold Var.interp in H19; rewrite H4 in H19. + unfold Lit.interp in H21. + case_eq (Lit.is_pos (a.[2])); intros. + apply negb_true_iff in H15;rewrite H15 in H24; discriminate. + rewrite H24 in H21. + unfold Var.interp in H21;rewrite H16 in H21. + unfold Lit.interp in H23. + case_eq (Lit.is_pos (a.[1])); intros. + apply negb_true_iff in H9; rewrite H9 in H25; discriminate. + rewrite H25 in H23. + unfold Var.interp in H23; rewrite H10 in H23. + rewrite <-H22, <- H20 in H21. + assert (t = Typ.TZ). + rewrite Typ.eqb_spec in H6; rewrite Typ.eqb_spec in H18; subst; auto. + rewrite H26 in H19. + case_eq (interp_atom (t_atom .[ b0])); intros t1 v1 Heq1. + assert (H50: t1 = Typ.TZ). + unfold get_type, get_type' in H12. rewrite t_interp_wf in H12; trivial. rewrite Heq1 in H12. simpl in H12. rewrite Typ.eqb_spec in H12. assumption. + subst t1. + case_eq (interp_atom (t_atom .[ a1])); intros t2 v2 Heq2. + assert (H50: t2 = Typ.TZ). + unfold get_type, get_type' in H11. rewrite t_interp_wf in H11; trivial. rewrite Heq2 in H11. simpl in H11. rewrite Typ.eqb_spec in H11. assumption. + subst t2. + elim (interp_binop_eqb_antisym (t_atom.[b0]) (t_atom.[a1]) v1 v2); trivial. + unfold interp_hatom in H19; do 2 rewrite t_interp_wf in H19; trivial. + unfold interp_hatom in H21; do 2 rewrite t_interp_wf in H21; trivial. + unfold interp_hatom in H23; do 2 rewrite t_interp_wf in H23; trivial. + trivial. + Qed. + + End Proof. + +End certif. |