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/cprop_connectives.ma".
17 record iff (A,B: CProp) : CProp ≝
22 notation > "hvbox(a break \liff b)"
23 left associative with precedence 25
26 notation "hvbox(a break \leftrightarrow b)"
27 left associative with precedence 25
30 interpretation "logical iff" 'iff x y = (iff x y).
32 record setoid : Type ≝
34 eq: carr → carr → CProp;
37 trans: transitive ? eq
40 definition proofs: CProp → setoid.
45 alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)".
55 record setoid1 : Type ≝
57 eq1: carr1 → carr1 → CProp;
58 refl1: reflexive ? eq1;
59 sym1: symmetric ? eq1;
60 trans1: transitive ? eq1
63 definition CCProp: setoid1.
76 cases H; cases H1; clear H H1;
83 record function_space (A,B: setoid): Type ≝
85 f_ok: ∀a,a':A. eq ? a a' → eq ? (f a) (f a')
88 notation "hbox(a break ⇒ b)" right associative with precedence 20 for @{ 'Imply $a $b }.
89 interpretation "function_space" 'Imply a b = (function_space a b).
91 record function_space1 (A: setoid) (B: setoid1): Type ≝
93 f1_ok: ∀a,a':A. eq ? a a' → eq1 ? (f1 a) (f1 a')
96 definition function_space_setoid: setoid → setoid → setoid.
101 apply (∀a:A. eq ? (f a) (f1 a));
112 apply (trans B ? (y a));
117 interpretation "function_space_setoid" 'Imply a b = (function_space_setoid a b).
119 record isomorphism (A,B: setoid): Type ≝
122 inv1: ∀a:A. eq ? (map2 (map1 a)) a;
123 inv2: ∀b:B. eq ? (map1 (map2 b)) b
126 interpretation "isomorphism" 'iff x y = (isomorphism x y).
130 definition setoids: setoid1.
137 [1,3: intro; assumption;
138 |*: intros; assumption]
146 record dependent_product (A:setoid) (B: function_space1 A setoids): Type ≝
147 { dp:> ∀a:A.carr (B a);
148 dp_ok: ∀a,a':A. ∀p:eq ? a a'. eq ? (dp a) (map2 ?? (f1_ok ?? B ?? p) (dp a'))
151 record forall (A:setoid) (B: function_space1 A CCProp): Type ≝
152 { fo:> ∀a:A.proofs (B a)
155 record subset (A: setoid) : Type ≝
156 { mem: function_space1 A CCProp
159 definition subset_eq ≝ λA:setoid.λU,V: subset A. ∀a:A. mem ? U a \liff mem ? V a.
162 ∀A:setoid.∀a,a':A.∀U,V: subset A.
163 eq ? a a' → subset_eq ? U V → mem ? U a \liff mem ? V a'.
167 [ lapply (H2 H4); clear H2 H3 H4;
168 apply (if ?? (f1_ok ?? (mem ? V) ?? H));
170 | apply H3; clear H2 H3;
171 apply (fi ?? (f1_ok ?? (mem ? V) ?? H));