From d21fa51e8a39d364bc6a4fabb5c32e5f91db8c7b Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 4 Dec 2012 10:40:10 +0100 Subject: [PATCH] Introduce the concept of decidable equality into Coq realizations. --- lib/coq/BuiltIn.v | 36 ++++++++++++++++++++++++++++++++++-- lib/coq/set/Set.v | 5 ++++- 2 files changed, 38 insertions(+), 3 deletions(-) diff --git a/lib/coq/BuiltIn.v b/lib/coq/BuiltIn.v index 8d1e2ee1e..55e81e976 100644 --- a/lib/coq/BuiltIn.v +++ b/lib/coq/BuiltIn.v @@ -1,28 +1,60 @@ Require Export ZArith. Require Export Rbase. -Class WhyType T := why_inhabitant : T. +Class WhyType T := { + why_inhabitant : T ; + why_decidable_eq : forall x y : T, { x = y } + { x <> y } +}. Notation int := Z. Global Instance int_WhyType : WhyType int. +Proof. +split. exact Z0. +exact Z_eq_dec. Qed. Notation real := R. Global Instance real_WhyType : WhyType real. +Proof. +split. exact R0. +intros x y. +destruct (total_order_T x y) as [[H|H]|H] ; + try (left ; exact H) ; right. +now apply Rlt_not_eq. +now apply Rgt_not_eq. Qed. Global Instance tuple_WhyType : forall T {T' : WhyType T} U {U' : WhyType U}, WhyType (T * U). -now split. +Proof. +intros T WT U WU. +split. +split ; apply why_inhabitant. +intros (x1,x2) (y1,y2). +destruct (why_decidable_eq x1 y1) as [H1|H1]. +destruct (why_decidable_eq x2 y2) as [H2|H2]. +left. +now apply f_equal2. +right. +now injection. +right. +now injection. Qed. Global Instance unit_WhyType : WhyType unit. +Proof. +split. exact tt. +intros [] []. +now left. Qed. Global Instance bool_WhyType : WhyType bool. +Proof. +split. exact false. +exact Bool.bool_dec. Qed. diff --git a/lib/coq/set/Set.v b/lib/coq/set/Set.v index 9575843c4..9eb090ac6 100644 --- a/lib/coq/set/Set.v +++ b/lib/coq/set/Set.v @@ -20,7 +20,10 @@ Defined. Global Instance set_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (set a). Proof. intros. +split. exact (fun _ => False). +intros x y. +apply excluded_middle_informative. Qed. (* Why3 goal *) @@ -176,7 +179,7 @@ Qed. (* Why3 goal *) Definition choose: forall {a:Type} {a_WT:WhyType a}, (set a) -> a. intros a a_WT s. -assert (i: inhabited a) by (apply inhabits; assumption). +assert (i: inhabited a) by (apply inhabits, why_inhabitant). exact (epsilon i (fun x => mem x s)). Defined. -- GitLab