Cardinal.v 27.9 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below    *)
Require Import BuiltIn.
Require BuiltIn.
Require HighOrd.
Require int.Int.
Require set.Set.
Require map.Map.
Require map.Const.

(* Why3 goal *)
Definition is_finite {a:Type} {a_WT:WhyType a} :
  (a -> Init.Datatypes.bool) -> Prop.
Proof.
intros f.
(* Weak Finite Sets seems difficult to use here because they are defined as a
   functor which takes the type as argument. For the type a here, we would need
   to define the module during proof (or inside section) which is not possible.
   When it becomes possible, it would be much better to use Weak Finite Sets.
*)
(* We take a list to represent sets because it is simple and convenient. 
   This is naive though and could easily be improved. The list is supposed to have
   no duplication (for cardinal). *)
exact (exists l: List.list a, List.NoDup l /\ forall e, List.In e l <-> f e = true). 
Defined.

(* Why3 goal *)
Lemma is_finite_empty {a:Type} {a_WT:WhyType a} :
  forall (s:a -> Init.Datatypes.bool), set.Set.is_empty s -> is_finite s.
Proof.
intros s h1.
exists List.nil.
split. constructor.
split; intros Hemp.
+ destruct Hemp.
+ destruct (h1 e Hemp).
Qed.

(* Why3 goal *)
Lemma is_finite_subset {a:Type} {a_WT:WhyType a} :
  forall (s1:a -> Init.Datatypes.bool) (s2:a -> Init.Datatypes.bool),
  is_finite s2 -> set.Set.subset s1 s2 -> is_finite s1.
Proof.
intros s1 s2 h1 h2.
destruct h1 as [l2 [Hdup h1]].
revert s1 s2 h1 h2.
(* The idea is to build the new list by induction. Two cases exists: the new element of s2 
   is in s1 too or not *)
induction l2; intros.
+ exists nil. 
  split; [|split].
  - constructor. 
  - eauto. 
  - intros. eapply h2 in H. eapply h1. assumption.
+ destruct (List.in_dec why_decidable_eq a0 l2).
  - eapply IHl2; eauto. { inversion Hdup; eauto. }
    split; intros.
    * destruct (why_decidable_eq a0 e). 
      ++ eapply h1. left. auto.
      ++ eapply h1; eauto. right. eauto.
    * destruct (h1 e). destruct H1; eauto. subst. assumption.
  - assert (Hdup2: List.NoDup l2). { inversion Hdup; eauto. } 
    destruct (Bool.bool_dec (s1 a0) true).
    * destruct (IHl2 Hdup2 (fun x => if why_decidable_eq x a0 then false else s1 x) 
                           (fun x => if why_decidable_eq x a0 then false else s2 x)).
      ++ intros. split; intros. destruct why_decidable_eq; eauto. subst. intuition.
         eapply h1. right. assumption.
         destruct why_decidable_eq; eauto. inversion H. eapply h1 in H. destruct H. destruct n0; auto. assumption.
      ++ intros x H1. unfold set.Set.mem in *. destruct why_decidable_eq. auto. eapply h2. apply H1.
      ++ exists (List.cons a0 x). split; [| split]; intros.
         -- destruct H. constructor; [| eauto]. intro Habs. eapply H0 in Habs.
            destruct why_decidable_eq. inversion Habs. auto.
         -- destruct H0; try subst; eauto. eapply H in H0. destruct why_decidable_eq; eauto.
            inversion H0.
         -- destruct H as [Hdup3 H]. specialize (H e0). destruct why_decidable_eq. left. auto. right. eapply H. assumption. 
    * destruct (IHl2 Hdup2 s1 (fun x => if why_decidable_eq x a0 then false else s2 x)).
      ++ split; intros. destruct why_decidable_eq. subst. intuition. eapply h1. right. assumption.
         destruct why_decidable_eq. inversion H. eapply h1 in H. destruct H; try subst; intuition.
      ++ intros e H. unfold set.Set.mem in *. destruct why_decidable_eq. subst.
         intuition.
         eapply h2. eapply H.
      ++ exists x. auto.
Qed.

(* Why3 goal *)
Lemma is_finite_add {a:Type} {a_WT:WhyType a} :
  forall (x:a) (s:a -> Init.Datatypes.bool), is_finite s ->
  is_finite (map.Map.set s x Init.Datatypes.true).
Proof.
intros x s h1.
destruct h1 as [l1 [Hdup h1]].
destruct (List.in_dec why_decidable_eq x l1).
- exists l1. split; eauto. intros. unfold Map.set. destruct why_decidable_eq. 
  subst. intuition. apply h1.
- exists (List.cons x l1). 
  split; [| split]; intros.
  + constructor; eauto.
  + destruct H. eapply Map.set_def; eauto.
    eapply h1 in H. unfold Map.set. destruct why_decidable_eq; eauto.
  + unfold Map.set in *. destruct why_decidable_eq. left. auto.
    right. eapply h1; eauto.
Qed.

(* Why3 goal *)
Lemma is_finite_add_rev {a:Type} {a_WT:WhyType a} :
  forall (x:a) (s:a -> Init.Datatypes.bool),
  is_finite (map.Map.set s x Init.Datatypes.true) -> is_finite s.
Proof.
intros x s h1.
eapply is_finite_subset; eauto.
intros e H. unfold Map.set, set.Set.mem in *. destruct why_decidable_eq; eauto. 
Qed.

(* Why3 goal *)
Lemma is_finite_singleton {a:Type} {a_WT:WhyType a} :
  forall (x:a),
  is_finite
  (map.Map.set
   (map.Const.const Init.Datatypes.false : a -> Init.Datatypes.bool) x
   Init.Datatypes.true).
Proof.
intros x.
exists (List.cons x List.nil).
unfold Map.set. 
split; [|split]; intros.
+ constructor. intro Habs. inversion Habs. constructor.
+ destruct why_decidable_eq; intuition.
  destruct H as [Hsubst | []]. subst. destruct n; reflexivity.
+ destruct why_decidable_eq; intuition.
  left. assumption.
  inversion H.
Qed.

(* Why3 goal *)
Lemma is_finite_remove {a:Type} {a_WT:WhyType a} :
  forall (x:a) (s:a -> Init.Datatypes.bool), is_finite s ->
  is_finite (map.Map.set s x Init.Datatypes.false).
Proof.
intros x s h1.
eapply is_finite_subset; eauto. 
eapply set.Set.subset_remove.
Qed.

(* Why3 goal *)
Lemma is_finite_remove_rev {a:Type} {a_WT:WhyType a} :
  forall (x:a) (s:a -> Init.Datatypes.bool),
  is_finite (map.Map.set s x Init.Datatypes.false) -> is_finite s.
Proof.
intros x s h1.
destruct h1 as [l1 [Hdup h1]].
destruct (Bool.bool_dec (s x) true) as [Heq | Heq].
+ exists (List.cons x l1).
  split.
  - constructor; auto. intro Habs. eapply h1 in Habs. unfold Map.set in Habs. 
    destruct why_decidable_eq; intuition.
  - unfold Map.set in h1. intros. specialize (h1 e). destruct why_decidable_eq; [| intuition]. subst.
    split; intuition. destruct H1; eauto.
+ exists l1.
  split; [auto|]. intros. specialize (h1 e). replace (Map.set s x false e) with (s e) in h1.
  eauto.
  unfold Map.set. destruct why_decidable_eq. subst. destruct (s e); intuition.
  reflexivity.
Qed.

(* Unnecessary lemma *)
Lemma NoDup_exists: forall {A} (eq_dec: forall x y: A, {x = y} + {x <> y}) P (Pdec: forall e, {P e} + {~ P e}) (l: List.list A), 
  exists l1, List.NoDup l1 /\ forall e, List.In e l1 <-> (List.In e l /\ P e).
Proof.
induction l.
- exists List.nil. split. constructor. intros. intuition. inversion H.
- destruct IHl. destruct H.
  destruct (List.in_dec eq_dec a l). 
  + exists x. split; eauto. intros. rewrite H0.
    split; intuition. inversion H2; eauto. subst. assumption.
  + destruct (Pdec a). 
    ++ exists (List.cons a x). split. constructor; eauto.
       rewrite H0. intro Habs. destruct Habs; eauto.
       intros. simpl. rewrite H0. intuition. subst. assumption.
    ++ exists x. split; eauto. intros. rewrite H0. intuition. simpl in H2. destruct H2; try subst; intuition. 
Qed.

(* Why3 goal *)
Lemma is_finite_union {a:Type} {a_WT:WhyType a} :
  forall (s1:a -> Init.Datatypes.bool) (s2:a -> Init.Datatypes.bool),
  is_finite s1 -> is_finite s2 -> is_finite (set.Set.union s1 s2).
Proof.
intros s1 s2 h1 h2.
destruct h1 as [l1 [Hdup1 h1]].
destruct h2 as [l2 [Hdup2 h2]].

assert (exists l, List.NoDup l /\ 
  forall x, List.In x l <-> List.In x (List.app l1 l2) /\ True).
{ eapply NoDup_exists. eapply why_decidable_eq. eauto. }
destruct H as [l [Hdup H]].
exists l.
split; eauto.
intros. generalize (List.in_app_iff l1 l2 e); intros.
rewrite H. clear H. unfold set.Set.union. rewrite Bool.orb_true_iff.
rewrite H0.
transitivity (List.In e l1 \/ s2 e = true). rewrite or_iff_compat_l; eauto. intuition.
rewrite or_iff_compat_r; eauto. reflexivity.
Qed.

(* Why3 goal *)
Lemma is_finite_union_rev {a:Type} {a_WT:WhyType a} :
  forall (s1:a -> Init.Datatypes.bool) (s2:a -> Init.Datatypes.bool),
  is_finite (set.Set.union s1 s2) -> is_finite s1 /\ is_finite s2.
Proof.
intros s1 s2 h1.
split; eapply is_finite_subset; eauto.
+ apply set.Set.subset_union_1.
+ apply set.Set.subset_union_2.
Qed.

(* Why3 goal *)
Lemma is_finite_inter_left {a:Type} {a_WT:WhyType a} :
  forall (s1:a -> Init.Datatypes.bool) (s2:a -> Init.Datatypes.bool),
  is_finite s1 -> is_finite (set.Set.inter s1 s2).
Proof.
intros s1 s2 h1.
eapply is_finite_subset; eauto.
eapply set.Set.subset_inter_1.
Qed.

(* Why3 goal *)
Lemma is_finite_inter_right {a:Type} {a_WT:WhyType a} :
  forall (s1:a -> Init.Datatypes.bool) (s2:a -> Init.Datatypes.bool),
  is_finite s2 -> is_finite (set.Set.inter s1 s2).
Proof.
intros s1 s2 h1.
eapply is_finite_subset; eauto.
eapply set.Set.subset_inter_2.
Qed.

(* Why3 goal *)
Lemma is_finite_diff {a:Type} {a_WT:WhyType a} :
  forall (s1:a -> Init.Datatypes.bool) (s2:a -> Init.Datatypes.bool),
  is_finite s1 -> is_finite (set.Set.diff s1 s2).
Proof.
intros s1 s2 h1.
eapply is_finite_subset; eauto.
eapply set.Set.subset_diff.
Qed.

(* Why3 goal *)
Lemma is_finite_map {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b} :
  forall (f:a -> b) (s:a -> Init.Datatypes.bool), is_finite s ->
  is_finite (set.Set.map f s).
Proof.
intros f s h1.
destruct h1 as [l1 [Hdup1 h1]].
assert (exists l, List.NoDup l /\ 
          forall e, List.In e l <-> List.In e (List.map f l1) /\ True).
{ eapply NoDup_exists. eapply why_decidable_eq. eauto. }
destruct H as [l [Hdupl H]].
exists l. 
split.
- assumption.
- intros. rewrite (set.Set.map_def f s e).
  rewrite H. 
  rewrite (List.in_map_iff f l1 e).
  split; intros. destruct H0. destruct H0.
  rewrite h1 in H0. exists x. intuition.
  destruct H0. 
  split.
  exists x. rewrite h1. intuition.
  constructor. 
Qed.

(* Why3 goal *)
Definition cardinal {a:Type} {a_WT:WhyType a} :
  (a -> Init.Datatypes.bool) -> Numbers.BinNums.Z.
Proof.
intros f.
(* There are no algorithms that decide at some point that the set is infinite *)
destruct (ClassicalEpsilon.excluded_middle_informative (is_finite f)).
+ (* Case when the set is finite. Take the length of a list with No duplication *)
  unfold is_finite in i. 
  assert (Hdef: {l : list a | is_finite f -> List.NoDup l /\ 
                    (forall e : a, List.In e l <-> f e = true)}).
  eapply (ClassicalEpsilon.classical_indefinite_description). 
  constructor. apply List.nil.
  destruct Hdef as (l, Hdef).
  apply (Z.of_nat (List.length l)).
+ (* Case when set is infinite: default value = 0 *)
  apply Z.zero.
Defined.

(* Why3 goal *)
Lemma cardinal_nonneg {a:Type} {a_WT:WhyType a} :
  forall (s:a -> Init.Datatypes.bool), (0%Z <= (cardinal s))%Z.
Proof.
intros s.
unfold cardinal. destruct ClassicalEpsilon.excluded_middle_informative.
destruct ClassicalEpsilon.classical_indefinite_description.
omega.
reflexivity.
Qed.

(* Why3 goal *)
Lemma cardinal_empty {a:Type} {a_WT:WhyType a} :
  forall (s:a -> Init.Datatypes.bool), is_finite s ->
  set.Set.is_empty s <-> ((cardinal s) = 0%Z).
Proof.
intros s h1.
unfold cardinal. assert (Hsav := h1). destruct h1. 
destruct ClassicalEpsilon.excluded_middle_informative as [Hfin | Hnfin].
- destruct ClassicalEpsilon.classical_indefinite_description as (l, Hex).
  specialize (Hex Hfin).
  split; intros. 
  * unfold set.Set.is_empty, set.Set.mem in H0. 
    destruct l.
    + reflexivity.
    + destruct (H0 a0). eapply Hex. left. reflexivity.
  * unfold set.Set.is_empty, set.Set.mem. intros e Habs. eapply Hex in Habs.
    destruct l. destruct Habs. inversion H0.
- intuition. 
Qed.

(* Why3 goal *)
Lemma cardinal_add {a:Type} {a_WT:WhyType a} :
  forall (x:a), forall (s:a -> Init.Datatypes.bool), is_finite s ->
  (set.Set.mem x s ->
   ((cardinal (map.Map.set s x Init.Datatypes.true)) = (cardinal s))) /\
  (~ set.Set.mem x s ->
   ((cardinal (map.Map.set s x Init.Datatypes.true)) =
    ((cardinal s) + 1%Z)%Z)).
Proof.
intros x s h1.
split; intros.
- rewrite <- (set.Set.extensionality s (Map.set s x true)). reflexivity. intro.
  unfold set.Set.mem, Map.set in *. destruct why_decidable_eq; try subst; intuition.
- assert (is_finite (Map.set s x true)). { apply is_finite_add. assumption. }
  unfold cardinal.
  destruct ClassicalEpsilon.excluded_middle_informative; [| intuition].
  destruct ClassicalEpsilon.classical_indefinite_description.
  destruct ClassicalEpsilon.excluded_middle_informative; [| intuition].
  destruct ClassicalEpsilon.classical_indefinite_description.
  specialize (a0 H0). specialize (a1 h1).
  assert (Hnat: length x0 = S (length x1)). 
  { (* Here we base the proof on the fact that the first list where one cons x is the 
       same length as the second one because they have the same elements and NoDup. *)
    assert (List.NoDup (List.cons x x1)). 
    { constructor. intro Habs. apply H. eapply a1 in Habs. assumption. apply a1. }
    assert (forall e, List.In e (x :: x1) <-> List.In e x0). 
    {
      intros. simpl. destruct a0 as (Hdupx0, Heq0). rewrite Heq0. destruct a1 as (Hdupx1, Heq1).
      rewrite Heq1. unfold Map.set. destruct why_decidable_eq; intuition. 
    }
    assert (length x0 <= length (List.cons x x1) /\ (length (List.cons x x1) <= length x0)).  
    {
      split.
      + eapply List.NoDup_incl_length; eauto. apply a0. intros e Hincl. eapply H2. assumption.
      + eapply List.NoDup_incl_length; eauto. intros e Hincl. eapply H2. assumption.
    }
    intuition.
  }
  rewrite Hnat. rewrite Nat2Z.inj_succ. ring. 
Qed.

(* Why3 goal *)
Lemma cardinal_remove {a:Type} {a_WT:WhyType a} :
  forall (x:a), forall (s:a -> Init.Datatypes.bool), is_finite s ->
  (set.Set.mem x s ->
   ((cardinal (map.Map.set s x Init.Datatypes.false)) =
    ((cardinal s) - 1%Z)%Z)) /\
  (~ set.Set.mem x s ->
   ((cardinal (map.Map.set s x Init.Datatypes.false)) = (cardinal s))).
Proof.
intros x s h1.
split.
- intros.
  pose (s' := Map.set s x false).
  fold s'. 
  assert (Map.set s' x true = s). 
  { 
    apply set.Set.extensionality. intro e.
    unfold s', set.Set.mem. unfold Map.set. destruct why_decidable_eq. subst. intuition.
    intuition.
  }
  rewrite <- H0.
  assert (~ set.Set.mem x s'). 
  { unfold s'. unfold Map.set, set.Set.mem.
    destruct why_decidable_eq; intuition. 
  }
  eapply cardinal_add in H1. rewrite H1. ring.
  unfold s'. eapply is_finite_remove. assumption.
- intros.
  assert (Map.set s x false = s).
  {
    apply set.Set.extensionality. intro. unfold Map.set, set.Set.mem.
    destruct why_decidable_eq; intuition. subst. eauto.
  }
  rewrite H0. reflexivity.
Qed.

(* Why3 goal *)
Lemma cardinal_subset {a:Type} {a_WT:WhyType a} :
  forall (s1:a -> Init.Datatypes.bool) (s2:a -> Init.Datatypes.bool),
  is_finite s2 -> set.Set.subset s1 s2 -> ((cardinal s1) <= (cardinal s2))%Z.
Proof.
intros s1 s2 h1 h2.
assert (is_finite s1).
{
  eapply is_finite_subset; eauto.
}
(* Remove ClassicalEpsilon noise *)
unfold cardinal.
destruct ClassicalEpsilon.excluded_middle_informative; [| intuition].
destruct ClassicalEpsilon.classical_indefinite_description.
destruct ClassicalEpsilon.excluded_middle_informative; [| intuition].
destruct ClassicalEpsilon.classical_indefinite_description.
specialize (a0 H). specialize (a1 h1).
destruct a0 as [Hdupx Heqx]. destruct a1 as [Hdupx0 Heqx0].
(* Same goal without ClassicalEpsilon indirection *)
assert (List.length x <= List.length x0).
{
  eapply List.NoDup_incl_length; eauto.
  intros e H1.
  eapply Heqx0. eapply Heqx in H1. unfold set.Set.subset, set.Set.mem in h2. eapply h2 in H1. assumption.
}
omega.
Qed.

(* Why3 goal *)
Lemma subset_eq {a:Type} {a_WT:WhyType a} :
  forall (s1:a -> Init.Datatypes.bool) (s2:a -> Init.Datatypes.bool),
  is_finite s2 -> set.Set.subset s1 s2 -> ((cardinal s1) = (cardinal s2)) ->
  (s1 = s2).
Proof.
intros s1 s2 h1 h2 h3.
assert (is_finite s1). 
{
  eapply is_finite_subset; eauto.
}
unfold cardinal in h3.
(* Remove classical epsilon noise *)
destruct ClassicalEpsilon.excluded_middle_informative; [| intuition].
destruct ClassicalEpsilon.classical_indefinite_description.
destruct ClassicalEpsilon.excluded_middle_informative; [| intuition].
destruct ClassicalEpsilon.classical_indefinite_description.
specialize (a0 H). specialize (a1 h1).
rename x into l1.
rename x0 into l2.
destruct a0 as [Hdup1 Heq1].
destruct a1 as [Hdup2 Heq2].
assert (List.incl l1 l2).
{
  intros e H1. eapply Heq2. eapply h2. eapply Heq1. assumption.
}
eapply set.Set.extensionality. intro.
unfold set.Set.mem.
unfold set.Set.subset in h2.
rewrite <- Heq2, <- Heq1.
assert (List.length l1 = List.length l2).
{
  omega.
}
split. eauto.
eapply List.NoDup_length_incl; eauto. omega.
Qed.

(* Why3 goal *)
Lemma cardinal1 {a:Type} {a_WT:WhyType a} :
  forall (s:a -> Init.Datatypes.bool), ((cardinal s) = 1%Z) -> forall (x:a),
  set.Set.mem x s -> (x = (set.Set.pick s)).
Proof.
intros s h1 x h2.
unfold cardinal in *.
destruct ClassicalEpsilon.excluded_middle_informative.
* destruct ClassicalEpsilon.classical_indefinite_description.
  specialize (a0 i). 
  assert (H: ~ set.Set.is_empty s). { unfold set.Set.is_empty. intro. eapply H. eassumption. } 
  specialize (set.Set.pick_def s H). intros. unfold set.Set.mem in *.
  destruct x0. 
  + inversion h1.
  + destruct x0.
    - simpl in a0. eapply a0 in h2. eapply a0 in H0. intuition. subst. assumption.
    - simpl in h1; contradict h1; zify; omega.
* inversion h1.
Qed.

Lemma length_prop: forall {A} (eq_dec: forall x y: A, {x = y} + {x <> y}) lu li (lui: List.list A), 
  List.NoDup lu -> List.NoDup li -> List.NoDup lui ->
  List.incl li lu -> (forall e, List.In e lui <-> List.In e lu /\ not (List.In e li)) ->
  List.length lui = List.length lu - List.length li.
Proof.
induction lu; intros.
+ assert (lui = List.nil). destruct lui; eauto. specialize (H3 a); eauto. intuition. destruct H4.
  left. reflexivity. destruct H4.
  subst. reflexivity.
+ destruct (List.in_dec eq_dec a li).
  * destruct (List.in_split a li i) as [li' [li'' Hlieq]].
    assert (List.length lui = List.length lu - List.length (List.app li' li'')).
    { 
      eapply IHlu; eauto.
      - inversion H; eauto.
      - rewrite Hlieq in H0. eapply List.NoDup_remove_1; eauto.
      - intro. intros. specialize (H2 a0). rewrite Hlieq in H2.
        simpl in H2. rewrite List.in_app_iff in H2. simpl in H2.
        destruct (eq_dec a a0). 
        * subst. eapply List.NoDup_remove_2 in H0; intuition.
        * destruct H2.
          ++ eapply List.in_app_iff in H4. intuition. 
          ++ destruct n; eauto.
          ++ assumption.
     - intros. rewrite H3. simpl. rewrite List.in_app_iff.
       rewrite Hlieq. rewrite List.in_app_iff. simpl. intuition.
       subst. inversion H. intuition.
   }
   rewrite Hlieq. rewrite List.app_length. simpl length.
   rewrite H4. rewrite List.app_length. omega.
  * assert (List.In a lui). { eapply H3. split. left. reflexivity. assumption. }
    destruct (List.in_split a lui H4) as [lui' [lui'' Hlui]].
    assert (length (List.app lui' lui'') = length lu - length li).
    {
      eapply IHlu; eauto.
      - inversion H. assumption.
      - rewrite Hlui in H1.  eapply List.NoDup_remove_1; eauto.
      - intros e Hincl. specialize (H2 e Hincl). simpl in H2. intuition. subst.
        intuition.
      - intros. destruct (eq_dec a e).
        -- split; intros. assert False. rewrite Hlui in H1. eapply List.NoDup_remove_2 in H1. destruct H1. 
           subst. assumption. destruct H6.
           inversion H. subst. destruct H8. apply H5.
        -- rewrite Hlui in H3. specialize (H3 e).
           rewrite List.in_app_iff in H3. simpl in H3.
           rewrite List.in_app_iff. clear - H3 n0. intuition.
    }
    rewrite Hlui. rewrite List.app_length. simpl length. rewrite List.app_length in H5.
    assert (List.length li <= List.length lu).
    {
      eapply List.NoDup_incl_length; eauto.
      intros e Hincl. specialize (H2 e Hincl). simpl in H2. intuition. subst.
      intuition.
    }
  omega.
Qed.

Lemma NoDup_app: forall {A} l l' 
  (Hnotin1: forall e: A, List.In e l -> ~ List.In e l')
  (Hnotin2: forall e, List.In e l' -> ~ List.In e l),
  List.NoDup l -> List.NoDup l' -> List.NoDup (List.app l l').
Proof.
induction l; intros.
+ simpl. assumption.
+ simpl. constructor; eauto.
  - intro. rewrite List.in_app_iff in H1. destruct H1. inversion H; intuition.
    eapply Hnotin1; eauto. left. reflexivity.
  - eapply IHl; eauto.
    * intros. eapply Hnotin1. right. assumption.
    * intros. eapply Hnotin2 in H1. intro Habs. destruct H1. right. assumption.
    * inversion H; eauto.
Qed.

(* Why3 goal *)
Lemma cardinal_union {a:Type} {a_WT:WhyType a} :
  forall (s1:a -> Init.Datatypes.bool) (s2:a -> Init.Datatypes.bool),
  is_finite s1 -> is_finite s2 ->
  ((cardinal (set.Set.union s1 s2)) =
   (((cardinal s1) + (cardinal s2))%Z - (cardinal (set.Set.inter s1 s2)))%Z).
Proof.
intros s1 s2 h1 h2.
assert (is_finite (set.Set.union s1 s2)). { apply is_finite_union; eauto. }
assert (is_finite (set.Set.inter s1 s2)). { apply is_finite_inter_left; eauto. }
unfold cardinal.
(* Remove classical epsilon noise *)
destruct ClassicalEpsilon.excluded_middle_informative; [| intuition].
destruct ClassicalEpsilon.classical_indefinite_description.
destruct ClassicalEpsilon.excluded_middle_informative; [| intuition].
destruct ClassicalEpsilon.classical_indefinite_description.
destruct ClassicalEpsilon.excluded_middle_informative; [| intuition].
destruct ClassicalEpsilon.classical_indefinite_description.
destruct ClassicalEpsilon.excluded_middle_informative; [| intuition].
destruct ClassicalEpsilon.classical_indefinite_description.
specialize (a0 H). specialize (a1 h1). specialize (a2 h2). specialize (a3 H0).
destruct a0 as [Hdup_un Heq_un].
destruct a1 as [Hdups2 Heqs2].
destruct a2 as [Hdups1 Heqs1].
destruct a3 as [Hdup_int Heq_int].
rename x into lun. rename x0 into l1. rename x1 into l2. rename x2 into lint.
(* In terms of list, we create the list that has elements of union - intersection. 
   And we create the union of (l1 - intersection) and (l2 - intersection).
   We obtain a list equality. We can deduce the length equation from that. *)
assert (exists lun_lint, List.NoDup lun_lint /\
  forall e, List.In e lun_lint <-> (List.In e lun /\ not (List.In e lint))).
{
  eapply NoDup_exists. eapply why_decidable_eq. intros. 
  destruct (List.in_dec why_decidable_eq e lint); eauto.
}
destruct H1 as [lun_lint [Hduplun_lint Heqlun_lint]].
assert (List.length lun_lint = List.length lun - List.length lint).
{
eapply length_prop; eauto. apply why_decidable_eq.
intro. intros. eapply Heq_un. eapply set.Set.union_def. eapply Heq_int in H1.
eapply set.Set.inter_def in H1. intuition.
}

assert (exists l1_lint, List.NoDup l1_lint /\
  forall e, List.In e l1_lint <-> (List.In e l1 /\ not (List.In e lint))).
{
  eapply NoDup_exists. eapply why_decidable_eq. intros. 
  destruct (List.in_dec why_decidable_eq e lint); eauto.
}
destruct H2 as [l1_lint [Hdupl1_lint Heql1_lint]].
assert (List.length l1_lint = List.length l1 - List.length lint).
{
  eapply length_prop; eauto. apply why_decidable_eq.
  intro. intros. eapply Heqs2. eapply Heq_int in H2.
  eapply set.Set.inter_def in H2. intuition.
}
assert (exists l2_lint, List.NoDup l2_lint /\
  forall e, List.In e l2_lint <-> (List.In e l2 /\ not (List.In e lint))).
{
  eapply NoDup_exists. eapply why_decidable_eq. intros. 
  destruct (List.in_dec why_decidable_eq e lint); eauto.
}
destruct H3 as [l2_lint [Hdupl2_lint Heql2_lint]].
assert (List.length l2_lint = List.length l2 - List.length lint).
{
  eapply length_prop; eauto. apply why_decidable_eq.
  intro. intros. eapply Heqs1. eapply Heq_int in H3.
  eapply set.Set.inter_def in H3. intuition.
}
assert (List.NoDup (List.app l1_lint l2_lint) /\
  forall e, List.In e lun_lint <-> List.In e (List.app l1_lint l2_lint)).
{
  split. 
  - eapply NoDup_app; eauto. 
    + intros. rewrite Heql2_lint. eapply Heql1_lint in H4.
      rewrite Heqs2 in H4. rewrite Heq_int in H4. rewrite Heq_int.
      rewrite Heqs1. rewrite set.Set.inter_def in H4. rewrite set.Set.inter_def.
      unfold set.Set.mem in *. intuition.
    + intros. rewrite Heql2_lint in H4. rewrite Heql1_lint.
      rewrite Heqs2. rewrite Heq_int. rewrite Heq_int in H4.
      rewrite Heqs1 in H4. rewrite set.Set.inter_def in H4. rewrite set.Set.inter_def.
      unfold set.Set.mem in *. intuition.
  - intros. rewrite List.in_app_iff. rewrite Heqlun_lint.
  rewrite Heql1_lint. rewrite Heql2_lint. rewrite Heq_un, Heqs2, Heqs1, Heq_int.
  rewrite set.Set.union_def. rewrite set.Set.inter_def. unfold set.Set.mem.
  clear - s1. intuition.
}
assert (List.length (List.app l1_lint l2_lint) = List.length lun_lint).
{
  assert (List.length (List.app l1_lint l2_lint) <= List.length lun_lint).
  eapply List.NoDup_incl_length; intuition. intro. apply H6.
  assert (List.length (List.app l1_lint l2_lint) >= List.length lun_lint).
  eapply List.NoDup_incl_length; intuition. intro. apply H7.
  omega.
}

assert (length l1 >= length lint).
{
  eapply List.NoDup_incl_length; intuition. intros e Hincl. eapply Heq_int in Hincl.
  eapply Heqs2. eapply set.Set.inter_def in Hincl. intuition.
}
assert (length l2 >= length lint).
{
  eapply List.NoDup_incl_length; intuition. intros e Hincl. eapply Heq_int in Hincl.
  eapply Heqs1. eapply set.Set.inter_def in Hincl. intuition.
}
assert (length lun >= length lint).
{
  eapply List.NoDup_incl_length; intuition. intros e Hincl. eapply Heq_int in Hincl.
  eapply Heq_un. eapply set.Set.inter_def in Hincl. eapply set.Set.union_def. intuition.
}
rewrite List.app_length in H5. omega.
Qed.

(* Why3 goal *)
Lemma cardinal_inter_disjoint {a:Type} {a_WT:WhyType a} :
  forall (s1:a -> Init.Datatypes.bool) (s2:a -> Init.Datatypes.bool),
  set.Set.disjoint s1 s2 -> ((cardinal (set.Set.inter s1 s2)) = 0%Z).
Proof.
intros s1 s2 h1.
eapply set.Set.disjoint_inter_empty in h1.
unfold set.Set.is_empty, set.Set.mem in h1.
unfold cardinal.
destruct ClassicalEpsilon.excluded_middle_informative; [| intuition].
destruct ClassicalEpsilon.classical_indefinite_description.
specialize (a0 i). destruct a0.
destruct x. reflexivity.
destruct (h1 a0). eapply H0. left. reflexivity.
Qed.

(* Why3 goal *)
Lemma cardinal_diff {a:Type} {a_WT:WhyType a} :
  forall (s1:a -> Init.Datatypes.bool) (s2:a -> Init.Datatypes.bool),
  is_finite s1 ->
  ((cardinal (set.Set.diff s1 s2)) =
   ((cardinal s1) - (cardinal (set.Set.inter s1 s2)))%Z).
Proof.
intros s1 s2 h1.
assert (is_finite (set.Set.inter s1 s2)). { apply is_finite_inter_left; eauto. }
assert (is_finite (set.Set.diff s1 s2)). { apply is_finite_diff; eauto. }
unfold cardinal.
(* Remove classical epsilon noise *)
destruct ClassicalEpsilon.excluded_middle_informative; [| intuition].
destruct ClassicalEpsilon.classical_indefinite_description.
destruct ClassicalEpsilon.excluded_middle_informative; [| intuition].
destruct ClassicalEpsilon.classical_indefinite_description.
destruct ClassicalEpsilon.excluded_middle_informative; [| intuition].
destruct ClassicalEpsilon.classical_indefinite_description.
specialize (a0 i). specialize (a1 i0). specialize (a2 i1).
destruct a0, a1, a2.
assert (List.length x = List.length x0 - List.length x1).
{
  eapply length_prop; eauto.
  - apply why_decidable_eq.
  - intros e Hin. eapply H6 in Hin. eapply H4. eapply set.Set.inter_def in Hin.
    apply Hin.
  - intros. rewrite H6. rewrite H4. rewrite H2. rewrite set.Set.diff_def.
    rewrite set.Set.inter_def. intuition.
}
assert (List.length x0 >= List.length x1).
eapply List.NoDup_incl_length; intuition.
{
  intros e Hincl. eapply H4. eapply H6 in Hincl. rewrite set.Set.inter_def in Hincl.
  intuition.
}
omega.
Qed.

(* Why3 goal *)
Lemma cardinal_map {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b} :
  forall (f:a -> b) (s:a -> Init.Datatypes.bool), is_finite s ->
  ((cardinal (set.Set.map f s)) <= (cardinal s))%Z.
Proof.
intros f s h1.
assert (is_finite (set.Set.map f s)). { eapply is_finite_map. assumption. }
unfold cardinal.
(* Remove classical epsilon noise *)
destruct ClassicalEpsilon.excluded_middle_informative; [| intuition].
destruct ClassicalEpsilon.classical_indefinite_description.
destruct ClassicalEpsilon.excluded_middle_informative; [| intuition].
destruct ClassicalEpsilon.classical_indefinite_description.
specialize (a0 i). specialize (a1 i0).
destruct a0, a1.
assert (List.length x <= List.length x0).
{
  eapply le_trans with (List.length (List.map f x0)).
  - assert (List.incl x (List.map f x0)).
    { intro. intros. eapply H1 in H4. rewrite set.Set.map_def in H4.
      destruct H4. destruct H4. subst.
      eapply List.in_map. eapply H3; eauto.
    }
    eapply List.NoDup_incl_length; eauto.
  - rewrite List.map_length; eauto.
}
omega.
Qed.