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: unary_morphism1 CPROP (unary_morphism1_setoid1 CPROP CPROP).
46 napply (mk_binary_morphism1 … And);
47 #a; #a'; #b; #b'; #Ha; #Hb; @; *; #x; #y; @
48 [ napply (. Ha^-1) | napply (. Hb^-1) | napply (. Ha) | napply (. Hb)] //.
51 unification hint 0 ≔ A,B ⊢
53 (λX.mk_unary_morphism1 … (And X) (prop11 … (and_morphism X)))
54 (prop11 … and_morphism)
60 nlemma test: ∀A,A',B: CProp[0]. A=A' → (B ∨ A) = B → (B ∧ A) ∧ B.
61 #A; #A'; #B; #H1; #H2; napply (. (#‡H1)‡H2^-1); nelim daemon.
68 ndefinition or_morphism: unary_morphism1 CPROP (unary_morphism1_setoid1 CPROP CPROP).
69 napply (mk_binary_morphism1 … Or);
70 #a; #a'; #b; #b'; #Ha; #Hb; @; *; #x
71 [ @1; napply (. Ha^-1) | @2; napply (. Hb^-1) | @1; napply (. Ha) | @2; napply (. Hb)] //.
74 unification hint 0 ≔ A,B ⊢
76 (λX.mk_unary_morphism1 … (Or X) (prop11 … (or_morphism X)))
77 (prop11 … or_morphism)
80 ndefinition if_morphism: unary_morphism1 CPROP (unary_morphism1_setoid1 CPROP CPROP).
81 napply (mk_binary_morphism1 … (λA,B:CProp[0]. A → B));
82 #a; #a'; #b; #b'; #Ha; #Hb; @; #H; #x
83 [ napply (. Hb^-1); napply H; napply (. Ha) | napply (. Hb); napply H; napply (. Ha^-1)]
87 unification hint 0 ≔ A,B ⊢
89 (λX:CProp[0].mk_unary_morphism1 … (λY:CProp[0]. X → Y) (prop11 … (if_morphism X)))
90 (prop11 … if_morphism)