helm/software/matita/library/didactic/exercises/natural_deduction1.ma

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