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