From 1513ecac25c14a837bdba6a9dcd2f55529b25479 Mon Sep 17 00:00:00 2001 From: grianneau <> Date: Tue, 13 Aug 2024 18:03:55 +0200 Subject: [PATCH 1/5] a tutorial draft about SSReflect tactics --- src/Tutorial_SSReflect_tactics.v | 871 +++++++++++++++++++++++++++++++ src/index.html | 7 + src/jscoq-agent.js | 2 +- src/package.json | 2 + 4 files changed, 881 insertions(+), 1 deletion(-) create mode 100644 src/Tutorial_SSReflect_tactics.v diff --git a/src/Tutorial_SSReflect_tactics.v b/src/Tutorial_SSReflect_tactics.v new file mode 100644 index 00000000..1d904e10 --- /dev/null +++ b/src/Tutorial_SSReflect_tactics.v @@ -0,0 +1,871 @@ +(** * Tutorial about SSReflect tactics + + *** Summary + In this tutorial, we introduce the main [SSReflect] tactics + with which one can do most reasoning steps. + After mastering this rather small set of tactics, + one should be able to write large parts of proof scripts and many complete proof scripts + from the proof scripts one is already able to write with vanilla Coq. + The main take-away is to understand intuitively what is the effect of each tactic on the proof state, + so that one have an overview of possible logical reasoning steps when in the proof mode + (within the kewwords [Proof] and [Qed]). + Small insecable steps are emphasised, however the examples can seem artificial + and the shown scripts do not necessarly meet coding conventions. + The code examples in this page serve only as memo-snippets + to remember how to achieve the main basic logical steps inside proof. + + [SSReflect] tactics are shipped with the standard Coq distribution. + The default proof mode is “Classic” and comes with the Ltac​ tactic language. + SSReflect tactics are made available after loading the SSReflect plugin. + + *** Table of content + + - 1. Introduction + - 2. SSReflect tactics + - 3. More SSReflect tactics + - 4. Exercices + + *** Prerequisites + - We assume known basic knowledge of Coq + + Installation: the SSReflect set of tactics is shipped with the Coq distribution. +*) + + + +(** ** 1. Introduction + + SSR means Small Scale Reflection, + which is a methodology that can been used in computer-assisted formalisation with Coq. + This methodology goes beyond just using SSRfeflect tactics and is not covered in this tutorial. + There is a benefit to using this set of tactics + since one can achieve most proof steps with a relatively small set of tactics + (even without using this methodology or the Mathematical Components Library). + + Let us start by importing SSReflect. +*) + +From Coq Require Import ssreflect. + +(* One may also need to uncomment the following two lines. *) +(* From Coq Require Import ssreflect ssrfun ssrbool. *) +(* Import ssreflect.SsrSyntax. *) + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +(** *** Some terminology + + During an interactive session with Coq, one should see three panels: + _ the source code, a .v file + _ the goal panel, which displays proof states (focused goals and local context of the current goal) + _ the answer panel. + + +*) + +(** ** 2. SSReflect tactics + The two main tactics are [rewrite] and [apply:]. + There are already a [rewrite] and [apply] tactics in vanilla Coq (before loading SSReflect). + The colon punctuation mark at the end of [apply:] distinguishes it + from the [apply] tactic from vanilla Coq. + After loading SSReflect, the default behaviour of [rewrite] is changed. + Both [rewrite] tactics are similar but they behave differently and have syntactic differences. +*) + +(** *** Moving things + +(a completely unrelated link, just a song in a movie: +https://www.youtube.com/watch?v=m1543Y2Em_k&pp=ygU6QnVybmluZyBMaWdodHMgLSBKb2UgU3RydW1tZXIgaW4gSSBIaXJlZCBhIENvbnRyYWN0IEtpbGxlcg%3D%3D ) + +We start by showing how to [move] things between the current goal and the context. +With [move=>] one can move the first assumption of the goal to the local context. +With [move:] one can move something from the local or global context to the first assumption +(also called "top"). +You are invited to execute the following example step-by-step +while looking at the goal panel. +Please not that the code showed below does not meet coding conventions. + +*) + +Goal forall (P Q : Prop), P -> Q. +Proof. +move=> P. +move=> Q. +move=> p. +Fail move: P. (* The command "move: P" should fail. *) +move: p. +move: Q. +move: P. +move: or_comm. (* moving something from the global context *) +Abort. + +(** *** Destructing + + The [move] tactic can be used in combination with destructing, whose syntax is [[]]. + Destructing can let one access values of a record, do a case analysis on an inductive type, + split a disjunction into subgoals. + If new goals are introduced just after destructing, they are separated by the pipe symbols [|] + within the brackets. + As a result, the number of pipe symbols is the number of subgoals minus one. + It is possible to use destructing within subgoals, subsubgoals and so on, + as in done with [[move=> [HQ | [HR | HS]]]]. + +*) + +Module Destructing. + +From mathcomp Require Import ssrbool ssrnat. +(* Tt is better to place all import commands at the beginning of the file, + contrary to what is done here. + Yeah, do what I say, not as I do xD *) + +Variables (T : Type) (P : T -> Prop) (y z : T). + +Goal (exists u : T, P u) -> y = z. +Proof. +move=> [x]. +Abort. + +Goal (exists u : T, P u) -> y = z. +Proof. +move=> [x Px]. +Abort. + +Record Pair : Set := mkPair + { n : nat + ; b : bool}. + +Lemma PairP (x : Pair) : n x <= n x + (b x). +Proof. +move: x. +move=> [n b]. +rewrite /=. +(* proof to be finished *) +Abort. + +Goal forall (Q R S : Prop), Q \/ R -> S. +Proof. +move=> Q R S. +move=> [HQ | HR]. +- admit. +- +Abort. + +Goal forall (Q R S U : Prop), Q \/ R \/ S -> U. +Proof. +move=> Q R S U. +move=> [HQ | HRS]. +- admit. +- move: HRS => [HR | HS]. + + admit. + + +Abort. + +(** + The previous script can be shortened into: +*) + +Goal forall (Q R S U : Prop), Q \/ R \/ S -> U. +Proof. +move=> Q R S U. +move=> [HQ | [HR | HS]]. +- admit. +- admit. +- +Abort. + + +End Destructing. + +(** *** Simplifying + + At any stage within a proof attempt, one may want to try to simplify the goal + with the tactic [rewrite /=], + which is a special case for the [rewrite] tactic. + The tactic [rewrite /=] does not fail, even if no simplification could be done. + + It is possible that simplifying does actually something but leads to a less readable term. + In this case, you would rather step back in order to keep the goal (and local context) readable. + It is also possible that it simplifies too much, + because simplification applies undesirably at several parts of the goal. + In this case, you may consider using patterns to guide the tactic + to simplify only some specific parts of the goal. + See *** for the use of patterns. + We will see that it is possible to combine moving with simplification attempt. + +*) + +Definition foo (b : bool) := match b with +| true => false +| false => true +end. + +Goal foo true = false. +Proof. +rewrite /=. +by []. +Qed. + +(** + + The tactic [by []] tries to kill the goal, otherwise it fails. + +*) + +(** *** Rewriting + + Rewriting is performed with the [rewrite] tactic. + Some use cases are presented below. + +*) + +(** **** Rewriting with equalities + +One of the use cases of the [rewrite] tactic is to rewrite the goal with a given an equality from the context. +Let's look at the following example. + +*) + +Goal forall (T : Type) (a b c : T) (H : a = b), a = c -> b = c. +Proof. +move=> T a b c H. (* it is possible to combine several [move] into one *) +rewrite H. (* rewrites with the equality H from left to right *) +by []. +Qed. + +(** + It is convenient to reason with the Coq builtin equality [=]. +*) + +(** + In this proof, the last two steps can be combined into a single one: [by rewrite H]. + If you want, you can try to rewrite from right to left instead. +*) + +Goal forall (T : Type) (a b c : T) (H : a = b), a = c -> b = c. +Proof. +move=> T a b c H. (* it is possible to combine several move into one *) +rewrite -H. (* rewrites with the equality H from right to left *) +by []. +Qed. + + +(** One can combine [rewrite] and partial application. + Let's look at the following example. +*) + +Module AnotherRewrite. + +(* it is better to import HB in order to display more nicely some messages *) +(* however it seems it is not available in jsCoq at the moment *) +(* From HB Require Import structures. *) +From mathcomp Require Import ssrbool ssralg ssrnum. + +(* Import GRing.Theory Num.Theory. *) +Local Open Scope ring_scope. + +Variable (R : numDomainType). + +Lemma add_leq_right (z x y : R) : (x <= y) = (x + z <= y + z). +Proof. +(* we are going to use this admitted lemma *) +(* proving this lemma can be left as an exercice once you are emore familiar with SSReflect tactics *) +(* and have started exploring the Mathematical Components Library. *) +Admitted. + +(** In the lemma [add_leq_right], please note that the argument [z] is in the first position. +*) + +Goal forall (x : R), x <= x. +Proof. +move=> x. +Fail rewrite add_leq_right. (* Coq cannot guess what x is *) +Check (add_leq_right x). +rewrite (add_leq_right x). (* uses the partial application of add_leq_right to x *) +Abort. + +End AnotherRewrite. + +(** *** Unfolding a definition. + + Unfolding a definition is done with [rewrite /the_definition_to_be_unfolded]. + +*) + +Definition secret : nat := 42. + +Goal secret = 41 + 1. +Proof. +rewrite /secret. +rewrite -/secret. (* folding back*) +by []. +Qed. + +(** *** The [apply:] tactic + +The [apply:] tactic tries to match the conclusion (and eventually some premisses) of the lemma +with the goal. +It lets one do backward reasoning. +Let's look at some examples. + +*) + +Goal forall (A B : Prop) (H : A-> B), B. +Proof. +move=> A B H. +apply: H. +Abort. + +Goal forall (A B C : Prop) (H : A -> B -> C), B -> C. +Proof. +move=> A B C H. +apply: H. (* the premise B has been included *) +Abort. + +(** *** Generalisation + +It is usually a valid logical step to strengthen the goal. +This is the case in the logic of Coq. +In other words, if one can prove more, then one can prove less. +Generalisation is a way to strengthen a statement by introducing one universal quantification. +Generalisation can be an essential step to prepare inductive reasoning, in order to get strong enough +inductive hypotheses (but not too strong, otherwise one gets stuck with unprovable base cases in the inductive reasoning). + +*) + +Module Generalisation. + +From mathcomp Require Import ssrbool ssralg ssrnum. +Local Open Scope ring_scope. + +Variable (R : numDomainType). + +Goal (4 + 1) ^+ 2 = 4 ^+ 2 + 4 *+ 2 + 1 :> R. +Proof. +move: 4. (* generalises over the term 4 *) +Abort. + +Goal 1 + 1 = 1 * 1 :> R. +Proof. +move: 1. (* generalises over all occurrences of 1 *) +Abort. + +Goal 1 + 1 = 1 * 1 :> R. +Proof. +move: {2}1. (* generalises the second occurrence of 1 *) +move=> x. +Abort. + +Goal 1 + 1 = 1 * 1 :> R. +Proof. +move: {2 4}1. (* generalises the second and the forth occurrence of 1 *) +move=> x. +Abort. + +Check list. + +Goal forall (T : Type) (l : list T) (C : Prop), C. +Proof. +move=> T l C. +(* imagine that we would like to make induction on the lentgh of l - which is a natural number- +not on the list l itself. *) +move: (eq_refl (length l)). (* this illustrates moving something from the global context to top *) +move: {2}(length l). (* generalises over the second occurrence only *) +move=> n. +Abort. + +End Generalisation. + + +(** *** Induction reasoning + + Let's say there is a value [v] of type [T] and there is an induction principle for the type [T]. + Induction reasoning on [v] consists in starting an induction reasoning exploiting this principle. + Case analysis can be seen as a special case of induction reasoning, + driven by the constructors + and where the induction hypotheses are not used. + + For a given inductive type, there may be several induction principles. + For instance, there are two induction principles for sequences in Mathematical Component Library. + Picking the induction principle impacts the proof effort. + + + Induction principles' names often contain the substring + "elim" in the Standard Library ("elim" which stands for "elimination") or + "ind" in the Mathematical Components Library. + + In the following examples, sequences from the Mathematical Components Library are used + instead of lists from the standard library. *) + +Module Range. + +From mathcomp Require Import ssrnat seq. + +Fixpoint range (a : nat) (n : nat) := match n with +| 0 => [::] +| m.+1 => a::(range (a.+1) m) +end. + +(* The following code is considered bad practise. *) +(* It is presented this way to ease playing it step-by-step *) +(* and identifying basic reasoning steps. *) +Goal forall (a : nat) (n : nat), size (range a n) = n. +Proof. +move=> a n. +move: a. +elim: n. (* starts induction on n *) +- (* base case *) + move=> n. + rewrite /=. + by []. +- (* inductive step *) + move=> n. + move=> IH. + move=> b. + rewrite /=. + rewrite IH. + by []. +Qed. +(* Les preuves n'ont pas d'odeur. *) + + +(* The previous script can be shortened to: *) + +Lemma size_range (a : nat) (n : nat) : size (range a n) = n. +Proof. +move: a; elim: n => // n IHn b /=. +by rewrite IHn. +Qed. + +(* The syntax [//] after [=>] in a [move] means: please rmove trivial goal. *) +(* In this example, Coq is able to kill the base case as a trivial goal. *) +(* As a result, only one goal remain after [//] and no pipe symbol is required. *) +(* Simplification and removing trivial goals can be combined with the syntax [//=]. *) + +End Range. + +Module InductionSequence. + +From mathcomp Require Import ssrnat seq. + +Variables (l m : seq nat). + +Goal size (l++m) = size l + size m. +Proof. +move: m. +elim: l=> // a l IH m /=. +by rewrite IH. +Qed. + +Check last_ind. + +(* The result [last_ind] is an alternative induction principle *) +(* that can be applied at the elimination step in the previous example. *) +(* Instead of using constructors *) +(* The syntax [elim/last_ind:] combines elimination with view application. *) +(* Starting from the same goal and applying the [last_ind] view: *) + +Goal size (l++m) = size l + size m. +Proof. +move: m. +elim/last_ind: l. (* elimination is done with the inductive principle last_ind *) +- by move=> m. +- move=> m a IH l. + rewrite size_rcons. + rewrite cat_rcons. + rewrite IH. + rewrite /=. + by rewrite addnS. +Qed. + + +End InductionSequence. + + +(** *** Congruence + + When it is required to prove an equality between two applications of the same function, + it suffices to prove that the corresponding arguments of both applications are equal. + For instance, in the following examples it is required to prove [op w x = op y z]. + This goal has the form of an equality with the same function applied in each member. + The first arguments are [w] on the left and [y] on the right. + The second arguments are [x] on the left and [z] on the right. + It is sufficient to prove that [w = y] and [x = z]. + +*) + +Section Congruence. + +Variables (T : Type) (op : T -> T -> T) (w x y z : T). + +Goal w = y -> x = z -> op w x = op y z. +Proof. +move=> eq_wy eq_xz. +congr op. +- exact: eq_wy. +- exact: eq_xz. +Qed. + +End Congruence. + +(** *** Forward reasoning + + From the point of view of proof engineering with Coq, + one generally prefers to work on the goal over working on the local context. + This proof style is used in the Mathematical Components Library and is orthogonal to SSReflect tactics. + One benefit of this style is to get failure earlier when the script gets broken, + and thus it is easier to fix it. Instead of working on the local context + (for instance by using [rewrite in] on an hypothesis in the local context) + it is preferable to work on it while it is still in the goal and before it is introduced to the local context. + This way, one avoids relying on the names of the introduced assumptions. + Pushing something to top might be changed without creating an error immediately, + leading to more difficulties to maintain the script. + This difficulty can be more apparent when reusing old code or code written by others. + + Still, one may want to use forward reasoning occasionally. + The main SSReflect forward reasoning tactic is [have:]. + +*) + +Goal False. +Proof. +have : 0 = 0. +- by []. +- move=> H. +Abort. + +Goal False. +Proof. +have H : 0 = 0. (* syntax to give a name to the introduced intermediate result *) +- by []. +- +Abort. + +(** *** Changing view + + Changing view is performed on the first assumption with the tactic [move/] + or on the conclusion with the tactic [apply/]. + It replaces it with a "different view". + The first asumption can be replaced by a weaker asumption + and the conclusion can be replaced by a stronger conclusion. + + With reflection results (with the [reflect] keyword) a proposition + can be replaced with an equivalent boolean and a boolean + can be replaced with an equivalent proposition. + This is part of the Small Scale Reflection methodology. + + Let's look at some examples. + +*) + +Module ChangingView. + +Variables (A B C D E : Prop). +Hypothesis (H : B -> C). + +Goal B -> D -> E. +Proof. +move/H. (* weakens B to C *) +Abort. + +Goal A -> C. +Proof. +move=> HA. +apply/H. (* strenghten C to B *) +move: HA. +Abort. + +(* + These examples also work with equivalence instead of implication. +*) + +Hypothesis (H' : B <-> C). + +Goal B -> D -> E. +Proof. +move/H'. (* weakens B to C *) +Abort. + +Goal A -> C. +Proof. +move=> HA. +apply/H'. (* strenghten C to B *) +move: HA. +Abort. + +End ChangingView. + +(* + We now show some examples of view changing with boolean reflection. + +*) + +Module BooleanReflection. +From mathcomp Require Import ssrbool ssrnat. + +Check minn_idPr. + +Variables (m n : nat) (P : Prop). + +Goal minn m n = n -> P. +Proof. +move/minn_idPr. +Abort. + +Goal n <= m-> P. +Proof. +move/minn_idPr. +Abort. + +Goal P -> minn m n = n. +Proof. +move=> H. +apply/minn_idPr. +Abort. + +Goal P -> n <= m. +Proof. +move=> H. +apply/minn_idPr. +Abort. + +End BooleanReflection. + +(* + One can combine changing view with moving things. +*) + +(** Rewriting pattern. *) + +(** + SSReflect offers rewrite patterns to guide Coq to select specific matches for a rewrite. + Otherwise the first match is selected, which is not necessarly the desired effect. + Please not that the match and the occurence are two different things. + A pattern has several matches - eventually none - and each match has one or multiple occurrences. + Let's look at examples. +*) + +Module RewritePatterns. + +From mathcomp Require Import ssrbool ssralg ssrnum. + +(* Import GRing.Theory Num.Theory. *) +Local Open Scope ring_scope. + +Variables (R : ringType) (a b c : R). +Hypothesis H : forall (x : R), x = c. + +Goal (a + b) * a + (a + b + a) * b = (b + b) * a + (a + b + b) * a * b. +Proof. +rewrite [LHS]H. (* rewrites the left-hand side of the equality *) +Abort. + +Goal (a + b) * a + (a + b + a) * b = (b + b) * a + (a + b + b) * a * b. +Proof. +rewrite [RHS]H. (* rewrites the right-hand side of the equality *) +Abort. + +Goal (a + b) * a + (a + b + a) * b = (b + b) * a + (a + b + b) * a * b. +Proof. +rewrite [a+b]H. (* rewrites the all occurrences of a+b with H *) +Abort. + +Goal (a + b) * a + (a + b + a) * b = (b + b) * a + (a + b + b) * a * b. +Proof. +rewrite [a+b in LHS]H. (* rewrites the all occurrences of a+b in the left-hand side *) +Abort. + +Goal (a + b) * a + (a + b + a) * b = (b + b) * a + (a + b + b) * a * b. +Proof. +rewrite {2}[a + b]H. (* rewrites the second occurrence of a+b with H *) +Abort. + +Goal (a + b) * a + (a + b + a) * b = (b + b) * a + (a + b + b) * a * b. +Proof. +rewrite [a + b + _]H. (* rewrites occurences of the first match of a + b + _ *) +Abort. + +Goal (a + b) * a + (a + b + a) * b = (b + b) * a + (a + b + b) * a * b. +Proof. +rewrite [X in X + b]H. (* the pattern X + b is matched against a + b then a is rewritten in occurences of a + b *) +Abort. + +(* The following examples shows that we can explicit a pattern +to the point that exactly one b is rewritten, +the one in the middle in the term a + b + b *) + +Goal (a + b) * a + (a + b + a) * b = (b + b) * a + (a + b + b) * a * b. +Proof. +rewrite [X in (_ + _)* _ + (_ + X + _)* _ * _]H. +Abort. + +End RewritePatterns. + +Module SomeMorePatterns. + +(* From HB Require Import structures. *) +From mathcomp Require Import ssrbool ssrnat order. + +Local Open Scope nat_scope. +Local Open Scope order_scope. + +Variables (a b c : nat). + +Hypothesis H : forall x, x = c. + +Goal (a + b) * a + (a + b + a) * b <= (b + b) * a + (a + b + b) * a * b. +Proof. +rewrite [leLHS]H. +Abort. + +Goal (a + b) * a + (a + b + a) * b < (b + b) * a + (a + b + b) * a * b. +Proof. +rewrite [ltRHS]H. +Abort. + +End SomeMorePatterns. + +(** ** 3. More SSReflect tactics +*) + +(** *** Case analysis + + Let's say there is a value [v] of type [T] where [T] is an inductive type + (an inductive type has a finite number of constructors). + Case analysis on [v] consists in examining how [v] is constructed, + which leads to one subgoal for each constructor. + +*) + +Goal forall (n : nat), n + n = n. +Proof. +move=> n. +case: n. +(* the goals is splitted into two goals *) +- rewrite /=. + by []. +- move=> n. + (* we get stuck here, because we are trying to prove something false *) +Abort. + +(** The previous script can be written more shortly as follows +*) + +Goal forall (n : nat), n + n = n. +Proof. +move=> n. +case: n=> [|n]. (* the pipe symbol '|' separates each subgoal *) +(* the goals is splitted into two goals *) +- by []. +- (* we get stuck here, because we are trying to prove something false *) +Abort. + +(** It is possible to combine moving (with [move =>]) + with simplification [/=] and removing trivial goals [//]. + In the following script, after the case analysis, the first goal is trivial and removed by [//]. + Thus, only one goal is remaining and [n] can be introduced without using the pipe symbol. +*) + +Goal forall (n : nat), n + n = n. +Proof. +move=> n. +case: n=> // n. +(* we get stuck here, because we are trying to prove something false *) +Abort. + +(** *** Specialising + + Conversely to strengthening the goal, one can always weaken assumptions. + In other words, if one can do with less then one can do with more. + One way to weaken an assumption is by specialising it. + In the following example, the assumption [forall y, P y] is specialised to [x], + which results in the asumption [P x]. + +*) + +Goal forall (T G : Type) (P : T -> Prop) (x : T), (forall y, P y) -> G. +Proof. +move=> T G P x. +move/(_ x). +Abort. + +(* + The same could have been achieved with partial application. +*) + +Goal forall (T G : Type) (P : T -> Prop) (x : T), (forall y, P y) -> G. +Proof. +move=> T G P x H. +move: (H x). +Abort. + +(** *** Setting a new definition (vanilla Coq) + +We remind here the [pose] tactic (that does not come from SSReflect) +which let one add a local definition to the current context. +It can be useful to see more clearly the goal and the local context. + +*) + +Goal 1 + 2 = (1 + 2) + (1 + 2). +Proof. +pose a := 1 + 2. +rewrite -/a. (* can see more clearly now *) +Abort. + +(** ** 4. Exercices +*) + +(** *** Exercice 1 + For this exercice, you may want to use the Coq tactic [split] + to break a cunjunction-goal into two goals. +*) + +Goal forall (P Q : Prop), P /\ Q -> Q /\ P. +Proof. +move=> P Q [HP HQ]. +split. +- exact: HQ. +- exact: HP. +Qed. + +(** *** Exercice 2 +*) + +Goal forall (P Q : Prop), P \/ Q -> Q \/ P. +Proof. +move=> P Q [HP | HQ]. +- right. + exact: HP. +- left. + exact: HQ. +Qed. + +(** *** Exercice 3 +*) + +Module Exercice3. + +From mathcomp Require Import ssrbool ssrnat div. + +Local Open Scope nat_scope. + +Lemma div2nSn (n : nat) : 2 %| n * n.+1. +Proof. by rewrite dvdn2 oddM /= andbN. Qed. + +End Exercice3. + +(** ** Where to go from here + + One may try to port one proof script from vanilla Coq to SSReflect and see the difference. + In addition to using SSReflect tactics, + one may start reusing some results from the Mathematical Components Library. + + Finally, one may get inspiration from the Mathematical Component Library for their own formalisation. + This includes Small Scale Reflection methodology and SSReflect coding conventions. + Some ingredients are boolean reflection, decidable structures + and hierarchy of structures (with Hierarchy Builder). + +*) diff --git a/src/index.html b/src/index.html index fe1a55b7..d2987214 100644 --- a/src/index.html +++ b/src/index.html @@ -30,6 +30,7 @@

About

Proof General, vim with CoqTail, vscode with vscoq).

+

Coq Tutorials

Equations tutorials

diff --git a/src/jscoq-agent.js b/src/jscoq-agent.js index 589a3700..630b87f6 100644 --- a/src/jscoq-agent.js +++ b/src/jscoq-agent.js @@ -36,7 +36,7 @@ var jscoq_opts = { // editor: { mode: { 'company-coq': true }, className: 'jscoq code-tight' }, editor: { className: 'jscoq code-tight' }, init_pkgs: ['init'], - all_pkgs: { '+': ['coq', 'equations'] }, + all_pkgs: { '+': ['coq', 'equations', 'elpi', 'mathcomp'] }, init_import: ['utf8'], implicit_libs: true }; diff --git a/src/package.json b/src/package.json index 47e2ef91..f1ce1809 100644 --- a/src/package.json +++ b/src/package.json @@ -3,6 +3,8 @@ "jscoq": "^0.17.1", "wacoq-deps": "^0.1.1", "@jscoq/equations": "^0.17.1", + "@jscoq/elpi": "^0.17.1", + "@jscoq/mathcomp": "^0.17.1", "http-server": "^14.1.0" } } From a3b6a8ef0d25cde24b088f46d27cb99880227513 Mon Sep 17 00:00:00 2001 From: grianneau <> Date: Mon, 19 Aug 2024 10:23:16 +0200 Subject: [PATCH 2/5] save --- src/Tutorial_SSReflect_tactics.v | 301 +++++++++++++++++++++++++------ 1 file changed, 249 insertions(+), 52 deletions(-) diff --git a/src/Tutorial_SSReflect_tactics.v b/src/Tutorial_SSReflect_tactics.v index 1d904e10..0fce804d 100644 --- a/src/Tutorial_SSReflect_tactics.v +++ b/src/Tutorial_SSReflect_tactics.v @@ -5,10 +5,10 @@ with which one can do most reasoning steps. After mastering this rather small set of tactics, one should be able to write large parts of proof scripts and many complete proof scripts - from the proof scripts one is already able to write with vanilla Coq. + from the scripts one is already able to write with vanilla Coq. The main take-away is to understand intuitively what is the effect of each tactic on the proof state, - so that one have an overview of possible logical reasoning steps when in the proof mode - (within the kewwords [Proof] and [Qed]). + so that one has an overview of possible logical reasoning steps when in the proof mode + (within the keywords [Proof] and [Qed]). Small insecable steps are emphasised, however the examples can seem artificial and the shown scripts do not necessarly meet coding conventions. The code examples in this page serve only as memo-snippets @@ -42,6 +42,16 @@ since one can achieve most proof steps with a relatively small set of tactics (even without using this methodology or the Mathematical Components Library). + Isolated basic reasoning steps are illustrated with examples. + It is about beeing aware of some basic valid reasoning steps that are available. + Performing a reasoning step + Technically, if there is no more goal remaining (just before [Qed]), + it might be still possible that the proof term + created by the proof script does not have the desired type. + The proof is definitively checked by the proof assistant after the command [Qed] has succeeded. + + In the section 3. More SSReflect tactics, one will find tactics that are not strictly necessary to know. + Let us start by importing SSReflect. *) @@ -58,13 +68,46 @@ Unset Printing Implicit Defensive. (** *** Some terminology During an interactive session with Coq, one should see three panels: - _ the source code, a .v file - _ the goal panel, which displays proof states (focused goals and local context of the current goal) - _ the answer panel. - + 1 the source code, a .v file + 2 the goal panel, which displays proof states. + A proof state consists in a collection of goals where a local context is attached to each goal. + The current goal is one of the goals of the collection (there may be only one). + The goal panel displays the focused goals (among which is the current goal) + and the local context of the current goal. + 3 the answer panel. + +*) +Goal forall (P Q R S : Prop), P -> (P -> Q) -> (Q -> R) -> (R -> S) -> S. +Proof. +move=> P Q R S HP impl_PQ. +(* now, the local context consists of P, Q, R, S, HP and impl_PQ *) +(* other things are available in the global context, for instance imp_iff_compat_r *) +Check imp_iff_compat_r. +(* the top assumption is Q -> R *) +(* the second and last assumption is R -> S *) +(* the conclusion is S *) +move=> impl_QR impl_RS. +apply: impl_RS. +apply: impl_QR. +exact: impl_PQ. +Qed. + +(** + The following code snippet provides an alternate proof script + for the same goal, + to illustrate chaining tactics with ';'. *) +Goal forall (P Q R S : Prop), P -> (P -> Q) -> (Q -> R) -> (R -> S) -> S. +Proof. +move=> P Q R S HP impl_PQ impl_QR impl_RS. +apply: impl_RS; apply: impl_QR. (* tactics can be chained with ; *) +exact: impl_PQ. +Qed. + + + (** ** 2. SSReflect tactics The two main tactics are [rewrite] and [apply:]. There are already a [rewrite] and [apply] tactics in vanilla Coq (before loading SSReflect). @@ -81,11 +124,12 @@ https://www.youtube.com/watch?v=m1543Y2Em_k&pp=ygU6QnVybmluZyBMaWdodHMgLSBKb2UgU We start by showing how to [move] things between the current goal and the context. With [move=>] one can move the first assumption of the goal to the local context. -With [move:] one can move something from the local or global context to the first assumption +In the opposite direction, +with [move:] one can move something from the local or global context to the first assumption (also called "top"). You are invited to execute the following example step-by-step while looking at the goal panel. -Please not that the code showed below does not meet coding conventions. +Please note that the code showed below does not meet coding conventions. *) @@ -94,7 +138,7 @@ Proof. move=> P. move=> Q. move=> p. -Fail move: P. (* The command "move: P" should fail. *) +Fail move: P. (* The command "move: P" should fail here. *) move: p. move: Q. move: P. @@ -117,7 +161,7 @@ Abort. Module Destructing. From mathcomp Require Import ssrbool ssrnat. -(* Tt is better to place all import commands at the beginning of the file, +(* It is better to place all import commands at the beginning of the file, contrary to what is done here. Yeah, do what I say, not as I do xD *) @@ -187,12 +231,12 @@ End Destructing. The tactic [rewrite /=] does not fail, even if no simplification could be done. It is possible that simplifying does actually something but leads to a less readable term. - In this case, you would rather step back in order to keep the goal (and local context) readable. + In this case, you would rather step back in order to keep the goal (or the local context) readable. It is also possible that it simplifies too much, because simplification applies undesirably at several parts of the goal. In this case, you may consider using patterns to guide the tactic to simplify only some specific parts of the goal. - See *** for the use of patterns. + See the section 'Rewriting pattern' for the use of patterns. We will see that it is possible to combine moving with simplification attempt. *) @@ -210,10 +254,21 @@ Qed. (** - The tactic [by []] tries to kill the goal, otherwise it fails. + The tactic [by []] tries to kill the goal - which is expected to be trivial for Coq - otherwise it fails. *) +Module NonTrivialCase. + +From mathcomp Require Import ssrbool ssrnat. + +Goal 2 * 3 = 3 + 3. +Proof. +by []. +Qed. + +End NonTrivialCase. + (** *** Rewriting Rewriting is performed with the [rewrite] tactic. @@ -223,14 +278,14 @@ Qed. (** **** Rewriting with equalities -One of the use cases of the [rewrite] tactic is to rewrite the goal with a given an equality from the context. +One of the use cases of the [rewrite] tactic is to rewrite the goal with a given equality from the context. Let's look at the following example. *) Goal forall (T : Type) (a b c : T) (H : a = b), a = c -> b = c. Proof. -move=> T a b c H. (* it is possible to combine several [move] into one *) +move=> T a b c H. (* it is possible to combine several [move] into a single one *) rewrite H. (* rewrites with the equality H from left to right *) by []. Qed. @@ -271,11 +326,11 @@ Variable (R : numDomainType). Lemma add_leq_right (z x y : R) : (x <= y) = (x + z <= y + z). Proof. (* we are going to use this admitted lemma *) -(* proving this lemma can be left as an exercice once you are emore familiar with SSReflect tactics *) +(* proving this lemma can be left as an exercice once you are more familiar with SSReflect tactics *) (* and have started exploring the Mathematical Components Library. *) Admitted. -(** In the lemma [add_leq_right], please note that the argument [z] is in the first position. +(** In the lemma [add_leq_right] just above, please note that the argument [z] is in the first position. *) Goal forall (x : R), x <= x. @@ -328,7 +383,7 @@ Abort. It is usually a valid logical step to strengthen the goal. This is the case in the logic of Coq. -In other words, if one can prove more, then one can prove less. +In other words, if one can prove more, then one can prove less (the current goal). Generalisation is a way to strengthen a statement by introducing one universal quantification. Generalisation can be an essential step to prepare inductive reasoning, in order to get strong enough inductive hypotheses (but not too strong, otherwise one gets stuck with unprovable base cases in the inductive reasoning). @@ -354,13 +409,13 @@ Abort. Goal 1 + 1 = 1 * 1 :> R. Proof. -move: {2}1. (* generalises the second occurrence of 1 *) +move: {2}1. (* generalises over the second occurrence of 1 *) move=> x. Abort. Goal 1 + 1 = 1 * 1 :> R. Proof. -move: {2 4}1. (* generalises the second and the forth occurrence of 1 *) +move: {2 4}1. (* generalises over the second and the forth occurrence of 1 *) move=> x. Abort. @@ -388,16 +443,25 @@ End Generalisation. and where the induction hypotheses are not used. For a given inductive type, there may be several induction principles. - For instance, there are two induction principles for sequences in Mathematical Component Library. + For instance, there are two induction principles for sequences in Mathematical Component Library + (sequences are the same as lists from the standard library). + + The default principle is based on the constructors. + There is one base case, when the sequence is empty. + There is one induction case, when the sequence is contructed with [cons]. + In this case, the induction hypothesis holds for the sequence-argument of [cons]. + An alternate induction principle for sequences is [last_ind]. + The base case is the same, and the inductive case + considers appending an element at the end of a sequence + (instead of the beginning). + Picking the induction principle impacts the proof effort. - Induction principles' names often contain the substring - "elim" in the Standard Library ("elim" which stands for "elimination") or - "ind" in the Mathematical Components Library. + "elim" (as in "elimination") in the Standard Library + or "ind" (as in "induction") in the Mathematical Components Library. - In the following examples, sequences from the Mathematical Components Library are used - instead of lists from the standard library. *) +*) Module Range. @@ -439,9 +503,9 @@ move: a; elim: n => // n IHn b /=. by rewrite IHn. Qed. -(* The syntax [//] after [=>] in a [move] means: please rmove trivial goal. *) +(* The syntax [//] after [=>] in a [move] means: please remove trivial goals. *) (* In this example, Coq is able to kill the base case as a trivial goal. *) -(* As a result, only one goal remain after [//] and no pipe symbol is required. *) +(* As a result, only one goal (out of two) remains after [//] and thus no pipe symbol is required. *) (* Simplification and removing trivial goals can be combined with the syntax [//=]. *) End Range. @@ -463,9 +527,9 @@ Check last_ind. (* The result [last_ind] is an alternative induction principle *) (* that can be applied at the elimination step in the previous example. *) -(* Instead of using constructors *) +(* Instead of using the default induction principle. *) (* The syntax [elim/last_ind:] combines elimination with view application. *) -(* Starting from the same goal and applying the [last_ind] view: *) +(* Starting again from the same goal and applying the [last_ind] view: *) Goal size (l++m) = size l + size m. Proof. @@ -508,21 +572,58 @@ congr op. - exact: eq_xz. Qed. +(** + If one does not know the [congr] tactic, + it is possible to go around by using forward reasoning. + However, it leads to a more cumbersome script. + In the example above, it is also possible to use the [rewrite] tactic, like this: +*) + +Goal w = y -> x = z -> op w x = op y z. +Proof. +move=> eq_wy eq_xz. +by rewrite eq_wy eq_xz. +Qed. + +(** + If an introduced assumption is used to rewrite and then no more used, + it is possible to use the [->] syntax: +*) + +Goal w = y -> x = z -> op w x = op y z. +Proof. +move => ->. +move => ->. +by []. +Qed. + +Goal w = y -> x = z -> op w x = op y z. +Proof. by move => -> ->. Qed. (* the best rewrite script for this proof *) + +Goal w = y -> x = z -> op w x = op y z. +Proof. +move->. +by move ->. +Qed. + End Congruence. (** *** Forward reasoning From the point of view of proof engineering with Coq, one generally prefers to work on the goal over working on the local context. - This proof style is used in the Mathematical Components Library and is orthogonal to SSReflect tactics. + This proof style is used in the Mathematical Components Library and is orthogonal to using SSReflect tactics. One benefit of this style is to get failure earlier when the script gets broken, and thus it is easier to fix it. Instead of working on the local context (for instance by using [rewrite in] on an hypothesis in the local context) it is preferable to work on it while it is still in the goal and before it is introduced to the local context. This way, one avoids relying on the names of the introduced assumptions. + It may also possible to factor some treatments and remove some subgoals right away, + which let one keep lower number of subgoals and sometimes avoid relying on the order of introduction of subgoals. Pushing something to top might be changed without creating an error immediately, leading to more difficulties to maintain the script. - This difficulty can be more apparent when reusing old code or code written by others. + This difficulty can be more apparent when reusing old code or code written by others + (and even more if one is just a user of the code and needs to fix a proof script). Still, one may want to use forward reasoning occasionally. The main SSReflect forward reasoning tactic is [have:]. @@ -543,17 +644,56 @@ have H : 0 = 0. (* syntax to give a name to the introduced intermediate result * - Abort. +(** + The [have:] tactic can be combined with destructing [[]] and with rewriting [->]. + Below are some examples: +*) + +Module MoreHave. + +(* From HB Require Import structures. *) + +From mathcomp Require Import ssrbool eqtype ssrnat. + +Local Open Scope nat_scope. + +Variables (P : nat -> nat -> bool) (m n : nat). + +Goal P m n. +Proof. +move: (eqVneq m n). +Print eq_xor_neq. +move=> [eq_mn|neq_mn]. +- rewrite eq_mn. + admit. +- +Abort. + +(** + The above code can be simplified into: +*) + +Goal P m n. +Proof. +move: (eqVneq m n) => [->|neq_mn]. +- admit. +- +Abort. + +End MoreHave. + + (** *** Changing view - Changing view is performed on the first assumption with the tactic [move/] + Changing view - also called view application - is performed on the first assumption with the tactic [move/] or on the conclusion with the tactic [apply/]. It replaces it with a "different view". - The first asumption can be replaced by a weaker asumption - and the conclusion can be replaced by a stronger conclusion. + The first asumption can be replaced with a weaker asumption + and the conclusion can be replaced with a stronger conclusion. With reflection results (with the [reflect] keyword) a proposition - can be replaced with an equivalent boolean and a boolean - can be replaced with an equivalent proposition. + can be replaced with an equivalent boolean + and conversely a boolean can be relpaced with an equivalent proposition. This is part of the Small Scale Reflection methodology. Let's look at some examples. @@ -642,7 +782,7 @@ End BooleanReflection. (** SSReflect offers rewrite patterns to guide Coq to select specific matches for a rewrite. Otherwise the first match is selected, which is not necessarly the desired effect. - Please not that the match and the occurence are two different things. + Please not that match and occurence are two different things. A pattern has several matches - eventually none - and each match has one or multiple occurrences. Let's look at examples. *) @@ -732,10 +872,10 @@ End SomeMorePatterns. (** *** Case analysis - Let's say there is a value [v] of type [T] where [T] is an inductive type - (an inductive type has a finite number of constructors). + Let's say there is a value [v] of type [T] where [T] is an inductive type. Case analysis on [v] consists in examining how [v] is constructed, - which leads to one subgoal for each constructor. + which leads to one subgoal for each constructor + (an inductive type has a finite number of constructors). *) @@ -743,8 +883,8 @@ Goal forall (n : nat), n + n = n. Proof. move=> n. case: n. -(* the goals is splitted into two goals *) -- rewrite /=. +(* the goal is splitted into two goals *) +- rewrite /=. by []. - move=> n. (* we get stuck here, because we are trying to prove something false *) @@ -762,10 +902,10 @@ case: n=> [|n]. (* the pipe symbol '|' separates each subgoal *) - (* we get stuck here, because we are trying to prove something false *) Abort. -(** It is possible to combine moving (with [move =>]) - with simplification [/=] and removing trivial goals [//]. +(** It is possible to combine moving ([move =>]) + with simplification [/=] and with removing trivial goals [//]. In the following script, after the case analysis, the first goal is trivial and removed by [//]. - Thus, only one goal is remaining and [n] can be introduced without using the pipe symbol. + Thus, only one goal remains and [n] can be introduced without using the pipe symbol. *) Goal forall (n : nat), n + n = n. @@ -778,10 +918,10 @@ Abort. (** *** Specialising Conversely to strengthening the goal, one can always weaken assumptions. - In other words, if one can do with less then one can do with more. + In other words, if one can achieve (the proof requirement) with less then one can do it with more (what is currenly available). One way to weaken an assumption is by specialising it. - In the following example, the assumption [forall y, P y] is specialised to [x], - which results in the asumption [P x]. + In the following example, the assumption [forall y, P y] is specialised with [x], + which results in the asumption [P x]. Specialising can be seen as a special case of view application. *) @@ -805,7 +945,7 @@ Abort. We remind here the [pose] tactic (that does not come from SSReflect) which let one add a local definition to the current context. -It can be useful to see more clearly the goal and the local context. +It can be useful - as temporary code - to see more clearly the goal and the local context. *) @@ -815,6 +955,63 @@ pose a := 1 + 2. rewrite -/a. (* can see more clearly now *) Abort. +(** *** Discarding top + + Still according to the principle + that if one can achieve (the proof requirement) with less then one can do it with more (what is currenly available), + it is a valid reasoning step to discard the top assumption. + It can be seen as an extreme case of weakening top. + Consider the following simple proof. + +*) + +Goal forall (P Q : Prop), P -> Q -> P. +Proof. +move=> P Q HP HQ. +exact: HP. +Qed. + +(** + The assumption that [Q] is inhabitated (proved) + is introduced with the name [HQ] and it is never used to achieve the proof. + Instead of moving it to the local context, it is better to discard it as follows: +*) +Goal forall (P Q : Prop), P -> Q -> P. +Proof. +move=> P Q HP _. +exact: HP. +Qed. + +(** + Sometimes, a variable from the local context is used in the proof of the current goal + and then is not used anymore. + In this scenario, it is possible to discard it as follows. +*) + +Module DiscardFromLocalContext. + +(* From HB Require Import structures. *) + +From mathcomp Require Import ssrbool eqtype ssralg ssrnum. +Import GRing.Theory Num.Theory. +Local Open Scope ring_scope. + +Variable (R : fieldType). +Variable (x : R). + +Goal x != 0 -> (x ^+ 2) / x = x. +Proof. +move=> x_neq_0. +rewrite -mulrA. +rewrite mulfV. +- move=> {x_neq_0}. (* we can discard x_neq_0 here *) + (* it may be interesting to do so in a longer script *) + by rewrite mulr1. +- exact: x_neq_0. +Qed. + +End DiscardFromLocalContext. + (** ** 4. Exercices *) @@ -865,7 +1062,7 @@ End Exercice3. Finally, one may get inspiration from the Mathematical Component Library for their own formalisation. This includes Small Scale Reflection methodology and SSReflect coding conventions. - Some ingredients are boolean reflection, decidable structures + Some ingredients are boolean reflection, structures with decidable equality and hierarchy of structures (with Hierarchy Builder). *) From 1e5f0a2669aed5cb216e7f1a5364a95c347f2b31 Mon Sep 17 00:00:00 2001 From: grianneau <> Date: Tue, 13 Aug 2024 18:03:55 +0200 Subject: [PATCH 3/5] a tutorial draft about SSReflect tactics for vanilla Rocq (Coq) users --- src/Tutorial_SSReflect_tactics.v | 953 +++++++++++++++++++++++++++++++ src/index.html | 7 + src/jscoq-agent.js | 2 +- src/package-lock.json | 14 + src/package.json | 2 + 5 files changed, 977 insertions(+), 1 deletion(-) create mode 100644 src/Tutorial_SSReflect_tactics.v diff --git a/src/Tutorial_SSReflect_tactics.v b/src/Tutorial_SSReflect_tactics.v new file mode 100644 index 00000000..74a047d0 --- /dev/null +++ b/src/Tutorial_SSReflect_tactics.v @@ -0,0 +1,953 @@ +(** * Tutorial about SSReflect tactics + + *** Summary + In this tutorial, we introduce the main [SSReflect] tactics for the Rocq (Coq) user + with which one can do most reasoning steps. + After mastering this rather small set of tactics, + one should be able to write large parts of proof scripts and many complete proof scripts + from the scripts one is already able to write with vanilla Coq. + The main take-away is to understand intuitively what is the effect of each tactic on the proof state, + so that one has an overview of possible logical reasoning steps when in the proof mode. + Small insecable steps are emphasised, however the examples can seem artificial + and the shown scripts do not necessarly meet coding conventions. + The code examples in this page serve only as memo-snippets + to remember how to achieve the main basic logical steps with SSReflect tactics. + + [SSReflect] tactics are shipped with the standard Coq distribution. + They are made available after loading the SSReflect plugin. + + *** Table of content + + - 1. Introduction + - 2. SSReflect tactics + - 3. More SSReflect tactics + - 4. Exercices + + *** Prerequisites + - We assume basic knowledge of Coq + + Installation: the SSReflect set of tactics is shipped with the Coq distribution. +*) + + + +(** ** 1. Introduction + + This tutorial covers SSRfeflect tactics, not Small Scale Reflection methodology neither Mathematical Components Library. + There is a benefit to using this set of tactics + since one can achieve most proof steps with a relatively small set of tactics + (even without using this methodology or the Mathematical Components Library). + + Isolated basic reasoning steps are illustrated with examples. + It is about beeing aware of some basic valid reasoning steps that are available. + + In the section 3. More SSReflect tactics, + one will find tactics that can technically be got around with previous tactics. + + Let us start by importing SSReflect. +*) + +From Coq Require Import ssreflect. + +(* One may also need to uncomment the following two lines. *) +(* From Coq Require Import ssreflect ssrfun ssrbool. *) +(* Import ssreflect.SsrSyntax. *) + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +(** ** 2. SSReflect tactics + The two main tactics are [rewrite] and [apply:]. + The colon punctuation mark at the end of [apply:] distinguishes it + from the [apply] tactic from vanilla Coq. + After loading SSReflect, the default behaviour of [rewrite] is changed. +*) + +(** *** Moving things + +(a completely unrelated link, just a song in a movie: +https://www.youtube.com/watch?v=m1543Y2Em_k&pp=ygU6QnVybmluZyBMaWdodHMgLSBKb2UgU3RydW1tZXIgaW4gSSBIaXJlZCBhIENvbnRyYWN0IEtpbGxlcg%3D%3D ) + +We start by showing how to [move] things between the current goal and the context. +With [move=>] one can move the first assumption of the goal to the local context. +In the opposite direction, +with [move:] one can move something from the local or global context to the first assumption +(also called "top"). +Some baby steps with the [move] tactic +(the code showed below does not meet coding conventions): + +*) + +Goal forall (P Q : Prop), P -> Q. +Proof. +move=> P. +move=> Q. +move=> p. +Fail move: P. (* The command "move: P" should fail here. *) +move: p. +move: Q. +move: P. +move: or_comm. (* moving something from the global context *) +Abort. + +(** *** Destructing + + The [move] tactic can be used in combination with destructing, whose syntax is [[]]. + Destructing can let one access values of a record, do a case analysis on an inductive type, + split a disjunction into subgoals. + If new goals are introduced just after destructing, they are separated by the pipe symbols [|] + within the brackets. + As a result, the number of pipe symbols is the number of subgoals minus one. + It is possible to use destructing within subgoals, subsubgoals and so on, + as is done with [[move=> [HQ | [HR | HS]]]]. + +*) + +Module Destructing. + +From mathcomp Require Import ssrbool ssrnat. +(* It is better to place all import commands at the beginning of the file, + contrary to what is done here. + Yeah, do what I say, not as I do xD *) + +Variables (T : Type) (P : T -> Prop) (y z : T). + +Goal (exists u : T, P u) -> y = z. +Proof. +move=> [x]. +Abort. + +Goal (exists u : T, P u) -> y = z. +Proof. +move=> [x Px]. +Abort. + +Record Pair : Set := mkPair + { n : nat + ; b : bool}. + +Lemma PairP (x : Pair) : n x <= n x + (b x). +Proof. +move: x. +move=> [n b]. +rewrite /=. +(* proof to be finished *) +Abort. + +Goal forall (Q R S : Prop), Q \/ R -> S. +Proof. +move=> Q R S. +move=> [HQ | HR]. +- admit. +- +Abort. + +Goal forall (Q R S U : Prop), Q \/ R \/ S -> U. +Proof. +move=> Q R S U. +move=> [HQ | HRS]. +- admit. +- move: HRS => [HR | HS]. + + admit. + + +Abort. + +(** + The previous script can be shortened into: +*) + +Goal forall (Q R S U : Prop), Q \/ R \/ S -> U. +Proof. +move=> Q R S U. +move=> [HQ | [HR | HS]]. +- admit. +- admit. +- +Abort. + + +End Destructing. + +(** *** Simplifying + + At any stage within a proof attempt, one may want to try to simplify the goal + with the tactic [rewrite /=], + which is a special case for the [rewrite] tactic. + It is similar to the [simpl] tactic from vanilla Coq. + The tactic [rewrite /=] does not fail, even if no simplification could be done. + + It is possible to use patterns to guide the tactic + to simplify only some specific parts of the goal. + See the section 'Rewriting pattern' for the use of patterns. + We will see that it is possible to combine moving with simplification attempt. + +*) + +Definition foo (b : bool) := match b with +| true => false +| false => true +end. + +Goal foo true = false. +Proof. +rewrite /=. +by []. +Qed. + +(** + + The tactic [by []] tries to kill the goal - which is expected to be trivial for Coq - otherwise it fails. + Some vanilla Coq tactics that cover similar cases are [reflexivity] and [assumption]. + +*) + +Module NonTrivialCase. + +From mathcomp Require Import ssrbool ssrnat. + +Goal 2 * 3 = 3 + 3. +Proof. +by []. +Qed. + +End NonTrivialCase. + +(** *** Rewriting + + Rewriting is performed with the [rewrite] tactic. + Some use cases are presented below. + +*) + +(** **** Rewriting with equalities + + As with the vanilla [rewrite] tactic, + one of the use cases of the [rewrite] tactic is to rewrite the goal with a given equality from the context. + Let's look at the following example. + +*) + +Goal forall (T : Type) (a b c : T) (H : a = b), a = c -> b = c. +Proof. +move=> T a b c H. (* it is possible to combine several [move] into a single one *) +rewrite H. +by []. +Qed. + +(** + In this proof, the last two steps can be combined into a single one with: [by rewrite H]. + If you want, you can try to rewrite from right to left instead. +*) + +Goal forall (T : Type) (a b c : T) (H : a = b), a = c -> b = c. +Proof. +move=> T a b c H. (* it is possible to combine several move into one *) +rewrite -H. (* rewrites with the equality H from right to left *) +by []. +Qed. + +(** + A shorter version of the code: +*) +Goal forall (T : Type) (a b c : T) (H : a = b), a = c -> b = c. +Proof. by move=> T a b c H; rewrite H. Qed. + +Module AnotherRewrite. + +From mathcomp Require Import ssrbool ssralg ssrnum. + +(* Import GRing.Theory Num.Theory. *) +Local Open Scope ring_scope. + +Variable (R : numDomainType). + +Lemma add_leq_right (z x y : R) : (x <= y) = (x + z <= y + z). +Proof. +(* we are going to use this admitted lemma *) +(* proving this lemma can be left as an exercice once you are more familiar with SSReflect tactics *) +(* and if you want to explore the Mathematical Components Library. *) +Admitted. + +Goal forall (x : R), x <= x. +Proof. +move=> x. +rewrite (add_leq_right x). +Abort. + +End AnotherRewrite. + +(** *** Unfolding a definition. + + Unfolding a definition is done with [rewrite /the_definition_to_be_unfolded]. + +*) + +Definition secret : nat := 42. + +Goal secret = 41 + 1. +Proof. +rewrite /secret. +rewrite -/secret. (* folding back *) +by []. +Qed. + +(** *** The [apply:] tactic + +The [apply:] tactic is similar to the vanilla Coq [apply] tactic. +It tries to match the conclusion (and eventually some premisses) of the lemma +with the goal. +It lets one do backward reasoning. +Let's look at some examples. + +*) + +Goal forall (A B : Prop) (H : A-> B), B. +Proof. +move=> A B H. +apply: H. +Abort. + +Goal forall (A B C : Prop) (H : A -> B -> C), B -> C. +Proof. +move=> A B C H. +apply: H. (* the premise B has been included *) +Abort. + +(** *** Generalisation *) + +Module Generalisation. + +From mathcomp Require Import ssrbool ssralg ssrnum. +Local Open Scope ring_scope. + +Variable (R : numDomainType). + +Goal (4 + 1) ^+ 2 = 4 ^+ 2 + 4 *+ 2 + 1 :> R. +Proof. +move: 4. (* generalises over the term 4 *) +Abort. + +Goal 1 + 1 = 1 * 1 :> R. +Proof. +move: 1. (* generalises over all occurrences of 1 *) +Abort. + +Goal 1 + 1 = 1 * 1 :> R. +Proof. +move: {2}1. (* generalises over the second occurrence of 1 *) +move=> x. +Abort. + +Goal 1 + 1 = 1 * 1 :> R. +Proof. +move: {2 4}1. (* generalises over the second and the forth occurrence of 1 *) +move=> x. +Abort. + +Check list. + +Goal forall (T : Type) (l : list T) (C : Prop), C. +Proof. +move=> T l C. +move: (eq_refl (length l)). (* this illustrates moving something from the global context to top *) +move: {2}(length l). (* generalises over the second occurrence only *) +move=> n. +Abort. + +End Generalisation. + + +(** *** Inductive reasoning + + The [induction] tactic from vanilla Coq is replaced by the [elim:] tactic. + +*) + +Module InductionExample. + +Variable (T : Type). + +Goal forall (l : list T), False. +Proof. +move=> l. +elim: l. +- admit. +- move=> a l IH. +Abort. + +End InductionExample. + +Module Range. + +From mathcomp Require Import ssrnat seq. + +Fixpoint range (a : nat) (n : nat) := match n with +| 0 => [::] +| m.+1 => a::(range (a.+1) m) +end. + +(* The following code is presented with more lines than necessary *) +(* to ease playing it step-by-step. *) +Goal forall (a : nat) (n : nat), size (range a n) = n. +Proof. +move=> a n. +move: a. +elim: n. (* starts induction on n *) +- (* base case *) + move=> n. + rewrite /=. + by []. +- (* inductive step *) + move=> n. + move=> IH. + move=> b. + rewrite /=. + rewrite IH. + by []. +Qed. +(* Les preuves n'ont pas d'odeur. *) + + +(* The previous script can be shortened to: *) + +Lemma size_range (a : nat) (n : nat) : size (range a n) = n. +Proof. +move: a; elim: n => // n IHn b /=. +by rewrite IHn. +Qed. + +(* The syntax [//] after [=>] in a [move] means: please remove trivial goals. *) +(* In this example, Coq is able to kill the base case as a trivial goal. *) +(* As a result, only one goal (out of two) remains after [//] and thus no pipe symbol is required. *) +(* Simplification and removing trivial goals can be combined into the syntax [//=]. *) + +End Range. + +Module InductionSequence. + +From mathcomp Require Import ssrnat seq. + +Variables (l m : seq nat). + +Goal size (l++m) = size l + size m. +Proof. +move: m. +elim: l=> // a l IH m /=. +by rewrite IH. +Qed. + +Check last_ind. + +(* The result [last_ind] is an alternative induction principle *) +(* that can be applied at the elimination step in the previous example. *) +(* Instead of using the default induction principle, *) +(* the syntax [elim/last_ind:] combines elimination with view application. *) +(* Starting again from the same goal and applying the [last_ind] view: *) + +Goal size (l++m) = size l + size m. +Proof. +move: m. +elim/last_ind: l. (* elimination is done with the inductive principle last_ind *) +- by move=> m. +- move=> m a IH l. + rewrite size_rcons. + rewrite cat_rcons. + rewrite IH. + rewrite /=. + by rewrite addnS. +Qed. + + +End InductionSequence. + + +(** *** Congruence + + When it is required to prove an equality between two applications of the same function, + it suffices to prove that the corresponding arguments of both applications are equal. + As a Coq user, you may already uses the [congruence] tactic. + With SSReflect, the [congr] tactic is used. + + For instance, in the following examples it is required to prove [op w x = op y z]. + This goal has the form of an equality with the same function applied in each member. + The first arguments are [w] on the left and [y] on the right. + The second arguments are [x] on the left and [z] on the right. + It is sufficient to prove that [w = y] and [x = z]. + +*) + +Section Congruence. + +Variables (T : Type) (op : T -> T -> T) (w x y z : T). + +Goal w = y -> x = z -> op w x = op y z. +Proof. +move=> eq_wy eq_xz. +congr op. +- exact: eq_wy. +- exact: eq_xz. +Qed. + +(** + In the example above, it is also possible to use the [rewrite] tactic + and get around the use of congruence, this way: +*) + +Goal w = y -> x = z -> op w x = op y z. +Proof. +move=> eq_wy eq_xz. +by rewrite eq_wy eq_xz. +Qed. + +(** + If an introduced assumption is used to rewrite and then no more used, + it is possible to use the [->] syntax: +*) + +Goal w = y -> x = z -> op w x = op y z. +Proof. +move => ->. +move => ->. +by []. +Qed. + +Goal w = y -> x = z -> op w x = op y z. +Proof. by move => -> ->. Qed. (* the shortest rewrite script for this proof *) + +Goal w = y -> x = z -> op w x = op y z. +Proof. +move->. +by move ->. +Qed. + +End Congruence. + +(** *** Forward reasoning + + One can use the SSReflect tactic [have:] instead of the vanilla Coq tactic [assert], + to do forward reasoning. + + From the point of view of proof engineering with Coq, + one generally prefers to work on the goal over working on the local context. + This proof style is used in the Mathematical Components Library and is orthogonal to using SSReflect tactics. + One benefit of this style is to get failure earlier when the script gets broken, + and thus it is easier to fix it. Instead of working on the local context + (for instance by using [rewrite in] on an hypothesis in the local context) + it is preferable to work on it while it is still in the goal and before it is introduced to the local context. + This way, one avoids relying on the names of the introduced assumptions. + It may also be possible to factor some treatments and remove some subgoals right away, + which let one keep lower number of subgoals and sometimes avoid relying on the order of introduction of subgoals. + Pushing something to top might be changed without creating an error immediately, + leading to more difficulties when maintaining the script. + This difficulty can be more apparent when reusing old code or code written by others + (and even more if one is just a user of the code and needs to fix a proof script). + + Still, one may want to use forward reasoning occasionally. + The main SSReflect forward reasoning tactic is [have:]. + +*) + +Goal False. +Proof. +have : 0 = 0. +- by []. +- move=> H. +Abort. + +Goal False. +Proof. +have H : 0 = 0. (* syntax to give a name to the introduced intermediate result *) +- by []. +- +Abort. + +(** + The [have:] tactic can be combined with destructing [[]] and with rewriting [->]. + Below are some examples: +*) + +Module MoreHave. + +From mathcomp Require Import ssrbool eqtype ssrnat. + +Local Open Scope nat_scope. + +Variables (P : nat -> nat -> bool) (m n : nat). + +Goal P m n. +Proof. +move: (eqVneq m n). +Print eq_xor_neq. +move=> [eq_mn|neq_mn]. +- rewrite eq_mn. + admit. +- +Abort. + +(** + The above code can be simplified into: +*) + +Goal P m n. +Proof. +move: (eqVneq m n) => [->|neq_mn]. +- admit. +- +Abort. + +End MoreHave. + + +(** *** Changing view + + Changing view - also called view application - is performed on the first assumption with the tactic [move/] + or on the conclusion with the tactic [apply/]. + It replaces it with a "different view". + The first assumption can be replaced with a weaker asumption + and the conclusion can be replaced with a stronger conclusion. + + One specific case of view application results are reflection results (which use the [reflect] keyword). + A reflection establishes the equivalence between a proposition and a boolean. + In this context, a boolean can always be coerced to a proposition with the coercion [is_true]. + By exploiting a reflection result, a proposition can be replaced with an equivalent boolean + and conversely a boolean can be replaced with an equivalent proposition. + This is part of the Small Scale Reflection methodology. + + Please note that one can use view application without necessarily using reflection. + + Let's look at some examples. + +*) + +Module ChangingView. + +Variables (A B C D E : Prop). +Hypothesis (H : B -> C). + +Goal B -> D -> E. +Proof. +move/H. (* weakens B to C *) +Abort. + +Goal A -> C. +Proof. +move=> HA. +apply/H. (* strenghten C to B *) +move: HA. +Abort. + +(* + These examples also work with equivalence instead of implication. +*) + +Hypothesis (H' : B <-> C). + +Goal B -> D -> E. +Proof. +move/H'. (* weakens B to C *) +Abort. + +Goal A -> C. +Proof. +move=> HA. +apply/H'. (* strenghten C to B *) +move: HA. +Abort. + +End ChangingView. + +(* + Some examples of view changing are now shown with boolean reflection. + +*) + +Module BooleanReflection. +From mathcomp Require Import ssrbool ssrnat. + +Check minn_idPr. + +Variables (m n : nat) (P : Prop). + +Goal minn m n = n -> P. +Proof. +move/minn_idPr. +Abort. + +(* + One can combine changing view with moving things: +*) + +Goal minn m n = n -> P. +Proof. +move/minn_idPr=> H. +Abort. + +(* + Some other examples: +*) + +Goal n <= m-> P. +Proof. +move/minn_idPr. +Abort. + +Goal P -> minn m n = n. +Proof. +move=> H. +apply/minn_idPr. +Abort. + +Goal P -> n <= m. +Proof. +move=> H. +apply/minn_idPr. +Abort. + +End BooleanReflection. + +(** Rewriting pattern. *) + +(** + SSReflect offers rewrite patterns to guide Coq to select specific matches for a rewrite. + Otherwise the first match is selected, which is not necessarly the desired effect. + Please not that match and occurence differs. + A pattern has several matches - eventually none - and each match has one or multiple occurrences. + Let's look at some examples. +*) + +Module RewritePatterns. + +From mathcomp Require Import ssrbool ssralg ssrnum. + +(* Import GRing.Theory Num.Theory. *) +Local Open Scope ring_scope. + +Variables (R : ringType) (a b c : R). +Hypothesis H : forall (x : R), x = c. + +Goal (a + b) * a + (a + b + a) * b = (b + b) * a + (a + b + b) * a * b. +Proof. +rewrite [LHS]H. (* rewrites the left-hand side of the equality *) +Abort. + +Goal (a + b) * a + (a + b + a) * b = (b + b) * a + (a + b + b) * a * b. +Proof. +rewrite [RHS]H. (* rewrites the right-hand side of the equality *) +Abort. + +Goal (a + b) * a + (a + b + a) * b = (b + b) * a + (a + b + b) * a * b. +Proof. +rewrite [a+b]H. (* rewrites the all occurrences of a+b with H *) +Abort. + +Goal (a + b) * a + (a + b + a) * b = (b + b) * a + (a + b + b) * a * b. +Proof. +rewrite [a+b in LHS]H. (* rewrites the all occurrences of a+b in the left-hand side *) +Abort. + +Goal (a + b) * a + (a + b + a) * b = (b + b) * a + (a + b + b) * a * b. +Proof. +rewrite {2}[a + b]H. (* rewrites the second occurrence of a+b with H *) +Abort. + +Goal (a + b) * a + (a + b + a) * b = (b + b) * a + (a + b + b) * a * b. +Proof. +rewrite [a + b + _]H. (* rewrites occurences of the first match of a + b + _ *) +Abort. + +Goal (a + b) * a + (a + b + a) * b = (b + b) * a + (a + b + b) * a * b. +Proof. +rewrite [X in X + b]H. (* the pattern X + b is matched against a + b then a is rewritten in occurences of a + b *) +Abort. + +(* + The following examples shows that we can explicit a pattern + to the point that exactly one [b] is rewritten, + the one in the middle in the term [a + b + b]. +*) + +Goal (a + b) * a + (a + b + a) * b = (b + b) * a + (a + b + b) * a * b. +Proof. +rewrite [X in (_ + _)* _ + (_ + X + _)* _ * _]H. +Abort. + +End RewritePatterns. + +Module SomeMorePatterns. + +From mathcomp Require Import ssrbool ssrnat order. + +Local Open Scope nat_scope. +Local Open Scope order_scope. + +Variables (a b c : nat). + +Hypothesis H : forall x, x = c. + +Goal (a + b) * a + (a + b + a) * b <= (b + b) * a + (a + b + b) * a * b. +Proof. +rewrite [leLHS]H. +Abort. + +Goal (a + b) * a + (a + b + a) * b < (b + b) * a + (a + b + b) * a * b. +Proof. +rewrite [ltRHS]H. +Abort. + +End SomeMorePatterns. + +(** ** 3. More SSReflect tactics +*) + +(** *** Case analysis + + The SSReflect tactic for case analysis is [case:]. + The colon punctuation mark at the end of [case:] distinguishes it + from the [case] tactic from vanilla Coq. + +*) + +Goal forall (n : nat), n + n = n. +Proof. +move=> n. +case: n. +(* the goal is splitted into two goals *) +- rewrite /=. + by []. +- move=> n. +Abort. + +(** The previous script can be written more shortly as follows +*) + +Goal forall (n : nat), n + n = n. +Proof. +move=> n. +case: n=> [|n]. (* the pipe symbol '|' separates each subgoal *) +(* the goals is splitted into two goals *) +- by []. +Abort. + +(** + It is possible to combine moving ([move =>]) + with simplification [/=] and with removing trivial goals [//]. + In the following script, after the case analysis, the first goal is trivial and removed by [//]. + Thus, only one goal remains and [n] can be introduced without using the pipe symbol. +*) + +Goal forall (n : nat), n + n = n. +Proof. +move=> n. +case: n=> // n. +Abort. + +(** *** Specialising + + One can always weaken the top assumtpion by specialising it. + With vanilla Coq, this can be achieved with the [specialize] tactic. + With SSReflect, it can be achieved as a special case of view application, with the syntax [/(_ value)]. + In the following example, the assumption [forall y, P y] is specialised with [x], + which results in the asumption [P x]. + +*) + +Goal forall (T G : Type) (P : T -> Prop) (x : T), (forall y, P y) -> G. +Proof. +move=> T G P x. +move/(_ x). +Abort. + +(** *** Discarding top + + Discarding the top assumption can be achieved with [move=> _] + as in the following example. + +*) + +Goal forall (P Q : Prop), P -> Q -> P. +Proof. +move=> P Q HP _. +exact: HP. +Qed. + +(** + Discarding something from the local context is achieved with the syntax [move=> {somehting}]. + Here is an example: +*) + +Module DiscardFromLocalContext. + +From mathcomp Require Import ssrbool eqtype ssralg ssrnum. +Import GRing.Theory Num.Theory. +Local Open Scope ring_scope. + +Variable (R : fieldType). +Variable (x : R). + +Goal x != 0 -> (x ^+ 2) / x = x. +Proof. +move=> x_neq_0. +rewrite -mulrA. +rewrite mulfV. +- move=> {x_neq_0}. (* we can discard x_neq_0 here *) + (* it may be interesting to do so in a longer script *) + by rewrite mulr1. +- exact: x_neq_0. +Qed. + +End DiscardFromLocalContext. + +(** ** 4. Exercices +*) + +(** *** Exercice 1 + For this exercice, you may want to use the vanilla tactic [split]. +*) + +Goal forall (P Q : Prop), P /\ Q -> Q /\ P. +Proof. +move=> P Q [HP HQ]. +split. +- exact: HQ. +- exact: HP. +Qed. + +(** *** Exercice 2 +*) + +Goal forall (P Q : Prop), P \/ Q -> Q \/ P. +Proof. +move=> P Q [HP | HQ]. +- right. + exact: HP. +- left. + exact: HQ. +Qed. + +(** *** Exercice 3 +*) + +Module Exercice3. + +From mathcomp Require Import ssrbool ssrnat div. + +Local Open Scope nat_scope. + +Lemma div2nSn (n : nat) : 2 %| n * n.+1. +Proof. by rewrite dvdn2 oddM /= andbN. Qed. + +End Exercice3. + +(** ** Where to go from here + + One may try to port one proof script from vanilla Coq to SSReflect and see the difference. + In addition to using SSReflect tactics, + one may start reusing some results from the Mathematical Components Library. + + Finally, one may get inspiration from the Mathematical Component Library for their own formalisation. + This includes Small Scale Reflection methodology and SSReflect coding conventions. + Some ingredients are boolean reflection, structures with decidable equality + and hierarchy of structures (with Hierarchy Builder). + +*) diff --git a/src/index.html b/src/index.html index fe1a55b7..d2987214 100644 --- a/src/index.html +++ b/src/index.html @@ -30,6 +30,7 @@

About

Proof General, vim with CoqTail, vscode with vscoq).

+

Coq Tutorials

Equations tutorials

diff --git a/src/jscoq-agent.js b/src/jscoq-agent.js index 589a3700..630b87f6 100644 --- a/src/jscoq-agent.js +++ b/src/jscoq-agent.js @@ -36,7 +36,7 @@ var jscoq_opts = { // editor: { mode: { 'company-coq': true }, className: 'jscoq code-tight' }, editor: { className: 'jscoq code-tight' }, init_pkgs: ['init'], - all_pkgs: { '+': ['coq', 'equations'] }, + all_pkgs: { '+': ['coq', 'equations', 'elpi', 'mathcomp'] }, init_import: ['utf8'], implicit_libs: true }; diff --git a/src/package-lock.json b/src/package-lock.json index 9d4eb333..d12341de 100644 --- a/src/package-lock.json +++ b/src/package-lock.json @@ -5,7 +5,9 @@ "packages": { "": { "dependencies": { + "@jscoq/elpi": "^0.17.1", "@jscoq/equations": "^0.17.1", + "@jscoq/mathcomp": "^0.17.1", "http-server": "^14.1.0", "jscoq": "^0.17.1", "wacoq-deps": "^0.1.1" @@ -22,11 +24,23 @@ "node": ">=6.0.0" } }, + "node_modules/@jscoq/elpi": { + "version": "0.17.1", + "resolved": "https://registry.npmjs.org/@jscoq/elpi/-/elpi-0.17.1.tgz", + "integrity": "sha512-qtQ7MB875/uhOi70MMdkzKbpDNVr8HYBaUfEJ9U5yrlyiGnNn98uiAw6Bod6KHl7AOunt94aV7j2o+JEn8MVZA==", + "license": "AGPL-3.0-or-later" + }, "node_modules/@jscoq/equations": { "version": "0.17.1", "resolved": "https://registry.npmjs.org/@jscoq/equations/-/equations-0.17.1.tgz", "integrity": "sha512-DU7XgFvIbFRidE8z9jtsB44mnTYyPMeDY2BU1SBz/kXsgeT/OErg7sDYa9enwpeQIx215AQZDdkIeQ3N5KVX9Q==" }, + "node_modules/@jscoq/mathcomp": { + "version": "0.17.1", + "resolved": "https://registry.npmjs.org/@jscoq/mathcomp/-/mathcomp-0.17.1.tgz", + "integrity": "sha512-QwTTYWpv/kADJAqvCqlRD/jEtZEyfniLp57fLZ4RonUuo0ieAM1zsR8WiFrOjDzJbnC4tYI8rd3akCgL050Kdw==", + "license": "AGPL-3.0-or-later" + }, "node_modules/@ocaml-wasm/4.12--janestreet-base": { "version": "0.16.0-0", "resolved": "https://registry.npmjs.org/@ocaml-wasm/4.12--janestreet-base/-/4.12--janestreet-base-0.16.0-0.tgz", diff --git a/src/package.json b/src/package.json index 47e2ef91..f1ce1809 100644 --- a/src/package.json +++ b/src/package.json @@ -3,6 +3,8 @@ "jscoq": "^0.17.1", "wacoq-deps": "^0.1.1", "@jscoq/equations": "^0.17.1", + "@jscoq/elpi": "^0.17.1", + "@jscoq/mathcomp": "^0.17.1", "http-server": "^14.1.0" } } From b9bfe65dd78995f6372a7aa8dfb6cde2a6c426b1 Mon Sep 17 00:00:00 2001 From: grianneau <> Date: Tue, 20 Aug 2024 09:14:37 +0200 Subject: [PATCH 4/5] new version of the tutorial about some vanilla and SSReflect tactics --- src/Tutorial_SSReflect_tactics.v | 1136 +++++++++++++++++++++--------- 1 file changed, 812 insertions(+), 324 deletions(-) diff --git a/src/Tutorial_SSReflect_tactics.v b/src/Tutorial_SSReflect_tactics.v index 74a047d0..2f0ee886 100644 --- a/src/Tutorial_SSReflect_tactics.v +++ b/src/Tutorial_SSReflect_tactics.v @@ -1,52 +1,62 @@ -(** * Tutorial about SSReflect tactics +(** * Tutorial about Rcoq (Coq) tactics *** Summary - In this tutorial, we introduce the main [SSReflect] tactics for the Rocq (Coq) user - with which one can do most reasoning steps. - After mastering this rather small set of tactics, - one should be able to write large parts of proof scripts and many complete proof scripts - from the scripts one is already able to write with vanilla Coq. + In this tutorial, we briefly introduce some main Rocq (Coq) tactics, + that are shipped with the standard distribution of Rocq. + Both vanilla tactics and SSReflect tactics are dealt with. + One can work either with vanilla tactics or with SSReflect tactics, + and short examples are provided for both sets of tactics. + One can do most reasoning steps with the introduced tactics. The main take-away is to understand intuitively what is the effect of each tactic on the proof state, so that one has an overview of possible logical reasoning steps when in the proof mode. - Small insecable steps are emphasised, however the examples can seem artificial - and the shown scripts do not necessarly meet coding conventions. - The code examples in this page serve only as memo-snippets - to remember how to achieve the main basic logical steps with SSReflect tactics. + Small insecable steps are emphasised. + The code examples in this page can serve as memo-snippets + to remember how to achieve some main basic logical steps within proofs in Rocq. - [SSReflect] tactics are shipped with the standard Coq distribution. + [SSReflect] tactics are shipped with the standard Rocq distribution. They are made available after loading the SSReflect plugin. *** Table of content - 1. Introduction - - 2. SSReflect tactics - - 3. More SSReflect tactics + - 2. Main tactics + - 3. Some more tactics - 4. Exercices *** Prerequisites - - We assume basic knowledge of Coq + - We assume basic knowledge of Rocq - Installation: the SSReflect set of tactics is shipped with the Coq distribution. *) - - (** ** 1. Introduction - This tutorial covers SSRfeflect tactics, not Small Scale Reflection methodology neither Mathematical Components Library. - There is a benefit to using this set of tactics - since one can achieve most proof steps with a relatively small set of tactics + One typically uses Rocq tactics in one of the two following ways: one exclusively uses vanilla tactics, + or else one uses SSReflect tactics with some vanilla tactics. + This tutorial covers some main tactics. Many tactics are twins (a vanilla one and a SSReflect one) + that behaves similarly. + When dealing with an SSReflect tactic, the two following aspects are not covered int his tutorial: + Small Scale Reflection methodology and Mathematical Components Library. + There are some benefits to using the SSReflect set of tactics. For instance, + they are equipped with a rewrite pattern language, + and fewer tactics are necessary to kill trivial goals (even without using this methodology or the Mathematical Components Library). - + Isolated basic reasoning steps are illustrated with examples. - It is about beeing aware of some basic valid reasoning steps that are available. + The objective is to be aware of some main valid reasoning steps that are available. + + In the section 3. More tactics, + one will find tactics that can technically be got around with previous tactics from section 2. - In the section 3. More SSReflect tactics, - one will find tactics that can technically be got around with previous tactics. + Let us start by showing how to load SSReflect tactics. +*) - Let us start by importing SSReflect. +(** + To work with SSReflect tactics, one typically runs the following commands + as is done in the following module: *) +Module LoadSSReflect. + From Coq Require Import ssreflect. (* One may also need to uncomment the following two lines. *) @@ -57,60 +67,135 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. -(** ** 2. SSReflect tactics - The two main tactics are [rewrite] and [apply:]. - The colon punctuation mark at the end of [apply:] distinguishes it - from the [apply] tactic from vanilla Coq. +End LoadSSReflect. + +(** ** 2. Main tactics + Overall, there are two main tactics, [rewrite] and [apply]/[apply:]. + The syntax for the [rewrite] tactic is the same for SSReflect and vanilla Rocq. + The colon punctuation mark at the end of the SSReflect tactic [apply:] + distinguishes it from the vanilla Rocq tactic [apply]. After loading SSReflect, the default behaviour of [rewrite] is changed. *) (** *** Moving things -(a completely unrelated link, just a song in a movie: -https://www.youtube.com/watch?v=m1543Y2Em_k&pp=ygU6QnVybmluZyBMaWdodHMgLSBKb2UgU3RydW1tZXIgaW4gSSBIaXJlZCBhIENvbnRyYWN0IEtpbGxlcg%3D%3D ) + (a completely unrelated link, just a song in a movie: + https://www.youtube.com/watch?v=m1543Y2Em_k&pp=ygU6QnVybmluZyBMaWdodHMgLSBKb2UgU3RydW1tZXIgaW4gSSBIaXJlZCBhIENvbnRyYWN0IEtpbGxlcg%3D%3D ) -We start by showing how to [move] things between the current goal and the context. -With [move=>] one can move the first assumption of the goal to the local context. -In the opposite direction, -with [move:] one can move something from the local or global context to the first assumption -(also called "top"). -Some baby steps with the [move] tactic -(the code showed below does not meet coding conventions): + We start by showing how to move things between the current goal and the context. + SSReflect has a simplier syntax to move things. + With SSReflect, with [move=>] (which can sometimes be shortened to just [=>] when combined with other tactics) + one can move the first assumption of the goal to the local context. + In the opposite direction, + with [move:], one can move something from the local or global context to the first assumption + (also called top assumption or just "top"). + Some basic steps with the [move] tactic + (the proof script shown below does not meet coding conventions): *) -Goal forall (P Q : Prop), P -> Q. +Module MoveWithSSReflect. + +From Coq Require Import ssreflect. + +(* For other uses of SSReflect, one may also need to uncomment the following two lines. *) +(* From Coq Require Import ssreflect ssrfun ssrbool. *) +(* Import ssreflect.SsrSyntax. *) + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Goal forall (P Q : Prop), P -> Q -> P. Proof. move=> P. move=> Q. -move=> p. -Fail move: P. (* The command "move: P" should fail here. *) -move: p. +move=> HP. +move=> HQ. +Fail move: P. (* As expected, the command "move: P" should fail here. *) +move: HQ. (* please note that HP is removed from the local context *) +move: HP. move: Q. -move: P. +move: P. (* one can keep P in the local context with: move: (P). *) move: or_comm. (* moving something from the global context *) Abort. +(* Several moves can be combined into one, as follows. *) + +Goal forall (P Q : Prop), P -> Q -> P. +Proof. +move=> P Q HP HQ. +move: or_comm P Q HP HQ. +Abort. + +End MoveWithSSReflect. + +(* With vanilla Rocq, one can move the top assumption to the local context with [intros]. *) +(* To move something from the context, one has to consider whether it comes from the local or the global context. *) +(* One can move something from the local context to top with [revert]. *) +(* One can move something from the global context to top with [generalize]. *) + +Goal forall (P Q : Prop), P -> Q -> P. +Proof. +intros P. +intros Q. +intros HP. +intros HQ. +revert HQ. +revert HP. +(* Here, the command revert P would succeed and generalise over P. *) +revert Q. +revert P. +generalize or_comm. (* moving something from the global context *) + (* alternatively: specialize or_comm. *) +(* assert ( H_or_comm := or_comm). *) +Abort. + +(* It can be simplified to: *) + +Goal forall (P Q : Prop), P -> Q -> P. +Proof. +intros P Q HP HQ. +revert P Q HP HQ. +generalize or_comm. +Abort. + +(* + One goes from a goal of the form [P] to [T -> P] where [T] is a result from the global context. + If one look at the goal only, it seems that it has been weakened. + However, it is indeed a generalisation and here follows an explanation why. + + One should look at the whole information that consists of both the context and the goal. + Initially, there is a goal [P] with some term [pr : T] in the global context. + The goal is generalised over [pr] and one gets the new goal [forall ( _ : T), P] + also written as [T -> P]. Instead of completing the goal with the specific proof [pr] + one aims at proving a universal quantification over that proof. + One should thus prefer to use the tactic [generalize] over [specialize]. + +*) + (** *** Destructing - The [move] tactic can be used in combination with destructing, whose syntax is [[]]. + The syntax for destructing is [[]]. Destructing can let one access values of a record, do a case analysis on an inductive type, split a disjunction into subgoals. - If new goals are introduced just after destructing, they are separated by the pipe symbols [|] + If new goals are introduced just after destructing, they are separated with the pipe symbols [|] within the brackets. As a result, the number of pipe symbols is the number of subgoals minus one. It is possible to use destructing within subgoals, subsubgoals and so on, - as is done with [[move=> [HQ | [HR | HS]]]]. + as is done with [[[HQ | [HR | HS]]]]. + With SSReflect, the [move] tactic can be used in combination with destructing. *) -Module Destructing. +Module SSRReflectDestructing. -From mathcomp Require Import ssrbool ssrnat. +From Coq Require Import ssreflect. (* It is better to place all import commands at the beginning of the file, contrary to what is done here. Yeah, do what I say, not as I do xD *) +Section S. Variables (T : Type) (P : T -> Prop) (y z : T). Goal (exists u : T, P u) -> y = z. @@ -127,63 +212,160 @@ Record Pair : Set := mkPair { n : nat ; b : bool}. -Lemma PairP (x : Pair) : n x <= n x + (b x). +Definition incr_pair (x : Pair) := mkPair (S (n x)) (negb (b x)). + +Lemma PairP (x : Pair) : incr_pair (incr_pair x) = mkPair (S (S (n x))) (b x). Proof. move: x. -move=> [n b]. -rewrite /=. -(* proof to be finished *) -Abort. +move=> [n b]. +by rewrite /incr_pair Bool.negb_involutive. +Qed. -Goal forall (Q R S : Prop), Q \/ R -> S. +Goal forall (Q R : Prop), Q \/ R -> R \/ Q. Proof. -move=> Q R S. +move=> Q R. move=> [HQ | HR]. -- admit. -- -Abort. +- right. + exact: HQ. +- left. + exact: HR. +Qed. -Goal forall (Q R S U : Prop), Q \/ R \/ S -> U. +Goal forall (Q R S : Prop), Q \/ R \/ S -> S \/ R \/ Q. Proof. -move=> Q R S U. +move=> Q R S. move=> [HQ | HRS]. -- admit. +- admit. (* a proof is given in the next Goal *) - move: HRS => [HR | HS]. + admit. + Abort. (** - The previous script can be shortened into: + The previous introductions can be shortened, as follows: *) -Goal forall (Q R S U : Prop), Q \/ R \/ S -> U. +Goal forall (Q R S : Prop), Q \/ R \/ S -> S \/ R \/ Q. Proof. -move=> Q R S U. +move=> Q R S. move=> [HQ | [HR | HS]]. +- by right; right. +- by right; left. +- by left. +Qed. + +End S. +End SSRReflectDestructing. + +Module Destructing. + +Section S. +Variables (T : Type) (P : T -> Prop) (y z : T). + +Goal (exists u : T, P u) -> y = z. +Proof. +intros [x Px]. +Abort. + +Record Pair : Set := mkPair + { n : nat + ; b : bool}. + +Definition incr_pair (x : Pair) := mkPair (S (n x)) (negb (b x)). + +Lemma PairP (x : Pair) : incr_pair (incr_pair x) = mkPair (S (S (n x))) (b x). +Proof. +case x. +intros n b. +unfold incr_pair. +simpl. +now rewrite Bool.negb_involutive. +Qed. + +Goal forall (Q R : Prop), Q \/ R -> R \/ Q. +Proof. +intros Q R. +intros [HQ | HR]. +- now right. +- now left. +Qed. + +Goal forall (Q R S : Prop), Q \/ R \/ S -> S \/ R \/ Q. +Proof. +intros Q R S. +intros [HQ | HRS]. - admit. -- admit. -- +- revert HRS. + intros [HR | HS]. + + admit. + + Abort. +(** + The previous script can be shortened into: +*) + +Goal forall (Q R S : Prop), Q \/ R \/ S -> S \/ R \/ Q. +Proof. +intros Q R S. +intros [HQ | [HR | HS]]. +- now right; right. +- now right; left. +- now left. +Qed. +End S. End Destructing. + (** *** Simplifying - At any stage within a proof attempt, one may want to try to simplify the goal - with the tactic [rewrite /=], - which is a special case for the [rewrite] tactic. - It is similar to the [simpl] tactic from vanilla Coq. - The tactic [rewrite /=] does not fail, even if no simplification could be done. + At any stage within a proof script, one can try to simplify the goal. + The simplification does not fail, even if no simplification could be done. + The syntax for simplification is [rewrite /=] with the SSReflect tactic and [simpl] with vanilla Rocq + (with similar but slighlty different behaviours). + The SSReflect simplification tactic is a special case for the [rewrite] tactic. - It is possible to use patterns to guide the tactic + It is possible to use patterns to guide the SSReflect tactic to simplify only some specific parts of the goal. See the section 'Rewriting pattern' for the use of patterns. - We will see that it is possible to combine moving with simplification attempt. + We will see that it is possible to combine SSReflect moving with simplification attempt. *) +(** + + At any proof step, one can start with ask to try to kill the current goal + which should be trivial for Rocq. + The SSReflect tactic [by []] tries to kill the goal - which is expected to be trivial for Rocq - otherwise it fails. + This SSReflect tactic can cover cases that require a few tactics with vanilla Rocq, + such as [reflexivity], [assumption] and [now trivial]. + + One can require a proof line to succeed in killing the current goal. + With vanilla Rocq, this is achieved by beginning the line with [now] + ([now trivial] is preferred over just [trivial], because the latter can silently fail). + +*) + +Module Simplification. + +Definition foo (b : bool) := match b with +| true => false +| false => true +end. + +Goal foo true = false. +Proof. +simpl. +reflexivity. +Qed. + +End Simplification. + +Module SSRSimplification. + +From Coq Require Import ssreflect. + Definition foo (b : bool) := match b with | true => false | false => true @@ -195,20 +377,24 @@ rewrite /=. by []. Qed. -(** +End SSRSimplification. - The tactic [by []] tries to kill the goal - which is expected to be trivial for Coq - otherwise it fails. - Some vanilla Coq tactics that cover similar cases are [reflexivity] and [assumption]. +Module SSRNonTrivialCase. -*) +From Coq Require Import ssreflect. -Module NonTrivialCase. +Goal 2 * 3 = 3 + 3. +Proof. +by []. +Qed. -From mathcomp Require Import ssrbool ssrnat. +End SSRNonTrivialCase. + +Module NonTrivialCase. Goal 2 * 3 = 3 + 3. Proof. -by []. +now simpl. Qed. End NonTrivialCase. @@ -216,28 +402,64 @@ End NonTrivialCase. (** *** Rewriting Rewriting is performed with the [rewrite] tactic. + The vanilla Rocq version of [rewrite] is loaded by default. + After having loaded SSReflect, the behaviour of [rewrite] is the one from SSReflect. Some use cases are presented below. *) (** **** Rewriting with equalities - As with the vanilla [rewrite] tactic, - one of the use cases of the [rewrite] tactic is to rewrite the goal with a given equality from the context. + The [rewrite] tactic let one rewrite the goal with a given equality from the context. Let's look at the following example. *) Goal forall (T : Type) (a b c : T) (H : a = b), a = c -> b = c. Proof. -move=> T a b c H. (* it is possible to combine several [move] into a single one *) +intros T a b c H. (* it is possible to combine several [intros] into a single one *) +rewrite H. +now trivial. +Qed. + +(** + In this proof, the last two steps can be combined into a single one with: [now rewrite H]. + One can also rewrite from right to left instead. +*) + +Goal forall (T : Type) (a b c : T) (H : a = b), a = c -> b = c. +Proof. +intros T a b c H. (* it is possible to combine several move into one *) +rewrite <-H. (* rewrites with the equality H from right to left *) +now trivial. +Qed. + +(** + A shorter version of the proof script: +*) +Goal forall (T : Type) (a b c : T) (H : a = b), a = c -> b = c. +Proof. now intros T a b c H; rewrite H. Qed. + +(** + + A similar script with the SSReflect [rewrite] tactic can be: + +*) + +Module SSRRewrite. + +From Coq Require Import ssreflect. + +Goal forall (T : Type) (a b c : T) (H : a = b), a = c -> b = c. +Proof. +move=> T a b c H. (* it is possible to combine several [intros] into a single one *) rewrite H. by []. Qed. (** In this proof, the last two steps can be combined into a single one with: [by rewrite H]. - If you want, you can try to rewrite from right to left instead. + One can also rewrite from right to left instead. *) Goal forall (T : Type) (a b c : T) (H : a = b), a = c -> b = c. @@ -253,35 +475,27 @@ Qed. Goal forall (T : Type) (a b c : T) (H : a = b), a = c -> b = c. Proof. by move=> T a b c H; rewrite H. Qed. -Module AnotherRewrite. +End SSRRewrite. -From mathcomp Require Import ssrbool ssralg ssrnum. +(** *** Unfolding a definition. -(* Import GRing.Theory Num.Theory. *) -Local Open Scope ring_scope. + Unfolding a definition is done with [rewrite /the_definition_to_be_unfolded] with SSReflect + and [unfold] with vanilla Rocq. -Variable (R : numDomainType). +*) -Lemma add_leq_right (z x y : R) : (x <= y) = (x + z <= y + z). -Proof. -(* we are going to use this admitted lemma *) -(* proving this lemma can be left as an exercice once you are more familiar with SSReflect tactics *) -(* and if you want to explore the Mathematical Components Library. *) -Admitted. +Definition secret : nat := 42. -Goal forall (x : R), x <= x. +Goal secret = 41 + 1. Proof. -move=> x. -rewrite (add_leq_right x). -Abort. - -End AnotherRewrite. - -(** *** Unfolding a definition. +unfold secret. +fold secret. (* folding back *) +now trivial. +Qed. - Unfolding a definition is done with [rewrite /the_definition_to_be_unfolded]. +Module SSRUnfolding. -*) +From Coq Require Import ssreflect. Definition secret : nat := 42. @@ -292,182 +506,235 @@ rewrite -/secret. (* folding back *) by []. Qed. -(** *** The [apply:] tactic +End SSRUnfolding. + +(** *** The [apply] tactic -The [apply:] tactic is similar to the vanilla Coq [apply] tactic. -It tries to match the conclusion (and eventually some premisses) of the lemma -with the goal. -It lets one do backward reasoning. +The [apply] tactic tries to match the conclusion (and eventually some premisses) +of the lemma being applied with the goal. It lets one do backward reasoning. +The syntax with SSReflect is [apply:] and +one can require that it should kill the goal with [exact:]. Let's look at some examples. *) -Goal forall (A B : Prop) (H : A-> B), B. +Goal forall (A B : Prop) (HA : A) (H : A-> B), B. Proof. -move=> A B H. -apply: H. -Abort. +intros A B HA H. +apply H. +assumption. +Qed. -Goal forall (A B C : Prop) (H : A -> B -> C), B -> C. +Goal forall (A B C : Prop) (HA : A) (H : A -> B -> C), B -> C. Proof. -move=> A B C H. +intros A B C HA H. +apply H. (* the premise B has been included *) +assumption. +Qed. + +Module SSReflectApply. + +From Coq Require Import ssreflect. + +Goal forall (A B : Prop) (HA : A) (H : A-> B), B. +Proof. +move=> A B HA H. +apply: H. (* or better: exact: H *) +by []. +Qed. + +Goal forall (A B C : Prop) (HA : A) (H : A -> B -> C), B -> C. +Proof. +move=> A B C HA H. apply: H. (* the premise B has been included *) -Abort. +by []. +Qed. -(** *** Generalisation *) +End SSReflectApply. -Module Generalisation. +(** *** Generalisation +The SSReflect syntax for generalising is the same as for moving things to top. *) -From mathcomp Require Import ssrbool ssralg ssrnum. -Local Open Scope ring_scope. -Variable (R : numDomainType). +Module SSRGeneralisation. -Goal (4 + 1) ^+ 2 = 4 ^+ 2 + 4 *+ 2 + 1 :> R. +Require Import Nat. +From Coq Require Import ssreflect. + +Goal (4 + 1) ^ 2 = 4 ^ 2 + 4 * 2 + 1 . Proof. move: 4. (* generalises over the term 4 *) +move=> n. Abort. -Goal 1 + 1 = 1 * 1 :> R. +Goal 1 + 1 = 1 * 1. Proof. -move: 1. (* generalises over all occurrences of 1 *) +move: 1 => n. (* generalises over all occurrences of 1 *) Abort. -Goal 1 + 1 = 1 * 1 :> R. +Goal 1 + 1 = 1 * 1. Proof. -move: {2}1. (* generalises over the second occurrence of 1 *) -move=> x. +move: {2}1 => n. (* generalises over the second occurrence of 1 *) Abort. -Goal 1 + 1 = 1 * 1 :> R. +Goal 1 + 1 = 1 * 1. Proof. -move: {2 4}1. (* generalises over the second and the forth occurrence of 1 *) -move=> x. +move: {2 4}1 => x. (* generalises over the second and the forth occurrence of 1 *) Abort. -Check list. - Goal forall (T : Type) (l : list T) (C : Prop), C. Proof. move=> T l C. move: (eq_refl (length l)). (* this illustrates moving something from the global context to top *) -move: {2}(length l). (* generalises over the second occurrence only *) -move=> n. +move: {2}(length l) => n. (* generalises over the second occurrence only *) Abort. -End Generalisation. +End SSRGeneralisation. +Module Generalisation. -(** *** Inductive reasoning +Require Import Nat. - The [induction] tactic from vanilla Coq is replaced by the [elim:] tactic. - -*) +Goal (4 + 1) ^ 2 = 4 ^ 2 + 4 * 2 + 1 . +Proof. +generalize 4. (* generalises over the term 4 *) +intros n. +Abort. -Module InductionExample. +Goal 1 + 1 = 1 * 1. +Proof. +generalize 1. (* generalises over all occurrences of 1 *) +intros n. +Abort. -Variable (T : Type). +Goal 1 + 1 = 1 * 1. +Proof. +generalize 1 at 2. (* generalises over the second occurrence of 1 *) +intros n. +Abort. -Goal forall (l : list T), False. +Goal 1 + 1 = 1 * 1. Proof. -move=> l. -elim: l. -- admit. -- move=> a l IH. +generalize 1 at 2 4. (* generalises over the second and the forth occurrence of 1 *) +intros n. +Abort. + +Goal forall (T : Type) (l : list T) (C : Prop), C. +Proof. +intros T l C. +generalize (eq_refl (length l)). (* this illustrates moving something from the global context to top *) +generalize (length l) at 2. (* generalises over the second occurrence only *) +intros n. Abort. -End InductionExample. +End Generalisation. + +(** *** Inductive reasoning + + Inductive reasoning is initiated with the [induction] tactic in vanilla Rocq + and the [elim:] tactic with SSReflect. + +*) -Module Range. +Module Induction. -From mathcomp Require Import ssrnat seq. +Require Import Lists.List. -Fixpoint range (a : nat) (n : nat) := match n with -| 0 => [::] -| m.+1 => a::(range (a.+1) m) -end. +Variable (T : Type). -(* The following code is presented with more lines than necessary *) -(* to ease playing it step-by-step. *) -Goal forall (a : nat) (n : nat), size (range a n) = n. +Goal forall (l m : list T), length (l ++ m) = length l + length m. Proof. -move=> a n. -move: a. -elim: n. (* starts induction on n *) -- (* base case *) - move=> n. - rewrite /=. - by []. -- (* inductive step *) - move=> n. - move=> IH. - move=> b. - rewrite /=. - rewrite IH. - by []. +intros l. +induction l. +- intros m. + now simpl. +- intros m. + rewrite <-app_comm_cons. + simpl. + now rewrite IHl. Qed. -(* Les preuves n'ont pas d'odeur. *) +End Induction. + +Module SSRInduction. + +From Coq Require Import ssreflect. -(* The previous script can be shortened to: *) +Section S. +Variable (T : Type). -Lemma size_range (a : nat) (n : nat) : size (range a n) = n. +Goal forall (l m : list T), length (l ++ m) = length l + length m. Proof. -move: a; elim: n => // n IHn b /=. -by rewrite IHn. +move=> l. +elim: l => //= a l IH m. +by rewrite IH. Qed. -(* The syntax [//] after [=>] in a [move] means: please remove trivial goals. *) -(* In this example, Coq is able to kill the base case as a trivial goal. *) -(* As a result, only one goal (out of two) remains after [//] and thus no pipe symbol is required. *) -(* Simplification and removing trivial goals can be combined into the syntax [//=]. *) - -End Range. +End S. +End SSRInduction. -Module InductionSequence. +Module OtherInduction. -From mathcomp Require Import ssrnat seq. +Require Import Lists.List. -Variables (l m : seq nat). +Section S. +Variable (T : Type). -Goal size (l++m) = size l + size m. +Goal forall (l m : list T), length (l ++ m) = length l + length m. Proof. -move: m. -elim: l=> // a l IH m /=. -by rewrite IH. +intros l m. +revert m. +induction l using rev_ind. (* induction is done with the inductive principle last_ind *) +- now intros m'. +- intros m'. + rewrite IHl; simpl. + rewrite <-app_assoc. + rewrite IHl; simpl. + rewrite <-PeanoNat.Nat.add_assoc. + now rewrite <-PeanoNat.Nat.add_1_l. Qed. -Check last_ind. +End S. +End OtherInduction. + +Module SSROtherInduction. -(* The result [last_ind] is an alternative induction principle *) +Require Import Lists.List. +From Coq Require Import ssreflect. + +(* The result [rev_ind] is an alternative induction principle *) (* that can be applied at the elimination step in the previous example. *) (* Instead of using the default induction principle, *) -(* the syntax [elim/last_ind:] combines elimination with view application. *) -(* Starting again from the same goal and applying the [last_ind] view: *) +(* the syntax [elim/rev_ind:] combines elimination with view application. *) +(* Starting again from the same goal and applying the [rev_ind] view: *) + +Section S. +Variable (T : Type). -Goal size (l++m) = size l + size m. +Goal forall (l m : list T), length (l ++ m) = length l + length m. Proof. +move=> l m. move: m. -elim/last_ind: l. (* elimination is done with the inductive principle last_ind *) -- by move=> m. -- move=> m a IH l. - rewrite size_rcons. - rewrite cat_rcons. +elim/rev_ind: l. (* elimination is done with the inductive principle last_ind *) +- by move=> m'. +- move=> m' a IH l'. + rewrite IH /=. + rewrite <-app_assoc. rewrite IH. rewrite /=. - by rewrite addnS. + rewrite -PeanoNat.Nat.add_assoc. + by rewrite PeanoNat.Nat.add_1_l. Qed. - -End InductionSequence. - +End S. +End SSROtherInduction. (** *** Congruence - When it is required to prove an equality between two applications of the same function, + When an equality is required between two applications of the same function, it suffices to prove that the corresponding arguments of both applications are equal. - As a Coq user, you may already uses the [congruence] tactic. - With SSReflect, the [congr] tactic is used. + With vanilla Rocq, this is achieved with the [congruence] tactic. + With SSReflect, this is achieved with the [congr] tactic. For instance, in the following examples it is required to prove [op w x = op y z]. This goal has the form of an equality with the same function applied in each member. @@ -477,8 +744,11 @@ End InductionSequence. *) -Section Congruence. +Module SSRCongruence. +From Coq Require Import ssreflect. + +Section S. Variables (T : Type) (op : T -> T -> T) (w x y z : T). Goal w = y -> x = z -> op w x = op y z. @@ -489,22 +759,40 @@ congr op. - exact: eq_xz. Qed. -(** - In the example above, it is also possible to use the [rewrite] tactic - and get around the use of congruence, this way: -*) +End S. +End SSRCongruence. + +Module Congruence. + +Section S. +Variables (T : Type) (op : T -> T -> T) (w x y z : T). Goal w = y -> x = z -> op w x = op y z. Proof. -move=> eq_wy eq_xz. -by rewrite eq_wy eq_xz. +intros eq_wy eq_xz. +congruence. Qed. +End S. +End Congruence. + +(** + In the example above, it is also possible to use the [rewrite] tactic + and get around the use of congruence. +*) + (** - If an introduced assumption is used to rewrite and then no more used, + If an assumption is used to rewrite just after being introduced and then no more used, it is possible to use the [->] syntax: *) +Module MoveAndRewrite. + +From Coq Require Import ssreflect. + +Section S. +Variables (T : Type) (op : T -> T -> T) (w x y z : T). + Goal w = y -> x = z -> op w x = op y z. Proof. move => ->. @@ -521,95 +809,159 @@ move->. by move ->. Qed. -End Congruence. +End S. +End MoveAndRewrite. + (** *** Forward reasoning - One can use the SSReflect tactic [have:] instead of the vanilla Coq tactic [assert], - to do forward reasoning. + To do forward reasoning. + one can use either the SSReflect tactic, [have:], or the vanilla Rocq tactic [assert]. - From the point of view of proof engineering with Coq, + From the point of view of proof engineering with Rocq, one generally prefers to work on the goal over working on the local context. This proof style is used in the Mathematical Components Library and is orthogonal to using SSReflect tactics. One benefit of this style is to get failure earlier when the script gets broken, - and thus it is easier to fix it. Instead of working on the local context + and thus it is easier to locate the proof steps that need to be fixed. Instead of working on the local context (for instance by using [rewrite in] on an hypothesis in the local context) it is preferable to work on it while it is still in the goal and before it is introduced to the local context. This way, one avoids relying on the names of the introduced assumptions. It may also be possible to factor some treatments and remove some subgoals right away, - which let one keep lower number of subgoals and sometimes avoid relying on the order of introduction of subgoals. + which let one keep fewer subgoals (and thus sometimes avoid relying on the order of introduction of subgoals). Pushing something to top might be changed without creating an error immediately, leading to more difficulties when maintaining the script. - This difficulty can be more apparent when reusing old code or code written by others + This difficulty can be more apparent when one needs to fix a proof script + to reuse old code or code written by others (and even more if one is just a user of the code and needs to fix a proof script). Still, one may want to use forward reasoning occasionally. - The main SSReflect forward reasoning tactic is [have:]. *) -Goal False. +Goal forall (n : nat), n * n = 0 -> n + 1 = 1. Proof. -have : 0 = 0. -- by []. -- move=> H. -Abort. +intros n Hn. +assert (n = 0). +- apply PeanoNat.Nat.eq_square_0. + assumption. +- rewrite H. + trivial. +Qed. + +Module ForwardReasoningWithSSReflect. + +From Coq Require Import ssreflect. -Goal False. +Goal forall (n : nat), n * n = 0 -> n + 1 = 1. Proof. -have H : 0 = 0. (* syntax to give a name to the introduced intermediate result *) -- by []. -- -Abort. +move=> n Hn. +have: n = 0. +- by apply/PeanoNat.Nat.eq_square_0. (* this is a view application *) +- by move ->. +Qed. + +(* It can be written more shortly: *) + +Goal forall (n : nat), n * n = 0 -> n + 1 = 1. +Proof. +move=> n /PeanoNat.Nat.eq_square_0 Hn. (* move + view application *) +by have: n = 0 => // ->. +Qed. + +(* In this example, it is better to avoid forward reasoning. *) + +Goal forall (n : nat), n * n = 0 -> n + 1 = 1. +Proof. by move=> n /PeanoNat.Nat.eq_square_0 ->. Qed. + +End ForwardReasoningWithSSReflect. (** The [have:] tactic can be combined with destructing [[]] and with rewriting [->]. Below are some examples: *) -Module MoreHave. +Module MoreForwardReasoning. +(* From Coq Require Import ssreflect. *) -From mathcomp Require Import ssrbool eqtype ssrnat. +Section S. -Local Open Scope nat_scope. +Require Import List. -Variables (P : nat -> nat -> bool) (m n : nat). +Variable (T : Type). +Hypothesis eq_dec : forall x y : T, {x = y} + {x <> y}. -Goal P m n. +Lemma nodupIn (a : T) (l : list T) : + In a l -> nodup eq_dec (a :: l) = nodup eq_dec l. Proof. -move: (eqVneq m n). -Print eq_xor_neq. -move=> [eq_mn|neq_mn]. -- rewrite eq_mn. - admit. -- -Abort. +intros In_al. +simpl. +now case (in_dec eq_dec a l); intros H; trivial. +Qed. -(** - The above code can be simplified into: -*) +Goal forall (x y : T) (l : list T), + List.nodup eq_dec (x::(y::l)) = if (eq_dec x y) + then List.nodup eq_dec (x::l) + else List.nodup eq_dec (x::(y::l)). +Proof. +intros x y l. +generalize (eq_dec x y). +intros [eq_xy|neq_xy]. +- rewrite eq_xy. + clear eq_xy. + rewrite nodupIn; last exact (in_eq y l). + reflexivity. +- reflexivity. +Qed. + +End S. +End MoreForwardReasoning. -Goal P m n. +Module MoreSSRForwardReasoning. +From Coq Require Import ssreflect. + +Section S. + +Require Import List. + +Variable (T : Type). +Hypothesis eq_dec : forall x y : T, {x = y} + {x <> y}. + +Lemma nodupIn (a : T) (l : list T) : + In a l -> nodup eq_dec (a :: l) = nodup eq_dec l. Proof. -move: (eqVneq m n) => [->|neq_mn]. -- admit. -- -Abort. +move=> In_al /=. +by case: (in_dec eq_dec a l). +Qed. -End MoreHave. +Goal forall (x y : T) (l : list T), + List.nodup eq_dec (x::(y::l)) = (if (eq_dec x y) + then List.nodup eq_dec (x::l) + else List.nodup eq_dec (x::(y::l)))%GEN_IF. +Proof. +move=> x y l. +have [->|neq_xy] := eq_dec x y. +- rewrite nodupIn; first exact: (in_eq y l). + by case: (eq_dec y y). +- by case: (eq_dec x y). +Qed. + +End S. +End MoreSSRForwardReasoning. (** *** Changing view - - Changing view - also called view application - is performed on the first assumption with the tactic [move/] + + View change - also called view application - is performed on the top assumption with the SSReflect tactic [move/] or on the conclusion with the tactic [apply/]. It replaces it with a "different view". - The first assumption can be replaced with a weaker asumption - and the conclusion can be replaced with a stronger conclusion. + The conclusion can be replaced with a stronger conclusion + and the top assumption can be replaced with a weaker asumption (when it is not the conclusion). One specific case of view application results are reflection results (which use the [reflect] keyword). - A reflection establishes the equivalence between a proposition and a boolean. - In this context, a boolean can always be coerced to a proposition with the coercion [is_true]. + A reflection establishes the equivalence between a proposition and a boolean + (the truth of the proposition is thus decidable). + In this context, a boolean can always be coerced to a proposition + and this is done with the coercion [is_true] on the Mathematical Components Library. By exploiting a reflection result, a proposition can be replaced with an equivalent boolean and conversely a boolean can be replaced with an equivalent proposition. This is part of the Small Scale Reflection methodology. @@ -622,6 +974,9 @@ End MoreHave. Module ChangingView. +From Coq Require Import ssreflect. + +Section S. Variables (A B C D E : Prop). Hypothesis (H : B -> C). @@ -637,32 +992,37 @@ apply/H. (* strenghten C to B *) move: HA. Abort. +Hypothesis (H2 : D -> (B -> C)). + +Goal A -> B -> C. +Proof. +move=> A' /=. +apply/H2. +Abort. + (* These examples also work with equivalence instead of implication. *) -Hypothesis (H' : B <-> C). +Hypothesis (H3 : B <-> C). Goal B -> D -> E. Proof. -move/H'. (* weakens B to C *) +move/H3. (* weakens B to C *) Abort. Goal A -> C. Proof. move=> HA. -apply/H'. (* strenghten C to B *) +apply/H3. (* strenghten C to B *) move: HA. Abort. -End ChangingView. - (* Some examples of view changing are now shown with boolean reflection. *) -Module BooleanReflection. From mathcomp Require Import ssrbool ssrnat. Check minn_idPr. @@ -680,7 +1040,7 @@ Abort. Goal minn m n = n -> P. Proof. -move/minn_idPr=> H. +move/minn_idPr=> H'. Abort. (* @@ -694,37 +1054,65 @@ Abort. Goal P -> minn m n = n. Proof. -move=> H. +move=> H'. apply/minn_idPr. Abort. Goal P -> n <= m. Proof. -move=> H. +move=> H'. apply/minn_idPr. Abort. -End BooleanReflection. +End S. +End ChangingView. + +Module ChangingViewVanillaCoq. + +Variables (P Q R : Prop). +Hypothesis (H : P <-> Q). + +Goal P. +Proof. +apply H. +(* apply <- H. *) +Abort. + +Goal Q. +Proof. +apply H. +(* apply -> H. *) +Abort. + +End ChangingViewVanillaCoq. + (** Rewriting pattern. *) (** - SSReflect offers rewrite patterns to guide Coq to select specific matches for a rewrite. - Otherwise the first match is selected, which is not necessarly the desired effect. + SSReflect offers rewrite patterns to guide Rocq to select specific matches for a rewrite. + By default (when no pattern is specified) the first match is selected, which is not necessarly the desired effect. Please not that match and occurence differs. A pattern has several matches - eventually none - and each match has one or multiple occurrences. Let's look at some examples. *) -Module RewritePatterns. +Module SSReflectRewritePatterns. -From mathcomp Require Import ssrbool ssralg ssrnum. +From Coq Require Import ssreflect. -(* Import GRing.Theory Num.Theory. *) -Local Open Scope ring_scope. +Section S. -Variables (R : ringType) (a b c : R). -Hypothesis H : forall (x : R), x = c. +Variable (T : Type). +Variables (add mul : T -> T -> T). + +Local Notation "x + y" := (add x y). +Local Notation "x * y" := (mul x y). + +Variable (c : T). +Hypothesis H : forall (x : T), x = c. + +Variables (a b : T). Goal (a + b) * a + (a + b + a) * b = (b + b) * a + (a + b + b) * a * b. Proof. @@ -772,10 +1160,13 @@ Proof. rewrite [X in (_ + _)* _ + (_ + X + _)* _ * _]H. Abort. -End RewritePatterns. +End S. -Module SomeMorePatterns. +End SSReflectRewritePatterns. +Module SomeMoreSSReflectPatterns. + +From Coq Require Import ssreflect. From mathcomp Require Import ssrbool ssrnat order. Local Open Scope nat_scope. @@ -795,39 +1186,89 @@ Proof. rewrite [ltRHS]H. Abort. -End SomeMorePatterns. +End SomeMoreSSReflectPatterns. -(** ** 3. More SSReflect tactics +(** ** 3. More tactics *) (** *** Case analysis - The SSReflect tactic for case analysis is [case:]. - The colon punctuation mark at the end of [case:] distinguishes it - from the [case] tactic from vanilla Coq. + Case analysis is performed with [case] with vanilla Rocq + and with [case:] with SSReflect. + The colon punctuation mark at the end of [case:] distinguishes both tactics. *) -Goal forall (n : nat), n + n = n. +Module CaseAnalysis. +Section S. + +Variables (a b : nat). + +Definition f n := match n with + | 0 => a + | S n => b + n +end. + +Require Import Nat. +Goal forall (n : nat), f n <= max a (b + n). +Proof. +intros n. +case n. +(* the goal is splitted into two goals *) +- simpl. + rewrite PeanoNat.Nat.add_0_r. + exact (PeanoNat.Nat.le_max_l a b). +- intros m. + simpl. + apply (PeanoNat.Nat.le_trans _ _ _ (ssreflect.iffLR (PeanoNat.Nat.add_le_mono_l _ _ _) (PeanoNat.Nat.le_succ_diag_r _))). + exact (PeanoNat.Nat.le_max_r a (b + S m)). +Qed. + +End S. +End CaseAnalysis. + +Module SSReflectCase. + +From Coq Require Import ssreflect. + +Section S. + +Variables (a b : nat). + +Definition f n := match n with + | 0 => a + | S n => b + n +end. + +Require Import Nat. +Goal forall (n : nat), f n <= max a (b + n). Proof. move=> n. case: n. (* the goal is splitted into two goals *) - rewrite /=. - by []. -- move=> n. -Abort. + rewrite PeanoNat.Nat.add_0_r. + exact: (PeanoNat.Nat.le_max_l a b). +- move=> m. + rewrite /=. + apply: (PeanoNat.Nat.le_trans _ _ _ (ssreflect.iffLR (PeanoNat.Nat.add_le_mono_l _ _ _) (PeanoNat.Nat.le_succ_diag_r _))). + exact: (PeanoNat.Nat.le_max_r a (b + S m)). +Qed. -(** The previous script can be written more shortly as follows -*) +(* The previous script can be simplified as follows: *) -Goal forall (n : nat), n + n = n. +Require Import Nat. +Goal forall (n : nat), f n <= max a (b + n). Proof. -move=> n. -case: n=> [|n]. (* the pipe symbol '|' separates each subgoal *) -(* the goals is splitted into two goals *) -- by []. -Abort. +move=> /= [|n]. +- rewrite PeanoNat.Nat.add_0_r. + exact: (PeanoNat.Nat.le_max_l a b). +- apply: (PeanoNat.Nat.le_trans _ _ _ (ssreflect.iffLR (PeanoNat.Nat.add_le_mono_l _ _ _) (PeanoNat.Nat.le_succ_diag_r _))). + exact: (PeanoNat.Nat.le_max_r a (b + S n)). +Qed. + +End S. + (** It is possible to combine moving ([move =>]) @@ -836,34 +1277,69 @@ Abort. Thus, only one goal remains and [n] can be introduced without using the pipe symbol. *) -Goal forall (n : nat), n + n = n. -Proof. -move=> n. -case: n=> // n. -Abort. +End SSReflectCase. (** *** Specialising - One can always weaken the top assumtpion by specialising it. - With vanilla Coq, this can be achieved with the [specialize] tactic. + One can always weaken the top assumption by specialising it. + With vanilla Rocq, this can be achieved with the [specialize] tactic. With SSReflect, it can be achieved as a special case of view application, with the syntax [/(_ value)]. In the following example, the assumption [forall y, P y] is specialised with [x], which results in the asumption [P x]. *) -Goal forall (T G : Type) (P : T -> Prop) (x : T), (forall y, P y) -> G. +Module Specialise. + +Section S. +Variables (T : Type) (P : T -> Prop) (Q : Prop) (a : T). +Hypothesis H : P a -> Q. + +Goal (forall (x : T), P x) -> Q. Proof. -move=> T G P x. -move/(_ x). -Abort. +intros H'. +specialize (H' a). +apply H. +assumption. +Qed. + +End S. +End Specialise. + + +Module SSReflectspecialise. + +From Coq Require Import ssreflect. + +Section S. +Variables (T : Type) (P : T -> Prop) (Q : Prop) (a : T). +Hypothesis H : P a -> Q. + +Goal (forall (x : T), P x) -> Q. +Proof. +move/(_ a). +exact: H. +Qed. + +End S. +End SSReflectspecialise. (** *** Discarding top - Discarding the top assumption can be achieved with [move=> _] + Discarding the top assumption can be achieved by introducing it with [_] instead of a proper name. + With SSReflect, this writes [move=> _] and with vanilla Rocq this writes [intros _]. as in the following example. *) +Goal forall (P Q : Prop), P -> Q -> P. +Proof. +intros P Q HP _. +exact HP. +Qed. + +Module SSReflectDiscard. + +From Coq Require Import ssreflect. Goal forall (P Q : Prop), P -> Q -> P. Proof. @@ -871,13 +1347,20 @@ move=> P Q HP _. exact: HP. Qed. +End SSReflectDiscard. + (** - Discarding something from the local context is achieved with the syntax [move=> {somehting}]. + One can also discard something from the local context. + It may be interesting to do so to keep a smaller local context + and to emphasise that it is not used anymore in the proof. + With SSReflect, this is achieved with the syntax [move=> {something}]. + With vanilla Rocq, one can do it with the [clear] tactic. Here is an example: *) -Module DiscardFromLocalContext. +Module SSReflectDiscardFromLocalContext. +From Coq Require Import ssreflect. From mathcomp Require Import ssrbool eqtype ssralg ssrnum. Import GRing.Theory Num.Theory. Local Open Scope ring_scope. @@ -891,16 +1374,34 @@ move=> x_neq_0. rewrite -mulrA. rewrite mulfV. - move=> {x_neq_0}. (* we can discard x_neq_0 here *) - (* it may be interesting to do so in a longer script *) by rewrite mulr1. - exact: x_neq_0. Qed. +End SSReflectDiscardFromLocalContext. + +Module DiscardFromLocalContext. + +Variables (P Q R : Prop). + +Goal P -> (P -> Q) -> (Q -> R) -> R. +Proof. +intros HP HPQ HQR. +apply HQR. +clear HQR. +apply HPQ. +clear HPQ. +exact HP. +Qed. + End DiscardFromLocalContext. (** ** 4. Exercices + with SSReflect. *) +From Coq Require Import ssreflect. + (** *** Exercice 1 For this exercice, you may want to use the vanilla tactic [split]. *) @@ -938,16 +1439,3 @@ Lemma div2nSn (n : nat) : 2 %| n * n.+1. Proof. by rewrite dvdn2 oddM /= andbN. Qed. End Exercice3. - -(** ** Where to go from here - - One may try to port one proof script from vanilla Coq to SSReflect and see the difference. - In addition to using SSReflect tactics, - one may start reusing some results from the Mathematical Components Library. - - Finally, one may get inspiration from the Mathematical Component Library for their own formalisation. - This includes Small Scale Reflection methodology and SSReflect coding conventions. - Some ingredients are boolean reflection, structures with decidable equality - and hierarchy of structures (with Hierarchy Builder). - -*) From 48f522422c74fc14c734b7cdcc7aa918c30f5389 Mon Sep 17 00:00:00 2001 From: grianneau <> Date: Mon, 26 Aug 2024 15:45:19 +0200 Subject: [PATCH 5/5] fix typo --- src/Tutorial_SSReflect_tactics.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Tutorial_SSReflect_tactics.v b/src/Tutorial_SSReflect_tactics.v index 2f0ee886..7d331089 100644 --- a/src/Tutorial_SSReflect_tactics.v +++ b/src/Tutorial_SSReflect_tactics.v @@ -160,9 +160,9 @@ revert P Q HP HQ. generalize or_comm. Abort. -(* +(** One goes from a goal of the form [P] to [T -> P] where [T] is a result from the global context. - If one look at the goal only, it seems that it has been weakened. + If one looks at the goal only, it seems that it has been weakened. However, it is indeed a generalisation and here follows an explanation why. One should look at the whole information that consists of both the context and the goal.