From f7bfc8096055b1a8e82594b7079bad987676e639 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 1 Dec 2008 11:41:01 +0000
Subject: [PATCH] more ex and more notation

---
 .../exercises/natural_deduction_fst_order.ma  | 89 ++++++++++++++++---
 .../didactic/support/natural_deduction.ma     | 21 +++--
 2 files changed, 87 insertions(+), 23 deletions(-)

diff --git a/helm/software/matita/library/didactic/exercises/natural_deduction_fst_order.ma b/helm/software/matita/library/didactic/exercises/natural_deduction_fst_order.ma
index 0ea0c5e67..790c4b2fc 100644
--- a/helm/software/matita/library/didactic/exercises/natural_deduction_fst_order.ma
+++ b/helm/software/matita/library/didactic/exercises/natural_deduction_fst_order.ma
@@ -41,7 +41,7 @@ I termini, le formule e i nomi delle ipotesi
   una regola, vengono scritti tra `{` e `}`.
 
 * Le formule, quando argomenti di
-  una regola, vengono scritti tra `(` e `)`.
+  una regola, vengono scritte tra `(` e `)`.
 
 * I nomi delle ipotesi, quando argomenti di
   una regola, vengono scritti tra `[` e `]`.
@@ -52,17 +52,82 @@ DOCEND*)
 
 include "didactic/support/natural_deduction.ma".
 
-theorem pippo : (∀x.P (f x) ∧ Q x) ⇒ (∃x.Q x) ⇒ ∃y.P y.
-apply rule (prove ((∀x.P (f x) ∧ Q x) ⇒ (∃x.Q x) ⇒ ∃y.P y));
+(* Il nostro linguaggio del primo ordine prevede le seguenti 
+   - costanti: c
+   - funzioni: f, g (unarie), h (binaria)
+   - predicati: P, Q (unari), R, S (binari) 
+*)
+axiom c : sort.
+axiom f : sort → sort.
+axiom g : sort → sort.
+axiom h : sort → sort → sort.
+axiom P : sort → CProp.
+axiom Q : sort → CProp.
+axiom R : sort →sort → CProp.
+axiom S : sort →sort → CProp.
+
+axiom EM : ∀A:CProp.A ∨ ¬A.
+
+(* intuizionista *)
+lemma ex1: ¬(∃x.P x) ⇒ ∀x.¬ P x.
+apply rule (prove (¬(∃x.P x) ⇒ ∀x.¬ P x));
+apply rule (discharge [x]);
+qed.
+
+(* classico *)
+lemma ex2: ¬(∀x.P x) ⇒ ∃x.¬ P x.
+apply rule (prove (¬(∀x.P x) ⇒ ∃x.¬ P x));
+(*BEGIN*)
+apply rule (⇒_i [h1] (∃x.¬ P x));
+apply rule (RAA [h2] (⊥));
+apply rule (¬_e (¬(∀x.P x)) (∀x.P x));
+	[ apply rule (discharge [h1]);
+	| apply rule (∀_i {y} (P y));
+    apply rule (RAA [h3] (⊥));
+    apply rule (¬_e (¬∃x.¬ P x) (∃x.¬ P x));
+	   [ apply rule (discharge [h2]);
+	   | apply rule (∃_i {y} (¬P y));
+       apply rule (discharge [h3]);
+	   ]
+	]
+(*END*)
+qed.
+
+(* intuizionista *)
+lemma ex3: ((∃x.P x) ⇒ Q c) ⇒ ∀x.P x ⇒ Q c.
+apply rule (prove (((∃x.P x) ⇒ Q c) ⇒ ∀x.P x ⇒ Q c));
+apply rule (discharge [x]);
+qed.
+
+(* classico *)
+lemma ex4: ((∀x.P x) ⇒ Q c) ⇒ ∃x.P x ⇒ Q c.
+apply rule (prove (((∀x.P x) ⇒ Q c) ⇒ ∃x.P x ⇒ Q c));
 (*BEGIN*)
-apply rule (⇒_i [h1] ((∃x.Q x) ⇒ ∃y.P y));
-apply rule (⇒_i [h2] (∃y.P y));
-apply rule (∃_e (∃x.Q x) {t} [h3] (∃y.P y));
-  [ apply rule (discharge [h2]);
-  | apply rule (let ft ≝ (f t) in ∃_i {ft} (P ft));
-    apply rule (∧_e_l (P (f t) ∧ Q t));
-    apply rule (∀_e {t} (∀x.P (f x) ∧ Q x));
-    apply rule (discharge [h1]);
+apply rule (⇒_i [h1] (∃x.P x ⇒ Q c));
+apply rule (∨_e ((∀x.P x) ∨ ¬(∀x.P x)) [h3] (?) [h3] (?));
+	[ apply rule (lem 0 EM);
+	| apply rule (∃_i {y} (P y ⇒ Q c));
+       apply rule (⇒_i [h4] (Q c));
+       apply rule (⇒_e ((∀x.P x) ⇒ Q c) ((∀x.P x)));
+	       [ apply rule (discharge [h1]);
+         | apply rule (discharge [h3]);
+	       ]
+  | apply rule (∃_e (∃x.¬P x) {y} [h4] (∃x.P x ⇒ Q c));
+	   [ apply rule (lem 1 ex2 (¬(∀x.P x)));
+	     apply rule (discharge [h3]);
+     | apply rule (∃_i {y} (P y ⇒ Q c));
+       apply rule (⇒_i [h5] (Q c));
+       apply rule (⊥_e (⊥));
+       apply rule (¬_e (¬P y) (P y));
+	       [ apply rule (discharge [h4]);
+	       | apply rule (discharge [h5]);
+	       ]
+	   ]
   ]
 (*END*)
-qed.
\ No newline at end of file
+qed.
+
+
+
+
+
diff --git a/helm/software/matita/library/didactic/support/natural_deduction.ma b/helm/software/matita/library/didactic/support/natural_deduction.ma
index f5799b90e..6c106a2d4 100644
--- a/helm/software/matita/library/didactic/support/natural_deduction.ma
+++ b/helm/software/matita/library/didactic/support/natural_deduction.ma
@@ -103,13 +103,10 @@ axiom L : CProp.
 axiom M : CProp.
 axiom N : CProp.
 axiom O : CProp.
-axiom P : sort →CProp.
-axiom Q : sort →CProp.
-axiom R : sort →sort →CProp.
-axiom S : sort →sort →CProp.
-axiom f : sort → sort.
-axiom g : sort → sort.
-axiom h : sort → sort → sort.
+axiom  x: sort.
+axiom  y: sort.
+axiom  z: sort.
+axiom  w: sort.
 
 (* Every formula user provided annotates its proof:
    `A` becomes `(show A ?)` *)
@@ -523,7 +520,7 @@ interpretation "Exists_intro_ok_2" 'Exists_intro_ok_2 Pn Px =
   (cast _ _ (show Px (Exists_intro _ _ _ Pn))).
 
 notation >"∃_'i' {term 90 t} term 90 Pt" non associative with precedence 19
-for @{'Exists_intro $t (λ_.?) (show $Pt ?)}. 
+for @{'Exists_intro $t (λw.? w) (show $Pt ?)}. 
 interpretation "Exists_intro KO" 'Exists_intro t P Pt =
  (cast _ _ (Exists_intro sort P t (cast _ _ Pt))).
 interpretation "Exists_intro OK" 'Exists_intro t P Pt =
@@ -550,14 +547,16 @@ for @{ 'Exists_elim_ok_2 $ExPx (λ${ident n}:$tn.λ${ident HPn}:$Pn.$Pc) $c }.
 interpretation "Exists_elim_ok_2" 'Exists_elim_ok_2 ExPx Pc c =
     (cast _ _ (show c (Exists_elim _ _ _ ExPx Pc))).
 
-definition ex_concl := λx:CProp.sort → unit → x.
+definition ex_concl := λx:sort → CProp.∀y:sort.unit → x y.
+definition ex_concl_dummy := ∀y:sort.unit → unit.
 definition fake_pred := λx:sort.unit.
 
 notation >"∃_'e' term 90 ExPt {ident t} [ident H] term 90 c" non associative with precedence 19
-for @{'Exists_elim (λ_.?) (show $ExPt ?) (λ${ident t}:sort.λ${ident H}.show $c ?)}. 
+for @{'Exists_elim (λx.? x) (show $ExPt ?) (λ${ident t}:sort.λ${ident H}.show $c ?)}. 
 interpretation "Exists_elim KO" 'Exists_elim P ExPt c =
  (cast _ _ (Exists_elim sort P _ 
-   (cast (Exists _ P)  _ ExPt) (cast (ex_concl unit) (ex_concl _) c))).
+   (cast (Exists _ P)  _ ExPt) 
+   (cast ex_concl_dummy (ex_concl _) c))).
 interpretation "Exists_elim OK" 'Exists_elim P ExPt c =
  (Exists_elim sort P _ ExPt c).
 
-- 
2.39.2