(**************************************) (* 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 (after implicit parameters resolution). 2) About shows the type of a constant (before implicit parameter resolution and some other information. 3) Print allows to print the definition of an constant 4) 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). This window can be detached with the dedicated button. *) (* A query worth noticing is "Search", that accepts several arguments and displays all definitions involving all these arguments. For instance, in the query pane, select "Search" and type exactly "eq nat 0" to see the definitions involving these 3 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:*) Require Import Extraction. 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. About 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. Test the function on some values. *) (***********************************) (* Lists are a classical example of inductive types. *) Require Import List. Print list. (* Notice that the first argument of cons and nil is implicit. *) About cons. About nil. (* Thus we omit it and give only the second and third arguments *) Check (cons 2 (cons 0 nil)). (* Standard notations allow to use infix :: for cons, 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]. (************ 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. You will need to use a function testing equality over nat. You can use the previously defined function or search the standard one with the following search query: Search nat bool. or better: SearchPattern (nat -> nat -> bool). *) (***********************************) (************ EXERCISE *************) (* EXERCISE: define the function mem which takes a type T, a boolean equality function over T and, a list l of T and a t of type T 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 *) (* A possible definition of the property "being a element of a list". Notice that A is implicit (that is what curly brackets { } mean below) 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 1 3 [1; 2] (B_found 1 [2]). (* Redundant parameters can be guessed by Coq:*) Definition belong2 := B_next _ 3 _ (B_found 1 (2::nil)). (* Check the type of this term: *) Check belong1. Check belong2. (* Print shows all explicit arguments *) Print belong1. Print belong2. (************ 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 *************) (* Let us see a proof by induction anyway. *) (* Proof that if l contains a element >= 12 then so does l++l', for any l'. This is done BY INDUCTION ON THE PROOF OF "l contains a element >= 12". See how this makes thing relatively easy (arguably easier than on paper actually). *) 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. (* Let us start with the Imp semantics from B. Piearce *) Inductive aexp : Type := | ANum (n : nat) | APlus (a1 a2 : aexp) | AMinus (a1 a2 : aexp) | AMult (a1 a2 : aexp). Inductive bexp : Type := | BTrue | BFalse | BEq (a1 a2 : aexp) | BLe (a1 a2 : aexp) | BNot (b : bexp) | BAnd (b1 b2 : bexp). Fixpoint aeval (a : aexp) : nat := match a with | ANum n => n | APlus a1 a2 => (aeval a1) + (aeval a2) | AMinus a1 a2 => (aeval a1) - (aeval a2) | AMult a1 a2 => (aeval a1) * (aeval a2) end. Example test_aeval1: aeval (APlus (ANum 2) (ANum 2)) = 4. Proof. (* Try this too: *) (* simpl. reflexivity. *) reflexivity. Qed. (** Similarly, evaluating a boolean expression yields a boolean. *) Fixpoint beval (b : bexp) : bool := match b with | BTrue => true | BFalse => false | BEq a1 a2 => (aeval a1) =? (aeval a2) | BLe a1 a2 => (aeval a1) <=? (aeval a2) | BNot b1 => negb (beval b1) | BAnd b1 b2 => andb (beval b1) (beval b2) end. (* Pour lister les notations utilisées: *) Locate "=?" . Locate "<=?" . (* Ou encore: 1) dans les menus de coqide décochez les notations, 2) puis faites: Print beval. *) (* ================================================================= *) (** ** Optimization *) (** We haven't defined very much yet, but we can already get some mileage out of the definitions. Suppose we define a function that takes an arithmetic expression and slightly simplifies it, changing every occurrence of [0 + e] (i.e., [(APlus (ANum 0) e]) into just [e]. *) Fixpoint optimize_0plus (a:aexp) : aexp := match a with | ANum n => ANum n | APlus (ANum 0) e2 => optimize_0plus e2 | APlus e1 e2 => APlus (optimize_0plus e1) (optimize_0plus e2) | AMinus e1 e2 => AMinus (optimize_0plus e1) (optimize_0plus e2) | AMult e1 e2 => AMult (optimize_0plus e1) (optimize_0plus e2) end. (** To make sure our optimization is doing the right thing we can test it on some examples and see if the output looks OK. *) Example test_optimize_0plus: optimize_0plus (APlus (ANum 2) (APlus (ANum 0) (APlus (ANum 0) (ANum 1)))) = APlus (ANum 2) (ANum 1). Proof. reflexivity. Qed. (** But if we want to be sure the optimization is correct -- i.e., that evaluating an optimized expression gives the same result as the original -- we should prove it. *) (* Avant de démarrer, regarder comment on peut enchainer des tactiques avec le point-virgule. *) Theorem optimize_0plus_sound: forall a, aeval (optimize_0plus a) = aeval a. Proof. (* TODO *) Admitted. (** **** Exercise: 3 stars, standard (optimize_0plus_b_sound) Since the [optimize_0plus] transformation doesn't change the value of [aexp]s, we should be able to apply it to all the [aexp]s that appear in a [bexp] without changing the [bexp]'s value. Write a function that performs this transformation on [bexp]s and prove it is sound. Use the tacticals we've just seen to make the proof as elegant as possible. *) Fixpoint optimize_0plus_b (b : bexp) : bexp (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted. Theorem optimize_0plus_b_sound : forall b, beval (optimize_0plus_b b) = beval b. Proof. (* FILL IN HERE *) Admitted. (** [] *) Require Import String. (* À partir d'ici nous démarrons le fichiers Imp.v dans "programing language foundations": Télécharger wget https://softwarefoundations.cis.upenn.edu/plf-current/plf.tgz tar xfz plf.tgz cd plf make -j 3 Imp.vo coqide Imp.v & Lisez les commentaires et faites les exercices à partir de la ligne suivante (envion ligne 930): (** * Expressions With Variables *) Il y sera question de map, decoercions et de notations avant d'entrer dans le vif, n'hésitez pas à poser des questions. N'oubliez pas: demander le type d'une constante: About foo. Demander les théorème à propos d'une ou plusieurs constantes: (* les théorème citant foo ET bar *) Search foo bar. (* exclure les théorème parlant de baroof: *) Search foo bar -baroof. (* exclure les théorèmes ayant "_eqb_" dans le nom: *) Search foo bar -"_eqb_". (* n'inclure que les théorèmes ayant "_eq_" dans le nom: *) Search foo bar "_eq_" -baroof -"_eqb_". *)