]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/didactic/exercises/natural_deduction_theories.ma
d955bd1248441bd0b762e14e198baada68ea71ed
[helm.git] / helm / software / matita / library / didactic / exercises / natural_deduction_theories.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 scritte tra `(` e `)`.
45
46 * I nomi delle ipotesi, quando argomenti di
47   una regola, vengono scritti tra `[` e `]`.
48
49 Le regole di deduzione naturale
50 ===============================
51
52 Per digitare le regole di deduzione naturale
53 è possibile utilizzare la palette che compare
54 sulla sinistra dopo aver premuto `F2`.
55
56 L'albero si descrive partendo dalla radice. Le regole
57 con premesse multiple sono seguite da `[`, `|` e `]`.
58 Ad esempio: 
59
60         apply rule (∧_i (A∨B) ⊥);
61           [ …continua qui il sottoalbero per (A∨B)
62           | …continua qui il sottoalbero per ⊥
63           ] 
64
65 Le regole vengono applicate alle loro premesse, ovvero
66 gli argomenti delle regole sono le formule che normalmente 
67 scrivete sopra la linea che rappresenta l'applicazione della
68 regola stessa. Ad esempio:
69
70         apply rule (∨_e (A∨B) [h1] C [h2] C);
71           [ …prova di (A∨B)
72           | …prova di C sotto l'ipotesi A (di nome h1)  
73           | …prova di C sotto l'ipotesi B (di nome h2)
74           ]
75
76 Le regole che hanno una sola premessa non vengono seguite 
77 da parentesi quadre.
78
79 L'albero di deduzione
80 =====================
81
82 Per visualizzare l'albero man mano che viene costruito
83 dai comandi impartiti al sistema, premere `F3` e poi
84 premere sul bottome home (in genere contraddistinto da
85 una icona rappresentate una casa).
86
87 Si suggerisce di marcare tale finestra come `always on top`
88 utilizzando il menu a tendina che nella maggior parte degli
89 ambienti grafici si apre cliccando nel suo angolo in 
90 alto a sinistra.
91
92 Applicazioni di regole errate vengono contrassegnate con
93 il colore rosso.
94
95 Usare i lemmi dimostrati in precedenza
96 ======================================
97
98 Una volta dimostrati alcuni utili lemmi come `A ∨ ¬A` è possibile
99 riutilizzarli in altre dimostrazioni utilizzando la "regola" `lem`.
100
101 La "regola" `lem` prende come argomenti:
102
103 - Il numero delle ipotesi del lemma che si vuole utilizzare, nel
104   caso del terzo escluso `0`, nel caso di `¬¬A⇒A` le ipotesi sono `1`.
105
106 - Dopo il numero di ipotesi, è necessario digitare il nome del lemma.
107
108 - Infine, le formule che devono essere scritte come premesse per la 
109   "regola".
110
111 Ad esempio, per usare il lemma EM (terzo escluso) basta digitare
112 `lem 0 EM`, mentre per usare il lemma NNAA (`¬¬A⇒A`) bisogna digitare
113 `lem 1 NNAA (¬¬A)`. Ai lemmi con più di una premessa è necessario 
114 far seguire le parentesi quadre come spiegato in precedenza.
115
116 Si noti che "regola" `lem` non è una vera regola, ma una forma compatta
117 per rappresentare l'albero di prova del lemma che si sta riutilizzando.
118
119 Per motivi che saranno più chiari una volta studiate logiche del 
120 primo ordine o di ordine superiore, i lemmi che si intende 
121 riutilizzare è bene che siano dimostrati astratti sugli atomi. 
122 Ovvero per ogni atomo `A`...`Z` che compare nella formula, 
123 è bene aggiungere una quantificazione all'inizio della formula stessa.
124 Ad esempio scrivendo `∀A:CProp.` prima della formula `A ∨ ¬A`.
125 La dimostrazione deve poi iniziare con il comando `assume`. 
126
127 In tale modo il lemma EM può essere utilizzato sia per dimostrare 
128 `A ∨ ¬A`, sia `B ∨ ¬B`, sia `(A∨C) ∨ ¬(A∨C)`, etc ...
129
130 DOCEND*)
131
132 include "nat/plus.ma".
133
134 lemma ex0: ∀n. n + O = n.
135  assume n: nat.
136  we proceed by induction on n to prove (n + O = n).
137   case O.
138    the thesis becomes (O + O = O).
139     conclude
140         (O + O)
141       = O
142     done.
143   case S.
144    assume n : nat.
145    by induction hypothesis we know (n + O = n) (H).
146    the thesis becomes (S n + O = S n).
147     conclude
148        (S n + O)
149      = (S (n + O)).
150      = (S n) by H
151     done.
152 qed.
153
154 include "didactic/support/natural_deduction.ma".
155
156 (* Il nostro linguaggio del primo ordine prevede le seguenti 
157    - costanti: O
158    - funzioni: S (unaria), plus, mult (binarie)
159    - predicati: eq (binari)
160 *)
161 axiom O : sort.                  (* zero *)
162 axiom S : sort → sort.           (* successore *)
163 axiom plus : sort → sort → sort. (* addizione *)
164 axiom mult: sort → sort → sort.  (* moltiplicazione *)
165 axiom eq : sort → sort → CProp.  (* uguaglianza *)
166
167 (*
168 notation < "+  term 90 x  term 90 y" non associative with precedence 80 for @{'plus $x $y}.
169 notation < "★  term 90 x  term 90 y" non associative with precedence 80 for @{'mult $x $y}.
170 notation < "=  term 90 x  term 90 y" non associative with precedence 80 for @{'eq $x $y}.
171 notation < "\S  term 90 x" non associative with precedence 80 for @{'S $x}.
172 notation < "\O" non associative with precedence 80 for @{'O}.
173 interpretation "O" 'O = O.
174 interpretation "S" 'S x y = (S x y).
175 interpretation "mult" 'mult x y = (mult x y).
176 interpretation "plus" 'plus x y = (plus x y).
177 interpretation "eq" 'eq x y = (eq x y).
178 *)
179
180 interpretation "+" 'my_plus x y = (plus x y). 
181 interpretation "*" 'my_mult x y = (mult x y).
182 interpretation "=" 'my_eq x y = (eq x y).
183 interpretation "S" 'my_S x = (S x).
184 interpretation "O" 'my_O = O.
185
186 notation "x + y" non associative with precedence 50 for @{'my_plus $x $y}.
187 notation "x * y" non associative with precedence 55 for @{'my_mult $x $y}.
188 notation "x = y" non associative with precedence 45 for @{'my_eq $x $y}.
189 notation > "'S' x" non associative with precedence 40 for @{'my_S $x}.
190 notation < "'S'  x" non associative with precedence 40 for @{'my_S $x}.
191 notation "'O'" non associative with precedence 90 for @{'my_O}.
192
193 (* Assumiamo la seguente teoria *)
194
195 (* l'uguaglianza e' una relazione d'equivalenza *)
196 axiom refl: ∀x. x = x.
197 axiom sym: ∀x.∀y. x = y ⇒ y = x.
198 axiom trans: ∀x.∀y.∀z. x = y ⇒ y = z ⇒ x = z.
199
200 (* assiomi di Peano *)
201 axiom discr: ∀x. ¬ O = (S x).
202 axiom inj: ∀x.∀y. (S x) = (S y) ⇒ x = y.
203 (* Questo è uno schema di assiomi: è come avere una regola di induzione per 
204    ogni predicato unario P. Il sistema inferisce automaticamente P. *)  
205 axiom induct: ΠP. P O ⇒ (∀n. P n ⇒ P (S n)) ⇒ ∀x.P x.
206
207 (* definizione ricorsiva di addizione *)
208 axiom plus_O: ∀x. O + x = x.
209 axiom plus_S: ∀x.∀y. (S x) + y = S (x + y).
210
211 (* definizione ricorsiva di moltiplicazione *)
212 axiom mult_O: ∀x.O * x = O.
213 axiom mult_S: ∀x.∀y. (S x) * y = x * y + y.
214
215 (* l'uguaglianza e' una congruenza rispetto a tutte le funzioni e predicati *)
216 axiom eq_S: ∀x.∀x'. x = x' ⇒ (S x) = (S x').
217 axiom eq_plus: ∀x.∀x'.∀y.∀y'. x = x' ⇒ y = y' ⇒ x + y = x' + y'.
218 axiom eq_mult: ∀x.∀x'.∀y.∀y'. x = x' ⇒ y = y' ⇒ x * y = x' * y'.
219
220 (* intuizionista *)
221 lemma ex1: ∀x.x + O = x.
222 apply rule (prove (∀x.x + O = x));
223 (* poichè tutti gli assiomi della teoria sono assiomi e non dimostrazioni,
224    l'unica forma di `apply rule lem` che potete usare è 
225    `apply rule (lem 0 nome_assioma)` *)
226 (*BEGIN*)
227 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)));
228         [ apply rule (⇒_e ((O + O) = O ⇒ (∀n.n + O = n ⇒ ((S n) + O) = (S n)) ⇒ (∀x.(x + O) = x)) (O + O = O));
229            [ apply rule (lem 0 induct);
230            | apply rule (∀_e {O} (∀y.(O + y) =y));
231              apply rule (lem 0 plus_O);
232            ]
233         | apply rule (∀_i {n} (n + O = n ⇒ ((S n) + O) = (S n)));
234     apply rule (⇒_i [H] (((S n) + O) = (S n)));
235     apply rule (⇒_e ((S (n + O)) = (S n) ⇒ ((S n) + O) = (S n)) ((S (n + O)) = (S n)));
236            [ 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))));
237               [ apply rule (∀_e {S n} (∀z.((S n) + O) =(S (n + O))⇒(S (n + O))= z⇒((S n) + O) =z));
238                 apply rule (∀_e {(S (n + O))} (∀y.∀z.((S n) + O) =y ⇒ y = z ⇒ ((S n) + O) =z));
239           apply rule (∀_e {(S n) + O} (∀x.∀y.∀z.x = y ⇒ y = z ⇒ x = z));
240           apply rule (lem 0 trans);
241               | apply rule (∀_e {O} (∀m.(S n) + m = (S (n + m))));
242           apply rule (∀_e {n} (∀n.∀m.(S n) + m = (S (n + m))));
243           apply rule (lem 0 plus_S);
244               ]
245            | apply rule (⇒_e (n + O = n ⇒ (S (n + O)) = (S n)) (n + O = n));
246               [ apply rule (∀_e {n} (∀w.n + O = w ⇒ (S (n + O)) = (S w)));
247           apply rule (∀_e {(n + O)} (∀y.∀w.y = w ⇒ (S y) = (S w)));
248           apply rule (lem 0 eq_S);
249               | apply rule (discharge [H]);
250               ]
251            ]
252         ]
253 (*END*)
254 qed.