diff --git a/lib/coq/set/Cardinal.v b/lib/coq/set/Cardinal.v index f9338432ed9f5d5a063633bfd0094e6d6f997c44..224efb9acea643cacd29e4f8fed584d44537922f 100644 --- a/lib/coq/set/Cardinal.v +++ b/lib/coq/set/Cardinal.v @@ -475,7 +475,7 @@ destruct ClassicalEpsilon.excluded_middle_informative. destruct x0. + inversion h1. + destruct x0. - - simpl in a0. eapply a0 in h2. eapply a0 in H0. intuition. subst. assumption. + - simpl in a0. eapply a0 in h2. eapply a0 in H0. intuition. subst. reflexivity. - simpl in h1; contradict h1; zify; omega. * inversion h1. Qed. @@ -748,4 +748,5 @@ assert (List.length x <= List.length x0). - rewrite List.map_length; eauto. } omega. -Qed. \ No newline at end of file +Qed. + diff --git a/lib/coq/set/Fset.v b/lib/coq/set/Fset.v index 32e9742c0659285c586efac5951a33b7a5a74a84..ab29510f4c50f6f891b25343b6a5c8b178fdd086 100644 --- a/lib/coq/set/Fset.v +++ b/lib/coq/set/Fset.v @@ -4,8 +4,6 @@ Require Import BuiltIn. Require BuiltIn. Require HighOrd. Require int.Int. -Require set.Cardinal. -Require set.Set. (* Why3 goal *) Definition fset : forall (a:Type), Type. @@ -19,6 +17,8 @@ Defined. Definition mem {a:Type} {a_WT:WhyType a} : a -> fset a -> Prop. Proof. intros. destruct X0 as (f, P). +(* TODO remove this *) +Require set.Set. apply (set.Set.mem X f). Defined. @@ -34,7 +34,8 @@ Proof. intros s1 s2 h1. unfold infix_eqeq in h1. unfold mem in h1. destruct s1, s2. -assert (x = x0). eapply set.Set.extensionality. intro. eauto. +assert (x = x0). +eapply set.Set.extensionality. intro. eauto. subst. assert (e = e0). (* TODO maybe provable on such property ? *) @@ -71,7 +72,10 @@ Definition is_empty {a:Type} {a_WT:WhyType a} (s:fset a) : Prop := (* Why3 goal *) Definition empty {a:Type} {a_WT:WhyType a} : fset a. Proof. -exists (fun x => false). apply Cardinal.is_finite_empty. unfold set.Set.is_empty. +exists (fun x => false). +(* TODO remove this *) +Require Cardinal. +apply Cardinal.is_finite_empty. unfold set.Set.is_empty. unfold set.Set.mem. intuition. Defined. diff --git a/lib/coq/set/FsetInt.v b/lib/coq/set/FsetInt.v index 3daf6246497958798a63b16075b6b9ae05094d45..7d770c02a113af41e008da282f16b5cc976b5a4e 100644 --- a/lib/coq/set/FsetInt.v +++ b/lib/coq/set/FsetInt.v @@ -196,7 +196,6 @@ unfold interval, Fset.mem, set.Set.mem. destruct Z_le_dec; try destruct Z_lt_dec; intuition; try inversion H. Qed. - Lemma interval_is_finite: forall l r, Cardinal.is_finite (fun x : int => if Z_le_dec l x then if Z_lt_dec x r then true