proposition: Lemma check_weaken_valid : forall rho s (cid:clause_id) (cl:list _lit), Valuation.wf rho -> valid rho s -> C.valid rho (check_weaken s cid cl).
proof: Proof. intros rho s cid cl Hw Hs. unfold check_weaken, C.valid. case_eq (subclause (get s cid) cl); try (intros; now apply C.interp_true). specialize (Hs cid). unfold C.valid, C.interp in Hs. apply existsb_exists in Hs. intro. unfold subclause in H. rewrite forallb_forall in H. unfold C.valid, C.interp. apply existsb_exists. destruct Hs as (x, (Hi, Hax)). specialize (H x Hi). rewrite !orb_true_iff in H. rewrite !eqb_spec in H. destruct H as [[H | H] | H]. - contradict Hax. subst. apply Lit.interp_false; trivial. - contradict Hax. subst. rewrite Lit.interp_neg. rewrite not_true_iff_false, negb_false_iff, Lit.interp_true; trivial. - apply existsb_exists in H. destruct H as (x', (Hcl, Hxx')). rewrite eqb_spec in Hxx'. subst x'. exists x. auto. Qed.
imports: List Bool Int63 Psatz Ring63 PArray Misc Ring