proposition: Lemma shorten_clause_correct : forall m l u cl an (EV : eval_units m u) (EVL : Annot.lift eval_literal l) (HASL : has_literal m (Annot.elt l)) (WFC : has_watched_clause m cl) (EC : eval_watched_clause cl), Annot.lift eval_clause (shorten_clause l u an cl).
proof: Proof. unfold shorten_clause;intros. assert (HW1 : has_literal m (watch1 cl)). { inv WFC. auto. } assert (HW2 : has_literal m (watch2 cl)). { inv WFC. inv H2; auto. } assert (HUW : Forall (has_literal m) (unwatched cl)). { inv WFC. inv H2; auto. } destruct_in_goal OPP. - unfold eval_watched_clause in EC. simpl in EC. apply eval_neg_literal_rec in EC; auto. apply eval_reduce with (m:=m); auto. eapply eval_opp_literal in OPP; eauto. - destruct_in_goal OPP1. unfold eval_watched_clause in EC. simpl in EC. apply eval_literal_rec_swap in EC; auto. apply eval_reduce with (m:=m); auto. eapply eval_opp_literal in OPP1; eauto. exact I. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause