proposition: Lemma wf_extract_thy_pb : forall hm u l1 l2 (WF : wf_map u) (WFU : wf_units_def u hm ), extract_theory_problem hm u = (l1,l2) -> Forall (has_literal hm) l1 /\ Forall (has_literal hm) l2.
proof: Proof. unfold extract_theory_problem. intros. change l1 with (fst (l1,l2)). rewrite <- H. change l2 with (snd (l1,l2)). rewrite <- H. clear H. set (Q := fun (r:list literal * list literal) => Forall (has_literal hm) (fst r) /\ Forall (has_literal hm) (snd r)). change (Q (IntMap.fold' (collect_literal hm) u (nil, nil))). rewrite PTrie.fold_elements'. unfold wf_units_def in WFU. assert (forall i v, In (i,v) (PTrie.elements' u 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 u <> 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,nil)). { unfold Q. simpl. split ; constructor. } revert QACC. generalize ((nil,nil): list literal * list literal). induction (PTrie.elements' u nil). - simpl. auto. - intros. simpl in *. eapply IHl ; eauto. unfold Q. unfold collect_literal. 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 p0. destruct l0 ; try congruence. inv GA. destruct a ; simpl in *. eapply H ; eauto. } destruct p ; simpl. destruct QACC. simpl in *. destruct (Annot.elt (snd a)) ; split ; simpl ; try constructor ; simpl; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause