Commit 23cf299e authored by Sylvain Dailler's avatar Sylvain Dailler

fix c5d97975 to a correct version of Coq

parent c5d97975
...@@ -475,7 +475,7 @@ destruct ClassicalEpsilon.excluded_middle_informative. ...@@ -475,7 +475,7 @@ destruct ClassicalEpsilon.excluded_middle_informative.
destruct x0. destruct x0.
+ inversion h1. + inversion h1.
+ destruct x0. + 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. - simpl in h1; contradict h1; zify; omega.
* inversion h1. * inversion h1.
Qed. Qed.
...@@ -748,4 +748,5 @@ assert (List.length x <= List.length x0). ...@@ -748,4 +748,5 @@ assert (List.length x <= List.length x0).
- rewrite List.map_length; eauto. - rewrite List.map_length; eauto.
} }
omega. omega.
Qed. Qed.
\ No newline at end of file
...@@ -4,8 +4,6 @@ Require Import BuiltIn. ...@@ -4,8 +4,6 @@ Require Import BuiltIn.
Require BuiltIn. Require BuiltIn.
Require HighOrd. Require HighOrd.
Require int.Int. Require int.Int.
Require set.Cardinal.
Require set.Set.
(* Why3 goal *) (* Why3 goal *)
Definition fset : forall (a:Type), Type. Definition fset : forall (a:Type), Type.
...@@ -19,6 +17,8 @@ Defined. ...@@ -19,6 +17,8 @@ Defined.
Definition mem {a:Type} {a_WT:WhyType a} : a -> fset a -> Prop. Definition mem {a:Type} {a_WT:WhyType a} : a -> fset a -> Prop.
Proof. Proof.
intros. destruct X0 as (f, P). intros. destruct X0 as (f, P).
(* TODO remove this *)
Require set.Set.
apply (set.Set.mem X f). apply (set.Set.mem X f).
Defined. Defined.
...@@ -34,7 +34,8 @@ Proof. ...@@ -34,7 +34,8 @@ Proof.
intros s1 s2 h1. intros s1 s2 h1.
unfold infix_eqeq in h1. unfold mem in h1. unfold infix_eqeq in h1. unfold mem in h1.
destruct s1, s2. destruct s1, s2.
assert (x = x0). eapply set.Set.extensionality. intro. eauto. assert (x = x0).
eapply set.Set.extensionality. intro. eauto.
subst. subst.
assert (e = e0). assert (e = e0).
(* TODO maybe provable on such property ? *) (* TODO maybe provable on such property ? *)
...@@ -71,7 +72,10 @@ Definition is_empty {a:Type} {a_WT:WhyType a} (s:fset a) : Prop := ...@@ -71,7 +72,10 @@ Definition is_empty {a:Type} {a_WT:WhyType a} (s:fset a) : Prop :=
(* Why3 goal *) (* Why3 goal *)
Definition empty {a:Type} {a_WT:WhyType a} : fset a. Definition empty {a:Type} {a_WT:WhyType a} : fset a.
Proof. 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. unfold set.Set.mem. intuition.
Defined. Defined.
......
...@@ -196,7 +196,6 @@ unfold interval, Fset.mem, set.Set.mem. ...@@ -196,7 +196,6 @@ unfold interval, Fset.mem, set.Set.mem.
destruct Z_le_dec; try destruct Z_lt_dec; intuition; try inversion H. destruct Z_le_dec; try destruct Z_lt_dec; intuition; try inversion H.
Qed. Qed.
Lemma interval_is_finite: forall l r, Lemma interval_is_finite: forall l r,
Cardinal.is_finite (fun x : int => Cardinal.is_finite (fun x : int =>
if Z_le_dec l x then if Z_lt_dec x r then true if Z_le_dec l x then if Z_lt_dec x r then true
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment