From e18929311cce5baed9bccd9f1de050180f336ed1 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 9 Dec 2008 12:18:42 +0000 Subject: [PATCH] fixed notation --- .../exercises/natural_deduction_theories.ma | 98 +++++++++++++------ 1 file changed, 66 insertions(+), 32 deletions(-) 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..d955bd124 100644 --- 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. -- 2.39.2