(**************************************************************************) (* ___ *) (* ||M|| *) (* ||A|| A project by Andrea Asperti *) (* ||T|| *) (* ||I|| Developers: *) (* ||T|| A.Asperti, C.Sacerdoti Coen, *) (* ||A|| E.Tassi, S.Zacchiroli *) (* \ / *) (* \ / This file is distributed under the terms of the *) (* v GNU Lesser General Public License Version 2.1 *) (* *) (**************************************************************************) include "Plogic/equality.ma". ninductive True: Prop ≝ I : True. default "true" cic:/matita/basics/connectives/True.ind. ninductive False: Prop ≝ . default "false" cic:/matita/basics/connectives/False.ind. (* ndefinition Not: Prop → Prop ≝ λA. A → False. *) ninductive Not (A:Prop): Prop ≝ nmk: (A → False) → Not A. notation "⊥" with precedence 90 for @{ match ? in False with [ ] }. interpretation "logical not" 'not x = (Not x). ntheorem absurd : ∀ A:Prop. A → ¬A → False. #A; #H; #Hn; nelim Hn;/2/; nqed. (* ntheorem absurd : ∀ A,C:Prop. A → ¬A → C. #A; #C; #H; #Hn; nelim (Hn H). nqed. *) ntheorem not_to_not : ∀A,B:Prop. (A → B) → ¬B →¬A. /4/; nqed. ninductive And (A,B:Prop) : Prop ≝ conj : A → B → And A B. interpretation "logical and" 'and x y = (And x y). ntheorem proj1: ∀A,B:Prop. A ∧ B → A. #A; #B; #AB; nelim AB; //. nqed. ntheorem proj2: ∀ A,B:Prop. A ∧ B → B. #A; #B; #AB; nelim AB; //. nqed. ninductive Or (A,B:Prop) : Prop ≝ or_introl : A → (Or A B) | or_intror : B → (Or A B). interpretation "logical or" 'or x y = (Or x y). ndefinition decidable : Prop → Prop ≝ λ A:Prop. A ∨ ¬ A. ninductive ex (A:Type[0]) (P:A → Prop) : Prop ≝ ex_intro: ∀ x:A. P x → ex A P. interpretation "exists" 'exists x = (ex ? x). ninductive ex2 (A:Type[0]) (P,Q:A \to Prop) : Prop ≝ ex_intro2: ∀ x:A. P x → Q x → ex2 A P Q. ndefinition iff := λ A,B. (A → B) ∧ (B → A). interpretation "iff" 'iff a b = (iff a b).