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 "sets/setoids1.ma".
17 ndefinition CPROP: setoid1.
20 | napply (mk_equivalence_relation1 CProp[0])
22 | #x; napply mk_iff; #H; nassumption
23 | #x; #y; *; #H1; #H2; napply mk_iff; nassumption
24 | #x; #y; #z; *; #H1; #H2; *; #H3; #H4; napply mk_iff; #w
25 [ napply (H3 (H1 w)) | napply (H2 (H4 w))]##]##]
28 unification hint 0 ((λx,y.True) (carr1 CPROP) CProp[0]).
30 (*ndefinition CProp0_of_CPROP: carr1 CPROP → CProp[0] ≝ λx.x.
31 ncoercion CProp0_of_CPROP : ∀x: carr1 CPROP. CProp[0] ≝ CProp0_of_CPROP
32 on _x: carr1 CPROP to CProp[0].*)
34 alias symbol "eq" = "setoid1 eq".
36 ndefinition fi': ∀A,B:CPROP. A = B → B → A.
37 #A; #B; #H; napply (fi … H); nassumption.
40 notation ". r" with precedence 50 for @{'fi $r}.
41 interpretation "fi" 'fi r = (fi' ?? r).
43 ndefinition and_morphism: binary_morphism1 CPROP CPROP CPROP.
44 napply mk_binary_morphism1
46 | #a; #a'; #b; #b'; *; #H1; #H2; *; #H3; #H4; napply mk_iff; *; #K1; #K2; napply conj
53 unification hint 0 (∀A,B.(λx,y.True) (fun21 ??? and_morphism A B) (And A B)).
55 (*nlemma test: ∀A,A',B: CProp[0]. A=A' → (B ∨ A) = B → (B ∧ A) ∧ B.
56 #A; #A'; #B; #H1; #H2;
57 napply (. ((#‡H1)‡H2^-1)); nnormalize;
60 (*interpretation "and_morphism" 'and a b = (fun21 ??? and_morphism a b).*)
62 ndefinition or_morphism: binary_morphism1 CPROP CPROP CPROP.
63 napply mk_binary_morphism1
65 | #a; #a'; #b; #b'; *; #H1; #H2; *; #H3; #H4; napply mk_iff; *; #H;
66 ##[##1,3: napply or_introl |##*: napply or_intror ]
73 unification hint 0 (∀A,B.(λx,y.True) (fun21 ??? or_morphism A B) (Or A B)).
75 (*interpretation "or_morphism" 'or a b = (fun21 ??? or_morphism a b).*)
77 ndefinition if_morphism: binary_morphism1 CPROP CPROP CPROP.
78 napply mk_binary_morphism1
79 [ napply (λA,B. A → B)
80 | #a; #a'; #b; #b'; #H1; #H2; napply mk_iff; #H; #w
81 [ napply (if … H2); napply H; napply (fi … H1); nassumption
82 | napply (fi … H2); napply H; napply (if … H1); nassumption]##]