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 "hints_declaration.ma".
16 include "sets/setoids1.ma".
18 ndefinition CPROP: setoid1.
21 | napply (mk_equivalence_relation1 CProp[0])
23 | #x; napply mk_iff; #H; nassumption
24 | #x; #y; *; #H1; #H2; napply mk_iff; nassumption
25 | #x; #y; #z; *; #H1; #H2; *; #H3; #H4; napply mk_iff; #w
26 [ napply (H3 (H1 w)) | napply (H2 (H4 w))]##]##]
29 alias symbol "hint_decl" = "hint_decl_CProp2".
30 unification hint 0 ≔ ⊢ CProp[0] ≡ carr1 CPROP.
32 (*ndefinition CProp0_of_CPROP: carr1 CPROP → CProp[0] ≝ λx.x.
33 ncoercion CProp0_of_CPROP : ∀x: carr1 CPROP. CProp[0] ≝ CProp0_of_CPROP
34 on _x: carr1 CPROP to CProp[0].*)
36 alias symbol "eq" = "setoid1 eq".
38 ndefinition fi': ∀A,B:CPROP. A = B → B → A.
39 #A; #B; #H; napply (fi … H); nassumption.
42 notation ". r" with precedence 50 for @{'fi $r}.
43 interpretation "fi" 'fi r = (fi' ?? r).
45 ndefinition and_morphism: binary_morphism1 CPROP CPROP CPROP.
46 napply mk_binary_morphism1
48 | #a; #a'; #b; #b'; *; #H1; #H2; *; #H3; #H4; napply mk_iff; *; #K1; #K2; napply conj
55 unification hint 0 ≔ A,B ⊢ fun21 … (mk_binary_morphism1 … And (prop21 … and_morphism)) A B ≡ And A B.
57 (*nlemma test: ∀A,A',B: CProp[0]. A=A' → (B ∨ A) = B → (B ∧ A) ∧ B.
58 #A; #A'; #B; #H1; #H2;
59 napply (. ((#‡H1)‡H2^-1)); nnormalize;
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 ⊢ fun21 … (mk_binary_morphism1 … Or (prop21 … or_morphism)) A B ≡ Or A B.
75 ndefinition if_morphism: binary_morphism1 CPROP CPROP CPROP.
76 napply mk_binary_morphism1
77 [ napply (λA,B. A → B)
78 | #a; #a'; #b; #b'; #H1; #H2; napply mk_iff; #H; #w
79 [ napply (if … H2); napply H; napply (fi … H1); nassumption
80 | napply (fi … H2); napply H; napply (if … H1); nassumption]##]