]> matita.cs.unibo.it Git - helm.git/blob - matitaB/matita/doc/primer.txt
lambda_delta: partial commit ...
[helm.git] / matitaB / matita / doc / primer.txt
1                    ***********************************
2                    *                                 *
3                    *  A   M a t i t a   p r i m e r  *
4                    *                                 *
5                    *   (with useful ??? exercises)   *
6                    ***********************************
7
8 =================================
9 Learning to use the on-line help:
10 =================================
11 * Select the menu Help and then the menu Contents or press F1
12 * In the menu you can find the syntax for lambda terms and the syntax
13   and semantics of every tactic and tactical available in the system
14
15 =================================
16 Learning to type Unicode symbols:
17 =================================
18 * Unicode symbols are written like this: \lambda \eta \leq ...
19 * Optional: to get the gliph corresponding to the Unicode symbol,
20   type Alt+L (for ligature) just after the \something stuff
21 * Additional ligatures (use Alt+L to get the gliph)
22   :=   for   \def
23   ->   for   \to
24   =>   for   \Rightarrow
25   <=   for   \leq
26   >=   for   \geq
27 * Commonly used Unicode symbols:
28   \to     for  logical implication and function space
29   \forall
30   \exists
31   \Pi     for dependent product
32   \lambda
33   \land   for logical and, both on propositions and booleans
34   \lor    for logical or, both on propositions and booleans
35   \lnot   for logical not, both on propositions and booleans
36
37 ==============================
38 How to set up the environment:
39 ==============================
40 * Every file must start with a line like this:
41
42   set "baseuri" "cic:/matita/nat/plus/".
43
44   that says that every definition and lemma in the current file
45   will be put in the cic:/matita/nat/plus namespace.
46   For an exercise put in a foo.ma file, use the namespace
47   cic:/matita/foo/
48 * Files can start with inclusion lines like this:
49
50   include "nat/plus.ma".
51
52   This is required to activate the notation given in the nat/times.ma file.
53   If you do not include "nat/times.ma", you will still be able to use all
54   the definitions and lemmas given in "nat/plus.ma", but without the nice
55   infix '+' notation for addition.
56
57 ====================================
58 How to browse and search the library:
59 ====================================
60 * Open the menu View and then New CIC Browser. You will get a browser-like
61   window with integrated searching functionalities
62 * To explore the library, type the URI "cic:" in the URI field and start
63   browsing. Definitions will be rendered as such. Theorems will be rendered
64   in a declarative style even if initially produced in a procedural style.
65 * To get a nice notation for addition and natural numbers, put in your
66   script  include "nat/plus.ma"  and execute it. Then use the browser to
67   render cic:/matita/nat/plus/associative_plus.con. The declarative proof
68   you see is not fully expanded. Every time you see a "Proof" or a
69   "proof of xxx" you can click on it to expand the proof. Every constant and
70   symbol is an hyperlink. Follow the hyperlinks to see the definition of
71   natural numbers and addition.
72 * The home button visualizes in declarative style the proof under development.
73   It shows nothin when the system is not in proof mode.
74 * Theorems and definitions can be looked for by name using wildcards. Write
75   "*associative*" in the seach bar, select "Locate" and press Enter.
76   You will see the result list of URIs. Click on them to follow the hyperlink.
77 * If you know the exact statement of a theorem, but not its name, you can write
78   its statement in the search bar and select match. Try with
79   "\forall n,m:nat. n + m = m + n". Sometimes you can find a theorem that is
80   just close enough to what you were looking for. Try with
81   "\forall n:nat. O = n + O"  (O is the letter O, not the number 0)
82 * Sometimes you may want to obtain an hint on what theorems can be applied
83   to prove something. Write the statement to prove in the search bar and select
84   Hint. Try with "S O + O = O + S O". As before, you can get some useful
85   results that are not immediately usable in their current form.
86 * Sometimes you may want to look for the theorems and definitions that are
87   instances of a given statement. Write the statement in the search bar
88   using lambda abstractions in front to quantify the variables to be
89   instantiated. Then use Instance. Try with "\lambda n.\forall x:nat.x+n=x".
90
91 =====================
92 How to define things:
93 =====================
94 * Look in the manual for Syntax and then Definitions and declarations.
95   Often you can omit the types of binders if they can be inferred.
96   Use question marks "?" to ask the system to infer an argument of an
97   application. Non recursive definitions must be given using "definition".
98   Structural recursive definitions must be given using "let rec".
99   Try the following examples:
100
101   axiom f: nat \to nat
102
103   definition square := \lambda A:Type.\lambda f:A \to A. \lambda x. f (f x).
104
105   definition square_f : nat \to nat \def square ? f.
106
107   inductive tree (A:Type) : Type \def
108      Empty: tree A
109    | Cons: A \to tree A \to tree A \to tree A.
110
111   let rec size (A:Type) (t: tree A) on t : nat \def
112    match t with
113     [ Empty \Rightarrow O
114     | Cons _ l r \Rightarrow size ? l + size ? r
115     ].
116
117 ====================
118 How to prove things:
119 ====================
120 * Elementary proofs can be done by directly writing the lambda-terms
121   (as in Agda or Epigram). Try to complete the following proofs:
122
123   lemma ex1:
124    \forall A,B:Prop.
125      ((\forall X:Prop.X \to  X) \to  A \to  B) \to  A \to  B \def 
126     λA,B:Prop.λH. ...
127
128   lemma ex2: \forall n,m. m + n = m + (n + O) \def 
129     ...
130
131   Hint: to solve ex2 use eq_f and plus_n_O. Look for their types using
132   the browser.
133
134 * The usual way to write proofs is by using either the procedural style
135   (as in Coq and Isabelle) or the still experimental declarative style
136   (as in Isar and Mizar). Let's start with the declarative style.
137   Look in the manual for the following declarative tactics:
138
139     assume id:type.                            (* new assumption *)
140     suppose formula (id).                      (* new hypothesis *)
141     by lambda-term done.                       (* concludes the proof *)
142     by lambda-term we proved formula (id).     (* intermediate step *)
143     by _ done.                                 (* concludes the proof *)
144     by _ we proved formula (id).               (* intermediate step *)
145
146   Declarative tactics must always be terminated by a dot.
147   When automation fails (last two tactics), you can always help the system
148   by adding new intermediate steps or by writing the lambda-term by hand.
149
150   Prove again ex1 and ex2 in declarative style. A proof in declarative
151   style starts with
152
153     lemma id: formula.
154     theorem id: formula.
155
156   (the two forms are totally equivalent) and ends with
157
158     qed.
159
160   Hint: you can select well-formed sub-formulae in the sequents window,
161   copy them (using the Edit/Paste menu item or the contextual menu item)
162   and paste them in the text (using the Edit/Copy menu item or the
163   contextual menu item).
164
165 * The most used style to write proofs in Matita is the procedural one.
166   In the rest of this tutorial we will only present the procedural style.
167   Look in the manual for the following procedural tactics:
168
169     intros
170     apply lambda-term
171     autobatch                (* in the manual autobatch is called auto *)
172
173   Prove again ex1 and ex2 in procedural style. A proof in procedural style
174   starts and ends as a proof in declarative style. The two styles can be
175   mixed.
176
177 * Some tactics open multiple new goals. For instance, copy the following
178   lemma:
179
180   lemma ex3: \forall A,B:Prop. A \to B \to (A \land B) \land (A \land B).
181    intros;
182    split;
183
184   Look for the split tactic in the manual. The split tactic of the previous
185   script has created two new goals, both of type (A \land B). Notice that
186   the labels ?8 and ?9 of both goals are now in bold. This means that both
187   goals are currently active and that the next tactic will be applied to
188   both goals. The ";" tactical used after "intros" and "split" has exactly
189   this meaning: it activates all goals created by the previous tactic.
190   Look for it in the manual, then execute "split;" again. Now you can see
191   four active goals. The first and third one ask to prove A; the reamining
192   ones ask to prove B. To apply different tactics to the selected goal, we
193   need to branch over the selected goals. This is achieved by using the
194   tactical "[" (branching). Now type "[" and exec it. Only the first goal
195   is now active (in bold), and all the previously active goals have now
196   subscripts ranging from 1 to 4. Use the "apply H;" tactic to solve the goal.
197   No goals are now selected. Use the "|" (next goal) tactical to activate
198   the next goal. Since we are able to solve the new active goal and the
199   last goal at once, we want to select the two branches at the same time.
200   Use the "2,4:" tactical to select the goals having as subscripts 2 and 4.
201   Now solve the goals with "apply H1;" and select the last remaining goal
202   with "|". Solve the goal with "apply H;". Finally, close the branching
203   section using the tactical "]" and complete the proof with "qed.".
204   Look for all this tacticals in the manual. The "*:" tactical is also
205   useful: it is used just after a "[" or "|" tactical to activate all the
206   remaining goals with a subscript (i.e. all the goals in the innermost
207   branch).
208
209   If a tactic "T" opens multiple goals, then "T;" activates all the new
210   goals opened by "T". Instead "T." just activates the first goal opened
211   by "T", postponing the remaining goals without marking them with subscripts.
212   In case of doubt, always use "." in declarative scripts and only all the
213   other tacticals in procedural scripts.
214
215 ==========================
216 Computation and rewriting:
217 ==========================
218 * State the following theorem:
219
220   lemma ex4: \forall n,m. S (S n) + m = S (S (n + m)).
221
222   and introduce the hypotheses with "intros". To complete the proof, we
223   can simply compute "S (S n) + m" to obtain "S (S (n + m))". Using the
224   browser (click on the "+" hyperlink), look at the definition of addition:
225   since addition is defined by recursion on the first argument, and since
226   the first argument starts with two constructors "S", computation can be
227   made. Look for the "simplify" tactic in the manual and use it to
228   obtain a trivial equality. Solve the equality using "reflexivity", after
229   having looked for it in the manual.
230 * State the following theorem:
231
232   lemma ex5: \forall n,m. n + S (S m) = S (S (n + m)).
233
234   Try to use simplify to complete the proof as before. Why is "simplify"
235   not useful in this case? To progress in the proof we need a lemma
236   stating that "\forall n,m. S (n + m) = n + S m". Using the browser,
237   look for its name in the library. Since the lemma states an equality,
238   it is possible to use it to replace an instance of its left hand side
239   with an instance of its right hand side (or the other way around) in the
240   current sequent. Look for the "rewrite" tactic in the manual, and use
241   it to solve the exercise. There are two possible solutions: one only
242   uses rewriting from left to right ("rewrite >"), the other rewriting
243   from right to left ("rewrite <"). Find both of them.
244 * It may happen that "simplify" fails to yield the simplified form you
245   expect. In some situations, simplify can even make your goal more complex.
246   In these cases you can use the "change" tactic to convert the goal into
247   any other goal which is equivalent by computation only. State again
248   exercise ex4 and solve the goal without using "simplify" by means of
249   "change with (S (S (n + m)) = S (S (n + m))".
250 * Simplify does nothing to expand definitions that are not given by
251   structural recursion. To expand definition "X" in the goal, use the
252   "unfold X" tactic.
253
254   State the following lemma and use "unfold Not" to unfold the definition
255   of negation in terms of implication and False. Then complete the proof
256   of the theorem.
257
258   lemma ex6: \forall A:Prop. \lnot A \to A \to False.
259
260 * Sometimes you may be interested in simplifying, changing, unfolding or even
261   substituting (by means of rewrite) only a sub-expression of the
262   goal. Moreover, you may be interested in simplifying, changing, unfolding or
263   substituting a (sub-)expression of one hypothesis. Look in the manual
264   for these tactics: all of them have an optional argument that is a
265   pattern. You can generate a pattern by: 1) selecting the sub-expression you
266   want to act on in the sequent; 2) copying it (using the Edit/Copy menu
267   item or the contextual menu); 3) pasting it as a pattern using the
268   "Edit/Paste as pattern" menu item. Other tactics also have pattern arguments.
269   State and solve the following exercise:
270
271   lemma ex7: \forall n. (n + O) + (n + O) = n + (n + O).
272
273   The proof of the lemma must rewrite the conclusion of the sequent to
274   n + (n + O) = n + (n + O) and prove it by reflexivity.
275
276   Hint: use the browser to look for the theorem that proves
277    \forall n. n = n + O  and then use a pattern to control the behaviour
278    of "rewrite <".
279
280 ====================
281 Proofs by induction:
282 ====================
283 * Functions can be defined by structural recursion over arguments whose
284   type is inductive. To prove properties of these functions, a common
285   strategy is to proceed by induction over the recursive argument of the
286   function. To proceed by induction over an inductive argument "x", use
287   the "elim x" tactic.
288
289   Now include "nat/orders.ma" to activate the notation \leq.
290   Then state and prove the following lemma by induction over n:
291
292   lemma ex8: \forall n,m. m \leq n + m.
293
294   Hint 1: use "autobatch" to automatically prove trivial facts
295   Hint 2: "autobatch" never performs computations. In inductive proofs
296    you often need to "simplify" the inductive step before using
297    "autobatch". Indeed, the goal of proceeding by induction over the
298    recursive argument of a structural recursive definition is exactly
299    that of allowing computation both in the base and inductive cases.
300 * Using the browser, look at the definition of addition over natural
301   numbers. You can notice that all the parameters are fixed during
302   recursion, but the one we are recurring on. This is the reason why
303   it is possible to prove a property of addition using a simple induction
304   over the recursive argument. When other arguments of the structural
305   recursive functions change in recursive calls, it is necessary to
306   proceed by induction over generalized predicates where the additional
307   arguments are universally quantified.
308
309   Give the following tail recursive definition of addition between natural
310   numbers:
311
312   let rec plus' n m on n \def
313    match n with
314     [ O \Rightarrow m
315     | S n' \Rightarrow plus' n' (S m)
316     ].
317
318   Note that both parameters of plus' change during recursion.
319   Now state the following lemma, and try to prove it copying the proof
320   given for ex8 (that started with "intros; elim n;")
321
322   lemma ex9: \forall n,m. m \leq plus' n m.
323
324   Why is it impossible to prove the goal in this way? 
325   Now start the proof with "intros 1;", obtaining the generalized goal
326   "\forall m. m \leq plus' n m", and proceed by induction on n using
327   "elim n" as before. Complete the proof by means of simplification and
328   autobatch. Why is it now possible to prove the goal in this way?
329 * Sometimes it is not possible to obtain a generalized predicate using the
330   "intros n;" trick. However, it is always possible to generalize the
331   conclusion of the goal using the "generalize" tactic. Look for it in the
332   manual.
333
334   State again ex9 and find a proof that starts with
335   "intros; generalize in match m;".
336 * Some predicates can also be given as inductive predicates.
337   In this case, remember that you can proceed by induction over the
338   proof of the predicate. In particular, if H is a proof of
339   False/And/Or/Exists, then "elim H" corresponds to False/And/Or/Exists
340   elimination.
341
342   State and prove the following lemma:
343
344   lemma ex10: \forall A,B:Prop. A \lor (False \land B) \to A.
345
346 ====================
347 Proofs by inversion:
348 ====================
349 * Some predicates defined by induction are really defined as dependent
350   families of predicates. For instance, the \leq relation over natural
351   numbers is defined as follow:
352
353   inductive le (n:nat) : nat \to Prop \def
354      le_n: le n n
355    | le_S: \forall m. le n m \to le n (S m).
356
357   In Matita we say that the first parameter of le is a left parameter
358   (since it is at the left of the ":" sign), and that the second parameter
359   is a right parameter. Dependent families of predicates are inductive
360   definitions having a right parameter.
361
362   Now, consider a proof H of (le n E) for some expression E.
363   Differently from what happens in Agda, proceeding by elimination of H
364   (i.e. doing an "elim H") ignores the fact that the second argument of
365   the type of H was E. Equivalently, eliminating H of type (le n E) and
366   H' of type (le n E'), you obtain exactly the same new goals even if
367   E and E' are different.
368
369   State the following exercise and try to prove it by elimination of
370   the first premise (i.e. by doing an "intros; elim H;").
371
372   lemma ex11: \forall n. n \leq O \to n = O.
373
374   Why cannot you solve the exercise?
375   To exploit hypotheses whose type is inductive and whose right parameters
376   are instantiated, you can sometimes use the "inversion" tactic. Look
377   for it in the manual. Solve exercise ex11 starting with
378   "intros; inversion H;". As usual, autobatch is your friend to automate
379   the proof of trivial facts. However, autobatch never performs introduction
380   of hypotheses. Thus you often need to use "intros;" just before "autobatch;".
381   
382   Note: most of the time the "inductive hypotheses" generated by inversion
383   are completely useless. To remove a useless hypothesis H from the context
384   you can use the "clear H" tactic. Look for it in the manual.
385 * The "inversion" tactic is based on the t_inv lemma that is automatically
386   generated for every inductive family of predicates t. Look for the
387   t_inv lemma using the browser and study the clever trick (a funny
388   generalization) that is used to prove it. Brave students can try to
389   prove t_inv using the tactics described so far.
390   
391 =========================================================
392 Proofs by injectivity and discrimination of constructors:
393 =========================================================
394 * It is not unusual to obtain hypotheses of the form k1 args1 = k2 args2
395   where k1 and k2 are either equal or different constructors of the same
396   inductive type. If k1 and k2 are different constructors, the hypothesis
397   k1 args1 = k2 args2 is contradictory (discrimination of constructors);
398   otherwise we can derive the equality between corresponding arguments
399   in args1 and args2 (injectivity of constructors). Both operations are
400   performed by the "destruct" tactic. Look for it in the manual.
401
402   State and prove the following lemma using the destruct tactic twice:
403
404   lemma ex12: \forall n,m. \lnot (O = S n) \land (S (S n) = S (S m) \to n = m).
405 * The destruct tactic is able to prove things by means of a very clever trick
406   you already saw in the course by Coquand. Using the browser, look at the
407   proof of ex12. Brave students can try to prove ex12 without using the
408   destruct tactic.
409
410 ============================================
411 Conjecturing and proving intermediate facts:
412 ============================================
413 * Look for the "cut" tactic in the manual. It is used to assume a new fact
414   that needs to be proved later on in order to finish the goal. The name
415   "cut" comes from the cut rule of sequent calculus. As you know from theory,
416   the "cut" tactic is handy, but not necessary. Moreover, remember that you
417   can use axioms at your own risk to assume that some facts are provable.
418 * Given a term "t" that proves an implication or universal quantification,
419   it is possible to do forward reasoning in procedural style by means of
420   the "lapply (t args)" tactic that introduces the instantiated version of
421   the assumption in the context. Look for lapply in the manual. As the
422   "cut" tactic, lapply is quite handy, but not a necessary tactic.
423
424 =====================================================
425 Overloading existent notations and creating new ones:
426 =====================================================
427 * Mathematical notation is highly overloaded and full of ambiguities.
428   In Matita you can freely overload notations. The type system is used
429   to efficiently disambiguate formulae written by the user. In case no
430   interpretation of the formula makes sense, the user is faced with a set
431   of errors, corresponding to the different interpretations. In case multiple
432   interpretations make sense, the system asks the user a minimal amount of
433   questions to understand the intended meaning. Finally, the system remembers
434   the history of disambiguations and the answers of the user to 1) avoid
435   asking the user the same questions the next time the script is executed
436   2) avoid asking the user many questions by guessing the intended
437   interpretation according to recent history.
438
439   State the following lemma:
440
441   lemma foo:
442    \forall n,m:nat.
443     n = m \lor  (\lnot  n = m \land  ((leb n m \lor  leb m n) = true)).
444
445   Following the hyperlink, look at the type inferred for leb.
446   What interpretation Matita choosed for the first and second \lor sign?
447   Click on the hyperlinks of the two occurrences of \lor to confirm your answer.
448 * The basic idea behind overloading of mathematical notations is the following:
449   1. during pretty printing of formulae, the internal logical representation
450      of mathematical notions is mapped to MathML Content (an infinitary XML
451      based standard for the description of abstract syntax tree of mathematical
452      formulae). E.g. both Or (a predicate former) and orb (a function over
453      booleans) are mapped to the same MathML Content symbol "'or".
454   2. then, the MathML Content abstract syntax tree of a formula is mapped
455      to concrete syntax in MathML Presentation (a finitary XML based standard
456      for the description of concrete syntax trees of mathematical formulae).
457      E.g. the "'or x y" abstract syntax tree is mapped to "x \lor y".
458      The sequent window and the browser are based on a widget that is able
459      to render and interact MathML Presentation.
460   3. during parsing, the two phases are reversed: starting from the concrete
461      syntax tree (which is in plain Unicode text), the abstract syntax tree
462      in MathML Content is computed unambiguously. Then the abstract syntax tree
463      is efficiently translated to every well-typed logical representation.
464      E.g. "x \lor y" is first translated to "'or x y" and then interpreted as
465      "Or x y" or "orb x y", depending on which interpretation finally yields
466      well-typed lambda-terms.
467 * Using leb and cases analysis over booleans, define the two new non
468   recursive predicates:
469
470    min: nat \to nat \to nat
471    max: nat \to nat \to nat
472
473   Now overload the \land notation (associated to the "'and x y" MathML
474   Content formula) to work also for min:
475
476   interpretation "min of two natural numbers" 'and x y =
477    (cic:/matita/exercise/min.con x y).
478
479   Note: you have to substitute "cic:/matita/exercise/min.con" with the URI
480   determined by the baseuri you picked at the beginning of the file.
481
482   Overload also the notation for \lor (associated to "'or x y") in the
483   same way.
484
485   To check if everything works correctly, state the following lemma:
486
487   lemma foo: \forall b,n. (false \land b) = false \land (O \land n) = O.
488
489   How the system interpreted the instances of \land?
490
491   Now try to state the following ill-typed statement:
492
493   lemma foo: \forall b,n. (false \land O) = false \land (O \land n) = O.
494
495   Click on the three error locations before trying to read the errors.
496   Then click on the errors and read them in the error message window
497   (just below the sequent window). Which error messages did you expect?
498   Which ones make sense to you? Which error message do you consider to be
499   the "right" one? In what sense?
500 * Defining a new notation (i.e. associating to a new MathML Content tree
501   some MathML Presentation tree) is more involved.
502
503   Suppose we want to use the "a \middot b" notation for multiplication
504   between natural numbers. Type:
505
506   notation "hvbox(a break \middot b)"
507   non associative with precedence 55
508   for @{ 'times $a $b }.
509
510   interpretation "times over natural numbers" 'times x y =
511    (cic:/matita/nat/times/times.con x y).
512
513   To check if everything was correct, state the following lemma:
514
515   lemma foo: \forall n. n \middot O = O.
516
517   The "hvbox (a break \middot b)" contains more information than just
518   "a \middot b". The "hvbox" tells the system to write "a", "\middot" and
519   "b" in an horizontal row if there is enough space, or vertically otherwise.
520   The "break" keyword tells the system where to break the formula in case
521   of need. The syntax for defining new notations is not documented in the
522   manual yet.
523
524 =====================================
525 Using notions without including them:
526 =====================================
527 * Using the browser, look for the "fact" function.
528   Notice that it is defined in the "cic:/matita/nat/factorial" namespace
529   that has not been included yet. Now state the following lemma:
530
531   lemma fact_O_S_O: fact O = 1.
532
533   Note that Matita automatically introduces in the script some informations
534   to remember where "fact" comes from. However, you do not get the nice
535   notation for factorial. Remove the lines automatically added by Matita
536   and replace them with
537
538   include "nat/factorial.ma"
539
540   before stating again the lemma. Now the lines are no longer added and you
541   get the nice notation. In the future we plan to activate all notation without
542   the need of including anything.
543
544 =============================
545 A relatively simple exercise:
546 =============================
547 * Start from an empty .ma file, change the baseuri and include the following
548   files for auxiliary notation:
549
550   include "nat/plus.ma".
551   include "nat/compare.ma".
552   include "list/sort.ma".
553   include "datatypes/constructors.ma".
554
555   In particular, the following notations for lists and pairs are introduced:
556    []                    is the empty list
557    hd::tl                is the list obtained putting a new element hd in
558                          front of the list tl
559    @                     list concatenation
560    \times                is the cartesian product
561    \langle l,r \rangle   is the pair (l,r)
562 * Define an inductive data type of propositional formulae built from
563   a denumerable set of atoms, conjunction, disjunction, negation, truth and
564   falsity (no primitive implication).
565
566   Hint: complete the following inductive definition.
567
568   inductive Formula : Type \def 
569    FTrue: Formula
570  | FFalse: Formula
571  | FAtom: nat \to  Formula
572  | FAnd: Formula \to  Formula \to  Formula
573  | ...
574 * Define a classical interpretation as a function from atom indexes to booleans:
575
576   definition interp \def  nat \to  bool.
577 * Define by structural recursion over formulas an evaluation function
578   parameterized over an interpretation.
579
580   Hint: complete the following definition. The order of the
581   different cases should be exactly the order of the constructors in the
582   definition of the inductive type.
583
584   let rec eval (i:interp) F on F : bool \def
585    match F with
586     [ FTrue \Rightarrow true
587     | FFalse \Rightarrow false
588     | FAtom n \Rightarrow interp n
589     | ...
590 * We are interested in formulas in a particular normal form where only atoms
591   can be negated. Define the "being in normal form" not_nf predicate as an
592   inductive predicate with one right parameter.
593
594   Hint: complete the following definition.
595
596   inductive not_nf : Formula \to  Prop \def 
597       NTrue: not_nf FTrue
598     | NFalse: not_nf FFalse
599     | NAtom: \forall n. not_nf (FAtom n)
600     ...
601     | NNot: \forall n. not_nf (FNot (FAtom n))
602 * We want to describe a procedure that reduces a formula to an equivalent
603   not_nf normal form. Define two mutually recursive functions elim_not and
604   negate over formulas that respectively 1: put the formula in normal form
605   and 2: put the negated of a formula in normal form.
606
607   Hint: complete the following definition.
608
609   let rec negate F \def 
610     match F with
611      [ FTrue \Rightarrow  FFalse
612      | FFalse \Rightarrow  FTrue
613      | ...
614      | FNot f \Rightarrow  elim_not f]
615    and elim_not F \def 
616     match F with
617      [ FTrue \Rightarrow  FTrue
618      | FFalse \Rightarrow  FFalse
619      | ...
620      | FNot f \Rightarrow  negate f
621      ].
622
623   Why is not possible to only define elim_not by changing the FNot case
624   to "FNot f \Rightarrow elim_not (FNot f)"?
625 * Prove that the procedures just given correctly produce normal forms.
626   I.e. prove the following theorem.
627
628   theorem not_nf_elim_not:
629    \forall F.not_nf (elim_not F) \land  not_nf (negate F).
630
631   Why is not possible to prove that one function produces normal forms
632   without proving the other part of the statement? Try and see what happens.
633
634   Hint: use the "n1,...,nm:" tactical to activate similar cases and solve
635   all of them at once.
636 * Finally prove that the procedures just given preserve the semantics of the
637   formula. I.e. prove the following theorem.
638
639   theorem eq_eval_elim_not_eval:
640    \forall i,F.
641     eval i (elim_not F) = eval i F \land  eval i (negate F) = eval i (FNot F).
642
643   Hint: you may need to prove (or assume axiomatically) additional lemmas on
644   booleans such as the two demorgan laws.
645
646 ================================
647 A moderately difficult exercise:
648 ================================
649 * Consider the inductive type of propositional formulae of the previous
650   exercise. Describe with an inductive type the set of well types derivation
651   trees for classical propositional sequent calculus without implication.
652   
653   Hint: complete the following definitions.
654
655   definition sequent \def  (list Formula) × (list Formula).
656
657   inductive derive: sequent \to  Prop \def 
658      ExchangeL:
659       \forall l,l1,l2,f. derive 〈f::l1@l2,l〉 \to  derive 〈l1 @ [f] @ l2,l〉
660    | ExchangeR: ...
661    | Axiom: \forall l1,l2,f. derive 〈f::l1, f::l2〉
662    | TrueR: \forall l1,l2. derive 〈l1,FTrue::l2〉
663    | ...
664    | AndR: \forall l1,l2,f1,f2.
665       derive 〈l1,f1::l2〉 \to  derive 〈l1,f2::l2〉 \to 
666        derive 〈l1,FAnd f1 f2::l2〉
667    | ...
668
669   Note that while the exchange rules are explicit, weakening and contraction
670   are embedded in the other rules.
671 * Define two functions that transform the left hand side and the right hand
672   side of a sequent into a logically equivalent formula obtained by making
673   the conjunction (respectively disjunction) of all formulae in the
674   left hand side (respectively right hand side). From those, define a function
675   that folds a sequent into a logically equivalent formula obtained by
676   negating the conjunction of all formulae in the left hand side and putting
677   the result in disjunction with the disjunction of all formuale in the
678   right hand side.
679 * Define a predicate is_tautology for formulae.
680 * Prove the soundness of the sequent calculus. I.e. prove
681
682   theorem soundness:
683    \forall F. derive F \to  is_tautology (formula_of_sequent F).
684
685   Hint: you may need to axiomatically assume or prove several lemmas on
686   booleans that are missing from the library. You also need to prove some
687   lemmas on the functions you have just defined.
688
689 ==========================
690 A long and tough exercise:
691 ==========================
692 * Prove the completeness of the sequent calculus studied in the previous
693   exercise. I.e. prove
694
695   theorem completeness:
696    \forall S. is_tautology (formula_of_sequent S) \to  derive S.
697
698   Hint: the proof is by induction on the size of the sequent, defined as the
699   size of all formulae in the sequent. The size of a formula is the number of
700   unary and binary connectives in the formula. In the inductive case you have
701   to pick one formula with a positive size, bring it in front using the
702   exchange rule, and construct the tree applying the appropriate elimination
703   rules. The subtrees are obtained by inductive hypotheses. In the base case,
704   since the formula is a tautology, either there is a False formula in the
705   left hand side of the sequent, or there is a True formula in the right hand
706   side, or there is a formula both in the left and right hand sides. In all
707   cases you can construct a tree by applying once or twice the exchange rules
708   and once the FalseL/TrueR/Axiom rule. The computational content of the proof
709   is a search strategy.
710
711   The main difficulty of the proof is to proceed by induction on something (the
712   size of the sequent) that does not reflect the structure of the sequent (made
713   of a pair of lists). Moreover, from the fact that the size of the sequent is
714   greater than 0, you need to detect the exact positions of a non atomic
715   formula in the sequent and this needs to be done by structural recursion
716   on the appropriate side, which is a list. Finally, from the fact that a
717   sequent of size 0 is a tautology, you need to detect the False premise or
718   the True conclusion or the two occurrences of a formula that form an axiom,
719   excluding all other cases. This last proof is already quite involved, and
720   finding the right inductive predicate is quite challenging.