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 (**************************************************************************)
17 http://mowgli.cs.unibo.it/~tassi/exercise-natural_deduction.html
24 Compilare i seguenti campi:
38 include "didactic/support/natural_deduction.ma".
40 theorem EM: ∀A:CProp. A ∨ ¬ A.
42 apply rule (prove (A ∨ ¬A));
43 apply rule (RAA [H] (⊥)).
44 apply rule (¬#e (¬(A ∨ ¬A)) (A ∨ ¬A));
45 [ apply rule (discharge [H]).
46 | apply rule (⊥#e (⊥));
47 apply rule (¬#e (¬¬A) (¬A));
48 [ apply rule (¬#i [K] (⊥)).
49 apply rule (¬#e (¬(A ∨ ¬A)) (A ∨ ¬A));
50 [ apply rule (discharge [H]).
51 | apply rule (∨#i_r (¬A)).
52 apply rule (discharge [K]).
54 | apply rule (¬#i [K] (⊥)).
55 apply rule (¬#e (¬(A ∨ ¬A)) (A ∨ ¬A));
56 [ apply rule (discharge [H]).
57 | apply rule (∨#i_l (A)).
58 apply rule (discharge [K]).
64 theorem ex0 : (F∧¬G ⇒ L ⇒ E) ⇒ (G ∧ L ⇒ E) ⇒ F ∧ L ⇒ E.
65 apply rule (prove ((F∧¬G ⇒ L ⇒ E) ⇒ (G ∧ L ⇒ E) ⇒ F ∧ L ⇒ E));
67 apply rule (⇒#i [h1] ((G ∧ L ⇒ E) ⇒ F ∧ L ⇒ E));
68 apply rule (⇒#i [h2] (F ∧ L ⇒ E));
69 apply rule (⇒#i [h3] (E));
70 apply rule (∨#e (G∨¬G) [h4] (E) [h4] (E));
71 [ apply rule (lem 0 EM);
72 | apply rule (⇒#e (G∧L⇒E) (G∧L));
73 [ apply rule (discharge [h2]);
74 | apply rule (∧#i (G) (L));
75 [ apply rule (discharge [h4]);
76 | apply rule (∧#e_r (F∧L));
77 apply rule (discharge [h3]);
80 | apply rule (⇒#e (L⇒E) (L));
81 [ apply rule (⇒#e (F∧¬G ⇒ L ⇒ E) (F∧¬G));
82 [ apply rule (discharge [h1]);
83 | apply rule (∧#i (F) (¬G));
84 [ apply rule (∧#e_l (F∧L));
85 apply rule (discharge [h3]);
86 | apply rule (discharge [h4]);
89 | apply rule (∧#e_r (F∧L));
90 apply rule (discharge [h3]);
96 theorem ex1 : (F ⇒ G∨E) ⇒ (G ⇒ ¬ (L ∧ ¬E)) ⇒ (¬L ∨ F) ⇒ L ⇒ E.
97 apply rule (prove (F ⇒ G∨E) ⇒ (G ⇒ ¬ (L ∧ ¬E)) ⇒ (¬L ∨ F) ⇒ L ⇒ E);
99 apply rule (⇒#i [h1] ((G ⇒ ¬ (L ∧ ¬E)) ⇒ (¬L ∨ F) ⇒ L ⇒ E));
100 apply rule (⇒#i [h2] ((¬L ∨ F) ⇒ L ⇒ E));
101 apply rule (⇒#i [h3] (L ⇒ E));
102 apply rule (⇒#i [h4] (E));
103 apply rule (∨#e (¬L∨F) [h5] (E) [h5] (E));
104 [ apply rule (discharge [h3]);
105 | apply rule (⊥#e (⊥));
106 apply rule (¬#e (¬L) (L));
107 [ apply rule (discharge [h5]);
108 | apply rule (discharge [h4]);
110 | apply rule (∨#e (G∨E) [h6] (E) [h6] (E));
111 [ apply rule (⇒#e (F⇒G∨E) (F));
112 [ apply rule (discharge [h1]);
113 | apply rule (discharge [h5]);
115 | apply rule (RAA [h7] (⊥));
116 apply rule (¬#e (¬ (L ∧ ¬E)) (L ∧ ¬E));
117 [ apply rule (⇒#e (G ⇒ ¬ (L ∧ ¬E)) (G));
118 [apply rule (discharge [h2]);
119 |apply rule (discharge [h6]);
121 | apply rule (∧#i (L) (¬E));
122 [ apply rule (discharge [h4]);
123 | apply rule (discharge [h7]);
126 | apply rule (discharge [h6]);
132 theorem ex2 : (F∧G ⇒ E) ⇒ (H ⇒ E∨F) ⇒ (¬G ⇒ ¬H) ⇒ H ⇒ E.
133 apply rule (prove ((F∧G ⇒ E) ⇒ (H ⇒ E∨F) ⇒ (¬G ⇒ ¬H) ⇒ H ⇒ E));
135 apply rule (⇒#i [h1] ((H ⇒ E∨F) ⇒ (¬G ⇒ ¬H) ⇒ H ⇒ E));
136 apply rule (⇒#i [h2] ((¬G ⇒ ¬H) ⇒ H ⇒ E));
137 apply rule (⇒#i [h3] (H ⇒ E));
138 apply rule (⇒#i [h4] (E));
139 apply rule (∨#e (G∨¬G) [h5] (E) [h5] (E));
140 [apply rule (lem 0 EM);
141 | apply rule (∨#e (E∨F) [h6] (E) [h6] (E));
142 [ apply rule (⇒#e (H ⇒ E∨F) (H));
143 [ apply rule (discharge [h2]);
144 | apply rule (discharge [h4]);
146 | apply rule (discharge [h6]);
147 | apply rule (⇒#e (F∧G ⇒ E) (F∧G));
148 [apply rule (discharge [h1]);
149 |apply rule (∧#i (F) (G));
150 [ apply rule (discharge [h6]);
151 | apply rule (discharge [h5]);
155 | apply rule (⊥#e (⊥));
156 apply rule (¬#e (¬H) (H));
157 [ apply rule (⇒#e (¬G ⇒ ¬H) (¬G));
158 [ apply rule (discharge [h3]);
159 | apply rule (discharge [h5]);
161 | apply rule (discharge [h4]);
167 theorem ex3 : (F∧G ⇒ E) ⇒ (¬E ⇒ G∨¬L) ⇒ (L ⇒ F) ⇒ L ⇒ E.
168 apply rule (prove ((F∧G ⇒ E) ⇒ (¬E ⇒ G∨¬L) ⇒ (L ⇒ F) ⇒ L ⇒ E)).
170 apply rule (⇒#i [h1] ((¬E ⇒ G∨¬L) ⇒ (L ⇒ F) ⇒ L ⇒ E));
171 apply rule (⇒#i [h2] ((L ⇒ F) ⇒ L ⇒ E));
172 apply rule (⇒#i [h3] (L ⇒ E));
173 apply rule (⇒#i [h4] (E));
174 apply rule (RAA [h5] (⊥));
175 apply rule (∨#e (G∨¬L) [h6] (⊥) [h6] (⊥));
176 [ apply rule (⇒#e (¬E ⇒ G∨¬L) (¬E));
177 [ apply rule (discharge [h2]);
178 | apply rule (discharge [h5]);
180 | apply rule (¬#e (¬E) (E));
181 [ apply rule (discharge [h5]);
182 | apply rule (⇒#e (F∧G ⇒ E) (F∧G));
183 [ apply rule (discharge [h1]);
184 | apply rule (∧#i (F) (G));
185 [ apply rule (⇒#e (L⇒F) (L));
186 [ apply rule (discharge [h3]);
187 | apply rule (discharge [h4]);
189 | apply rule (discharge [h6]);
193 | apply rule (¬#e (¬L) (L));
194 [ apply rule (discharge [h6]);
195 | apply rule (discharge [h4]);