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 (¬¬A) (¬A));
  28            [ apply rule (¬_i [K] (⊥)).
  29        apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
  30               [ apply rule (discharge [H]).
  31               | apply rule (∨_i_r (¬A)).
  32           apply rule (discharge [K]).
  33               ]
  34            | apply rule (¬_i [K] (⊥)).
  35        apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
  36               [ apply rule (discharge [H]).
  37               | apply rule (∨_i_l (A)).
  38           apply rule (discharge [K]).
  39               ]
  40            ]
  41         ]
  42 qed.
  43
  44 theorem demorgan : ¬(A ∧ B) ⇒ ¬A ∨ ¬B.
  45 apply rule (prove (¬(A ∧ B) ⇒ ¬A ∨ ¬B));
  46 apply rule (⇒_i [H] (¬A ∨ ¬B));
  47 apply rule (RAA [K] (⊥));
  48 apply rule (¬_e (¬(¬A ∨ ¬B)) (¬A ∨ ¬B));
  49         [ apply rule (discharge [K]).
  50         | apply rule (∨_i_l (¬A));
  51           apply rule (¬_i [L] (⊥)).
  52           apply rule (¬_e (¬B) (B));
  53            [ apply rule (¬_i [M] (⊥)).
  54        apply rule (¬_e (¬(A ∧ B)) (A ∧ B));
  55               [ apply rule (discharge [H]).
  56               | apply rule (∧_i (A) (B));
  57                  [ apply rule (discharge [L]).
  58                  | apply rule (discharge [M]).
  59                  ]
  60               ]
  61            | apply rule EM;
  62            ]
  63         ]