(* 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.