--- /dev/null
+ ***********************************
+ * *
+ * A M a t i t a p r i m e r *
+ * *
+ * (with useful ??? exercises) *
+ ***********************************
+
+=================================
+Learning to use the on-line help:
+=================================
+* Select the menu Help and then the menu Contents or press F1
+* In the menu you can find the syntax for lambda terms and the syntax
+ and semantics of every tactic and tactical available in the system
+
+=================================
+Learning to type Unicode symbols:
+=================================
+* Unicode symbols are written like this: \lambda \eta \leq ...
+* Optional: to get the gliph corresponding to the Unicode symbol,
+ type Alt+L (for ligature) just after the \something stuff
+* Additional ligatures (use Alt+L to get the gliph)
+ := for \def
+ -> for \to
+ => for \Rightarrow
+ <= for \leq
+ >= for \geq
+* Commonly used Unicode symbols:
+ \to for logical implication and function space
+ \forall
+ \exists
+ \Pi for dependent product
+ \lambda
+ \land for logical and, both on propositions and booleans
+ \lor for logical or, both on propositions and booleans
+ \lnot for logical not, both on propositions and booleans
+
+==============================
+How to set up the environment:
+==============================
+* Every file must start with a line like this:
+
+ set "baseuri" "cic:/matita/nat/plus/".
+
+ that says that every definition and lemma in the current file
+ will be put in the cic:/matita/nat/plus namespace.
+ For an exercise put in a foo.ma file, use the namespace
+ cic:/matita/foo/
+* Files can start with inclusion lines like this:
+
+ include "nat/plus.ma".
+
+ This is required to activate the notation given in the nat/times.ma file.
+ If you do not include "nat/times.ma", you will still be able to use all
+ the definitions and lemmas given in "nat/plus.ma", but without the nice
+ infix '+' notation for addition.
+
+====================================
+How to browse and search the library:
+====================================
+* Open the menu View and then New CIC Browser. You will get a browser-like
+ window with integrated searching functionalities
+* To explore the library, type the URI "cic:" in the URI field and start
+ browsing. Definitions will be rendered as such. Theorems will be rendered
+ in a declarative style even if initially produced in a procedural style.
+* To get a nice notation for addition and natural numbers, put in your
+ script include "nat/plus.ma" and execute it. Then use the browser to
+ render cic:/matita/nat/plus/associative_plus.con. The declarative proof
+ you see is not fully expanded. Every time you see a "Proof" or a
+ "proof of xxx" you can click on it to expand the proof. Every constant and
+ symbol is an hyperlink. Follow the hyperlinks to see the definition of
+ natural numbers and addition.
+* The home button visualizes in declarative style the proof under development.
+ It shows nothin when the system is not in proof mode.
+* Theorems and definitions can be looked for by name using wildcards. Write
+ "*associative*" in the seach bar, select "Locate" and press Enter.
+ You will see the result list of URIs. Click on them to follow the hyperlink.
+* If you know the exact statement of a theorem, but not its name, you can write
+ its statement in the search bar and select match. Try with
+ "\forall n,m:nat. n + m = m + n". Sometimes you can find a theorem that is
+ just close enough to what you were looking for. Try with
+ "\forall n:nat. O = n + O" (O is the letter O, not the number 0)
+* Sometimes you may want to obtain an hint on what theorems can be applied
+ to prove something. Write the statement to prove in the search bar and select
+ Hint. Try with "S O + O = O + S O". As before, you can get some useful
+ results that are not immediately usable in their current form.
+* Sometimes you may want to look for the theorems and definitions that are
+ instances of a given statement. Write the statement in the search bar
+ using lambda abstractions in front to quantify the variables to be
+ instantiated. Then use Instance. Try with "\lambda n.\forall x:nat.x+n=x".
+
+=====================
+How to define things:
+=====================
+* Look in the manual for Syntax and then Definitions and declarations.
+ Often you can omit the types of binders if they can be inferred.
+ Use question marks "?" to ask the system to infer an argument of an
+ application. Non recursive definitions must be given using "definition".
+ Structural recursive definitions must be given using "let rec".
+ Try the following examples:
+
+ axiom f: nat \to nat
+
+ definition square := \lambda A:Type.\lambda f:A \to A. \lambda x. f (f x).
+
+ definition square_f : nat \to nat \def square ? f.
+
+ inductive tree (A:Type) : Type \def
+ Empty: tree A
+ | Cons: A \to tree A \to tree A \to tree A.
+
+ let rec size (A:Type) (t: tree A) on t : nat \def
+ match t with
+ [ Empty \Rightarrow O
+ | Cons _ l r \Rightarrow size ? l + size ? r
+ ].
+
+====================
+How to prove things:
+====================
+* Elementary proofs can be done by directly writing the lambda-terms
+ (as in Agda or Epigram). Try to complete the following proofs:
+
+ lemma ex1:
+ \forall A,B:Prop.
+ ((\forall X:Prop.X \to X) \to A \to B) \to A \to B \def
+ λA,B:Prop.λH. ...
+
+ lemma ex2: \forall n,m. m + n = m + (n + O) \def
+ ...
+
+ Hint: to solve ex2 use eq_f and plus_n_O. Look for their types using
+ the browser.
+
+* The usual way to write proofs is by using either the procedural style
+ (as in Coq and Isabelle) or the still experimental declarative style
+ (as in Isar and Mizar). Let's start with the declarative style.
+ Look in the manual for the following declarative tactics:
+
+ assume id:type. (* new assumption *)
+ suppose formula (id). (* new hypothesis *)
+ by lambda-term done. (* concludes the proof *)
+ by lambda-term we proved formula (id). (* intermediate step *)
+ by _ done. (* concludes the proof *)
+ by _ we proved formula (id). (* intermediate step *)
+
+ Declarative tactics must always be terminated by a dot.
+ When automation fails (last two tactics), you can always help the system
+ by adding new intermediate steps or by writing the lambda-term by hand.
+
+ Prove again ex1 and ex2 in declarative style. A proof in declarative
+ style starts with
+
+ lemma id: formula.
+ theorem id: formula.
+
+ (the two forms are totally equivalent) and ends with
+
+ qed.
+
+ Hint: you can select well-formed sub-formulae in the sequents window,
+ copy them (using the Edit/Paste menu item or the contextual menu item)
+ and paste them in the text (using the Edit/Copy menu item or the
+ contextual menu item).
+
+* The most used style to write proofs in Matita is the procedural one.
+ In the rest of this tutorial we will only present the procedural style.
+ Look in the manual for the following procedural tactics:
+
+ intros
+ apply lambda-term
+ autobatch (* in the manual autobatch is called auto *)
+
+ Prove again ex1 and ex2 in procedural style. A proof in procedural style
+ starts and ends as a proof in declarative style. The two styles can be
+ mixed.
+
+* Some tactics open multiple new goals. For instance, copy the following
+ lemma:
+
+ lemma ex3: \forall A,B:Prop. A \to B \to (A \land B) \land (A \land B).
+ intros;
+ split;
+
+ Look for the split tactic in the manual. The split tactic of the previous
+ script has created two new goals, both of type (A \land B). Notice that
+ the labels ?8 and ?9 of both goals are now in bold. This means that both
+ goals are currently active and that the next tactic will be applied to
+ both goals. The ";" tactical used after "intros" and "split" has exactly
+ this meaning: it activates all goals created by the previous tactic.
+ Look for it in the manual, then execute "split;" again. Now you can see
+ four active goals. The first and third one ask to prove A; the reamining
+ ones ask to prove B. To apply different tactics to the selected goal, we
+ need to branch over the selected goals. This is achieved by using the
+ tactical "[" (branching). Now type "[" and exec it. Only the first goal
+ is now active (in bold), and all the previously active goals have now
+ subscripts ranging from 1 to 4. Use the "apply H;" tactic to solve the goal.
+ No goals are now selected. Use the "|" (next goal) tactical to activate
+ the next goal. Since we are able to solve the new active goal and the
+ last goal at once, we want to select the two branches at the same time.
+ Use the "2,4:" tactical to select the goals having as subscripts 2 and 4.
+ Now solve the goals with "apply H1;" and select the last remaining goal
+ with "|". Solve the goal with "apply H;". Finally, close the branching
+ section using the tactical "]" and complete the proof with "qed.".
+ Look for all this tacticals in the manual. The "*:" tactical is also
+ useful: it is used just after a "[" or "|" tactical to activate all the
+ remaining goals with a subscript (i.e. all the goals in the innermost
+ branch).
+
+ If a tactic "T" opens multiple goals, then "T;" activates all the new
+ goals opened by "T". Instead "T." just activates the first goal opened
+ by "T", postponing the remaining goals without marking them with subscripts.
+ In case of doubt, always use "." in declarative scripts and only all the
+ other tacticals in procedural scripts.
+
+==========================
+Computation and rewriting:
+==========================
+* State the following theorem:
+
+ lemma ex4: \forall n,m. S (S n) + m = S (S (n + m)).
+
+ and introduce the hypotheses with "intros". To complete the proof, we
+ can simply compute "S (S n) + m" to obtain "S (S (n + m))". Using the
+ browser (click on the "+" hyperlink), look at the definition of addition:
+ since addition is defined by recursion on the first argument, and since
+ the first argument starts with two constructors "S", computation can be
+ made. Look for the "simplify" tactic in the manual and use it to
+ obtain a trivial equality. Solve the equality using "reflexivity", after
+ having looked for it in the manual.
+* State the following theorem:
+
+ lemma ex5: \forall n,m. n + S (S m) = S (S (n + m)).
+
+ Try to use simplify to complete the proof as before. Why is "simplify"
+ not useful in this case? To progress in the proof we need a lemma
+ stating that "\forall n,m. S (n + m) = n + S m". Using the browser,
+ look for its name in the library. Since the lemma states an equality,
+ it is possible to use it to replace an instance of its left hand side
+ with an instance of its right hand side (or the other way around) in the
+ current sequent. Look for the "rewrite" tactic in the manual, and use
+ it to solve the exercise. There are two possible solutions: one only
+ uses rewriting from left to right ("rewrite >"), the other rewriting
+ from right to left ("rewrite <"). Find both of them.
+* It may happen that "simplify" fails to yield the simplified form you
+ expect. In some situations, simplify can even make your goal more complex.
+ In these cases you can use the "change" tactic to convert the goal into
+ any other goal which is equivalent by computation only. State again
+ exercise ex4 and solve the goal without using "simplify" by means of
+ "change with (S (S (n + m)) = S (S (n + m))".
+* Simplify does nothing to expand definitions that are not given by
+ structural recursion. To expand definition "X" in the goal, use the
+ "unfold X" tactic.
+
+ State the following lemma and use "unfold Not" to unfold the definition
+ of negation in terms of implication and False. Then complete the proof
+ of the theorem.
+
+ lemma ex6: \forall A:Prop. \lnot A \to A \to False.
+
+* Sometimes you may be interested in simplifying, changing, unfolding or even
+ substituting (by means of rewrite) only a sub-expression of the
+ goal. Moreover, you may be interested in simplifying, changing, unfolding or
+ substituting a (sub-)expression of one hypothesis. Look in the manual
+ for these tactics: all of them have an optional argument that is a
+ pattern. You can generate a pattern by: 1) selecting the sub-expression you
+ want to act on in the sequent; 2) copying it (using the Edit/Copy menu
+ item or the contextual menu); 3) pasting it as a pattern using the
+ "Edit/Paste as pattern" menu item. Other tactics also have pattern arguments.
+ State and solve the following exercise:
+
+ lemma ex7: \forall n. (n + O) + (n + O) = n + (n + O).
+
+ The proof of the lemma must rewrite the conclusion of the sequent to
+ n + (n + O) = n + (n + O) and prove it by reflexivity.
+
+ Hint: use the browser to look for the theorem that proves
+ \forall n. n = n + O and then use a pattern to control the behaviour
+ of "rewrite <".
+
+====================
+Proofs by induction:
+====================
+* Functions can be defined by structural recursion over arguments whose
+ type is inductive. To prove properties of these functions, a common
+ strategy is to proceed by induction over the recursive argument of the
+ function. To proceed by induction over an inductive argument "x", use
+ the "elim x" tactic.
+
+ Now include "nat/orders.ma" to activate the notation \leq.
+ Then state and prove the following lemma by induction over n:
+
+ lemma ex8: \forall n,m. m \leq n + m.
+
+ Hint 1: use "autobatch" to automatically prove trivial facts
+ Hint 2: "autobatch" never performs computations. In inductive proofs
+ you often need to "simplify" the inductive step before using
+ "autobatch". Indeed, the goal of proceeding by induction over the
+ recursive argument of a structural recursive definition is exactly
+ that of allowing computation both in the base and inductive cases.
+* Using the browser, look at the definition of addition over natural
+ numbers. You can notice that all the parameters are fixed during
+ recursion, but the one we are recurring on. This is the reason why
+ it is possible to prove a property of addition using a simple induction
+ over the recursive argument. When other arguments of the structural
+ recursive functions change in recursive calls, it is necessary to
+ proceed by induction over generalized predicates where the additional
+ arguments are universally quantified.
+
+ Give the following tail recursive definition of addition between natural
+ numbers:
+
+ let rec plus' n m on n \def
+ match n with
+ [ O \Rightarrow m
+ | S n' \Rightarrow plus' n' (S m)
+ ].
+
+ Note that both parameters of plus' change during recursion.
+ Now state the following lemma, and try to prove it copying the proof
+ given for ex8 (that started with "intros; elim n;")
+
+ lemma ex9: \forall n,m. m \leq plus' n m.
+
+ Why is it impossible to prove the goal in this way?
+ Now start the proof with "intros 1;", obtaining the generalized goal
+ "\forall m. m \leq plus' n m", and proceed by induction on n using
+ "elim n" as before. Complete the proof by means of simplification and
+ autobatch. Why is it now possible to prove the goal in this way?
+* Sometimes it is not possible to obtain a generalized predicate using the
+ "intros n;" trick. However, it is always possible to generalize the
+ conclusion of the goal using the "generalize" tactic. Look for it in the
+ manual.
+
+ State again ex9 and find a proof that starts with
+ "intros; generalize in match m;".
+* Some predicates can also be given as inductive predicates.
+ In this case, remember that you can proceed by induction over the
+ proof of the predicate. In particular, if H is a proof of
+ False/And/Or/Exists, then "elim H" corresponds to False/And/Or/Exists
+ elimination.
+
+ State and prove the following lemma:
+
+ lemma ex10: \forall A,B:Prop. A \lor (False \land B) \to A.
+
+====================
+Proofs by inversion:
+====================
+* Some predicates defined by induction are really defined as dependent
+ families of predicates. For instance, the \leq relation over natural
+ numbers is defined as follow:
+
+ inductive le (n:nat) : nat \to Prop \def
+ le_n: le n n
+ | le_S: \forall m. le n m \to le n (S m).
+
+ In Matita we say that the first parameter of le is a left parameter
+ (since it is at the left of the ":" sign), and that the second parameter
+ is a right parameter. Dependent families of predicates are inductive
+ definitions having a right parameter.
+
+ Now, consider a proof H of (le n E) for some expression E.
+ Differently from what happens in Agda, proceeding by elimination of H
+ (i.e. doing an "elim H") ignores the fact that the second argument of
+ the type of H was E. Equivalently, eliminating H of type (le n E) and
+ H' of type (le n E'), you obtain exactly the same new goals even if
+ E and E' are different.
+
+ State the following exercise and try to prove it by elimination of
+ the first premise (i.e. by doing an "intros; elim H;").
+
+ lemma ex11: \forall n. n \leq O \to n = O.
+
+ Why cannot you solve the exercise?
+ To exploit hypotheses whose type is inductive and whose right parameters
+ are instantiated, you can sometimes use the "inversion" tactic. Look
+ for it in the manual. Solve exercise ex11 starting with
+ "intros; inversion H;". As usual, autobatch is your friend to automate
+ the proof of trivial facts. However, autobatch never performs introduction
+ of hypotheses. Thus you often need to use "intros;" just before "autobatch;".
+
+ Note: most of the time the "inductive hypotheses" generated by inversion
+ are completely useless. To remove a useless hypothesis H from the context
+ you can use the "clear H" tactic. Look for it in the manual.
+* The "inversion" tactic is based on the t_inv lemma that is automatically
+ generated for every inductive family of predicates t. Look for the
+ t_inv lemma using the browser and study the clever trick (a funny
+ generalization) that is used to prove it. Brave students can try to
+ prove t_inv using the tactics described so far.
+
+=========================================================
+Proofs by injectivity and discrimination of constructors:
+=========================================================
+* It is not unusual to obtain hypotheses of the form k1 args1 = k2 args2
+ where k1 and k2 are either equal or different constructors of the same
+ inductive type. If k1 and k2 are different constructors, the hypothesis
+ k1 args1 = k2 args2 is contradictory (discrimination of constructors);
+ otherwise we can derive the equality between corresponding arguments
+ in args1 and args2 (injectivity of constructors). Both operations are
+ performed by the "destruct" tactic. Look for it in the manual.
+
+ State and prove the following lemma using the destruct tactic twice:
+
+ lemma ex12: \forall n,m. \lnot (O = S n) \land (S (S n) = S (S m) \to n = m).
+* The destruct tactic is able to prove things by means of a very clever trick
+ you already saw in the course by Coquand. Using the browser, look at the
+ proof of ex12. Brave students can try to prove ex12 without using the
+ destruct tactic.
+
+============================================
+Conjecturing and proving intermediate facts:
+============================================
+* Look for the "cut" tactic in the manual. It is used to assume a new fact
+ that needs to be proved later on in order to finish the goal. The name
+ "cut" comes from the cut rule of sequent calculus. As you know from theory,
+ the "cut" tactic is handy, but not necessary. Moreover, remember that you
+ can use axioms at your own risk to assume that some facts are provable.
+* Given a term "t" that proves an implication or universal quantification,
+ it is possible to do forward reasoning in procedural style by means of
+ the "lapply (t args)" tactic that introduces the instantiated version of
+ the assumption in the context. Look for lapply in the manual. As the
+ "cut" tactic, lapply is quite handy, but not a necessary tactic.
+
+=====================================================
+Overloading existent notations and creating new ones:
+=====================================================
+* Mathematical notation is highly overloaded and full of ambiguities.
+ In Matita you can freely overload notations. The type system is used
+ to efficiently disambiguate formulae written by the user. In case no
+ interpretation of the formula makes sense, the user is faced with a set
+ of errors, corresponding to the different interpretations. In case multiple
+ interpretations make sense, the system asks the user a minimal amount of
+ questions to understand the intended meaning. Finally, the system remembers
+ the history of disambiguations and the answers of the user to 1) avoid
+ asking the user the same questions the next time the script is executed
+ 2) avoid asking the user many questions by guessing the intended
+ interpretation according to recent history.
+
+ State the following lemma:
+
+ lemma foo:
+ \forall n,m:nat.
+ n = m \lor (\lnot n = m \land ((leb n m \lor leb m n) = true)).
+
+ Following the hyperlink, look at the type inferred for leb.
+ What interpretation Matita choosed for the first and second \lor sign?
+ Click on the hyperlinks of the two occurrences of \lor to confirm your answer.
+* The basic idea behind overloading of mathematical notations is the following:
+ 1. during pretty printing of formulae, the internal logical representation
+ of mathematical notions is mapped to MathML Content (an infinitary XML
+ based standard for the description of abstract syntax tree of mathematical
+ formulae). E.g. both Or (a predicate former) and orb (a function over
+ booleans) are mapped to the same MathML Content symbol "'or".
+ 2. then, the MathML Content abstract syntax tree of a formula is mapped
+ to concrete syntax in MathML Presentation (a finitary XML based standard
+ for the description of concrete syntax trees of mathematical formulae).
+ E.g. the "'or x y" abstract syntax tree is mapped to "x \lor y".
+ The sequent window and the browser are based on a widget that is able
+ to render and interact MathML Presentation.
+ 3. during parsing, the two phases are reversed: starting from the concrete
+ syntax tree (which is in plain Unicode text), the abstract syntax tree
+ in MathML Content is computed unambiguously. Then the abstract syntax tree
+ is efficiently translated to every well-typed logical representation.
+ E.g. "x \lor y" is first translated to "'or x y" and then interpreted as
+ "Or x y" or "orb x y", depending on which interpretation finally yields
+ well-typed lambda-terms.
+* Using leb and cases analysis over booleans, define the two new non
+ recursive predicates:
+
+ min: nat \to nat \to nat
+ max: nat \to nat \to nat
+
+ Now overload the \land notation (associated to the "'and x y" MathML
+ Content formula) to work also for min:
+
+ interpretation "min of two natural numbers" 'and x y =
+ (cic:/matita/exercise/min.con x y).
+
+ Note: you have to substitute "cic:/matita/exercise/min.con" with the URI
+ determined by the baseuri you picked at the beginning of the file.
+
+ Overload also the notation for \lor (associated to "'or x y") in the
+ same way.
+
+ To check if everything works correctly, state the following lemma:
+
+ lemma foo: \forall b,n. (false \land b) = false \land (O \land n) = O.
+
+ How the system interpreted the instances of \land?
+
+ Now try to state the following ill-typed statement:
+
+ lemma foo: \forall b,n. (false \land O) = false \land (O \land n) = O.
+
+ Click on the three error locations before trying to read the errors.
+ Then click on the errors and read them in the error message window
+ (just below the sequent window). Which error messages did you expect?
+ Which ones make sense to you? Which error message do you consider to be
+ the "right" one? In what sense?
+* Defining a new notation (i.e. associating to a new MathML Content tree
+ some MathML Presentation tree) is more involved.
+
+ Suppose we want to use the "a \middot b" notation for multiplication
+ between natural numbers. Type:
+
+ notation "hvbox(a break \middot b)"
+ non associative with precedence 55
+ for @{ 'times $a $b }.
+
+ interpretation "times over natural numbers" 'times x y =
+ (cic:/matita/nat/times/times.con x y).
+
+ To check if everything was correct, state the following lemma:
+
+ lemma foo: \forall n. n \middot O = O.
+
+ The "hvbox (a break \middot b)" contains more information than just
+ "a \middot b". The "hvbox" tells the system to write "a", "\middot" and
+ "b" in an horizontal row if there is enough space, or vertically otherwise.
+ The "break" keyword tells the system where to break the formula in case
+ of need. The syntax for defining new notations is not documented in the
+ manual yet.
+
+=====================================
+Using notions without including them:
+=====================================
+* Using the browser, look for the "fact" function.
+ Notice that it is defined in the "cic:/matita/nat/factorial" namespace
+ that has not been included yet. Now state the following lemma:
+
+ lemma fact_O_S_O: fact O = 1.
+
+ Note that Matita automatically introduces in the script some informations
+ to remember where "fact" comes from. However, you do not get the nice
+ notation for factorial. Remove the lines automatically added by Matita
+ and replace them with
+
+ include "nat/factorial.ma"
+
+ before stating again the lemma. Now the lines are no longer added and you
+ get the nice notation. In the future we plan to activate all notation without
+ the need of including anything.
+
+=============================
+A relatively simple exercise:
+=============================
+* Start from an empty .ma file, change the baseuri and include the following
+ files for auxiliary notation:
+
+ include "nat/plus.ma".
+ include "nat/compare.ma".
+ include "list/sort.ma".
+ include "datatypes/constructors.ma".
+
+ In particular, the following notations for lists and pairs are introduced:
+ [] is the empty list
+ hd::tl is the list obtained putting a new element hd in
+ front of the list tl
+ @ list concatenation
+ \times is the cartesian product
+ \langle l,r \rangle is the pair (l,r)
+* Define an inductive data type of propositional formulae built from
+ a denumerable set of atoms, conjunction, disjunction, negation, truth and
+ falsity (no primitive implication).
+
+ Hint: complete the following inductive definition.
+
+ inductive Formula : Type \def
+ FTrue: Formula
+ | FFalse: Formula
+ | FAtom: nat \to Formula
+ | FAnd: Formula \to Formula \to Formula
+ | ...
+* Define a classical interpretation as a function from atom indexes to booleans:
+
+ definition interp \def nat \to bool.
+* Define by structural recursion over formulas an evaluation function
+ parameterized over an interpretation.
+
+ Hint: complete the following definition. The order of the
+ different cases should be exactly the order of the constructors in the
+ definition of the inductive type.
+
+ let rec eval (i:interp) F on F : bool \def
+ match F with
+ [ FTrue \Rightarrow true
+ | FFalse \Rightarrow false
+ | FAtom n \Rightarrow interp n
+ | ...
+* We are interested in formulas in a particular normal form where only atoms
+ can be negated. Define the "being in normal form" not_nf predicate as an
+ inductive predicate with one right parameter.
+
+ Hint: complete the following definition.
+
+ inductive not_nf : Formula \to Prop \def
+ NTrue: not_nf FTrue
+ | NFalse: not_nf FFalse
+ | NAtom: \forall n. not_nf (FAtom n)
+ ...
+ | NNot: \forall n. not_nf (FNot (FAtom n))
+* We want to describe a procedure that reduces a formula to an equivalent
+ not_nf normal form. Define two mutually recursive functions elim_not and
+ negate over formulas that respectively 1: put the formula in normal form
+ and 2: put the negated of a formula in normal form.
+
+ Hint: complete the following definition.
+
+ let rec negate F \def
+ match F with
+ [ FTrue \Rightarrow FFalse
+ | FFalse \Rightarrow FTrue
+ | ...
+ | FNot f \Rightarrow elim_not f]
+ and elim_not F \def
+ match F with
+ [ FTrue \Rightarrow FTrue
+ | FFalse \Rightarrow FFalse
+ | ...
+ | FNot f \Rightarrow negate f
+ ].
+
+ Why is not possible to only define elim_not by changing the FNot case
+ to "FNot f \Rightarrow elim_not (FNot f)"?
+* Prove that the procedures just given correctly produce normal forms.
+ I.e. prove the following theorem.
+
+ theorem not_nf_elim_not:
+ \forall F.not_nf (elim_not F) \land not_nf (negate F).
+
+ Why is not possible to prove that one function produces normal forms
+ without proving the other part of the statement? Try and see what happens.
+
+ Hint: use the "n1,...,nm:" tactical to activate similar cases and solve
+ all of them at once.
+* Finally prove that the procedures just given preserve the semantics of the
+ formula. I.e. prove the following theorem.
+
+ theorem eq_eval_elim_not_eval:
+ \forall i,F.
+ eval i (elim_not F) = eval i F \land eval i (negate F) = eval i (FNot F).
+
+ Hint: you may need to prove (or assume axiomatically) additional lemmas on
+ booleans such as the two demorgan laws.
+
+================================
+A moderately difficult exercise:
+================================
+* Consider the inductive type of propositional formulae of the previous
+ exercise. Describe with an inductive type the set of well types derivation
+ trees for classical propositional sequent calculus without implication.
+
+ Hint: complete the following definitions.
+
+ definition sequent \def (list Formula) × (list Formula).
+
+ inductive derive: sequent \to Prop \def
+ ExchangeL:
+ \forall l,l1,l2,f. derive 〈f::l1@l2,l〉 \to derive 〈l1 @ [f] @ l2,l〉
+ | ExchangeR: ...
+ | Axiom: \forall l1,l2,f. derive 〈f::l1, f::l2〉
+ | TrueR: \forall l1,l2. derive 〈l1,FTrue::l2〉
+ | ...
+ | AndR: \forall l1,l2,f1,f2.
+ derive 〈l1,f1::l2〉 \to derive 〈l1,f2::l2〉 \to
+ derive 〈l1,FAnd f1 f2::l2〉
+ | ...
+
+ Note that while the exchange rules are explicit, weakening and contraction
+ are embedded in the other rules.
+* Define two functions that transform the left hand side and the right hand
+ side of a sequent into a logically equivalent formula obtained by making
+ the conjunction (respectively disjunction) of all formulae in the
+ left hand side (respectively right hand side). From those, define a function
+ that folds a sequent into a logically equivalent formula obtained by
+ negating the conjunction of all formulae in the left hand side and putting
+ the result in disjunction with the disjunction of all formuale in the
+ right hand side.
+* Define a predicate is_tautology for formulae.
+* Prove the soundness of the sequent calculus. I.e. prove
+
+ theorem soundness:
+ \forall F. derive F \to is_tautology (formula_of_sequent F).
+
+ Hint: you may need to axiomatically assume or prove several lemmas on
+ booleans that are missing from the library. You also need to prove some
+ lemmas on the functions you have just defined.
+
+==========================
+A long and tough exercise:
+==========================
+* Prove the completeness of the sequent calculus studied in the previous
+ exercise. I.e. prove
+
+ theorem completeness:
+ \forall S. is_tautology (formula_of_sequent S) \to derive S.
+
+ Hint: the proof is by induction on the size of the sequent, defined as the
+ size of all formulae in the sequent. The size of a formula is the number of
+ unary and binary connectives in the formula. In the inductive case you have
+ to pick one formula with a positive size, bring it in front using the
+ exchange rule, and construct the tree applying the appropriate elimination
+ rules. The subtrees are obtained by inductive hypotheses. In the base case,
+ since the formula is a tautology, either there is a False formula in the
+ left hand side of the sequent, or there is a True formula in the right hand
+ side, or there is a formula both in the left and right hand sides. In all
+ cases you can construct a tree by applying once or twice the exchange rules
+ and once the FalseL/TrueR/Axiom rule. The computational content of the proof
+ is a search strategy.
+
+ The main difficulty of the proof is to proceed by induction on something (the
+ size of the sequent) that does not reflect the structure of the sequent (made
+ of a pair of lists). Moreover, from the fact that the size of the sequent is
+ greater than 0, you need to detect the exact positions of a non atomic
+ formula in the sequent and this needs to be done by structural recursion
+ on the appropriate side, which is a list. Finally, from the fact that a
+ sequent of size 0 is a tautology, you need to detect the False premise or
+ the True conclusion or the two occurrences of a formula that form an axiom,
+ excluding all other cases. This last proof is already quite involved, and
+ finding the right inductive predicate is quite challenging.
projects / helm.git / blobdiff