From 23cf299ea8a0a3a73df143b5dced6ba43caacea3 Mon Sep 17 00:00:00 2001 From: Sylvain Dailler Date: Thu, 4 Apr 2019 17:34:13 +0200 Subject: [PATCH] fix c5d97975b to a correct version of Coq --- lib/coq/set/Cardinal.v | 5 +++-- lib/coq/set/Fset.v | 12 ++++++++---- lib/coq/set/FsetInt.v | 1 - 3 files changed, 11 insertions(+), 7 deletions(-) diff --git a/lib/coq/set/Cardinal.v b/lib/coq/set/Cardinal.v index f9338432e..224efb9ac 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 32e9742c0..ab29510f4 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 3daf62464..7d770c02a 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 -- GitLab