proposition: Lemma eval_annot_shorten_clauses : forall diff l st (CD : check_annot has_literal (hconsmap st) diff) (ED : eval_annot eval_literal (hconsmap st) diff) (WFL: WMap.wf_watch_map l) (ALL1: WMap.Forall_watch_map (eval_annot eval_watched_clause (hconsmap st)) l) (ALL2: WMap.Forall_watch_map (check_annot has_watched_clause (hconsmap st)) l) (WF: wf_state st /\ eval_annot_state st), wf_result_state (shorten_clauses diff l st) /\ eval_annot_result_state (shorten_clauses diff l st).
proof: Proof. unfold shorten_clauses. intros. set (Q := fun x => wf_result_state x /\ eval_annot_result_state x /\ check_annot has_literal (hconsmap_result x) diff /\ eval_annot eval_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 => eval_annot eval_watched_clause (hconsmap st) 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. } destruct H as (EA & CA). destruct H0 as (EA' & CA'). rewrite OM in *. tauto. - destruct acc ; simpl ; auto. intros. destruct H as (HH1 & HH2 & HH3 & HH4). destruct H1 as (WFA & WFE & WFH). generalize (wf_remove_watched_clause (fst a) (Annot.elt (snd a)) st0 HH1 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. simpl in H; destruct H;auto. simpl in *. destruct HH3;auto. } { apply eval_annot_insert_watched_clause; auto. rewrite hconsmap_remove_watched_clause. split ; auto. apply eval_annot_remove_watched_clause;auto. } { rewrite hconsmap_insert_watched_clause. rewrite hconsmap_remove_watched_clause. auto. apply not_fail_insert_watched_clause. } { 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