Commit d21fa51e authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Introduce the concept of decidable equality into Coq realizations.

parent 86385555
Require Export ZArith. Require Export ZArith.
Require Export Rbase. 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. Notation int := Z.
Global Instance int_WhyType : WhyType int. Global Instance int_WhyType : WhyType int.
Proof.
split.
exact Z0. exact Z0.
exact Z_eq_dec.
Qed. Qed.
Notation real := R. Notation real := R.
Global Instance real_WhyType : WhyType real. Global Instance real_WhyType : WhyType real.
Proof.
split.
exact R0. 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. Qed.
Global Instance tuple_WhyType : forall T {T' : WhyType T} U {U' : WhyType U}, WhyType (T * U). 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. Qed.
Global Instance unit_WhyType : WhyType unit. Global Instance unit_WhyType : WhyType unit.
Proof.
split.
exact tt. exact tt.
intros [] [].
now left.
Qed. Qed.
Global Instance bool_WhyType : WhyType bool. Global Instance bool_WhyType : WhyType bool.
Proof.
split.
exact false. exact false.
exact Bool.bool_dec.
Qed. Qed.
...@@ -20,7 +20,10 @@ Defined. ...@@ -20,7 +20,10 @@ Defined.
Global Instance set_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (set a). Global Instance set_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (set a).
Proof. Proof.
intros. intros.
split.
exact (fun _ => False). exact (fun _ => False).
intros x y.
apply excluded_middle_informative.
Qed. Qed.
(* Why3 goal *) (* Why3 goal *)
...@@ -176,7 +179,7 @@ Qed. ...@@ -176,7 +179,7 @@ Qed.
(* Why3 goal *) (* Why3 goal *)
Definition choose: forall {a:Type} {a_WT:WhyType a}, (set a) -> a. Definition choose: forall {a:Type} {a_WT:WhyType a}, (set a) -> a.
intros a a_WT s. 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)). exact (epsilon i (fun x => mem x s)).
Defined. Defined.
......
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