proposition: Lemma valid_check_spl_arith : forall orig, C.valid rho orig -> forall res l, C.valid rho (check_spl_arith orig res l).
proof: Proof. unfold check_spl_arith; intros [ |li [ |t q]]. intros; apply C.interp_true; auto. intros H res l; case_eq (build_clause Lia.empty_vmap (Lit.neg li :: res :: nil)); [ |intros; apply C.interp_true; auto]. intros (vm1, bf) Heq; destruct (Lia.build_clause_correct _ _ _ t_func ch_atom ch_form wt_t_atom _ _ _ _ Heq) as [H1 H0]. red; simpl; auto with smtcoq_core. decompose [and] H0; case_eq (ZTautoChecker bf l); [intros Heq3|intros; apply C.interp_true; auto]. unfold C.valid; replace (C.interp rho (res :: nil)) with (C.interp rho (Lit.neg li :: res :: nil)). rewrite H6; apply ZTautoChecker_sound with l;trivial. simpl; replace (Lit.interp rho (Lit.neg li)) with false; auto. rewrite Lit.interp_neg; unfold C.valid in H; simpl in H; rewrite orb_false_r in H; rewrite H; auto. intros; apply C.interp_true; auto. Qed.
imports: List PArray Bool Int63 ZMicromega Misc State SMT_terms