fixed notation

[helm.git] / helm / software / matita / library / didactic / exercises / natural_deduction_theories.ma

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 38d28c83c98338772fe86277a4536bf06a3b36b7..d955bd1248441bd0b762e14e198baada68ea71ed 100644 (file)
--- a/helm/software/matita/library/didactic/exercises/natural_deduction_theories.ma
+++ b/helm/software/matita/library/didactic/exercises/natural_deduction_theories.ma
@@ -140,7 +140,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 +164,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.