Last change
on this file since 2200 was
1635,
checked in by tranquil, 10 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  

1  include "hints_declaration.ma". 

2  include "basics/types.ma". 

3  include "basics/relations.ma". 

4  

5  record 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  

13  definition 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  

19  interpretation "setoid equality" 'std_eq x y = (std_eq ? x y). 

20  

21  notation "x ≅ y" with precedence 45 for @{'std_eq $x $y}. 

22  

23  definition 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  (* 

32  interpretation "Setoid Product" 'product X Y = (std_pair X Y). 

33  *) 

34  

35  definition 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.