proposition: Theorem invariant_clauses_update: forall n p z c cs s, invariant ((n, L p z :: c) :: 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 datatypes. intros n p z c cs s (V1, (V2, (V3, V4))). assert (H: valid_lit (L p z) s)... apply (V2 n (L p z :: c))... split... apply clauses_update_ordered... apply anti_literals_ordered... intros n2 c2 Hn2; apply (V1 n2 c2)... split... apply clauses_update_valid... intros n2 c2 Hn2; apply (V1 n2 c2)... apply anti_literals_ordered... intros; apply anti_literals_in... intros n2 c2 Hn2; apply (V2 n2)... 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 H; intuition. rewrite update_get... case H; intuition. apply valid_pos2n... case H; intuition. rewrite update_get... apply valid_pos2n... case H; intuition. split; intros Hs2. apply clauses_update_sat_rev... apply anti_literals_ordered... intros n2 c2 Hn2; apply (V1 n2)... intros l Hl Hl1. case (anti_literals_sat p z s1)... case H; intros _ (tmp, _)... exists l... case (V4 s1)... apply refine_trans with (2 := Hs1)... apply refine_update... case H; intuition. intros tmp _; generalize (tmp Hs2); intros HH; clear tmp. intros n2 c2 Hn2; apply (HH n2)... case (V4 s1)... apply refine_trans with (2 := Hs1)... apply refine_update... case H; intuition. intros _ tmp; apply tmp; auto; clear tmp. assert (Heq: sat cs s1). apply clauses_update_sat with (4 := Hs2)... apply anti_literals_ordered... intros n2 c2 Hn2; apply (V1 n2)... intros n2 c2; simpl; intros [Hn2 | Hn2]. injection Hn2; intros; subst. exists (L p (get p s1)); split... simpl... apply (Heq n2 c2)... Qed.
imports: List UList Permutation Div OrderedList ListOp Lia