helm/software/matita/library/didactic/exercises/natural_deduction1.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 (* Istruzioni:
  16
  17      http://mowgli.cs.unibo.it/~tassi/exercise-natural_deduction.html
  18
  19 *)
  20
  21 (* Esercizio 0
  22    ===========
  23
  24    Compilare i seguenti campi:
  25
  26    Nome1: ...
  27    Cognome1: ...
  28    Matricola1: ...
  29    Account1: ...
  30
  31    Nome2: ...
  32    Cognome2: ...
  33    Matricola2: ...
  34    Account2: ...
  35
  36 *)
  37
  38 include "didactic/support/natural_deduction.ma".
  39
  40 theorem EM: ∀A:CProp. A ∨ ¬ A.
  41 assume A: CProp.
  42 apply rule (prove (A ∨ ¬A));
  43 apply rule (RAA [H] (⊥)).
  44 apply rule (¬#e (¬(A ∨ ¬A)) (A ∨ ¬A));
  45         [ apply rule (discharge [H]).
  46         | apply rule (⊥#e (⊥));
  47           apply rule (¬#e (¬¬A) (¬A));
  48            [ apply rule (¬#i [K] (⊥)).
  49        apply rule (¬#e (¬(A ∨ ¬A)) (A ∨ ¬A));
  50               [ apply rule (discharge [H]).
  51               | apply rule (∨#i_r (¬A)).
  52           apply rule (discharge [K]).
  53               ]
  54            | apply rule (¬#i [K] (⊥)).
  55        apply rule (¬#e (¬(A ∨ ¬A)) (A ∨ ¬A));
  56               [ apply rule (discharge [H]).
  57               | apply rule (∨#i_l (A)).
  58           apply rule (discharge [K]).
  59               ]
  60            ]
  61         ]
  62 qed.
  63
  64 theorem ex0 : (F∧¬G ⇒ L ⇒ E) ⇒ (G ∧ L ⇒ E) ⇒ F ∧ L ⇒ E.
  65 apply rule (prove ((F∧¬G ⇒ L ⇒ E) ⇒ (G ∧ L ⇒ E) ⇒ F ∧ L ⇒ E));
  66 (*BEGIN*)
  67 apply rule (⇒#i [h1] ((G ∧ L ⇒ E) ⇒ F ∧ L ⇒ E));
  68 apply rule (⇒#i [h2] (F ∧ L ⇒ E));
  69 apply rule (⇒#i [h3] (E));
  70 apply rule (∨#e (G∨¬G) [h4] (E) [h4] (E));
  71         [ apply rule (lem 0 EM);
  72         | apply rule (⇒#e (G∧L⇒E) (G∧L));
  73             [ apply rule (discharge [h2]);
  74             | apply rule (∧#i (G) (L));
  75                 [ apply rule (discharge [h4]);
  76                 | apply rule (∧#e_r (F∧L));
  77                   apply rule (discharge [h3]);
  78                 ]
  79             ]
  80         | apply rule (⇒#e (L⇒E) (L));
  81             [ apply rule (⇒#e (F∧¬G ⇒ L ⇒ E) (F∧¬G));
  82                 [ apply rule (discharge [h1]);
  83                 | apply rule (∧#i (F) (¬G));
  84                     [ apply rule (∧#e_l (F∧L));
  85                       apply rule (discharge [h3]);
  86                     | apply rule (discharge [h4]);
  87                     ]
  88                 ]
  89             | apply rule (∧#e_r (F∧L));
  90               apply rule (discharge [h3]);
  91             ]
  92         ]
  93 (*END*)
  94 qed.
  95
  96 theorem ex1 : (F ⇒ G∨E) ⇒ (G ⇒ ¬ (L ∧ ¬E)) ⇒ (¬L ∨ F) ⇒ L ⇒ E.
  97 apply rule (prove (F ⇒ G∨E) ⇒ (G ⇒ ¬ (L ∧ ¬E)) ⇒ (¬L ∨ F) ⇒ L ⇒ E);
  98 (*BEGIN*)
  99 apply rule (⇒#i [h1] ((G ⇒ ¬ (L ∧ ¬E)) ⇒ (¬L ∨ F) ⇒ L ⇒ E));
 100 apply rule (⇒#i [h2] ((¬L ∨ F) ⇒ L ⇒ E));
 101 apply rule (⇒#i [h3] (L ⇒ E));
 102 apply rule (⇒#i [h4] (E));
 103 apply rule (∨#e (¬L∨F) [h5] (E) [h5] (E));
 104         [ apply rule (discharge [h3]);
 105         | apply rule (⊥#e (⊥));
 106     apply rule (¬#e (¬L) (L));
 107             [ apply rule (discharge [h5]);
 108             | apply rule (discharge [h4]);
 109             ]
 110         | apply rule (∨#e (G∨E) [h6] (E) [h6] (E));
 111            [ apply rule (⇒#e (F⇒G∨E) (F));
 112               [ apply rule (discharge [h1]);
 113               | apply rule (discharge [h5]);
 114               ]
 115            | apply rule (RAA [h7] (⊥));
 116        apply rule (¬#e (¬ (L ∧ ¬E)) (L ∧ ¬E));
 117                [ apply rule (⇒#e (G ⇒ ¬ (L ∧ ¬E)) (G));
 118                    [apply rule (discharge [h2]);
 119                    |apply rule (discharge [h6]);
 120                    ]
 121                | apply rule (∧#i (L) (¬E));
 122                    [ apply rule (discharge [h4]);
 123                    | apply rule (discharge [h7]);
 124                    ]
 125                ]
 126            | apply rule (discharge [h6]);
 127            ]
 128         ]
 129 (*END*)
 130 qed.
 131
 132 theorem ex2 : (F∧G ⇒ E) ⇒ (H ⇒ E∨F) ⇒ (¬G ⇒ ¬H) ⇒ H ⇒ E.
 133 apply rule (prove ((F∧G ⇒ E) ⇒ (H ⇒ E∨F) ⇒ (¬G ⇒ ¬H) ⇒ H ⇒ E));
 134 (*BEGIN*)
 135 apply rule (⇒#i [h1] ((H ⇒ E∨F) ⇒ (¬G ⇒ ¬H) ⇒ H ⇒ E));
 136 apply rule (⇒#i [h2] ((¬G ⇒ ¬H) ⇒ H ⇒ E));
 137 apply rule (⇒#i [h3] (H ⇒ E));
 138 apply rule (⇒#i [h4] (E));
 139 apply rule (∨#e (G∨¬G) [h5] (E) [h5] (E));
 140         [apply rule (lem 0 EM);
 141         | apply rule (∨#e (E∨F) [h6] (E) [h6] (E));
 142            [ apply rule (⇒#e (H ⇒ E∨F) (H));
 143                [ apply rule (discharge [h2]);
 144                | apply rule (discharge [h4]);
 145                ]
 146            | apply rule (discharge [h6]);
 147            | apply rule (⇒#e (F∧G ⇒ E) (F∧G));
 148               [apply rule (discharge [h1]);
 149               |apply rule (∧#i (F) (G));
 150                 [ apply rule (discharge [h6]);
 151                 | apply rule (discharge [h5]);
 152                 ]
 153               ]
 154            ]
 155         | apply rule (⊥#e (⊥));
 156     apply rule (¬#e (¬H) (H));
 157         [ apply rule (⇒#e (¬G ⇒ ¬H) (¬G));
 158                [ apply rule (discharge [h3]);
 159                | apply rule (discharge [h5]);
 160                ]
 161             | apply rule (discharge [h4]);
 162             ]
 163         ]
 164 (*END*)
 165 qed.
 166
 167 theorem ex3 : (F∧G ⇒ E) ⇒ (¬E ⇒ G∨¬L) ⇒ (L ⇒ F) ⇒ L ⇒ E.
 168 apply rule (prove ((F∧G ⇒ E) ⇒ (¬E ⇒ G∨¬L) ⇒ (L ⇒ F) ⇒ L ⇒ E)).
 169 (*BEGIN*)
 170 apply rule (⇒#i [h1] ((¬E ⇒ G∨¬L) ⇒ (L ⇒ F) ⇒ L ⇒ E));
 171 apply rule (⇒#i [h2] ((L ⇒ F) ⇒ L ⇒ E));
 172 apply rule (⇒#i [h3] (L ⇒ E));
 173 apply rule (⇒#i [h4] (E));
 174 apply rule (RAA [h5] (⊥));
 175 apply rule (∨#e (G∨¬L) [h6] (⊥) [h6] (⊥));
 176         [ apply rule (⇒#e (¬E ⇒ G∨¬L) (¬E));
 177             [ apply rule (discharge [h2]);
 178             | apply rule (discharge [h5]);
 179             ]
 180         | apply rule (¬#e (¬E) (E));
 181         [ apply rule (discharge [h5]);
 182             | apply rule (⇒#e (F∧G ⇒ E) (F∧G));
 183                [ apply rule (discharge [h1]);
 184                | apply rule (∧#i (F) (G));
 185                    [ apply rule (⇒#e (L⇒F) (L));
 186                       [ apply rule (discharge [h3]);
 187                       | apply rule (discharge [h4]);
 188                       ]
 189                    | apply rule (discharge [h6]);
 190                    ]
 191                ]
 192             ]
 193         | apply rule (¬#e (¬L) (L));
 194             [ apply rule (discharge [h6]);
 195             | apply rule (discharge [h4]);
 196             ]
 197         ]
 198 (*END*)
 199 qed.