1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 include "Plogic/equality.ma".
17 ninductive True: Prop ≝
20 default "true" cic:/matita/basics/connectives/True.ind.
22 ninductive False: Prop ≝ .
24 default "false" cic:/matita/basics/connectives/False.ind.
27 ndefinition Not: Prop → Prop ≝
30 ninductive Not (A:Prop): Prop ≝
31 nmk: (A → False) → Not A.
35 interpretation "logical not" 'not x = (Not x).
37 ntheorem absurd : ∀ A:Prop. A → ¬A → False.
38 #A; #H; #Hn; nelim Hn;/2/; nqed.
41 ntheorem absurd : ∀ A,C:Prop. A → ¬A → C.
42 #A; #C; #H; #Hn; nelim (Hn H).
45 ntheorem not_to_not : ∀A,B:Prop. (A → B) → ¬B →¬A.
48 ninductive And (A,B:Prop) : Prop ≝
49 conj : A → B → And A B.
51 interpretation "logical and" 'and x y = (And x y).
53 ntheorem proj1: ∀A,B:Prop. A ∧ B → A.
54 #A; #B; #AB; nelim AB; //.
57 ntheorem proj2: ∀ A,B:Prop. A ∧ B → B.
58 #A; #B; #AB; nelim AB; //.
61 ninductive Or (A,B:Prop) : Prop ≝
62 or_introl : A → (Or A B)
63 | or_intror : B → (Or A B).
65 interpretation "logical or" 'or x y = (Or x y).
67 ndefinition decidable : Prop → Prop ≝
70 ninductive ex (A:Type[0]) (P:A → Prop) : Prop ≝
71 ex_intro: ∀ x:A. P x → ex A P.
73 interpretation "exists" 'exists x = (ex ? x).
75 ninductive ex2 (A:Type[0]) (P,Q:A \to Prop) : Prop ≝
76 ex_intro2: ∀ x:A. P x → Q x → ex2 A P Q.
79 λ A,B. (A → B) ∧ (B → A).