source: src/utilities/setoids.ma @ 2896

Last change on this file since 2896 was 1635, checked in by tranquil, 8 years ago
  • lists with binders and monads
  • Joint.ma and other temprarily forked, awaiting feedback from Claudio
  • translation of RTLabs → RTL refactored with new tools
File size: 1.4 KB
Line 
1include "hints_declaration.ma".
2include "basics/types.ma".
3include "basics/relations.ma".
4
5record Setoid : Type[1] ≝ {
6  std_supp :> Type[0] ;
7  std_eq : relation std_supp;
8  std_refl : reflexive ? std_eq;
9  std_trans : transitive ? std_eq;
10  std_symm : symmetric ? std_eq
11}.
12
13definition as_std : Type[0] → Setoid ≝
14  λT.mk_Setoid T (eq T) (refl T) (trans_eq T) (sym_eq T).
15
16(* coercion setoid_from_set nocomposites:
17  ∀t : Type[0].Setoid ≝ set_to_setoid on _t : Type[0] to Setoid.*)
18
19interpretation "setoid equality" 'std_eq x y = (std_eq ? x y).
20
21notation "x ≅ y" with precedence 45 for @{'std_eq $x $y}.
22
23definition std_prod ≝ λX,Y : Setoid.mk_Setoid (X×Y)
24  (λp,q. 'pi1 p ≅ 'pi1 q ∧ 'pi2 p ≅ 'pi2 q) ???./2/
25[(* transitivity *)
26  *#p1#p2*#q1#q2*#r1#r2*#H1#H2*#H3#H4 %/2/
27|(* symmetry *)
28  *#p1#p2*#q1#q2*#H1#H2%/2/
29]qed.
30
31(*
32interpretation "Setoid Product" 'product X Y = (std_pair X Y).
33*)
34
35definition std_union ≝ λX,Y : Setoid.mk_Setoid (X+Y)
36  (λp,q. match p with
37    [inl x ⇒ match q with
38      [ inl y ⇒ x ≅ y
39      | _ ⇒ False
40      ]
41    |inr x ⇒ match q with
42      [ inr y ⇒ x ≅ y
43      | _ ⇒ False
44      ]
45    ]) ???.
46[(* reflexivity *)
47  *#x normalize //
48|
49  (* transitivity *)
50  *#x normalize *#y normalize *#z normalize /2/ #F elim F
51|(* symmetry *)
52  *#x normalize *#y normalize /2/
53]qed.
54
55(* interpretation "setoid union" 'plus X Y = (std_union X Y). *)
56
Note: See TracBrowser for help on using the repository browser.