Add experimental coq realization for Fset and other Set theory

The underlying datastructure is not satisfying nor are the proofs but at
least there is a quick simple realization. It uses ClassicalEpsilon axioms
such as excluded middle, indefinite_description etc...
Some theory realizations are very far from reality because the axiom
characterization is small.

CHANGES.md

@@ -31,6 +31,10 @@ Transformations
 Counterexamples
   * Improved display of counterexamples in Task view
 
+Realizations
+  * Added experimental realizations for new Set theories in both Isabelle and
+  Coq
+
 
 Version 1.2.0, February 11, 2019
 --------------------------------

Makefile.in

@@ -974,7 +974,7 @@ COQLIBS_REAL = $(addprefix lib/coq/real/, $(COQLIBS_REAL_FILES))
 COQLIBS_NUMBER_FILES = Divisibility Gcd Parity Prime Coprime
 COQLIBS_NUMBER = $(addprefix lib/coq/number/, $(COQLIBS_NUMBER_FILES))
 
-COQLIBS_SET_FILES = Set
+COQLIBS_SET_FILES = Set Cardinal Fset FsetInduction FsetInt FsetSum SetApp SetAppInt SetImp SetImpInt
 COQLIBS_SET = $(addprefix lib/coq/set/, $(COQLIBS_SET_FILES))
 
 COQLIBS_MAP_FILES = Map Const Occ MapPermut MapInjection

lib/coq/set/Cardinal.v

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