proposition: Theorem invariant_clauses_update1: forall p z cs s, valid_lit (L p z) s -> invariant cs s -> invariant (clauses_update (L p z) (anti_literals (L p z)) cs) (update p z s).
proof: Proof. Proof with auto with arith. intros p z cs s V0 (V1, (V2, (V3, V4))). split... apply clauses_update_ordered... apply anti_literals_ordered... split... apply clauses_update_valid... apply anti_literals_ordered... intros; apply anti_literals_in... split... rewrite length_update... intros s1 Hs1. assert (Heq1: get p s1 = z). case Hs1; intros _ (_, tmp); case (tmp p); auto with arith; clear tmp. case V0; intuition. rewrite update_get... case V0; intuition. apply valid_pos2n... case V0; intuition. rewrite update_get... apply valid_pos2n... case V0; intuition. split; intros Hs2. apply clauses_update_sat_rev... apply anti_literals_ordered... intros l Hl Hl1. case (anti_literals_sat p z s1)... case V0; intros _ (tmp, _)... exists l... case (V4 s1)... apply refine_trans with (2 := Hs1)... apply refine_update... case V0; intuition. case (V4 s1)... apply refine_trans with (2 := Hs1)... apply refine_update... case V0; intuition. intros _ tmp; apply tmp; auto; clear tmp. apply clauses_update_sat with (4 := Hs2)... apply anti_literals_ordered... Qed.
imports: List UList Permutation Div OrderedList ListOp Lia