proposition: Lemma eval_shorten_clauses : forall diff l st (CA : check_annot has_literal (hconsmap st) diff) (ED : Annot.lift eval_literal diff) (WFL: WMap.wf_watch_map l) (ALL1: WMap.Forall_watch_map (Annot.lift eval_watched_clause) l) (ALL2: WMap.Forall_watch_map (check_annot has_watched_clause (hconsmap st)) l) (WF: wf_state st /\ eval_state st), wf_result_state (shorten_clauses diff l st) /\ eval_result_state (shorten_clauses diff l st).
proof: Proof. unfold shorten_clauses. intros. set (Q := fun x => wf_result_state x /\ eval_result_state x /\ check_annot has_literal (hconsmap_result x) diff). assert ((Q (WMap.fold_watch_map (fun (acc : dresult) (i : int) (k : Annot.t watched_clause) => update_watched_clause diff i k acc) l (Progress st)))). eapply fold_lemma with (P:= fun (o: dresult) cl => match o with Success _ => True | Fail _ => False | Progress st => Annot.lift eval_watched_clause cl /\ check_annot has_watched_clause (hconsmap st) cl end);auto. - apply WMap.Forall_watch_map_ForallAnd;auto. - destruct acc ; simpl ; auto. intros. destruct_in_goal EQ; auto. + eapply not_fail_insert_watched_clause. rewrite EQ. simpl. auto. + assert (OM : (hconsmap st1) = (hconsmap st0)). { change (hconsmap_result (Progress st1) = hconsmap st0). rewrite <- EQ. eapply hconsmap_comp. apply hconsmap_remove_watched_clause. apply hconsmap_insert_watched_clause; auto. apply not_fail_insert_watched_clause. } intuition. congruence. - destruct acc ; simpl ; auto. intros. destruct H. destruct H1 as (WFA & WFE & WFH). destruct H2 as (ER & CA'). generalize (wf_remove_watched_clause (fst a) (Annot.elt (snd a)) st0 H WFH). intro. unfold Q. split_and. + apply wf_insert_normalised_clause;auto. { rewrite hconsmap_remove_watched_clause. rewrite units_remove_watched_clause. apply check_annot_normalise_watched_clause; auto. destruct H;auto. simpl in H. destruct H ; auto. simpl;auto. destruct CA';auto. } + apply eval_insert_watched_clause; auto. rewrite hconsmap_remove_watched_clause. simpl in CA'. simpl ; auto. destruct CA';auto. simpl. apply eval_remove_watched_clause;auto. + rewrite hconsmap_insert_watched_clause. rewrite hconsmap_remove_watched_clause. auto. apply not_fail_insert_watched_clause. - unfold Q;tauto. - unfold Q in H. tauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause