proposition: Theorem clauses_update_sat: forall l c cs s, ordered_clause c -> lit_sat l s -> ordered cs -> sat (clauses_update l c cs) s -> sat cs s.
proof: Proof. intros l c cs s H1 H2 H3; generalize H3; elim cs; simpl; auto; clear H3. intros (n1, c1) cs1 Rec H3. assert (F1: ordered_clause c1). apply (H3 n1); auto with datatypes. generalize (lit_is_in_correct l c1 F1). case (lit_is_in l c1); auto; intros H4 H5. intros n2 c2; simpl; intros [Hn2 | Hn2]. injection Hn2; intros; subst; clear Hn2. exists l; split; auto. assert (F2: sat cs1 s). apply Rec; auto. intros n3 c3 Hn3; apply (H3 n3); auto with datatypes. apply (F2 n2); auto. match type of H5 with sat (clause_insert ?X ?Y) ?Z => case (clause_insert_sat X Y Z); intros tmp _; generalize (tmp H5); clear tmp H5; intros ((l1,(H6, H7)),H8) end. assert (F2: sat cs1 s). apply Rec; auto. intros n3 c3 Hn3; apply (H3 n3); auto with datatypes. intros n2 c2; simpl; intros [Hn2 | Hn2]. injection Hn2; intros; subst; clear Hn2. exists l1; split; auto. case (lit_rm_in l1 c c2); intuition. apply (F2 n2); auto with datatypes. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia