proposition: Lemma NoDup_incl_ordered_powerlist: forall (l: list E), NoDup l -> exists L, (forall l', (NoDup l' /\ incl l' l /\ (forall x y, In x l' -> In y l' -> (find l' x 0 <= find l' y 0 <-> find l x 0 <= find l y 0))) <-> In l' L).
proof: Proof. induction l; intros. exists (nil::nil). intros; split; intros. destruct H0 as [? [? ?]]. destruct l'. left; auto. assert (In e (e::l')). left; auto. apply H1 in H3; contradiction. destruct H0. subst l'. split. apply NoDup_nil. split. unfold incl; intros; auto. intros. simpl. lia. contradiction. assert (~ In a l). apply NoDup_cons_2 in H; auto. apply NoDup_cons_1 in H. destruct (IHl H) as [L ?]. clear IHl. assert (forall l', In l' L -> ~ In a l'). intros. apply H1 in H2. destruct H2 as [? [? ?]]. unfold not; intros. apply H3 in H5. contradiction. exists (L ++ map (fun l' => (a::l')) L). intros; split; intros. ** destruct H3 as [? [? ?]]. apply in_or_app. destruct (in_dec E_EqDec a l'). **** right. destruct l'. contradiction. destruct (E_EqDec e a). ****** hnf in e0. subst e. apply in_map. apply H1. split. apply NoDup_cons_1 in H3; auto. split. unfold incl; intros. assert (In a0 (a::l)). apply H4. right; auto. destruct H7. subst a0. apply NoDup_cons_2 in H3. contradiction. auto. intros. assert (find (a :: l') x 0 <= find (a :: l') y 0 <-> find (a :: l) x 0 <= find (a :: l) y 0). apply H5. right; auto. right; auto. apply NoDup_cons_2 in H3. simpl in H8. destruct (E_EqDec a x). hnf in e. subst x. contradiction. destruct (E_EqDec a y). hnf in e. subst y. contradiction. replace 1 with (1+0) in H8 by lia. repeat rewrite find_accum_add1 in H8. split; intros. lia. lia. ****** unfold complement, equiv in c. assert (find (e :: l') e 0 <= find (e :: l') a 0 <-> find (a :: l) e 0 <= find (a :: l) a 0). apply H5. left; auto. auto. simpl in H6. destruct (E_EqDec e e). 2: { unfold complement, equiv in c0; contradiction. } destruct (E_EqDec a a). 2: { unfold complement, equiv in c0; contradiction. } clear e0 e1. destruct (E_EqDec e a). hnf in e0; contradiction. destruct (E_EqDec a e). hnf in e0; symmetry in e0; contradiction. clear c0 c1. assert (0 <= find l' a 1). { apply (Z.le_trans 0 1). lia. apply find_lbound. } apply H6 in H7. assert (1 <= 0). { apply (Z.le_trans 1 (find l e 1)). apply find_lbound. auto. } lia. **** left. apply H1. split. auto. split. unfold incl; intros. assert (In a0 (a::l)). apply H4; auto. destruct H7. subst a0. contradiction. auto. intros. assert (find l' x 0 <= find l' y 0 <-> find (a :: l) x 0 <= find (a :: l) y 0). apply H5; auto. simpl in H8. destruct (E_EqDec a x). hnf in e. subst x. contradiction. destruct (E_EqDec a y). hnf in e. subst y. contradiction. replace 1 with (1+0) in H8 by lia. do 2 rewrite find_accum_add1 in H8. split; intros. apply H8 in H9. lia. apply H8. lia. ** apply in_app_or in H3. destruct H3. **** apply H1 in H3. destruct H3 as [? [? ?]]. split. auto. split. unfold incl; intros. right. apply H4. auto. intros. assert (find l' x 0 <= find l' y 0 <-> find l x 0 <= find l y 0). apply H5; auto. simpl. destruct (E_EqDec a x). hnf in e; subst x. apply H4 in H6; contradiction. destruct (E_EqDec a y). hnf in e; subst y. apply H4 in H7; contradiction. replace 1 with (1+0) by lia. do 2 rewrite (find_accum_add1). split; intros. apply H8 in H9. lia. lia. **** apply list_in_map_inv in H3. destruct H3 as [lx [? ?]]. subst l'. rename lx into l'. assert (~ In a l'). apply H2; auto. apply H1 in H4. destruct H4 as [? [? ?]]. split. apply NoDup_cons; auto. split. unfold incl; intros. destruct H7. subst a0. left; auto. right. apply H5. auto. intros. destruct H7. subst x. simpl. destruct (E_EqDec a a). 2: { unfold complement, equiv in c; contradiction. } destruct (E_EqDec a y). lia. split; intros. apply (Z.le_trans 0 1). lia. apply find_lbound. apply (Z.le_trans 0 1). lia. apply find_lbound. destruct H8. subst y. simpl. destruct (E_EqDec a a). 2: { unfold complement, equiv in c; contradiction. } destruct (E_EqDec a x). lia. split; intros. assert (1 <= 0). apply (Z.le_trans 1 (find l' x 1)). apply find_lbound. lia. lia. assert (1 <= 0). apply (Z.le_trans 1 (find l x 1)). apply find_lbound. lia. lia. assert (find l' x 0 <= find l' y 0 <-> find l x 0 <= find l y 0). apply H6; auto. simpl. destruct (E_EqDec a x). hnf in e; subst x; contradiction. destruct (E_EqDec a y). hnf in e; subst y; contradiction. replace 1 with (1+0) by lia. repeat rewrite find_accum_add1. split; intros; lia. Qed.
imports: VST.floyd.proofauto Coq.Classes.Equivalence CertiGraph.lib.List_ext