[258] | 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 | |
---|

[260] | 15 | include "Plogic/equality.ma". |
---|

[258] | 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 | |
---|

[268] | 33 | notation "⊥" with precedence 90 |
---|

| 34 | for @{ match ? in False with [ ] }. |
---|

| 35 | |
---|

[258] | 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). |
---|