]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/nlibrary/logic/connectives.ma
- we introduce stratified term equivalence to remove the parameter g from cpx
[helm.git] / matita / matita / nlibrary / logic / connectives.ma
1 (**************************************************************************)
2 (*       ___                                                                *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU Lesser General Public License Version 2.1         *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "logic/pts.ma".
16
17 inductive True: CProp[0] ≝
18   I : True.
19
20 inductive False: CProp[0] ≝.
21
22 definition Not: CProp[0] → CProp[0] ≝
23   λA. A → False.
24
25 interpretation "logical ot" 'not x = (Not x).
26
27 inductive And (A,B:CProp[0]) : CProp[0] ≝
28     conj : A → B → And A B.
29
30 interpretation "logical and" 'and x y = (And x y).
31
32 inductive Or (A,B:CProp[0]) : CProp[0] ≝
33      or_introl : A → Or A B
34    | or_intror : B → Or A B.
35
36 interpretation "logical or" 'or x y = (Or x y).
37
38 inductive Ex (A:Type[0]) (P:A → CProp[0]) : CProp[0] ≝
39     ex_intro: ∀x:A. P x → Ex A P.
40
41
42 inductive Ex1 (A:Type[1]) (P:A → CProp[0]) : CProp[1] ≝
43     ex_intro1: ∀x:A. P x → Ex1 A P.
44
45 interpretation "exists1" 'exists x = (Ex1 ? x).
46 interpretation "exists" 'exists x = (Ex ? x).
47
48 inductive sigma (A : Type[0]) (P : A → CProp[0]) : Type[0] ≝ 
49  sig_intro : ∀x:A.P x → sigma A P. 
50
51 interpretation "sigma" 'sigma \eta.p = (sigma ? p). 
52
53 record iff (A,B: CProp[0]) : CProp[0] ≝
54  { if: A → B;
55    fi: B → A
56  }.
57
58 notation > "hvbox(a break \liff b)"
59   left associative with precedence 25
60 for @{ 'iff $a $b }.
61
62 notation "hvbox(a break \leftrightarrow b)"
63   left associative with precedence 25
64 for @{ 'iff $a $b }.
65
66 interpretation "logical iff" 'iff x y = (iff x y).