# hub.darcs.net :: rdockins -> domains -> files

A Coq library for domain theory

## root / basics.v

 ```1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 ``` ``````(* Copyright (c) 2014, Robert Dockins *) Require Import Setoid. Require Export notations. (** * Setoids and equality. This module introduces setoids, which consist of a type packaged together with an equivalence relation. We roughly follow the techniques described in the paper _Packaging Mathematical Structures_ by Garillot et al. (TPHOLS 2009). The mainstay of this technique is using canonoical structures to automatically infer structures given the carrier type. We use the symbol ≈ to indicate the equality relation on setoids. For the vast majority of this development, ≈ will be the notion of equivalence of interest. *) Delimit Scope equiv_scope with eq. Open Scope equiv_scope. Module Eq. Record mixin_of (T:Type) := Mixin { eq : T -> T -> Prop ; refl : forall x, eq x x ; symm : forall x y, eq x y -> eq y x ; trans : forall x y z, eq x y -> eq y z -> eq x z }. Structure type : Type := Pack { carrier :> Type ; mixin : mixin_of carrier }. End Eq. Definition eq_op T := Eq.eq _ (Eq.mixin T). Notation "x ≈ y" := (@eq_op _ x y) : equiv_scope. Notation "x ≉ y" := (~(@eq_op _ x y)) : equiv_scope. Coercion Eq.carrier : Eq.type >-> Sortclass. Lemma eq_refl : forall (T:Eq.type) (x:T), x ≈ x. Proof. intros. destruct T. destruct mixin. apply refl. Qed. Lemma eq_trans : forall (T:Eq.type) (x y z:T), x ≈ y -> y ≈ z -> x ≈ z. Proof. intros. destruct T. destruct mixin. eapply trans; eauto. Qed. Lemma eq_symm : forall (T:Eq.type) (x y:T), x ≈ y -> y ≈ x. Proof. intros. destruct T. destruct mixin. eapply symm; eauto. Qed. Hint Resolve eq_refl eq_symm eq_trans. Add Parametric Relation (T:Eq.type) : (Eq.carrier T) (@eq_op T) reflexivity proved by (@eq_refl T) symmetry proved by (@eq_symm T) transitivity proved by (@eq_trans T) as eq_op_rel. Record eq_dec (T:Eq.type) := EqDec { eqdec :> forall x y:T, {x ≈ y}+{x ≉ y} }. Arguments eqdec [T] [e] x y.``````