| 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 | notation "⊥" with precedence 90 |
|---|
| 34 | for @{ match ? in False with [ ] }. |
|---|
| 35 | |
|---|
| 36 | interpretation "logical not" 'not x = (Not x). |
|---|
| 37 | |
|---|
| 38 | ntheorem absurd : ∀ A:Prop. A → ¬A → False. |
|---|
| 39 | #A; #H; #Hn; nelim Hn;/2/; nqed. |
|---|
| 40 | |
|---|
| 41 | (* |
|---|
| 42 | ntheorem absurd : ∀ A,C:Prop. A → ¬A → C. |
|---|
| 43 | #A; #C; #H; #Hn; nelim (Hn H). |
|---|
| 44 | nqed. *) |
|---|
| 45 | |
|---|
| 46 | ntheorem not_to_not : ∀A,B:Prop. (A → B) → ¬B →¬A. |
|---|
| 47 | /4/; nqed. |
|---|
| 48 | |
|---|
| 49 | ninductive And (A,B:Prop) : Prop ≝ |
|---|
| 50 | conj : A → B → And A B. |
|---|
| 51 | |
|---|
| 52 | interpretation "logical and" 'and x y = (And x y). |
|---|
| 53 | |
|---|
| 54 | ntheorem proj1: ∀A,B:Prop. A ∧ B → A. |
|---|
| 55 | #A; #B; #AB; nelim AB; //. |
|---|
| 56 | nqed. |
|---|
| 57 | |
|---|
| 58 | ntheorem proj2: ∀ A,B:Prop. A ∧ B → B. |
|---|
| 59 | #A; #B; #AB; nelim AB; //. |
|---|
| 60 | nqed. |
|---|
| 61 | |
|---|
| 62 | ninductive Or (A,B:Prop) : Prop ≝ |
|---|
| 63 | or_introl : A → (Or A B) |
|---|
| 64 | | or_intror : B → (Or A B). |
|---|
| 65 | |
|---|
| 66 | interpretation "logical or" 'or x y = (Or x y). |
|---|
| 67 | |
|---|
| 68 | ndefinition decidable : Prop → Prop ≝ |
|---|
| 69 | λ A:Prop. A ∨ ¬ A. |
|---|
| 70 | |
|---|
| 71 | ninductive ex (A:Type[0]) (P:A → Prop) : Prop ≝ |
|---|
| 72 | ex_intro: ∀ x:A. P x → ex A P. |
|---|
| 73 | |
|---|
| 74 | interpretation "exists" 'exists x = (ex ? x). |
|---|
| 75 | |
|---|
| 76 | ninductive ex2 (A:Type[0]) (P,Q:A \to Prop) : Prop ≝ |
|---|
| 77 | ex_intro2: ∀ x:A. P x → Q x → ex2 A P Q. |
|---|
| 78 | |
|---|
| 79 | ndefinition iff := |
|---|
| 80 | λ A,B. (A → B) ∧ (B → A). |
|---|
| 81 | |
|---|
| 82 | interpretation "iff" 'iff a b = (iff a b). |
|---|
