(**************************************)
(* I. FIRST LINES: QUERIES. *)
(**************************************)
(* By default, some libraries are loaded at start. *)
(* Hit ctrl-down to start coq and got one step. Look at
the answer on the right panel. You can see that nat is
of type Set. *)
Check nat.
About nat.
(* SYNTAX: ALL COMMANDS END WITH A PERIOD. *)
(* Hit ctrl-down again on these second query, you can see that
nat can also be seen as of type Type. The "id:T" syntax
forces the type of id to T but T has to be equal (convertible)
to the type registered for id. *)
Check (nat:Type).
(* This command fails (Fail allows to ignore the error). *)
Fail Check (nat:Prop).
(* You can hit ctrl-up to go back one step *)
(* ctrl-down once more: Print shows the definition of a constant.
Here we can see that nat is the type of natural numbers à la Peano.*)
Print nat.
(* Notice that
1) Check allows to print the type of an expression
1) Print allows to print the definition of an constant
2) These queries are not really meant to be written in a file, it
is better to use "Queries" menus and/or keyboard shortcut
instead. Shortcuts are displayed in menus.
Default shortcut for Check is ctrl-shft-C, it operates
on the selected text.
Try selecting the following word:
Nat.eqb
and hit Check and Print. *)
(* Hit ctrl-down again to see the type of the "3" notation. *)
Check 3.
(* For more complex queries you can display a dedicated query
window with F1 (menu View/query pane).
A query worth noticing is "Search", that accepts several arguments and displays all
definitions involving all arguments.
For instance, in the query pane, select "Search" and type exactly "eq Z.le 0 1"
to see the definitions involving these 4 constants. *)
(**************************************)
(* II. NOTATIONS AND SCOPES *)
(**************************************)
(* Now we load the library about arithmetic over the set Z: *)
Require Import ZArith.
(* Let us open a new notation for numbers. *)
Open Scope Z_scope.
(* Notice how the same notation than before now
corresponds to another type. *)
Check 3.
(* The other notation has not disappeard, it is just not the
default one, to use it again just put %nat at the end. *)
Check 3%nat.
(* Likewise: *)
Check (3+5).
Check (3+5)%nat.
(* You can perform the two following lines in one shot by putting
cursor below them and hit ctrl-right. *)
Check (Nat.add 0 1).
Check (Z.add 0 1).
(* The same shortcut allows to go backward too: put
the cursor above Nat.add and hit ctrl-right again. *)
(* Note that all queries depend on which libraries have been loaded
and which definitions have been processed currently.
Unprocess backward until backtracking the line "Require ... ZArith."
and perform the same queries, you will notice the difference. *)
(* Let us close the Z notations for now*)
Close Scope Z_scope.
(**************************************)
(* III. FUNCTIONS AND EVALUATIONS *)
(**************************************)
(* Printing a functions displays its definition, i.e. its code. *)
Print Nat.add.
(* Notice the "fix" construction which defines a recursive function,
we will comme back to that later. *)
(* Functions can compute, use "Eval compute in e." to the
computation (reduction) of expression e:*)
Time Eval compute in (Z.mul 1000 1000).
(* Computation over nat is very slow and may raise stack overflows,
due to Peano's definition that is computably inefficient. *)
Time Eval compute in (Nat.mul 1000 50).
(* HIT THE RED BUTTON ABOVE IF coqide gets stuck, then
go back one line and comment this line to go further.*)
(* Try selecting a function name above and hit
ctrl-shft-c (for check), and ctrl-shft-k for
searching all definitions about it in the
current environment. *)
(* There is a mechanism for extracing Coq definition into ocaml ones:*)
Recursive Extraction Nat.add.
(* or in Haskell ones *)
Extraction Language Haskell.
Recursive Extraction Nat.add.
(* or in scheme ones*)
Extraction Language Scheme.
Recursive Extraction Nat.add.
(* Let us write our first function: *)
Definition f x := x + 1.
Print f.
Check f.
Eval compute in (f 4).
(* An example of the if construct *)
Check (if true then 1 else 2).
Eval compute in (if true then 1 else 2).
(************ EXERCISE *************)
(* EXERCISE: Define function g, taking 2 nat parameters and returning their sum.
Test it with "Eval compute" with 2 sets of arguments. *)
(***********************************)
(************ EXERCISE *************)
(* EXERCISE: Define a function (with no pattern matching) with one
nat arguments x that returns true if x is equal to 1 and false
otherwise. NOTE: Look in the standard library for the constant
function performing boolean equality test over nat by the following
query: [Search bool nat "eq"], ("eq" is a pattern that must be
matched by the constant name). *)
(***********************************)
(* Let us define a function with a pattern matching. *)
Definition eq_0 (n:nat):bool :=
match n with
| O => true
| S _ => false
end.
Eval compute in (eq_0 0).
Eval compute in (eq_0 3).
Eval compute in (eq_0 (S (S (S O)))).
(* Notice that like in most functional programming languages the
type annotations are not necessary. You can replace the first line
of the definition by:
Definition eq_0 n :=
*)
(* Now we define a recursive function, introduced by the
keyword Fixpoint. Let us redefine the equality test over
nat by ourselves:*)
Fixpoint my_eqb n m :=
match n,m with
| O,O => true
| S n', S m' => my_eqb n' m'
| _ , _ => false
end.
(* Notice the message "(decreasing on 1st argument)". One of the
arguments must be such that recursive calls are all done on a
structurally smaller value for this argument. Here the first
and the second are OK. Replace the first line by:
Fixpoint my_eqb n m {struct m} :=
*)
(************ EXERCISE *************)
(* EXERCISE: define the function my_leb that takes 2 parameters
n and m and returns true if n is smaller than or equal to m,
and false otherwise. You must define this function recursively *)
(***********************************)
(* Lists are a classical example of inductive types. *)
Require Import List.
Print list.
Check (cons 2 (cons 0 nil)).
(* Standard notations allow to use infox :: for con, that can
be used in pattern matching.*)
Check (1::2::3::4::nil).
Check (match (cons 4 :: nil) with
| nil => false
| x::l => true
end).
(* This adds another notation for lists *)
Import ListNotations.
Check [1;2;3;4].
Require Import List.
Import ListNotations.
(* LISTS. Use a query to see the definition of type list as an
inductive type. *)
(* Like nat, list is defined with two constructors. *)
About nil.
About cons.
(* See how notations correspond to constructors:*)
Check (cons 1 nil).
Check (cons true (cons false nil)).
Check [1].
Check [true;false].
(************ EXERCISE *************)
(* EXERCISE: define the function my_length that computes
the length (nat) of a list. Try to make this function polymorphic
in the type of the elements of the list. *)
(***********************************)
(************ EXERCISE *************)
(* EXERCISE: define the function mem which takes a list of nat
l and a nat n and returns true iff n belongs to l. *)
(***********************************)
(************ EXERCISE *************)
(* EXERCISE: define the function mem which takes a type T, a boolean equality function eqb and, a list of T
l and a t of type T n and returns true iff n belongs to l. *)
(* Help: here is the first line: *)
(*Fixpoint mem (T:Type) (eqb:T -> T -> bool) (l:list T) (n:T) {struct l}: bool := *)
(*and here are some tests:*)
(*
Eval compute in (mem _ Nat.eqb [4;5;6;7] 3).
Eval compute in (mem _ Nat.eqb [4;5;6;7] 4).
Eval compute in (mem _ Bool.eqb [true;true;true;false] false).
Eval compute in (mem _ Bool.eqb [true;true;true;true] false).
*)
(* If you want you can write other examples. You can find other boolean
comparison functions with this query: *)
SearchPattern (?X -> ?X -> bool).
(* Note: if we use type classes and register Nat.eqb and Bool.eqb correctly it is
possible to have Coq guess them automatically. Pactole uses this kind of mechanism.*)
(***********************************)
(* Defining properties *)
(* Look a possible definition of the property "being a element of a
list". Notice that A is implicit in Belongs and also in B_found and
B_next. *)
Inductive Belongs {A:Type} : A -> list A -> Prop :=
B_found: forall (a:A)(l:list A), Belongs a (a::l)
| B_next: forall (a b:A)(l:list A), Belongs a l -> Belongs a (b::l).
Definition belong1 := B_next _ 3 _ (B_found 1 (2::nil)).
(* Check the type of this term: *)
Check belong1.
(* Print shows all explicit arguments *)
Print belong1.
(************ EXERCISE *************)
(* Can you build a term of type Belongs 3 [3; 1; 2] *)
(* Definition belongs3: ??. *)
(***********************************)
(************ EXERCISE *************)
(* Can you build a term of type Belongs 2 [3; 1; 2] *)
(* Definition belongs2: ??. *)
(* We can do it the other way around: let us declare that we want to
build a term of type Belongs 4 [3; 1; 4; 2]. Notice the use of the
"apply" tactic. *)
Lemma belongs4: Belongs 4 [3; 1; 4; 2].
Proof. (* Starts the proof. *)
apply B_next.
(* Show Proof. *)(* uncomment this to see the partial term built until now *)
apply B_next.
(* Show Proof. *)(* uncomment this to see the partial term built until now *)
apply B_found.
Qed. (* Ends the proof *)
Print belongs4.
(***********************************)
(************ EXERCISE *************)
(* Define an inductive property "there is a member >= 12 in this list." *)
Inductive Exists_greater12 : list nat -> Prop :=
(* | EG_found: *)
(* | EG_next: ? *)
.
(* Prove this. Note: you can use "do tactic." to repeat tactic
times, and "auto" solves easy inequalities. You still need
apply like in the proof of belongs4. *)
Lemma ex1 : Exists_greater12 (3::4::5::12::1::2::nil).
Proof.
(* PROVE HERE *)
Admitted. (* Replace this by Qed once the proof is finished. *)
(***********************************)
(************ EXAMPLE OF A MORE COMPLEX PROOF *************)
(* This tutorial is not about proving things, only about specifying,
but let us see a proof by induction anyway. *)
(* Proof that if l contains a element >= 12 then so does l++l', for
any l'. *)
Lemma ex2: forall l l',
Exists_greater12 l ->
Exists_greater12 (l++l').
Proof.
intros l l' h.
induction h;cbn.
(* Once Exists_greater12 is defined above, this should give 2
subgoals. You can solve them by applying constructors + auto. *)
Admitted.
(***********************************)
(***********************************)
(* IV. DEFINING OUR OWN TYPES *)
(***********************************)
(* Suppose now we want to formalize the behaviour of a set of three
normal robot and 2 byzantine robots. We can first define the two
types of robot names. *)
Inductive GoodRobot: Type :=
| gr1: GoodRobot
| gr2: GoodRobot
| gr3: GoodRobot.
Inductive ByzRobot: Type :=
| br1: ByzRobot
| br2: ByzRobot.
(* Now we need to specialize the type identifier. Since we will
explore another solution after this one, we define the first one in
a module. Once closed all definitions inside this module will be
accessible only by putting the prefix "NoClass." *)
Module NoClass.
(* We define the type of all robot as the union two types of robots. *)
Inductive ident G B: Type :=
| Good: G -> ident G B
| Byz: B -> ident G B.
(* Let us define some robots from our two dedictated robot types: *)
Definition r1'' := Good GoodRobot ByzRobot gr2.
Definition r1''' := Byz GoodRobot ByzRobot br1.
(************ EXERCISE *************)
(* Define the boolean equality function on type (ident GoodRobot
ByzRobot). You can start by defining the equality functions over
GoodRobot and ByzRobot. *)
Definition robot_eq (r1 r2: ident GoodRobot ByzRobot) : bool :=
match r1,r2 with
(* FINISH HERE *)
| _,_ => false
end.
(* Some exemple of comutation with this function. *)
Eval compute in (robot_eq (Good GoodRobot ByzRobot gr2) (Good GoodRobot ByzRobot gr2)).
Eval compute in (robot_eq (Good GoodRobot ByzRobot gr2) (Good GoodRobot ByzRobot gr1)).
Eval compute in (robot_eq (Byz GoodRobot ByzRobot br1) (Good GoodRobot ByzRobot gr1)).
Eval compute in (robot_eq (Byz GoodRobot ByzRobot br1) (Byz GoodRobot ByzRobot br1)).
(* Note that putting the detailed type parameters is tedious.
See the following on this problem.*)
(***********************************)
(* When the models get more complex, giving all parameters everywhere
becomes really impracticable. For instnace the current pactole
models have about 14 parameters!
We need a way to make parameters implicit. We can make arguments
implicit like this: *)
Global Arguments ident {_} {_}. (* curly brace means implicit *)
Global Arguments Good {_} {_}.
Global Arguments Byz {_} {_}.
(* But coq cannot guess all arguments, by lack of information *)
Fail Definition g1 := Good 2. (* B cannot be guessed *)
Fail Definition b1 := Byz true. (* G cannot be guessed *)
(* We still have to put parameters somewhere. Either in the type: *)
Definition g1: @ident nat bool := Good 2. (* B is guessed once given somewhere *)
Definition b2: @ident nat bool := Byz false.
(* Or in the term: *)
Definition g1' := @Good nat nat 2.
Definition b2' := @Byz bool bool false.
End NoClass.
(* This is not satisfying and won't scale if we do not get rid of
implicits. TYPE CLASSES allow to register some types to instantiate
automatically parameters of other types. In the following we
redefine the type of robot's ids using type classes. *)
(************** TYPE CLASSES ************** *)
(* Here we describe a simplified version of pactole's infrastructure
for Robots identifiers and sets. *)
(* Let us have a class (i.e. a type) packaging the informations we
want to know about the type of robots. Here, only the two types G
and B (in pactole much more: number of robots, a decidable equality
on it etc). *)
Class Names := {
G : Type;
B : Type;
}.
(* The idea is that we can declare an "instance" of this class
(preferably one declared at any time) and then this instance will
be used to solve implicit arguments. This is coq's equivalent of
"In this section each we talk about a robots we mean ......". *)
(* This needs to be done locally so that we can instantiate something
else later in the same coq session. So we start a section or a
module. *)
Section Robot3Good2Byz.
(* First we need to parameteriz things with class Names. *)
(* Note the effect of curly braces here: H is an implicit arguments
(to be solved by typing or by an class instance). Besides H is also
used for solving implicits inside this definition. *)
Inductive ident {H:Names}: Type :=
| Good: G -> ident (* !!! Here G is recognized as (@G H) declared *)
| Byz: B -> ident. (* !!! Here B is recognized as (@B H) declared *)
(* CHECK the View/display implicit arguments for the next Print. *)
Print ident.
(* See? the implicit arg of G has been instantiated by H. *)
(* un check the option*)
(* For now we don't have an instance of Hnames so implicit arguments
cannot be solved: *)
Check G.
Check Good.
(* Now let us declare an instnace of Hnames. "Instance" is like
Definition but Coq will use this definition to guess implicit
arguments later. *)
Instance MyRobots : Names := {| G:=GoodRobot ; B:= ByzRobot |}.
(* Now the implicit arguments of type Hnames are instantiated by
MyRobots. *)
Check G.
Check Good.
(* Which is the same as: *)
Check (@G MyRobots).
(************ EXERCISE *************)
(* Let us show that there are only 5 robots. You can use tactic
"destruct ." Where is the name of a variable or hypothesis
of which you want to consider each cases. "auto" can solve trivial
disjunctions (i.e. where one of the disjuncts is trivial). *)
Lemma foo: forall robot:ident,
robot = Good gr1 \/ robot = Good gr2 \/ robot = Good gr3
\/ robot = Byz br1 \/ robot = Byz br2.
Proof.
intros robot. (* let robot be any robot *)
(* try "destruct robot." for a start and try to finish. *)
Admitted. (* replace by "Qed." when proof is finished. *)
(***********************************)
End Robot3Good2Byz.
Require Streams.
(* Streams are infinite lists of the form (Cons x (Cons y ... )) *)
Print Streams.Stream.
(* Defining a stream needs a cofixpoint: *)
CoFixpoint oneforever : Streams.Stream nat :=
Streams.Cons 1 oneforever.
Print oneforever.
(* Coinductive are unfolfded lazily: *)
Eval compute in oneforever.
(* TO AVOID WRITING "Streams." EVERYWHERE we do: *)
Import Streams.
(* Unfolding is triggered by "match", which is the only way of looking
at the first element. *)
Eval compute in (match oneforever with
| Cons a l => Cons a l
end).
Eval compute in (match oneforever with
| Cons a l => Cons a (Cons a l)
end).
(************ EXERCISE *************)
(* Prove this unfolding equality. You will need to reason by case on x
by using "destruct x." tactic. "auto" generally discharges easy
goals. *)
Lemma unfold_stream: forall (A : Type) (x : Stream A), x = match x with
| Cons a s => Cons a s
end.
Proof.
(* PROVE HERE *)
Admitted.
(* This lemme actually already exists in coq's library: *)
Check unfold_Stream.
(***********************************)
(* Then we can prove things like that, where EqSt is the bisimilarity on streams: *)
Lemma unfold_streamone: EqSt oneforever (Cons 1 oneforever).
Proof.
cofix.
rewrite unfold_Stream at 1.
simpl.
apply EqSt_reflex.
Qed.
(* Function Streams.hd allows to extract the first element of a stream. *)
Print Streams.hd.
(* Function Streams.tl allows to extract the tail of a stream. *)
Print Streams.tl.
(* And one can prove another unfolding lemma. *)
Lemma unfold_stream': forall A (s:Stream A),
EqSt s (Cons (hd s) (tl s)).
Proof.
constructor;cbn.
- reflexivity.
- apply EqSt_reflex.
Qed.
(* Some well known connectors over streams are defined in coq's
library, and pactole makes heavy use of them. Take some time
reading and understanding them. They take a stream and a predicate
on streams as parameters. *)
Print Streams.Exists.
Print Streams.ForAll.
(************ EXERCISE *************)
(* Define the property of a stream of "containing 42 somewhere". Using
Streams.hd is advised. *)
Definition fourtytwo_somewhere (s:Stream nat) :=
False. (* REPLACE BY DEFINITION HERE *)
(* Let us see if we can prove thie property on these two streams *)
CoFixpoint ftforever : Streams.Stream nat :=
Streams.Cons 42 oneforever.
Definition ftforeverafter3steps : Streams.Stream nat :=
(Cons 1 (Cons 2 (Cons 54 ftforever))).
Lemma streams1 : fourtytwo_somewhere ftforever.
Proof.
Admitted. (*replace by the above when fourtytwo_somewhere is defined above.*)
(* apply Here.
auto.
Qed.*)
(************ EXERCISE *************)
(* Prove this: *)
Lemma streams2 : fourtytwo_somewhere ftforeverafter3steps.
Proof.
(* PROVE HERE *)
Admitted. (* replace by "Qed." when proved *)
(* ********************************* *)
(************ EXERCISE *************)
(* Define the property of a stream of "after any number of elements,
there is still 42 somewhere". *)
Definition fourtytwo_somewhere_always (s:Stream nat) :=
False. (* REPLACE BY DEFINITION HERE *)
(* ********************************* *)
(************ EXERCISE *************)
(* Define the property of a stream of "all elements are equals". *)
Definition always_alleq (s:Stream nat) :=
False. (* REPLACE BY DEFINITION HERE *)
(************ EXERCISE *************)
(* Define the property of a stream of "after some number of elements,
all elements are equals". *)
Definition always_alleq_somewhere (s:Stream nat) :=
False. (* REPLACE BY DEFINITION HERE *)
(* ********************************* *)
(* ********************************* *)
(* One last thing about Reals in Coq. *)
(* Suppose the robot move on a line, we want to associate to each id a
position on the line. *)
Require Import Reals.
Definition position := R.
Definition configuration := R.
(* Contrary to integers or boolean, Reals are axiomatized in Coq
standard library, you can ask coq which axioms have been used to
define some results on reals you are: *)
Print Assumptions CV_Cauchy.
(* So in coq one can only reason about R, not compute. *)