Last change
on this file 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  

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.