helm/software/matita/library/didactic/exercises/natural_deduction_fst_order.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 (*DOCBEGIN
  19
  20 I connettivi logici
  21 ===================
  22
  23 Per digitare i connettivi logici:
  24
  25 * `∧` : `\land`
  26 * `∨` : `\lor`
  27 * `¬` : `\lnot`
  28 * `⇒` : `=>`, `\Rightarrow`
  29 * `⊥` : `\bot`
  30 * `⊤` : `\top`
  31
  32 Per digitare i quantificatori:
  33
  34 * `∀` : `\forall`
  35 * `∃` : `\exists`
  36
  37 I termini, le formule e i nomi delle ipotesi
  38 ============================================
  39
  40 * I termini quantificati da `∀` e `∃`, quando argomenti di
  41   una regola, vengono scritti tra `{` e `}`.
  42
  43 * Le formule, quando argomenti di
  44   una regola, vengono scritti tra `(` e `)`.
  45
  46 * I nomi delle ipotesi, quando argomenti di
  47   una regola, vengono scritti tra `[` e `]`.
  48
  49
  50 DOCEND*)
  51
  52
  53 include "didactic/support/natural_deduction.ma".
  54
  55 theorem pippo : (∀x.P (f x) ∧ Q x) ⇒ (∃x.Q x) ⇒ ∃y.P y.
  56 apply rule (prove ((∀x.P (f x) ∧ Q x) ⇒ (∃x.Q x) ⇒ ∃y.P y));
  57 (*BEGIN*)
  58 apply rule (⇒_i [h1] ((∃x.Q x) ⇒ ∃y.P y));
  59 apply rule (⇒_i [h2] (∃y.P y));
  60 apply rule (∃_e (∃x.Q x) {t} [h3] (∃y.P y));
  61   [ apply rule (discharge [h2]);
  62   | apply rule (let ft ≝ (f t) in ∃_i {ft} (P ft));
  63     apply rule (∧_e_l (P (f t) ∧ Q t));
  64     apply rule (∀_e {t} (∀x.P (f x) ∧ Q x));
  65     apply rule (discharge [h1]);
  66   ]
  67 (*END*)
  68 qed.