diff options
Diffstat (limited to 'src/State.v')
| -rw-r--r-- | src/State.v | 572 |
1 files changed, 572 insertions, 0 deletions
diff --git a/src/State.v b/src/State.v new file mode 100644 index 0000000..d793410 --- /dev/null +++ b/src/State.v @@ -0,0 +1,572 @@ +(**************************************************************************) +(* *) +(* 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 List. +Require Import Bool. +Require Import Int63. +Require Import PArray. + +(* Require Import AxiomesInt. *) + +Local Open Scope int63_scope. +Local Open Scope array_scope. + +Coercion is_true (x: bool) := x = true. + +Set Vm Optimize. + +Notation var := int (only parsing). + +(* Variables interpretation *) +Module Valuation. +(* TODO : Should be var -> Prop *) + Definition t := var -> bool. + Definition wf (rho : t) : Prop := rho 0 /\ ~ rho 1. + +End Valuation. + + +Module Var. + + Definition _true : var := 0. (* true *) + Register _true as PrimInline. + + Definition _false : var := 1. (* false *) + + Definition interp (rho:Valuation.t) (x:var) : bool := rho x. + + Lemma interp_true : forall rho, Valuation.wf rho -> interp rho _true. + Proof. intros rho [H _];exact H. Qed. + + Lemma interp_false : forall rho, Valuation.wf rho -> ~ interp rho _false. + Proof. intros rho [_ H];exact H. Qed. + +End Var. + +Notation _lit := int (only parsing). + +Module Lit. + + Definition is_pos (l:_lit) := is_even l. + Register is_pos as PrimInline. + + Definition blit (l:_lit) : var := l >> 1. + Register blit as PrimInline. + + Definition lit (x:var) : _lit := x << 1. + Register lit as PrimInline. + + Definition neg (l:_lit) : _lit := l lxor 1. + Register neg as PrimInline. + + Definition nlit (x:var) : _lit := neg (lit x). + Register nlit as PrimInline. + + Definition _true : _lit := Eval compute in lit Var._true. + Register _true as PrimInline. + + Lemma lit_true : _true = lit Var._true. + Proof. reflexivity. Qed. + + Definition _false : _lit := Eval compute in lit Var._false. + Register _false as PrimInline. + + Lemma lit_false : _false = lit Var._false. + Proof. reflexivity. Qed. + + Definition eqb (l l' : _lit) := l == l'. + Register eqb as PrimInline. + + Lemma eqb_spec : forall l l', eqb l l' = true <-> l = l'. + Proof eqb_spec. + + Lemma neg_involutive : forall l, neg (neg l) = l. + Proof. + unfold neg;intros; rewrite <- lxor_assoc;change (1 lxor 1) with 0;rewrite lxor_0_r;trivial. + Qed. + + Lemma blit_neg : forall l, blit (neg l) = blit l. + Proof. + unfold blit, neg;intros l. + rewrite lxor_lsr, lxor_0_r;trivial. + Qed. + + Lemma lit_blit: forall l, + is_pos l = true -> lit (blit l) = l. + Proof. + unfold is_pos, lit, blit;intros. + rewrite (bit_xor_split l) at 2. + rewrite is_even_bit, negb_true_iff in H;rewrite H. + symmetry;apply lxor_0_r. + Qed. + + Lemma lit_blit_neg: forall l, + is_pos l = false -> lit (blit l) = neg l. + Proof. + unfold is_pos, lit, blit;intros. + rewrite (bit_xor_split l) at 2. + rewrite is_even_bit, negb_false_iff in H;rewrite H. + rewrite <- (neg_involutive ((l >> 1) << 1)) at 1;trivial. + Qed. + + Lemma nlit_blit: forall l, + is_pos l = false -> nlit (blit l) = l. + Proof. + unfold nlit;intros;rewrite lit_blit_neg;auto using neg_involutive. + Qed. + + Lemma nlit_blit_neg: forall l, + is_pos l = true -> nlit (blit l) = neg l. + Proof. + unfold nlit;intros;rewrite lit_blit;auto using neg_involutive. + Qed. + + Lemma is_pos_lit : forall l, + is_pos (lit l) = true. + Proof. + unfold is_pos, lit;apply is_even_lsl_1. + Qed. + + Lemma is_pos_neg : forall l, + is_pos (neg l) = negb (is_pos l). + Proof. + unfold neg, is_pos;intros l. + rewrite is_even_xor, xorb_false_r;trivial. + Qed. + + Lemma is_pos_nlit : forall l, + is_pos (nlit l) = false. + Proof. + unfold nlit;intros l;rewrite is_pos_neg, is_pos_lit;trivial. + Qed. + + Lemma is_pos_true : is_pos _true. + Proof. reflexivity. Qed. + + Lemma is_pos_false : is_pos _false. + Proof. reflexivity. Qed. + + Lemma blit_pos :forall a b, + Lit.blit a = Lit.blit b -> Lit.is_pos a = Lit.is_pos b -> + a = b. + Proof lsr_is_even_eq. + + Lemma blit_lit : forall l, blit (lit (blit l)) = blit l. + Proof. + intros l;case_eq (is_pos l);intros. + rewrite lit_blit;trivial. + rewrite lit_blit_neg, blit_neg;trivial. + Qed. + + Lemma blit_nlit : forall l, blit (nlit (blit l)) = blit l. + Proof. + intros l;case_eq (is_pos l);intros. + rewrite nlit_blit_neg, blit_neg;trivial. + rewrite nlit_blit;trivial. + Qed. + + Lemma blit_true : blit _true = Var._true. + Proof. reflexivity. Qed. + + Lemma blit_false : blit _false = Var._false. + Proof. reflexivity. Qed. + + (* Interpretation of a literal *) + Definition interp rho (l:_lit) := + if is_pos l then Var.interp rho (blit l) + else negb (Var.interp rho (blit l)). + + Lemma interp_true : forall rho, Valuation.wf rho -> interp rho _true. + Proof. + intros rho Hwf;unfold interp;rewrite is_pos_true, blit_true. + apply Var.interp_true;trivial. + Qed. + + Lemma interp_false : forall rho, Valuation.wf rho -> ~interp rho _false. + Proof. + intros rho Hwf;unfold interp;rewrite is_pos_false, blit_false. + apply Var.interp_false;trivial. + Qed. + + Lemma interp_neg : forall rho l, interp rho (neg l) = negb (interp rho l). + Proof. + intros rho l;unfold interp;rewrite is_pos_neg, blit_neg. + destruct (is_pos l);simpl;auto using negb_involutive. + Qed. + + Lemma interp_lit : forall rho l, interp rho (lit (blit l)) = Var.interp rho (blit l). + Proof. + intros;unfold interp;rewrite is_pos_lit, blit_lit;trivial. + Qed. + + Lemma interp_nlit : forall rho l, interp rho (nlit (blit l)) = negb (Var.interp rho (blit l)). + Proof. + unfold nlit;intros rho l;rewrite interp_neg, interp_lit;trivial. + Qed. + + Lemma interp_eq_compat : forall rho1 rho2 l, + rho1 (blit l) = rho2 (blit l) -> + interp rho1 l = interp rho2 l. + Proof. + unfold interp, Var.interp;intros rho1 rho2 l Heq;rewrite Heq;trivial. + Qed. + + Lemma lxor_neg : forall l1 l2, (l1 lxor l2 == 1) = true -> l1 = Lit.neg l2. + Proof. + unfold Lit.neg; intros l1 l2;rewrite eqb_spec;intros Heq;rewrite <- Heq. + rewrite lxor_comm, <- lxor_assoc, lxor_nilpotent, lxor_0_r;trivial. + Qed. + +End Lit. + + +Lemma compare_spec' : forall x y, + match x ?= y with + | Lt => x < y + | Eq => x = y + | Gt => y < x + end. +Proof. + intros x y;rewrite compare_def_spec;unfold compare_def. + case_eq (x < y);intros;[reflexivity | ]. + case_eq (x == y);intros. + rewrite <- eqb_spec;trivial. + rewrite <- not_true_iff_false in H, H0. + unfold is_true in *;rewrite ltb_spec in H |- *;rewrite eqb_spec in H0. + assert ([|x|] <> [|y|]) by (intros Heq;apply H0, to_Z_inj;trivial);omega. +Qed. + + +Module C. + + Definition t := list _lit. + + Definition interp (rho:Valuation.t) (l:t) := + List.existsb (Lit.interp rho) l. + + Definition valid rho c := + interp rho c = true. + + Definition _true : t := Lit._true :: nil. + + Definition is_false (c:t) := + match c with + | nil => true + | _ => false + end. + + Section OR. + + Variable or : t -> t -> t. + Variable l1 : _lit. + Variable c1 : t. + + Fixpoint or_aux (c2:t) := + match c2 with + | nil => l1 :: c1 + | l2::c2' => + match l1 ?= l2 with + | Eq => l1 :: or c1 c2' + | Lt => l1 :: or c1 c2 + | Gt => l2 :: or_aux c2' + end + end. + + Variable rho : Valuation.t. + Hypothesis or_correct : forall c2, + interp rho (or c1 c2) = interp rho c1 || interp rho c2. + + Lemma or_aux_correct : forall c2, + interp rho (or_aux c2) = interp rho (l1::c1) || interp rho c2. + Proof. + induction c2;simpl. + rewrite orb_false_r;trivial. + generalize (compare_spec' l1 a);destruct (l1 ?= a);intros H;simpl. + rewrite H;destruct (Lit.interp rho a);trivial. + rewrite !orb_false_l, or_correct;trivial. + rewrite or_correct;simpl;rewrite orb_assoc;trivial. + rewrite IHc2;simpl. + destruct (Lit.interp rho a);simpl;trivial. + rewrite orb_true_r;trivial. + Qed. + + End OR. + + Fixpoint or (c1 c2:t) {struct c1} : t := + match c1, c2 with + | nil, _ => c2 + | _, nil => c1 + | l1::c1, l2::c2' => + match compare l1 l2 with + | Eq => l1 :: or c1 c2' + | Lt => l1 :: or c1 c2 + | Gt => l2 :: or_aux or l1 c1 c2' + end + end. + + Lemma or_correct : forall rho c1 c2, + interp rho (or c1 c2) = interp rho c1 || interp rho c2. + Proof. + induction c1;simpl;trivial. + destruct c2;simpl. + rewrite orb_false_r;trivial. + generalize (compare_spec' a i);destruct (a ?= i);intros H;simpl. + rewrite H, IHc1;simpl;destruct (Lit.interp rho i);simpl;trivial. + rewrite IHc1, orb_assoc;trivial. + rewrite or_aux_correct;simpl;trivial. + destruct (Lit.interp rho i);trivial. + simpl;rewrite !orb_true_r;trivial. + Qed. + + Section RESOLVE. + + Variable resolve : t -> t -> t. + Variable l1 : _lit. + Variable c1 : t. + + Fixpoint resolve_aux (c2:t) : t := + match c2 with + | nil => _true + | l2::c2' => + match compare l1 l2 with + | Eq => l1 :: resolve c1 c2' + | Lt => if l1 lxor l2 == 1 then or c1 c2' else l1 :: resolve c1 c2 + | Gt => + if l1 lxor l2 == 1 then or c1 c2' else l2 :: resolve_aux c2' + end + end. + + Lemma resolve_aux_correct : forall rho, + (forall c2, interp rho c1 -> interp rho c2 -> interp rho (resolve c1 c2)) -> + interp rho (l1 :: c1) -> + forall c2, interp rho c2 -> + interp rho (resolve_aux c2). + Proof. + intros rho resolve_correct Hc1;simpl in Hc1. + induction c2;simpl;try discriminate. + generalize (compare_spec' l1 a);destruct (l1 ?= a);intros;subst;simpl. + simpl in Hc1;destruct (Lit.interp rho a);simpl in *;auto. + generalize (Lit.lxor_neg l1 a);destruct (l1 lxor a == 1);intros. + rewrite or_correct. + rewrite H1, Lit.interp_neg in Hc1;trivial;destruct (Lit.interp rho a). + simpl in Hc1;rewrite Hc1;trivial. + simpl in H0;rewrite H0, orb_true_r;trivial. + simpl;destruct (Lit.interp rho l1);simpl;auto. + generalize (Lit.lxor_neg l1 a);destruct (l1 lxor a == 1);intros. + rewrite or_correct. + rewrite H1, Lit.interp_neg in Hc1;trivial;destruct (Lit.interp rho a). + simpl in Hc1;rewrite Hc1;trivial. + simpl in H0;rewrite H0, orb_true_r;trivial. + simpl;destruct (Lit.interp rho a);simpl;auto. + Qed. + + End RESOLVE. + + Fixpoint resolve (c1 c2:t) {struct c1} : t := + match c1, c2 with + | nil, _ => _true + | _, nil => _true + | l1::c1, l2::c2' => + match compare l1 l2 with + | Eq => l1 :: resolve c1 c2' + | Lt => if l1 lxor l2 == 1 then or c1 c2' else l1 :: resolve c1 c2 + | Gt => + if l1 lxor l2 == 1 then or c1 c2' else l2 :: resolve_aux resolve l1 c1 c2' + end + end. + + Lemma resolve_correct : forall rho c1 c2, + interp rho c1 -> interp rho c2 -> + interp rho (resolve c1 c2). + Proof. + induction c1;simpl;try discriminate. + destruct c2;simpl;try discriminate. + intros Hc1 Hc2. + generalize (compare_spec' a i);destruct (a ?= i);intros;subst;simpl. + destruct (Lit.interp rho i);simpl in *;auto. + generalize (Lit.lxor_neg a i);destruct (a lxor i == 1);intros. + rewrite or_correct. + rewrite H0, Lit.interp_neg in Hc1;trivial;destruct (Lit.interp rho i). + simpl in Hc1;rewrite Hc1;trivial. + simpl in Hc2;rewrite Hc2, orb_true_r;trivial. + simpl;destruct (Lit.interp rho a);simpl;auto. + generalize (Lit.lxor_neg a i);destruct (a lxor i == 1);intros. + rewrite or_correct. + rewrite H0, Lit.interp_neg in Hc1;trivial;destruct (Lit.interp rho i). + simpl in Hc1;rewrite Hc1;trivial. + simpl in Hc2;rewrite Hc2, orb_true_r;trivial. + simpl;destruct (Lit.interp rho i);simpl;auto using resolve_aux_correct. + Qed. + + Lemma interp_true : forall rho, Valuation.wf rho -> interp rho _true = true. + Proof. + unfold _true, interp;intros rho Hwf;simpl. + rewrite Lit.interp_true;trivial. + Qed. + + Lemma is_false_correct : + forall c, is_false c = true -> + forall rho, ~valid rho c. + Proof. + unfold valid, interp;destruct c;simpl; auto;discriminate. + Qed. + +End C. + + +Notation clause_id := int (only parsing). + +Notation resolution := (array clause_id) (only parsing). + +Module S. + + Definition t := array C.t. + + Definition get (s:t) (cid:clause_id) := s.[cid]. + Register get as PrimInline. + + (* Do not use this function outside this module *) + (* expect if you are sure that [c = sort_uniq c] *) + Definition internal_set (s:t) (cid:clause_id) (c:C.t) : t := s.[cid <- c]. + Register internal_set as PrimInline. + + Definition make (nclauses : int) : t := + PArray.make nclauses C._true. + + Definition valid rho s := + forall id, C.valid rho (get s id). + + + (* Specification of make *) + + Lemma valid_make : forall rho nclauses, + Valuation.wf rho -> + valid rho (make nclauses). + Proof. + unfold valid, make, get;intros. + rewrite PArray.get_make; apply C.interp_true;trivial. + Qed. + + + (* Specification of get *) + + Lemma valid_get : forall rho s, valid rho s -> + forall id, C.valid rho (get s id). + Proof. auto. Qed. + + + (* Specification of internal_set *) + + Lemma valid_internal_set : + forall rho s, valid rho s -> + forall c, C.valid rho c -> + forall id, valid rho (set s id c). + Proof. + unfold valid, get, set;simpl;intros. + destruct (Int63Properties.reflect_eqb id id0);subst. + case_eq (id0 < length s);intros. + rewrite PArray.get_set_same;trivial. + rewrite PArray.get_outofbound. + rewrite PArray.default_set. + rewrite <- (PArray.get_outofbound _ _ (length s)); trivial. + rewrite <- not_true_iff_false, ltb_spec;auto with zarith. + rewrite PArray.length_set;trivial. + rewrite get_set_other;trivial. + Qed. + + (* Building clause *) + (* Same as set but without precondition *) + + (* TODO: It can be a good idea to change the insertion sort algorithm *) + + Fixpoint insert l1 c := + match c with + | nil => l1:: nil + | l2 :: c' => + match l1 ?= l2 with + | Lt => if l1 lxor l2 == 1 then C._true else l1 :: c + | Eq => c + | Gt => if l1 lxor l2 == 1 then C._true else l2 :: insert l1 c' + end + end. + + Fixpoint sort_uniq c := + match c with + | nil => nil + | l1 :: c => insert l1 (sort_uniq c) + end. + + Lemma insert_correct : forall rho (Hwf:Valuation.wf rho) l1 c, + C.interp rho (insert l1 c) = C.interp rho (l1 :: c). + Proof. + intros rho Hwf l1;induction c;simpl;trivial. + generalize (compare_spec' l1 a);destruct (l1 ?= a);intros;subst;simpl. + destruct (Lit.interp rho a);simpl in *;auto. + generalize (Lit.lxor_neg l1 a);destruct (l1 lxor a == 1);intros;trivial. + rewrite C.interp_true;trivial. + rewrite H0, Lit.interp_neg;trivial;destruct (Lit.interp rho a);trivial. + generalize (Lit.lxor_neg l1 a);destruct (l1 lxor a == 1);intros. + rewrite C.interp_true;trivial. + rewrite H0, Lit.interp_neg;trivial;destruct (Lit.interp rho a);trivial. + simpl;rewrite orb_assoc,(orb_comm (Lit.interp rho l1)),<-orb_assoc,IHc;trivial. + Qed. + + Lemma sort_uniq_correct : forall rho (Hwf:Valuation.wf rho) c, + C.interp rho (sort_uniq c) = C.interp rho c. + Proof. + intros rho Hwf;induction c;simpl;trivial. + rewrite insert_correct;trivial;simpl;rewrite IHc;trivial. + Qed. + + Definition set_clause (s:t) pos (c:C.t) : t := + set s pos (sort_uniq c). + + Lemma valid_set_clause : + forall rho s, Valuation.wf rho -> valid rho s -> forall pos c, + C.valid rho c -> valid rho (set_clause s pos c). + Proof. + unfold valid, get, set_clause. intros rho s Hrho Hs pos c Hc id. + destruct (Int63Properties.reflect_eqb pos id);subst. + case_eq (id < length s); intro H. + unfold get;rewrite PArray.get_set_same; trivial. + unfold C.valid;rewrite sort_uniq_correct;trivial. + generalize (Hs id);rewrite !PArray.get_outofbound, PArray.default_set;trivial. + rewrite length_set;trivial. + rewrite get_set_other;trivial. + Qed. + + + (* Resolution *) + + Definition set_resolve (s:t) pos (r:resolution) : t := + let len := PArray.length r in + if len == 0 then s + else + let c := foldi (fun i c => C.resolve (get s (r.[i])) c) 1 (len - 1) + (get s (r.[0])) in + internal_set s pos c. + + Lemma valid_set_resolve : + forall rho s, Valuation.wf rho -> valid rho s -> + forall pos r, valid rho (set_resolve s pos r). + Proof. + unfold set_resolve; intros rho s Hrho Hv pos r. + destruct (Int63Properties.reflect_eqb (length r) 0);[trivial | ]. + apply valid_internal_set;trivial. + apply foldi_ind;auto. + intros i c _ _ Hc;apply C.resolve_correct;auto;apply Hv. + Qed. + +End S. |