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

   1 (* Esercizio 0
   2    ===========
   3
   4    Compilare i seguenti campi:
   5
   6    Nome1: ...
   7    Cognome1: ...
   8    Matricola1: ...
   9    Account1: ...
  10
  11    Nome2: ...
  12    Cognome2: ...
  13    Matricola2: ...
  14    Account2: ...
  15
  16 *)
  17
  18
  19 include "didactic/support/natural_deduction.ma".
  20
  21 theorem EM: ∀A. A ∨ ¬ A.
  22 assume A: CProp.
  23 apply rule (prove (A ∨ ¬A));
  24 apply rule (RAA [H] (⊥)).
  25 apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
  26         [ apply rule (discharge [H]).
  27         | apply rule (⊥_e (⊥));
  28           apply rule (¬_e (¬¬A) (¬A));
  29            [ apply rule (¬_i [K] (⊥)).
  30        apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
  31               [ apply rule (discharge [H]).
  32               | apply rule (∨_i_r (¬A)).
  33           apply rule (discharge [K]).
  34               ]
  35            | apply rule (¬_i [K] (⊥)).
  36        apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
  37               [ apply rule (discharge [H]).
  38               | apply rule (∨_i_l (A)).
  39           apply rule (discharge [K]).
  40               ]
  41            ]
  42         ]
  43 qed.
  44
  45 theorem demorgan : ¬(A ∧ B) ⇒ ¬A ∨ ¬B.
  46 apply rule (prove (¬(A ∧ B) ⇒ ¬A ∨ ¬B));
  47 apply rule (⇒_i [H] (¬A ∨ ¬B));
  48 apply rule (RAA [K] (⊥));
  49 apply rule (¬_e (¬(¬A ∨ ¬B)) (¬A ∨ ¬B));
  50         [ apply rule (discharge [K]).
  51         | apply rule (∨_i_l (¬A));
  52           apply rule (¬_i [L] (⊥)).
  53           apply rule (¬_e (¬B) (B));
  54            [ apply rule (¬_i [M] (⊥)).
  55        apply rule (¬_e (¬(A ∧ B)) (A ∧ B));
  56               [ apply rule (discharge [H]).
  57               | apply rule (∧_i (A) (B));
  58                  [ apply rule (discharge [L]).
  59                  | apply rule (discharge [M]).
  60                  ]
  61               ]
  62            | apply rule (∨_e (B ∨ ¬B) [h1] (B) [h2] (B));
  63                [ apply rule (lem EM);
  64
  65
  66                | apply rule (discharge [h1]);
  67                |
  68                ]
  69
  70            apply rule (show EM);
  71            ]
  72         ]