proposition: Lemma wf_collect_all_wneg : forall hm w (WF : wf_map w) (WFU : wf_units_def w hm), Forall (has_literal hm) (collect_all_wneg hm w).
proof: Proof. unfold collect_all_wneg. intros. set (Q := fun (r:list literal) => Forall (has_literal hm) r). rewrite PTrie.fold_elements'. unfold wf_units_def in WFU. assert (forall i v, In (i,v) (PTrie.elements' w nil) -> forall b a, IntMap.get' i hm = Some (b,LAT a) -> has_form hm (HCons.mk i b (LAT a))). { intros. apply PTrie.in_elements' with (opt:=None) in H. simpl in H. destruct H ; [|tauto]. assert (PTrie.get' i w <> None) by congruence. apply WFU in H1. destruct H1 as (f1 & HF & ID). inv HF; simpl in * ; try congruence. rewrite H0 in H1. inv H1. constructor; auto. auto. } assert (QACC : Q nil). { unfold Q. simpl. constructor. } revert QACC. generalize (nil: list literal). induction (PTrie.elements' w nil). - simpl. auto. - intros. simpl in *. eapply IHl ; eauto. unfold Q. unfold get_wneg. destruct (get_atom hm (fst a)) eqn:GA ; auto. assert (has_form hm t0). { unfold get_atom in GA. destruct (IntMap.get' (fst a) hm) eqn:EQ ; try congruence. destruct p. destruct l1 ; try congruence. inv GA. destruct a ; simpl in *. eapply H ; eauto. } constructor ; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause