From 3ef4b170c3cb0bcfc3b26a082e792da936f52044 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sun, 21 May 2017 08:24:08 +0200 Subject: [PATCH] Fix some Coq realizations. --- lib/coq/int/Int.v | 28 ++--- lib/coq/list/List.v | 18 +++ lib/coq/map/Const.v | 13 +- lib/coq/map/Map.v | 46 +++---- lib/coq/number/Divisibility.v | 11 +- lib/coq/number/Parity.v | 3 - lib/coq/option/Option.v | 18 +++ lib/coq/real/Real.v | 32 ++--- lib/coq/real/RealInfix.v | 7 ++ lib/coq/set/Set.v | 220 +++++++++++++++++----------------- 10 files changed, 221 insertions(+), 175 deletions(-) diff --git a/lib/coq/int/Int.v b/lib/coq/int/Int.v index d354c0e39..77962ac75 100644 --- a/lib/coq/int/Int.v +++ b/lib/coq/int/Int.v @@ -15,22 +15,27 @@ Require Import BuiltIn. Require BuiltIn. (* Why3 comment *) -(* infix_ls is replaced with (x < x1)%Z by the coq driver *) - -(* Why3 goal *) -Lemma infix_lseq_def : forall (x:Z) (y:Z), (x <= y)%Z <-> ((x < y)%Z \/ - (x = y)). -exact Zle_lt_or_eq_iff. -Qed. +(* prefix_mn is replaced with (-x)%Z by the coq driver *) (* Why3 comment *) (* infix_pl is replaced with (x + x1)%Z by the coq driver *) (* Why3 comment *) -(* prefix_mn is replaced with (-x)%Z by the coq driver *) +(* infix_as is replaced with (x * x1)%Z by the coq driver *) (* Why3 comment *) -(* infix_as is replaced with (x * x1)%Z by the coq driver *) +(* infix_ls is replaced with (x < x1)%Z by the coq driver *) + +(* Why3 goal *) +Lemma infix_mn_def : forall (x:Z) (y:Z), ((x - y)%Z = (x + (-y)%Z)%Z). +reflexivity. +Qed. + +(* Why3 goal *) +Lemma infix_lseq_def : forall (x:Z) (y:Z), (x <= y)%Z <-> ((x < y)%Z \/ + (x = y)). +exact Zle_lt_or_eq_iff. +Qed. (* Why3 goal *) Lemma Assoc : forall (x:Z) (y:Z) (z:Z), @@ -96,11 +101,6 @@ intros x y z. apply Zmult_plus_distr_l. Qed. -(* Why3 goal *) -Lemma infix_mn_def : forall (x:Z) (y:Z), ((x - y)%Z = (x + (-y)%Z)%Z). -reflexivity. -Qed. - (* Why3 goal *) Lemma Comm1 : forall (x:Z) (y:Z), ((x * y)%Z = (y * x)%Z). Proof. diff --git a/lib/coq/list/List.v b/lib/coq/list/List.v index 6fc73fd98..4eb9c2379 100644 --- a/lib/coq/list/List.v +++ b/lib/coq/list/List.v @@ -14,7 +14,25 @@ Require Import BuiltIn. Require BuiltIn. +(* Why3 assumption *) +Definition is_nil {a:Type} {a_WT:WhyType a} (l:(list a)): Prop := + match l with + | Init.Datatypes.nil => True + | (Init.Datatypes.cons _ _) => False + end. + +(* Why3 goal *) +Lemma is_nil_spec : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)), + (is_nil l) <-> (l = Init.Datatypes.nil). +Proof. +intros a a_WT l. +split. +now destruct l. +now intros ->. +Qed. + Global Instance list_WhyType : forall T {T_WT : WhyType T}, WhyType (list T). +Proof. split. apply nil. induction x as [|xh x] ; intros [|yh y] ; try (now right). diff --git a/lib/coq/map/Const.v b/lib/coq/map/Const.v index 1559df983..6f9a6a4b0 100644 --- a/lib/coq/map/Const.v +++ b/lib/coq/map/Const.v @@ -13,22 +13,23 @@ (* Beware! Only edit allowed sections below *) Require Import BuiltIn. Require BuiltIn. +Require HighOrd. Require map.Map. (* Why3 goal *) Definition const: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, - b -> (map.Map.map a b). + b -> (a -> b). +Proof. intros a a_WT b b_WT v. intros i. exact v. Defined. (* Why3 goal *) -Lemma Const : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, - forall (b1:b) (a1:a), ((map.Map.get (const b1: (map.Map.map a b)) - a1) = b1). +Lemma const_def : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, + forall (v:b), forall (us:a), (((const v: (a -> b)) us) = v). +Proof. intros a a_WT b b_WT b1 a1. -unfold const. -auto. +reflexivity. Qed. diff --git a/lib/coq/map/Map.v b/lib/coq/map/Map.v index e94d1bd40..1dc429dd9 100644 --- a/lib/coq/map/Map.v +++ b/lib/coq/map/Map.v @@ -13,6 +13,7 @@ (* Beware! Only edit allowed sections below *) Require Import BuiltIn. Require BuiltIn. +Require HighOrd. (* This file is generated by Why3's Coq-realize driver *) (* Beware! Only edit allowed sections below *) @@ -21,11 +22,8 @@ Require BuiltIn. Require Import ClassicalEpsilon. -(* Why3 goal *) -Definition map : forall (a:Type) (b:Type), Type. -intros. -exact (a -> b). -Defined. +(* Why3 assumption *) +Definition map (a:Type) (b:Type) := (a -> b). Global Instance map_WhyType : forall (a:Type) {a_WT:WhyType a} (b:Type) {b_WT:WhyType b}, WhyType (map a b). Proof. @@ -36,16 +34,10 @@ intros x y. apply excluded_middle_informative. Qed. -(* Why3 goal *) -Definition get: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, - (map a b) -> a -> b. -intros a a_WT b b_WT m x. -exact (m x). -Defined. - (* Why3 goal *) Definition set: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, - (map a b) -> a -> b -> (map a b). + (a -> b) -> a -> b -> (a -> b). +Proof. intros a a_WT b b_WT m x y. intros x'. destruct (why_decidable_eq x x') as [H|H]. @@ -54,22 +46,18 @@ exact (m x'). Defined. (* Why3 goal *) -Lemma Select_eq : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, - forall (m:(map a b)), forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> - ((get (set m a1 b1) a2) = b1). -Proof. -intros a a_WT b b_WT m a1 a2 b1 h1. -unfold get, set. -now case why_decidable_eq. -Qed. - -(* Why3 goal *) -Lemma Select_neq : forall {a:Type} {a_WT:WhyType a} - {b:Type} {b_WT:WhyType b}, forall (m:(map a b)), forall (a1:a) (a2:a), - forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1) a2) = (get m a2)). +Lemma set_def : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, + forall (f:(a -> b)) (x:a) (v:b), forall (y:a), ((y = x) -> (((set f x v) + y) = v)) /\ ((~ (y = x)) -> (((set f x v) y) = (f y))). Proof. -intros a a_WT b b_WT m a1 a2 b1 h1. -unfold get, set. -now case why_decidable_eq. +intros a a_WT b b_WT f x v y. +unfold set. +case why_decidable_eq. +intros <-. +easy. +intros H. +split ; intros H'. +now elim H. +easy. Qed. diff --git a/lib/coq/number/Divisibility.v b/lib/coq/number/Divisibility.v index 29898a7cf..705ce58aa 100644 --- a/lib/coq/number/Divisibility.v +++ b/lib/coq/number/Divisibility.v @@ -22,13 +22,22 @@ Require number.Parity. (* Hack so that Why3 does not override the notation below. (* Why3 assumption *) -Definition divides (d:Z) (n:Z): Prop := exists q:Z, (n = (q * d)%Z). +Definition divides (d:Z) (n:Z): Prop := ((d = 0%Z) -> (n = 0%Z)) /\ + ((~ (d = 0%Z)) -> ((ZArith.BinInt.Z.rem n d) = 0%Z)). *) Require Import Znumtheory. Notation divides := Zdivide (only parsing). +(* Why3 goal *) +Lemma divides_spec : forall (d:Z) (n:Z), (divides d n) <-> exists q:Z, + (n = (q * d)%Z). +Proof. +intros d n. +easy. +Qed. + (* Why3 goal *) Lemma divides_refl : forall (n:Z), (divides n n). Proof. diff --git a/lib/coq/number/Parity.v b/lib/coq/number/Parity.v index f60bd4764..5403dbf6a 100644 --- a/lib/coq/number/Parity.v +++ b/lib/coq/number/Parity.v @@ -17,9 +17,6 @@ Require int.Int. Require int.Abs. Require int.ComputerDivision. -(* Why3 assumption *) -Definition unit := unit. - (* Why3 assumption *) Definition even (n:Z): Prop := exists k:Z, (n = (2%Z * k)%Z). diff --git a/lib/coq/option/Option.v b/lib/coq/option/Option.v index 96676ce8d..9cc341538 100644 --- a/lib/coq/option/Option.v +++ b/lib/coq/option/Option.v @@ -14,7 +14,25 @@ Require Import BuiltIn. Require BuiltIn. +(* Why3 assumption *) +Definition is_none {a:Type} {a_WT:WhyType a} (o:(option a)): Prop := + match o with + | Init.Datatypes.None => True + | (Init.Datatypes.Some _) => False + end. + +(* Why3 goal *) +Lemma is_none_spec : forall {a:Type} {a_WT:WhyType a}, forall (o:(option a)), + (is_none o) <-> (o = Init.Datatypes.None). +Proof. +intros a a_WT o. +split. +now destruct o. +now intros ->. +Qed. + Global Instance option_WhyType : forall T {T_WT : WhyType T}, WhyType (option T). +Proof. split. apply @None. intros [x|] [y|] ; try (now right) ; try (now left). diff --git a/lib/coq/real/Real.v b/lib/coq/real/Real.v index a761d215a..69407d722 100644 --- a/lib/coq/real/Real.v +++ b/lib/coq/real/Real.v @@ -15,22 +15,23 @@ Require Import BuiltIn. Require BuiltIn. (* Why3 comment *) -(* infix_ls is replaced with (x < x1)%R by the coq driver *) - -(* Why3 goal *) -Lemma infix_lseq_def : forall (x:R) (y:R), (x <= y)%R <-> ((x < y)%R \/ - (x = y)). -reflexivity. -Qed. +(* prefix_mn is replaced with (-x)%R by the coq driver *) (* Why3 comment *) (* infix_pl is replaced with (x + x1)%R by the coq driver *) (* Why3 comment *) -(* prefix_mn is replaced with (-x)%R by the coq driver *) +(* infix_as is replaced with (x * x1)%R by the coq driver *) (* Why3 comment *) -(* infix_as is replaced with (x * x1)%R by the coq driver *) +(* infix_ls is replaced with (x < x1)%R by the coq driver *) + +(* Why3 goal *) +Lemma infix_lseq_def : forall (x:R) (y:R), (x <= y)%R <-> ((x < y)%R \/ + (x = y)). +Proof. +reflexivity. +Qed. (* Why3 goal *) Lemma Assoc : forall (x:R) (y:R) (z:R), @@ -92,11 +93,6 @@ intros x y z. apply Rmult_plus_distr_r. Qed. -(* Why3 goal *) -Lemma infix_mn_def : forall (x:R) (y:R), ((x - y)%R = (x + (-y)%R)%R). -reflexivity. -Qed. - (* Why3 goal *) Lemma Comm1 : forall (x:R) (y:R), ((x * y)%R = (y * x)%R). Proof. @@ -122,12 +118,20 @@ Qed. (* Why3 goal *) Lemma Inverse : forall (x:R), (~ (x = 0%R)) -> ((x * (Reals.Rdefinitions.Rinv x))%R = 1%R). +Proof. exact Rinv_r. Qed. +(* Why3 goal *) +Lemma infix_mn_def : forall (x:R) (y:R), ((x - y)%R = (x + (-y)%R)%R). +Proof. +reflexivity. +Qed. + (* Why3 goal *) Lemma infix_sl_def : forall (x:R) (y:R), ((x / y)%R = (x * (Reals.Rdefinitions.Rinv y))%R). +Proof. reflexivity. Qed. diff --git a/lib/coq/real/RealInfix.v b/lib/coq/real/RealInfix.v index 44ad8c0cd..c14dd8850 100644 --- a/lib/coq/real/RealInfix.v +++ b/lib/coq/real/RealInfix.v @@ -15,3 +15,10 @@ Require Import BuiltIn. Require BuiltIn. Require real.Real. +(* Why3 goal *) +Lemma infix_mndt_def : forall (x:R) (y:R), ((x - y)%R = (x + (-y)%R)%R). +Proof. +intros x y. +reflexivity. +Qed. + diff --git a/lib/coq/set/Set.v b/lib/coq/set/Set.v index 3fc141b76..0476b20c5 100644 --- a/lib/coq/set/Set.v +++ b/lib/coq/set/Set.v @@ -13,234 +13,238 @@ (* Beware! Only edit allowed sections below *) Require Import BuiltIn. Require BuiltIn. +Require HighOrd. +Require map.Map. +Require map.Const. Require Import ClassicalEpsilon. Lemma predicate_extensionality: - forall A (P Q : A -> Prop), - (forall x, P x <-> Q x) -> P = Q. + forall A (P Q : A -> bool), + (forall x, P x = Q x) -> P = Q. Admitted. -(* "it is folklore that the two together are consistent" *) -(* Why3 goal *) -Definition set : forall (a:Type), Type. -intros. -exact (a -> Prop). -Defined. +(* Why3 assumption *) +Definition set (a:Type) := (a -> bool). Global Instance set_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (set a). Proof. intros. split. -exact (fun _ => False). +exact (fun _ => false). intros x y. apply excluded_middle_informative. Qed. -(* Why3 goal *) -Definition mem: forall {a:Type} {a_WT:WhyType a}, a -> (set a) -> Prop. -intros a a_WT x s. -exact (s x). -Defined. +(* Why3 assumption *) +Definition mem {a:Type} {a_WT:WhyType a} (x:a) (s:(a -> bool)): Prop := ((s + x) = true). Hint Unfold mem. (* Why3 assumption *) -Definition infix_eqeq {a:Type} {a_WT:WhyType a} (s1:(set a)) (s2:(set - a)): Prop := forall (x:a), (mem x s1) <-> (mem x s2). +Definition infix_eqeq {a:Type} {a_WT:WhyType a} (s1:(a -> bool)) (s2:(a -> + bool)): Prop := forall (x:a), (mem x s1) <-> (mem x s2). Notation "x == y" := (infix_eqeq x y) (at level 70, no associativity). (* Why3 goal *) -Lemma extensionality : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a)) - (s2:(set a)), (infix_eqeq s1 s2) -> (s1 = s2). +Lemma extensionality : forall {a:Type} {a_WT:WhyType a}, forall (s1:(a -> + bool)) (s2:(a -> bool)), (infix_eqeq s1 s2) -> (s1 = s2). Proof. intros a a_WT s1 s2 h1. -now apply predicate_extensionality. +apply predicate_extensionality. +intros x. +generalize (h1 x). +unfold mem. +intros [h2 h3]. +destruct (s1 x). +now rewrite h2. +destruct (s2 x). +now apply h3. +easy. Qed. (* Why3 assumption *) -Definition subset {a:Type} {a_WT:WhyType a} (s1:(set a)) (s2:(set - a)): Prop := forall (x:a), (mem x s1) -> (mem x s2). +Definition subset {a:Type} {a_WT:WhyType a} (s1:(a -> bool)) (s2:(a -> + bool)): Prop := forall (x:a), (mem x s1) -> (mem x s2). (* Why3 goal *) -Lemma subset_refl : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)), +Lemma subset_refl : forall {a:Type} {a_WT:WhyType a}, forall (s:(a -> bool)), (subset s s). Proof. now intros a a_WT s x. Qed. (* Why3 goal *) -Lemma subset_trans : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a)) - (s2:(set a)) (s3:(set a)), (subset s1 s2) -> ((subset s2 s3) -> (subset s1 - s3)). +Lemma subset_trans : forall {a:Type} {a_WT:WhyType a}, forall (s1:(a -> + bool)) (s2:(a -> bool)) (s3:(a -> bool)), (subset s1 s2) -> ((subset s2 + s3) -> (subset s1 s3)). Proof. intros a a_WT s1 s2 s3 h1 h2 x H. now apply h2, h1. Qed. -(* Why3 goal *) -Definition empty: forall {a:Type} {a_WT:WhyType a}, (set a). -intros. -exact (fun _ => False). -Defined. - (* Why3 assumption *) -Definition is_empty {a:Type} {a_WT:WhyType a} (s:(set a)): Prop := +Definition is_empty {a:Type} {a_WT:WhyType a} (s:(a -> bool)): Prop := forall (x:a), ~ (mem x s). (* Why3 goal *) -Lemma empty_def1 : forall {a:Type} {a_WT:WhyType a}, (is_empty (empty : (set - a))). +Lemma mem_empty : forall {a:Type} {a_WT:WhyType a}, (is_empty + (map.Const.const false: (a -> bool))). Proof. now intros a a_WT x. Qed. (* Why3 goal *) -Lemma mem_empty : forall {a:Type} {a_WT:WhyType a}, forall (x:a), ~ (mem x - (empty : (set a))). -Proof. -now intros a a_WT x. -Qed. - -(* Why3 goal *) -Definition add: forall {a:Type} {a_WT:WhyType a}, a -> (set a) -> (set a). -intros a a_WT x s. -exact (fun y => x = y \/ s y). -Defined. - -(* Why3 goal *) -Lemma add_def1 : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a), - forall (s:(set a)), (mem x (add y s)) <-> ((x = y) \/ (mem x s)). +Lemma add_spec : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(a -> + bool)), forall (y:a), (mem y (map.Map.set s x true)) <-> ((y = x) \/ (mem y + s)). Proof. intros a a_WT x y s. -unfold add, mem; intuition. +unfold Map.set, mem. +destruct why_decidable_eq ; intuition. Qed. (* Why3 goal *) -Definition remove: forall {a:Type} {a_WT:WhyType a}, a -> (set a) -> (set a). -intros a a_WT x s. -exact (fun y => x <> y /\ s y). -Defined. - -(* Why3 goal *) -Lemma remove_def1 : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a) - (s:(set a)), (mem x (remove y s)) <-> ((~ (x = y)) /\ (mem x s)). +Lemma remove_spec : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(a -> + bool)), forall (y:a), (mem y (map.Map.set s x false)) <-> ((~ (y = x)) /\ + (mem y s)). Proof. -intros a a_WT x y s. -unfold remove, mem; intuition. +intros a a_WT x s y. +unfold Map.set, mem. +destruct why_decidable_eq ; intuition. Qed. (* Why3 goal *) -Lemma add_remove : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(set - a)), (mem x s) -> ((add x (remove x s)) = s). +Lemma add_remove : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(a -> + bool)), (mem x s) -> ((map.Map.set (map.Map.set s x false) x true) = s). Proof. intros a a_WT x s h1. apply extensionality; intro y. -rewrite add_def1. -rewrite remove_def1. +rewrite add_spec. +rewrite remove_spec. destruct (why_decidable_eq y x) as [->|H] ; intuition. Qed. (* Why3 goal *) -Lemma remove_add : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(set - a)), ((remove x (add x s)) = (remove x s)). +Lemma remove_add : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(a -> + bool)), ((map.Map.set (map.Map.set s x true) x false) = (map.Map.set s x + false)). Proof. intros a a_WT x s. apply extensionality; intro y. -rewrite remove_def1. -rewrite remove_def1. -rewrite add_def1. +rewrite remove_spec. +rewrite remove_spec. +rewrite add_spec. destruct (why_decidable_eq y x) as [->|H] ; intuition. Qed. (* Why3 goal *) -Lemma subset_remove : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(set - a)), (subset (remove x s) s). +Lemma subset_remove : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(a -> + bool)), (subset (map.Map.set s x false) s). Proof. intros a a_WT x s y. -rewrite remove_def1. +rewrite remove_spec. now intros [_ H]. Qed. (* Why3 goal *) -Definition union: forall {a:Type} {a_WT:WhyType a}, (set a) -> (set a) -> - (set a). +Definition union: forall {a:Type} {a_WT:WhyType a}, (a -> bool) -> (a -> + bool) -> (a -> bool). +Proof. intros a a_WT s1 s2. -exact (fun x => s1 x \/ s2 x). +exact (fun x => orb (s1 x) (s2 x)). Defined. (* Why3 goal *) -Lemma union_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a)) - (s2:(set a)) (x:a), (mem x (union s1 s2)) <-> ((mem x s1) \/ (mem x s2)). +Lemma union_spec : forall {a:Type} {a_WT:WhyType a}, forall (s1:(a -> bool)) + (s2:(a -> bool)), forall (x:a), (mem x (union s1 s2)) <-> ((mem x s1) \/ + (mem x s2)). Proof. -now intros a a_WT s1 s2 x. +intros a a_WT s1 s2 x. +apply Bool.orb_true_iff. Qed. (* Why3 goal *) -Definition inter: forall {a:Type} {a_WT:WhyType a}, (set a) -> (set a) -> - (set a). +Definition inter: forall {a:Type} {a_WT:WhyType a}, (a -> bool) -> (a -> + bool) -> (a -> bool). +Proof. intros a a_WT s1 s2. -exact (fun x => s1 x /\ s2 x). +exact (fun x => andb (s1 x) (s2 x)). Defined. (* Why3 goal *) -Lemma inter_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a)) - (s2:(set a)) (x:a), (mem x (inter s1 s2)) <-> ((mem x s1) /\ (mem x s2)). +Lemma inter_spec : forall {a:Type} {a_WT:WhyType a}, forall (s1:(a -> bool)) + (s2:(a -> bool)), forall (x:a), (mem x (inter s1 s2)) <-> ((mem x s1) /\ + (mem x s2)). Proof. -now intros a a_WT s1 s2 x. +intros a a_WT s1 s2 x. +apply Bool.andb_true_iff. Qed. (* Why3 goal *) -Definition diff: forall {a:Type} {a_WT:WhyType a}, (set a) -> (set a) -> (set - a). +Definition diff: forall {a:Type} {a_WT:WhyType a}, (a -> bool) -> (a -> + bool) -> (a -> bool). +Proof. intros a a_WT s1 s2. -exact (fun x => s1 x /\ ~(s2 x)). +exact (fun x => andb (s1 x) (negb (s2 x))). Defined. (* Why3 goal *) -Lemma diff_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a)) - (s2:(set a)) (x:a), (mem x (diff s1 s2)) <-> ((mem x s1) /\ ~ (mem x s2)). +Lemma diff_spec : forall {a:Type} {a_WT:WhyType a}, forall (s1:(a -> bool)) + (s2:(a -> bool)), forall (x:a), (mem x (diff s1 s2)) <-> ((mem x s1) /\ + ~ (mem x s2)). Proof. -now intros a a_WT s1 s2 x. +intros a a_WT s1 s2 x. +unfold mem, diff. +rewrite Bool.not_true_iff_false. +rewrite <- Bool.negb_true_iff. +apply Bool.andb_true_iff. Qed. (* Why3 goal *) -Lemma subset_diff : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a)) - (s2:(set a)), (subset (diff s1 s2) s1). +Lemma subset_diff : forall {a:Type} {a_WT:WhyType a}, forall (s1:(a -> bool)) + (s2:(a -> bool)), (subset (diff s1 s2) s1). Proof. intros a a_WT s1 s2 x. -rewrite diff_def1. +rewrite diff_spec. now intros [H _]. Qed. (* Why3 goal *) -Definition choose: forall {a:Type} {a_WT:WhyType a}, (set a) -> a. +Definition complement: forall {a:Type} {a_WT:WhyType a}, (a -> bool) -> (a -> + bool). +Proof. intros a a_WT s. -assert (i: inhabited a) by (apply inhabits, why_inhabitant). -exact (epsilon i (fun x => mem x s)). +exact (fun x => negb (s x)). Defined. (* Why3 goal *) -Lemma choose_def : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)), - (~ (is_empty s)) -> (mem (choose s) s). +Lemma complement_def : forall {a:Type} {a_WT:WhyType a}, forall (s:(a -> + bool)), forall (x:a), (((complement s) x) = true) <-> ~ ((s x) = true). Proof. -intros a a_WT s h. -unfold choose. -apply epsilon_spec. -now apply not_all_not_ex. +intros a a_WT s x. +unfold complement. +rewrite Bool.not_true_iff_false. +apply Bool.negb_true_iff. Qed. (* Why3 goal *) -Definition all: forall {a:Type} {a_WT:WhyType a}, (set a). -intros a a_WT. -exact (fun x => True). +Definition choose: forall {a:Type} {a_WT:WhyType a}, (a -> bool) -> a. +Proof. +intros a a_WT s. +assert (i: inhabited a) by (apply inhabits, why_inhabitant). +exact (epsilon i (fun x => mem x s)). Defined. (* Why3 goal *) -Lemma all_def : forall {a:Type} {a_WT:WhyType a}, forall (x:a), (mem x - (all : (set a))). +Lemma choose_spec : forall {a:Type} {a_WT:WhyType a}, forall (s:(a -> bool)), + (~ (is_empty s)) -> (mem (choose s) s). Proof. -now intros a a_WT x. +intros a a_WT s h1. +unfold choose. +apply epsilon_spec. +now apply not_all_not_ex. Qed. -- GitLab