1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
18 Compilare i seguenti campi:
37 Per digitare i connettivi logici:
42 * `⇒` : `=>`, `\Rightarrow`
46 Per digitare i quantificatori:
51 I termini, le formule e i nomi delle ipotesi
52 ============================================
54 * I termini quantificati da `∀` e `∃`, quando argomenti di
55 una regola, vengono scritti tra `{` e `}`.
57 * Le formule, quando argomenti di
58 una regola, vengono scritte tra `(` e `)`.
60 * I nomi delle ipotesi, quando argomenti di
61 una regola, vengono scritti tra `[` e `]`.
63 Le regole di deduzione naturale
64 ===============================
66 Per digitare le regole di deduzione naturale
67 è possibile utilizzare la palette che compare
68 sulla sinistra dopo aver premuto `F2`.
70 L'albero si descrive partendo dalla radice. Le regole
71 con premesse multiple sono seguite da `[`, `|` e `]`.
74 apply rule (∧#i (A∨B) ⊥);
75 [ …continua qui il sottoalbero per (A∨B)
76 | …continua qui il sottoalbero per ⊥
79 Le regole vengono applicate alle loro premesse, ovvero
80 gli argomenti delle regole sono le formule che normalmente
81 scrivete sopra la linea che rappresenta l'applicazione della
82 regola stessa. Ad esempio:
84 apply rule (∨#e (A∨B) [h1] C [h2] C);
86 | …prova di C sotto l'ipotesi A (di nome h1)
87 | …prova di C sotto l'ipotesi B (di nome h2)
90 Le regole che hanno una sola premessa non vengono seguite
96 Per visualizzare l'albero man mano che viene costruito
97 dai comandi impartiti al sistema, premere `F3` e poi
98 premere sul bottome home (in genere contraddistinto da
99 una icona rappresentate una casa).
101 Si suggerisce di marcare tale finestra come `always on top`
102 utilizzando il menu a tendina che nella maggior parte degli
103 ambienti grafici si apre cliccando nel suo angolo in
106 Applicazioni di regole errate vengono contrassegnate con
109 Usare i lemmi dimostrati in precedenza
110 ======================================
112 Una volta dimostrati alcuni utili lemmi come `A ∨ ¬A` è possibile
113 riutilizzarli in altre dimostrazioni utilizzando la "regola" `lem`.
115 La "regola" `lem` prende come argomenti:
117 - Il numero delle ipotesi del lemma che si vuole utilizzare, nel
118 caso del terzo escluso `0`, nel caso di `¬¬A⇒A` le ipotesi sono `1`.
120 - Dopo il numero di ipotesi, è necessario digitare il nome del lemma.
122 - Infine, le formule che devono essere scritte come premesse per la
125 Ad esempio, per usare il lemma EM (terzo escluso) basta digitare
126 `lem 0 EM`, mentre per usare il lemma NNAA (`¬¬A⇒A`) bisogna digitare
127 `lem 1 NNAA (¬¬A)`. Ai lemmi con più di una premessa è necessario
128 far seguire le parentesi quadre come spiegato in precedenza.
130 Si noti che "regola" `lem` non è una vera regola, ma una forma compatta
131 per rappresentare l'albero di prova del lemma che si sta riutilizzando.
133 Per motivi che saranno più chiari una volta studiate logiche del
134 primo ordine o di ordine superiore, i lemmi che si intende
135 riutilizzare è bene che siano dimostrati astratti sugli atomi.
136 Ovvero per ogni atomo `A`...`Z` che compare nella formula,
137 è bene aggiungere una quantificazione all'inizio della formula stessa.
138 Ad esempio scrivendo `∀A:CProp.` prima della formula `A ∨ ¬A`.
139 La dimostrazione deve poi iniziare con il comando `assume`.
141 In tale modo il lemma EM può essere utilizzato sia per dimostrare
142 `A ∨ ¬A`, sia `B ∨ ¬B`, sia `(A∨C) ∨ ¬(A∨C)`, etc ...
146 include "nat/plus.ma".
148 lemma ex0: ∀n. n + O = n.
150 we proceed by induction on n to prove (n + O = n).
152 the thesis becomes (O + O = O).
159 by induction hypothesis we know (n + O = n) (H).
160 the thesis becomes (S n + O = S n).
168 include "didactic/support/natural_deduction.ma".
170 (* Il nostro linguaggio del primo ordine prevede le seguenti
172 - funzioni: S (unaria), plus, mult (binarie)
173 - predicati: eq (binari)
175 axiom O : sort. (* zero *)
176 axiom S : sort → sort. (* successore *)
177 axiom plus : sort → sort → sort. (* addizione *)
178 axiom mult: sort → sort → sort. (* moltiplicazione *)
179 axiom eq : sort → sort → CProp. (* uguaglianza *)
182 notation < "+ term 90 x term 90 y" non associative with precedence 80 for @{'plus $x $y}.
183 notation < "★ term 90 x term 90 y" non associative with precedence 80 for @{'mult $x $y}.
184 notation < "= term 90 x term 90 y" non associative with precedence 80 for @{'eq $x $y}.
185 notation < "\S term 90 x" non associative with precedence 80 for @{'S $x}.
186 notation < "\O" non associative with precedence 80 for @{'O}.
187 interpretation "O" 'O = O.
188 interpretation "S" 'S x y = (S x y).
189 interpretation "mult" 'mult x y = (mult x y).
190 interpretation "plus" 'plus x y = (plus x y).
191 interpretation "eq" 'eq x y = (eq x y).
194 interpretation "+" 'my_plus x y = (plus x y).
195 interpretation "*" 'my_mult x y = (mult x y).
196 interpretation "=" 'my_eq x y = (eq x y).
197 interpretation "S" 'my_S x = (S x).
198 interpretation "O" 'my_O = O.
200 notation "x + y" non associative with precedence 50 for @{'my_plus $x $y}.
201 notation "x * y" non associative with precedence 55 for @{'my_mult $x $y}.
202 notation "x = y" non associative with precedence 45 for @{'my_eq $x $y}.
203 notation > "'S' x" non associative with precedence 40 for @{'my_S $x}.
204 notation < "'S' x" non associative with precedence 40 for @{'my_S $x}.
205 notation "'O'" non associative with precedence 90 for @{'my_O}.
207 (* Assumiamo la seguente teoria *)
209 (* l'uguaglianza e' una relazione d'equivalenza *)
210 axiom refl: ∀x. x = x.
211 axiom sym: ∀x.∀y. x = y ⇒ y = x.
212 axiom trans: ∀x.∀y.∀z. x = y ⇒ y = z ⇒ x = z.
214 (* assiomi di Peano *)
215 axiom discr: ∀x. ¬ O = (S x).
216 axiom inj: ∀x.∀y. (S x) = (S y) ⇒ x = y.
217 (* Questo è uno schema di assiomi: è come avere una regola di induzione per
218 ogni predicato unario P. Il sistema inferisce automaticamente P. *)
219 axiom induct: ΠP. P O ⇒ (∀n. P n ⇒ P (S n)) ⇒ ∀x.P x.
221 (* definizione ricorsiva di addizione *)
222 axiom plus_O: ∀x. O + x = x.
223 axiom plus_S: ∀x.∀y. (S x) + y = S (x + y).
225 (* definizione ricorsiva di moltiplicazione *)
226 axiom mult_O: ∀x.O * x = O.
227 axiom mult_S: ∀x.∀y. (S x) * y = x * y + y.
229 (* l'uguaglianza e' una congruenza rispetto a tutte le funzioni e predicati *)
230 axiom eq_S: ∀x.∀x'. x = x' ⇒ (S x) = (S x').
231 axiom eq_plus: ∀x.∀x'.∀y.∀y'. x = x' ⇒ y = y' ⇒ x + y = x' + y'.
232 axiom eq_mult: ∀x.∀x'.∀y.∀y'. x = x' ⇒ y = y' ⇒ x * y = x' * y'.
235 lemma ex1: ∀x.x + O = x.
236 apply rule (prove (∀x.x + O = x));
237 (* poichè tutti gli assiomi della teoria sono assiomi e non dimostrazioni,
238 l'unica forma di `apply rule lem` che potete usare è
239 `apply rule (lem 0 nome_assioma)` *)
241 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)));
242 [ apply rule (⇒#e ((O + O) = O ⇒ (∀n.n + O = n ⇒ ((S n) + O) = (S n)) ⇒ (∀x.(x + O) = x)) (O + O = O));
243 [ apply rule (lem 0 induct);
244 | apply rule (∀#e {O} (∀y.(O + y) =y));
245 apply rule (lem 0 plus_O);
247 | apply rule (∀#i {n} (n + O = n ⇒ ((S n) + O) = (S n)));
248 apply rule (⇒#i [H] (((S n) + O) = (S n)));
249 apply rule (⇒#e ((S (n + O)) = (S n) ⇒ ((S n) + O) = (S n)) ((S (n + O)) = (S n)));
250 [ 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))));
251 [ apply rule (∀#e {S n} (∀z.((S n) + O) =(S (n + O))⇒(S (n + O))= z⇒((S n) + O) =z));
252 apply rule (∀#e {(S (n + O))} (∀y.∀z.((S n) + O) =y ⇒ y = z ⇒ ((S n) + O) =z));
253 apply rule (∀#e {(S n) + O} (∀x.∀y.∀z.x = y ⇒ y = z ⇒ x = z));
254 apply rule (lem 0 trans);
255 | apply rule (∀#e {O} (∀m.(S n) + m = (S (n + m))));
256 apply rule (∀#e {n} (∀n.∀m.(S n) + m = (S (n + m))));
257 apply rule (lem 0 plus_S);
259 | apply rule (⇒#e (n + O = n ⇒ (S (n + O)) = (S n)) (n + O = n));
260 [ apply rule (∀#e {n} (∀w.n + O = w ⇒ (S (n + O)) = (S w)));
261 apply rule (∀#e {(n + O)} (∀y.∀w.y = w ⇒ (S y) = (S w)));
262 apply rule (lem 0 eq_S);
263 | apply rule (discharge [H]);