-(*
-Data types, functions and theorems
+(****************** Data types, functions and theorems ************************)
-Matita is both a programming language and a theorem proving environment:
-you define datatypes and programs, and then prove properties on them.
-Very few things are built-in: not even booleans or logical connectives
-(but you may of course use 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.
+(* Matita is both a programming language and a theorem proving environment: you
+define datatypes and programs, and then prove properties on them.
+Very few things are built-in: not even booleans or logical connectives (but you
+may of course use 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.
+known problem: the goat, the wolf and the cabbage.
-The goat, the wolf and the cabbage
A farmer need to transfer a goat, a wolf and a 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
include "basics/logic.ma".
-inductive bank: Type[0] ≝
+inductive bank: Type[0] ≝
| east : bank
| west : bank.
-(* We can now define a simple function computing, for each bank of the river, the
+(* 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). We have
+basically two sorts in Matita: "Prop" and "Type". "Prop" is meant for logical
+propositions, while "Type" should be used for dataypes (we shall tell more about
+the attribute $0$ in a later Section).
+
+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 keyword | (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 declaration of a constructor c for and inductive type T has the
+following typical shape:
+ A1 → … → An → T
+where A1 … A_n can be arbitrary types, comprising T itself. Not every form of
+recursive constructors is accepted however: in order to ensure logical
+consistency, we must respect some positivity conditions, that we shall discuss
+in Section ??.
+
+As a general rule, the inductive type must be conceptually understood as the
+smallest collection of terms freely generated by its constructors. *)
+
+(********************************* functions **********************************)
+
+(* We define a first simple function computing, for each bank of the river, the
opposite one. *)
definition opposite ≝ λs.
| west ⇒ east
].
+(* Non recursive functions must be defined in Matita using the keyword
+"definition" followed by the name of the function. The type of the function is
+optional, since in many cases it can be 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 λ
+(\lambda); many latex-like macro are automatically converted by Matita into
+Unicode symbols: see \verb+View >Tex\UTF-8 table+ in the menu bar for a complete
+list.
+
+The definition proceeds 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.
+
+Pattern matching is a well known feature typical of functional programming
+(especially of the ML family), allowing simple access to the components of
+complex data structures. A function definition most often corresponds to pattern
+matching over 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
+ [ p1 => expr1
+ | p2 => expr1
+ :
+ | pn => exprn
+ ]
+
+The expression expr, that is supposed to be an element of an inductive type T,
+is matched sequentially to the various patterns p1, ..., pn. A pattern pi is
+just a constructor of the inductive type T possibly applied to a list of
+variables, bound inside the corresponding branch expri.
+If the pattern pi matches the value expr, then the corresponding branch expri is
+evaluated (after replacing in it the pattern variables with the corresponding
+subterms of expr).
+Usually, all expressions expr have a same, uniform type; since however Matita
+supports dependent types, the type of branches could depend on the matched
+expression, too. *)
+
+(******************************* A first lemma ********************************)
+
(* Functions are live entities, and can be actually computed. To check this, let
-us state the property that the opposite bank of east is west; every lemma needs a
-name for further reference, and we call it "east_to_west". *)
+us state the property that the opposite bank of east is west; every lemma needs
+a name for further reference, and we call it "east_to_west". *)
lemma east_to_west : opposite east = west.
In this case, we avoid the unnecessary simplification step: // will take care of
it. *)
-lemma west_to_east : opposite west = east.
+lemma west_to_east: opposite west = east.
// qed.
-(*
-Introduction
+(* 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. *)
+
+(********************************* Introduction *******************************)
-A slightly more complex problem consists in proving that opposite is idempotent *)
+(* A slightly more complex problem consists in proving that opposite is
+idempotent *)
lemma idempotent_opposite : ∀x. opposite (opposite x) = x.
the object of the case analysis (in our case, b).
*)
-cases b
+cases b
(* Executing the previous command has the effect of opening two subgoals,
corresponding to the two cases b=east and b=west: you may switch from one to the
// qed.
-(*
-Predicates
+(********************************** Predicates ********************************)
-Instead of working with functions, it is sometimes convenient to work with
+(*I nstead of working with functions, it is sometimes convenient to work with
predicates. For instance, instead of defining a function computing the opposite
bank, we could declare a predicate stating when two banks are opposite to each
other. Only two cases are possible, leading naturally to the following
(* 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 case, the two facts - ast_west and
-west_east.
+predicate defined by the two clauses - in this case, the two facts - ast_west
+and west_east.
Between opp and opposite we have the following relation:
opp a b iff a = opposite b
cases oppab // qed.
-(*
-Rewriting
+(******************************** Rewriting ***********************************)
-Let us come to the opposite direction. *)
+(* Let us come to the opposite direction. *)
lemma opposite_to_opp: ∀a,b. a = opposite b → opp a b.
cases b // qed.
-(*
-Records
+(******************************** Records *************************************)
-It is time to proceed with our formalization of the farmer's problem.
+(* 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 cabbage, and the boat. The simplest way to declare such a data type
is to use a record.
| one : ∀x,y.move x y → reachable x y
| more : ∀x,z,y. reachable x z → safe_state z → move z y → reachable x y.
-(*
-Automation
-
-Remarkably, Matita is now able to solve the problem by itslef, provided
-you allow automation to exploit more 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.
+(********************************* Automation *********************************)
+
+(* Remarkably, Matita is now able to solve the problem by itslef, provided you
+allow automation to exploit more 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.
+normalize /9/ qed.
-(*
-Application
+(********************************* Application ********************************)
-Let us now try to derive the proof in a more interactive way. Of course, we
+(* 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 property named foo is to write "@foo". In general, the philosophy
-of Matita is to describe each proof of a property P as a structured collection of
-objects involved in the proof, prefixed by simple modalities (#,<,@,...) explaining
-the way it is actually used (e.g. for introduction, rewriting, in an applicative
-step, and so on).
+application of a property named foo is to write "@foo". In general, the
+philosophy of Matita is to describe each proof of a property P as a structured
+collection of objects involved in the proof, prefixed by simple modalities (#,<,
+@,...) explaining the way it is actually used (e.g. for introduction, rewriting,
+in an applicative step, and so on).
*)
lemma problem1: reachable start end.
normalize @more
-(*
-Focusing
+(********************************* Focusing ***********************************)
-After performing the previous application, we have four open subgoals:
+(* After performing the previous application, we have four open subgoals:
X : STATE
Y : reachable [east,east,east,east] X
Let us see the effect of the "[" on our proof:
*)
- [
-
+ [
+
(* As you see, only the first goal has now the focus on. Moreover, all goals got
a progressive numerical label, to help designating them, if needed.
We can now proceed in several possible ways. The most straightforward way is to
| /2/ ]
-(*
-Implicit arguments
+(************************** Implicit arguments ********************************)
-Let us perform the next step, namely moving back the boat, in a sligtly
+(* Let us perform the next step, namely moving back the boat, in a sligtly
different way. The more operation expects as second argument the new
intermediate state, hence instead of applying more we can apply this term
-already instatated on the next intermediate state. As first argument, we
-type a question mark that stands for an implicit argument to be guessed by
-the system. *)
+already instatated on the next intermediate state. As first argument, we type a
+question mark that stands for an implicit argument to be guessed by the system.
+*)
@(more ? (mk_state east west west west))
projects / helm.git / commitdiff