Home

Matita Tutorial - Dipartimento di Informatica

1. 9 2 Universe Constraints ses sess acca SPE pS aS a aa a aa 9 3 Informative and non informative content 10 Further readings Journal of Formalized Reasoning Vol 7 No 2 2014 94 i A Asperti and W Ricciotti and C Sacerdoti Coen 0 GETTING STARTED Matita 4 is a dependently typed interactive prover under development at the Com puter Science Department of the University of Bologna An interactive prover is a software tool aiding the development of formal proofs by man machine collaboration It provides a formal language where mathemat ical definitions executable algorithms and theorems coexist and an interactive environment keeping the current status of the proof and updating it according to commands usually called tactics issued by the user 13 24 This tutorial provides an introduction to the system explicitly addressed to absolute beginners and does not require previous knowledge about interactive the orem proving or type theory An executable version of the tutorial is available in the usr share matita lib tutorial directory after having installed Matita see next Section The reader is supposed to run the executable tutorial while reading the current document in this document we only illustrate those code snapshots that showcase noteworthy concepts and techniques for the first time The tutorial is also a companion document to the user manual of Matita that can be browsed from the H
2. We say that a state is safe if either the goat is on the same bank of the boat or both the wolf and the cabbage are on the opposite bank of the goat Journal of Formalized Reasoning Vol 7 No 2 2014 Matita Tutorial e 105 inductive safe_state state Prop with_boat Vg w c safe_state mk_state g wc g opposite_side Vg g1 b opp g gl gt safe_state mk_state g gl gl b Finally a state y is reachable from zg if either there is a single move leading from to y or there is a safe state z such that z is reachable from z and there is a move leading from z to y gt inductive reachable state state Prop one Va y move x y reachable z y more Vzx z y reachable x z gt safe_state z move z y reachable z y 1 9 Automation Remarkably Matita is now able to solve the farmer problem by itself provided you allow automation to exploit enough resources The command n is similar to where n is a measure of this complexity in particular it is a bound to the depth of the expected proof tree more precisely to the number of nested applicative nodes In this case there is a solution in six moves and we need a few more applications to handle reachability and side conditions The magic number to let automation work is in this case 9 lemma problem reachable start end normalize 9 qed The reader is referred to 9 10 for technical information on Ma
3. 2 2 Existentials We are interested in proving that for any natural number n there exists a natural number mthat is the integer half of n defined as the result of the integer division of n by 2 This will give us the opportunity to introduce new connectives and quantifiers and later on to highlight some important aspects of proofs and computations It is interesting to observe that not even existential quantification is a primitive notion in Matita in fact it is defined in the library file basic logic ma and in order to use it we need to include this file or another one that recursively includes it we shall come back on the actual definition of the existential in section 3 2 Here is the formal statement of the theorem we are interested in Journal of Formalized Reasoning Vol 7 No 2 2014 Matita Tutorial 111 7 include basics types ma definition twice An add n n theorem ex_half Vn dm n twice m Vn S twice m We proceed by induction on n after normalizing we get the following goals goal type G dm 0 add 0O0VO S add m m Go Yx Im z add mmVz S add mm gt dm S x add mmVS z S add m m The only way we have to prove an existential goal is by exhibiting the witness which in the case of the first goal is O We do it by applying the term called ex_intro instantiated by the witness Then it is clear that we must follow the left branch of the disjunction In Secti
4. theorem equiv_sem VS DeqSet Vel e2 pre S e1 e2 Vw cofinal moves w e1 moves w e2 This does not directly imply decidability we have no bound on the length of w moreover so far we made no assumption on the cardinality of s Instead of requiring S to be finite we may restrict the analysis to characters occurring in the given PREs This means we can prove the following stronger result lemma equiv_sem_occ VS Vel e2 pre S Vw sublist S w occ S el e2 gt cofinal moves w el moves w e2 el e2 The proof essentially requires the notion of sink state and a few trivial properties definition sink_pre AS Ai blank S lil false lemma not_occur_to_sink VS a Vi pitem S memb S a occur S il true gt move a i sink_pre S i lemma moves_sink VS w i moves w sink_pre S i sink_pre S i Let us say that a list of pairs of PREs is a bisimulation if it is closed w r t moves and all its members are cofinal definition sons AS DegSet Al list S Ap pre S x pre S map Aa move a fst fst p move a fst snd p l definition s_bisim AS DegSet Al list Aalpha list S Vp pre S x pre S memb p l true gt cofinal p A sublist sons alpha p l Using lemma equiv_sem_occ it is easy to prove lemma bisim_to_sem VWS DeqSet Vl list Vel e2 pre S is_bisim S l occ S el e2 memb e1 e2 l true gt el e2 This is already
5. More interesting are the notions of subset and equality Given two sets P and Q P is a subset of Q when any element u in Pis also in Q that is when P u implies Q u gt definition subset VU Typel0 VP Q U Prop Prop AU P Q Vu U P u gt Q u Then two sets P and Q are equal when P C Qand Q C P or equivalently when for any element u P u OQ u P definition egP U Type 0 AP Q U Prop Vu U P u Q u We shall use the infix notation for the previous notion of equality It is impor tant to observe that the egP is different from Leibniz equality of section 3 4 As we already observed Leibniz equality is a pretty syntactic or intensional notion that is a notion concerning the connotation of an object and not its denotation the shape assumed by the object and not the information it is supposed to con vey Intensionality stands in contrast with extensionality referring to principles that judge objects to be equal if they enjoy a given subset of external observable Journal of Formalized Reasoning Vol 7 No 2 2014 142 A Asperti and W Ricciotti and C Sacerdoti Coen properties e g the property of having the same elements For instance given two sets A and B we can prove that AUB BU A since they have the same elements but there is no way to prove AUB BUA The main practical consequence is that while we can always exploit a Leibniz equality between two terms t and tz for rewritin
6. Sp match m with 0 gt false S q gt negb p ql It is so important to know if Leibniz equality for a given type is decidable that we often pack this information together into a single algebraic data structure called DeqSet record DeqSet Type 1 carr gt Type 0 eqb carr carr bool eqb_true Vz y eqb x y true O a y A DegSet is simply a record composed by a carrier type carr a boolean function egb carr carr carr representing the decision algorithm and a proof eqb_true that the decision algorithm is correct The definition of a DegSet is an instance of a mathematical structure in algebra that are often denoted simply by their carriers For example if G is a group we Journal of Formalized Reasoning Vol 7 No 2 2014 Matita Tutorial 143 write x Gto say that x belongs to the carrier of G The same abuse of notation is achieved in Matita via coercions A coercion from a type T to a type T2 is a function that is silently inserted around an expression e 7 to turn it into an expression of type T2 The gt symbol in the definition of DegSet declares the projection carr as a coercion from a DeqSet to its carrier type The reader may consul the user manual of Matita for the general syntax to declare coercions We use the infix notation for the decidable equality egb of the carrier The notations P H and b H are used respectively to convert a boolean equ
7. However this is prefectly legal y inductive U Prop c VA Prop 4 gt Prop gt U and one could and should naturally wonder how we avoid the paradox in this case What happens is that the definitions of carrier and property are rejected For instance if we enter the following definition definition carrier u U match u with c AP gt 4 we would now get the error message Sort elimination not allowed Prop towards Type The intuition is that proofs elements of sort Prop should be merely understood as certificates testifying that their type is inhabited but are not supposed to carry Journal of Formalized Reasoning Vol 7 No 2 2014 Matita Tutorial i 195 any additional information This can be further stressed by the principle of proof irrelevance asserting that all proofs of a same proposition A are provably equal inside the logic In this sense proofs are non informative no kind of inspection can be perfomed on proofs and no data can be extracted from them For instance the previous definition of carrier is trying to extract from the proof u U Prop the carrier that is an observable information some propositions could have carrier True and some others carrier False and True is provably different from False So we would be able to discriminate proofs according to the extracted carrier contradicting the principle of proof irrelevance To take a simple example suppose we have a proof of AV B
8. diverging scons hd tl The two coinductive definitions of diverging traces are equivalent To state the two results we first need a function to retrieve the head from traces and diverging traces definition head_of_streamseg VA Typel0l streamseq A gt A AA s match s with sscons hd _ gt hd definition head_of_stream WA Typel0 stream A option A AA s match s with snil gt None scons hd _ Some hd A streamseq can be extracted from a diverging stream using corecursion let corec mk_diverging_trace_to_div_trace s stream state diverging s gt streamseg state match s return As diverging s gt streamseg state with snil abs diverging snil scons hd tl AH sscons hd mk_diverging_trace_to_div_trace tl cases False inversion abs hd tl _ abs destruct inversion H hd tl K eq destruct OK qed An expansion lemma will be needed soon lemma mk_diverging_trace_to_div_trace_expansion Vhd tl H AK mk_diverging_trace_to_div_trace scons state hd tl H sscons hd mk_diverging_trace_to_div_trace tl K tthd tl H cases eta_streamseg mk_diverging_trace_to_div_trace 2f qed To complete the proof we need a final lemma streamseqs extracted from well formed diverging streams are well formed too The definition is mostly interactive Journal of Formalized Reasoning
9. nil gt nil cons x tl gt f mp A Bf tl l The map function distributes over append as can be simply proved by induction on the first list a lemma map_append VA B f 11 12 map A B f 11 map A B f 12 map A B f 11012 HA HB f 11 elim 11 12 Orefl h tt IH 12 normalize qed The most important iterator is traditionally called fold we shall only consider the so called fold right variant that takes as input a function f 4 gt B gt B a list a1 n of elements of type 4 a base element b B and returns the value fa fas f an b y let rec foldr 4 B Typel01 f 4 gt B B b B Ll list A on l B match l with nil b cons a l f a foldr A Bf b 131 Many other interesting functions can be defined in terms of foldr A first interesting example is the filter function taking as input a boolean test p and a list 1 and returning the sublist of all elements of 1 satisfying the test gt definition filter AT Ap T gt bool foldr T list T A2 10 if p x then 2 10 else 10 nil T As another example we can generalize the map function to an operation taking as input a binary function f 4 gt B gt C two lists a1 n and b1 bm and returning the list f a1 bi f an di3 5f 1 bm f an dm Journal of Formalized Reasoning Vol 7 No 2 2014 Matita Tutorial 141 N definition compose A4 B C Af A gt B gt C A
10. If you type the previous definition Matita will complain with the following error TypeChecker failure Sort elimination not allowed Prop towards Type 0 Even returning the two propositions True and False instead of two booleans would not work definition discriminate_to_Prop A4 B Prop Ap AV B match p with or_introl a gt True or_intror b gt False The error message is the same as before in both cases the sort of the branches the right hand sides of the pattern matching construct is Type 0 The only thing we can do is return other proofs like in the following example definition or_elim A4 B C Prop Ap AVB Af 4A gt C Ag B gt C match p with Journal of Formalized Reasoning Vol 7 No 2 2014 136 A Asperti and W Ricciotti and C Sacerdoti Coen or_introl a gt fa or_intror b gt g b l Exercise repeat the previous examples in interactive mode by elimination on the hypothesis p AV B Journal of Formalized Reasoning Vol 7 No 2 2014 Matita Tutorial i 137 5 MORE DATA TYPES In this section we shall consider more examples of datatypes starting from quite traditional ones like option types and lists to conclude with less common struc tures like finite sets or vectors with a specified length 5 1 Option Type Matita can only define total functions However we are not always in a condition where we can return a meaningful value for instance working on nat
11. Matita Tutorial A 145 n lt m leb n m true Then we could reduce the verification of 2 lt 3 to that of of leb 2 3 true that just requires a mere computation 5 8 Finite Sets A finite set is a record consisting of a DeqSet A a list of elements of type A enu merating all the elements of the set and the proofs that the enumeration does not contain repetitions and is complete memb is the membership operation on lists de fined in the obvious way and uniqueb is the function that returns true if its third argument is an enumeration without repetitions record FinSet Type l1 FinSetcarr gt DeqSet enum list FinSetcarr enum_unique uniqueb FinSetcarr enum true enum_complete Va FinSetcarr memb x enum true The standard library of Matita provides many operations for building new FinSets by composing existing ones for example if Aand B have type FinSet then option A AXB A B are finite sets too In all these cases unification hints are used to suggest the intended finite set structure associated with them that makes their use quite transparent to the user A particularly interesting case is that of the arrow type A B We may define the graph of f 4 B as the set sigma type of all pairs a b such that f a b definition graph_of M4 B Af A gt B YXp AXB f fst p snd p When the equality on Bis decidable we can effectively enumerate all elements of the graph by simply
12. VB Type 0 Vy B z gt y gt P B y The difference between JMeq_ind and eq_ind is analogous to that in the definition of the two equalities in JMeq_ind the scheme P is abstracted not only over the term to be rewritten but also over its type which is also going to be rewritten This is not as nice as it sounds because not every predicate can be made generic over the type of its argument when this is not possible in practice most of the time all attempts to use JMeq_ind to perform rewriting will fail While the above discussion may sound abstract a very concrete example is that the property jmeq_to_eq VT Typel0l Vzx y T r y gt ay is not an immediate consequence of JMeg_ind in particular depending on certain characteristics of the type theory in use it may even be not provable In Matita it is proved by exploiting proof irrelevance which we will briefly discuss in Section 9 3 and declared as a coercion allowing heterogeneous equalities where both sides have the same type to be used in tactics in place of Leibniz equalities Heterogeneous equality is integrated in Matita after the file basics jmeq ma has been included the system will create heterogeneous versions of discrimination and inversion principles for all the inductive types subsequently defined In particular returning to our example if we know by hypothesis that ti t2 and we want to prove that xz node nc d Ny node ma b it is sufficient to destruct the
13. default element or decide to return an option type We have an additional complication in this case since the default element should have type 4 as the head and we know nothing about 4 it could even be an empty type We have no way to guess a canonical element and the only possibility along this approach is to take it as input These are the two options definition hd A Al list A Ad A match l with nil gt d cons a _ gt al definition option_hd AA Al list A match l with nil gt None cons a _ gt Some a What remains of a list after removing its head is called the tail of the list Again the tail of an empty list is undefined but in this case the result must be a list and we have a canonical inhabitant of lists that is the empty list So it is natural to extend the definition of tail saying that the tail of nil is nil that is very similar to saying that the predecessor of 0 is 0 ps definition tail A4 Al list A match l with nil gt cons hd tl gt tl Using destruct it is easy to prove that cons is injective in both arguments lemma cons_injective_l VA Va1 a2 A V11 12 a1 11 a2 12 al al HA Hal a2 11 12 Heq destruct qed lemma cons_injective_r VA Va1 a2 A V11 12 a1 11 a2 12 11 12 A Hal a2 11 12 Heq destruct qed The append function is defined by recursion on the first list Journal of Formalized Rea
14. east 2 Alternatively we can directly instantiate the bank into the move Let us complete the proof in this very readable way more move_goat west 2 more move_cabbage east 2 more move_boat west 2 Cone 2 qed Journal of Formalized Reasoning Vol 7 No 2 2014 Matita Tutorial i 109 2 INDUCTION Most of the types we have seen so far have been enumerated types composed of a finite set of alternatives and records composed of tuples of heterogeneous elements A more interesting case of type definition is when some of the rules defining its elements are recursive i e they allow the formation of more elements of the type in terms of the already defined ones The most typical case is provided by the natural numbers which can be defined as the smallest set generated by a constant 0 and a successor function from natural numbers to natural numbers inductive nat Type 0 0 nat S nat gt nat The two terms 0 and S are called constructors they define the signature of the type whose objects are the elements freely generated by means of them So examples of natural numbers are 0 S 0 S S 0 S S S 0 and so on The language of Matita allows the definition of well founded recursive functions on inductive types in order to guarantee termination of recursion you are only allowed to make recursive calls on arguments structurally smaller than the ones
15. nil gt None cons hd k gt Some match hd with p_set n gt n k p_incr gt S 0 k p_while b gt match o with 0 0 k Sp S p dO p_while b k 11 We can esasiliy prove that next o nif and only if step o Some n N theorem step_nest Vo n step o Some n nest o n theorem next_step Vo n next o n step o Some n Termination is the archetypal undecidable problem Therefore there is no func tion that given an initial state returns a diverging trace if the program diverges or fails in case of error The best we can do is to give an alternative definition of trace that captures both diverging and converging computations N record trace Type 0 tr seg option state well_formed Vn s tr n Some s gt tr S n step s The trace is diverging if every state is not final definition diverging trace gt Prop At Vn tr t n None We leave as a simple exercise for the reader to check that the two definitions of diverging traces are equivalent as expressed by the following statements theorem div_trace_to_diverging_trace Vd div_trace dt trace diverging t Atr t 0 Some div_tr d 0 theorem diverging_trace_to_div_trace Vt trace diverging t dd div_trace tr t 0 Some div_tr d 0 While we cannot decide divergence we can always compute a trace from a given initial state Note that every time
16. true b false b H CAP H qed In a similar way unification hint 0 b1 b2 bool x mk_DeqSet bool begb beqb_true begb b1 b2 eqb X b1 b2 5 7 Prop vs bool It is probably time to have a discussion about Prop and bool and their different roles in the Calculus of Inductive Constructions Inhabitants of the sort Prop are logical propositions In turn logical propositions P Prop can be inhabitated by their proofs H P Since in general the validity of a property P is not decidable the role of the proof is to provide a witness of the correctness of P that the system can automatically check On the other hand bool is just an inductive datatype with two constructors true and false these are terms not types and cannot be inhabited Logical connectives on bool are computable functions defined by their truth tables using case analysis Prop and bool are in a sense complementary the former is more suited to abstract logical reasoning while the latter allows in some situations for brute force proving by evaluation Suppose for instance that we wish to prove that the 2 lt 3 Starting from the definition of the factorial function and properties of the less or equal relation the previous proof could take several steps Suppose however we proved the decidability of lt that is the existence of a boolean function leb reflecting lt in the sense that Journal of Formalized Reasoning Vol 7 No 2 2014
17. where 4 A can be arbitrary types comprising T itself As a general rule the inductive type must be conceptually understood as the smallest collection of terms freely generated by its constructors 1 2 Defining functions We can now define a simple function computing for each bank of the river the opposite one definition opposite As match s with east gt west west gt east l Non recursive functions must be defined in Matita using the keyword definition followed by the name of the function and an optional type The type bank bank is omitted in the example because it is automatically inferred by the system The definition proceeds with the keyword followed by the function body The body starts with a list of input parameters preceded by the symbol A lambda many T X like macros are automatically converted by Matita into Unicode symbols see View gt TeX UTF 8 table in the menu bar for a complete list We then proceed by pattern matching on the parameter s if the input bank is east we return west and conversely if it is west we return east Since the input parameter sis matched against the constructors of the type bank its type is inferred to be bank Since in every case the match returns a bank the output of opposite is inferred to be bank too Pattern matching is a well known feature typical of functional programming especially of the ML family allowing simple access to the component
18. Claudio Sacerdoti Coen and Enrico Tassi A compact kernel for the Calculus of Inductive Constructions Sadhana 34 1 71 144 2009 6 Andrea Asperti Wilmer Ricciotti Claudio Sacerdoti Coen and Enrico Tassi Hints in unification In TPHOLs 2009 volume 5674 of LNCS pages 84 98 Springer Verlag 2009 7 Andrea Asperti Wilmer Ricciotti Claudio Sacerdoti Coen and Enrico Tassi A Bi Directional Refinement Algorithm for the Calculus of Co Inductive Con structions Logical Methods in Computer Science 8 1 2012 Journal of Formalized Reasoning Vol 7 No 2 2014 198 8 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 A Asperti and W Ricciotti and C Sacerdoti Coen Andrea Asperti Claudio Sacerdoti Coen Enrico Tassi and Stefano Zacchi roli User interaction with the Matita proof assistant Journal of Automated Reasoning 39 2 109 139 2007 Andrea Asperti and Enrico Tassi Smart matching In Intelligent Com puter Mathematics 10th International Conference AISC 2010 17th Sympo sium Calculemus 2010 and 9th International Conference MKM 2010 Paris France July 5 10 2010 Proceedings volume 6167 of Lecture Notes in Com puter Science pages 263 277 Springer 2010 Andrea Asperti and Enrico Tassi Superposition as a logical glue EPTCS 53 1 15 2011 Andrea Asperti Enrico Tassi and Claudio Sacerdoti Coen Regular expres sions au point
19. In the case of the existential it allows us to pass from a goal of the shape de P 1 gt Q to a goal of the shape Vz P r gt Q Journal of Formalized Reasoning Vol 7 No 2 2014 112 A Asperti and W Ricciotti and C Sacerdoti Coen At this point we are left with a new goal with the following shape Gz Vm x add mmVax S add m mM gt We should introduce m the hypothesis H s add m m V S add m m and then reason by cases on this hypothesis It is the same situation as before we must explode the disjunctive hypothesis into its constituents In the case of a disjunction the tactic allows us to pass from a goal of the form AVB Q to two subgoals of the form A gt Q and B gt Qq In the first subgoal we are under the assumption that x add m m Half of S lt x is therefore m and we have to prove the right branch of the disjunction In the second subgoal we are under the assumption that x S add m m The half of S zx is hence S m and we have to follow the left branch of the disjunction Here is the simple proof of G ltz m tego ex_intro m 2 Olezx_intro S m normalize 2 qed 2 4 Computing vs Proving Instead of proving the existence of a number corresponding to the half of n we could be interested in computing it The best way to do it is to define this division operation together with remainder that in our case is just a boolean value true if the inp
20. Q can seem puzzling at first note that it closely matches the term opp opp opp 2 Each occurrence of the unary morphism opp is replaced by and the occurrence z to be rewritten to y is replaced by EQ x y Therefore the term F t EQ is a compact notation to express at once where the rewriting should be performed and what hypothesis should be used for rewriting In the next section we address the problem of setoid rewriting in full generality 7 1 Rewriting setoid equalities In set theory once a quotient S R has been defined equivalence classes are com pared using the standard equality whose main property is to allow rewriting in Journal of Formalized Reasoning Vol 7 No 2 2014 168 A Asperti and W Ricciotti and C Sacerdoti Coen every context if Ej Ez then f E can be replaced with f Ez in every context f Note that f is applied to equivalence classes of elements of S If we started instead from a function f defined on elements of S first of all we would need to lift it to work on equivalence classes and this is possible only if f is a proper context for R defined as an f such that s Rs implies f s f so When using setoids we keep working with elements of S instead of forming a new type Therefore we must deal with contexts f that are not proper When fis not proper f E1 cannot be replaced with f 2 even if E1 E2 For exam ple 0 1 1 2 but fst 0 1 4 fst 1 2 Therefor
21. T Matita dome Fig 1 Matita interface Standard ML and OCaml convention of being bracketed with the lexical tokens and Let us now try to import one of the files of the standard library of Matita that you should have downloaded along with the source Type the following line in the editor window include basics logic ma and then hit Ctrl Alt Page Down or press the button at the top of the Matita window with a downarrow on it If everything is working right the bottom right hand pane will start printing out numerous messages telling you that the system is recursively typechecking and including basics logic ma and its dependencies When the include command has been completely processed the command line of the editor pane will turn a light shade of blue Lines highlighted with this colour are locked and cannot be edited any longer to edit them you must first ask the system to retract them You may use Ctrl A1t Page Up or the button with an uparrow to retract a single statement and Ctr1 A1t Home or the button with an overlined uparrow to retract everything in the current file If the execution of the command fails Matita will report its diagnosis in the bottom right hand pane in the case of the include command the most frequent reason for a failure is that the system has not been able to find the requested file If this happens please check that the root file of the previous section has been correct
22. Vl list A PUL that we can rewrite up to currying as VA Type 0 VP Prop Cunit A xlist A xP gt P gt list A gt P and turning the recursor into an iterator to the simpler form VA Type 0 VP Prop Cunit A XP gt P gt list A gt P Thinking of a list as the least fixpoint of the equation list A unit A xlist A Journal of Formalized Reasoning Vol 7 No 2 2014 Matita Tutorial i 189 the above principle says that we can prove P as soon as we can prove P for every possible shape of the list replacing sublists list A with the result P of recursive calls of the iterator Streams are the greatest fixpoint of the same equation stream A unit A Xstream A Dualizing the idea of a generic destructor for list we obtain the type of the generic constructor for streams VA Type 0 VP Prop P gt unit A xP gt P stream A The above principle says that we can build a stream from a proof of P as soon as we can observe from P what shape the stream has and what P will be used to generate the reamining of the stream The principle is indeed easily provable in Matita let corec stream coind A Type 0 P Prop H P gt Sum unit A xP p P stream A match H p with inl _ gt snil A inr cpl gt let hd p cpl in scons A hd stream_coind A PH p 1 At the moment Matita does not automatically prove any generic constructio
23. set as an element of the universe U We can define definition carrier u U match u with c A P A definition property Au U match u return Au carrier u gt Prop with c A P gt P so from each element u U we can extract its characteristic property Given two terms u U and a A such that A carrier u we say that a is a member of u provided a satisfies the characteristic property of u A tricky point is that property u expects as input an element of type carrier u while a 4 we know that they are equal but this does not imply that they are convertible What we can do is to use the equality between the two types A and B to define an embedding from A to B A lemma embed VA B Typel0l 4 B B gt A HA B th gt h qed The previous embedding has very good properties in particular if the two types can be proved to be identical via reflexivity the corresponding embedding is just the identity lemma embed_id VA a embed A A refl a a qed Using the previous embedding we can now define the following membership relation definition member Vu U VA Type 0 Va A carrier u A Prop Au A rAa A Ah property u embed carrier u A h a where in particular lemma member_to_P VA P a property c A P embed refl 7 a Pa Journal of Formalized Reasoning Vol 7 No 2 2014 194 E A Asperti and W Ricciotti and C Sacerdoti Coen However suppose
24. we know that this is either a proof of A or a proof of B and we could be tempted to define a function distinguishing among these two situations returing True in the first case and False in the second definition discriminate_or A4 B Ap AVB match p with or_intror _ gt True lor_introl _ gt False Suppose we accept the previous definition and consider the following proofs of TrueV True that we can assume to be equal by proof irrelevance axiom eq_proofs or_introl True True I or_intror True True I But then True would be equal to discriminate_or or_intro_l or_True True I that is equal to discriminate_or or_intro_r or_True True I that is equal to False To make another example let us see how we can derive the paradox of the previous section axiomatizing the existence of carrier and property inductive U Prop c VA Prop A Prop U axiom carrier U Prop axiom carrier_def VA P carrier c A P A axiom property Vu U carrier u Prop axiom property def VA P a property c A P embed carrier_def A P a Pa definition member Vu U VA Prop Va A carrier u A Prop Au A rAa A Ah property u embed carrier u Aha lemma member_to_P VA P a member c A P a carrier_def A P P a HA P Ha whd in match member 7777 qed definition RussellP u U Vh carrier u U a member u U u h definition Russell c U RussellP lemma not_RussellP_Russell
25. 0 and can be solved by computation 2 6 Cut The next subgoal after performing a few introductions looks like the following n nat a nat Hind Wq nat Vr bool div2 a q r gt a add nat_of_bool r twice q q nat r bool div2 S a q r gt S a add nat_of_bool r twice q We should proceed by case analysis on the remainder of div2 a but before doing it we should emphasize the fact that div2 a can be expressed as a pair of its two projections The tactic that allows to introduce a new hypothesis splitting complex proofs into smaller components is called cut The invocation of cut A transforms the current goal G into the two subgoals A and A gt G A is called the cut formula In our case the cut formula is div2 a fst div2 a snd div2 a whose proof is trivial After typing the following commands cut div2 a fst div2 a snd div2 a Journal of Formalized Reasoning Vol 7 No 2 2014 Matita Tutorial z 115 we are left in the new state n nat a nat Hind Vq nat Vr bool div2 a q r gt a add nat_of_bool r twice q q nat r bool div2 a fst div2 a snd div2 a gt div2 S a q r gt 8S a add nat_of_bool r twice q We now proceed by induction on snd div2 a the two subgoals are respec tively closed using the two lemmas div2S0 and div2S1 in conjunction with the inductive hypothesis and do not contain additional challenges The whole p
26. 0 2 y Z X ZPLUS Ii ar aa a E E T Yy mor_carr X T y The identity function is a morphism and composition of morphisms is also a morphism This means that the identity function is always proper and a compound context is proper if every constituent is 2 definition d_morphism VS setoid S gt S AS mk_morphism Az m qed definition comp_morphism WS1 82 83 S2 S3 gt S1 S2 gt S1 gt S3 AS1 52 83 f1 f2 mk_morphism Ax f1 f2 2D normalize 21 22 EQ Omor_proper Omor_proper qed By iterating applications of mor_proper we can consume the context one appli cation at a time in order to perform a rewriting Like in ex2 the proof works on any setoid because it does not reference OPP anywhere The above theorem on composition of morphisms justifies the correctness of the proofs example ex3 Vzx y x y opp opp opp 2 opp opp Copp y tz ty EQ Omor_proper Omor_proper Omor_proper EQ qed We can improve the readability of the previous proof by assigning a notation to mor_proper and by packing together the various applications of mor_proper and EQ We pick the prefix symbol notation f c with precedence 90 for proper c interpretation mor_proper proper c mor_proper c example ex3 Vz y x y opp opp opp z opp Copp Copp y a y EQ OCF TF TED qed While the term
27. 1121 gt aUCderiv 2 a by deriv_cat deriv 1 1221JU i2p a by deriv_union deriv i1 i2 a by definition of The move operation is generalized to strings in the obvious way let rec moves S DeqSet we on w pre S match w with nil gt e cons a tl moves S tl move S a fst e lemma same_carrier_moves WS DegSet Vw Ve pre S fst moves w e fst el theorem decidable_sem VS DeqSet Vw word S Ve pre S snd moves w e true ole w The proof of decidable_semis by induction on w The case use is trivial if w a w we have snd moves a w e true snd moves wi move a fst e true by def of moves move a fst e w by ind hyp gt el a w by move_ok It is now clear that we can build a deterministic finite automaton DFA De for e by taking PREs as states and move as transition function the initial state is e e and a state 2 6 is final if and only if b true The fact that states in De are finite is obvious in fact their cardinality is at most 2 where n is the number of symbols in e This is one of the advantages of pointed regular expressions w r t derivatives whose finite nature only holds after a suitable quotient EXAMPLE 5 Figure 4 depicts the DFA for the regular expression actbc The graphical description of the automaton is the traditional one with nodes for states and labelled arcs for transitions Unreachable states are not shown Final states ar
28. Qstreamseg_nth is defined by recursion on the index gt lemma Qstreamseq_nth_Rplus_streamseq Vi T Yy Qstreamseq_nth Rplus_streamseg x y i Qstreamseq_nth x i Qstreamseg_nth y 1 i elim 2 2 7 IH tzhd txtl yhd ytl normalize IH qed The proof that the resulting sequence is Cauchy is exactly the same we used for sequences up to two applications of the previous lemma gt definition Rplus_ R gt R gt R Arl r2 mk_R_ Rplus_streamseqg r ri r r2 eps cases isCauchy ri Qhalve eps n1 H1 cases isCauchy r2 Qhalve eps n2 H2 Cmaz ni n2 4 7 K1 K2 gt Qstreamseg_nth_Rplus_streamseq gt Qstreamseq_nth_Rplus_streamseq transitive_Qleq Qdist_Qplus lt Qplus_Qhalve_Qhalve eps Oleg plus 0H1 le_mazl H2 le_mazr 2 6 K1 4 8 k2 qed We lift Rplus_ to a morphism by proving that it respects the equality for real numbers The script is exactly the same we used to lift Rplus_ but for two appli cations of Qstreamseg_nth_Rplus_streamseq definition Rplus P gt RP gt R mk_bin_morphism Rplus_ 21 4x2 y1 y2 Hx Hy eps cases Hx Qhalve eps i Hx Hr cases Hy Qhalve eps j Hy Hy A Cmaz i j l Hmax lt Qplus_Qhalve_Qhalve eps transitive_Qleq 3 O Qleg Qplus Hx l Hy l 2 by le_masl le_masr 12 gt Qstreamseq_nth_Rplus_streamseq gt Qstreamseq_nth_Rplus_stream
29. Vol 7 No 2 2014 162 i A Asperti and W Ricciotti and C Sacerdoti Coen 7 QUOTIENTING IN TYPE THEORY One fundamental operation in set theory is quotienting given a set S and an equivalence relation R over S quotienting creates a new set S R whose elements are equivalence classes of elements of S The idea behind quotienting is to replace the structural equality over S with R therefore identifying elements up to R The use of equivalence classes is just a technicality Matita does not have the type theoretic counterpart to quotienting which are quotient types In the literature there are alternative proposals to introduce quo tient types but no consensus has been reached Nevertheless the notion of setoids delivers all the features of quotient types without needing to extend the type the ory A setoid is defined as a type S coupled with an equivalence relation R used to compare elements of S In place of working with equivalence classes of S up to R one keeps working with elements of S but compares them using R in place of Setoids over types elements of Type 0 can be declared in Matita as follows 7 record equivalence_relation A Type 0 Type 0 4 eqrel gt relation A equiv_refl reflexive eqrel equiv_sym symmetric eqrel equiv_trans transitive eqrel record setoid Type i 1 carrier gt Type 0 eq setoid equivalence_relation carrier Note that carrier has b
30. any property is true for an element of type void since we have no such element Similarly the elimination principle for the unit type is VP unit Prop P it gt Vz unit Pg Indeed in order to prove that a property is true for any element of the unit type it is enough to prove it for the unique canonical inhabitant it As an exercise let us prove that all inhabitants of unit are equal to each other lemma eq_unit Va b unit a b Journal of Formalized Reasoning Vol 7 No 2 2014 130 A Asperti and W Ricciotti and C Sacerdoti Coen The idea is to proceed by case analysis on a and b we have only one possibility namely a it and b it hence we end up proving it it that is trivial Here is the proof a cases a b cases b qed also qed It is interesting to observe that we get exactly the same behavior by directly apply ing unit_ind instead of proceeding by case analysis In fact this is an alternative proof Cunit_ind unit_ind qed 4 2 Sigma Types and dependent matching As a final example let us consider type variants of the existential quantifier in this case we have two interesting possibilities inductive Sig A Type 0 Q A Prop Type 0 Sig_intro Va A Q x gt Sig A Q inductive DPair A Type 0 Q 4 Type 0 Typelol DPair_intro Va A Q x gt DPair A Q In the first case traditionally called sigma type an elem
31. booleans is a DeqSet too this means that the type of PREs automatically inherits the structure of a DeqSet in Section 6 10 we shall deal with pairs of PREs and in this case too without having anything to declare the type will inherit the structure of a DegSet Items and PREs can also be enumerated In particular it is easy to define a function pre_enum that takes as input a regular expression and gives back the list of all PREs having e for carrier Completeness of pre_enumis stated by the following lemma lemma pre_enum_complete VS Ve pre S memb e pre_enum S fst el true 6 5 Broadcasting points Intuitively a regular expression e must be understood as a pointed expression with a single point in front of it However since we only allow points before symbols we must broadcast this initial point inside e traversing all nullable subexpressions i e subexpressions denoting languages that accept the empty string which essentially corresponds to the e closure operation on automata We use the notation e to denote such an operation its definition is the expected one let us start discussing an example EXAMPLE 3 Let us broadcast a point inside ate b atb b We start working in parallel on the first occurrence of a where the point stops and on e that gets Journal of Formalized Reasoning Vol 7 No 2 2014 154 A Asperti and W Ricciotti and C Sacerdoti Coen traversed We have hence reached the end
32. by case analysis on b Here is the whole proof r a b eqa gt eqa cases b qed 1 8 Records It is time to proceed with our formalization of the farmer s problem A state of the system is defined by the position of four items the goat the wolf the head of cabbage and the boat The simplest way to declare such a data type is to use a record P record state Typelol goat_pos bank wolf_pos bank cabbage_pos bank boat_pos bank When you define a record named foo the system automatically defines a record constructor named mk_foo To create a new record you need to pass as arguments to mk_foo the values of the record fields definition start mk_state east east east east definition end mk_state west west west west We must now define the possible moves A natural way to do it is in the form ofa relation a binary predicate on states inductive move state gt state Prop move_goat Vg g1 u c opp g g1 gt move mk_state g wc g mk_state gl w c gl We can move the goat from a bank g to the opposite bank gl if and only if the boat is on the same bank g as the goat and we move the boat along with it move_wolf Vg w wl c opp w wi move mk_state g w c w mk_state g wi c w1 move_cabbage Wg w c cl opp c cl gt move mk_state g w c c mk_state g w cl cl move_boat Vg w c b b1 opp b b1 move mk_state g w c b mk_state g wc b1
33. by the system with the following error message Error Non positive occurence in D gt D gt D The definition of D should be quite familiar for instance in order to build a model for the A calculus one needs a domain D that is isomorphic to its own function space D gt D each term is also a function and one could be tempted to simply define it as the smallest type D for which there exists an embedding D gt D gt D Suppose we accept such a definition We would then expect to be able to reason by case analysis on an object d D In particular d must reduce to the form lam f for some function f and we would expect to be able to extract this information out of d by means of the usual pattern matching operation This is all we need to write a function that given two terms in D interprets the first as a function i e unboxes the embedded function and applies it to the second definition app D gt D gt D Ad e match d with lam f gt f el At this point it should be clear that what we are really doing is embedding the A calculus into CIC More importantly our embedding reuses the binding structures of CIC to express binding in the object calculus For instance we can easily express the familiar duplicator term of the A calculus i e Az z 2 as follows definition dup D lam Az D app z 2 However our embedding goes beyond that we can even reuse reduction in CIC to express reduction in the object A calcu
34. case n 0 we conclude the proof in ez_half by providing the witness 0 and a proof of A 0 this corresponds to returning the pair 0 false in div2 Similarly in the inductive case n S a we must exploit the inductive hypothesis for a i e the result of the recursive call distinguishing two subcases according to the two possibilities A a or B a i e the two possible values of the remainder for a The reader is invited to check all the details of this correspondence 2 5 Destruct Let us now prove that our div2 function has the expected behaviour We start proving a few easy lemmas lemma div2S0 Vn q div2 n q false gt div2 S n q true tin tq H normalize gt H normalize qed lemma div2S1 Vn q div2 n q true gt div2 S n S q false tin q H normalize gt H normalize qed Here is our statement where nat_of_bool is the conversion function that maps false to zero and true to one F lemma div2_ok Vn q r div2 n q r gt n add nat_of_bool r twice q We proceed by induction on n which produces two subgoals The first subgoal looks like the following Vg r div2 O q r gt 0 add nat_of_bool r twice q We may introduce q r and the hypothesis H div2 0 q r Note that the left hand side of this equation is not in normal form and we would like to reduce it We can do it by specifying a pattern for the normalize tactic introduced by the in keyword and delimited b
35. convertible The whole proof is hence HA B p cases p a tb qed Ap cases p can be replaced by When we call cases p we are actually applying the dependent elimination principle for the product so it becomes interesting to have a look at it VA B VP AXB Prop Va A Vb B P a b gt Vz AxB Px The previous principle has a very natural backward reading in order to prove that the property P holds for any of type AxB is is enough to prove P a b for any a A and b B By reflecting in Type 0 the definition of logical disjunction we obtain the disjoint union the sum of two types inductive Sum A B Type 0 Type 0 inl A Sum A B inr B gt Sum A B notation huboxla break b left associative with precedence 55 for plus a b y interpretation Disjoint union plus A B Sum A B The two constructors are the left and right injections The dependent elimination principle has the following shape VA B VP A B Prop Va A P inl a gt Vb B P inr b gt Vz A B P x that is in order to prove the property P for any 2 4 B it is enough to prove P inl a and P inr b for all a A and b B The counterparts of False and True are respectively an empty type and a sin gleton type P inductive void Type 0 inductive unit Type 0 it unit The elimination principle for void is simply VP void Prop Va void P z stating that
36. e2 pre S ez e2 e1 Il fst e2l Uleg theorem sem_ostar VS Ve pre S e e Ifst el Journal of Formalized Reasoning Vol 7 No 2 2014 Matita Tutorial i 157 For example let us look at the proof of the latter Given e 4 b we proceed by case analysis on b If b is false the result is trivial if b is true we have 4 true Cfst e 2 JUtet by definition of fst e 4 fst lero ULte by definition of fst e 4 lel Utet by erase_bullet e 4 fe Iil UL by minus_eps_pre zJ Ul al fe lil Ue by sem_bullet 24 fe UC IA IU by distr_minus 2z U lil 109 lil Ut by minus_eps_ item f l2l U li lil U e by distr_cat_r f 121J U I lt 1 by star_fizx_eps JuUto ll by distr_cat_r 4 true 141 by definition of 6 9 Moves We now define the move operation corresponding to the advancement of the state in response to the processing of an input character a The intuition is clear we have to look at points preceding the given character a allow the point to traverse the character and broadcast it All other points must be removed We can give a particularly elegant definition in terms of the lifted operators of the previous section let rec move S DeqSet a S E pitem S on E pre S match E with pz pz S false pe pe S false ps y ps S y false pp y ps S x y the point is advanced
37. eprint arXiv 1010 2604 2010 Henk Barendregt Lambda Calculi with Types In Abramsky Samson and others editor Handbook of Logic in Computer Science volume 2 Oxford Uni versity Press 1992 Herman Geuvers Proof Assistants history ideas and future Sadhana 34 1 3 25 2009 Jean Yves Girard Yves Lafont and Paul Taylor Proofs and Types volume 7 of Cambridge Tracts in Theoretical Computer Science Cambridge University Press 1989 Burt Jacobs Categorical Logic and Type Theory volume 141 North Holland 1998 Per Martin L f Intuitionistic Type Theory Bibliopolis 1984 Alexandre Miquel and Benjamin Werner The not so simple proof irrelevant model of CC In Herman Geuvers and Freek Wiedijk editors Types for Proofs and Programs International Workshop TYPES 2002 volume 2646 of Lecture Notes in Computer Science pages 240 258 Springer Verlag 2003 Christine Paulin Mohring D finitions Inductives en Th orie des Types d Ordre Sup rieur Habilitation diriger les recherches Universit Claude Bernard Lyon I December 1996 Claudio Sacerdoti Coen and Enrico Tassi Nonuniform coercions via unification hints volume 53 of EPTCS pages 16 29 2011 Claudio Sacerdoti Coen Enrico Tassi and Stefano Zacchiroli Tinycals step by step tacticals In Proceedings of User Interface for Theorem Provers 2006 volume 174 of Electronic Notes in Theoretical Computer Science pages 125 142 Elsevier Science 2006 Morten Heine Soren
38. filtering from pairs in AxB those satisfying the test Ap f fst p snd p as expressed by the following definition definition graph_enum A4 B FinSet Af A gt B filter Ap f fst p snd p enum FinProd A B The proofs that this enumeration does not contain repetitions and is complete are straightforward 5 9 Vectors A vector of length n of elements of type A is simply defined in Matita as a record composed by a list of elements of type 4 plus a proof that the list has the expected length Vectors are a paradigmatic example of dependent type that is of a type whose definition depends on a term record Vector A Type 0 n nat Type 0 vec gt list A len length vec n Given a list 1 we may trivially turn it into a vector of length 11 we just need to prove that 21 21 which follows from the reflexivity of equality Journal of Formalized Reasoning Vol 7 No 2 2014 146 E A Asperti and W Ricciotti and C Sacerdoti Coen i lemma Vector_of_list A l mk_Vector A 1 1 refl Most functions operating on lists can be naturally extended to vectors interesting cases are vec_append concatenating vectors and vec_map mapping a function f on all the elements of the input vector and returning a vector of the same length as the input one Since a vector is automatically coerced if needed to the list of its elements we may simply use typical functions over lists such as n
39. gt A the system will complain about the type of h The issue is that the type of this term depends on a that itself depends non trivially on the input argument z In such a Journal of Formalized Reasoning Vol 7 No 2 2014 Matita Tutorial i 131 situation the type inference algorithm of Matita requires a little help in particular the user is asked to explicitly provide the return type of the match expression that is a map uniformly expressing the type of all branches of the case as a function of the matched expression In our case we only have one branch and the return type is As P Sig_fst A P x we declare such a type immediately after the match introduced by the keyword return definition Sig_snd VA P Va Sig A P P Sig_fst A P x 4A P match g return Az P Sig fst A P x with Sig intro a h gt h REMARK 2 We already did a systematic abuse of the arrow symbol the es pression A B was sometimes interpreted as the implication between A and B and sometimes as the function space between A and B Actually in a foundational sys tem like the Calculus of Construction they are the very same notion we only distinguish them according to the sort of the resulting expression Similarly for the dependent product Iz 4 B if the resulting expression is of sort Prop we shall look at it as a universal quantification using the notation Vx A B while if it is in some Type li we shall typically regard it as a genera
40. hypothesis The goal will become node n c d node n c d Anode n a b node na b which is easily closed by reflexivity notice that destruct has also performed unifica tion in the context changing the type of a and b to from SBBT S m to SBBT S n Journal of Formalized Reasoning Vol 7 No 2 2014 150 A Asperti and W Ricciotti and C Sacerdoti Coen 6 A FORMALIZATION EXAMPLE REGULAR EXPRESSIONS AND DFA As a first non trivial application of the notions we have been studying so far we shall investigate in this section some basic results on regular expressions and deterministic finite automata In particular we shall provide a formal construction of the deterministic finite automaton associated with a given regular expression and a fully verified bisimilarity algorithm to check regular expression equivalence Our approach is based on the notion of pointed regular expression pre intro duced in 11 1 A pointed regular expression for e is just a regular expression e internally labelled with some additional points Intuitively points mark the po sitions inside the regular expression which have been reached after reading some prefix of the input string or better the positions where the processing of the re maining string has to be started Each pointed expression for e represents a state of the deterministic automaton associated with e since we obviously have only a finite number of possible labellings the number of state
41. if z y erased otherwise po el e2 move x el G move z e2 pc el e2 move x el move x e2 pk e gt move ey EXAMPLE 4 Let us consider the PRE eate eb eated b and the two moves w r t the characters a and b For a we have two possible positions all other points gets erased the innermost point stops in front of the final the other one is broadcasted inside b a b b so move a ea e eb ea teb b Cate od eated eb false For b we have two positions too The innermost point stops in front of the final b too while the other point reaches the end of b and must go back through b a move b eate eb eateb b Cate obd eatb eb false Obviously a move does not change the carrier of the item as one can easily prove by induction on the item Journal of Formalized Reasoning Vol 7 No 2 2014 158 A Asperti and W Ricciotti and C Sacerdoti Coen l gt lemma same_carrier VS DeqSet Va S Vi pitem S I fst move a i 1l Here is our first major result theorem move_ok VS DeqSet Va S Vi pitem S move a i deriv i a The proof is a simple induction on 7 Let us see the case of concatentation move a 1 42 move a 110 move a ta by def of move move a 11 lfst move a i2 Ulmove a i2 by sem odot move a 11 1 21 JU move a i by same_carrier deriv iiJ 1421 UCderiv 12 0 by ind hyp deriv 21
42. next step that consists of moving the wolf Suppose that instead of specifying the next intermediate state we prefer to specify the next move In the spirit of the previous example we can do it in by simply instantiating more with the suitable move that is more move_wolf The dots stand here for an arbitrary number of implicit arguments to be guessed by the system and can be typed in Matita as ldots Unfortunately the previous move is not enough to fully instantiate the new in termediate state and we obtain the following goals goal type X reachable mk_state east east east east mk_state east W west W Y safe_state mk_state east W west W Z opp W west W bank In particular the bank towards which we move W remains unknown we know that it is the opposite of the current one 2 but this information is still implicit Journal of Formalized Reasoning Vol 7 No 2 2014 108 E A Asperti and W Ricciotti and C Sacerdoti Coen Automation cannot help here since all goals depend from the bank w they are in a same cluster in Matita terminology and automation refuses to close some subgoals instantiating other subgoals remaining open the instantiation could be arbitrary The simplest way to proceed is to focus on the bank that is the fourth subgoal and explicitly instantiate it Instead of repeatedly using we can perform focusing by typing 4 as described by the following command 4
43. the n th element of the trace is accessed all the elements in position lt n are computed too let rec compute_trace_seq s state n nat on n option state match n with 0 gt Some s Sm gt match compute_trace_seq s m with None gt None Some o gt step o Journal of Formalized Reasoning Vol 7 No 2 2014 176 A Asperti and W Ricciotti and C Sacerdoti Coen We can emphasize that the initial state of the trace computed by the previous function is s by returning a suitable sigma type definition compute_trace Vs state Uit trace tr t 0 Some s ts 7 compute_trace_seq s n o elim n whd in 77 77 7 EQ destruct n tn _ H whd in whd in 77 7 gt H qed 8 3 Infinite data types as coinductive types All the previous examples were handled very easily via sequences declared as func tions A few criticisms can be made to this approach though 1 the sequence allows for random access In many situations however the ele ments of the sequence are meant to be read one after the other in increasing order of their position Moreover the elements are meant to be consumed read linearly i e just once This suggests a more efficient implementation where sequences are implemented with state machines that emit the next value and enter a new state every time they are read Indeed some programming languages like OCaml differ
44. the next section 5 2 Lists Options products and sums are simple examples of polymorphic types that is types that depend in a uniform and effective way on other types This form of Journal of Formalized Reasoning Vol 7 No 2 2014 138 E A Asperti and W Ricciotti and C Sacerdoti Coen polymorphism sometimes called parametric polymporphism to distinguish it from ad hoc polymorphism also known as overloading is a major feature of modern functional programming languages in many interesting cases it allows us to write generic functions operating on inputs without depending on their type We illus trate this with a typical polymorphic type lists For instance appending two lists is an operation that is essentially independent of the type 4 of the elements in the list and we would like to write a single append function working parametrically on A The first step is to define a type for lists polimorphic on the type A of its elements inductive list A Type 0 Type 0 nil list A cons A gt list A gt list A The definition should be clear a list is either empty nil or is obtained by prefixing cons an element of type 4 to a given list In other words the type of lists is the smallest inductive type generated by the two constructors nil and cons The first element of a list is called its head If the list is empty the head is undefined as discussed in the previous section we should either return a
45. the system that the variable is expected to be an identifier Matita abstract syntax trees include lambda terms as primitive data types and the previous declaration simply maps the notation dz T P into a content term of the form ezists Aa T P where 7 and P are the content term obtained from T and P The interpretation is then straightforward Journal of Formalized Reasoning Vol 7 No 2 2014 Matita Tutorial e 123 r N interpretation egists exists x ex 2 Our notational language has an additional list operator for dealing with variable sized terms having a regular structure This operator has a corresponding fold operator used to build up trees at the content level For example in the case of quantifiers it is customary to group multiple variable declarations under a same quantifier writing e g dz y z P instead of 3x 3y 3z P This can be achieved by the following notation used only during parsing as specified by the gt symbol notation gt exists list1 ident z sep opt T term 19 Pr with precedence 20 for default fold right GQ Pa rec acc G exists A ident x T acc Ot fold right G Px rec acc Ol exists A ident x acc y The presentational pattern matches terms starting with the existential symbol followed by a list of identifiers separated by commas optionally terminated by a type declaration followed b
46. 1 with nil gt mil A cons a tl gt rev A tl a lG However this implementation is sligtly inefficient since it has a quadratic complex ity A better solution consists of exploiting an accumulator passing through the following auxilary function pen rec rev_append S 11 12 list S on l1 match 11 with nil gt 12 cons a tl gt rev_append S tl a 12 J definition reverse AS Al rev_append S 1 Journal of Formalized Reasoning Vol 7 No 2 2014 140 E A Asperti and W Ricciotti and C Sacerdoti Coen Exercise Prove the following results gt lemma reverse_cons VS a l reverse S a 1 reverse S 1 a lemma reverse_append VS 11 12 reverse S 11 12 reverse S 12 reverse S 11 lemma reverse_reverse VS l reverse S reverse S 1 l For a solution look into the file basics lists list ma in the standard library 5 3 List iterators In general an iterator for some data type is an object that enables us to traverse its structure performing a given computation There is a canonical set of iterators on lists deriving from programming experience In this section we shall review a few of them proving some of their properties A first famous iterator is the map function that applies a function f to each element of a list az an building the list f a1 f an let rec map 4 B Typel01 f A gt B l list A on l list B match l with
47. 11 12 foldr At acc map f i 12 acc 11 The folded function Ai acc map f i 12 acc takes as input an element i and an accumulator and adds to the accumulator the values obtained by mapping the partial instantiation f i on the elements of 12 This function is iterated over all elements of the first list 11 starting with an empty accumulator 5 4 Naive Set Theory Given a universe U an arbitrary type U Type i for some i a practical way to deal with subsets of Vis simply to identify them with their characteristic property i e as functions of type U Prop For instance the empty set is defined by the False predicate a singleton set x is defined by the property that its elements are equal to g definition empty_set U Type 0 Au U False definition singleton AU Az2 u U z u The membership relation is trivial an element z is in the set defined by the property P if and only if it enjoys the property o definition member U Type 0 Au U P Prop U P u The operations of union intersection complementation and difference are defined in a straightforward way in terms of logical operations N definition union AU TypelO AP Q U gt Prop a P a VQ a definition intersection U Type 0 AP Q U Prop a P a AQ a definition complement U Type 0 A A U gt Prop Aw gt A uw definition difference AU Type l01 14 B U Prop Aw A wA B u
48. 6 6 5 ee be ee ee ees 5 11 A heterogeneous notion of equality 20 A formalization example regular expressions and DFA 6 1 Words and Languages o 0 2 44 02 Regular Expressions oo c ngpa 2666500 AAA A ee 6 3 Pointed regular expressions 6 4 Intensional equality of PRES ha Broadcasting points q aoe dos e ar e e an e a Oe ee aes 00 PAWAN e o a a a AAA Br ya BARS occiso iia paddle 0S Lied OPEL so al acetate dd a a RARA AAA EA Mewes gt lt a as aaa ear a 6 10 Regular expression equivalence o o Journal of Formalized Reasoning Vol 7 No 2 2014 Matita Tutorial 7 Quotienting in type theory 7 1 Rewriting setoid equalities o e o sa saaa o T2 Dependent setoids 666065544446 wee eee d idamaa 7 3 Avoiding setolds 2 2 4 58444 546 20 bd dew ee ee 8 Infinite structures and Coinductive Types 8 1 Real Numbers as Cauchy sequences o ooo 82 Traces OLA programi eo ke ROR EER RRR Ce HES 8 3 Infinite data types as coinductive types 8 4 Real numbers via coinductive types 00 4 8 5 Intermezzo the dynamics of coinductive data 8 6 Traces of a program via coinductive types 8 7 How to compare coinductive types o 8 8 Generic construction principles o a 9 Logical Restrictions 9 1 Positivity in inductive definitions
49. 7 7 The pattern specifies that the term is an application of one term called head of the application to three arguments the head and the first two arguments are generic this is expressed by the symbol while the last argument is itself an application with one head and two arguments the former of which should be the scope of a tactic as expressed by the symbol Notice that the pattern sublanguage does not understand at all user defined notation comprising that defined in the standard library therefore a pattern in the form is not legal Patterns can be used to identify a path in either a hypothesis or in the conclusion by means of the following syntaxes normalize in H 4 rewrites in the conclusion normalize in H1 7 7 rewrites in hypothesis H1 We use vdash to insert the symbol which is required when specifying a subterm in the conclusion Patterns are not restricted to applicative terms but can be used under all cir cumstances in arrow types in a term 2 1 2 gt 0 774 7 specifies the first z Journal of Formalized Reasoning Vol 7 No 2 2014 118 A Asperti and W Ricciotti and C Sacerdoti Coen within binders in Vz y nat P 2xy V_ _ specifies x xy notice that in the pattern bound variables can be replaced by the _ don t care placeholder within a match match with _ gt _ gt specifies the subterm contained in the f
50. Matita Tutorial ANDREA ASPERTI DISI Dipartimento di Informatica Universita degli Studi di Bologna and WILMER RICCIOTTI IRIT Universit de Toulouse and CLAUDIO SACERDOTI COEN DISI Dipartimento di Informatica Universita degli Studi di Bologna This tutorial provides a pragmatic introduction to the main functionalities of the Matita interac tive theorem prover offering a guided tour through a set of not so trivial examples in the field of software specification and verification Contents O Getting Started 94 Dl Trstelling Matta os cercos idad AA wee 94 0 2 Preparing a working directory o c coic orao ace a a a a a 95 o AN 95 0 4 Browsing the library isos ooo p 1 es 96 AAA A A ha eS a a ea BR ee a ees 97 DU Maula WER osos as PEP a ee AA 98 1 Data Types Functions and Theorems 99 1 1 The goat the wolf and the cabbage o 99 1 2 Defining ECOS cda ca a Ew re ae eS 100 L3 Que host lei coo sa eS aw REE Se ae aes 101 1 4 Introducing hypothesis in the context 102 lo Casc analysis ee ae a ee Oe eee a a aa aaa 102 6 e o caos tra a E a 103 Lf Rew oe os oa a a aea e a e p a A 103 US o EE AA eee BG 104 LO Automation oo ee 4 44 a a e eda a E eS 105 L O Application oco a ek AA a AA AA ROA RRA 105 INTA POLUSME a o a e dd RB wl ete ees 106 1 12 Implicit arguments and partial instantiation 107 2 Induction 109 Sal PUA aa ar Se Relay at ets 109 pie EROTI woe
51. RussellP Russell False whd in match Russell whd in 437 H cases H carrier_def 7 H1 H1 gt member_to_P OH Journal of Formalized Reasoning Vol 7 No 2 2014 196 E A Asperti and W Ricciotti and C Sacerdoti Coen qed Moreover assuming proof irrelevance P axiom irrel VA P Vh1 h2 carrier c A P A hi h2 lemma RussellP_Russell RussellP Russell whd in match Russell th cut carrier_def h irrel Hcut lt Hcut gt member_to_P not_RussellP_Russell qed Journal of Formalized Reasoning Vol 7 No 2 2014 Matita Tutorial e 197 10 FURTHER READINGS Unfortunately there is no really good theoretical introduction to modern depen dent type theory The best textbook probably remains old Martin L6f s monograph 16 that however does not address any major metatheoretical issue normaliza tion consistency etc For the simply typed lambda calculus system T and system F i e the poly morphic lambda calculus an excellent introductory text is the book by Girard et al 14 in it the reader may also find a clear explanation of the so called impred icative encoding of inductive types that is a way for expressing inductive types using higher order polymorphism For pure type systems PTSs i e various systems of typed lambda calculi comprising types dependent on terms but not explicit inductive definitions a very clear but a bit dry reference is Barendergt s mo
52. Since we make frequent use of logical connectives and quantifiers it would be nice to have the possibility to use a more familiar looking notation for them Matita offers you the possibility to associate your own notation to any notion you define To exploit the natural overloading of notation typical of scientific literature its management in Matita is split in two steps one from presentation level to content level where we associate a notation to a fragment of abstract syntax and one from content level to term level where we provide possibly multiple interpretations for the abstract syntax The mapping between the presentation level i e what the user writes as input and what is displayed in the goal panes and the content level is defined with the notation command notation hvboxr a break land b left associative with precedence 35 for and a b y This declaration associates the infix notation a land b rendered as a b by a built in Unicode mapping with an abstract syntax tree composed by the new symbol and applied to the result of the parsing of input argument a and b The presentation pattern is always enclosed in double quotes The special key word break indicates the line breaking point and the box schema hvboz indicates a horizontal or vertical layout according to the available space for the rendering they can be safely ignored for this tutorial The content pattern begins right after the for keyword and
53. The definition of e eclose and gt pre_concat_1 are mutually recursive In item pre item 41 42 41 lt le2 41 lt 42 b 41 42 b pre ejbia e10 e2 41 true Pig lt e 12 e10 i2 b let 4 b ejbia 41 false Pig 41 2 false in i bV b Fig 3 Concatenations between items and PREs and respective equations this situation a viable alternative that is usually simpler to reason about is to abstract one of the two functions with respect to the other definition pre_concat_l AS Abcast VS pitem S gt pre S Ael pre S Ai2 pitem S let i1 b1 el in if b1 then i1 lt bcast 12 else i1 12 false Journal of Formalized Reasoning Vol 7 No 2 2014 Matita Tutorial 7 155 ret rec eclose S DeqSet i pitem S on 1 pre S match with pz gt pz S false pe gt pe S true ps x gt ps S a false pp x gt pp S a false po 11 12 gt eil GPei2 pc il 12 gt etl gt i2 pk i gt Cfst e1 true The definition of eclose can then be lifted from items to PREs definition lift S Af pitem S gt pre S Xe pre S let 1 b e in fst f i snd f 1 VD definition preclose S lift S eclose S By induction on the item 7 it is easy to prove the following result lemma erase_bullet VS Vi pitem S fst el lil 6 6 Semantics We are now ready to state the m
54. Vol 7 No 2 2014 184 f A Asperti and W Ricciotti and C Sacerdoti Coen because we need to use the expansion lemma above to rewrite the type of the scons branch Otherwise Matita rejects the term as ill typed let corec div_well_formed_co_mk_diverging_trace_to_div_trace t stream state VW well_ formed t VH diverging t div_well_formed_co mk_diverging_trace_to_div_trace t H match t return At well_formed t diverging t gt with snil gt A_ Aabs scons hd tl gt AW AH cases False inversion abs hd tl _ eq destruct cases mk_diverging_trace_to_div_trace_expansion H H eq lapply sym_eq eq Req cases Req Req eq H cases tl in W P _ abs cases False inversion abs hd tl _ eq destruct tl hd2 tl W H cases mk_diverging_trace_to_div_trace_expansion H K eq gt eq inversion W ts _ abs destruct hd1 hd2 tl eq1 wf eq2 lapply eqi cut hd hd1 Ahd2 hd2 Atl tl destruct 3 eq2 tegl 7 step_next lt eq div_well_formed_co_mk_diverging_trace_to_div_trace 11 qed theorem diverging_trace_to_div_trace Vt trace diverging t gt 3d div_trace head_of_stream t Some head_of_streamseq d t H mk_diverging_trace_to_div_trace H div_well_formed_co_to_div_well_formed div_well_formed_co_mk_diverging_trace_to_div_trace well_formed t ca
55. ain semantic properties of 6 gt lt and e lemma sem_oplus VS DeqSet Vel e2 pre S el 9 e2 ei U e2 lemma sem_pre_concat_r VS i Ve pre S i lt e i Ifst el U e lemma sem_pre_concat_l VS Vel pre S Vi2 pitem S ep ti e 131 U i theorem sem_bullet VS DeqSet Vi pitem S et i U lel The proofs of sem_oplus and sem_pre_concat_r are straightforward For the others we proceed as follow we first prove the following auxiliary lemma that assumes sem_bullet lemma sem_pre_concat_l_auz VS Vel pre S Vi2 pitem S ez2 22 U l 21 gt ez gt i2 et I 21 U 22 Then using the previous result we prove sem_bullet by induction on i Finally sem_pre_concat_l_auz and sem_bullet give sem_pre_concat_l It is important to observe that all proofs have an algebraic flavor Let us consider for instance the proof of sem_pre_concat_l_auz Assuming es 71 61 we proceed Journal of Formalized Reasoning Vol 7 No 2 2014 156 A Asperti and W Ricciotti and C Sacerdoti Coen by case analysis on b If b is false the result is trivial if b is true we have 41 true lt i2 iibe 42 by def of lt 11 Ifst e i2 1JUle i2 by sem pre_concat_r 21 1121uU 2JU 21 by erase_bullet and sem_bullet 41 1421 JULI 22 1JU 2 by assoc and comm tJUten I 12 Uz by distr_cat_r 41 true l 21 JU ze by the semanti
56. al elements the type of natural numbers satisfies the equation nat unit nat The reasoning can be generalized to any inductive type X In particular X must be isomorphic to the disjoint sum 4aLT of the Cartesian product of the types of the constructor s arguments To take another example let us consider the type of lists Journal of Formalized Reasoning Vol 7 No 2 2014 192 5 A Asperti and W Ricciotti and C Sacerdoti Coen on a parametric type A In this case list A unit HAX list A The delicate issue is to ensure the existence of solutions to such recursive domain equations see e g 2 for an introduction In general the standard approach to solve a recursive definition is to look for a fixed point There are a lot of interesting fixed point theorems in mathematics but one that is particularly simple and appealing is the Knaster Tarski theorem This theorem says that if L is a complete lattice and f L gt Lis a monotone function then the set of fixed points of f is also a complete lattice In particular there is a least fixed point wf as well as a greatest fixed point vf A lattice is just a degenerate case of a category Instead of having elements and a partial order relation on them in a category we have a collection of objects and for each pair of objects a b a collection hom la b of morphisms from a to b we write f a gt b to express that f homla b Morphisms are supposed to be closed unde
57. ality x y true into a propositional equality z y and vice versa and are con verted to instances of egb_ true of course z and y must belong to a DegSet in order for this notation to work P notation a b non associative with precedence 45 for eqb a b interpretation egb eqb a b eqb a b notation P H non associative with precedence 90 for proji eqb_true H notation b H non associative with precedence 90 for Ot proj2 eqb_true H Suppose we proved the following facts do it as an exercise lemma begb_true_to_eq Vb1 b2 beqb bi b2 true b1 b2 lemma neqb_true_to_eq Vn m nat eqb n m true gt n m Then we can build the following records definition DegBool mk_DeqSet bool beqb beqb_true_to_eq definition DeqNat mk_DeqSet nat eqb eqbnat_true Note that since we declared a coercion from the DegSet to its carrier the expression 0 DeqNat is well typed and it is understood by the system as 0 carr DeqNat 5 6 Unification hints Now suppose we need to write an expression of the following kind b false that after removing the notation is equivalent to eqb b false The system knows that false is a boolean so in order to accept the expression it should figure out some DegSet having bool as carrier This is not a trivial operation Matita should either try to synthesize it which is a complex operation known as narrowi
58. am_of_streamseq_expansion Qwell_formed_stream_of_streamseq tn OCH S n next_step H 0 qed theorem div_trace_to_diverging_trace Vd div_trace Jt trace diverging t head_of_stream t Some head_of_streamsegq d d mk_trace stream_of_streamseq d 2 1 cases d qed 8 7 How to compare coinductive types Inhabitants of inductive types are compared using Leibniz s equality that on closed terms coincides with convertibility The situation is radically different in the case of coinductive types Because of the restrictions for the evaluation strategy see Section 8 5 two inhabitants of coinductive types even if closed may not be con vertible having distinct normal forms but can be shown to be Leibniz equal For example the following two definitions in normal form produce the same streamseq 0 1 0 1 but are not equal because the normal forms are syntactically different 7 let corec zero_one_streamseq1 streamseq N sscons 0 sscons 1 zero_one_streamseq1 let corec one_zero_streamseq streamseg N sscons 1 sscons 0 one_zero_streamseg definition zero_one_streamseq2 streamseq N sscons 0 one_zero_streamseq Journal of Formalized Reasoning Vol 7 No 2 2014 186 y A Asperti and W Ricciotti and C Sacerdoti Coen In place of Leibniz equality the right notion to compare coinductive terms is bisimulation Two
59. an be useful to acquire confidence with inductive types and to get a better theoretical grasp on them 3 1 Conjunction In natural deduction logical rules for connectives are divided in two groups there are introduction rules allowing us to introduce a logical connective in the conclusion and there are elimination rules describing how to deconstruct information about a compound proposition into information about its constituents i e how to use a hypothesis having a given top level connective Consider conjunction In order to understand the introduction rule for conjunc tion you should answer the question how can we prove 4AB The answer is simple we must prove both A and B Hence the introduction rule for conjunction is A gt B gt 4 B The general idea for defining a logical connective as an inductive type is simply to define it as the smallest proposition generated by its introduction rule s For instance in the case of conjunction we define inductive And A B Prop Prop conj A B gt And A B The corresponding elimination rule is induced by minimality if we have a proof of AMB it may only derive from the conjunction of a proof of A and a proof of B A possible way to formally express the elimination rule is the following VA B P Prop A gt B gt P gt 4ANAB gt P that is for all A and B and for any proposition P if we need to prove P under the assumption 4A B we can reduce it to proving P u
60. an equation G1 G2 by first rewriting into E1 leaving a new goal G1 G2 Concretely it applies transitivity of notation l jr with precedence 90 for proper2 1 r y interpretation mor_proper2 proper2 z y mor_proper function_space x y notation with precedence 90 for reflea interpretation reflexivity reflez equiv_refl 7 interpretation symmetry invert r equiv_sym r notation r with precedence 55 for trans r Journal of Formalized Reasoning Vol 7 No 2 2014 Matita Tutorial i 169 notation r with precedence 55 for QA fi r definition fi VA B Prop A B gt B gt 4 24 B r proj2 r interpretation fi fir fi r The following example shows several of the features at once 1 the first occurrence of z2 is turned into 21 by rewriting the hypothesis from right to left 2 the first occurrence of 21 is turned into 22 by rewriting the hypothesis from left to right 3 the two rewritings are performed at once 4 the subterm z y does not need to be rewritten Therefore a single is used in place of 4 which is also correct but produces a larger proof 5 we can directly start with an application of because the goal is a setoid equality example exZ Vzxl m2 y 2 Z tl 12 gt y 22 21 z y y 21 12 z y x1 202 ty tz HEQ OC IEQ 1 EQi qed The following examp
61. an interesting result checking if 1 is a bisimulation is decidable hence we could generate 1 with some untrusted piece of code and then run a boolean version of is_bisim to check that it is actually a bisimulation However in order to prove that equivalence of regular expressions is decidable we must prove that we can always effectively build such a list or find a counterexample The idea is that the list we are interested in is just the set of all pair of PREs reachable from the initial pair via some sequence of moves The algorithm for computing reachable nodes in a graph is a very traditional one We split nodes in two disjoint lists a list of visited nodes and a frontier composed of all nodes connected to a node in visited but not visited already At each step we select a node a from the frontier compute its childrens add a to the set of visited nodes and the not already visited childrens to the frontier Journal of Formalized Reasoning Vol 7 No 2 2014 Matita Tutorial i 161 Instead of first computing reachable nodes and then performing the bisimilarity test we can directly integrate it into the algorithm the set of visited nodes is closed by construction w r t reachability so we just have to check cofinality for any node we add to visited Here is the extremely simple algorithm let rec bisim S l n frontier visited list on n match n with 0 false visited unreachable code Sm gt match frontier w
62. c transitive_ss_bisimilar A Type 0 transitive ss_bisimilar A hd1 tl1 hd2 tl2 hd3 tl3 thd tl1 tl2 H1 H inversion H hd tl1 tl2 H HH EQ1 _ cut hd hd A tl1 tl2 destruct 2 HEQ Y transitive_ss_bisimilar qed definition STREAMSEQ Type 0 setoid AA mk_setoid streamseq A mk_equivalence_relation ss_bisimilar A qed unification hint 0 A Type 0 X STREAMSEQ A streamseq A carrier X As an example we lift streamseg_nth to a morphism A definition STREAMSEQ_NTH VA Typel0l STREAMSEQ A LEIBNIZ N LEIBNIZ A AA mk_bin_morphism streamseq_nth A 21 22 nl n2 bisim lapply bisim bisim lapply 12 x2 lapply x x1 n2 elim ni 21 422 H inversion H m IH 01 02 H inversion H hd tl1 t12 bisim EQ1 EQ2 destruct IH qed Working with setoids introduces technical complications that one would rather avoid The alternative encoding of streams via sequences does not solve the issue Sequences are functions and to capture the mathematical meaning of equality for sequences functions need to be compare using functional extensionality Two functions are extensionally equal when they are pointiwse equal i e they map equal inputs to the same outputs Intensional equality of functions in contrast just compares the two codes For example the next
63. cs of pre As another example let us consider the proof of sem_ bullet The proof is by induction on i let us consider the case of 41 42 We have e Ci 12 0 41 lt 2 by definition of e e 413 1 2 Uf ze by sem_pre_concat_l 4 JUL 41 1 42 1JUu 2 by induction hypothesis 41 1221JU 1411 1 lt 21Juli2 by distr_cat_r 41 1421JUli2DU Ii1 21 by assoc and comm 41 120 JUL 41 221 by definition of 6 7 Initial state As a corollary of theorem sem_bullet given a regular expression e we can easily find an item with the same semantics of e it is enough to get an item blank S e having e as carrier and no point and then broadcast a point in it e blank S e blank S e Ule el The definition of blank is straightforward its main properties both proved by an easy induction on e are the following lemma forget_blank VS Ve re S blank S el e lemma sem_blank VS Ve re S blank S el 0 theorem re_embedding VS Ve re S e blank S e e 6 8 Lifted operators plus and eclose have been already lifted from items to PREs We can now do a similar job for concatenation and and Kleene s star 9 N definition lifted_cat AS DeqSet Ae pre S lift S pre_concat_l S eclose e definition lk S DeqSet Xe pre S let i1 b1 e in if bi then fst eclose i1 true else i1 false We can easily prove the following properties lemma sem_odot VS Vel
64. ctions as previously explained for eta_streamseq lemma eta_stream VA Typel0 Vs stream A match s with snil gt snil scons hd tl gt scons hd tl s HA qed In order to give the formal definition of a trace we first need to coinductively define the well_formedness predicate whose definition is slightly more complex than the previous one coinductive well_formed stream state Prop wf_snil Vs step s None gt vwell_ formed scons s snil wf_scons Vhd1 hd2 tl step hd1 Some hd2 gt Journal of Formalized Reasoning Vol 7 No 2 2014 Matita Tutorial i 183 well_formed scons hd2 tl gt well_formed scons hd1 scons hd2 tl Note we could have equivalently defined wett_formed avoiding coinduction by defining a recursive function to retrieve the n th element of the stream if any From now on we will stick to coinductive predicates only to show more examples of usage of coinduction In a formalization however it is always better to explore several alternatives and see which ones work best for the problem at hand record trace Type 0 tr gt stream state well_formed well_formed tr The trace is diverging if every state is not final Again this can be defined by means of a coinductive definition a D coinductive diverging stream state Prop mk_diverging Vhd tl diverging tl
65. culus of Inductive Constructions known as strong elimination Suppose now we want to prove the following property theorem not_eq 0S Vn nat O S n gt False Journal of Formalized Reasoning Vol 7 No 2 2014 126 s A Asperti and W Ricciotti and C Sacerdoti Coen After introducing n and the hypothesis H 0 S n we are left with the goal False Now observe that also not_zero Ois false actually not_zero O reduces to False and the two terms are actually convertible that is identical So it should be possible to replace False with not_zero Oin the conclusion since they are the same term The tactic that does the job is the change with tactic The invocation of change with t checks that the current goal is convertible with t and in this case t becomes the new current goal In our case typing change with not_zero 0 we get the new goal not_zero 0 But we know by H that 0 S n hence by rewriting we get the goal not_zero S n that reduces to True whose proof is trivial use I or Here is the complete proof n H change with not_zero 0 gt H qed Using a similar technique you can always prove that different constructors of the same inductive type are distinct from each other actually this technique is also at the core of the destruct tactics of Section 2 5 in order to automatically close absurd cases 3 6 Inversion The only type that really needs arguments is equality In al
66. current value nis returned as head of the stream seq and the tail of the streamseq is the automaton with state S n In order to retrieve the n th element from a streamseq we can write a function recursive on n let rec streamseg_nth A Typel01 s streamseg A n N on n A match s with sscons hd tl gt match n with 0 gt hd S m streamseg_nth tl m Any sequence can be turned into the equivalent streamseq and the other way around let corec streamseq_of_seq A Type 0 s seq A n N streamseq A Journal of Formalized Reasoning Vol 7 No 2 2014 178 5 A Asperti and W Ricciotti and C Sacerdoti Coen sscons s n streamseq_of_seq A s S n lemma streamseq_of_seq_ok VA Type 0 Vs seq A Vm n streamseg_nth A streamseq_of_seq s n m s mn HA Hs ttm elim m normalize qed definition seq_of_streamseq VA Type 0 streamseq A seq A streamseq_nth lemma seq_of_streamseq_ok VA Type 0 Vs streamseg A Vn seg _of_streamseg s n streamseq_nth Sn qed 8 4 Real numbers via coinductive types In thi section we closely follow the content of Section 8 1 replacing sequences with streamseqs definition Qstreamseq Type 0 streamseq Q definition Qstreamseq_nth streamseq_nth Q Here is the Cauchy property definition Cauchy Qstreamseq gt Prop AR Qstreamseq Veps dn Vi j n Li gt n lt j gt Qdist Qstreamseq_n
67. d by automation example uncurrying_ez uncurrying plus 2 3 5 refl qed 4 4 The Curry Howard correspondence The philosophical ideas contained in the BHK interpretation of a proof as construc tive procedure building a proof of the conclusion from proofs of the hypothesis get a precise syntactic systematization via the Curry Howard correspondence expressing a direct relationship between computer programs and proofs The Curry Howard correspondence also known as proofs as programs analogy is a generalization of a syntactic analogy between systems of formal logic and computational calculi first observed by Curry for Combinatory Logic and Hilbert style deduction systems and later by Howard for A calculus and Natural Deduction in both cases the formation rules for well typed terms have precisely the same shape of the logical rules of in troduction of the correspondent connective as we already exploited in Sections 4 1 and 4 2 So the expression M A really has a double possible reading 1 M is a term of type A 2 M is a proof of the proposition A In both cases M is a witness that the object A is inhabited A free variable x A is an assumption about the validity of A we assume to have an unknown proof Journal of Formalized Reasoning Vol 7 No 2 2014 Matita Tutorial i 133 named x Let us consider the cases of the introduction and elimination rule of the implication in natural deduction that are particular
68. duct Ie A B If the sort of Bis Prop then Ilz 4 B Prop whatever the sort of A is If A Type i and B Type j then Iz 4 B Type k where Type k is the smallest sort strictly larger than Type i and Type j Typelx Typeli U Typel TrA s T xz AF B Prop TF A Typeli T x AF B Typelj TF A B Prop TF 2 A B Typelk It is worth observing that in Matita the index 7 is just a label constraints among universes are declared by the user The standard library see basics pts ma de clares a few of them with the following relations TypelO lt Typel1 lt Type 2 lt The impredicativity of Prop is not a problem from the point of view of logical consistency but there is a price to be paid for this we are not allowed to eliminate a proposition of type Prop when the current conclusion is a type of type TypeLil In concrete terms this means that while we are allowed to build terms types or even propositions by structural induction on terms the only thing we can do by structural induction case analysis on proofs is to build other proofs For instance we know that a proof of p AV Bis either a proof of 4 or a proof of B and one could be tempted to define a function that returns the boolean true in the first case and false otherwise by performing a simple case analysis on p definition discriminate_to_bool A4 B Prop Ap AV B match p with or_introl a gt true or_intror b gt false J
69. e 0 Vs streamseg A match s with sscons hd tl sscons hd tl s HA qed Journal of Formalized Reasoning Vol 7 No 2 2014 Matita Tutorial i 181 In order to prove now that all_zeros is equal to its definiendum it suffices to rewrite it using the eta_streamseq lemma in order to insert around the definiens the match destructor that triggers its expansion lemma all_zeros_expansion all_zeros sscons 0 all_zeros lt eta_streamseq all_zeros in F qed Expansions lemmas as the one just presented are almost always required to progress in non trivial proofs as we will see in the next example In contrast the equivalent expansions lemmas for let rec definitions are rarely required 8 6 Traces of a program via coinductive types A diverging trace is a streamseq of states such that the n 1 th state is obtained by executing one step from the n th state The definition of div_well_formed is the same we already used for sequences but on streamseqs cr definition div_well_formed streamseq state Prop As streamseq state Vn next streamseg_nth s n streamseg_nth s S n record div_trace Type 0 div_tr gt streamseq state div_well_formed div_well_formed div_tr The well formedness predicate on streamseq can also be redefined using as a coinductive predicate A streamseq of states is well formed if the second element is the next
70. e emphasized by a double circle since a state e b is final if and only if b is true we may just label nodes with the item Journal of Formalized Reasoning Vol 7 No 2 2014 Matita Tutorial e 159 alble Fig 4 DFA for ac bc The automaton is not minimal it is easy to see that the two states corresponding to the PREs aec bc and actbec are equivalent A way to prove it is to observe that they define the same language In fact each state has a clear semantics given in terms of the associated PRE e and not of the behaviour of the automaton As a consequence the construction of the automaton is not only direct but also extremely intuitive and locally verifiable EXAMPLE 6 Starting from the regular expression ate b a b b we obtain the automaton in Figure 5 ea Ellebea eb b Fig 5 DFA for ate b a b b Remarkably this DFA is minimal testifying to the small number of states produced by our technique the pair of states 6 8 and 7 9 differ for the fact that 6 and 7 are final while 8 and 9 are not Journal of Formalized Reasoning Vol 7 No 2 2014 160 A Asperti and W Ricciotti and C Sacerdoti Coen 6 10 Regular expression equivalence We say that two PREs 41 01 and i2 b2 are cofinal if and only if b1 b2 As a corollary of decidable_sem we have that two expressions e and ez are equiva lent iff for any word w the states reachable through w are cofinal
71. e every time we want to rewrite E1 with 2 under the assumption that E1 E2 we need to prove the context to be proper Most of the time the context is just a composition of morphisms and like in ex3 the only information that the user needs to give to the system is the position of the occurrences of E1 to be replaced and the equations to be used for the rewriting As for ex3 we can provide a simple syntax to describe contexts and equations at the same time The syntax is just given by a few notations to hide applications of mor_proper reflexivity symmetry and transitivity Here is a synopsis of the syntax fo to rewrite in the argument of a unary morphism _ _ to rewrite in both arguments of a binary morphism to avoid rewriting in this position t to rewrite from left to right in this position using the proof t Usually t is the name of an hypothesis in the context of type El E2 t 1 to rewrite from right to left in this position using the proof t Concretely it applies symmetry to t proving 2 E1 from El E2 to start rewriting when the goal PE1 is not an equation and the goal to be obtained is P 2 Concretely it applies the proof of P E2 P E1 obtained by splitting the double implication P E2 P 1 which is equivalent to P E2 P El where is the equality of the PROP setoid Thus the argument should be a proof of P E2 P 1 obtained using the previous symbols according to the shape of P to prove
72. ed to a normal form By the Curry Howard correspondence this should correspond to a normalization procedure on proofs does this operation make any sense at the logical level Again the answer is yes not only it makes sense but it was indepen dently investigated in the field of proof theory A reducible expression corresponds to what is traditionally called a cut a logical detour typically arising by an intro duction rule immediately followed by an elimination rule for the same connective as in a P redex where we have a direct interaction between an application and a A abstraction Ar MN One of the main meta theoretical results that is usually investigated on proof sys tems is if they enjoy the so called cut elimination principle that is if the cut rule is admissible any proof that makes use of cuts can be turned into a cut free proof Since cuts are redexes a cut free proof is a term that does not contain any redex that is a term in normal form Hence the system enjoys cut elimination if and only if the corresponding calculus is normalizing Cut elimination is a major tool of proof theory with important implications on e g consistency automation and interpolation Journal of Formalized Reasoning Vol 7 No 2 2014 134 A Asperti and W Ricciotti and C Sacerdoti Coen Logic Programming proposition type proof program cut reducible expression redex cut free normal form cut elimination normaliza
73. een defined as a coercion so that when S is a setoid we can write z Sin place of s carrier sS We use the notation for the equality on setoid elements N r notation huboz n break m non associative with precedence 45 for OL congruent n m y interpretation eg _setoid congruent n m eqrel eq _setoid 7 n m Example integers are traditionally defined as pairs n m of natural numbers quotiented by nl m1 n2 m2 iff nl m2 ml n2 The integer n is represented by any pair k n k while the integer n by any pair n k n If we write definition Z setoid mk_setoid N xN mk_equivalence_relation Ac1 c2 fst c1 snd c2 fst c2 snd c1 we are left with three proof obligations i e three open goals corresponding to reflexivity symmetry and transitivity of the given relation We can immediately close two of them by automation while transitivity requires some algebraic manip ulation Journal of Formalized Reasoning Vol 7 No 2 2014 Matita Tutorial 163 whd x1 02 y1 y2 21 23 H1 H2 cut 21 y2 yl 23 yl w2 z1 y2 H3 cut y2 y1 21 23 y2 y1 z1 22 H Cinjective_plus_r H4 qed The two integers 0 1 and 1 2 are equal up to written 0 1 1 2 Un folding the notation that corresponds to eqrel eq_setoid 0 1 1 2 which means that the two pairs are to be compared accord
74. eeping operations qed close the goal by invoking automation and add the theorem to the library In exactly the same way we can prove that the opposite side of west is east In this case we avoid the unnecessary simplification step will take care of it Journal of Formalized Reasoning Vol 7 No 2 2014 102 i A Asperti and W Ricciotti and C Sacerdoti Coen is lemma west_to_east opposite west east qed Instead of lemma you may also use theorem or corollary Matita does not attempt to make a semantic distinction between them and their use is entirely up to the user In some cases the normalize tactic is too aggressive since the normal form of a term can be very large and unreadable An alternative is the whd tactic that reduce terms only at the top level Moreover we will introduce patterns in Section 2 9 to better control reduction by restricting it to chosen subterms 1 4 Introducing hypothesis in the context A slightly more complex problem consists in proving that opposite is idempotent 7 lemma idempotent_opposite Va opposite opposite x z We start the proof by moving z from the conclusion into the context that is a backward introduction step Matita syntax for an introduction step is simply the sharp character followed by the name of the item to be moved into the context This also allows us to rename the item if needed for instance if we wish to rename z t
75. elp menu of the application The manual provides the comprehensive list of commands of Matita comprising their syntax and semantics 0 1 Installing Matita At present Matita only works on Linux based systems Both Debian and Ubuntu systems have packages called matita in the standard system repositories but we do not suggest to use them since they would install an out of date and incompatible version of the Matita system If you are running a Debian based system with APT installed you should first of all install the required dependencies by issuing the following command at a terminal window apt get install ocaml ocaml findlib libgdome2 ocaml dev liblablgtk2 ocaml dev liblablgtksourceview ocaml dev libsqlite3 ocaml dev libocamlnet ocaml dev libzip ocaml dev libhttp ocaml dev ocaml ulex08 libexpat ocaml dev libmysql ocaml dev camlp5 The next step is to prepare a directory for the Matita sources and binaries and enter it for instance issue the following series of commands cd 7 mkdir Matita cd Matita We shall henceforth refer to this directory as MATITA_HOME You should now down load and unpack from the Matita download page at http matita cs unibo it download shtml the most recent version of the Matita development source tarball at present this is matita_130312 tar gz Mf you are running the latest Ubuntu release the package liblablgtksourceview ocaml dev has been superseded by liblablgtksourceview2 ocaml dev Jou
76. ence 90 for OA pair a b interpretation Pair construction pair z y pair x y We can define the two projections fst and snd as a simple case analysis on the term definition fst A B p AXB match p with pair a b a definition snd A B A p AXB match p with pair a b gt b As in the case of inductive propositions Matita automatically generates elimination principles for AxB In this case however it is interesting to consider the possibility that the proposition towards which we are eliminating a given pair p AxB contains a copy of p itself In other words if we have p AxB in the current context it is possible that p also occurs in the current goal that is that the current goal depends on p A typical example is in the proof of the so called surjective pairing property lemma surjective_pair VA B Vp AXB p fst p snd p where p occurs in the conclusion The proof is straightforward we introduce A B and p and proceed by case analysis on p since pis a pair the only possible case is that it is of the form a b for some a and b At this point the goal looks like TThis is also possible when we are eliminating a proof h of a conjunction since proofs are first class and may occur inside other types but it is less frequent Journal of Formalized Reasoning Vol 7 No 2 2014 Matita Tutorial i 129 a b fst a b snd a b and the two sides of the equation are
77. ent of type Sig A Pisa pair Sig_intro a h we shall use the traditional pair notation a h where a is an element of type A and his a proof that the property P a holds A suggestive reading of of Sig A Pis as the subset of A satisfying the property P that is La A P a In the second case an element of DPair A Bis a dependent pair DProd_intro a h we shall use the following notation in this case a h gt where a is element of type a and h maps a into an element in B a the intuition is to look at DProd A Bas a disjoint family of sets B a indexed over elements a A In both cases it is possible to define projections extracting the two components of the pair Let us discuss the case of the sigma type the other one is analogous Extracting the first component the element is easy definition Sig fst A Type 0 AP 4 Prop Au Sig A P match x with Sig introah gt a Getting the second component is a bit trickier The first problem is the type of the result given a pair a h Sig A P the type of his P a that is P applied to the first argument of the pair of which we want to extract the second component Luckily in a language with dependent types it is not a problem to write such a type definition Sig_snd VWA P Va Sig A P P Sig_fst A P x A subtler problem occurs when we define the body If we just write definition Sig_snd VA P Vz Sig A P P Sig _fst A P x 2M4 P z match x with Sig_intro a h
78. entiate between possibly infinite lists that are immutable from mutable streams whose only access operation yields the head and turns the stream into its tail Data streams read from the network are a typical example of streams the previously read values are not automatically memoized and are lost if not saved when read Files on disk are also usually read via streams to avoid keeping all of them in main memory Another typi cal case where streams are used is that of diverging computations instead of generating at once an infinite sequence of outputs a function is turned into a stream and asking the next element of the stream runs one more iteration of the function to produce the next output often an approximation if a sequence computes the n th entry by recursively calling itself on every entry less than n accessing the n th entry requires re computation of all entries in position lt n which is very inefficient by representing an infinite object as a collection of approximations the struc ture of the object is lost This was not evident in the previous examples because in all cases the intrinsic structure of the datatype was just that of being ordered and sequences capture the order well Imagine however that we want to rep resent an infinite binary tree of elements of type A with the previous technique We need to associate to each position in the infinite tree an element of type A A position in the tree is itself a path from the r
79. er setoid poses no additional problem For example we can build a setoid out of vectors of length n assigning to it the type N gt setoid All the machinery for setoids just introduced keeps working On the other hand types that depend over a setoid require much more complex machinery and in practice it is not advised to try to work with them in an intentional type theory like the one of Matita To understand the issue imagine that we have defined a family of types I de pendent over integers I Z Type 0 Because 0 1 and 1 2 both represent the same integer 1 the two types I 0 1 and I 1 2 should have exactly the same inhabitants However being different types their inhabitants are disjoint The solu tion is to equip the type I with a transport function t Vn m Z n 2m gt In gt Im that maps an element of I n to the corresponding element of I m Starting from this idea the picture quickly becomes complex when one start considering all the additional equations that the transport functions should satisfy For example if p n mthent p t p 1 z 2 ie the element in I n corresponding to the element in I m that corresponds to zin I n should be exactly Moreover for any function f Vn I n gt T n for some other type T dependent on n the following equation should hold f t p a t p f 2 ie transporting and ap plying f should commute because f should be insensitive too up to to the actual representation o
80. es an argument In this case the argument is just a variable In case of a compound expression parentheses are needed around it Executing the previous command has the effect of opening two subgoals cor responding to the two cases b east and b west you may view one or the other by clicking on the tabs within the goal pane Both goals can be closed by trivial computations so we may use as usual If we had to treat each subgoal in a different way we should have focused on each of them in turn in a way that will be described at the end of this section qed this command closes both goals 1 6 Predicates Instead of working with functions it is sometimes convenient to work with pred icates For instance instead of defining a function computing the opposite bank we could declare a predicate opp stating when two banks are opposite to each other opp is a binary predicate on banks that is in curried form an object of type bank bank Prop Only two cases are possible leading naturally to the following inductive definition inductive opp bank bank Prop east_west opp east west west_east opp west east In precisely the same way as bank is the smallest type containing east and west opp is the smallest predicate containing the two sub cases east_west and weast_east If you have some familiarity with Prolog you may look at opp as the predicate defined by the two clauses in this ca
81. extends to the end of the declaration Parts of the pattern surrounded by denote verbatim content fragments those surrounded by denote meta operators and references to notational meta variables occurring in the presentation pattern for example a Journal of Formalized Reasoning Vol 7 No 2 2014 122 A Asperti and W Ricciotti and C Sacerdoti Coen The declaration also informs the system that the notation is supposed to be left associative and provides information about the syntactic precedence of the operator which governs the way an expression with different operators is interpreted by the system For instance suppose we declare logical disjunction at a lower precedence y notation huboz a break lor b left associative with precedence 30 for gt or a b y Then an expression like A A B VC will be understood as A A B VC and not as AN BVO An annoying aspect of user defined notation is that it will eventually interfere with the primitive one so introducing operators with suitable precedence is an important and delicate issue The best thing to do is to consult the file basics core_notation ma and unless you cannot reuse an already existing notation overloading it which is the recommended solution try to figure out the most suitable precedence for your notation by analogy with other notations Another possibility is to use the Terms grammar entry of the View menu of Matita to look at all notation
82. f of properness Journal of Formalized Reasoning Vol 7 No 2 2014 Matita Tutorial 171 2 at the moment automation in Matita is only available for Leibniz equalities By switching to setoids fewer proofs are automatically found 3 types dependent on plain types do not need ad hoc transport functions because the rewriting principle for Leibniz equality plays that role and already satisfies for free all required equations 4 normal forms are usually smaller than other forms By sticking to normal forms both the memory consumption and the computational cost of operations may be reduced Journal of Formalized Reasoning Vol 7 No 2 2014 172 A Asperti and W Ricciotti and C Sacerdoti Coen 8 INFINITE STRUCTURES AND COINDUCTIVE TYPES The only primitive data types of Matita are dependent products and universes So far every other user defined data type has been an inductive type An inductive type is declared by giving its list of constructors or introduction rules in the case of predicates An inhabitant of an inductive type is obtained by composing together a finite number of constructors and data of other types according to the type of the constructors Therefore all inhabitants of inductive types are essentially finite objects obviously up to the possible arguments of constructors Natural numbers lists trees states a DFA letters of an alphabet are all finite and can be defined inductively Sometimes however i
83. f the integral indexes Luckily enough types dependent on setoids are rare in practice Most examples of dependent types are indexed over discrete objects like natural integers and rationals that admit a unique representation By continuity types dependent on real numbers can also be represented as types dependent on a dense subset of the reals like the rational numbers 7 3 Avoiding setoids Quotients are used pervasively in mathematics In many practical situations for example when dealing with finite objects like pairs of naturals a unique represen tation can be imposed for example by introducing a normalization procedure to be called after every operation For example integer numbers can be normalized to either 0 7 or n 0 Or they can be represented as either 0 or a non zero number with the latter being encoded by a boolean the sign and a natural the predecessor of the absolute value For example 3 would be represented by NonZero false 2 3 by NonZero true 2 and 0 by Zero Rational numbers n m can be put in normal form by dividing both n and m by their greatest common divisor or by picking n 0 m 1 when nis 0 Imposing a unique representation is not always possible For example picking a canonical representative for a Cauchy sequence is not a computable operation Nevertheless when possible avoiding setoids is preferable 1 when Leibniz equality is used replacing n with m knowing n m does not require any proo
84. g one into the other in fact this is the essence of Leibniz equality we cannot do the same for an extensional equality we could only rewrite inside propositions compatible with our external observation of the objects 5 5 Sets with decidable equality We say that a property P 4 Prop over a datatype A is decidable when we have an effective way of assessing the validity of P a for any a 4 As a consequence of G del s incompleteness theorem not every predicate is decidable for instance extensional equality of sets is not decidable in general Decidability can be expressed in several possible ways A convenient one is to state it in terms of the computability of the characteristic function of the predicate P that is in terms of the existence of a function Pb A bool such that P a 4 Pb a true Decidability is an important issue and since equality is an essential predicate it is always interesting to try to understand when a given notion of equality is decidable or not In particular Leibniz equality on inductively generated datastructures is often decidable since we can simply write a decision algorithm by structural induction on the terms For instance we can define characteristic functions for booleans and natural numbers in the following way definition begb Ab1 b2 match b1 with true gt b2 false gt notb b2 let rec neqb n m match n with 0 match m with 0 gt true S q gt false
85. ge can be burned to a bootable DVD or it can be directly executed in a virtual machine using any virtual machine emulator like VMWare The image is a full Debian installation 3We shall give more details on Matita system of types and its logical restrictions in Section 9 Journal of Formalized Reasoning Vol 7 No 2 2014 98 i A Asperti and W Ricciotti and C Sacerdoti Coen with a copy of Matita already installed It is sufficient to open a terminal and type matita to start experimenting 0 6 Matita Web Still another alternative is to interact with Matita on line through our web interface 3 Matita is available as a multi user web application running remotely on our server The web application can process the same proof scripts as the stand alone system adding support for scripts containing HTML like markup Every Matitaweb user has a separate space for storing definitions and proofs The personal copies can then be synchronized with the centralized library for col laborative developments selected users currently testing only In order to get access to Matita Web follow the instructions at the following url http matita cs unibo it matitaweb shtml You will also find an on line executable version of this tutorial Journal of Formalized Reasoning Vol 7 No 2 2014 Matita Tutorial 3 99 1 DATA TYPES FUNCTIONS AND THEOREMS Matita is both a programming language and a theorem proving environment you can define datat
86. h leaf k gt None node m t1 t2 Some ti To typecheck the match Matita will ensure that the type of each branch corre sponds to the properly instantiated return type In particular in the first branch the type of leaf kis SBBT 0 thus Matita verifies that None has type Ano to option SBBT predno O leafk in the second branch the type of node m t1 t2is SBBT S m thus Matita verifies that Some t1 has type Ano to option SBBT predny Sm nodemt ta Since both checks succeed the type of the match will be the return type instantiated on the matched term Ano to option SBBT predng nt which reduces to option SBBT pred n that is the type declared for subtree_left The typing rule for dependent matching is one of the most complex rules of the type theory implemented in Matita A formal description of the rules can be found in 7 5 11 A heterogeneous notion of equality While the SBBT n type contains strictly balanced binary trees of a given height n we might be interested in stating properties of SBBTs regardless of their height In set theoretical terms this is achieved by stating the properties on the disjoint union indexed over n of the family of sets SBBT n In type theory this indexed disjoint union corresponds to the dependent pair type DPair of Section 4 2 the unified type of SBBTs USBBT DPair nat SBBT contains all the pairs k t gt where kis a natura
87. induction in a very simple way If the goal is of the form P n the invocation of Journal of Formalized Reasoning Vol 7 No 2 2014 110 A Asperti and W Ricciotti and C Sacerdoti Coen elim n will break it down to the two subgoals P 0 and Vm P m P S m Let us apply it to our case lemma add_0 Va add a 0 a ta elim a We generated the following goals goal type G add 0 0 0 Go Vz add xz O z Gadd S 1 0 Szw After normalization both goals are trivial normalize qed In a similar way it is convenient to state a lemma about the behaviour of add when the second argument is not zero the proof is a simple induction on a lemma add_S Va b add a S b S add a b a b elim a normalize qed We are now in the position to prove the commutativity of add We proceed by induction on the first argument and simplify the goals by invoking normalization theorem add_comm Va b add a b add b a ta elim a normalize We are left with two sub goals goal type G Vb b add b O Go Va Vb add x b add b z gt Vb S add z b add b S 2 G is just our lemma add_0 For G2 we could start introducing z and the induction hypothesis IH then the goal would be proved by rewriting using add_S and JH The resulting script would be tz IH gt add_S gt IH Instead this easy proof can be found automatically by Matita invoking the automation tactic
88. ing let us perform a simple ex periment Open Matita by invoking MATITA_HOME matita matita opt from a command line A window should appear on your screen with the shape in Fig ure 0 3 The interface 8 is divided into three subpanes one on the left and two stacked vertically on the right The pane in the top right contains at the moment the Matita logo when you are in the middle of a proof it will be used to visualize open goals in a sequent like fashion the pane beneath it is a read only area meant for error and log messages finally the pane on the left is an editor pane When you open a new file the latter pane contains a default comment with copyright information Let us observe by the way that Matita s style of comments follow the 21f autoconf is not installed in your system you will have to install it using the command apt get install autoconf first Journal of Formalized Reasoning Vol 7 No 2 2014 96 i A Asperti and W Ricciotti and C Sacerdoti Coen Applications Places system m 4 O al D FiFeb e 5 20 Pm MN SE E 00MH 3 elx a z Ele Edit Script view Debug Help p o J matita A project by Andrea Asperti Developers The HELM team http shelm cs unibo it This file is distributed under the terms of th v GNU General Public License Version 2 Matita version 0 99 1 5 ECEE un e e perso N e gt js andrea debian he
89. ing to the equivalence relation of an unknown setoid whose carrier is Nx N A hint can be used to always pick Zas intended setoid for N x N unification hint 0 N x N carrier X For instance thanks to the hint Matita accepts the following statement example exi 0 1 1 2 Every type is a setoid when elements are compared up to Leibniz equality definition LEIBNIZ Typel0 setoid AA mk_setoid A mk_equivalence_relation eq qed As before a hint can be used to enrich a type to a LEIBNIZ setoid unification hint 10 A Type 0 X LEIBNIZ A A carrier X Note that we declare the previous hint with a lower precedence level 10 vs 0 precedence levels are in decreasing order In this way an ad hoc setoid hint will be always preferred to the Leibniz one for example 0 1 1 2 is still interpreted in Z while 1 2 is interpreted as 1 2 As another example propositions up to equivalence form a setoid Journal of Formalized Reasoning Vol 7 No 2 2014 164 A Asperti and W Ricciotti and C Sacerdoti Coen 7 definition PROP setoid mk_setoid Prop mk_equivalence_relation Az y y whd iff_trans iff_sym 2 qed unification hint 0 Prop carrier X In set theory functions and relations over a quotient S R can be defined by lifting a function relation over S that res
90. ions of complex notations 3 4 Leibniz Equality Even equality is a derived notion in Matita and a particular case of an inductive type The idea is to define it as the smallest relation containing reflexivity that is Journal of Formalized Reasoning Vol 7 No 2 2014 124 A Asperti and W Ricciotti and C Sacerdoti Coen as the smallest reflexive relation on a given type inductive eq 4 Typel01 2 4 A gt Prop refl eq A z z We can associate the standard infix notation for equality via the following dec larations notation gt hubozx a break b non associative with precedence 45 for A eq a b interpretation leibnitz s equality eq t x y eq t z y The induction principle eg_ind automatically generated by the system has the following shape after removing type dependencies for clarity VA Type 0 Va A VP A Prop Px gt Vy A wy gt P y This principle is usually known as Leibniz equality two objects z and y are equal if they cannot be told apart that is for any property P P implies P y The order of the arguments in eg_ ind may look a bit random but as we shall see it is motivated by the underlying structure of the inductive type Before discussing the way eq_ind is generated it is time to have an important discussion about the parameters of inductive types If you look back at the definition of equality you will see that the first argument x has bee
91. irst branch of a binary match Notice that the names of costructors must be replaced by underscores in the pattern A second kind of pattern is used to specify all the subterms that match a user specified term u these are expressed by the syntax in match u For instance it is possible to match all additions in the conclusion by means of the pattern in match EXAMPLE 1 The two kinds of patterns can be combined in a single statement Suppose the current goal has a hypothesis H of type Vz nat 2x aty zxatzxy Then to match only the leftmost sum we can use the pattern This instructs Matita to match additions but only within the left hand side of the equality Journal of Formalized Reasoning Vol 7 No 2 2014 Matita Tutorial i 119 3 EVERYTHING IS AN INDUCTIVE TYPE As we have mentioned several times very few notions are really primitive in Matita one of them is the notion of universal quantification or dependent product type and the other one is the notion of inductive type Even the arrow type also called function space 4 gt B is not really primitive it can be seen as a particular case of the dependent product Vz 4 B in the degenerate case when B does not depends on x All the other familiar logical connectives conjunction disjunction negation existential quantification even equality can be defined as particular inductive types We shall look at those definitions in this section since it c
92. is fragment of the proof mk_state east west west east 2 Note that we had four goals we closed three of them hence we are left with a single goal reachable mk_state east east east east mk_state east west west east 1 12 Implicit arguments and partial instantiation Let us perform the next step namely moving back the boat in a slightly different way The more operation expects as its second argument the new intermediate state hence instead of applying more we can apply this term already instantiated on the next intermediate state that is more mk_state east west west west The question mark stands for an implicit argument to be inferred by the system The joint use of partial instantiation and implicit arguments is a very powerful tool for reducing the length of proofs Matita s inference system is based on a sophisticated bidirectional algorithm 7 exploiting both exptected and inferred types that is particularly convenient for the automatic management of implicit information By applying the previous term we get three independent subgoals i e not sharing any variable all active and two of them are trivial We can just apply automation to all of them in parallel and it will close the two trivial goals In this case we performed a move of the boat with the following code note in particular the we had no need to focus more mk_state east west west west 2 Let us come to the
93. ith nil gt true visited cons hd tl gt if begb snd fst hd snd snd hd cofinality then bisim S lm unique_append filter Az notb memb x hd visited sons S l hd tl hd visited else false visited Jy The integer n is an upper bound to the number of recursive calls equal to the dimension of the graph It returns a pair composed of a boolean and the set of visited nodes the boolean is true if and only if all visited nodes are cofinal The main test function is N definition equiv Sig Arel re2 re Sig let el e blank rel in let e2 e blank re2 in let n S length space_enum Sig lfst ell fst e21 in let sig occ Sig el e2 in bisim sig n e1 e21 O We proved both correctness and completeness so we have theorem equiv_sem VSig Vel e2 re Sig fst equiv el e2 true e1 e2 For correctness we use the invariant that at each call of bisimthe two lists visited and frontier only contain nodes reachable from e1 e2 hence it is absurd to suppose the existence of a pair that is not cofinal For completeness we use the invariant that all the nodes in visited are cofinal and the childrens of visited are either in visited or in the frontier since at the end frontier is empty visited is therefore a bisimulation All in all correctness and completeness take little more than a few hundred lines Journal of Formalized Reasoning
94. ition directly or indi rectly mentions or quantifies on the entity being defined are called impredicative The opposite notion to impredicativity is predicativity which essentially entails building stratified or ramified theories where quantification on lower levels results in objects of some new type Impredicativity can be dangerous a well known example is Russell s set of all sets resulting in famous logical paradox Consider in particular the set U of all sets not containing themself as an element Does such a set contain itself as an element If it does then by definition it should not and if it does not then by definition it should A predicative approach would consist of distinguishing e g between small sets and large sets where the set of all small sets would result in a large set In fact if we look at VP Type 0 P as a dependent product and we identify Type 0 as a universe of small sets it would seem strange to conclude that quantifying on all small sets we could obtain another small set In Matita VP Type 0 P has in fact type Type 1 and not Type 0 where Type 1 is also the type of Type o Journal of Formalized Reasoning Vol 7 No 2 2014 Matita Tutorial r 135 So while Prop is impredicative sorts of the kind Type i define a potentially infinite hierarchy of predicative sorts The difference between predicative and impredicative sorts is in the typing rule for the pro
95. ized Reasoning Vol 7 No 2 2014 116 A Asperti and W Ricciotti and C Sacerdoti Coen The lapply tactic can also be used to generalize hypotheses e g before perform ing an elimination If we have a goal G in a context where a 4 the execution of the command lapply z will transform the goal into Vx 4 G generalizing the variable in G If is also used in some hypothesis H P the goal is usually generalized on H using lapply H before doing the same on zx resulting in Vz 4 P gt G After generalizing on the command z is often used to erase the old and now useless assumption z A from the context 2 8 Mixing proofs and computations So far we have seen how to prove the existence of the integer half of a natural number how to compute it by an explicit program and how to specify and prove the correctnes of such a program There is still another possibility to mix the program and its specification into a single entity The idea is to refine the output type of the div2 function it should not just be a generic pair q r of natural numbers but a specific pair satisfying the specification of the function In other words we need the possibility to define for a type A and a property P on A the subset type a AlP a of all elements a of type A that satisfy the property P Subset types are just a particular case of dependent types that are types that can depend on arguments such as arrays of a specified length
96. l f 212 y2 definition mk_bin_morphism VI1 12 0 setoid Vf I1 gt 12 gt 0 proper2 f gt 1I1 gt I2 gt 0 AI1 12 0 f proper mk_morphism Az mk_morphism Ay f y normalize 2 qed We can also coerce a binary morphism to a binary function and prove that proper2 holds for every binary morphism definition binary_function_of_binary_morphism VI1 12 0 setoid 11 gt I2 4 0 gt I1 gt 12 gt 0 AI1 12 0 f t y f y coercion binary_function_of_binary_morphism VI1 I2 0 setoid Vf I1 gt I2 gt 0 11 gt 12 gt 0 binary_function_of_binary_morphism on _f gt gt to gt gt theorem mor_proper2 VI1 12 0 setoid Vf I1 gt I2 gt O proper2 f I2 12 0 f 01 12 y1 y2 EQx EQy O mor_proper f EQu EQy qed Continuing our example on integer numbers let us define addition As usual we first define it as a function and then lift it to a morphism we overload over integers definition Zplus Z gt Z gt Z da y fst c fst y snd z snd y interpretation Zplus plus x y Zplus z y definition ZPLUS Z gt Z Z mk_bin_morphism Zplus normalize ala txib qed Journal of Formalized Reasoning Vol 7 No 2 2014 Matita Tutorial 167 The following hint allow the system to automatically retrieve the morphism ZPLUS associated with Zplus as needed 3 unification hint
97. l number and t has type SBBT k USBBT enables us to consider properties involving balanced trees of unknown height This means of course that we can immediately express equalities or in equalities about any pair of USBBTs Consider for instance the following context Journal of Formalized Reasoning Vol 7 No 2 2014 148 A Asperti and W Ricciotti and C Sacerdoti Coen m n nat a b SBBT m c d SBBT n z SBBT S m y SBBT S n Let us define two terms of type USBBT t KS S m node S m node m a b gt t2 KS S n node S n y node n c d gt or graphically e e a o y e a b c d t t2 Since t and t2 have the same type USBTT an equation involving them is well typed even though m and n a priori could be different Actually since t and ta are dependent pairs and DPair is an inductive type we expect to be able to derive from t t2 that the two pairs are component wise equal e S S m S S n ez node S m node m a b node S n y node n c d Even though by e we know that mand n are equal ez is still ill typed for ez to typecheck the knowledge that its two sides have the same type must be formalized for instance by rewriting the left hand side by means of e1 using the eg_ ind principle of Section 3 4 ez eq_ind node S m node m a b x e1 node S n y node n c d eq_ind changes the type of the left hand side from SBBT S S m to SBBT S S n and makes it
98. l other cases you could conceptually get rid of them by adding inside the type of constructors the suitable equalities that would allow to turn arguments into parameters Consider for instance our opp relation of Section 1 6 inductive opp bank bank Prop east_west opp east west west_east opp west east The predicate has two arguments and since they are mixed up in the type of constructors we cannot express them as parameters However we could state it in the following alternative way inductive opp1 b1 b2 bank Prop east_west b1 east b2 west opp1 b1 b2 west_east b1 west gt b2 east gt opp1 b1 b2 Or also more elegantly inductive opp2 b1 b2 bank Prop opposite_to_opp2 b1 opposite b2 gt opp2 b1 b2 Now suppose we know H opp z west where z is a variable of type bank From this hypothesis we should be able to conclude z east but this is slightly less trivial than one could expect One would be naturally tempted to proceed by case analysis on H but this would lead him nowhere in fact it would generate the following two Journal of Formalized Reasoning Vol 7 No 2 2014 Matita Tutorial 127 subgoals G1 east east Go west east where the second one cannot be proved Also induction on z does not help since we would get the goals G opp east west east east Go opp west west west east The first goal is trivial bu
99. le is just to illustrate the use of We prove the same statement of ex4 but this time we perform one rewriting at a time Note that in an intermediate goal Matita replaces occurrences of Zplus with occurrences of the carrier of ZPLUS To recover the notation it is sufficient to expand the declaration of ZPLUS Da example exb Val z2 y 2 Z tl 12 gt y 22 21 z y y 21 22 z y ol 02 ty tz EQ O iEQ 1 1t whd in match ZPLUS EQt qed Our last example involves rewriting under a predicate different from We first introduce such a predicate over integers definition s_zero Z Prop Ac fst c snd c definition IS_ZERO Z PROP mk_morphism s_zero normalize 3 by conj injective_plus_r qed unification hint 0 Z X IS_ZERO k parr rrr nnn E is_zero mor_carr X T u We can rewrite under any predicate using example ex6 Vz y Z x y gt 1 8s_zero x y gt 3s_zero a 2 tx ty EQ H O GHEQ OH qed Journal of Formalized Reasoning Vol 7 No 2 2014 170 y A Asperti and W Ricciotti and C Sacerdoti Coen 7 2 Dependent setoids A setoid is essentially a type equipped with its own notion of equality In a frame work with dependent types one expects to be able to build setoids dependent on other types and setoids Working with families of setoids that depend on a plain type i e not anoth
100. lized Cartesian product of a family of types B indexed over a base type A 4 3 Kolmogorov interpretation The previous analogy between propositions and types is a consequence of a deep philosophical interpretation of the notion of proof in terms of a constructive proce dure that transforms proofs of the premises into a proof of the conclusion This is usually referred to as Kolmogorov interpretation or Brouwer Heyting Kolmogorov BHK interpretation The interpretation states what is intended to be a proof of a given proposition and is specified by induction on its structure a proof of PAQ is a pair a b where ais a proof of P and b is a proof of Q a proof of PV Qis a pair a b where either a is 0 and bis a proof of P or a is 1 and bis a proof of Q a proof of P gt Q is a function f which transforms a proof of Pinto a proof of Q a proof of dz S P zis a pair a b where a is an element of S and b is a proof of P a a proof of Va S P zis a function f which transforms an element a of S into a proof of P a the proposition P is defined as P gt False so a proof of it is a function f which transforms a proof of P into a proof of False there is no proof of False For instance a proof of the proposition P gt Pis a function transforming a proof of Pinto a proof of P the identity function will do You can explicitly exploit this idea for writing proofs in Matita Instead of declaring a lemma and pro
101. lus Since the A calculus admits non terminating terms making the definition of D legal has surreptitiously added non terminating computations into CIC as well Let for example 7 definition omega D app dup dup Then omega app dup dup Az D app x x dup app dup dup omega hence omega would reduce to itself resulting in a non terminating computation So what is so dangerous with non termination Consider for instance the fol lowing definitions Journal of Formalized Reasoning Vol 7 No 2 2014 Matita Tutorial 191 definition F D lam Az lam Ay z Az y z definition Far D lam Az app F app x 2 Az F 2 a definition YF D app Fax Faz Fix Fox Y F We used basic results about existence of fixed points in the A calculus to build a non terminating term YF that upon reduction produces infinite copies of the lam constructor Then we can define a function size whose purpose is to count the number of constructors used in a term of type D definition I D lam Az z let rec size d match d with lam f S size f I where the identity term I is a dummy used to obtain from f a new term for a recursive call to size Then if we try to compute the size of YF we discover that it is equal to S Ay app Fax Fer I S size YF but this is simply absurd since no natural number can be equal to its successor The point is that nat was supposed to range
102. ly created and saved in SCRIPTS_HOME 0 4 Browsing the library For the moment it is not very important to know what has been loaded by the system including the file logic ma however if you are curious to have a look at its content the best choice is to directly open it To this purpose click File gt Open in the menu bar this will open a new pop up window allowing you to browse the Journal of Formalized Reasoning Vol 7 No 2 2014 Matita Tutorial 97 file system Choose the desired file e g logic ma and confirm your choice by pressing the OK button the file will open up in the editing window Sometimes you are not interested in reading an entire file but just to check a specific result For instance after having included logic ma as described in the previous section type the following line without a fullstop and execute it as usual by hitting Ctrl Alt Page Down check True a new window called Matita Browser should pop up with type information about the constant True In particular this window should tell you that True Prop The language of Matita is strongly typed every term of the language has a type including types themselves The syntax m T is the standard notation adopted in type theory to express the fact that the term M has type T So the previous statement informs us that True is a term of type Prop Prop that is a shorthand for Proposition is a primitive constant of the sy
103. ly interesting T AF B TFA gt B TFA TFA gt B TFB The first step is to enrich the representation by decorating propositions with explicit proof terms In particular propositions in the context being assumptions will be decorated with pairwise distinct free variables while the conclusion will be decorated with a term whose free variables appear in the context Suppose P x A M B what is the expected decoration for A gt B Ac cording to the Kolmogorov interpretation M is a procedure transforming the proof x A into a proof of B the proof of A gt B is hence the function that taken x as input returns M and our canonical notation for expressing such a function is Ax A M Hence we get T 2 AFM B TFA AM A gt B that is precisely the typing rule for functions Similarly let us suppose that TF M 4 gt BandT F N A and let us derive a natural proof decoration for the arrow elimination rule that is just the well known modus ponens rule Again we get inspiration from Kolmogorov interpretation a proof M A gt B is a function transforming a proof of A into a proof of B hence since we have a proof N A in order to get a proof of B it is enough to apply M to the argument N TEM ASB TEN A TE MN B But this is nothing else than the typing rule for application There is still a point that deserves discussion the most interesting point of pro grams is that they can be executed in a functional setting terms can be reduc
104. m with an additional boolean that must be understood as the possibility of having a trailing point at the end of the expression As we shall see pointed regular expressions can be understood as states of a DFA and the boolean indicates if the state is final or not r N definition pre S pitem S xbool The carrier il of an item is the regular expression obtained from i by removing all the points Similarly the carrier of a pointed regular expression is the carrier of its item The formal definition of this functions are straightforward so we omit them The intuitive semantics of a point is as a mark on the position where we should start reading the regular expression The language associated to a PRE is the union of the languages associated with its points Here is the straightforward definition the question mark is an implicit parameter let rec semi S DegSet i pitem S on i word S gt Prop match r with pz gt pe O lps _ gt pp gt x pe 11 12 gt semi 11 l22I Ulsemi i2 po 11 r2 semi 11 U semi 12 pk 11 gt semi 11 1311 1 definition semp AS DeqSet Ap pre S if snd p then semi fst p Ufe else semi fst p In the sequel we shall often use the same notation for functions defined over re items or PRES leaving to the reader the simple disambiguation task Matita is also able to solve automatically this kind of notati
105. n i let corec div_well_formed_to_div_well_formed_co s streamseg state div_well_formed s div_well_formed_co s match s with sscons hd1 tli gt match tli with sscons hd2 tl gt AH div_well_formed sscons hd1 sscons hd2 tl is_nezt div_well_ formed_to_div_well_formed_co sscons hd2 tl First proof obligation next hdl hd2 CH 0 Second proof obligation div_well_formed sscons hd2 tl An H S n qed A div_well_formed_co stream is also div_well_formed This time the proof is by induction on the index and inversion on the div_well_formed_co hypothesis se theorem div_well_formed_co_to_div_well_formed Vs streamseq state div_well_formed_co s gt div_well_formed s ts H n lapply H H lapply s s elim n 2 m 14 hdl hd2 tl normalize H inversion H hdl hd2 tl Hnext Huf eq destruct 2 qed Like for sequences because of undecidability of termination there is no function that given an initial state returns the diverging trace if the program diverges or fails in case of error We need a new data type to represent a possibly finite stream of elements Such a data type is usually called stream and can be defined elegantly as a coinductive type coinductive stream A Type 0 Type 0 snil stream A scons A stream A gt stream A The following lemma will be used to unblock blocked redu
106. n principle One reason is that the type of the generated principles is less informa tive than that for elimination principles The problem is that in the type theory of Matita it is not possible to generalize the above type to a dependent version to obtain the exact dual of the elimination principle In case of the elimination principle the type P depends on the value of the input and the principle proves the dependent product V1 list A P A In the case of the introduction principle the output is P gt list A To obtain a dependent version we would need a dual of the dependent product such that the type of the input is dependent on the value of the output a notion that is not even meaningful when the function is not injective Journal of Formalized Reasoning Vol 7 No 2 2014 190 A Asperti and W Ricciotti and C Sacerdoti Coen 9 LOGICAL RESTRICTIONS In this section we shall discuss some of the logical restrictions of the logical system required for preserving consistency At the same time we shall provide a more detailed and precise exposition of the Calculus of Inductive Constructions In order to fully understand all nuances of the type system the reader is invited to read the description of the Matita kernel in 5 9 1 Positivity in inductive definitions Not every inductive definition is accepted by Matita The following is a typical example inductive D Typel0 lam D gt D gt D which is rejected
107. n a different way for each of them The operation of selecting a goal among the active ones is called focusing and is described in the next section When applying a tactic check that there is at least one active goal otherwise the command will be silently discharged 1 11 Focusing The general idea is that when you have multiple subgoals you should structure your proof accordingly using a syntax like pil pol pn where you have a subproofs pi for every active subgoal The inner proofs can branch again when multiple goals become active resulting in a tree like proof structure In all other provers pi p21 lpn is a new tactic built from the tactical 1 A tactical builds a tactic from arguments that are tactics or proofs themselves Tactics built with tacticals are executed as a monolitic step it is not possible to stop in the middle of execution to observe the intermediate proof states Matita decomposes the tactical into three commands 1 called tinycals 20 that can be executed individually More precisely and the tinycal opens a new focusing section for the currently active goals and focus on the first of them 66 the tinycal shifts the focus to the next goal in the current section the tinycal closes the focusing section falling back to the previous level and adding to it all the remaining not yet closed goals Matita also provides o
108. n explicitly declared together with 4 as a formal parameter of the inductive type while the second argument has been left implicit in the resulting type 4 gt Prop One could wonder if this really matters and in particular if we could use the following alternative definitions x inductive eq1 A Type 0 a2 y 4 Prop refli eqi Az z inductive eq2 4 Typel01 A A gt Prop refl2 Vr eq2 Aa a The first definition is wrong If you try to write it in Matita you would get the following error message CicUnification failure Can t unify x with y The issue is that the role of parameters is really to define a family of types uniformly indexed over them This means that we expect all occurrences of the inductive type in the type of constructors to be precisely instantiated with the input parameters in the order they are declared If 4 zand y are parameters for eq1 then all occurrences of this type in the type of constructors must be of the kind eq1 A y while we have eq1 A x x that explains the typing error If you cannot express an argument as a parameter the only alternative is to implicitly declare it in the type of the inductive type Henceforth when we talk 6 The definition can only be used to equate inhabitants of small types of type Type 0 Matita does not provide a way to define a property that works uniformly at every universe Therefore in the rare cases when equality is needed at higher u
109. nder the pair of assumptions A and B It is interesting to observe that the elimination rule can be easily derived from the introduction rule in a completely syntactic way Basically the general structure of the non dependent elimination rule for an inductive type T is the following VA P 1 gt gt C 2 gt T gt P where A is the list of parameters of the inductive type and every C is derived from the type T of a constructor c of T by just replacing T with P in it For instance in the case of the conjunction we only have one constructor of type A B gt AABand replacing AA B with P we get C A gt B gt P Journal of Formalized Reasoning Vol 7 No 2 2014 120 a A Asperti and W Ricciotti and C Sacerdoti Coen Every time we declare a new inductive proposition or type T Matita automati cally declares an axiom called T_ind which embodies the elimination principle for this type The actual shape of the elimination axiom is more complex than the one described above since it also takes into account the possibility that the predicate P depends on the term of the given inductive type and possible arguments of the inductive type Actually the elimination tactic elim for an element of type Tis a straightforward wrapper that applies the suitable elimination axiom 3 2 Disjunction False True Existential Quantification Let us introduce now other connectives as inductive types mimicking what we did for conjunction and s
110. ng all its elements The type itself is called bank Let s have a look at the definition then we shall discuss its syntax inductive bank Type 0 east bank west bank The definition starts with the keyword inductive followed by the name we want to give to the new datatype in this case bank followed by its type a type of a type is traditionally called a sort in type theory A sort in Matita is either Prop or a Type i As we already said in the introduction Prop is meant for propositions Type 0 for datatypes and Type i for large collections The definition proceeds with the keyword or def followed by the body of the definition The body is just a list of constructors for the inductive type separated by the symbol vertical bar Each constructor is a pair composed by a name and its type Constructors in our case east and west are the canonical inhabitants of the inductive type we are defining in our case bank hence their type must be of type bank In general as we shall see constructors for an inductive type T may have a more complex structure and in particular can be recursive the general proviso is that they must always return a result of type T Hence the Journal of Formalized Reasoning Vol 7 No 2 2014 100 A Asperti and W Ricciotti and C Sacerdoti Coen declaration of a constructor c for and inductive type T has the following typical shape c Ay gt gt An gt T
111. ng or look into its database of results for a possible solution In this situation we may suggest the intended solution in Matita which uses the mechanism of unification hints 6 19 The concrete syntax of unification hints is a bit involved we strongly recommend that the user include the file hints_declaration ma allowing us to write hints in a more convenient and readable way Journal of Formalized Reasoning Vol 7 No 2 2014 144 A Asperti and W Ricciotti and C Sacerdoti Coen include hints_declaration ma The following declaration uses the aforementioned mechanism to hint that a solution of the equation bool carr Xis X DeqBool unification hint 0 Xx 2 DeqBool bool carr X Using the previous notation we suggest the reader to cut and paste it from previ ous hints the hint is expressed as an inference rule The conclusion of the rule is the unification problem that we intend to solve containing one or more variables Xi X The premises of the rule are the solutions we are suggesting Matita In general unification hints should only be used when there exists just one intended canonical solution for the given equation When you declare a unification hint Matita verifies its correctness by instantiating the unification problem with the hinted solution and checking the convertibility between the two sides of the equa tion A example exhint Vb bool b false
112. niverse Constraints Another constraint on inductive definitions requires that the sorts of constructors and the sort of the inductive type must be equal Considering that each constructor for an inductive type T must have a type of the form Ay gt gt An gt T there are two possibilities either T Prop and then any argument is accepted but as we shall see with restrictions on the elimination rules or 7 Type 31 In this case for every i such that 4 Type k we expect to have ki lt j Consider for instance the case of DeqSets E record DegSet Type i Journal of Formalized Reasoning Vol 7 No 2 2014 Matita Tutorial e 193 carr gt Type 0 eqb carr carr bool eqb_true Vz y eqb x y true a y As we know this is syntactic sugar for an inductive type with a single constructor taking as arguments the values of the record fields So among the arguments we have the carrier and since we are quantifying over generic elements in Type 0 we shall end up with a larger type the smallest being Type 1 In order to understand the reasons for this restriction we shall prove that its omission essentially opens the way to an encoding of Russell s paradox as first observed in 23 Let us consider the following type P inductive U Type 1 c VA TypeL0l 4 gt Prop gt U You may look at cas a sort of comprehension axiom that for every property builds the corresponding
113. niverses the user needs to duplicate its definition or to re declare it to work on say Type 1 Every type that inhabits a Type 7 is also recognized to be of type Type j for every j gt i Journal of Formalized Reasoning Vol 7 No 2 2014 Matita Tutorial 125 about arguments of inductive types we shall implicitly refer to arguments which are not parameters Sometimes people call them right and left parameters according to their position w r t the colon in the type declaration In general it is always possible to declare everything as an argument but it is a very good practice to shift as many argument as possible in parameter position As we shall see the induction principle generated for eg2 is harder to understand than eq_ind The elimination rule for an inductive type T having a list of parameters Aanda list of arguments B has the following shape still up to dependencies Va A P B Prop C1 gt gt Cn oVEB TG OPE where C is obtained from the type T of the constructor c replacing in it each occurrence of T t with P t For instance eq2 only has A as parameter and two arguments The correspond ing elimination principle eq2_ind is then as follows VA Type 0 VP 4 gt A Prop Vz Pzz Va y A wy gt P z y It is possible to prove that eq2_ind and eg_ind are logically equivalent that is they mutually imply each other but eg2_ nd is slighty more complex and unnatural 3 5 Equalit
114. nograph 12 Alternatively you may consult the conspicuous book by Sorensen and Urzyczyn on the Curry Howard analogy 21 Concrete models of the Calculus of Inductive Construction have been mostly investigated by Miquel et al 17 For a categorical investigation and the relation between type theory and categorical logic see Jacobs s book 15 Recently a very interesting relation between Type Theory and Omotopy The ory has been discovered giving birth to Homotopy Type Theory HoTT People interested in this topic can start from 22 References 1 Andrea Asperti A compact proof of decidability for regular expression equiv alence In Interactive Theorem Proving Third International Conference ITP 2012 Princeton NJ USA August 13 15 2012 Proceedings volume 7406 of Lecture Notes in Computer Science pages 283 298 Springer 2012 2 Andrea Asperti and Giuseppe Longo Categories Types and Structures M I T Press 1991 3 Andrea Asperti and Wilmer Ricciotti A Web Interface for Matita In Proceed ings of Intelligent Computer Mathematics CICM 2012 Bremen Germany volume 7362 of Lecture Notes in Artificial Intelligence Springer 2012 4 Andrea Asperti Wilmer Ricciotti Claudio Sacerdoti Coen and Enrico Tassi The Matita Interactive Theorem Prover In Proceedings of the 23rd Interna tional Conference on Automated Deduction CADE 2011 Wroclaw Poland volume 6803 of LNCS 2011 5 Andrea Asperti Wilmer Ricciotti
115. o b since it is a bank we just type 0 40 introduce b into the context After executing this command the goal pane will look like the following b bank opposite opposite b b The variable b has been added to the context replacing z in the conclusion more over its implicit type bank has been made explicit The foundational language of Matita is strongly typed hence every time you declare a variable with some binding mechanism you are supposed to provide its type Luckily in many cases this type can be automatically inferred by the system according to the usage of variable sparing the user the burden to write it 1 5 Case analysis But how are we supposed to proceed now Simplification cannot help us since b is a variable just try to call normalize and you will see that it has no effect The point is that we must proceed by case analysis according to the possible values of b namely east and west To this aim you must invoke the cases command followed by the name of the hypothesis more generally an arbitrary expression that must be the object of the case analysis in our case b Note that we do not need to specify the possible cases the system is able to compute them from the type of the expression that must be an inductive type cases b cases analysis on b Journal of Formalized Reasoning Vol 7 No 2 2014 Matita Tutorial i 103 This is the first example of a tactic that tak
116. oa wk A 110 A o oo oes Ba eee Ge Se a e aa 111 Journal of Formalized Reasoning Vol 7 No 2 2014 Pages 91 199 A Asperti and W Ricciotti and C Sacerdoti Coen 24 Computing vs Proving coo occocsosn soso o AR oh Ge AP A ae Re a a 2 ROME og eA MASA a Oe ee EEE ea ee ea ee LA CAm e ee ces he bok ee EEE RE EA ERS 2 8 Mixing proofs and computations se e ea a aaeeea cd wi Tacte pane IA Everything is an inductive type ol at IA 3 2 Disjunction False True Existential Quantification 33 A PILOTO ON oc ew ee ws eB a a Ed eee PR 34 Leibniz Equality co eR ew eee we aes 3 5 Equality convertibility inequality Om a 2 va Ge ee hea ee eee ORES See a eS Propositions as Types 4 1 Cartesian Product and Disjoint Sum 4 2 Sigma Types and dependent matching 4 3 Kolmogorov interpretation e s ssaa cso esete 004 4 4 The Curry Howard correspondence Ab Prop ve Type c s ea ioa a Fe eb bb td a eae More Data Types Go Opiom Type Goes a oe eee ee PEE RAR EE eae D Bie LOSS fo ho be hE OE SOA ee RR EEE EES SEE RLS ooo Last HAGEN RRA ee 5 4 Naive Set Theory c oooooo on e 5 5 Sets with decidable equality ocos ca e amam a o o ab Umitication Bots 640 ao canas aa A A Ge Saf Prop ve bool 4 coco cc e a Be Fto Sete ecw we ek we ERR el EE E E OS Pe o ad ae s e ee alk he es SA we ee EDA a ORES 5 10 Dependent matching 0 0 2
117. of a e and we must pursue broadcasting inside b a b b Again we work in parallel on the two additive subterms b a and b the first point is allowed to both enter the star and to traverse it stopping in front of a the second point just stops in front of b No point reached the end of b atb hence no further propagation is possible In conclusion e ate b a b b eate eb eateb b false Note that broadcasting a point inside an item generates a PRE since the point could possibly reach the end of the expression Broadcasting inside a pair 42 amounts to broadcasting in parallel inside 1 and iz If we define a1 01 42 02 i1 i2 b1V b2 then we just have e iit i2 e 41 e 12 Concatenation is a bit more complex In order to broadcast an item inside 1 Ai t2 we should start broadcasting it inside 1 and then proceed into ia if and only if a point reached the end of i This suggests to define e 41 42 as e 41 gt 2 where eb is a general operation of concatenation between a PRE and item named pre_concat_1 defined by cases on the boolean in e i1 true Pi2 lt e 4_2 i1 false Pti2g 41 42 false In turn lt named pre_concat_r says how to concatenate an item with a PRE which is extremely simple 41 lt 41 D 41 42 d The different kinds of concatenation between items and PREs are summarized in Fig 3 where we also depict the concatenation between two PREs of Section 6 8
118. of the first and the stream without the first element is recursively well formed E coinductive div_well_formed_co streamseq state gt Prop is_nezt Vhd1 state Vhd2 state Vtl streamseq state next hdi hd2 div_well_formed_co sscons hd2 tl gt div_well_formed_co sscons hd1 sscons hd2 tl Note that Matita automatically proves the inversion principles for every coinduc tive type but no general coinduction principle That means that the elim tactic does not work when applied to a coinductive type The tactics inversion and cases are the only ways to work with coinductive hypothesis A proof of div_well_formed cannot be built stacking a finite number of construc tors The type can only be inhabited by a coinductive definition As an example we show the equivalence between the two definitions of well formedness for streamseqs A div_well_formed stream is also div_well_formed_co We write the proof term explicitly omitting the subterms that prove div_well_formed sscond hd2 tl and next hdi hd2 Therefore we will obtain two proof obligations The given proof term is productive if we apply it to a closed term of type streamseq state and a proof that it is well formed the two matches in head position will reduce and the lambda abstraction will be consumed exposing the is_nezt constructor Journal of Formalized Reasoning Vol 7 No 2 2014 182 i A Asperti and W Ricciotti and C Sacerdoti Coe
119. on 3 2 we will explain that the disjuction connective is defined as an inductive type generated by two constructors called or_introl and or_intror Therefore to proceed in the proof we can apply the term or_introl However remembering the names of constructors can be annoying we can invoke the application of the n th constructor of an inductive type inferred from the current goal by typing n At this point we are left with the subgoal O add O O that is closed by computation It is worth to observe that invoking automation at depth 3 would also automatically close Here is the fragment of the proof up to this point n elim n normalize ex_intro 0 1 2 3 Decomposition The case of Ga is more complex We should start introducing z and the induction hypothesis TH dm c add mmVz S add m m The induction hypothesis IH asserts the existence of an m that satisfies the thesis to obtain such an m we eliminate the existential at the front of the hypothesis using the case tactic This is motivated by the fact that the existential is just a particular inductive type This situation where we introduce something into the context and immediately eliminate it by case analysis is so frequent that Matita provides a convenient shorthand you can just type a single x The star symbol should be reminiscent of an explosion the idea is that you have a structured hypothesis and you ask to explode it into its constituents
120. onal overloading We shall denote with e all semantic functions sem semi and semp EXAMPLE 2 1 If e contains no point then e 0 2 Catebdb bbCa bb T Here are a few simple semantic properties of items Journal of Formalized Reasoning Vol 7 No 2 2014 Matita Tutorial e 153 r y lemma not_epsilon_item VS DeqSet Vi pitem S 1 lemma epsilon_pre VS Vi pre S Ci Y snd i true lemma minus_eps_item VS Vi pitem S lil fe lemma minus_eps_pre VS Vi pre S fst i il e The first property is proved by a simple induction on i the other results are easy corollaries 6 4 Intensional equality of PREs Items and PREs area very concrete datatype they can be effectively compared and enumerated This is important since PREs are the states of our finite automata and we shall need to compare states for bisimulation in Section 6 10 We can define beqitemand beqitem_true enriching the set pitem S to a DeqSet definition Degltem AS mk_DeqSet pitem S begitem S beqitem_true S Matita s mechanism of unification hints 6 see Section 5 6 allows the type in ference system to look at pitem S as the carrier of DegSet and at begitem as if it were the equality function of DegSet The product of two DeqSets is clearly still a DeqSet Via unification hints we may enrich a product type to the corresponding DeqSet since moreover the type of
121. oning Vol 7 No 2 2014 128 A Asperti and W Ricciotti and C Sacerdoti Coen 4 PROPOSITIONS AS TYPES In the previous section we introduced several logical connectives by means of in ductive definitions in the sort Prop Do the same constructions make any sense in Type 1 The answer is yes Not only do they make sense but they are the familiar type constructors Cartesian product disjoint sum empty and singleton types and sigma types disjoint unions of families of types indexed over a given base type This is not a coincidence but an instance of a principle known under the name of Propositions as Types analogy or Curry Howard correspondence We shall first discuss the constructions and then we shall come back on the general correspondence 4 1 Cartesian Product and Disjoint Sum The Cartesian product of two types 4 and Bis defined in the following way inductive Prod 4 B Typel01 Type 0 pair A gt B gt Prod A B Observe that the definition is identical to the definition of logical conjunction but for the fact that the sort Prop has been replaced by Type o The following declarations allow us to use the canonical notations AxB for the product and a b for the pair of the two elements a and b notation hubozl z break xy with precedence 70 for A product x y interpretation Cartesian product product A B Prod A B notation hubozr term 19 a break term 19 b with preced
122. oot to the node of interest Therefore the infinite tree is represented as the function NB A where B are the booleans and the tree structure is already less clear Suppose now that the binary tree may not be full i e some nodes can have fewer than two children Representing such a tree is definitely harder We may for example use the data type NB option A where None would be associated to the position b b if a node in such position does not exist However we would Journal of Formalized Reasoning Vol 7 No 2 2014 Matita Tutorial 177 need to add the invariant that if b bn is undefined i e assigned to None so are all suffixes b bn dny1 bn j The previous observations suggest the need for primitive infinite datatypes in the language usually called coinductive types or codata Matita allows us to declare coinductive types with the same syntax used for inductive types just replacing the keyword inductive with coinductive Semantically the two declarations differ because a coinductive type also contains infinite inhabitants or more precisely finite cyclic generators for them that respect the typechecking rules As a simple example instead of using functions an infinite sequence of elements of type 4 can be defined by the following coinductive definition coinductive streamseg A Type 0 Typel0l sscons A gt streamseq A gt streamseg A No
123. over natural numbers while introducing the possibility of divergence we are surreptitiously extending the domain adding a new bottom element In order to ensure consistency the inductive definition must respect some posi tivity conditions concerning the occurrences of the inductive type in the types of the arguments of constructors The polarity of an occurrence of a propositions A inside a propositions Bis defined in the following way If A B then 4 occurs positively in B if B C gt Dor B Ye C D then if A occurs positively negatively in D then it occurs positively in B conversely if it occurs positively negatively in C then it occurs negatively positively in B For instance D occurs two times in D gt D the type of the only argument of embed the first occurrence is negative while the second is positive As a first approximation the strict positivity requirement for inductive definitions imposes that for any constructor c Ay gt gt An gt X the inductive type X can only occur positively in any of the 4 To understand the reasons for this restriction we need to make a short digression on recursive domain equations When we define a recursive inductive type we are essentially defining a type as a solution of a suitable equation Consider for instance the type of natural numbers The type of the two constructors can be seen as two injections 0 unit gt nat and S nat nat since we have no addition
124. pects R Respecting R means that the relation holds for an element x of S iff it holds for every y of S such that Ry Similarly a function f respects Riff f x f y for every x y such that Ry We say that a function between two setoids is proper when it respects their equalities definition proper VI 0 setoid I gt 0 gt Prop AI 0 f Va y TI s xy gt frfy A proper function is called a morphism record morphism 1 0 setoid Typelol 1 mor_carr 1 gt I gt 0 mor_proper proper mor_carr We introduce a notation for morphisms using the symbol of an arrow followed by a dot notation hubox I break 0 right associative with precedence 20 for OL morphism I 0 y interpretation morphism morphism I O morphism I 0 By declaring mor_carr as a coercion using 1 gt it is possible to write f for mor_carr f x in order to apply a morphism f to an argument The 1 in 1 gt is the number of arguments required to trigger the coercion As a simple example let us define the negation opp of an integer number We first implement the function over Z and then lift it to a morphism The proof obligation is to prove properness definition opp Z gt Z Xc snd c fst c definition OPP Z Z mk_morphism opp normalize qed Journal of Formalized Reasoning Vol 7 No 2 2014 Matita Tutorial i 165 When writing expressions over Z we will always
125. possible to equate it to the right hand side Working with explicit rewritings is cumbersome and becomes essentially infeasible as the number of rewriting steps grows To directly express the equality of terms whose actual types differ but may be made equal by means of rewriting we have to abandon Leibniz equality and switch to a heterogeneous equality In Matita heterogeneous equality is defined as an inductive type which likely its Leibniz counterpart is only inhabited by reflexivity the difference between the two is that heterogeneous equality has an additional argument allowing the type of the right hand side to be different from that of the left hand side For a concrete proof of equality built by reflexivity the two types and the two terms have to be Journal of Formalized Reasoning Vol 7 No 2 2014 Matita Tutorial 149 the same but unlike with Leibniz equality merely stating an equality involving two different types is still well typed This is the definition of heterogeneous equality taken from the library file basics jmeg ma inductive JMeg 4 Typel01 x2 4 VB Typel01 B Prop refl_jmeq JMeq A z A z For a heterogeneous equality JMeg A a B b equating a 4 and b B we use the nota tion a b Like every inductive type heterogeneous equality provides an induction principle its shape looks quite similar to that of its Leibniz counterpart JMeq_ind WA Type 0 Va A VP VT Type 0 T Prop PA aw gt
126. property that the opposite bank of east is west every lemma needs a name for further reference so we will call this one east_to_west lemma east_to_west opposite east west If you enter the previous declaration and execute it you will see a new pane re placing the matita logo on the right side of the screen it is the goal pane providing a sequent like representation of the following form for each open goal in the proof B By Br A A is the conclusion of the goal and Bj By are the hypotheses in the context In our case we only have one goal and the context is initially empty opposite east west We proceed in the proof by issuing commands traditionally called tactics to the system In this case we want to evaluate the function which can be done by invoking the normalize command remember that strings within the delimiters x and x are just comments normalize this command reduces the goal to the normal form By executing it you will see that the goal will change to west west in particular the subexpression opposite east has been reduced to west You may use the retract button to undo the step if you wish The new goal west west is trivial it is just a consequence of reflexivity Such trivial steps can be closed in Matita by just typing a double slash We complete the proof by the ged command that instructs the system to store the lemma performing some book k
127. q_eq qed We can finally turn streamseqs into a setoid and lift every operation on streamseqs to morphisms We first prove reflexivity symmetry and transitivity of bisimulation because each proof must be given using let corec let corec reflerive_ss_bisimilar A Type 0 reflexive ss_bisimilar A ati hd tl Greflexive_ss_bisimilar qed let corec symmetric_ss_bisimilar A Type 0 symmetric ss_bisimilar A 1 7 hd1 tl1 hd2 tl2 hd tl1 tl2 H Y Osymmetric_ss_bisimilar OH qed In the proof of transitivity we face a technical problem After inverting one of the bisimilarity hypothesis we are left with an equation of the form sscons hd1 tl1 sscons hd2 t12 and we need to infer the two equations hd1 hd2 and tl1 t12 to conclude the proof The destruct tactic does exactly this but it produces a proof term that is not recognized to be productive by Matita Moreover for technical reasons checking for productivity is only performed at qed Journal of Formalized Reasoning Vol 7 No 2 2014 Matita Tutorial i 187 time every step of the proof would be accepted by Matita but the whole proof would be rejected at qed The trick to preserve productivity is to cut the two equalities and to use destruct to prove them In this way the destruct tactic is used only in a side proof inside which there is no recursive call and the whole proof term is recognized to be productive let core
128. r composition generalizing the transitivity of the order relation and we are supposed to have identities for any object generalizing reflexivity The notion of monotone function generalizes to the notion of functor A functor F between two categories C and D is a transformation mapping any object a of C into an object F a of D and any morphism f a gt b into a morphism E f F a gt F b in D The functor is supposed to be well behaved in the sense that it maps identities to identities F id idp a and it preserves composition F f 0g F f o F g So when we try to interpret types defined by a recursive equations of the form X F X an essential prerequisite is to be able to provide a functorial description of the transformation F and in particular of the action of F on morphisms i e on terms Consider for instance the equation X unit X definining nat Given a function f A gt B it is natural to lift it to F f unit A gt unit B as idunit f Now suppose we have an equation of the form X X gt X then given f A B we would need to lift f to a morphism in A gt A gt B gt B and there is no natural way to do it we miss a transformation from B to A The strict positivity condition is a syntactic criterion that guarantees that we can always associate a functorial action with our construction This is actually directly exploited in the definition of the eliminators for the inductive type 9 2 U
129. races of a program Let s introduce a very simple programming language whose instructions can test and set a single implicit variable inductive instr Type 0 p_set N gt instr sets the variable to a constant p_incr instr increments the variable p_while list instr gt instr repeats until the variable is O The states of a program are given by the current value of the variable and the list of instructions to be executed definition state Nx list instr The following function defines the transition relation beteen states inductive next state state Prop n_set Vn k o next o p_set n k n k m_incr Vk o next 0 p_incr k S o k n_while_exit Vb k next 0 p_while b k 0 k n_while_loop Vb k o next S o p_while b k S 0 b p_while b k A diverging trace is a sequence of states such that the n 1 th state is obtained executing one step from the n th state record div_trace Type 0 div_tr seq state div_well_formed Vn next div_tr n div_tr S n The previous definition of trace is not computable we cannot write a program that given an initial state returns its trace To write such a function we first write a computable version of next called step Journal of Formalized Reasoning Vol 7 No 2 2014 Matita Tutorial gt 175 gt definition step state option state As let 0 k s in match k with
130. re put on let corec definitions If fis a let rec defined term f is only expanded when it occurs in the scrutinee of a match expression that is in a situation of the kind match f t1 tn with To better understand the duality that is not syntactically perfect note that in the recursive case f destructs terms and is expanded only when applied to a constructor in the co recursive case f constructs terms and is expanded only when it becomes argument of the match destructor Termination is guaranteed by the combination of this restriction and f being productive the term match f t1 tn with will reduce in a finite amount of time to a match applied to a constructor whose reduction can expose another application of f but not another match f t1 tn with Therefore since no new matches around f can be created by reduction the number of destructors that surrounds the application of f decreases at every reduction of the match eventually leading to termination Even if a coinductively defined f does not reduce in every context to its definien dum it is possible to prove that the definiens is Leibniz equal to its definiendum The trick is to prove first an eta expansion lemma for the coinductive type that states that an inhabitant of the coinductive type is equal to the one obtained destructing and rebuilding it via a match The proof is done by cases on the in habitant Let s see an example lemma eta_streamseq VA Typ
131. rnal of Formalized Reasoning Vol 7 No 2 2014 Matita Tutorial s 95 wget http matita cs unibo it sources matita_130312 tar gz tar xzf matita_130312 tar gz In MATITA_HOME you should now be left with two further subdirectories matita and components as well as numerous makefiles and auto configuration scripts Build the configuration script with the following command autoconf configure ac gt configure chmod x configure configure This will check that all needed tools and libraries are installed and prepare the sources for compilation and installation Then type make world All being well the previous command will build the various Matita related binaries and their optimised counterparts and place them in MATITA_HOME matita In particular check for the presence of the optimised Matita binary matita opt in this subdirectory 0 2 Preparing a working directory Before you start editing proof scripts you must prepare a working directory this can be anywhere in your file system AZs file hierarchy and does not need to be a subdirectory of MATITA_HOME For example cd mkdir ProofScripts cd ProofScripts We shall refer to this directory as SCRIPTS_HOME henceforth In SCRIPTS_HOME create a file called root containing the following declaration baseuri cic matita Congratulations you are ready to start proving things 0 3 Matita interface In order to check that everything is up and runn
132. roof of div2_ok is therefore the following n elim n q r H normalize in H destruct a Hind q tr cut div2 a fst div2 a snd div2 a cases snd div2 a H gt div2S1 H H1 destruct normalize eq_f gt add_S Hind H gt div2sO H H1 destruct normalize eq_f Hind H qed 2 7 Lapply The cut rule is the main tool for forward reasoning in interactive provers that is for introducing a new intermediate proposition P between the given hypothesis and the current goal If we already have in mind an explicit proof H for the proposition P a viable alternative to introduce P with a cut and prove it with His to call the following tactic y lapply H If the type of His P the effect of the tactic is to transform the current goal G into the new goal P gt G For instance if n nat the tactic lapply add_Sn 0 S would transform a goal Ginto add n S 0 S add n 0 gt G The name lapply stands for left application where left should be understood in sequent like sense that is as referring to the left side of the sequent which is the context It is in fact a generalization of the left introduction rule for application in sequent like calculi The advantage of lapply with respect to a cut is to avoid the explicit writing of the cut formula that in the case of lapply is automatically inferred being the type of its argument Journal of Formal
133. rue is to prove P 5In case of inductive data types of sort T ype j for some j the system also generates for each i an elimination rules towards P Type i called T_rect_Typei The rule allows us to inhabit some type U Typeli by recursion on the eliminated term of type Type j Journal of Formalized Reasoning Vol 7 No 2 2014 Matita Tutorial 121 True_ind VP Prop P True gt P Finally let us consider the case of existential quantification In order to conclude Jz 4 Q x we need to prove Q a for some term a A Hence the introduction rule for the existential looks like the following Va A Qa gt J1 Q z from which we get the following inductive definition parametric in 4 and q inductive ex A Type 0 Q 4A Prop Prop ex_intro Va A Q z gt ez ARQ In the next Section we will see how to associate the usual notation 3x 4 Q to ez A Az Q The elimination principle automatically generated by Matita is ez_ind VA VQ 4 gt Prop VP Prop Vzx A Qa gt P gt 1 4 0 gt P That is if we know that P is a consequence of Q x for any 2 4 then it is enough to know 32 4 Q to conclude P It is also worth spelling out the backward reading of the previous principle Suppose we need to prove P under the assumption Jz A Q Then eliminating the latter amounts to assuming the existence of z A such that Q zand proceed to prove P under these new hypotheses 3 3 A bit of notation
134. s the proof is in general a complex lambda term whose only purpose is to provide a mechanically verifiable certificate that the witness satisfies a given property We shall come back to subset types is section 4 2 2 9 Tactic patterns Generally speaking the scope of a tactic is the conclusion of the current goal or the current goals if many are selected at once In section 2 5 however we have used normalize in H to indicate that the tactic should take effect within hypothesis H rather than the conclusion This in H is an instance of a more general scheme to express paths within the current goals by means of patterns Patterns allows us to specify any subterm of the conclusion or of any hypothesis Since the purpose of a pattern is to identify a subterm within a term its syntax is similar to that of a term where in addition to the usual syntax the symbol is used to specify the target position i e the subterm where the tactic should act all the parts of the term that must not be targeted by the tactic are replaced by symbols in the pattern For the purpose of matching against patterns all user defined notation e g infix symbols omitted terms to be inferred by the system is ignored Notations will be discussed in Section 3 3 For example if we are given a term z a b c that ignoring notation for addition and equality is eq nat x plus plus a b c we can specify the subterm a b by means of the pattern 777
135. s currently loaded partitioned according to their precedence level The next step is to associate an interpretation with content patterns in the following way interpretation logical and and x y And z y interpretation logical or or x y Or z y With these commands we are saying that a possible interpretation of the symbol and is the inductive type And and a possible interpretation of the symbol or is the inductive type Or But we could e g define boolean functions andb and orb and provide an alternative interpretation of and and or on them As a result the notations AA B and AV B would be overloaded and interpreted as a proposition or a boolean depending on the context they occur in For details on the resolution of overloading see Let us conclude this section with a discussion of the notation for the existential quantifier In contrast to what we did previously we use one mapping for the notation used to pretty print terms and a different one for parsing The one for parsing will be more complex to allow omission of types and packing of multiple declarations into a more compact syntax notation lt huboxr exists ident i ty break p right associative with precedence 20 for exists A ident i ty p The lt symbol after the notation keyword states that this mapping will only be used during pretty printing The other main novelty is the special keyword ident that instructs
136. s of complex data structures A function definition most often corresponds to pattern matching on one or more of its parameters allowing the function to be easily defined by cases The syntactic structure of a match expression is the following match expr with pi gt expri p2 gt expra Pn gt ezprn The expression expr which is supposed to be an element of an inductive type 7 is matched sequentially to the various patterns p pn A pattern p is just a constructor of the inductive type T possibly applied to a list of variables bound 4The notion of inductive type is more general and admits other shapes They will be discussed in Section 3 Moreover not every form of recursive constructor is accepted since in order to ensure logical consistency we must respect some positivity conditions that we shall discuss in Section 9 Journal of Formalized Reasoning Vol 7 No 2 2014 Matita Tutorial 101 inside the corresponding branch ezpr If the pattern p matches the value ezpr then the corresponding branch ezpr is evaluated after replacing in it the pattern variables with the corresponding subterms of espr Usually all expressions expr have a single uniform type however since Matita supports dependent types the type of branches could depend on the matched expression too see section 5 10 1 3 Our first lemma Functions are live entities and can be actually computed To check this let us state the
137. s of the automaton is finite Pointed regular expressions offer an appealing alternative to Brzozowski s deriva tives avoiding their weakest point namely the fact of being forced to quotient derivatives with respect to a suitable notion of equivalence in order to get a finite number of states that is not essential for recognizing strings but is crucial for comparing regular expressions 6 1 Words and Languages An alphabet is an arbitrary set of elements equipped with a decidable equality a DegSet see Section 5 5 A string or word over the alphabet s is just an element of list s The empty string e is then another notation for the empty list A language L over an alphabet S is a set of strings in list S As described in Section 5 4 a traditional way to encode subsets of a given set U in type theory is by means of predicates over a type U which are elements of U Prop A language over an alphabet Sis hence an element of list S gt Prop Languages inherit all the basic operations for sets namely union intersection complementation difference and so on In addition we may define some new operations induced by string concatenation and in particular the concatenation A B of two languages A and B the Kleene s star A of A and the derivative of a language 4 w r t a given character a which is the set of all strings w such that aw E A definition cat AS 4 B Aw word S Jw1 w2 w1 0 w2 w A w1 AB w2 defini
138. se the two facts east_west and west_east Between opp and opposite the following relation holds opp a b a opposite b Let us prove it starting from the left to right implication first lemma opp_to_opposite Va b opp a b gt a opposite b We start the proof introducing a b and the hypothesis opp a b that we call oppab Next we proceed by case analysis on the possible proofs of opp a b i e on the possible shapes of oppab By definition there are only two possibilities namely east_west or west_east Both resulting subcases are trivial and can be closed by automation The whole proof is hence a b oppab cases oppab qed 1 7 Rewriting Let us consider the opposite direction lemma opposite_to_opp Va b a opposite b opp a b Journal of Formalized Reasoning Vol 7 No 2 2014 104 A Asperti and W Ricciotti and C Sacerdoti Coen As usual we start introducing a b and the hypothesis a opposite b that we call eqa The right way to proceed now is by rewriting a into opposite b We do this by typing gt ega that instructs the system to rewrite inside the goal using the equation named ega oriented from left to right If we wished to rewrite in the opposite direction namely opposite b into a we would have typed lt ega In section 2 9 we shall explain how to restrict localize rewriting and other operations by means of patterns After rewriting we simply conclude the proof
139. sen and Pawel Urzyczyn Lectures on the Curry Howard Isomorphism volume 149 Elsevier 2006 The Univalent Foundations Program Homotopy Type Theory Univalent Foundations of Mathematics http homotopytypetheory org book Insti tute for Advanced Study 2013 Benjamin Werner Une Th orie des Constructions Inductives PhD thesis Universit Paris VII May 1994 Freek Wiedijk The seventeen provers of the world LNAI 3600 2006 Journal of Formalized Reasoning Vol 7 No 2 2014 Matita Tutorial 199 Journal of Formalized Reasoning Vol 7 No 2 2014
140. seq qed Journal of Formalized Reasoning Vol 7 No 2 2014 180 A Asperti and W Ricciotti and C Sacerdoti Coen 8 5 Intermezzo the dynamics of coinductive data Corecursive definitions like recursive ones are a form of definition where the definiens occurs in the definiendum Matita compares terms up to reduction and reduction always allows the expansion of non recursive definitions If it also allowed the expansion of recursive definitions reduction could diverge and type checking would become undecidable For example consider again the definition of all_zeros let corec all_zeros streamseq nat sscons nat O all_zeros If the system expanded all occurrences of all_zeros it would expand it forever to sscons 0 sscons 0 sscons 0 In order to avoid divergence recursive definitions are only expanded when a certain condition is satisfied In the case of a let rec defined function f that is recursive on its n th argument f is only expanded when it occurs in an applica tion f t1 tn and tn is the application of a constructor Termination is guaranteed by the combination of this restriction and f being guarded by destruc tors the application f t1 tn can reduce to a term that contains another application f t1 tn but the size of tn roughly the number of nested constructors will be smaller than the size of tn eventually leading to termination Dual restrictions a
141. ses t in H normalize abs cases False inversion abs Hs _ eq destruct hd1 hd2 tl _ _ eq destruct qed A stream can be extracted from a streamseq using corecursion let corec stream_of_streamseq A Type 0 s streamseg A stream A match s with sscons hd tl scons hd stream_of_streamseg tl We need again an expansion lemma to typecheck the proof that the resulting stream is divergent lemma stream_of_streamseq_expansion VA hd tl stream_of_streamseg A sscons hd tl scons hd stream_of_streamseq tl Journal of Formalized Reasoning Vol 7 No 2 2014 Matita Tutorial e 185 HA hd tl lt eta_stream stream_of_streamseq qed The proof that the resulting stream is diverging also needs corecursion let corec diverging stream_of_streamseq s streamseq state diverging stream_of_streamseq s match s return As diverging stream_of_streamseq s with sscons hd tl gt gt stream_of_streamseq_expansion h qed let corec well_formed_stream_of_streamseg d streamseq state div_well_formed d gt well_formed stream_of_streamseq state d match d return Ad div_well_formed d gt with sscons hd1 tl gt match tl return Atl div_well_formed sscons tl gt with sscons hd2 tl2 gt H 1 gt stream_of_streamseq_expansion gt stream_of_streamseg_ezpansion 2 2 lt stre
142. soning Vol 7 No 2 2014 Matita Tutorial e 139 det rec append A l1 list A 12 on l1 match 11 with nil gt 12 cons hd tl gt hd append A tl 12 We leave it to the reader to prove that append is associative and that nil is a neutral element for it Before discussing more operations over lists it is convenient to introduce a bit of notation we shall write a 1 for cons a 1 a1 a2 an for the list composed by the elements a a2 an and 1 012 for the concatenation of l and 12 This can be obtained by means of the following declarations a Y notation hubor hd break tl right associative with precedence 47 for cons hd tl notation listO term 19 z sep non associative with precedence 90 for fold right nil rec acc Ol cons x acc notation hubor 1l1 break 12 right associative with precedence 47 for Cf append 11 12 interpretation nil nil nil interpretation cons cons hd tl cons hd tl interpretation append append 11 12 append 11 12 Note that is an alternative notation for the empty list and a is a list containing a singleton element a We conclude this section discussing another important operation over lists namely the reverse function returning a list with the same elements as the original list but in reverse order One could define the reverse operation as follows r s let rec rev A l1 on l1 match 1
143. stem that stands for the type of all propositions Hence the sentence True Prop simply affirms that True is a proposition So this is the type of True but what is its actual definition The Matita Browser similarly to the goal window is hypertextual you can directly jump to the def initions of objects by just clicking on them If you click on True you will discover that it is an instance of an entity called inductive type Matita is actually based on a Dependent Type System known as the Calculus of Inductive Constructions see 23 18 in such a framework as we shall explain in Section 3 almost everything is defined as an inductive type we shall also come back in that occasion to the definition of True We claimed that every term has a type so you might wonder what is the type of Prop If you check it you will discover that Prop Typelo In the same way as Prop is the type of all propositions Type is in a sense the type of all types But what is the meaning of the label 0 Well the point is that to avoid logical paradoxes a la Russell types of types called universes should be organized into a hierarchy of the following kind Type 0 Type 1 Typel2 Typel3l For the moment you may just ignore the existence of Type i for i larger than 0 0 5 Live DVD If you are not running Linux or you do not want to install Matita you can download a Live DVD image from the download page of Matita The ima
144. t subtrees have different heights whereas parameters must remain constant inductive SBBT nat Type 0 leaf nat SBBT 0 node Vn SBBT n SBBT n gt SBBT S n Suppose we want to write a function subtree_left which given a SBBT returns its left subtree assuming it exists A possible implementation uses as the output type of the function an optional value which allows us to return a None when the input is a leaf definition subtree_left Vn Vt SBBT n option SBBT pred n An t match t with leaf k gt None node m t1 t2 Some ti Journal of Formalized Reasoning Vol 7 No 2 2014 Matita Tutorial 147 This operationally correct implementation is rejected by the system which is unable to synthesize the return type of the match To overcome this problem as we did in Section 4 2 we need to add more type annotations by means of the return clause to the match Since the matched type depends on an argument the height of the tree which changes depending on the branch of the match the function expressing the return type must depend not only on the matched term but also on the index n of its type SBBT n For the subtree_left function we need to specify that the output type is an optional SBBT whose height is the predecessor of that of the input tree definition subtree_left Vn Vt SBBT n option SBBT pred n An t match t return An0 t0 option SBBT pred n0 wit
145. t may be necessary to represent and manipulate infinite structures Typical examples are sequences real numbers a special case of se quences data streams e g as read from a network interface traces of diverging computations of a program etc In the next section we shall start discussing a few examples exploiting functions for the representation of objects then we shall move on to a different encoding based on coinductive types 8 1 Real Numbers as Cauchy sequences In many cases it is possible to describe an infinite object by means of an infinite sequence of approximations also called observations where the sequence can be simply defined as a function on the domain of natural numbers definition seg Typel0 Typel0 AA Type 0 N gt A A well known example is the definition of Real numbers by means of Cauchy se quences First of all we axiomatize the relevant properties of rational numbers r axiom Q Type 0 axiom Qdist Q gt Q gt Q axiom symmetric_Qdist Va y Qdist z y Qdist y z axiom Qleq Q gt Q Prop interpretation Qleq leq x y Qleq z y axiom transitive Qleq transitive Qleq axiom Qplus Q gt Q gt Q interpretation Qplus plus x y Qplus z y axiom leg plus Vqa1 qb1 qa2 qb2 qal lt qb1 gt qa2 lt qb2 gt qal qa2 lt qb1 qb2 axiom Qdist_Qplus Vqal qb1 qa2 qb2 Qdist qal qa2 qb1 qb2 lt Qdist qal qb1 Qdist qa2 qb2 a
146. t proving that opp west west is absurd has about the same complexity of the original problem In fact the best approach consists of generalizing the statement to something similar to opp_to_opposite and then prove it as a corollary of the latter It is interesting to observe that we would not have the same problem with opp1 or opp2 For instance by cases analysis on H opp1 west we would obtain the two subgoals G1 w east gt uwest west gt u east Go a west gt west east a east The first one is trivial while the second one is easily closed using destruct The point is that naive pattern matching is not powerful enough to discriminate the structure of arguments of inductive types To this aim however you may exploit an alternative tactic called inversion Suppose to have in the local context an expression H T t where T is some induc tive type Then inversion H derives for each possible constructor c of T E all the necessary conditions that should hold for the instance T to be proved by ci For instance if the current goal is z east invoking inversion on the hypothesis H opp x west would result in the following subgoals G1 w east west west gt z east Go a west gt west east a east that are precisely the same goals generated by case analysis on opp1 REMARK 1 Invoking inversion on inductive types without arguments does not make any sense and has no practical effect Journal of Formalized Reas
147. taken as a parameter This kind of types is quite unusual in traditional programming languages and their study is one of the new frontiers of the current research on type systems There is nothing special in a subset type fa A P a it is just a record composed of an element a of type 4 and a proof of P a Nevertheless it provides a language rich enough to comprise proofs among its expressions AS record Sub A Type 0 P A4 Prop Type 0 witness A proof P witness definition gr_spec An Ap Vq r p q r gt n add nat_of_bool r twice q We can now construct a function from n to plqr_spec n p by composing the objects we already have definition div2P Vn Sub natxbool qr_spec n An mk_Sub div2 n div2_ok n But we can also try to directly build such an object definition div2Pagain Vn Sub natxbool qr_spec n tn elim n mk_Sub 0 false normalize tq tr H destruct a p qrspec cut p fst p snd p cases snd p H mk_Sub S fst p false tq tr H1 Journal of Formalized Reasoning Vol 7 No 2 2014 Matita Tutorial 117 destruct eq_f gt add_S qrspec H mk_Sub fst p true q tr H1 destruct eq_f O grspec H qed The reader is invited to run the computation of the previous function on a few examples to see what the output looks like The only readable information is in fact the witnes
148. tarting with disjunction The first point is to derive the introduction rule s When can we conclude AV B Clearly we must either have a proof of A or a proof of B So we have two introduction rules in this case A gt AVB and B AVB that leads us to the following inductive definition of disjunction inductive Or A B Prop Prop or_introl A gt r A B or_intror B gt 0r A B The elimination principle automatically generated by the system is or_ind VA B P Prop A gt P gt B gt P gt AVB gt P that is a traditional formulation of the elimination rule for the logical disjunction in natural deduction if P follows from both A and B then it also follows from their disjunction More surprisingly we can apply the same methodology to define the constant False The point is that obviously there is no canonical way to conclude False so we have no introduction rule and we must define an inductive type without constructors which is accepted by the system inductive False Prop The elimination principle is in this case False_ind VP Prop False P that is the well known principle ex falso quodlibet What about True You may always conclude True hence corresponding inductive definition just has one trivial constructor traditionally named 1 inductive True Prop I True As expected the elimination rule is not informative in this case the only way to conclude P from T
149. te that we do not have a base case so how can we inhabit the previous type In general coinductive types are inhabited by infinite data obtained by means of a special kind of coinductive definitions introduced by the keyword let corec The syntax of let corec definitions is the same of let rec definitions but for the declarations of the recursive argument While let rec definitions are recursive def inition that are strictly decreasing on the recursive argument let corec definitions are productive recursive definitions A recursive definition is productive if when its definiendum is fully applied to its arguments it reduces in a finite amount of time to the application of a constructor of a coinductive type In typical cases the definiendum is already the application of a constructor Let us see some simple examples of coinductive definitions of corecursive stream seqs The following definition defines an infinite sequence of zeros let corec all_zeros streamseq nat sscons nat O all_zeros Note that al1_zeros is not a function and does not have any argument The definition is clearly productive because its definiendum is the constructor sscons The following definition defines the sequence n n 1 n 2 starting from an input value n let corec from_n n N streamseq nat sscons n fromn S n The definition essentially behaves like an automaton with state n When the streamseq is pattern matched the
150. terms t1 t2are bisimilar if one simulates the other and the other way around where t2 simulates t1 if every observation on t1 can be performed on t2 as well and the observed subterms are co recursively bisimilar In practice two coinductive terms are bisimilar if they are the same constructor applied to bisimilar coinductive subterms We define bisimilarity for streamseqs using a coinductive predicate coinductive ss_bisimilar A Type 0 streamseq A gt streamseq A Prop sscons_bisim Va tl1 tl2 ss_bisimilar tl1 tl2 gt ss_bisimilar sscons z tl1 sscons x tl2 The two streams above can be proved to be bisimilar By using the eta_streamseq trick twice we expand both definitions once so to obtain a proof obligation that asks to show that the stream sscons 0 sscons 1 zero_one_streamseq1 is bisimilar to sscons 0 sscons 1 zero_one_streamseq2 Then we apply twice the sscons_bisim constructor to consume the leading 0 and 1 finding again the original goal Finally we conclude with the coinductive hypothesis The proof is productive because after the two rewriting steps it reduces to two applications of the sscons_bisim constructor immediately followed by the recursive call let corec zero_one_streamseq_eq ss_bisimilar zero_one_streamseq1 zero_one_streamseq2 lt eta_streamseq zero_one_streamseq1 normalize lt eta_streamseq one_zero_streamseq normalize h Ozero_one_streamse
151. th to extract filter specific components The function change_vec A n v a treplaces the content of the vector v at position 4 with the value a The most frequent operation on vectors for our purposes is comparison In this case we have essentially two possible approaches we may proceed component wise using the following lemma lemma eq_vec VA n Vvu1 v2 Vector A n Vd Vi i lt n nth i Avi d nth i A v2 d gt v1 v2 or alternatively we may manipulate vectors by exploiting commutativity or idem potency of change_vec and its interplay with other operations 5 10 Dependent matching We are now going to present the full syntax of the pattern matching construct as well as its typing rule by means of simple examples concerning a type of strictly balanced binary trees In standard textbooks on data structures a binary tree is balanced when the heights of the left and right subtrees of every node differ by at most 1 our definition is strictly balanced because we require the subtrees of every node to have exactly the same height Concretely we define the inductive type SBBT nof strictly balanced binary trees of height n that store natural numbers in their leafs The constructor leaf has as input the natural number stored in the leaf and builds ans SBTT of zero height The constructor node combines two SBBTs t t2 of the same height minto a new SBBT of height S m The height cannot be expressed as a parameter because differen
152. th R i Qstreamseq_nth R j lt eps and the definition of a real numbers as an equivalence class of Cauchy sequences record R_ Typel0 r Qstreamseq tsCauchy Cauchy r The following statement provides the setoid structure for reals the proof that Cauchy is an equivalence relation is identical to the proof is section 8 1 and we skip it r definition R setoid mk_setoid R_ mk_equivalence_relation Ar1 r2 R_ Veps dn Vi n lt 1i gt Qdist Qstreamseg_nth r ri i Qstreamseg_nth r r2 i lt eps unification hint 0 R carrier P Journal of Formalized Reasoning Vol 7 No 2 2014 Matita Tutorial i 179 The following coercion is used to write r n to extract the n th approximation from the real number r coercion R_to_fun Vr R N gt Q Ar Qstreamseg_nth r r on _r R to 7l Pointwise addition over Qstreamseg defined by corecursion The definition is productive because when Rplus_streamseq is applied to two closed values of type Qstreamseq it will reduce to sscons let corec Rplus_streamseq x Qstreamseq y streamseg Qstreamseg match with sscons hdz tle gt match y with sscons hdy tly gt sscons hdx hdy Rplus_streamseg tla tly J The following lemma was for free using sequences In the case of streamseqs it must be proved by induction on the index because
153. the n th approximation from the real number r coercion R_to_fun Vr R N gt Q r on _r R to We conclude this first example considering the definition of the sum operation between real numbers This just requires pointwise addition of the approximations The proof that the resulting sequence is Cauchy is the standard one to obtain an approximation up to e it is necessary to approximate both summands up to e 2 definition Aplus_ R_ gt R_ gt R_ Ar1 r2 m_R_ An ri n r2m tteps cases isCauchy ri Qhalve eps n1 H1 cases isCauchy r2 Qhalve eps n2 H2 i maz n1 n2 i 7 K1 K2 O transitive leg Qdist_Qplus lt Qplus_Qhalve_Qhalve eps O leg_ plus 0H1 le_mazl H2 le_mazr 2 6 K1 4 8 0K2 qed Journal of Formalized Reasoning Vol 7 No 2 2014 174 A Asperti and W Ricciotti and C Sacerdoti Coen We lift Rplus_ to a morphism by proving that it respects equivalence of real numbers We closely follow the usual mathematical proof to compute the sum up to epsilon it is sufficient to fetch the arguments at precision 2 A definition Aplus R gt R gt R mk_bin_morphism Rplus_ 21 x2 y1 y2 Hx Hy eps cases Hx Qhalve eps i Hx Ha cases Hy Qhalve eps j Hy Hy A Cmaz i j l Hmax lt Qplus_Qhalve_Qhalve eps transitive_Qleq 3 O Qleg_Qplus Hx l Hy l 2 by le mazl le_masr 12 1 qed 8 2 T
154. ther tinycals and a few tacticals that are not described in the tutorial but can be found in the user manual Let us see the effect of the on our proof We were in a state where we had four active goals By executing the four goals get a progressive number and the first of them the new intermediate state gets the focus We can now proceed in several possible ways The most straightforward way is to explicitly supply the next intermediate state that is mk_state east west west east We can do it by applying the term mk_state east west west east This application closes the current goal at present no goal has the focus on In order to act on the next goal we must focus on it using the operator In this case we would like to skip the next goal and focus on the trivial third subgoal a simple way to do it is by typing again The current goal is hence safe_state mk_state east west west east whose proof is trivial and can be delegated to automation We then advance to the next goal namely the fact that there is a move from mk_state east west west east to mk_state west west west west this is triv ial too but it requires 2 automation at depth two since move_goat opens an Journal of Formalized Reasoning Vol 7 No 2 2014 Matita Tutorial 107 additional subgoal By applying we refocus on the skipped goal going back to a situation similar to the one we started with Here is th
155. tion o re S gt re S gt re S plus k re S gt reS kleene s star We skip the obvious notational command that allow us to use the traditional nota tion for regular expressions namely a e1 e2 e1 e2 e where a ranges over the alphabet s The language sem r notation r associated with the regular expression r is defined by the following function let rec sem S DeqSet r re S on r word S gt Prop match r with z gt f gt te x gt z ri r2 gt r1 r2 ri r2 gt r1 Ul r2 l l l l kri gt r1 xr OA Hh 6 3 Pointed regular expressions A pointed item is a data type used to encode a set of positions inside a regular expression A simple way to formalize pointers inside a data type is by means of a labelled version of the very same data type For our purposes it is enough to mark positions preceding individual characters so we shall have two kinds of characters ea pp a and a ps a according to whether a is pointed or not Journal of Formalized Reasoning Vol 7 No 2 2014 152 i A Asperti and W Ricciotti and C Sacerdoti Coen N inductive pitem S DegSet Type 0 pz pitem S pe pitem S ps S gt pitem S pp S gt pitem S pe pitem S gt pitem S gt pitem S po pitem S pitem S gt pitem S pk pitem S gt pitem S A pointed regular expression PRE is just a pointed ite
156. tion correctness verification type checking Fig 2 Curry Howard Correspondence Let us make a final remark If a program is a proof then what corresponds to the act of verifying the correctness of a proof M of some proposition A Well M is just an expression that is supposed to have type A so proof verification is nothing else than type checking This should also clarify that proof verification is a much easier task than proof search While the former corresponds to type checking the second one corresponds to the automatic synthesis of a program from a specification The main ideas behind the Curry Howard correspondence are summarized in Figure 2 4 5 Prop vs Type In view of the Curry Howard analogy the reader could wonder if there is any actual difference between the two sorts Prop and Type in a system like the Calculus of Constructions or if it is just a matter of flavour In fact there is a subtle difference concerning the type of product types over the given sorts Consider for instance a higher order statement like VP Prop P This is just a sentence asserting that any proposition is true and it looks natural to look at it as an object of sort Prop However if this is the case when we are quantifying on all propositions we are also implicitly quantifying over the proposition we are in the act of defining that creates a strange and possibly dangerous circularity In mathematics definitions of this kind where the defin
157. tion star AS A Aw word S 3lw flatten S lw w Alist_forall S lw A definition deriv AS 4 a w A a w In the definition of star flatten and list_forall are standard functions over lists mapping 11 2n to l1 l2 ln and w wo Un to 4 w A A w A A un Two languages are equal if they are equal as sets see the definition of egP in Section 5 4 that is if they contain the same words Journal of Formalized Reasoning Vol 7 No 2 2014 Matita Tutorial i 151 The main equations between languages that we shall need for the purposes of this tutorial in addition to the set theoretic ones and those expressing extensionality of operations are listed below the simple proofs are omitted sama epsilon_cat_r VS VA word S Prop A fe A lemma epsilon_cat_l VS VA word S Prop fe A A lemma distr_cat_r VS VA B C word S Prop AUB C A CUB C lemma deriv_union VS A B a deriv S A UB a deriv S A a U deriv S B a lemma deriv_cat VS A B a A gt deriv S AB a deriv S A a B lemma star_fix_eps VS VA word S Prop AX A 4H 44 U e 6 2 Regular Expressions The type re of regular expressions over an alphabet S is the smallest collection of objects generated by the following constructors inductive re S DeqSet Type 0 z res empty e res epsilon s Sores symbol c re S gt re S gt re S concatena
158. tita s automation facilities 1 10 Application Let us now try to derive the proof in a more interactive way Of course we expect to need several moves to transfer all items from a bank to the other so we should start our proof by applying more Matita syntax for invoking the application of a lemma or theorem named foo is to write foo In general the philosophy of Matita is to describe each proof of a property Pas a structured collection of objects involved in the proof prefixed by simple modalities lt explaining the way it is actually used e g for introduction rewriting in an applicative step and so on lemma problemi reachable start end normalize more After performing the previous application we have four open subgoals note by the way that the type of some goals may depend on the values of other goals goal type X state Y reachable mk_state east east east east X W safe state X Z move X mk_state west west west west Journal of Formalized Reasoning Vol 7 No 2 2014 106 A A Asperti and W Ricciotti and C Sacerdoti Coen namely we must provide a state X such that Y it is reachable from start m it is safe and Z there is a move leading from X to end All goals are active as emphasized by the fact that their title in the goal pane are all bold Any command typed by the user is normal ly applied in parallel to all active goals but clearly in the above case we must proceed i
159. toid AI 0 mk_setoid I gt 0 mk_equivalence_relation Af g Va y I v gt y gt f 229 Y whd f1 412 f3 f1_f2 f2_f3 tx y EQ equiv_trans f2 2 2 f1 f2 f1_f2 tx y EQ Olequiv_sym f1_f2 equiv_sym f 0 ty EQ Omor_proper qed unification hint 0 1 0 setoid po function_space I 0 I 0 carrier X We overload the notation so that I gt 0 can mean both the type of morphisms from I to O or the function space from I to 0 Journal of Formalized Reasoning Vol 7 No 2 2014 166 E A Asperti and W Ricciotti and C Sacerdoti Coen interpretation function_space morphism I O function_space I 0 A binary morphism is just obtained by currying In the following we will use I1 gt 12 gt 0 directly in place of bin_morphism definition bin_morphism setoid gt setoid gt setoid gt Typel0 A11 12 0 11 gt 12 gt 0 Directly constructing an inhabitant of a binary morphism is annoying because one needs to write a function that returns a morphism instead of a binary function Moreover there are two proof obligations to prove We can simplify the work by introducing a new constructor for binary morphisms that takes in input a binary function and opens a single proof obligation called proper2 definition proper2 WI1 I2 0 setoid I1 gt I2 gt 0 gt Prop AI1 12 0 f Vzxl 12 y1 y2 21 212 gt y1 y2 gt f x1 y
160. two enumerations 0 1 2 are extensionally but not intensionally equal N Journal of Formalized Reasoning Vol 7 No 2 2014 188 E A Asperti and W Ricciotti and C Sacerdoti Coen definition enum_N1 seq N i i definition enum_N2 seq N Ai i 0 Functional extensionality is defined in the standard library of Matita as follows definition exteqF WA B Typel0l Vf g A gt B Prop A B Af g Va fa qa The proof that the two sequences above are extensionally equal is trivial lemma enum_N_equal exteqF enum_N1 enum_N2 normalize qed Like for bisimulation to work systematically with functional extensionality we need to turn the type of sequences into a setoid The two alternatives are actually equivalent with respect to this issue 8 8 Generic construction principles When an inductive type is defined Matita automatically proves a generic elimination principle using a recursive definition Later the user can apply the generic eliminator in the middle of a proof without the need to make a lemma and prove it using a let rec For example the principle generated for a list is the following VA Type 0 VP A Prop P nil gt Vhd A Vtl list A P tl gt P hd t1 gt Vi list A PL Here the predicate P is dependent on the list we are analyzing The useless corresponding non dependent principle is VA Type 0 VP Prop P gt Vhd A Vtl list A P gt P gt
161. ural numbers the predecessor of 0 is undefined In these situations we may either return a default value usually pred 0 0 or decide to return an option type as a result An option type is a polymorphic type that represents encapsulation of an optional value It consists of either an empty constructor traditionally called None or a constructor encapsulating the original data type A written Some A inductive option A Type 0 Type 0 None option A Some A gt option A The type option A is isomorphic to the disjoint sum between unit and A The two bijections are simply defined as follows definition option_to_sum A Az option A match x with None gt inl it Some a gt inr a D definition sum_to_option A4 Az unit A match x with inl a gt None A inr a gt Some Aa The fact that going from the option type to the sum and back again we get the original element follows from a straightforward case analysis y lemma option_bij1 VA x sum_to_option A option_to_sum A a z HA ged The other direction is just slightly more complex since we need to exploit the fact that the unit type contains a single element we could use lemma eg_unit or proceed by case analysis on the unit element lemma option_bij2 VA x option_to_sum A sum_to_option A a z HA qed We shall see more examples of functions involving the option type in
162. use the function opp which does not carry additional information The following hints will be automatically used by the system to retrieve the morphism associated to opp when needed i e to retrieve the proof of properness of opp This is a use of unification hints to implement automatic proof search The first hint is used when the function is partially applied the second one when it is applied to an argument unification hint 0 A II E opp mor_carr X unification hint 0 2 Z X OPP a ie E E opp x mor_carr X z For instance consider the proof that opp is proper We can prove it without any explicit mention of OPP In particular when we apply the universal property mor_proper of morphisms Matita looks for the morphism associated to opp z and finds it thanks to the second unification hint above completing the proof example ex2 Vr y Y opp T opp y tz ty EQ Omor_proper 0EQ qed The previous definition of proper only deals with unary functions In type theory n ary functions are better handled in curried form as unary functions whose output is a function space When we restrict to morphisms we do not need a notion of properness for n ary functions because the function space can also be seen as a setoid quotienting functions using functional extensionality two morphisms are equal when they map equal elements to equal elements definition function_space setoid setoid se
163. ut term is even and false if the input term is odd The boolean data type is defined in basics bool ma it is just an inductive type with two constructors true and false Since we must return a pair we could use a suitably defined record type or simply a product type natx bool already defined in the basic library in basics types ma together with notation for building and destructuring pairs The product type is just a sort of general purpose record with standard fields fst and snd called projections A pair of values n and mis written n m When p is a pair the expression let z y p in E binds g and yin E respectively to the first and second component of p We first write down the division function and then discuss it let rec div2 n match n with 0 gt 0 false Sa gt let q r div2 a in match r with true gt S q false false q true J Journal of Formalized Reasoning Vol 7 No 2 2014 Matita Tutorial 113 It is important to point out the substantial analogy between the algorithm for computing div2 and the proof of ez_kalf Consider ez_ha1f which returns a proof of the form 3n 4 n VB n the real informative content in it is the witness n and a boolean indicating which one between the two conditions A n and B n is met This is precisely the quotient remainder pair returned by div2 In both cases we recur respectively by induction or by recursion over the input argument n In
164. ving it interactively you may define your lemma as if it were the type of an expression and directly proceed to inhabit it with its proof definition trivial WP Prop P gt P AP h h Journal of Formalized Reasoning Vol 7 No 2 2014 132 A Asperti and W Ricciotti and C Sacerdoti Coen It is interesting to observe that this is really the same proof intensionally that would be produced interactively as testified by the following fragment of code lemma trivial1 WP Prop P gt P P h Oh qed lemma same_proofs trivial triviall refl qed Even more interestingly we can do the opposite namely define functions interac tively Suppose for instance that we need to define a function with the following type VA B C Typel01 A gt B gt gt AXB gt C If we just declare the type of the function followed by a fullstop Matita will start an interactive session completely analogous to a proof session and we can use the usual tactics to close the goal that is to inhabit the type definition uncurrying VA B C Type 0 A gt B gt C gt Ax B gt C HA B HC Hf Of qed If you are not convinced you generated a function or and this is plausible you are not so sure about the function you generated you can check your term or test it like in the following example example is just another Matita keyword similar to lemma or theorem examples may be referred to in proofs but are not use
165. we accept the following definition with U Type 0 inductive U Type 0 c VA Typel0 A Prop gt U Then we may look inside the type U for all those elements having U as carrier and for these elements it would be sound to ask if they belong to themselves or not A definition RussellP u U Vh carrier u U member u U u h Then we could form the following paradoxical element of U definition Russell U c U RussellP Suppose RussellP Russell by expanding the definition of Russel1P this is equiv alent to Vh carrier Russell U member Russell U Russell h In particular we may instantiate h with reflexivity and by member_to_P we get gt RussellP Russell Since RussellP Russell implies its negation we conclude Russel1P Russell To get a contradiction we still need to prove RussellP Russell or equivalently Vh carrier Russell U member Russell U Russell h If we assume proof irrelevance in fact Streicher s axiom of the uniqueness of iden tity proofs is enough all proofs that carrier Russell U are the same and we may replace h with reflexivity getting the goal member Russell U Russell h that we just proved 9 3 Informative and non informative content As we observed in the previous section the following definition is not accepted by Matita since it would be inconsistent inductive U Typel0 c VA Typel0 4 gt Prop gt U
166. xiom Qhalve Q gt Q axiom Qplus_Qhalve_Qhalve Vq Whalve q Qhalve q q axiom triangular_Qdist Vz y z Qdist x z lt Qdist x y Qdist y z Then we can define a sequence of rationals ys definition seg Type 0 seq Q and state the Cauchy property Journal of Formalized Reasoning Vol 7 No 2 2014 Matita Tutorial 173 A definition Cauchy Qseq Prop AR Qseq Veps dn Vi j n lt i gt n lt j gt Qd ist R i R J lt eps A real number is an equivalence class of Cauchy sequences In type theory we can define Ras a setoid whose carrier R_ is the type of Cauchy sequences record R_ Typelo r Qseq tsCauchy Cauchy r Two sequences are equal when for every epsilon they are eventually pointwise closer than epsilon definition R setoid mk_setotd R_ mk_equivalence_relation Ar1 r2 R_ Veps dn Vi n lt i gt Qdist r r1 i r r2 i lt eps transitivity tx ty tz H1 H2 tteps cases H1 Whalve eps i H1 H1 cases H2 Qhalve eps 7 H2 H2 7 max i 7 1 Hmax lt Qplus_Qhalve_Qhalve eps transitive_Qleq 3 Qleq_Qplus H1 1 H21 2 by le_mazl le_mazr 12 1 symmetry x y HH tteps cases H eps 3 by ex_intro reflexivity tx tteps cases isCauchy z eps 3 by ex_intro qed unification hint 0 R_ carrier R The following coercion is used to write r n to extract
167. y convertibility inequality Leibniz equality is a pretty syntactic intensional notion two objects are equal when they are the same term There is however an important point to under stand here the notion of sameness on terms is convertibility the smallest equiv alence relation containing reduction When reduction is confluent two terms are convertible if they have the same normal form For this reason not only 2 2 but also 1 1 2 since the normal form of 1 1 is 2 Having understood the notion of equality one could easily wonder how we can prove that two objects are different For instance in Peano arithmetic the fact that for any x 0 Sz is an independent axiom With our inductive definition on natural numbers of Section 2 can we prove it or are we supposed to assume such a property axiomatically In fact in a logical system like the Calculus of Inductive Constructions it is possible to prove it We shall discuss the proof here since it is both elegant and instructive The crucial point is to define by case analysis on the structure of inductive terms a characteristic property for the different cases For instance in the case of natural numbers we could define a property not_zero as follows definition not_zero nat Prop An nat match n with 0 gt False S p gt True The possibility of defining predicates by structural recursion on terms is one of the major characteristics of the Cal
168. y a fullstop and finally by the body term We use list1 instead of listo since we expect to have at least one identifier conversely you should use listo when the list can possibly be empty The default meta operator at content level matches the presentational opt and has two branches which are chosen depending on the matching of the optional subexpression Let us consider the first case where we have an explicit type The content term is built by folding the function rec acc exists A ident xz T acc rec is the binder acc the bound variable and the rest is the body over the initial content expression Pz When a notation is not a simple infix operator it may be the case that a different precedence is required for its arguments In this case we can use the term n X syntax to declare that the term matched by the variable X needs to be parsed or pretty printed at precedence n For example knowing that conjunction has precedence 35 by requiring Pz to be parsed at level 19 in the notation of the existential an expression like 4z P will be parsed as 32 PA Q whereas it would be parsed as dz P A Q if Px was required to be at any level greater than 35 The maximal level of precedence is 90 By asking an argument to have precedence 90 we force the argument to be always either a single identifier or to be delimited e g by parentheses The user is invited to consult basics core_notation ma for more examples of declarat
169. y a semicolon In this case the pattern is just the name of the hypothesis and we should write normalize in H At this point the first subgoal looks like the following n nat q nat r bool H 0 false q r O add nat_of_bool r twice q Journal of Formalized Reasoning Vol 7 No 2 2014 114 A Asperti and W Ricciotti and C Sacerdoti Coen From the hypothesis H we expect to be able to conclude that q 0 and r false The tactic that provides this functionality is called destruct The tactic decomposes every hypothesis that is an equality between structured terms into smaller compo nents if an absurd situation is recognized like an equality between 0 and S n built from different constructors the current goal is automatically closed other wise all derived equations where one of the sides is a variable are automatically substituted in the proof and the remaining equations are added to the context re placing the original equation The tactic considers the two sides to be structured if they are the application of constructors and skips equalities involving at least one function application e g f n S m unless the other side is a variable e g f n m handled by substituting f n for m everywhere In the above case by invoking destruct we would get the two equations q 0 and r false these are immediately substituted in the goal that becomes n nat nat bool 3R O add nat_of_bool false twice
170. you received as input Most mathematical functions can be naturally defined in this way For instance the sum of two natural numbers can be defined as follows let rec add n m match n with 0 gt m Sa gt S add a m i Observe that the definition of a recursive function requires the keyword let rec instead of definition The specification of formal parameters is different too In this case they come before the body and do not require a A If you need to specify the type of some argument you need to enclose it in parentheses e g n nat By convention recursion is supposed to operate on the first argument that means that this is the only argument that is supposed to decrease in the recursive calls In case you need to work on a different argument say foo you can specify it by explicitly mentioning on foo just after the declaration of all parameters 2 1 Elimination As we remarked at the end of the previous section the function add works by recursion on the first argument This means that for instance add O x will reduce to x as expected but the computation of add x 0 is stuck How can we prove that for a generic z add z O 2 The mathematical tool to do this is called induction The induction principle for natural numbers states that given a property P n if we prove P O and prove that for any m P m implies P S m then we can conclude P n for any n The elim tactic allows us to apply
171. ypes and programs and then prove properties about them Very few things are built in not even booleans or logical connectives but you may of course freely include and reuse libraries as in normal programming languages The main philosophy of the system is to let you define your own data types and functions using a powerful computational mechanism based on the declaration of inductive types Let us start this tutorial with a simple example based on the following well known problem 1 1 The goat the wolf and the cabbage A farmer needs to transfer a goat a wolf and a head of cabbage across a river but there is only one place available on his boat Furthermore the goat will eat the cabbage if they are left alone on the same bank and similarly the wolf will eat the goat The problem consists in bringing all three items safely across the river Let us start with including the file logic ma that contains a few preliminary notions not worth discussing for the moment As a general practice it is advisable to always include basics pts ma that contains the declaration of universes or at least to include basics core_notation ma for some basic notations The former includes the latter and every file from the standard library recursively includes both include basics logic ma Our first data type defines the two banks of the river which will be named east and west It is a simple example of enumerated type defined by explicitly declari

Matita Tutorial - Dipartimento di Informatica

Contents

Download Pdf Manuals

Related Search

Related Contents