X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdidactic%2Fexercises%2Fnatural_deduction_theories.ma;h=9768e26e2997da01f7c6b1da99a4cdff2ae1c174;hb=b254cc57f5e082712f3ec6be9295eec0062b8d47;hp=38d28c83c98338772fe86277a4536bf06a3b36b7;hpb=01d82c5e0c4f01881aeb746062438dcc3d05bc29;p=helm.git

diff --git a/helm/software/matita/library/didactic/exercises/natural_deduction_theories.ma b/helm/software/matita/library/didactic/exercises/natural_deduction_theories.ma
index 38d28c83c..9768e26e2 100644
--- a/helm/software/matita/library/didactic/exercises/natural_deduction_theories.ma
+++ b/helm/software/matita/library/didactic/exercises/natural_deduction_theories.ma
@@ -1,3 +1,17 @@
+(**************************************************************************)
+(*       ___	                                                          *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
+(*      ||A||       E.Tassi, S.Zacchiroli                                 *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU Lesser General Public License Version 2.1         *)
+(*                                                                        *)
+(**************************************************************************)
+
 (* Esercizio 0
    ===========
 
@@ -57,7 +71,7 @@ L'albero si descrive partendo dalla radice. Le regole
 con premesse multiple sono seguite da `[`, `|` e `]`.
 Ad esempio: 
 
-        apply rule (∧_i (A∨B) ⊥);
+        apply rule (∧#i (A∨B) ⊥);
           [ …continua qui il sottoalbero per (A∨B)
           | …continua qui il sottoalbero per ⊥
           ] 
@@ -67,7 +81,7 @@ gli argomenti delle regole sono le formule che normalmente
 scrivete sopra la linea che rappresenta l'applicazione della
 regola stessa. Ad esempio:
 
-        apply rule (∨_e (A∨B) [h1] C [h2] C);
+        apply rule (∨#e (A∨B) [h1] C [h2] C);
           [ …prova di (A∨B)
           | …prova di C sotto l'ipotesi A (di nome h1)  
           | …prova di C sotto l'ipotesi B (di nome h2)
@@ -140,7 +154,8 @@ lemma ex0: ∀n. n + O = n.
         (O + O)
       = O
     done.
-  case S (n:nat).
+  case S.
+   assume n : nat.
    by induction hypothesis we know (n + O = n) (H).
    the thesis becomes (S n + O = S n).
     conclude
@@ -163,58 +178,91 @@ axiom plus : sort → sort → sort. (* addizione *)
 axiom mult: sort → sort → sort.  (* moltiplicazione *)
 axiom eq : sort → sort → CProp.  (* uguaglianza *)
 
+(*
+notation < "+  term 90 x  term 90 y" non associative with precedence 80 for @{'plus $x $y}.
+notation < "★  term 90 x  term 90 y" non associative with precedence 80 for @{'mult $x $y}.
+notation < "=  term 90 x  term 90 y" non associative with precedence 80 for @{'eq $x $y}.
+notation < "\S  term 90 x" non associative with precedence 80 for @{'S $x}.
+notation < "\O" non associative with precedence 80 for @{'O}.
+interpretation "O" 'O = O.
+interpretation "S" 'S x y = (S x y).
+interpretation "mult" 'mult x y = (mult x y).
+interpretation "plus" 'plus x y = (plus x y).
+interpretation "eq" 'eq x y = (eq x y).
+*)
+
+interpretation "+" 'my_plus x y = (plus x y). 
+interpretation "*" 'my_mult x y = (mult x y).
+interpretation "=" 'my_eq x y = (eq x y).
+interpretation "S" 'my_S x = (S x).
+interpretation "O" 'my_O = O.
+
+notation "x + y" non associative with precedence 50 for @{'my_plus $x $y}.
+notation "x * y" non associative with precedence 55 for @{'my_mult $x $y}.
+notation "x = y" non associative with precedence 45 for @{'my_eq $x $y}.
+notation > "'S' x" non associative with precedence 40 for @{'my_S $x}.
+notation < "'S'  x" non associative with precedence 40 for @{'my_S $x}.
+notation "'O'" non associative with precedence 90 for @{'my_O}.
+
 (* Assumiamo la seguente teoria *)
 
 (* l'uguaglianza e' una relazione d'equivalenza *)
-axiom refl: ∀x. eq x x.
-axiom sym: ∀x.∀y. eq x y ⇒ eq y x.
-axiom trans: ∀x.∀y.∀z. eq x y ⇒ eq y z ⇒ eq x z.
+axiom refl: ∀x. x = x.
+axiom sym: ∀x.∀y. x = y ⇒ y = x.
+axiom trans: ∀x.∀y.∀z. x = y ⇒ y = z ⇒ x = z.
 
 (* assiomi di Peano *)
-axiom discr: ∀x. ¬ eq O (S x).
-axiom inj: ∀x.∀y. eq (S x) (S y) ⇒ eq x y.
-axiom induct: ΠP. P O ⇒ (∀n. P n ⇒ P (S n)) ⇒ ∀x. P x.
+axiom discr: ∀x. ¬ O = (S x).
+axiom inj: ∀x.∀y. (S x) = (S y) ⇒ x = y.
+(* Questo è uno schema di assiomi: è come avere una regola di induzione per 
+   ogni predicato unario P. Il sistema inferisce automaticamente P. *)  
+axiom induct: ΠP. P O ⇒ (∀n. P n ⇒ P (S n)) ⇒ ∀x.P x.
 
 (* definizione ricorsiva di addizione *)
-axiom plus_O: ∀x. eq (plus O x) x.
-axiom plus_S: ∀x.∀y. eq (plus (S x) y) (S (plus x y)).
+axiom plus_O: ∀x. O + x = x.
+axiom plus_S: ∀x.∀y. (S x) + y = S (x + y).
 
 (* definizione ricorsiva di moltiplicazione *)
-axiom mult_O: ∀x.eq (mult O x) O.
-axiom mult_S: ∀x.∀y. eq (mult (S x) y) (plus (mult x y) y).
+axiom mult_O: ∀x.O * x = O.
+axiom mult_S: ∀x.∀y. (S x) * y = x * y + y.
 
 (* l'uguaglianza e' una congruenza rispetto a tutte le funzioni e predicati *)
-axiom eq_S: ∀x.∀x'. eq x x' ⇒ eq (S x) (S x').
-axiom eq_plus: ∀x.∀x'.∀y.∀y'. eq x x' ⇒ eq y y' ⇒ eq (plus x y) (plus x' y').
-axiom eq_mult: ∀x.∀x'.∀y.∀y'. eq x x' ⇒ eq y y' ⇒ eq (mult x y) (mult x' y').
+axiom eq_S: ∀x.∀x'. x = x' ⇒ (S x) = (S x').
+axiom eq_plus: ∀x.∀x'.∀y.∀y'. x = x' ⇒ y = y' ⇒ x + y = x' + y'.
+axiom eq_mult: ∀x.∀x'.∀y.∀y'. x = x' ⇒ y = y' ⇒ x * y = x' * y'.
 
 (* intuizionista *)
-lemma ex1: ∀x.eq (plus x O) x.
-apply rule (prove (∀x.eq (plus x O) x));
-apply rule (⇒_e ((∀n.eq (plus n O) n ⇒ eq (plus (S n) O) (S n)) ⇒ (∀x.eq (plus x O) x)) (∀n.eq (plus n O) n ⇒ eq (plus (S n) O) (S n)));
-	[ apply rule (⇒_e (eq (plus O O) O ⇒ (∀n.eq (plus n O) n ⇒ eq (plus (S n) O) (S n)) ⇒ (∀x.eq (plus x O) x)) (eq (plus O O) O));
+lemma ex1: ∀x.x + O = x.
+apply rule (prove (∀x.x + O = x));
+(* poichè tutti gli assiomi della teoria sono assiomi e non dimostrazioni,
+   l'unica forma di `apply rule lem` che potete usare è 
+   `apply rule (lem 0 nome_assioma)` *)
+(*BEGIN*)
+apply rule (⇒#e ((∀n.(n + O) = n ⇒ ((S n) + O) = (S n)) ⇒ (∀x.(x + O) = x)) (∀n.(n + O) = n ⇒ ((S n) + O) = (S n)));
+	[ apply rule (⇒#e ((O + O) = O ⇒ (∀n.n + O = n ⇒ ((S n) + O) = (S n)) ⇒ (∀x.(x + O) = x)) (O + O = O));
 	   [ apply rule (lem 0 induct);
-	   | apply rule (∀_e {O} (∀y.eq (plus O y) y));
+	   | apply rule (∀#e {O} (∀y.(O + y) =y));
 	     apply rule (lem 0 plus_O);
 	   ]
-	| apply rule (∀_i {n} (eq (plus n O) n ⇒ eq (plus (S n) O) (S n)));
-    apply rule (⇒_i [H] (eq (plus (S n) O) (S n)));
-    apply rule (⇒_e (eq (S (plus n O)) (S n) ⇒ eq (plus (S n) O) (S n)) (eq (S (plus n O)) (S n)));
-	   [ apply rule (⇒_e (eq (plus (S n) O) (S (plus n O)) ⇒ eq (S (plus n O)) (S n)⇒eq (plus (S n) O) (S n)) (eq (plus (S n) O) (S (plus n O))));
-	      [ apply rule (∀_e {S n} (∀z.eq (plus (S n) O) (S (plus n O))⇒eq (S (plus n O)) z⇒eq (plus (S n) O) z));
-	        apply rule (∀_e {(S (plus n O))} (∀y.∀z.eq (plus (S n) O) y ⇒ eq y z ⇒ eq (plus (S n) O) z));
-          apply rule (∀_e {plus (S n) O} (∀x.∀y.∀z.eq x y ⇒ eq y z ⇒ eq x z));
+	| apply rule (∀#i {n} (n + O = n ⇒ ((S n) + O) = (S n)));
+    apply rule (⇒#i [H] (((S n) + O) = (S n)));
+    apply rule (⇒#e ((S (n + O)) = (S n) ⇒ ((S n) + O) = (S n)) ((S (n + O)) = (S n)));
+	   [ apply rule (⇒#e (((S n) + O) =(S (n + O)) ⇒ (S (n + O)) = (S n)⇒((S n) + O) =(S n)) (((S n) + O) =(S (n + O))));
+	      [ apply rule (∀#e {S n} (∀z.((S n) + O) =(S (n + O))⇒(S (n + O))= z⇒((S n) + O) =z));
+	        apply rule (∀#e {(S (n + O))} (∀y.∀z.((S n) + O) =y ⇒ y = z ⇒ ((S n) + O) =z));
+          apply rule (∀#e {(S n) + O} (∀x.∀y.∀z.x = y ⇒ y = z ⇒ x = z));
           apply rule (lem 0 trans);
-	      | apply rule (∀_e {O} (∀m.eq (plus (S n) m) (S (plus n m))));
-          apply rule (∀_e {n} (∀n.∀m.eq (plus (S n) m) (S (plus n m))));
+	      | apply rule (∀#e {O} (∀m.(S n) + m = (S (n + m))));
+          apply rule (∀#e {n} (∀n.∀m.(S n) + m = (S (n + m))));
           apply rule (lem 0 plus_S);
 	      ]
-	   | apply rule (⇒_e (eq (plus n O) n ⇒ eq (S (plus n O)) (S n)) (eq (plus n O) n));
-	      [ apply rule (∀_e {n} (∀w.eq (plus n O) w ⇒ eq (S (plus n O)) (S w)));
-          apply rule (∀_e {(plus n O)} (∀y.∀w.eq y w ⇒ eq (S y) (S w)));
+	   | apply rule (⇒#e (n + O = n ⇒ (S (n + O)) = (S n)) (n + O = n));
+	      [ apply rule (∀#e {n} (∀w.n + O = w ⇒ (S (n + O)) = (S w)));
+          apply rule (∀#e {(n + O)} (∀y.∀w.y = w ⇒ (S y) = (S w)));
           apply rule (lem 0 eq_S);
 	      | apply rule (discharge [H]);
 	      ]
 	   ]
 	]
-qed.
\ No newline at end of file
+(*END*)
+qed.