1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "logic/connectives.ma".
16 include "properties/relations.ma".
17 include "hints_declaration.ma".
20 notation "hvbox(a break = \sub \ID b)" non associative with precedence 45
23 notation > "hvbox(a break =_\ID b)" non associative with precedence 45
24 for @{ cic:/matita/logic/equality/eq.ind#xpointer(1/1) ? $a $b }.
26 interpretation "ID eq" 'eqID x y = (cic:/matita/logic/equality/eq.ind#xpointer(1/1) ? x y).
29 nrecord setoid : Type[1] ≝
31 eq: equivalence_relation carr
34 interpretation "setoid eq" 'eq t x y = (eq_rel ? (eq t) x y).
36 notation > "hvbox(a break =_0 b)" non associative with precedence 45
37 for @{ eq_rel ? (eq ?) $a $b }.
39 interpretation "setoid symmetry" 'invert r = (sym ???? r).
40 notation ".= r" with precedence 50 for @{'trans $r}.
41 interpretation "trans" 'trans r = (trans ????? r).
43 nrecord unary_morphism (A,B: setoid) : Type[0] ≝
45 prop1: ∀a,a'. eq ? a a' → eq ? (fun1 a) (fun1 a')
48 nrecord binary_morphism (A,B,C:setoid) : Type[0] ≝
50 prop2: ∀a,a',b,b'. eq ? a a' → eq ? b b' → eq ? (fun2 a b) (fun2 a' b')
53 notation "† c" with precedence 90 for @{'prop1 $c }.
54 notation "l ‡ r" with precedence 90 for @{'prop2 $l $r }.
55 notation "#" with precedence 90 for @{'refl}.
56 interpretation "prop1" 'prop1 c = (prop1 ????? c).
57 interpretation "prop2" 'prop2 l r = (prop2 ???????? l r).
58 interpretation "refl" 'refl = (refl ???).
60 ndefinition binary_morph_setoid : setoid → setoid → setoid → setoid.
61 #S1; #S2; #T; @ (binary_morphism S1 S2 T); @;
62 ##[ #f; #g; napply (∀x,y. f x y = g x y);
63 ##| #f; #x; #y; napply #;
64 ##| #f; #g; #H; #x; #y; napply ((H x y)^-1);
65 ##| #f; #g; #h; #H1; #H2; #x; #y; napply (trans … (H1 …) (H2 …)); ##]
68 ndefinition unary_morph_setoid : setoid → setoid → setoid.
69 #S1; #S2; @ (unary_morphism S1 S2); @;
70 ##[ #f; #g; napply (∀x. f x = g x);
72 ##| #f; #g; #H; #x; napply ((H x)^-1);
73 ##| #f; #g; #h; #H1; #H2; #x; napply (trans … (H1 …) (H2 …)); ##]
78 (∀o1,o2. (λx,y:Type[0].True) (carr (unary_morph_setoid o1 o2)) (unary_morphism o1 o2)).
81 ndefinition composition ≝
82 λo1,o2,o3:Type[0].λf:o2 → o3.λg: o1 → o2.λx.f (g x).
84 interpretation "function composition" 'compose f g = (composition ??? f g).
86 ndefinition comp_unary_morphisms:
88 unary_morphism o2 o3 → unary_morphism o1 o2 →
90 #o1; #o2; #o3; #f; #g; @ (f ∘ g);
91 #a; #a'; #e; nnormalize; napply (.= †(†e)); napply #.
94 unification hint 0 ≔ o1,o2,o3:setoid,f:unary_morphism o2 o3,g:unary_morphism o1 o2;
95 R ≟ (mk_unary_morphism ?? (composition … f g)
96 (prop1 ?? (comp_unary_morphisms o1 o2 o3 f g)))
97 (* -------------------------------------------------------------------- *) ⊢
98 fun1 ?? R ≡ (composition … f g).
100 ndefinition comp_binary_morphisms:
102 binary_morphism (unary_morph_setoid o2 o3) (unary_morph_setoid o1 o2)
103 (unary_morph_setoid o1 o3).
105 [ #f; #g; napply (comp_unary_morphisms … f g) (*CSC: why not ∘?*)
106 | #a; #a'; #b; #b'; #ea; #eb; #x; nnormalize;
107 napply (.= †(eb x)); napply ea.