]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/nlibrary/Plogic/connectives.ma
bf17771fb9890a632f0f49f2b8e223837712f36a
[helm.git] / matita / matita / nlibrary / Plogic / 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 "Plogic/equality.ma".
16
17 ninductive True: Prop ≝  
18 I : True.
19
20 default "true" cic:/matita/basics/connectives/True.ind.
21
22 ninductive False: Prop ≝ .
23
24 default "false" cic:/matita/basics/connectives/False.ind.
25
26 (*
27 ndefinition Not: Prop → Prop ≝
28 λA. A → False. *)
29
30 ninductive Not (A:Prop): Prop ≝
31 nmk: (A → False) → Not A.
32
33 interpretation "logical not" 'not x = (Not x).
34
35 ntheorem absurd : ∀ A:Prop. A → ¬A → False.
36 #A; #H; #Hn; nelim Hn;/2/; nqed.
37
38 (*
39 ntheorem absurd : ∀ A,C:Prop. A → ¬A → C.
40 #A; #C; #H; #Hn; nelim (Hn H).
41 nqed. *)
42
43 ntheorem not_to_not : ∀A,B:Prop. (A → B) → ¬B →¬A.
44 /4/; nqed.
45
46 ninductive And (A,B:Prop) : Prop ≝
47     conj : A → B → And A B.
48
49 interpretation "logical and" 'and x y = (And x y).
50
51 ntheorem proj1: ∀A,B:Prop. A ∧ B → A.
52 #A; #B; #AB; nelim AB; //.
53 nqed.
54
55 ntheorem proj2: ∀ A,B:Prop. A ∧ B → B.
56 #A; #B; #AB; nelim AB; //.
57 nqed.
58
59 ninductive Or (A,B:Prop) : Prop ≝
60      or_introl : A → (Or A B)
61    | or_intror : B → (Or A B).
62
63 interpretation "logical or" 'or x y = (Or x y).
64
65 ndefinition decidable : Prop → Prop ≝ 
66 λ A:Prop. A ∨ ¬ A.
67
68 ninductive ex (A:Type[0]) (P:A → Prop) : Prop ≝
69     ex_intro: ∀ x:A. P x →  ex A P.
70     
71 interpretation "exists" 'exists x = (ex ? x).
72
73 ninductive ex2 (A:Type[0]) (P,Q:A \to Prop) : Prop ≝
74     ex_intro2: ∀ x:A. P x → Q x → ex2 A P Q.
75
76 ndefinition iff :=
77  λ A,B. (A → B) ∧ (B → A).
78
79 interpretation "iff" 'iff a b = (iff a b).