Commit e58d9baf authored by Sylvain Dailler's avatar Sylvain Dailler

Merge branch 'issue_290' #fix 290

parents f5daea84 23cf299e
......@@ -30,6 +30,10 @@ IDE
* display of counterexamples in the Task view has been improved
* auto jumping to next unproved goal can now be disabled in the preferences
Realizations
* Added experimental realizations for new Set theories in both Isabelle and
Coq
Version 1.2.0, February 11, 2019
--------------------------------
......
......@@ -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
......
(* 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. reflexivity.
- 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.