]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/didactic/exercises/natural_deduction1.ma
c2778fbc5c0b548296f75fd5e0642810558d411e
[helm.git] / helm / software / matita / library / didactic / exercises / natural_deduction1.ma
1 (* Istruzioni: 
2
3      http://mowgli.cs.unibo.it/~tassi/exercise-natural_deduction.html 
4
5 *)
6
7 (* Esercizio 0
8    ===========
9
10    Compilare i seguenti campi:
11
12    Nome1: ...
13    Cognome1: ...
14    Matricola1: ...
15    Account1: ...
16
17    Nome2: ...
18    Cognome2: ...
19    Matricola2: ...
20    Account2: ...
21
22 *)
23
24 include "didactic/support/natural_deduction.ma".
25
26 theorem EM: ∀A:CProp. A ∨ ¬ A.
27 assume A: CProp.
28 apply rule (prove (A ∨ ¬A));
29 apply rule (RAA [H] (⊥)).
30 apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
31         [ apply rule (discharge [H]).
32         | apply rule (⊥_e (⊥));
33           apply rule (¬_e (¬¬A) (¬A));
34            [ apply rule (¬_i [K] (⊥)).
35        apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
36               [ apply rule (discharge [H]).
37               | apply rule (∨_i_r (¬A)).
38           apply rule (discharge [K]).
39               ]
40            | apply rule (¬_i [K] (⊥)).
41        apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
42               [ apply rule (discharge [H]).
43               | apply rule (∨_i_l (A)).
44           apply rule (discharge [K]).
45               ]
46            ]
47         ]
48 qed.
49
50 theorem ex0 : (F∧¬G ⇒ L ⇒ E) ⇒ (G ∧ L ⇒ E) ⇒ F ∧ L ⇒ E.
51 apply rule (prove ((F∧¬G ⇒ L ⇒ E) ⇒ (G ∧ L ⇒ E) ⇒ F ∧ L ⇒ E));
52 (*BEGIN*)
53 apply rule (⇒_i [h1] ((G ∧ L ⇒ E) ⇒ F ∧ L ⇒ E));
54 apply rule (⇒_i [h2] (F ∧ L ⇒ E));
55 apply rule (⇒_i [h3] (E));
56 apply rule (∨_e (G∨¬G) [h4] (E) [h4] (E));
57         [ apply rule (lem 0 EM);
58         | apply rule (⇒_e (G∧L⇒E) (G∧L));
59             [ apply rule (discharge [h2]);
60             | apply rule (∧_i (G) (L));
61                 [ apply rule (discharge [h4]);
62                 | apply rule (∧_e_r (F∧L));
63                   apply rule (discharge [h3]);
64                 ]
65             ]
66         | apply rule (⇒_e (L⇒E) (L));
67             [ apply rule (⇒_e (F∧¬G ⇒ L ⇒ E) (F∧¬G));
68                 [ apply rule (discharge [h1]);
69                 | apply rule (∧_i (F) (¬G));
70                     [ apply rule (∧_e_l (F∧L));
71                       apply rule (discharge [h3]);
72                     | apply rule (discharge [h4]);
73                     ]
74                 ]  
75             | apply rule (∧_e_r (F∧L));
76               apply rule (discharge [h3]);
77             ]
78         ]
79 (*END*)
80 qed.
81
82 theorem ex1 : (F ⇒ G∨E) ⇒ (G ⇒ ¬ (L ∧ ¬E)) ⇒ (¬L ∨ F) ⇒ L ⇒ E.
83 apply rule (prove (F ⇒ G∨E) ⇒ (G ⇒ ¬ (L ∧ ¬E)) ⇒ (¬L ∨ F) ⇒ L ⇒ E);
84 (*BEGIN*)
85 apply rule (⇒_i [h1] ((G ⇒ ¬ (L ∧ ¬E)) ⇒ (¬L ∨ F) ⇒ L ⇒ E));
86 apply rule (⇒_i [h2] ((¬L ∨ F) ⇒ L ⇒ E));
87 apply rule (⇒_i [h3] (L ⇒ E));
88 apply rule (⇒_i [h4] (E));
89 apply rule (∨_e (¬L∨F) [h5] (E) [h5] (E));
90         [ apply rule (discharge [h3]);
91         | apply rule (⊥_e (⊥));
92     apply rule (¬_e (¬L) (L));
93             [ apply rule (discharge [h5]);
94             | apply rule (discharge [h4]);
95             ]
96         | apply rule (∨_e (G∨E) [h6] (E) [h6] (E));
97            [ apply rule (⇒_e (F⇒G∨E) (F));
98               [ apply rule (discharge [h1]);
99               | apply rule (discharge [h5]);
100               ]
101            | apply rule (RAA [h7] (⊥));
102        apply rule (¬_e (¬ (L ∧ ¬E)) (L ∧ ¬E));
103                [ apply rule (⇒_e (G ⇒ ¬ (L ∧ ¬E)) (G));
104                    [apply rule (discharge [h2]);
105                    |apply rule (discharge [h6]);
106                    ]
107                | apply rule (∧_i (L) (¬E));
108                    [ apply rule (discharge [h4]);
109                    | apply rule (discharge [h7]);
110                    ]
111                ]
112            | apply rule (discharge [h6]);
113            ]
114         ]
115 (*END*)
116 qed.
117
118 theorem ex2 : (F∧G ⇒ E) ⇒ (H ⇒ E∨F) ⇒ (¬G ⇒ ¬H) ⇒ H ⇒ E.
119 apply rule (prove ((F∧G ⇒ E) ⇒ (H ⇒ E∨F) ⇒ (¬G ⇒ ¬H) ⇒ H ⇒ E));
120 (*BEGIN*)
121 apply rule (⇒_i [h1] ((H ⇒ E∨F) ⇒ (¬G ⇒ ¬H) ⇒ H ⇒ E));
122 apply rule (⇒_i [h2] ((¬G ⇒ ¬H) ⇒ H ⇒ E));
123 apply rule (⇒_i [h3] (H ⇒ E));
124 apply rule (⇒_i [h4] (E));
125 apply rule (∨_e (G∨¬G) [h5] (E) [h5] (E));
126         [apply rule (lem 0 EM);
127         | apply rule (∨_e (E∨F) [h6] (E) [h6] (E));
128            [ apply rule (⇒_e (H ⇒ E∨F) (H));
129                [ apply rule (discharge [h2]);
130                | apply rule (discharge [h4]);
131                ]
132            | apply rule (discharge [h6]);
133            | apply rule (⇒_e (F∧G ⇒ E) (F∧G));
134               [apply rule (discharge [h1]);
135               |apply rule (∧_i (F) (G));
136                 [ apply rule (discharge [h6]);
137                 | apply rule (discharge [h5]);
138                 ]
139               ]
140            ]
141         | apply rule (⊥_e (⊥));
142     apply rule (¬_e (¬H) (H));
143         [ apply rule (⇒_e (¬G ⇒ ¬H) (¬G));
144                [ apply rule (discharge [h3]);
145                | apply rule (discharge [h5]);
146                ]
147             | apply rule (discharge [h4]);
148             ]
149         ]
150 (*END*)
151 qed.
152
153 theorem ex3 : (F∧G ⇒ E) ⇒ (¬E ⇒ G∨¬L) ⇒ (L ⇒ F) ⇒ L ⇒ E.
154 apply rule (prove ((F∧G ⇒ E) ⇒ (¬E ⇒ G∨¬L) ⇒ (L ⇒ F) ⇒ L ⇒ E)).
155 (*BEGIN*)
156 apply rule (⇒_i [h1] ((¬E ⇒ G∨¬L) ⇒ (L ⇒ F) ⇒ L ⇒ E));
157 apply rule (⇒_i [h2] ((L ⇒ F) ⇒ L ⇒ E));
158 apply rule (⇒_i [h3] (L ⇒ E));
159 apply rule (⇒_i [h4] (E));
160 apply rule (RAA [h5] (⊥));
161 apply rule (∨_e (G∨¬L) [h6] (⊥) [h6] (⊥));
162         [ apply rule (⇒_e (¬E ⇒ G∨¬L) (¬E));
163             [ apply rule (discharge [h2]);
164             | apply rule (discharge [h5]);
165             ]
166         | apply rule (¬_e (¬E) (E));
167         [ apply rule (discharge [h5]);
168             | apply rule (⇒_e (F∧G ⇒ E) (F∧G));
169                [ apply rule (discharge [h1]);
170                | apply rule (∧_i (F) (G));
171                    [ apply rule (⇒_e (L⇒F) (L));
172                       [ apply rule (discharge [h3]);
173                       | apply rule (discharge [h4]);
174                       ]
175                    | apply rule (discharge [h6]);
176                    ]
177                ]
178             ]
179         | apply rule (¬_e (¬L) (L));
180             [ apply rule (discharge [h6]);
181             | apply rule (discharge [h4]);
182             ]
183         ]
184 (*END*)
185 qed.