From cdcce0019f8a33fd451ae826f953efe6a3d34fbe Mon Sep 17 00:00:00 2001 From: Thomas Lamiaux Date: Mon, 23 Dec 2024 05:06:32 +0100 Subject: [PATCH 01/18] sec1 --- src/Tutorial_intro_patterns.v | 212 ++++++++++++++++++++++++++++++++++ 1 file changed, 212 insertions(+) create mode 100644 src/Tutorial_intro_patterns.v diff --git a/src/Tutorial_intro_patterns.v b/src/Tutorial_intro_patterns.v new file mode 100644 index 00000000..c97e0f54 --- /dev/null +++ b/src/Tutorial_intro_patterns.v @@ -0,0 +1,212 @@ +(** * Tutorial: Intro Patterns + + *** Main contributors + + - Thomas Lamiaux + + *** Summary + + In this tutorial, we explain how to use intro patterns to write more concise code. + + *** Table of content + + - 1. Introducing Variables + - 2. Destructing Variables + - 3. Rewriting and Injection + - 3. Applying Lemma + - 4. + + *** Prerequisites + + Needed: + - No Prerequisites + + Not Needed: + - No Prerequisites + + Installation: + - Available by default with coq + +*) + +From Coq Require Import List. +Import ListNotations. + + +(** ** 1. Introducing Variables *) + +(** The basic tactic to introduces variables is [intros]. In its most basic forms + [intros x y ... z] will introduce as much variables as mentioned with the + names specified [x], [y], ..., [z]. Note, it will fail if one of the names + is already used. +*) + +Goal forall n m, n < m -> n <= m. +Proof. + intros n m H. +Abort. + +Goal forall n m, n < m -> n <= m. +Proof. + Fail intros n n H. +Abort. + +(** It can happen that we have an hypothesis to introduce that is not useful + to our proof. In this case, rather than introducing it we would rather like + to directly forget it. This is possible using the wildcard pattern [_]. + Note that logically it is not possible to forget an hypothesis that appear + in the conclusion. +*) + +Goal forall n m, n = 0 -> n < m -> n <= m. +Proof. + intros n m _ H. +Abort. + +Goal forall n m, n < m -> n <= m. +Proof. + Fail intros _ m H. +Abort. + + +(** In some cases, we do not wish to choose a name and would rather have Coq to + choose a name for us. This is possible with the [?] pattern. +*) + +Goal forall n m, n < m -> n <= m. +Proof. + intros n m ?. +Abort. + +(** However, be careful that referring explicitly to auto-generated names in a + proof is bad practice as later modification to the file could change the + generated names, and hence break the proof. This can happen very fast. + Auto-generated names should hence only be used in combination with tactic + like [assumption] that do not rely on names. +*) + +(** Similarly, it happens that we want to introduce all the variables, and + do not want to name them. In this case, it possible to simply write [intros] + or as an alias [intros **] +*) + +Goal forall n m, n < m -> n <= m. +Proof. + intros. +Abort. + +Goal forall n m, n < m -> n <= m. +Proof. + intros **. +Abort. + +(** As a variant [intros *] will introduce all the variables that do no appear + dependently in the rest of the goal. In this example, it will hence introduce + [n] and [m] but not [n < m] as it depends on [n] and [m]. +*) + +Goal forall n m, n < m -> n <= m. +Proof. + intros *. +Abort. + +(** An important difference between [intros] and [intros ?x] is that [intros] + is to be understood as "introduce as much variables as you see" whereas + [intros ?X] is to be understood as "introduce exactly one variable". + [intros] will hence introduce as much variables as possible without + simplifying the goal, whereas [intros ?x] will first compute the head normal + form before trying to introduce a variable. + + For instance, consider the definition that a relation is reflexive. +*) + +Definition Reflexive {A} (R : A -> A -> Prop) := forall a, R a a. + +(** If we try to prove that logical equivalence is reflexive by using [intros] + then nothing will happen as [Reflexive] is a constant, and it needs to + be unfolded for a variable to introduce to appear. + However, as [intros ?x] simplify the goal first, it will succed and progress: +*) + +Goal Reflexive (fun P Q => P <-> Q). + Fail progress intros. intros P. +Abort. + + + +(** ** 2. Destructing Variables *) + +(* constructor *) +Definition and_comm : forall P Q, P /\ Q -> Q /\ P. + intros P Q [p q]. split. + + exact q. + + exact p. +Qed. + + + + +(* disjunction *) +Definition or_comm : forall P Q, P \/ Q -> Q \/ P. +Proof. + intros P Q [p | q]. + + right. exact p. + + left. exact q. +Qed. + + + +(** ** 3. Rewriting Lemmas *) + +(** It is common when introducing variables that we introduce an equality that + we wish to later rewite the goal by. *) +Goal forall n m, n = 0 -> n + m = m. +Proof. + intros n m H. rewrite H. cbn. reflexivity. +Qed. + +(** It is so common that there is an intro patterns to do this automatically for us. + Writing [->] or [<-] will introduce [H] then rewrite in the goal then + clear it from the context. *) +Goal forall n m, n = 0 -> n + m = m. +Proof. + intros n m ->. cbn. reflexivity. +Qed. + +Goal forall n m, 0 = n -> n + m = m. +Proof. + intros n m <-. cbn. reflexivity. +Qed. + +(** It will also rewrite the variable if it is present in the context. *) + +Goal forall n m p, n + p = m -> n = 0 -> p = m. +Proof. + intros n m p H. intros ->. cbn in *. apply H. +Qed. + +(* injection *) +Goal forall n m, S n = S 0 -> n + m = m. + intros n m H. injection H. intros H'. rewrite H'. cbn. reflexivity. +Qed. + +Goal forall n m, S n = S 0 -> n + m = m. + intros n m [=]. rewrite H0. cbn. reflexivity. +Qed. + +Goal forall n m, S n = S 0 -> n + m = m. + intros n m [= ->]. cbn. reflexivity. +Qed. + + + +(* 4. Views *) + + +Theorem app_eq_unit {A} (x y:list A) (a:A) : + x ++ y = [a] -> x = [] /\ y = [a] \/ x = [a] /\ y = []. +Proof. + destruct x; cbn. + - intros ->. left. easy. + - intros [= -> [-> ->]%app_eq_nil]. right. easy. +Qed. \ No newline at end of file From 400f0708c4cbfe4d5e74495c672f8d710211f1ee Mon Sep 17 00:00:00 2001 From: Thomas Lamiaux Date: Mon, 23 Dec 2024 06:48:16 +0100 Subject: [PATCH 02/18] write most of sec 3 and 4 --- src/Tutorial_intro_patterns.v | 155 ++++++++++++++++++++++++++++------ 1 file changed, 128 insertions(+), 27 deletions(-) diff --git a/src/Tutorial_intro_patterns.v b/src/Tutorial_intro_patterns.v index c97e0f54..158419a3 100644 --- a/src/Tutorial_intro_patterns.v +++ b/src/Tutorial_intro_patterns.v @@ -13,8 +13,8 @@ - 1. Introducing Variables - 2. Destructing Variables - 3. Rewriting and Injection - - 3. Applying Lemma - - 4. + - 4. Simplifying Equalities + - 5. Applying Lemmas *** Prerequisites @@ -109,6 +109,16 @@ Goal forall n m, n < m -> n <= m. Proof. intros *. Abort. + +(** It is particularly practical to introduce type variables on which the goal + depends but on wish we do not want to perform any specific action but introduction + *) + +Goal forall P Q, P /\ Q -> Q /\ P. +Proof. + intros *. +Abort. + (** An important difference between [intros] and [intros ?x] is that [intros] is to be understood as "introduce as much variables as you see" whereas @@ -133,74 +143,165 @@ Goal Reflexive (fun P Q => P <-> Q). Abort. +(** ** 2. Destructing Variables -(** ** 2. Destructing Variables *) + When proving properties, it is very common to introduce variables only to + pattern-match on them just after, e.g to properties about an inductive type + or simplify an inductively defined function: +*) -(* constructor *) -Definition and_comm : forall P Q, P /\ Q -> Q /\ P. - intros P Q [p q]. split. - + exact q. - + exact p. +Goal forall P Q, P /\ Q -> Q /\ P. + intros P Q x. destruct x. split. + + assumption. + + assumption. Qed. +Goal forall P Q, P \/ Q -> Q \/ P. +Proof. + intros P Q x. destruct x. + + right. assumption. + + left. assumption. +Qed. + +(** Consequently, Coq as special intro patterns [ [] ] to introduce and pattern + match on a variable at the same time. If the inductive type only has one + constructor like [/\], it suffices to list the names of the variables: +*) +Goal forall P Q, P /\ Q -> Q /\ P. + intros P Q [p q]. split. + + assumption. + + assumption. +Qed. +(** In the general case with several constructors, it suffices to add branches + delimited by [ | ] in the pattern for each constructors: +*) -(* disjunction *) -Definition or_comm : forall P Q, P \/ Q -> Q \/ P. +Goal forall P Q, P \/ Q -> Q \/ P. Proof. intros P Q [p | q]. - + right. exact p. - + left. exact q. + + right. assumption. + + left. assumption. +Qed. + +(** Note that destructing over [False] expects nothing no branche as [False] has + no constructors, and that it solves the goal automatically: +*) + +Goal forall P, False -> P. +Proof. + intros P []. Qed. +(** It is further possible to nest the intro-patterns when inductive type are + nested into each other, e.g. like a sequence of +*) + +Goal forall P Q R, P /\ Q /\ R -> R /\ Q /\ P. + intros P Q R [p [q r]]. +Abort. + +(** In practice, two patterns comes up so often that they have dedicated patterns. + The first one is for iterated binary inductive types like [/\]. + Rather than having to destruct recursively as [ [p [q [r h]]] ], we can + instead simply write [p & q & r & h]: *) + +Goal forall P Q R H, P /\ Q /\ R /\ H -> H /\ R /\ Q /\ P. +Proof. + intros * (p & q & r & h). +Abort. + +(** The second pattern is for inductive types that only have one constructor, + like records. In this case, it is possible to write [(a, b, ..., d)] rather + than [ [a b ... d]]. The interrest is that it enables to preserves [let-in] + if there are any: +*) + +(* Record Foo := { + foo1 : nat; + foo2 : nat; + foo12 := foo1 + foo2; + foo_inf : foo12 = 10 +}. *) + +Inductive Foo := + foo : forall n m, let p := n + m in p = 10 -> Foo. + +Goal Foo -> {n & {m | n + m = 10}}. +Proof. intros (n, m, H). Abort. + +Goal Foo -> {n & {m | n + m = 10}}. +Proof. intros [n m H]. Abort. + +(* TO FIX !!! => do not match refman ! *) (** ** 3. Rewriting Lemmas *) (** It is common when introducing variables that we introduce an equality that - we wish to later rewite the goal by. *) + we wish to later rewrite: +*) + Goal forall n m, n = 0 -> n + m = m. Proof. intros n m H. rewrite H. cbn. reflexivity. Qed. -(** It is so common that there is an intro patterns to do this automatically for us. - Writing [->] or [<-] will introduce [H] then rewrite in the goal then - clear it from the context. *) -Goal forall n m, n = 0 -> n + m = m. +(** It is so common that there is an intro patterns dedicated to that. + Writing [->] or [<-] will introduce [H] then rewrite it and in the context, + then clear it from the context. +*) + +Goal forall n m p, n + p = m -> n = 0 -> p = m. Proof. - intros n m ->. cbn. reflexivity. + intros n m p H ->. cbn in *. apply H. Qed. -Goal forall n m, 0 = n -> n + m = m. +Goal forall n m p, n + p = m -> 0 = n -> p = m. Proof. - intros n m <-. cbn. reflexivity. + intros n m p H <-. cbn in *. apply H. Qed. -(** It will also rewrite the variable if it is present in the context. *) +(** ** 4. Simplifying Equalities -Goal forall n m p, n + p = m -> n = 0 -> p = m. -Proof. - intros n m p H. intros ->. cbn in *. apply H. -Qed. + It is also very common that we have an equality as to introduce . + Most often, we want to simplify this equality using [injection] then rewrite + by it. +*) -(* injection *) Goal forall n m, S n = S 0 -> n + m = m. intros n m H. injection H. intros H'. rewrite H'. cbn. reflexivity. Qed. +(** This is possible by using the [ [=] ] pattern that will introduce + an equality then simplify it with [injection]: + *) + Goal forall n m, S n = S 0 -> n + m = m. intros n m [=]. rewrite H0. cbn. reflexivity. Qed. +(** It is then possible to combine it with the intro pattern for rewriting to + directly simplify the goal: *) + Goal forall n m, S n = S 0 -> n + m = m. intros n m [= ->]. cbn. reflexivity. Qed. +(** Another way of simplifying an equality is when it is absurd like [S n = 0] + in which case we can prove the goal automatically using [discriminate]. + This is also possible autimatically thanks to the [=] pattern: +*) + +Goal forall n, S n = 0 -> False. +Proof. + intros n [=]. +Qed. + -(* 4. Views *) +(** ** 5. Applying Lemmas *) Theorem app_eq_unit {A} (x y:list A) (a:A) : From aeacd91d426922054c563522ec6eacefc8ed102f Mon Sep 17 00:00:00 2001 From: Thomas Lamiaux Date: Mon, 23 Dec 2024 08:40:47 +0100 Subject: [PATCH 03/18] some work on section 5 --- src/Tutorial_intro_patterns.v | 92 ++++++++++++++++++++++++++++++++--- 1 file changed, 84 insertions(+), 8 deletions(-) diff --git a/src/Tutorial_intro_patterns.v b/src/Tutorial_intro_patterns.v index 158419a3..24649990 100644 --- a/src/Tutorial_intro_patterns.v +++ b/src/Tutorial_intro_patterns.v @@ -265,7 +265,7 @@ Qed. (** ** 4. Simplifying Equalities - It is also very common that we have an equality as to introduce . + It is also very common that we have an equality to introduce . Most often, we want to simplify this equality using [injection] then rewrite by it. *) @@ -291,7 +291,7 @@ Qed. (** Another way of simplifying an equality is when it is absurd like [S n = 0] in which case we can prove the goal automatically using [discriminate]. - This is also possible autimatically thanks to the [=] pattern: + This is also possible automatically thanks to the [=] pattern: *) Goal forall n, S n = 0 -> False. @@ -301,13 +301,89 @@ Qed. -(** ** 5. Applying Lemmas *) +(** ** 5. Applying Lemmas + A situation that often arises when proving properties is to we have an + hypothesis to introduce that we need to transform by applying lemmas to it + before being able to use it. -Theorem app_eq_unit {A} (x y:list A) (a:A) : - x ++ y = [a] -> x = [] /\ y = [a] \/ x = [a] /\ y = []. + For instance, consider the following example where we know that [length l1 = 0]. + To conclude that [l1 ++ l2 = l2, we must prove that [l1 = []] by applying + [length_zero_iff_nil] to [length l1 = 0], then rewriting it: +*) + +Goal forall A (l1 l2 : list A), length l1 = 0 -> l1 ++ l2 = l2. +Proof. + intros A l1 l2 H. apply length_zero_iff_nil in H. rewrite H. cbn. reflexivity. +Qed. + +(** To help us do this, there is an intro pattern [?x/H] that introduce the + variable [x] and apply the lemma [H] to it. We can hence write + [intros H%length_zero_iff_nil] rather than [intros H. apply length_zero_iff_nil in H]. +*) + +Goal forall A (l1 l2 : list A), length l1 = 0 -> l1 ++ l2 = l2. +Proof. + intros A l1 l2 H%length_zero_iff_nil. rewrite H. cbn. reflexivity. +Qed. + +(** We can then further combine it with rewrite patterns to simplify the proof: +*) + +Goal forall A (l1 l2 : list A), length l1 = 0 -> l1 ++ l2 = l2. +Proof. + intros A l1 l2 ->%length_zero_iff_nil. cbn. reflexivity. +Qed. + +(** For a more concrete example of how intro patterns can be useful, consider + the following example asserting that the concatenation of two list has one + element if and only if one has one element and the other is empty. + + In the first direction, we get an equality [a1::l1++l2 = [a]] that we have + to simplify to [a1 = a] and [l1 ++ l2 = []] with injection, then to [l1 = []] + and [l2 = []] and rewrite. + This creates a load overhead as introduction and operations are duplicated, + and we have to introduce fresh names that do not matters in the end. + Similarly, in the converse direction. +*) + +Goal forall {A} (l1 l2 : list A) (a : A), + l1 ++ l2 = [a] <-> l1 = [] /\ l2 = [a] \/ l1 = [a] /\ l2 = []. +Proof. + intros A l1 l2 a. split. + + destruct l1; cbn. + - intros H. rewrite H. left. split; reflexivity. + - intros H. injection H. intros H1 H2. rewrite H2. apply app_eq_nil in H1. + destruct H1 as [H3 H4]. rewrite H3, H4. right. split; reflexivity. + + intros H. destruct H as [H | H]. + - destruct H as [H1 H2]. rewrite H1, H2. reflexivity. + - destruct H as [H1 H2]. rewrite H1, H2. reflexivity. +Qed. + +(** Using intros patterns we can significantly shorten this proof and make it + more intuitive, getting rid of tedious manipulations of hypothesis. + + In the first direction and the second case, we can use the intro pattern + [[=]] to simplify the equality [a1::l1++l2 = [a]] to [a1 = a] and [l1 ++ l2 + = []]. We can then rewrite the first equality with [->], and simplify the + second equality to [l1 = [] /\ l2 = []] thanks to [%app_eq_nil]. Finally, we + can rewrite both equality using [->], giving us the intro pattern [intros [= + -> [-> ->]%app_eq_nil]]. + + In the converse direction, we can use intro patterns to decompose the + hypothesis into [[H1 H2 | H1 H2]], and as they are equalities rewrite them + with [->]. This gives the intro pattern [intros [[-> ->]| [-> ->]]] that as + it can be seen trivialize the goal. +*) + +Goal forall {A} (l1 l2 : list A) (a : A), + l1 ++ l2 = [a] <-> l1 = [] /\ l2 = [a] \/ l1 = [a] /\ l2 = []. Proof. - destruct x; cbn. - - intros ->. left. easy. - - intros [= -> [-> ->]%app_eq_nil]. right. easy. + intros A l1 l2 a. split. + + destruct l1; cbn. + - intros ->. left. split; reflexivity. + - intros [= -> [-> ->]%app_eq_nil]. right. split; reflexivity. + + intros [[-> ->]| [-> ->]]. + - cbn. reflexivity. + - cbn. reflexivity. Qed. \ No newline at end of file From acecc89bc1548c257d22a4ac1831152fd01bc09a Mon Sep 17 00:00:00 2001 From: Thomas Lamiaux Date: Mon, 23 Dec 2024 20:32:58 +0100 Subject: [PATCH 04/18] first draft --- src/Tutorial_intro_patterns.v | 196 +++++++++++++++++----------------- 1 file changed, 100 insertions(+), 96 deletions(-) diff --git a/src/Tutorial_intro_patterns.v b/src/Tutorial_intro_patterns.v index 24649990..e9c10d9b 100644 --- a/src/Tutorial_intro_patterns.v +++ b/src/Tutorial_intro_patterns.v @@ -6,8 +6,13 @@ *** Summary - In this tutorial, we explain how to use intro patterns to write more concise code. + In this tutorial, we explain how the tactic [intros] and its intro patterns + works enabling us to to introduce variable and at the same the same do operations + like pattern-matching or rewriting equations enabling us to write more concise code. + + In this tutorial, we explain how the tactic [intros] and its intro patterns + works enabling us to to introduce variable and at the same the same do *** Table of content - 1. Introducing Variables @@ -33,12 +38,11 @@ From Coq Require Import List. Import ListNotations. -(** ** 1. Introducing Variables *) +(** ** 1. Introducing Variables -(** The basic tactic to introduces variables is [intros]. In its most basic forms + The basic tactic to introduces variables is [intros]. In its most basic forms [intros x y ... z] will introduce as much variables as mentioned with the - names specified [x], [y], ..., [z]. Note, it will fail if one of the names - is already used. + names specified [x], [y], ..., [z], and fail if one of the names is already used. *) Goal forall n m, n < m -> n <= m. @@ -53,9 +57,8 @@ Abort. (** It can happen that we have an hypothesis to introduce that is not useful to our proof. In this case, rather than introducing it we would rather like - to directly forget it. This is possible using the wildcard pattern [_]. - Note that logically it is not possible to forget an hypothesis that appear - in the conclusion. + to directly forget it. This is possible using the wildcard pattern [_], that + will introduce and forget a variable that do do not appear in the conclusion. *) Goal forall n m, n = 0 -> n < m -> n <= m. @@ -68,9 +71,8 @@ Proof. Fail intros _ m H. Abort. - (** In some cases, we do not wish to choose a name and would rather have Coq to - choose a name for us. This is possible with the [?] pattern. + choose a name for us. This is possible with the [?] pattern. *) Goal forall n m, n < m -> n <= m. @@ -83,11 +85,10 @@ Abort. generated names, and hence break the proof. This can happen very fast. Auto-generated names should hence only be used in combination with tactic like [assumption] that do not rely on names. -*) -(** Similarly, it happens that we want to introduce all the variables, and - do not want to name them. In this case, it possible to simply write [intros] - or as an alias [intros **] + Similarly, to [?] it happens that we want to introduce all the variables + automatically and without naming them. This is possible by simply writing + [intros] or as an alias [intros **]. *) Goal forall n m, n < m -> n <= m. @@ -100,9 +101,9 @@ Proof. intros **. Abort. -(** As a variant [intros *] will introduce all the variables that do no appear - dependently in the rest of the goal. In this example, it will hence introduce - [n] and [m] but not [n < m] as it depends on [n] and [m]. +(** As a variant of [intros], [intros *] will introduce all the variables that + do no appear dependently in the rest of the goal. In this example, it will + introduce [n] and [m] but not [n < m] as it depends on [n] and [m]. *) Goal forall n m, n < m -> n <= m. @@ -110,8 +111,8 @@ Proof. intros *. Abort. -(** It is particularly practical to introduce type variables on which the goal - depends but on wish we do not want to perform any specific action but introduction +(** This is particularly practical to introduce type variables that other variables + depends upon, but that we do not want to perform any specific action on but introduction. *) Goal forall P Q, P /\ Q -> Q /\ P. @@ -119,13 +120,12 @@ Proof. intros *. Abort. - -(** An important difference between [intros] and [intros ?x] is that [intros] - is to be understood as "introduce as much variables as you see" whereas - [intros ?X] is to be understood as "introduce exactly one variable". - [intros] will hence introduce as much variables as possible without - simplifying the goal, whereas [intros ?x] will first compute the head normal - form before trying to introduce a variable. +(** An important difference between [intros] and [intros ?x] is that [intros] + introduce as much variables as possible without simplifying the goal, + whereas [intros ?x] will first compute the head normal form before trying to + introduce a variable. This difference can be intuitively understood + by considering that [intros ?x] means there is a variable to introduce, + and requires to find it. For instance, consider the definition that a relation is reflexive. *) @@ -135,7 +135,7 @@ Definition Reflexive {A} (R : A -> A -> Prop) := forall a, R a a. (** If we try to prove that logical equivalence is reflexive by using [intros] then nothing will happen as [Reflexive] is a constant, and it needs to be unfolded for a variable to introduce to appear. - However, as [intros ?x] simplify the goal first, it will succed and progress: + However, as [intros ?x] simplifies the goal first, it will succeed and progress: *) Goal Reflexive (fun P Q => P <-> Q). @@ -143,10 +143,11 @@ Goal Reflexive (fun P Q => P <-> Q). Abort. + (** ** 2. Destructing Variables When proving properties, it is very common to introduce variables only to - pattern-match on them just after, e.g to properties about an inductive type + pattern-match on them just after, e.g to prove properties about an inductive type or simplify an inductively defined function: *) @@ -163,9 +164,12 @@ Proof. + left. assumption. Qed. -(** Consequently, Coq as special intro patterns [ [] ] to introduce and pattern - match on a variable at the same time. If the inductive type only has one - constructor like [/\], it suffices to list the names of the variables: +(** To shorten the code, it is possible to do both at the same time using the + intro pattern [ [ x ... y | ... | z ... w ] where [|] enables to separate the + arguments of the different constructors. + For instance, as [/\] + + If no branches or names are specified, Coq will just use auto-generated names. *) Goal forall P Q, P /\ Q -> Q /\ P. @@ -174,10 +178,6 @@ Goal forall P Q, P /\ Q -> Q /\ P. + assumption. Qed. -(** In the general case with several constructors, it suffices to add branches - delimited by [ | ] in the pattern for each constructors: -*) - Goal forall P Q, P \/ Q -> Q \/ P. Proof. intros P Q [p | q]. @@ -185,8 +185,15 @@ Proof. + left. assumption. Qed. -(** Note that destructing over [False] expects nothing no branche as [False] has - no constructors, and that it solves the goal automatically: +Goal forall P Q, P \/ Q -> Q \/ P. +Proof. + intros P Q []. + + right. assumption. + + left. assumption. +Qed. + +(** Note that destructing over [False] expects no branches nor names as [False] + has no constructors, and that it solves the goal automatically: *) Goal forall P, False -> P. @@ -195,52 +202,37 @@ Proof. Qed. (** It is further possible to nest the intro-patterns when inductive type are - nested into each other, e.g. like a sequence of + nested into each other, e.g. like a sequence of the form: *) +Goal forall P Q R, (P \/ Q) /\ R -> P /\ R \/ Q /\ R. + intros P Q R [[p|q] r]. + + left. split; assumption. + + right. split; assumption. +Qed. + Goal forall P Q R, P /\ Q /\ R -> R /\ Q /\ P. intros P Q R [p [q r]]. Abort. -(** In practice, two patterns comes up so often that they have dedicated patterns. - The first one is for iterated binary inductive types like [/\]. - Rather than having to destruct recursively as [ [p [q [r h]]] ], we can - instead simply write [p & q & r & h]: *) + +(** Actually, the latter pattern is so common that it has a special intro-pattern. + When the goal is for the form [X Op1 Y ... Opk W] where all the binary operation + have one constructor with two arguments like [/\], then it is possible to + introduce the variables as [intros p & q & r & h] rather than by having to + destruct recursively them with [intros [p [q [r h]]] ]. +*) Goal forall P Q R H, P /\ Q /\ R /\ H -> H /\ R /\ Q /\ P. Proof. intros * (p & q & r & h). Abort. -(** The second pattern is for inductive types that only have one constructor, - like records. In this case, it is possible to write [(a, b, ..., d)] rather - than [ [a b ... d]]. The interrest is that it enables to preserves [let-in] - if there are any: -*) - -(* Record Foo := { - foo1 : nat; - foo2 : nat; - foo12 := foo1 + foo2; - foo_inf : foo12 = 10 -}. *) - -Inductive Foo := - foo : forall n m, let p := n + m in p = 10 -> Foo. - -Goal Foo -> {n & {m | n + m = 10}}. -Proof. intros (n, m, H). Abort. - -Goal Foo -> {n & {m | n + m = 10}}. -Proof. intros [n m H]. Abort. - -(* TO FIX !!! => do not match refman ! *) (** ** 3. Rewriting Lemmas *) -(** It is common when introducing variables that we introduce an equality that - we wish to later rewrite: +(** It is also very common to introduce an equality that we wish to later rewrite by: *) Goal forall n m, n = 0 -> n + m = m. @@ -248,50 +240,62 @@ Proof. intros n m H. rewrite H. cbn. reflexivity. Qed. -(** It is so common that there is an intro patterns dedicated to that. - Writing [->] or [<-] will introduce [H] then rewrite it and in the context, - then clear it from the context. +(** It is possible to do so both at the time using the intro patterns [->] or + [<-] that will introduce [H], rewrite it in the goal and context, then clear it. + It has the advantage to be much more concise, and save ourself from introducing + a name for [n = 0] that we fundamentally do not really care about: *) -Goal forall n m p, n + p = m -> n = 0 -> p = m. +Goal forall n m, n = 0 -> n + m = m. Proof. - intros n m p H ->. cbn in *. apply H. + intros n m ->. cbn. reflexivity. Qed. -Goal forall n m p, n + p = m -> 0 = n -> p = m. +Goal forall n m, 0 = n -> n + m = m. Proof. - intros n m p H <-. cbn in *. apply H. + intros n m <-. cbn. reflexivity. Qed. +Goal forall n m p, n + p = m -> n = 0 -> p = m. +Proof. + intros n m p H ->. cbn in *. apply H. +Qed. + + + (** ** 4. Simplifying Equalities - It is also very common that we have an equality to introduce . - Most often, we want to simplify this equality using [injection] then rewrite - by it. + Rewriting automatically equalities is practical but sometimes we need to + first simplify them with [injection] before being able to rewrite by them. + For instance in the example below, we have an equality [S n = 1] but + as it is [n] that appear in the conclusion, we first need to simplify the equation + with [injection] to [n = 0] before being able to rewrite it. *) -Goal forall n m, S n = S 0 -> n + m = m. +Goal forall n m, S n = 1 -> n + m = m. intros n m H. injection H. intros H'. rewrite H'. cbn. reflexivity. Qed. -(** This is possible by using the [ [=] ] pattern that will introduce - an equality then simplify it with [injection]: - *) +(** To do this automatically, there is a dedicated intro pattern [ [=] ] + that will introduce the equalities obtained simplification by [injection]. +*) Goal forall n m, S n = S 0 -> n + m = m. intros n m [=]. rewrite H0. cbn. reflexivity. Qed. (** It is then possible to combine it with the intro pattern for rewriting to - directly simplify the goal: *) + directly simplify the goal, giving us a particular simple proof. +*) Goal forall n m, S n = S 0 -> n + m = m. intros n m [= ->]. cbn. reflexivity. Qed. -(** Another way of simplifying an equality is when it is absurd like [S n = 0] - in which case we can prove the goal automatically using [discriminate]. - This is also possible automatically thanks to the [=] pattern: +(** Another particularly useful way of simplifying an equality is to deduce the + goal is true from an absurd equation like [S n = 0]. + This is usually done by introducing variables then using [discriminate], + but can also be automatically done thanks to the intro pattern [=]: *) Goal forall n, S n = 0 -> False. @@ -304,12 +308,12 @@ Qed. (** ** 5. Applying Lemmas A situation that often arises when proving properties is to we have an - hypothesis to introduce that we need to transform by applying lemmas to it + hypothesis to introduce that we need to first transform by applying lemmas to it before being able to use it. For instance, consider the following example where we know that [length l1 = 0]. - To conclude that [l1 ++ l2 = l2, we must prove that [l1 = []] by applying - [length_zero_iff_nil] to [length l1 = 0], then rewriting it: + To conclude that [l1 ++ l2 = l2, we must first prove that [l1 = []] by applying + [length_zero_iff_nil] to [length l1 = 0], then rewrite it: *) Goal forall A (l1 l2 : list A), length l1 = 0 -> l1 ++ l2 = l2. @@ -335,16 +339,16 @@ Proof. intros A l1 l2 ->%length_zero_iff_nil. cbn. reflexivity. Qed. -(** For a more concrete example of how intro patterns can be useful, consider - the following example asserting that the concatenation of two list has one - element if and only if one has one element and the other is empty. +(** For a more concrete example, consider the assertion that the concatenation of + two list has one element if and only if one has one element and the other is empty. In the first direction, we get an equality [a1::l1++l2 = [a]] that we have - to simplify to [a1 = a] and [l1 ++ l2 = []] with injection, then to [l1 = []] - and [l2 = []] and rewrite. - This creates a load overhead as introduction and operations are duplicated, - and we have to introduce fresh names that do not matters in the end. - Similarly, in the converse direction. + to simplify to [a1 = a] and [l1 ++ l2 = []] with [injection], then to [l1 = []] + and [l2 = []] with [app_eq_nil], before rewrite them. + This creates a lot over overhead as introduction and operations like destruction, + simplification and rewriting has to be done separately. + Further, at every step we have to introduce fresh names that do not + really matters in the end. *) Goal forall {A} (l1 l2 : list A) (a : A), From 96a78ba36c76e32d7c129c82384441c57cc8ef8a Mon Sep 17 00:00:00 2001 From: Thomas Lamiaux Date: Mon, 23 Dec 2024 23:45:41 +0100 Subject: [PATCH 05/18] first draft 2 --- src/Tutorial_intro_patterns.v | 33 +++++++++++++-------------------- 1 file changed, 13 insertions(+), 20 deletions(-) diff --git a/src/Tutorial_intro_patterns.v b/src/Tutorial_intro_patterns.v index e9c10d9b..9c0bc05a 100644 --- a/src/Tutorial_intro_patterns.v +++ b/src/Tutorial_intro_patterns.v @@ -6,13 +6,10 @@ *** Summary - In this tutorial, we explain how the tactic [intros] and its intro patterns - works enabling us to to introduce variable and at the same the same do operations - like pattern-matching or rewriting equations enabling us to write more concise code. + In this tutorial, we discuss intro patterns that enables us to introduce + hypothesis and to transform them at the same time, e.g. by pattern-matching + or rewriting them. This enables us to factorize and to write more direct code. - - In this tutorial, we explain how the tactic [intros] and its intro patterns - works enabling us to to introduce variable and at the same the same do *** Table of content - 1. Introducing Variables @@ -55,7 +52,7 @@ Proof. Fail intros n n H. Abort. -(** It can happen that we have an hypothesis to introduce that is not useful +(** It can happen that we have a hypothesis to introduce that is not useful to our proof. In this case, rather than introducing it we would rather like to directly forget it. This is possible using the wildcard pattern [_], that will introduce and forget a variable that do do not appear in the conclusion. @@ -165,10 +162,8 @@ Proof. Qed. (** To shorten the code, it is possible to do both at the same time using the - intro pattern [ [ x ... y | ... | z ... w ] where [|] enables to separate the - arguments of the different constructors. - For instance, as [/\] - + intro pattern [ [ x ... y | ... | z ... w ]. It enables to give a + name of each argument of each constructor separating them by [|]. If no branches or names are specified, Coq will just use auto-generated names. *) @@ -215,12 +210,11 @@ Goal forall P Q R, P /\ Q /\ R -> R /\ Q /\ P. intros P Q R [p [q r]]. Abort. - -(** Actually, the latter pattern is so common that it has a special intro-pattern. +(** Actually, the latter pattern is common enough that there is a specific intro-pattern for it. When the goal is for the form [X Op1 Y ... Opk W] where all the binary operation have one constructor with two arguments like [/\], then it is possible to introduce the variables as [intros p & q & r & h] rather than by having to - destruct recursively them with [intros [p [q [r h]]] ]. + destruct them recursively with [intros [p [q [r h]]] ]. *) Goal forall P Q R H, P /\ Q /\ R /\ H -> H /\ R /\ Q /\ P. @@ -307,13 +301,12 @@ Qed. (** ** 5. Applying Lemmas - A situation that often arises when proving properties is to we have an - hypothesis to introduce that we need to first transform by applying lemmas to it - before being able to use it. + A situation that often arises when proving properties is having a hypothesis + that we first need to transform before being able to use it. For instance, consider the following example where we know that [length l1 = 0]. - To conclude that [l1 ++ l2 = l2, we must first prove that [l1 = []] by applying - [length_zero_iff_nil] to [length l1 = 0], then rewrite it: + To conclude that [l1 ++ l2 = l2], we must first prove that [l1 = []] by + applying [length_zero_iff_nil] to [length l1 = 0], then rewrite it: *) Goal forall A (l1 l2 : list A), length l1 = 0 -> l1 ++ l2 = l2. @@ -371,7 +364,7 @@ Qed. [[=]] to simplify the equality [a1::l1++l2 = [a]] to [a1 = a] and [l1 ++ l2 = []]. We can then rewrite the first equality with [->], and simplify the second equality to [l1 = [] /\ l2 = []] thanks to [%app_eq_nil]. Finally, we - can rewrite both equality using [->], giving us the intro pattern [intros [= + can rewrite both equalities using [->], giving us the intro pattern [intros [= -> [-> ->]%app_eq_nil]]. In the converse direction, we can use intro patterns to decompose the From e7ad5cb0c68b7ee018297be94478bcef115f768d Mon Sep 17 00:00:00 2001 From: Thomas Lamiaux Date: Mon, 23 Dec 2024 23:46:29 +0100 Subject: [PATCH 06/18] typo --- src/Tutorial_intro_patterns.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Tutorial_intro_patterns.v b/src/Tutorial_intro_patterns.v index 9c0bc05a..e14ae86a 100644 --- a/src/Tutorial_intro_patterns.v +++ b/src/Tutorial_intro_patterns.v @@ -2,7 +2,7 @@ *** Main contributors - - Thomas Lamiaux + - Thomas Lamiaux, Pierre Rousselin *** Summary From f1eb5faab5b046008a3ed89112f9d4384b3162b7 Mon Sep 17 00:00:00 2001 From: Thomas Lamiaux Date: Mon, 23 Dec 2024 23:59:22 +0100 Subject: [PATCH 07/18] edit index --- src/index.html | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/index.html b/src/index.html index 099b93f1..576f5174 100644 --- a/src/index.html +++ b/src/index.html @@ -106,6 +106,12 @@

Coq Tutorials

Writing Proofs

    +
  • + Introducing Hypothesis with Intro Patterns + interactive version + and + source code +
  • Chaining Tactics to Simplify and Factorize proofs interactive version From cea5f4d32dbab3063eb809ea095657c2583154c2 Mon Sep 17 00:00:00 2001 From: Thomas Lamiaux <85848641+thomas-lamiaux@users.noreply.github.com> Date: Tue, 24 Dec 2024 16:15:14 +0100 Subject: [PATCH 08/18] Fix Pierre Courtieu's comments --- src/Tutorial_intro_patterns.v | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/Tutorial_intro_patterns.v b/src/Tutorial_intro_patterns.v index e14ae86a..9b0ede43 100644 --- a/src/Tutorial_intro_patterns.v +++ b/src/Tutorial_intro_patterns.v @@ -117,11 +117,11 @@ Proof. intros *. Abort. -(** An important difference between [intros] and [intros ?x] is that [intros] +(** An important difference between [intros] and [intros x] is that [intros] introduce as much variables as possible without simplifying the goal, - whereas [intros ?x] will first compute the head normal form before trying to + whereas [intros x] will first compute the head normal form before trying to introduce a variable. This difference can be intuitively understood - by considering that [intros ?x] means there is a variable to introduce, + by considering that [intros x] means there is a variable to introduce, and requires to find it. For instance, consider the definition that a relation is reflexive. @@ -132,7 +132,7 @@ Definition Reflexive {A} (R : A -> A -> Prop) := forall a, R a a. (** If we try to prove that logical equivalence is reflexive by using [intros] then nothing will happen as [Reflexive] is a constant, and it needs to be unfolded for a variable to introduce to appear. - However, as [intros ?x] simplifies the goal first, it will succeed and progress: + However, as [intros x] simplifies the goal first, it will succeed and progress: *) Goal Reflexive (fun P Q => P <-> Q). @@ -314,7 +314,7 @@ Proof. intros A l1 l2 H. apply length_zero_iff_nil in H. rewrite H. cbn. reflexivity. Qed. -(** To help us do this, there is an intro pattern [?x/H] that introduce the +(** To help us do this, there is an intro pattern [x%H] that introduce the variable [x] and apply the lemma [H] to it. We can hence write [intros H%length_zero_iff_nil] rather than [intros H. apply length_zero_iff_nil in H]. *) @@ -383,4 +383,4 @@ Proof. + intros [[-> ->]| [-> ->]]. - cbn. reflexivity. - cbn. reflexivity. -Qed. \ No newline at end of file +Qed. From 9401d72c95d1c7a72b3c15c9c02144e9c5110f10 Mon Sep 17 00:00:00 2001 From: Thomas Lamiaux Date: Tue, 24 Dec 2024 18:02:15 +0100 Subject: [PATCH 09/18] separate example of sec5 in two part => rewriting sec3 & views sec5 --- src/Tutorial_intro_patterns.v | 89 ++++++++++++++++++++--------------- 1 file changed, 51 insertions(+), 38 deletions(-) diff --git a/src/Tutorial_intro_patterns.v b/src/Tutorial_intro_patterns.v index e14ae86a..eea93d2e 100644 --- a/src/Tutorial_intro_patterns.v +++ b/src/Tutorial_intro_patterns.v @@ -255,6 +255,31 @@ Proof. intros n m p H ->. cbn in *. apply H. Qed. +(** For a more concrete example, consider proving that if a list has one element + and the other one is empty, then the concatenation of the two lists has one element. + The usual proof would require us to introduce the hypothesis and decompose it + into pieces before being able to rewrite and simplify the goal: +*) + +Goal forall {A} (l1 l2 : list A) (a : A), + l1 = [] /\ l2 = [a] \/ l1 = [a] /\ l2 = [] -> l1 ++ l2 = [a]. +Proof. + intros A l1 l2 a. + intros H. destruct H as [H | H]. + - destruct H as [H1 H2]. rewrite H1, H2. reflexivity. + - destruct H as [H1 H2]. rewrite H1, H2. reflexivity. +Qed. + +(** Using intro patterns to do the pattern-matching and the rewriting, we can get + a very intuitive and compact proof without having to introduce any fresh names: *) + +Goal forall {A} (l1 l2 : list A) (a : A), + l1 = [] /\ l2 = [a] \/ l1 = [a] /\ l2 = [] -> l1 ++ l2 = [a]. +Proof. + intros A l1 l2 a [[-> ->]| [-> ->]]. + - reflexivity. + - reflexivity. +Qed. (** ** 4. Simplifying Equalities @@ -332,55 +357,43 @@ Proof. intros A l1 l2 ->%length_zero_iff_nil. cbn. reflexivity. Qed. -(** For a more concrete example, consider the assertion that the concatenation of - two list has one element if and only if one has one element and the other is empty. - - In the first direction, we get an equality [a1::l1++l2 = [a]] that we have - to simplify to [a1 = a] and [l1 ++ l2 = []] with [injection], then to [l1 = []] - and [l2 = []] with [app_eq_nil], before rewrite them. - This creates a lot over overhead as introduction and operations like destruction, - simplification and rewriting has to be done separately. - Further, at every step we have to introduce fresh names that do not - really matters in the end. +(** For a more involved example, consider the converse of the example of section 3: + if the concatenation of two list has one element then one list has one + element and the other one is empty. + + After pattern matching on [l1], we have an equality [a1::l1++l2 = [a]]. We + must simplify it to [a1 = a] and [l1 ++ l2 = []] with [injection], then to + [l1 = []] and [l2 = []] with [app_eq_nil], before being able to rewrite. + This creates a lot over overhead as introduction and operations like + destruction, simplification and rewriting have to be done separately. + Further, at every step we have to introduce fresh names that do not really + matters in the end. *) Goal forall {A} (l1 l2 : list A) (a : A), - l1 ++ l2 = [a] <-> l1 = [] /\ l2 = [a] \/ l1 = [a] /\ l2 = []. + l1 ++ l2 = [a] -> l1 = [] /\ l2 = [a] \/ l1 = [a] /\ l2 = []. Proof. - intros A l1 l2 a. split. - + destruct l1; cbn. - - intros H. rewrite H. left. split; reflexivity. - - intros H. injection H. intros H1 H2. rewrite H2. apply app_eq_nil in H1. - destruct H1 as [H3 H4]. rewrite H3, H4. right. split; reflexivity. - + intros H. destruct H as [H | H]. - - destruct H as [H1 H2]. rewrite H1, H2. reflexivity. - - destruct H as [H1 H2]. rewrite H1, H2. reflexivity. + intros A l1 l2 a. destruct l1; cbn. + - intros H. rewrite H. left. split; reflexivity. + - intros H. injection H. intros H1 H2. rewrite H2. apply app_eq_nil in H1. + destruct H1 as [H3 H4]. rewrite H3, H4. right. split; reflexivity. Qed. (** Using intros patterns we can significantly shorten this proof and make it more intuitive, getting rid of tedious manipulations of hypothesis. - In the first direction and the second case, we can use the intro pattern - [[=]] to simplify the equality [a1::l1++l2 = [a]] to [a1 = a] and [l1 ++ l2 - = []]. We can then rewrite the first equality with [->], and simplify the - second equality to [l1 = [] /\ l2 = []] thanks to [%app_eq_nil]. Finally, we - can rewrite both equalities using [->], giving us the intro pattern [intros [= - -> [-> ->]%app_eq_nil]]. - - In the converse direction, we can use intro patterns to decompose the - hypothesis into [[H1 H2 | H1 H2]], and as they are equalities rewrite them - with [->]. This gives the intro pattern [intros [[-> ->]| [-> ->]]] that as - it can be seen trivialize the goal. + We can use the intro pattern [[=]] to simplify the equality [a1::l1++l2 = [a]] + to [a1 = a] and [l1 ++ l2 = []]. We can then rewrite the first equality + with [->], and simplify the second equality to [l1 = [] /\ l2 = []] thanks + to [%app_eq_nil]. Finally, we can rewrite both equalities using [->], giving + us the intro pattern [intros [= -> [-> ->]%app_eq_nil]]. + This gives a much shorter proof without a bunch of fresh names. *) Goal forall {A} (l1 l2 : list A) (a : A), - l1 ++ l2 = [a] <-> l1 = [] /\ l2 = [a] \/ l1 = [a] /\ l2 = []. + l1 ++ l2 = [a] -> l1 = [] /\ l2 = [a] \/ l1 = [a] /\ l2 = []. Proof. - intros A l1 l2 a. split. - + destruct l1; cbn. - - intros ->. left. split; reflexivity. - - intros [= -> [-> ->]%app_eq_nil]. right. split; reflexivity. - + intros [[-> ->]| [-> ->]]. - - cbn. reflexivity. - - cbn. reflexivity. + intros A l1 l2 a. destruct l1; cbn. + - intros ->. left. split; reflexivity. + - intros [= -> [-> ->]%app_eq_nil]. right. split; reflexivity. Qed. \ No newline at end of file From 47df7aa655e338bc387ecc80ba35404f65fc2829 Mon Sep 17 00:00:00 2001 From: Thomas Lamiaux <85848641+thomas-lamiaux@users.noreply.github.com> Date: Fri, 27 Dec 2024 15:43:44 +0100 Subject: [PATCH 10/18] Apply suggestions from code review Co-authored-by: Quentin VERMANDE --- src/Tutorial_intro_patterns.v | 89 ++++++++++++++++++----------------- 1 file changed, 45 insertions(+), 44 deletions(-) diff --git a/src/Tutorial_intro_patterns.v b/src/Tutorial_intro_patterns.v index 253e66d6..c4431c0f 100644 --- a/src/Tutorial_intro_patterns.v +++ b/src/Tutorial_intro_patterns.v @@ -6,8 +6,8 @@ *** Summary - In this tutorial, we discuss intro patterns that enables us to introduce - hypothesis and to transform them at the same time, e.g. by pattern-matching + In this tutorial, we discuss intro patterns that enable us to introduce + hypotheses and transform them at the same time, e.g. by pattern-matching or rewriting them. This enables us to factorize and to write more direct code. *** Table of content @@ -37,8 +37,8 @@ Import ListNotations. (** ** 1. Introducing Variables - The basic tactic to introduces variables is [intros]. In its most basic forms - [intros x y ... z] will introduce as much variables as mentioned with the + The basic tactic to introduce variables is [intros]. Its most basic form + [intros x y ... z] will introduce as many variables as mentioned with the names specified [x], [y], ..., [z], and fail if one of the names is already used. *) @@ -55,7 +55,7 @@ Abort. (** It can happen that we have a hypothesis to introduce that is not useful to our proof. In this case, rather than introducing it we would rather like to directly forget it. This is possible using the wildcard pattern [_], that - will introduce and forget a variable that do do not appear in the conclusion. + will introduce and forget a variable that does not appear in the conclusion. *) Goal forall n m, n = 0 -> n < m -> n <= m. @@ -68,7 +68,7 @@ Proof. Fail intros _ m H. Abort. -(** In some cases, we do not wish to choose a name and would rather have Coq to +(** In some cases, we do not wish to choose a name and would rather have Coq choose a name for us. This is possible with the [?] pattern. *) @@ -78,12 +78,12 @@ Proof. Abort. (** However, be careful that referring explicitly to auto-generated names in a - proof is bad practice as later modification to the file could change the + proof is bad practice as subsequent modifications of the file could change the generated names, and hence break the proof. This can happen very fast. - Auto-generated names should hence only be used in combination with tactic + Auto-generated names should hence only be used in combination with tactics like [assumption] that do not rely on names. - Similarly, to [?] it happens that we want to introduce all the variables + Similarly to [?], it happens that we want to introduce all the variables automatically and without naming them. This is possible by simply writing [intros] or as an alias [intros **]. *) @@ -108,8 +108,8 @@ Proof. intros *. Abort. -(** This is particularly practical to introduce type variables that other variables - depends upon, but that we do not want to perform any specific action on but introduction. +(** This is particularly convenient to introduce type variables that other variables + depend upon, but that we do not want to perform any specific action on but introduction. *) Goal forall P Q, P /\ Q -> Q /\ P. @@ -136,7 +136,8 @@ Definition Reflexive {A} (R : A -> A -> Prop) := forall a, R a a. *) Goal Reflexive (fun P Q => P <-> Q). - Fail progress intros. intros P. + Fail progress intros. + intros P. Abort. @@ -144,7 +145,7 @@ Abort. (** ** 2. Destructing Variables When proving properties, it is very common to introduce variables only to - pattern-match on them just after, e.g to prove properties about an inductive type + pattern-match on them just after, e.g. to prove properties about an inductive type or simplify an inductively defined function: *) @@ -163,8 +164,8 @@ Qed. (** To shorten the code, it is possible to do both at the same time using the intro pattern [ [ x ... y | ... | z ... w ]. It enables to give a - name of each argument of each constructor separating them by [|]. - If no branches or names are specified, Coq will just use auto-generated names. + name to each argument of each constructor, separating them by [|]. + If neither branches nor names are specified, Coq will just use auto-generated names. *) Goal forall P Q, P /\ Q -> Q /\ P. @@ -187,7 +188,7 @@ Proof. + left. assumption. Qed. -(** Note that destructing over [False] expects no branches nor names as [False] +(** Note that destructing over [False] expects neither branches nor names as [False] has no constructors, and that it solves the goal automatically: *) @@ -196,8 +197,8 @@ Proof. intros P []. Qed. -(** It is further possible to nest the intro-patterns when inductive type are - nested into each other, e.g. like a sequence of the form: +(** It is further possible to nest the intro-patterns when inductive types are + nested into each other: *) Goal forall P Q R, (P \/ Q) /\ R -> P /\ R \/ Q /\ R. @@ -211,10 +212,10 @@ Goal forall P Q R, P /\ Q /\ R -> R /\ Q /\ P. Abort. (** Actually, the latter pattern is common enough that there is a specific intro-pattern for it. - When the goal is for the form [X Op1 Y ... Opk W] where all the binary operation + When the goal is of the form [X Op1 Y ... Opk W] where all the binary operation have one constructor with two arguments like [/\], then it is possible to - introduce the variables as [intros p & q & r & h] rather than by having to - destruct them recursively with [intros [p [q [r h]]] ]. + introduce the variables with [intros p & q & r & h] rather than by having to + destruct recursively with [intros [p [q [r h]]] ]. *) Goal forall P Q R H, P /\ Q /\ R /\ H -> H /\ R /\ Q /\ P. @@ -226,7 +227,7 @@ Abort. (** ** 3. Rewriting Lemmas *) -(** It is also very common to introduce an equality that we wish to later rewrite by: +(** It is also very common to introduce an equality that we wish to later rewrite: *) Goal forall n m, n = 0 -> n + m = m. @@ -234,9 +235,9 @@ Proof. intros n m H. rewrite H. cbn. reflexivity. Qed. -(** It is possible to do so both at the time using the intro patterns [->] or - [<-] that will introduce [H], rewrite it in the goal and context, then clear it. - It has the advantage to be much more concise, and save ourself from introducing +(** It is possible to do both at the time using the intro patterns [->] and + [<-] that will introduce [H], rewrite it in the goal and context and then clear it. + It has the advantage to be much more concise, and save us from introducing a name for [n = 0] that we fundamentally do not really care about: *) @@ -256,7 +257,7 @@ Proof. Qed. (** For a more concrete example, consider proving that if a list has one element - and the other one is empty, then the concatenation of the two lists has one element. + and another one is empty, then the concatenation of the two lists has one element. The usual proof would require us to introduce the hypothesis and decompose it into pieces before being able to rewrite and simplify the goal: *) @@ -284,10 +285,10 @@ Qed. (** ** 4. Simplifying Equalities - Rewriting automatically equalities is practical but sometimes we need to - first simplify them with [injection] before being able to rewrite by them. + Rewriting automatically equalities is practical but sometimes we first need to + simplify them with [injection] before being able to rewrite with them. For instance in the example below, we have an equality [S n = 1] but - as it is [n] that appear in the conclusion, we first need to simplify the equation + as it is [n] that appears in the conclusion, we first need to simplify the equation with [injection] to [n = 0] before being able to rewrite it. *) @@ -296,15 +297,15 @@ Goal forall n m, S n = 1 -> n + m = m. Qed. (** To do this automatically, there is a dedicated intro pattern [ [=] ] - that will introduce the equalities obtained simplification by [injection]. + that will introduce the equalities obtained after simplification by [injection]. *) Goal forall n m, S n = S 0 -> n + m = m. intros n m [=]. rewrite H0. cbn. reflexivity. Qed. -(** It is then possible to combine it with the intro pattern for rewriting to - directly simplify the goal, giving us a particular simple proof. +(** It is then possible to combine this with the intro pattern for rewriting to + directly simplify the goal, giving us a particularly simple proof. *) Goal forall n m, S n = S 0 -> n + m = m. @@ -331,7 +332,7 @@ Qed. For instance, consider the following example where we know that [length l1 = 0]. To conclude that [l1 ++ l2 = l2], we must first prove that [l1 = []] by - applying [length_zero_iff_nil] to [length l1 = 0], then rewrite it: + applying [length_zero_iff_nil] to [length l1 = 0], and then rewrite it: *) Goal forall A (l1 l2 : list A), length l1 = 0 -> l1 ++ l2 = l2. @@ -339,8 +340,8 @@ Proof. intros A l1 l2 H. apply length_zero_iff_nil in H. rewrite H. cbn. reflexivity. Qed. -(** To help us do this, there is an intro pattern [x%H] that introduce the - variable [x] and apply the lemma [H] to it. We can hence write +(** To help us do this, there is an intro pattern [x%H] that introduces the + variable [x] and applies the lemma [H] to it. We can hence write [intros H%length_zero_iff_nil] rather than [intros H. apply length_zero_iff_nil in H]. *) @@ -349,7 +350,7 @@ Proof. intros A l1 l2 H%length_zero_iff_nil. rewrite H. cbn. reflexivity. Qed. -(** We can then further combine it with rewrite patterns to simplify the proof: +(** We can then further combine this with rewrite patterns to simplify the proof: *) Goal forall A (l1 l2 : list A), length l1 = 0 -> l1 ++ l2 = l2. @@ -357,17 +358,17 @@ Proof. intros A l1 l2 ->%length_zero_iff_nil. cbn. reflexivity. Qed. -(** For a more involved example, consider the converse of the example of section 3: - if the concatenation of two list has one element then one list has one +(** For a more involved example, consider the converse of the last example of section 3: + if the concatenation of two lists has one element, then one list has one element and the other one is empty. After pattern matching on [l1], we have an equality [a1::l1++l2 = [a]]. We must simplify it to [a1 = a] and [l1 ++ l2 = []] with [injection], then to [l1 = []] and [l2 = []] with [app_eq_nil], before being able to rewrite. - This creates a lot over overhead as introduction and operations like + This creates a lot of overhead as introduction and operations like destruction, simplification and rewriting have to be done separately. - Further, at every step we have to introduce fresh names that do not really - matters in the end. + Furthermore, at every step we have to introduce fresh names that do not really + matter in the end. *) Goal forall {A} (l1 l2 : list A) (a : A), @@ -379,15 +380,15 @@ Proof. destruct H1 as [H3 H4]. rewrite H3, H4. right. split; reflexivity. Qed. -(** Using intros patterns we can significantly shorten this proof and make it - more intuitive, getting rid of tedious manipulations of hypothesis. +(** Using intro patterns we can significantly shorten this proof and make it + more intuitive, getting rid of tedious manipulations of hypotheses. We can use the intro pattern [[=]] to simplify the equality [a1::l1++l2 = [a]] to [a1 = a] and [l1 ++ l2 = []]. We can then rewrite the first equality with [->], and simplify the second equality to [l1 = [] /\ l2 = []] thanks to [%app_eq_nil]. Finally, we can rewrite both equalities using [->], giving us the intro pattern [intros [= -> [-> ->]%app_eq_nil]]. - This gives a much shorter proof without a bunch of fresh names. + This yields a much shorter proof without a bunch of fresh names. *) Goal forall {A} (l1 l2 : list A) (a : A), From 1b6e0df11c3e248ae077607fe404cd1b0ae94271 Mon Sep 17 00:00:00 2001 From: Thomas Lamiaux Date: Sat, 28 Dec 2024 07:47:31 +0100 Subject: [PATCH 11/18] add ex Exists --- src/Tutorial_intro_patterns.v | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/src/Tutorial_intro_patterns.v b/src/Tutorial_intro_patterns.v index c4431c0f..a2e81f1a 100644 --- a/src/Tutorial_intro_patterns.v +++ b/src/Tutorial_intro_patterns.v @@ -223,6 +223,16 @@ Proof. intros * (p & q & r & h). Abort. +(** A particularly useful case is to introduce existential quantifications. +*) + +Goal forall P Q (f : forall x y, P x y -> Q x y), + (exists (x y: nat), P x y) -> (exists (x y : nat), Q x y). +Proof. + intros P Q f (x & y & Pxy). + exists x, y. apply f. assumption. +Qed. + (** ** 3. Rewriting Lemmas *) From c62193a0e7d94c471dfe002a7c507ddb7e36128c Mon Sep 17 00:00:00 2001 From: Thomas Lamiaux <85848641+thomas-lamiaux@users.noreply.github.com> Date: Sat, 28 Dec 2024 17:28:29 +0100 Subject: [PATCH 12/18] Apply suggestions from code review Co-authored-by: Pierre Rousselin <119015057+Villetaneuse@users.noreply.github.com> --- src/Tutorial_intro_patterns.v | 29 ++++++++++++++++------------- 1 file changed, 16 insertions(+), 13 deletions(-) diff --git a/src/Tutorial_intro_patterns.v b/src/Tutorial_intro_patterns.v index a2e81f1a..b1da7247 100644 --- a/src/Tutorial_intro_patterns.v +++ b/src/Tutorial_intro_patterns.v @@ -27,7 +27,7 @@ - No Prerequisites Installation: - - Available by default with coq + - Available by default with Coq/Rocq *) @@ -38,8 +38,8 @@ Import ListNotations. (** ** 1. Introducing Variables The basic tactic to introduce variables is [intros]. Its most basic form - [intros x y ... z] will introduce as many variables as mentioned with the - names specified [x], [y], ..., [z], and fail if one of the names is already used. + [intros x y ... z] will introduce as many variables and hypotheses as mentioned with the + names specified [x], [y], ..., [z], and fails if one of the names is already used, or if there are no more variables or hypotheses to introduce. *) Goal forall n m, n < m -> n <= m. @@ -150,14 +150,14 @@ Abort. *) Goal forall P Q, P /\ Q -> Q /\ P. - intros P Q x. destruct x. split. + intros P Q x. destruct H as [H1 H2]. split + assumption. + assumption. Qed. Goal forall P Q, P \/ Q -> Q \/ P. Proof. - intros P Q x. destruct x. + intros P Q x. destruct H as [H1 | H2]. + right. assumption. + left. assumption. Qed. @@ -202,7 +202,7 @@ Qed. *) Goal forall P Q R, (P \/ Q) /\ R -> P /\ R \/ Q /\ R. - intros P Q R [[p|q] r]. + intros P Q R [[p | q] r]. + left. split; assumption. + right. split; assumption. Qed. @@ -214,7 +214,7 @@ Abort. (** Actually, the latter pattern is common enough that there is a specific intro-pattern for it. When the goal is of the form [X Op1 Y ... Opk W] where all the binary operation have one constructor with two arguments like [/\], then it is possible to - introduce the variables with [intros p & q & r & h] rather than by having to + introduce the variables with [intros (p & q & r & h)] rather than by having to destruct recursively with [intros [p [q [r h]]] ]. *) @@ -237,7 +237,7 @@ Qed. (** ** 3. Rewriting Lemmas *) -(** It is also very common to introduce an equality that we wish to later rewrite: +(** It is also very common to introduce an equality that we only wish to use once as a rewrite rule on the goal: *) Goal forall n m, n = 0 -> n + m = m. @@ -287,7 +287,7 @@ Qed. Goal forall {A} (l1 l2 : list A) (a : A), l1 = [] /\ l2 = [a] \/ l1 = [a] /\ l2 = [] -> l1 ++ l2 = [a]. Proof. - intros A l1 l2 a [[-> ->]| [-> ->]]. + intros A l1 l2 a [[-> ->] | [-> ->]]. - reflexivity. - reflexivity. Qed. @@ -303,6 +303,7 @@ Qed. *) Goal forall n m, S n = 1 -> n + m = m. +Proof. intros n m H. injection H. intros H'. rewrite H'. cbn. reflexivity. Qed. @@ -311,7 +312,8 @@ Qed. *) Goal forall n m, S n = S 0 -> n + m = m. - intros n m [=]. rewrite H0. cbn. reflexivity. +Proof. + intros n m [= H]. rewrite H. cbn. reflexivity. Qed. (** It is then possible to combine this with the intro pattern for rewriting to @@ -319,10 +321,11 @@ Qed. *) Goal forall n m, S n = S 0 -> n + m = m. +Proof. intros n m [= ->]. cbn. reflexivity. Qed. -(** Another particularly useful way of simplifying an equality is to deduce the +(** Another particularly useful way of simplifying an equality is to deduce that the goal is true from an absurd equation like [S n = 0]. This is usually done by introducing variables then using [discriminate], but can also be automatically done thanks to the intro pattern [=]: @@ -350,8 +353,8 @@ Proof. intros A l1 l2 H. apply length_zero_iff_nil in H. rewrite H. cbn. reflexivity. Qed. -(** To help us do this, there is an intro pattern [x%H] that introduces the - variable [x] and applies the lemma [H] to it. We can hence write +(** To help us do this, the [%] intro pattern [H%impl] introduces the + hypothesis [H] and applies the implication [impl] in it. We can hence write [intros H%length_zero_iff_nil] rather than [intros H. apply length_zero_iff_nil in H]. *) From 9e4774dbc2b6145d0b8e043ef41d9bb3f67460de Mon Sep 17 00:00:00 2001 From: Thomas Lamiaux <85848641+thomas-lamiaux@users.noreply.github.com> Date: Sat, 28 Dec 2024 17:29:00 +0100 Subject: [PATCH 13/18] Apply suggestions from code review --- src/Tutorial_intro_patterns.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Tutorial_intro_patterns.v b/src/Tutorial_intro_patterns.v index b1da7247..4203421f 100644 --- a/src/Tutorial_intro_patterns.v +++ b/src/Tutorial_intro_patterns.v @@ -163,7 +163,7 @@ Proof. Qed. (** To shorten the code, it is possible to do both at the same time using the - intro pattern [ [ x ... y | ... | z ... w ]. It enables to give a + intro pattern [ [ x ... y | ... | z ... w ]]. It enables to give a name to each argument of each constructor, separating them by [|]. If neither branches nor names are specified, Coq will just use auto-generated names. *) From 44286d83450a6e1ec7e5ff6407c1942b2531fbee Mon Sep 17 00:00:00 2001 From: Thomas Lamiaux Date: Sat, 28 Dec 2024 17:40:52 +0100 Subject: [PATCH 14/18] add Pierre Rousselin's example --- src/Tutorial_intro_patterns.v | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) diff --git a/src/Tutorial_intro_patterns.v b/src/Tutorial_intro_patterns.v index 4203421f..a8b5f15f 100644 --- a/src/Tutorial_intro_patterns.v +++ b/src/Tutorial_intro_patterns.v @@ -197,6 +197,36 @@ Proof. intros P []. Qed. +(** Using intro patterns is not at all restricted to logical formulas. + Consider Peano's natural numbers (the type [nat] here). +*) + +Print nat. + +(** It has two constructors, one called [O : nat] without argument for the + number zero, and the successor function [S : nat -> nat], basically [1 + _]. + This says that any number of type [nat] is either 0 or the successor of + another number of type [nat]. This can be used to reason by case analysis on + (the nullity of) a natural number. +*) + +Goal forall (n : nat), n = 0 \/ (exists (m : nat), n = 1 + m). +Proof. + (* two cases, the first one is empty because [O] has no argument. *) + intros n. destruct n as [| n']. + - left. reflexivity. + - right. exists n'. reflexivity. +Qed. + +(** Again, we can [intros] and [destruct] our [n] variable in one step. *) + +Goal forall (n : nat), n = 0 \/ (exists (m : nat), n = 1 + m). +Proof. + intros [| n']. (* two cases, the first one is empty because [O] has no argument. *) + - left. reflexivity. + - right. exists n'. reflexivity. +Qed. + (** It is further possible to nest the intro-patterns when inductive types are nested into each other: *) From d89551e0a2b6b7265cea33f5b8f20838eefddfd9 Mon Sep 17 00:00:00 2001 From: Thomas Lamiaux Date: Sat, 28 Dec 2024 17:44:15 +0100 Subject: [PATCH 15/18] add parentheses --- src/Tutorial_intro_patterns.v | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/Tutorial_intro_patterns.v b/src/Tutorial_intro_patterns.v index a8b5f15f..e1828c4e 100644 --- a/src/Tutorial_intro_patterns.v +++ b/src/Tutorial_intro_patterns.v @@ -150,14 +150,14 @@ Abort. *) Goal forall P Q, P /\ Q -> Q /\ P. - intros P Q x. destruct H as [H1 H2]. split + intros P Q H. destruct H as [H1 H2]. split. + assumption. + assumption. Qed. Goal forall P Q, P \/ Q -> Q \/ P. Proof. - intros P Q x. destruct H as [H1 | H2]. + intros P Q H. destruct H as [H1 | H2]. + right. assumption. + left. assumption. Qed. @@ -237,18 +237,18 @@ Goal forall P Q R, (P \/ Q) /\ R -> P /\ R \/ Q /\ R. + right. split; assumption. Qed. -Goal forall P Q R, P /\ Q /\ R -> R /\ Q /\ P. +Goal forall P Q R, P /\ (Q /\ R) -> R /\ (Q /\ P). intros P Q R [p [q r]]. Abort. (** Actually, the latter pattern is common enough that there is a specific intro-pattern for it. - When the goal is of the form [X Op1 Y ... Opk W] where all the binary operation + When the goal is of the form [X Op1 (Y ... Opk W)] where all the binary operation have one constructor with two arguments like [/\], then it is possible to introduce the variables with [intros (p & q & r & h)] rather than by having to destruct recursively with [intros [p [q [r h]]] ]. *) -Goal forall P Q R H, P /\ Q /\ R /\ H -> H /\ R /\ Q /\ P. +Goal forall P Q R H, P /\ (Q /\ (R /\ H)) -> H /\ (R /\ (Q /\ P)). Proof. intros * (p & q & r & h). Abort. From 0822b035e8459aee23ef4b9aae1c18f4c76c9499 Mon Sep 17 00:00:00 2001 From: Thomas Lamiaux Date: Sat, 28 Dec 2024 18:12:33 +0100 Subject: [PATCH 16/18] add Lyes Saadi's comment --- src/Tutorial_intro_patterns.v | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/Tutorial_intro_patterns.v b/src/Tutorial_intro_patterns.v index e1828c4e..72982239 100644 --- a/src/Tutorial_intro_patterns.v +++ b/src/Tutorial_intro_patterns.v @@ -98,9 +98,11 @@ Proof. intros **. Abort. -(** As a variant of [intros], [intros *] will introduce all the variables that - do no appear dependently in the rest of the goal. In this example, it will - introduce [n] and [m] but not [n < m] as it depends on [n] and [m]. +(** As a variant of [intros], [intros *] will introduce all the hypothesis + from the goal until it reaches one depending on the ones that it is has introduced, + or that there is no more hypotheses to introduce. + In this example, [intros *] will introduce [n] and [m], then stops at [n < m] + as it depends on [n] and [m] that it has just introduced. *) Goal forall n m, n < m -> n <= m. From 65bc16dbcb174829e312e018202c18a450bf8055 Mon Sep 17 00:00:00 2001 From: Pierre Rousselin Date: Mon, 30 Dec 2024 11:51:50 +0100 Subject: [PATCH 17/18] Add other tactics with as also correct some whitespace issues and add a small remark after the first "destruct as". --- src/Tutorial_intro_patterns.v | 234 ++++++++++++++++++++++++---------- 1 file changed, 166 insertions(+), 68 deletions(-) diff --git a/src/Tutorial_intro_patterns.v b/src/Tutorial_intro_patterns.v index 72982239..cd1846e5 100644 --- a/src/Tutorial_intro_patterns.v +++ b/src/Tutorial_intro_patterns.v @@ -8,15 +8,16 @@ In this tutorial, we discuss intro patterns that enable us to introduce hypotheses and transform them at the same time, e.g. by pattern-matching - or rewriting them. This enables us to factorize and to write more direct code. + or rewriting them. This enables us to factorize and to write more direct code. *** Table of content - 1. Introducing Variables - 2. Destructing Variables - 3. Rewriting and Injection - - 4. Simplifying Equalities + - 4. Simplifying Equalities - 5. Applying Lemmas + - 6. Intro patterns everywhere *** Prerequisites @@ -31,15 +32,17 @@ *) -From Coq Require Import List. +From Coq Require Import List. Import ListNotations. -(** ** 1. Introducing Variables +(** ** 1. Introducing Variables The basic tactic to introduce variables is [intros]. Its most basic form - [intros x y ... z] will introduce as many variables and hypotheses as mentioned with the - names specified [x], [y], ..., [z], and fails if one of the names is already used, or if there are no more variables or hypotheses to introduce. + [intros x y ... z] will introduce as many variables and hypotheses as + mentioned with the names specified [x], [y], ..., [z], and fails if one of + the names is already used, or if there are no more variables or hypotheses + to introduce. *) Goal forall n m, n < m -> n <= m. @@ -81,10 +84,10 @@ Abort. proof is bad practice as subsequent modifications of the file could change the generated names, and hence break the proof. This can happen very fast. Auto-generated names should hence only be used in combination with tactics - like [assumption] that do not rely on names. + like [assumption] that do not rely on names. - Similarly to [?], it happens that we want to introduce all the variables - automatically and without naming them. This is possible by simply writing + Similarly to [?], it happens that we want to introduce all the variables + automatically and without naming them. This is possible by simply writing [intros] or as an alias [intros **]. *) @@ -99,8 +102,8 @@ Proof. Abort. (** As a variant of [intros], [intros *] will introduce all the hypothesis - from the goal until it reaches one depending on the ones that it is has introduced, - or that there is no more hypotheses to introduce. + from the goal until it reaches one depending on the ones that it is has introduced, + or that there is no more hypotheses to introduce. In this example, [intros *] will introduce [n] and [m], then stops at [n < m] as it depends on [n] and [m] that it has just introduced. *) @@ -110,36 +113,36 @@ Proof. intros *. Abort. -(** This is particularly convenient to introduce type variables that other variables +(** This is particularly convenient to introduce type variables that other variables depend upon, but that we do not want to perform any specific action on but introduction. *) Goal forall P Q, P /\ Q -> Q /\ P. Proof. - intros *. + intros *. Abort. (** An important difference between [intros] and [intros x] is that [intros] introduce as much variables as possible without simplifying the goal, whereas [intros x] will first compute the head normal form before trying to - introduce a variable. This difference can be intuitively understood - by considering that [intros x] means there is a variable to introduce, + introduce a variable. This difference can be intuitively understood + by considering that [intros x] means there is a variable to introduce, and requires to find it. - For instance, consider the definition that a relation is reflexive. + For instance, consider the definition that a relation is reflexive. *) Definition Reflexive {A} (R : A -> A -> Prop) := forall a, R a a. -(** If we try to prove that logical equivalence is reflexive by using [intros] - then nothing will happen as [Reflexive] is a constant, and it needs to - be unfolded for a variable to introduce to appear. +(** If we try to prove that logical equivalence is reflexive by using [intros] + then nothing will happen as [Reflexive] is a constant, and it needs to + be unfolded for a variable to introduce to appear. However, as [intros x] simplifies the goal first, it will succeed and progress: *) Goal Reflexive (fun P Q => P <-> Q). Fail progress intros. - intros P. + intros P. Abort. @@ -147,7 +150,7 @@ Abort. (** ** 2. Destructing Variables When proving properties, it is very common to introduce variables only to - pattern-match on them just after, e.g. to prove properties about an inductive type + pattern-match on them just after, e.g. to prove properties about an inductive type or simplify an inductively defined function: *) @@ -163,9 +166,9 @@ Proof. + right. assumption. + left. assumption. Qed. - -(** To shorten the code, it is possible to do both at the same time using the - intro pattern [ [ x ... y | ... | z ... w ]]. It enables to give a + +(** To shorten the code, it is possible to do both at the same time using the + intro pattern [[ x ... y | ... | z ... w ]]. It enables to give a name to each argument of each constructor, separating them by [|]. If neither branches nor names are specified, Coq will just use auto-generated names. *) @@ -183,6 +186,11 @@ Proof. + left. assumption. Qed. +(** As a side remark, the fact that intro patterns have the same syntax that + what is after [as] in [destruct ... as] is no accident, since the [as] + keyword in a tactic is followed by ... an intro pattern. +*) + Goal forall P Q, P \/ Q -> Q \/ P. Proof. intros P Q []. @@ -191,7 +199,7 @@ Proof. Qed. (** Note that destructing over [False] expects neither branches nor names as [False] - has no constructors, and that it solves the goal automatically: + has no constructors, and that it solves the goal automatically: *) Goal forall P, False -> P. @@ -199,8 +207,8 @@ Proof. intros P []. Qed. -(** Using intro patterns is not at all restricted to logical formulas. - Consider Peano's natural numbers (the type [nat] here). +(** Using intro patterns is not at all restricted to logical formulas. + Consider Peano's natural numbers (the type [nat] here). *) Print nat. @@ -209,13 +217,13 @@ Print nat. number zero, and the successor function [S : nat -> nat], basically [1 + _]. This says that any number of type [nat] is either 0 or the successor of another number of type [nat]. This can be used to reason by case analysis on - (the nullity of) a natural number. + (the nullity of) a natural number. *) Goal forall (n : nat), n = 0 \/ (exists (m : nat), n = 1 + m). Proof. (* two cases, the first one is empty because [O] has no argument. *) - intros n. destruct n as [| n']. + intros n. destruct n as [| n']. - left. reflexivity. - right. exists n'. reflexivity. Qed. @@ -229,7 +237,7 @@ Proof. - right. exists n'. reflexivity. Qed. -(** It is further possible to nest the intro-patterns when inductive types are +(** It is further possible to nest the intro-patterns when inductive types are nested into each other: *) @@ -244,63 +252,61 @@ Goal forall P Q R, P /\ (Q /\ R) -> R /\ (Q /\ P). Abort. (** Actually, the latter pattern is common enough that there is a specific intro-pattern for it. - When the goal is of the form [X Op1 (Y ... Opk W)] where all the binary operation - have one constructor with two arguments like [/\], then it is possible to - introduce the variables with [intros (p & q & r & h)] rather than by having to + When the goal is of the form [X Op1 (Y ... Opk W)] where all the binary operations + have one constructor with two arguments like [/\], then it is possible to + introduce the variables with [intros (p & q & r & h)] rather than by having to destruct recursively with [intros [p [q [r h]]] ]. *) Goal forall P Q R H, P /\ (Q /\ (R /\ H)) -> H /\ (R /\ (Q /\ P)). Proof. - intros * (p & q & r & h). + intros * (p & q & r & h). Abort. -(** A particularly useful case is to introduce existential quantifications. +(** A particularly useful case is to introduce existentially quantified hypotheses. *) -Goal forall P Q (f : forall x y, P x y -> Q x y), +Goal forall P Q (f : forall x y, P x y -> Q x y), (exists (x y: nat), P x y) -> (exists (x y : nat), Q x y). Proof. intros P Q f (x & y & Pxy). exists x, y. apply f. assumption. Qed. - - (** ** 3. Rewriting Lemmas *) -(** It is also very common to introduce an equality that we only wish to use once as a rewrite rule on the goal: +(** It is also very common to introduce an equality that we only wish to use once as a rewrite rule on the goal: *) -Goal forall n m, n = 0 -> n + m = m. +Goal forall n m, n = 0 -> n + m = m. Proof. intros n m H. rewrite H. cbn. reflexivity. Qed. (** It is possible to do both at the time using the intro patterns [->] and - [<-] that will introduce [H], rewrite it in the goal and context and then clear it. - It has the advantage to be much more concise, and save us from introducing - a name for [n = 0] that we fundamentally do not really care about: + [<-] that will introduce [H], rewrite it in the goal and context and then clear it. + It has the advantage to be much more concise, and save us from introducing + a name for [n = 0] that we fundamentally do not really care about: *) -Goal forall n m, n = 0 -> n + m = m. +Goal forall n m, n = 0 -> n + m = m. Proof. intros n m ->. cbn. reflexivity. Qed. -Goal forall n m, 0 = n -> n + m = m. +Goal forall n m, 0 = n -> n + m = m. Proof. intros n m <-. cbn. reflexivity. Qed. -Goal forall n m p, n + p = m -> n = 0 -> p = m. +Goal forall n m p, n + p = m -> n = 0 -> p = m. Proof. intros n m p H ->. cbn in *. apply H. Qed. (** For a more concrete example, consider proving that if a list has one element - and another one is empty, then the concatenation of the two lists has one element. - The usual proof would require us to introduce the hypothesis and decompose it + and another one is empty, then the concatenation of the two lists has one element. + The usual proof would require us to introduce the hypothesis and decompose it into pieces before being able to rewrite and simplify the goal: *) @@ -308,12 +314,12 @@ Goal forall {A} (l1 l2 : list A) (a : A), l1 = [] /\ l2 = [a] \/ l1 = [a] /\ l2 = [] -> l1 ++ l2 = [a]. Proof. intros A l1 l2 a. - intros H. destruct H as [H | H]. + intros H. destruct H as [H | H]. - destruct H as [H1 H2]. rewrite H1, H2. reflexivity. - destruct H as [H1 H2]. rewrite H1, H2. reflexivity. Qed. -(** Using intro patterns to do the pattern-matching and the rewriting, we can get +(** Using intro patterns to do the pattern-matching and the rewriting, we can get a very intuitive and compact proof without having to introduce any fresh names: *) Goal forall {A} (l1 l2 : list A) (a : A), @@ -325,14 +331,14 @@ Proof. Qed. -(** ** 4. Simplifying Equalities +(** ** 4. Simplifying Equalities - Rewriting automatically equalities is practical but sometimes we first need to + Rewriting automatically equalities is practical but sometimes we first need to simplify them with [injection] before being able to rewrite with them. - For instance in the example below, we have an equality [S n = 1] but + For instance in the example below, we have an equality [S n = 1] but as it is [n] that appears in the conclusion, we first need to simplify the equation with [injection] to [n = 0] before being able to rewrite it. -*) +*) Goal forall n m, S n = 1 -> n + m = m. Proof. @@ -357,9 +363,9 @@ Proof. intros n m [= ->]. cbn. reflexivity. Qed. -(** Another particularly useful way of simplifying an equality is to deduce that the +(** Another particularly useful way of simplifying an equality is to deduce that the goal is true from an absurd equation like [S n = 0]. - This is usually done by introducing variables then using [discriminate], + This is usually done by introducing variables then using [discriminate], but can also be automatically done thanks to the intro pattern [=]: *) @@ -368,9 +374,7 @@ Proof. intros n [=]. Qed. - - -(** ** 5. Applying Lemmas +(** ** 5. Applying Lemmas A situation that often arises when proving properties is having a hypothesis that we first need to transform before being able to use it. @@ -382,30 +386,30 @@ Qed. Goal forall A (l1 l2 : list A), length l1 = 0 -> l1 ++ l2 = l2. Proof. - intros A l1 l2 H. apply length_zero_iff_nil in H. rewrite H. cbn. reflexivity. + intros A l1 l2 H. apply length_zero_iff_nil in H. rewrite H. cbn. reflexivity. Qed. (** To help us do this, the [%] intro pattern [H%impl] introduces the - hypothesis [H] and applies the implication [impl] in it. We can hence write + hypothesis [H] and applies the implication [impl] in it. We can hence write [intros H%length_zero_iff_nil] rather than [intros H. apply length_zero_iff_nil in H]. *) Goal forall A (l1 l2 : list A), length l1 = 0 -> l1 ++ l2 = l2. Proof. - intros A l1 l2 H%length_zero_iff_nil. rewrite H. cbn. reflexivity. + intros A l1 l2 H%length_zero_iff_nil. rewrite H. cbn. reflexivity. Qed. -(** We can then further combine this with rewrite patterns to simplify the proof: +(** We can then further combine this with rewrite patterns to simplify the proof: *) Goal forall A (l1 l2 : list A), length l1 = 0 -> l1 ++ l2 = l2. Proof. - intros A l1 l2 ->%length_zero_iff_nil. cbn. reflexivity. + intros A l1 l2 ->%length_zero_iff_nil. cbn. reflexivity. Qed. (** For a more involved example, consider the converse of the last example of section 3: if the concatenation of two lists has one element, then one list has one - element and the other one is empty. + element and the other one is empty. After pattern matching on [l1], we have an equality [a1::l1++l2 = [a]]. We must simplify it to [a1 = a] and [l1 ++ l2 = []] with [injection], then to @@ -421,14 +425,14 @@ Goal forall {A} (l1 l2 : list A) (a : A), Proof. intros A l1 l2 a. destruct l1; cbn. - intros H. rewrite H. left. split; reflexivity. - - intros H. injection H. intros H1 H2. rewrite H2. apply app_eq_nil in H1. + - intros H. injection H. intros H1 H2. rewrite H2. apply app_eq_nil in H1. destruct H1 as [H3 H4]. rewrite H3, H4. right. split; reflexivity. Qed. (** Using intro patterns we can significantly shorten this proof and make it more intuitive, getting rid of tedious manipulations of hypotheses. - We can use the intro pattern [[=]] to simplify the equality [a1::l1++l2 = [a]] + We can use the intro pattern [[=]] to simplify the equality [a1::l1++l2 = [a]] to [a1 = a] and [l1 ++ l2 = []]. We can then rewrite the first equality with [->], and simplify the second equality to [l1 = [] /\ l2 = []] thanks to [%app_eq_nil]. Finally, we can rewrite both equalities using [->], giving @@ -442,4 +446,98 @@ Proof. intros A l1 l2 a. destruct l1; cbn. - intros ->. left. split; reflexivity. - intros [= -> [-> ->]%app_eq_nil]. right. split; reflexivity. -Qed. +Qed. + +(** ** Intro patterns everywhere *) + +(** We mentioned before the fact that the tactic [destruct ... as ...] expects + an intro pattern after [as]. + + In fact, many tactics can have an [as ...] part, with an intro pattern. + + Let's give examples. *) + +(** We concentrate on [apply ... in ...]. In general, using this tactic can + result in a weaker proof state, which may or may not be an issue. *) + +Goal forall (P Q R : Prop), (P -> Q) -> P -> (P -> R) -> Q /\ R. +Proof. + intros P Q R H1 H2 H3. + (* Now I'm tired and I want to deduce that [Q] holds. *) + apply H1 in H2. + (* Ouch, no more way to prove that [P] holds! *) +Abort. + +Goal forall (P Q R : Prop), (P -> Q) -> P -> (P -> R) -> Q /\ R. +Proof. + intros P Q R H1 H2 H3. + (* Now I'm less tired and I give a new name to what I deduce from [H1] and + [H2]. *) + apply H1 in H2 as HQ. + (* This is fun, I can do this with a proof of [R], too. *) + apply H3 in H2 as HR. + split. + - assumption. + - assumption. +Qed. + +(** In many cases, applying an implication in an hypothesis will give something + which: + - can (and should) be [destruct]ed with [[...]] or + - is an equality to use with [rewrite] with [->] or [<-] or + - can be simplified ([injection]), or is directly contradictory + [discriminate] (with [[= ...]]) or + - can be served as a condition to another implication with [%] + In that case, we're free to use everything we already learned after [as]. *) + +Goal forall (P Q R : Prop) (n : nat), (Q -> S n = S 21) -> (P -> Q /\ R) -> P -> + (n + n = 42). +Proof. + intros P Q R n H1 H2 H3. + apply H2 in H3 as [HQ _]. (* "and" intro pattern, drop a useless part *) + apply H1 in HQ as [= ->]. (* injection, then rewrite *) + reflexivity. +Qed. + +(** We can go crazier: *) +Goal forall (P Q R : Prop) (n : nat), (Q -> S n = S 21) -> (P -> Q /\ R) -> P -> + (n + n = 42). +Proof. + intros P Q R n H1 H2 H3. + apply H2 in H3 as [[= ->]%H1 _]. + reflexivity. +Qed. + +(** Who needs [apply]? *) +Goal forall (P Q R : Prop) (n : nat), (Q -> S n = S 21) -> (P -> Q /\ R) -> P -> + (n + n = 42). +Proof. intros P Q R n H1 H2 [[= ->]%H1 _]%H2. reflexivity. Qed. + +(** Other useful and frequently used tactics which can be used with + [as intro_pattern] include: + - [destruct] + - [pose proof] + - [specialize] + - [assert] and [enough] + - [inversion] (restricted to "and" and "or" intro patterns) + - [injection] +*) + +Goal forall (n m : nat), n * 2 + n * m = 0 -> n + m = m. +Proof. + intros n m H. + enough (n = 0) as ->. { + reflexivity. + } + rewrite <-PeanoNat.Nat.mul_add_distr_l in H. + pose proof PeanoNat.Nat.mul_eq_0 as mul0. + (* specialize and discard useless right to left implication: *) + specialize (mul0 n (2 + m)) as [H' _]. + (* apply H' in H and reason by case + - in the first one, change 0 with n in the goal + - in the second one, 2 + m = 0 can be reduced to (S (S m) = 0) which is + discriminable. + *) + apply H' in H as [<- | [=]]. + reflexivity. +Qed. From d777063d5a274ee7556d5b57fd85687e630df9ec Mon Sep 17 00:00:00 2001 From: Thomas Lamiaux <85848641+thomas-lamiaux@users.noreply.github.com> Date: Fri, 3 Jan 2025 17:20:55 +0100 Subject: [PATCH 18/18] Update src/Tutorial_intro_patterns.v --- src/Tutorial_intro_patterns.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Tutorial_intro_patterns.v b/src/Tutorial_intro_patterns.v index cd1846e5..8f90380f 100644 --- a/src/Tutorial_intro_patterns.v +++ b/src/Tutorial_intro_patterns.v @@ -448,7 +448,7 @@ Proof. - intros [= -> [-> ->]%app_eq_nil]. right. split; reflexivity. Qed. -(** ** Intro patterns everywhere *) +(** ** 6. Intro patterns everywhere *) (** We mentioned before the fact that the tactic [destruct ... as ...] expects an intro pattern after [as].