From e8cc98c297556a39e27ad3892e906be3801a19bc Mon Sep 17 00:00:00 2001 From: thomas-lamiaux Date: Tue, 14 May 2024 02:59:38 +0200 Subject: [PATCH 01/12] add draft tuto equations indexed ind --- src/Tutorial_Equations_indexed.v | 597 +++++++++++++++++++++++++++++++ 1 file changed, 597 insertions(+) create mode 100644 src/Tutorial_Equations_indexed.v diff --git a/src/Tutorial_Equations_indexed.v b/src/Tutorial_Equations_indexed.v new file mode 100644 index 00000000..54a71986 --- /dev/null +++ b/src/Tutorial_Equations_indexed.v @@ -0,0 +1,597 @@ +(* begin hide *) +Axiom to_fill : forall A, A. +Arguments to_fill {_}. +(* end hide *) + +(** * Well-founded Recursion using Equations + + *** Summary: + + [Equations] is a plugin for %\cite{Coq}% that offers a powerful support + for writing functions by dependent pattern matching. + In this tutorial, we focus on the facilities provided by Equations to + define function using well-founded recursion and reason about them. + + In section 1, we explain the basic of defining and reasoning by + well-founded recursion using Equations. + - In section 1.1, we contextualise and recall the concept of + well-founded recursion. + - In section 1.2, we explain how to define and reason about basic + functions defined using well-founded recursion and Equations. + - In section 1.3, we explain how to define more complex examples using + obligations. + + In section 2, we discuss different techniques that can be useful when + attempting to define functions by well-founded recursion: + - In section 2.1, we explain TODO. + - When matching on terms, it can happen that we loose information relevant + to termination. + In Section 2.2, we show an example of that and discuss the inspect + method as a possible solution to this problem. + - When defining functions by well-founded recursion, it often happens + that we are left with easy theory specific obligations to solve, + for instance basic arithmetic on lists. + In section 2.3, we explain how to adapt locally the tactic trying to + solve obligations to deal with such goals. + + *** Table of content: + + - 1. Defining and reasoning using well-founded recursion + - 1.1 Introduction to well-founded recursion + - 1.2 Basic definitions and reasoning + - 1.3 Well-founded recursion and Obligations + - 2. Different methods to work with well-founded recursion + - 2.1 Subterm relations for indexed inductive types + - 2.2 The inspect method + - 2.3 Personalising the tactic proving obligations + + *** Prerequisites: + + Needed: + - We assume known basic knowledge of Coq, of and defining functions by recursion + - We assume basic knowledge of the plugin Equations, e.g, as presented + in the tutorial Equations : Basics + + Not needed: + - This tutorial discuss well-founded recursion but no prior knowledge + about it is required, and we recall the concept at the beginning + - Defining functions by well-founded recursion using Equations relies on + Coq's obligation mechanism, but no previous knowledge about it is needed. + - To simplify proofs involving arithmetics, we use the automatisation + tactic [lia] and [auto with arith], but they can be used as black boxes + + Installation: + - Equations is available by default in the Coq Platform + - Otherwise, it is available via opam under the name coq-equations + +*) + +From Equations Require Import Equations. +From Coq Require Import List Arith Lia. +Import ListNotations. + + + +(** * 1. Defining and reasoning using well-founded recursion + + ** 1.1 Introduction to well-founded recursion + + For Coq to be consistent, all functions must be terminating. + To ensure they are, Coq check that they verify a complex syntactic + criterion named the guard condition. + While powerful, this syntactic criterion is by nature limited, and it + happens that functions can be proven terminating, using a potentially non + trivial size argument and some mathematical reasoning, that Coq syntactic + guard fails to see as such on its own. + + For instance, consider the function [last] that returns the last + element of a list if there is one and None otherwise. + To return the last element, we must distinguish if a list has + zero, one, or more than 2 elements leading to nested matching + [ last (a::(a'::l)) := last (a'::l) ]. + Yet, doing so is not accepted by Coq's current syntactic guard as the + nested matching forgets that [a'::l] is a subterm of [a::(a'::l)] + and only recall [l] as a smaller subterm. +*) + +Fail Equations last {A} (l : list A) {struct l} : option (list A) := +last [] := None; +last (a::nil) := Some [a]; +last (a::(a'::l)) := last (a'::l). + +(** For an other example consider the definition of the Ackerman function. + This function is clearly terminating using the lexicographic order : + [(n,m) negb (eq x y)) xs] + is indeed performed on a smaller instance, and so that nubBy is terminating. + Yet, without surprise, it can not be checked automatically using Coq's + syntactic guard as it involves mathematical reasoning on [filter]. +*) + +Fail Equations nubBy {A} (eq : A -> A -> bool) (l : list A) : list A := +nubBy eq [] => []; +nubBy eq (x :: xs) => x :: nubBy eq (filter (fun y => negb (eq x y)) xs). + + +(** TEXT ON WELL-FOUNDED REC + + This functions can still be accepted using well-founded recursion, + that is by directly providing a size measure that is known to be + decreasing and terminating like nil], then there exists an + [a : A] such that [last l = (Some a)]. + By functional elimination, we only need to deal with the case where + [l := nil], [l := [a]] and [l := (a::a'::l)]. + Moreover, in the last case, we know recursively that + [a' :: l <> [] -> {a : A & last (a' :: l) = Some a}]. + As we can see, the condition [l <> nil] as correctly been + particularise and quantified by. +*) + +Definition exists_last {A} (l : list A) (Hneq : l <> nil) : + { a : A & last l = (Some a)}. +Proof. + funelim (last l); simp last. + - specialize (Hneq eq_refl) as []. + - exists a. reflexivity. + - apply X. discriminate. +Defined. + +(** Similarly, we can prove that [last] respects [app] in a suitable way. +*) + +Definition last_app {A} (l l': list A) (Hneq : l' <> nil) : + last (l ++ l') = last l'. +Proof. + funelim (last l); cbn; autorewrite with last. + - reflexivity. + - funelim (last l'); simp last. + -- specialize (Hneq eq_refl) as []. + -- reflexivity. + -- reflexivity. + - apply H. assumption. +Qed. + +(** Let's now consider the Ackerman function. + The ackerman function is decreasing according to the usual lexicographic + order on [nat * nat], [(<,<)] which is accessible as both [<] are. + To build the lexicographic order, we use a function predefine in + Equations' library [Equations.Prop.Subterm.lexprod]. + As we can see, once again no obligations are generated as Coq can prove + on its own that [(m, (ack (S m) n)) nil) : + removelast (l ++ l') = l ++ removelast l'. +Proof. +Admitted. + +(* You may need to use assert *) +Definition removelast_last {A} (l : list A) (Hneq : l <> nil) : + {a : A & { _ : last l = Some a & l = removelast l ++ [a]}}. +Proof. +Admitted. + + +(** ** 1.3 Well-founded recursion and Obligations + + For a more involved example where Coq can not prove on its own that the + recursive call are performed on smaller arguments, let's consider the + [nubBy] function from Haskell's prelude defined below. + + Given an equality test, [nubBy] recursively filters out the duplicates + of a list and only keeps the first occurrence of each element. + It is terminating as the recursive call is performed on + [filter (fun y => negb (eq x y)) xs] which is smaller than [xs] as + [filter] can only remove elements. + Consequently, to define [nubBy] by well-founded recursion, we need to + add [wf (length l) lt]. + + As we can see, it is not enough as Coq can not prove on its own that + the recursive call is indeed smaller, and therefore leaves it for us to prove. + That is, [length (filter (fun y : A => negb (eq x y)) xs) < length (x::xs)]. + It is not surprising as our argument rests on the property that + for any test [f : A -> bool], [length (filter f l) ≤ length l]. + Property that is not trivial, and that Coq can not know to look for, + nor where to look for without any indications. + + To make the obligations generated by well-founded recursion available, + it suffices to start the definition by [Equations?] rather than by + [Equations] as below. + We can then prove the missing properties ourself in proof mode. + This enables to separate the proofs from the definition of the function + while dealing automatically with trivial cases. +*) + +Equations? nubBy {A} (eq : A -> A -> bool) (l : list A) : list A by wf (length l) lt := +nubBy eq [] => []; +nubBy eq (x :: xs) => x :: nubBy eq (filter (fun y => negb (eq x y)) xs). +Proof. + eapply Nat.le_lt_trans. + - apply filter_length_le. + - auto with arith. +Defined. + +(** reasoning on functions defined by well-founded recursion with + obligations is no different than when there is none. + Using function elimination ([funelim]) we can prove our properties + without having to redo the well-founded recursion. + + As examples, we show how to prove in a few lines that [nubBy] do + remove all duplicates. +*) + +Lemma In_nubBy {A} (eq : A -> A -> bool) (l : list A) (a : A) + : In a (nubBy eq l) -> In a l. +Proof. + funelim (nubBy eq l); simp nubBy; cbn. + intros [Heq | H0]. + - rewrite Heq. left; reflexivity. + - specialize (H _ H0). apply filter_In in H as [Inal eqa]. + right; assumption. +Qed. + +Lemma nubBy_nodup {A} (eq : A -> A -> bool) (l : list A) : + (forall x y, (eq x y = true) <-> (x = y)) -> NoDup (nubBy eq l). +Proof. + intros Heq; funelim (nubBy eq l). + - simp nubBy. constructor. + - specialize (H Heq). simp nubBy. constructor. + -- intros Hi. + apply In_nubBy in Hi. + apply filter_In in Hi as [_ Hneqx]. + specialize (Heq x x); destruct Heq as [_ Heqx]. + specialize (Heqx eq_refl); rewrite Heqx in Hneqx. + inversion Hneqx. + -- assumption. +Qed. + + +(** ** 2. Different methods to work with well-founded recursion *) + +(** ** 2.1 Subterm relations for indexed inductive types *) + +(** ISSUES: FIND AN EXAMPLE*) +Inductive vec A : nat -> Type := + | vnil : vec A 0 + | vcons : A -> forall (n : nat), vec A n -> vec A (S n). + +Arguments vnil {_}. +Arguments vcons {_} _ {_} _. + +Derive Signature NoConfusion NoConfusionHom for vec. +Derive Subterm for vec. + +Equations vmap {A B n} (f : A -> B) (v : vec A n) : vec B n := +vmap f vnil := vnil ; +vmap f (vcons a v) := vcons (f a) (vmap f v). + +Check well_founded_vec_subterm : forall A, WellFounded (vec_subterm A). + + +(* ISSUE WORK WITHOUT *) +Equations unzip {A B n} (v : vec (A * B) n) : vec A n * vec B n := +(* by wf (signature_pack v) (@t_subterm (A * B)) := *) +unzip vnil := (vnil, vnil) ; +unzip (vcons (pair x y) v) with unzip v := { +| pair xs ys := (vcons x xs, vcons y ys) }. + +(** We can use the packed relation to do well-founded recursion on the vector. + Note that we do a recursive call on a subterm of type [vector A n] which + must be shown smaller than a [vector A (S n)]. They are actually compared + at the packed type [{ n : nat & vector A n}]. The default obligation + tactic defined in [Equations.Init] includes a proof-search + for [subterm] proofs which can resolve the recursive call obligation + automatically in this case. *) + + + +(** ** 2.2 The inspect method + + When defining a functions, it can happen that we loose information + relevant for termination when matching a value, and that we then get + stuck trying to prove termination. + + In this section, we discuss such an example, and explain a solution to + this problem using the function [inspect]. + + Working with a particular well-founded order [lt], it may happen that + we have a choice function [f : A -> option A] that for any [(a :A)] + return a strictly smaller element if there is one. + This situation is axiomatised by the following context : +*) + +Section Inspect. + + Context {A : Type} {lt : A -> A -> Prop} `{WellFounded A lt} + (f : A -> option A) (decr_f : forall n p, f n = Some p -> lt p n). + +(** In this case, given an element (a : A), we may be interested in + computing the associated decreasing chain of elements starting from + [a]. + Naively, we would like to do so as below. + That is check if there is an element smaller than [a] by matching [f a] + with a with clause, if there is one [Some p] then returns [p] added to + chain starting [f_sequence p] here our recursive call, and otherwise + stop the computation. +*) + + Equations? f_sequence (a : A) : list A by wf a lt := + f_sequence a with (f a) := { + | Some p => p :: f_sequence p; + | None => nil + }. + Proof. + apply decr_f. + (* What to do now ? *) + Abort. + +(** Unfortunately, as we can see, if do so it generates an unprovable + obligation as we don't remember information about the call to [f n] being + equal to [Some p] in the recursive call [f_sequence p]. + + To go around this issue and remember the origin of the pattern, + we can wrap our match with the [inspect] function, which simply packs a + value with a proof of an equality to itself. + In other words, given an element [(a : A)], [inspect (a)] returns the + elements [(a, eq_refl) : {b : A | a = b}]. +*) + + Definition inspect {A} (a : A) : {b | a = b} := exist _ a eq_refl. + + Notation "x 'eqn:' p" := (exist _ x p) (only parsing, at level 20). + +(** In our case, wrapping with [inspect] means matching first on + [inspect (f a)] then on the first component which is by definition [f a], + rather than directly on the term [f a]. + This may seem pointless as if one destruct [f a] in an equality + [f a = f a], one would surely get [Some p = Some p] and learn nothing ? + The trick here is that [inspect (f a)] returns an object of type + [{b : A | f a = b}], type in which [f a] is a fixed constant. + Consequently, destructing the first component, in our case [f a], + will only affect the right-hand side of the equality, and we will + indeed get the desired equality [f a = Some p]. + As it can be seen below it works perfectly, and Coq is even able to + prove the call is terminating on its own leaving us no obligations + to fill. +*) + + Equations f_sequence (a : A) : list A by wf a lt := + f_sequence a with inspect (f a) := { + | Some p eqn: eq1 => p :: f_sequence p; + | None eqn:_ => List.nil + }. + +End Inspect. + + +(** ** 2.3 Personalising the tactic proving obligations + + When working, it is common to be dealing with a particular class of + functions that shares a common theory, e.g, they involves basic + arithmetic. + Yet, by default the tactic trying to prove obligations is not + aware of the particular theory at hand, and it will fail to solve + most of the obligations generated. + This is normal, it would be very inefficient if Coq were trying to solve + a goal using all lemma ever defined., or even all lemma featuring + [+] in its definition. + Therefore, it can be interesting to define a local custom strategy for + solving obligations specific to our theory at hand. + + In this section, we explain how to do so to for the [gcd] function, + and show how function elimination then enables to prove a few properties + efficiently. + + TO EXPANSE + To define [gcd x y], we first check if [x] or [y] is [0], and if not + we check if they are equal. + + It is terminating as the sum [x + y] is decreasing for the usual + well-founded order on nat, accounted for by [wf (x + y) lt]. +*) + +Equations? gcd (x y : nat) : nat by wf (x + y) lt := +gcd 0 x := x ; +gcd x 0 := x ; +gcd x y with gt_eq_gt_dec x y := { + | inleft (left _) := gcd x (y - x) ; + | inleft (right refl) := x ; + | inright _ := gcd (x - y) y }. +Proof. + lia. lia. +Abort. + +(** As we can see, Coq fails to prove the obligations on its own as they + involve basic reasoning on arithmetic, a theory that Coq is unaware of + by default. + This can be checked by using [Show Obligation Tactic] to print the + tactic currently used to solve obligations and inspecting it. +*) + +Show Obligation Tactic. + +(** The obligations generated are not complicated to prove but tedious, + and they can actually be solved automatically via the arithmetic + solver [lia]. + Therefore, we would like to locally change the tactic solving the + obligations to take into account arithmetic, and try lia. + + To do so, we use the command [ #[local] Obligation Tactic := tac ] + to change locally the tactic solving obligation to a tactic [tac]. + + In our case, we choose for [tac] to be the previously used + tactic to which we have added a call to [lia] at the end: +*) + +#[local] Obligation Tactic := + simpl in *; + Tactics.program_simplify; + CoreTactics.equations_simpl; + try Tactics.program_solve_wf; + try lia. + +(** As we can see by running [Show Obligation Tactic] again, the tactic + has indeed been changed. +*) + +Show Obligation Tactic. + +(** We can see our change was useful as [gcd] can now be defined by + well-founded recursion without us having to solve any obligations. +*) + +Equations gcd (x y : nat) : nat by wf (x + y) lt := +gcd 0 x := x ; +gcd x 0 := x ; +gcd x y with gt_eq_gt_dec x y := { + | inleft (left _) := gcd x (y - x) ; + | inleft (right refl) := x ; + | inright _ := gcd (x - y) y }. + + +(** For further examples of how functional elimination works on well-founded + recursion and is useful on complex definitions, we will now show a + few properties of [gcd] +*) + +Lemma gcd_same x : gcd x x = x. +Proof. + funelim (gcd x x); try lia. reflexivity. +Qed. + +Lemma gcd_spec0 a : gcd a 0 = a. +Proof. + funelim (gcd a 0); reflexivity. +Qed. + +Lemma mod_minus a b : b <> 0 -> b < a -> (a - b) mod b = a mod b. +Proof. + intros. + replace a with ((a - b) + b) at 2 by lia. + rewrite <- Nat.Div0.add_mod_idemp_r; auto. + rewrite Nat.Div0.mod_same; auto. +Qed. + +Lemma gcd_spec1 a b: 0 <> b -> gcd a b = gcd (Nat.modulo a b) b. +Proof. + funelim (gcd a b); intros. + - now rewrite Nat.Div0.mod_0_l. + - reflexivity. + - now rewrite (Nat.mod_small (S n) (S n0)). + - simp gcd; rewrite Heq; simp gcd. + rewrite refl, Nat.Div0.mod_same. + reflexivity. + - simp gcd; rewrite Heq; simp gcd. + rewrite H; auto. rewrite mod_minus; auto. +Qed. \ No newline at end of file From 1a6d2ce74ee9fb7b6c819fe83d2a967f6c5dd7f6 Mon Sep 17 00:00:00 2001 From: thomas-lamiaux Date: Tue, 10 Sep 2024 18:16:28 +0200 Subject: [PATCH 02/12] fix file --- src/Tutorial_Equations_indexed.v | 786 +++++++++++-------------------- 1 file changed, 265 insertions(+), 521 deletions(-) diff --git a/src/Tutorial_Equations_indexed.v b/src/Tutorial_Equations_indexed.v index 54a71986..8ea8997f 100644 --- a/src/Tutorial_Equations_indexed.v +++ b/src/Tutorial_Equations_indexed.v @@ -1,64 +1,36 @@ -(* begin hide *) -Axiom to_fill : forall A, A. -Arguments to_fill {_}. -(* end hide *) - -(** * Well-founded Recursion using Equations +(** * Tutorial Equations : Dealing with indexed inductive types *** Summary: - [Equations] is a plugin for %\cite{Coq}% that offers a powerful support + [Equations] is a plugin for Coq that offers a powerful support for writing functions by dependent pattern matching. - In this tutorial, we focus on the facilities provided by Equations to - define function using well-founded recursion and reason about them. - - In section 1, we explain the basic of defining and reasoning by - well-founded recursion using Equations. - - In section 1.1, we contextualise and recall the concept of - well-founded recursion. - - In section 1.2, we explain how to define and reason about basic - functions defined using well-founded recursion and Equations. - - In section 1.3, we explain how to define more complex examples using - obligations. - - In section 2, we discuss different techniques that can be useful when - attempting to define functions by well-founded recursion: - - In section 2.1, we explain TODO. - - When matching on terms, it can happen that we loose information relevant - to termination. - In Section 2.2, we show an example of that and discuss the inspect - method as a possible solution to this problem. - - When defining functions by well-founded recursion, it often happens - that we are left with easy theory specific obligations to solve, - for instance basic arithmetic on lists. - In section 2.3, we explain how to adapt locally the tactic trying to - solve obligations to deal with such goals. - - *** Table of content: - - - 1. Defining and reasoning using well-founded recursion - - 1.1 Introduction to well-founded recursion - - 1.2 Basic definitions and reasoning - - 1.3 Well-founded recursion and Obligations - - 2. Different methods to work with well-founded recursion - - 2.1 Subterm relations for indexed inductive types - - 2.2 The inspect method - - 2.3 Personalising the tactic proving obligations + In this tutorial, we focus on the facilities provided by [Equations] to + define function by dependent pattern matching on indexed inductive types, + and reason about them. + + In Section 1, we discuss indexed inductive types on the particularities + of defining and reasoning about functions defined by pattern matching over + them. + In section 2, we discuss the no confusion property and how it enables to + automatically discard impossible cases for indexed inductive types. + In section 3, we discuss the particularity that indexed types have + to particularise indices when matching, and issues that can arise. + + *** Table of content + - 1. Reasoning about indexed inductive types + - 2. The No-Confusion property + - 3. Unifying Indices and Inaccessible Patterns *** Prerequisites: Needed: - - We assume known basic knowledge of Coq, of and defining functions by recursion + - We assume basic knowledge of Coq, of and defining functions by recursion - We assume basic knowledge of the plugin Equations, e.g, as presented in the tutorial Equations : Basics Not needed: - - This tutorial discuss well-founded recursion but no prior knowledge - about it is required, and we recall the concept at the beginning - - Defining functions by well-founded recursion using Equations relies on - Coq's obligation mechanism, but no previous knowledge about it is needed. - - To simplify proofs involving arithmetics, we use the automatisation - tactic [lia] and [auto with arith], but they can be used as black boxes + - We discuss here indexed inductives but we recall the concept so previous + knowledge about them is not needed Installation: - Equations is available by default in the Coq Platform @@ -67,531 +39,303 @@ Arguments to_fill {_}. *) From Equations Require Import Equations. -From Coq Require Import List Arith Lia. -Import ListNotations. - - - -(** * 1. Defining and reasoning using well-founded recursion - - ** 1.1 Introduction to well-founded recursion - - For Coq to be consistent, all functions must be terminating. - To ensure they are, Coq check that they verify a complex syntactic - criterion named the guard condition. - While powerful, this syntactic criterion is by nature limited, and it - happens that functions can be proven terminating, using a potentially non - trivial size argument and some mathematical reasoning, that Coq syntactic - guard fails to see as such on its own. - For instance, consider the function [last] that returns the last - element of a list if there is one and None otherwise. - To return the last element, we must distinguish if a list has - zero, one, or more than 2 elements leading to nested matching - [ last (a::(a'::l)) := last (a'::l) ]. - Yet, doing so is not accepted by Coq's current syntactic guard as the - nested matching forgets that [a'::l] is a subterm of [a::(a'::l)] - and only recall [l] as a smaller subterm. + (** ** 1. Reasoning about indexed inductive types + + Indexed inductive types are particular kind of inductive definitions + that consist in defining not one single inductive type but a family + of linked inductive types. + The most well-known example of indexed inductive types are vectors. + Given a fixed parameter [A : Type], vectors define a familly of inductive + types [vec A n : Type] indexed by natural numbers [n : nat] representing + the lengths of the vectors. + Vectors have two constructor. + The first constructor [vnil : vec A 0] represent the empty vector, + logically of size [0]. + Given an element [a:A] and a vector [v : vec A n] of size [n], the + second constructor [vcons] constructs a vector of size [n+1] + [vcons a n v : vec A (S n)], intuitively by adding [a] at the beginning of [v]. *) -Fail Equations last {A} (l : list A) {struct l} : option (list A) := -last [] := None; -last (a::nil) := Some [a]; -last (a::(a'::l)) := last (a'::l). - -(** For an other example consider the definition of the Ackerman function. - This function is clearly terminating using the lexicographic order : - [(n,m) negb (eq x y)) xs] - is indeed performed on a smaller instance, and so that nubBy is terminating. - Yet, without surprise, it can not be checked automatically using Coq's - syntactic guard as it involves mathematical reasoning on [filter]. -*) - -Fail Equations nubBy {A} (eq : A -> A -> bool) (l : list A) : list A := -nubBy eq [] => []; -nubBy eq (x :: xs) => x :: nubBy eq (filter (fun y => negb (eq x y)) xs). - - -(** TEXT ON WELL-FOUNDED REC - - This functions can still be accepted using well-founded recursion, - that is by directly providing a size measure that is known to be - decreasing and terminating like Type := + | vnil : vec A 0 + | vcons : A -> forall (n : nat), vec A n -> vec A (S n). - This is a very useful technical but it often tedious to apply. - Consequently, Equations provide a built-in mechanism to help us - write functions by well-founded recursion. +Arguments vnil {_}. +Arguments vcons {_} _ _ _. + +(** The difference between a parameter and an indice is that a parameter is + constant over all the constructors, whereas an indice changes in the + constructor. + For instance, in the definition of vectors the type [A] is a parameter + as it is constant in all the constructors, but [n:nat] is an indice as + [vcons] relates two different types of the family, [vec A n] and [vec A (S n)]. + + Reasoning about indexed inductive types like vectors is a bit more + involved than for basic inductive types like lists as the indices can + matter. + Noticeably pattern matching on constructors of indexed inductive types + like [vec n A] may particularise the indices. + For instance, matching a vector [v : vec A n] to [vnil] forces the + value [n] to be [0] and to [vcons] to be of the form [S m] for some integer [m]. + Consequently, when writing a function on an indexed inductive type, + we must also specify the form of the indices when pattern matching. + + For instance, consider the definition of [vmap] and [vapp] : *) +Equations vmap {A B} (f : A -> B) (n : nat) (v : vec A n) : vec B n := +vmap f 0 vnil := vnil ; +vmap f (S n) (vcons a n v) := vcons (f a) n (vmap f n v). +Equations vapp {A} (n : nat) (v : vec A n) (m : nat) (v' : vec A m) : vec A (n+m) := +vapp 0 vnil m v' := v'; +vapp (S n) (vcons a n v) m v' := vcons a (n+m) (vapp n v m v'). -(** ** 1.2 Basic definitions and reasoning - - To define a function by well-founded recursion with Equations, one must - add the command [by wf x rel] where [x] is the term decreasing, - and rel the well-founded relation for which it decrease after the return type. - Equations will then automatically try to prove that the recursive call - are made on decreasing arguments according to the relation. - If it can not do it on its own it will generate a proof obligation, - intuitively a goal for the user to fill. - This enables to separate the proofs from the definition of the function - while dealing automatically with trivial cases. - - In this section, we focus on simple examples where no obligations are - left for the user to refer to section 1.3 for such examples. - - Let's first consider the definition of [last]. - The function [last] terminates as the size of the list decrease in each - recursive call according to the usual well-founded strict order < on nat, - which is named lt in Coq. - Therefore, to define [last] by well-founded recursion, we must - add [wf (length l) lt] after typing. - Once added, we can check that last is now accepted. -*) - -Equations last {A} (l : list A) : option A by wf (length l) lt := -last [] := None; -last (a::nil) := Some a; -last (a::(a'::l)) := last (a'::l). - -(** Thanks to functional elimination through [funelim], we can reason about - function defined by well-founded recursion without having to repeat - the well-founded induction principle. - For each recursive call, the tactic [funelim] will create a goal - goal and an induction hypothesis where all the dependent terms have been - quantified. - - For instance, let's prove that if [l <> nil], then there exists an - [a : A] such that [last l = (Some a)]. - By functional elimination, we only need to deal with the case where - [l := nil], [l := [a]] and [l := (a::a'::l)]. - Moreover, in the last case, we know recursively that - [a' :: l <> [] -> {a : A & last (a' :: l) = Some a}]. - As we can see, the condition [l <> nil] as correctly been - particularise and quantified by. -*) - -Definition exists_last {A} (l : list A) (Hneq : l <> nil) : - { a : A & last l = (Some a)}. -Proof. - funelim (last l); simp last. - - specialize (Hneq eq_refl) as []. - - exists a. reflexivity. - - apply X. discriminate. -Defined. +(** Reasoning on indexed inductive is not very different than reasoning + on regular inductive types except that we have to account for indices, + which can in some cases cause some overheads. -(** Similarly, we can prove that [last] respects [app] in a suitable way. + For basic properties as below, it makes no differences: *) -Definition last_app {A} (l l': list A) (Hneq : l' <> nil) : - last (l ++ l') = last l'. +Definition vmap_comp {A B C} (f : A -> B) (g : B -> C) (n : nat) (v : vec A n) : + vmap g n (vmap f n v) = vmap (fun a => g (f a)) n v. Proof. - funelim (last l); cbn; autorewrite with last. + funelim (vmap f n v). - reflexivity. - - funelim (last l'); simp last. - -- specialize (Hneq eq_refl) as []. - -- reflexivity. - -- reflexivity. - - apply H. assumption. + - simp vmap. f_equal. apply H. Qed. -(** Let's now consider the Ackerman function. - The ackerman function is decreasing according to the usual lexicographic - order on [nat * nat], [(<,<)] which is accessible as both [<] are. - To build the lexicographic order, we use a function predefine in - Equations' library [Equations.Prop.Subterm.lexprod]. - As we can see, once again no obligations are generated as Coq can prove - on its own that [(m, (ack (S m) n)) B) (g : B -> A) (Hrect : forall (a:A), g (f a) = a) + (n : nat) (v : vec A n) : vmap (fun a => g (f a)) n v = vmap (fun a => a) n v. Proof. - induction n; simp ack; auto. - rewrite IHn. reflexivity. - (* Restart. *) - (* WHY SO SLOW ??? *) - (* funelim (ack 1 n). + funelim (vmap _ n v); simp vmap. - reflexivity. - - simp ack. rewrite H. reflexivity. *) + - now rewrite Hrect, H. Qed. -(* ISSUES BUGS + SLOW *) -Definition ack_incr {m n} : ack m n < ack m (n+1). -Proof. - (* COMPLETELY BUGS *) - (* funelim (ack m n). *) - apply ack_elim; intros. - (* ISSUES *) - - cbn. simp ack. -Admitted. - - -(** As exercices, you can try to: - - Prove that if [last l = None] than [l = nil] - - Define a function [removelast] removing the last element of a list - - Prove the two properties about it -*) - -Definition last_none {A} (l : list A) (Hn : last l = None) : l = nil. -Proof. -Admitted. - -Equations removelast {A} (l : list A) : list A by wf (length l) lt := -removelast _ := to_fill. - -Definition removelast_app {A} (l l': list A) (Hneq : l' <> nil) : - removelast (l ++ l') = l ++ removelast l'. -Proof. -Admitted. - -(* You may need to use assert *) -Definition removelast_last {A} (l : list A) (Hneq : l <> nil) : - {a : A & { _ : last l = Some a & l = removelast l ++ [a]}}. +(** However, it can make some differences when operations on indices are + involved as indices are relevant for simplification. + For instance, if we try to prove that [vmap] respects [vapp] as below, + in the [vcons] case simplification fails to simplify [vmap f (S n + m) ...]. + The reason is that the simplification rule associated to [vcons] is + [vmap f (S n) (vcons a n v) = vcons (f a) n (vmap f n v)]. + Hence, [simp] can not simplify [vmap] until [S n + m] has been + simplified to [S (n+m)] using [cbn]. + It then behaves as usual. + *) + +Definition vmap_vapp {A B} (n m : nat) (f : A -> B) (v : vec A n) (v' : vec A m) : + vmap f (n+m) (vapp n v m v') = vapp n (vmap f n v) m (vmap f m v'). Proof. -Admitted. - - -(** ** 1.3 Well-founded recursion and Obligations - - For a more involved example where Coq can not prove on its own that the - recursive call are performed on smaller arguments, let's consider the - [nubBy] function from Haskell's prelude defined below. - - Given an equality test, [nubBy] recursively filters out the duplicates - of a list and only keeps the first occurrence of each element. - It is terminating as the recursive call is performed on - [filter (fun y => negb (eq x y)) xs] which is smaller than [xs] as - [filter] can only remove elements. - Consequently, to define [nubBy] by well-founded recursion, we need to - add [wf (length l) lt]. - - As we can see, it is not enough as Coq can not prove on its own that - the recursive call is indeed smaller, and therefore leaves it for us to prove. - That is, [length (filter (fun y : A => negb (eq x y)) xs) < length (x::xs)]. - It is not surprising as our argument rests on the property that - for any test [f : A -> bool], [length (filter f l) ≤ length l]. - Property that is not trivial, and that Coq can not know to look for, - nor where to look for without any indications. - - To make the obligations generated by well-founded recursion available, - it suffices to start the definition by [Equations?] rather than by - [Equations] as below. - We can then prove the missing properties ourself in proof mode. - This enables to separate the proofs from the definition of the function - while dealing automatically with trivial cases. -*) + funelim (vmap f n v). + - reflexivity. + - simp vapp. + (* Here we can see [simp] fails to simplify [vmap f (S n + m) ...] as + [S n + m] is not of the form [S x] for some [x : nat]. + We need to first simplify [+] using [cbn] : *) + cbn. + (* We can now simplify *) + simp vmap vapp. f_equal. apply H. +Abort. -Equations? nubBy {A} (eq : A -> A -> bool) (l : list A) : list A by wf (length l) lt := -nubBy eq [] => []; -nubBy eq (x :: xs) => x :: nubBy eq (filter (fun y => negb (eq x y)) xs). -Proof. - eapply Nat.le_lt_trans. - - apply filter_length_le. - - auto with arith. -Defined. - -(** reasoning on functions defined by well-founded recursion with - obligations is no different than when there is none. - Using function elimination ([funelim]) we can prove our properties - without having to redo the well-founded recursion. - - As examples, we show how to prove in a few lines that [nubBy] do - remove all duplicates. +(** In practice, indices are mostly inferable, so it is usually possible to + make them implicit. + It has the advantage to make the code much more concise. + For instance, for [vec], it enables to write much shorte definitions + of [vmap] and [vapp]: *) -Lemma In_nubBy {A} (eq : A -> A -> bool) (l : list A) (a : A) - : In a (nubBy eq l) -> In a l. -Proof. - funelim (nubBy eq l); simp nubBy; cbn. - intros [Heq | H0]. - - rewrite Heq. left; reflexivity. - - specialize (H _ H0). apply filter_In in H as [Inal eqa]. - right; assumption. -Qed. - -Lemma nubBy_nodup {A} (eq : A -> A -> bool) (l : list A) : - (forall x y, (eq x y = true) <-> (x = y)) -> NoDup (nubBy eq l). -Proof. - intros Heq; funelim (nubBy eq l). - - simp nubBy. constructor. - - specialize (H Heq). simp nubBy. constructor. - -- intros Hi. - apply In_nubBy in Hi. - apply filter_In in Hi as [_ Hneqx]. - specialize (Heq x x); destruct Heq as [_ Heqx]. - specialize (Heqx eq_refl); rewrite Heqx in Hneqx. - inversion Hneqx. - -- assumption. -Qed. - - -(** ** 2. Different methods to work with well-founded recursion *) - -(** ** 2.1 Subterm relations for indexed inductive types *) - -(** ISSUES: FIND AN EXAMPLE*) -Inductive vec A : nat -> Type := - | vnil : vec A 0 - | vcons : A -> forall (n : nat), vec A n -> vec A (S n). - -Arguments vnil {_}. Arguments vcons {_} _ {_} _. -Derive Signature NoConfusion NoConfusionHom for vec. -Derive Subterm for vec. - -Equations vmap {A B n} (f : A -> B) (v : vec A n) : vec B n := -vmap f vnil := vnil ; -vmap f (vcons a v) := vcons (f a) (vmap f v). - -Check well_founded_vec_subterm : forall A, WellFounded (vec_subterm A). - - -(* ISSUE WORK WITHOUT *) -Equations unzip {A B n} (v : vec (A * B) n) : vec A n * vec B n := -(* by wf (signature_pack v) (@t_subterm (A * B)) := *) -unzip vnil := (vnil, vnil) ; -unzip (vcons (pair x y) v) with unzip v := { -| pair xs ys := (vcons x xs, vcons y ys) }. - -(** We can use the packed relation to do well-founded recursion on the vector. - Note that we do a recursive call on a subterm of type [vector A n] which - must be shown smaller than a [vector A (S n)]. They are actually compared - at the packed type [{ n : nat & vector A n}]. The default obligation - tactic defined in [Equations.Init] includes a proof-search - for [subterm] proofs which can resolve the recursive call obligation - automatically in this case. *) - - - -(** ** 2.2 The inspect method - - When defining a functions, it can happen that we loose information - relevant for termination when matching a value, and that we then get - stuck trying to prove termination. - - In this section, we discuss such an example, and explain a solution to - this problem using the function [inspect]. - - Working with a particular well-founded order [lt], it may happen that - we have a choice function [f : A -> option A] that for any [(a :A)] - return a strictly smaller element if there is one. - This situation is axiomatised by the following context : +Equations vmap' {A B n} (f : A -> B) (v : vec A n) : vec B n := +vmap' f vnil := vnil ; +vmap' f (vcons a v) := vcons (f a) (vmap' f v). + +Equations vapp' {A n m} (v : vec A n) (v' : vec A m) : vec A (n+m) := +vapp' vnil v' := v'; +vapp' (vcons a v) v' := vcons a (vapp' v v'). + +(** Setting indices to be implicit also makes them implicit in proofs. + Doing so is not an issue even in the case of [vmap_vapp] where + we need to simplify indices to reduce. + If we think a term should have been reduced but hasn't been because of + indices, we can always make them temporally explicit to check. + We can do so by defining an alias for the functions using the tactic + [set (name_function_ex := @(name_function _ _ _))] with an underscore + for the arguments we do not want to make explicit. + After inspecting the goal, you can just erase the tactic or unfold + the notations. + As an example, let's reprove [vmap_vapp] : *) -Section Inspect. +Definition vmap_vapp {A B n m }(f : A -> B) (v : vec A n) (v' : vec A m) : + vmap' f (vapp' v v') = vapp' (vmap' f v) (vmap' f v'). +Proof. + funelim (vmap' f v). + - reflexivity. + - simp vapp'. + (* If we think [vmap' f (vcons a ...)] should have been simplified, + we can set an alias to check if the indice is of the form [S x] *) + set (vmap'_ex := @vmap' _ _). + (* After inspecting the goal, you can just erase the tactic + or unfold the alias *) + cbn. unfold vmap'_ex. + (* It is now possible to simplify *) + simp vmap' vapp'. f_equal. apply H. +Abort. - Context {A : Type} {lt : A -> A -> Prop} `{WellFounded A lt} - (f : A -> option A) (decr_f : forall n p, f n = Some p -> lt p n). -(** In this case, given an element (a : A), we may be interested in - computing the associated decreasing chain of elements starting from - [a]. - Naively, we would like to do so as below. - That is check if there is an element smaller than [a] by matching [f a] - with a with clause, if there is one [Some p] then returns [p] added to - chain starting [f_sequence p] here our recursive call, and otherwise - stop the computation. -*) +(** ** 2. The No-Confusion property - Equations? f_sequence (a : A) : list A by wf a lt := - f_sequence a with (f a) := { - | Some p => p :: f_sequence p; - | None => nil - }. - Proof. - apply decr_f. - (* What to do now ? *) - Abort. - -(** Unfortunately, as we can see, if do so it generates an unprovable - obligation as we don't remember information about the call to [f n] being - equal to [Some p] in the recursive call [f_sequence p]. - - To go around this issue and remember the origin of the pattern, - we can wrap our match with the [inspect] function, which simply packs a - value with a proof of an equality to itself. - In other words, given an element [(a : A)], [inspect (a)] returns the - elements [(a, eq_refl) : {b : A | a = b}]. + Having information directly part of typing, like the length for vector, + can have advantages. + Most noticeably, it can be used to exclude invalid cases. + For instance, consider the function tail that returns the last element. + In the case of list, the [tail] function had to return a term of type + [option A] as were no insurance that the input would not be the empty list. + This is not necessary for vectors as we can use the indice to ensure + there is at least one element by defining tail as a function of type + [vec A (S n) -> vec A n]. + This can be implemented very directly with Equations as Equations can + deduce on its own that the [vnil] case is impossible : *) - Definition inspect {A} (a : A) : {b | a = b} := exist _ a eq_refl. - - Notation "x 'eqn:' p" := (exist _ x p) (only parsing, at level 20). - -(** In our case, wrapping with [inspect] means matching first on - [inspect (f a)] then on the first component which is by definition [f a], - rather than directly on the term [f a]. - This may seem pointless as if one destruct [f a] in an equality - [f a = f a], one would surely get [Some p = Some p] and learn nothing ? - The trick here is that [inspect (f a)] returns an object of type - [{b : A | f a = b}], type in which [f a] is a fixed constant. - Consequently, destructing the first component, in our case [f a], - will only affect the right-hand side of the equality, and we will - indeed get the desired equality [f a = Some p]. - As it can be seen below it works perfectly, and Coq is even able to - prove the call is terminating on its own leaving us no obligations - to fill. +Equations vtail {A n} (v : vec A (S n)) : vec A n := +vtail (vcons a v) := v. + +(** Similarly, we can give a very short definition of a function computing + the diagonal of a square matrix of size [n * n] represented as a + vector of vector [v : vector (vector A n) n)]. + On the empty matrice it returns the empty list. + On a matrice [(vcons (vcons a v) v')] of size [(S n) x (S n)] representing + + [[ + | a | v | + |---------------| + | v' | + | | + ]] + + it returns [a] added to the diagonal of vmap [vtail v'], that is + [v'] where the first column has been forgotten. + Note, that in this case, pattern match on [n] needs to be added to help + Coq see it is strictly decreasing. *) - Equations f_sequence (a : A) : list A by wf a lt := - f_sequence a with inspect (f a) := { - | Some p eqn: eq1 => p :: f_sequence p; - | None eqn:_ => List.nil - }. - -End Inspect. - - -(** ** 2.3 Personalising the tactic proving obligations - - When working, it is common to be dealing with a particular class of - functions that shares a common theory, e.g, they involves basic - arithmetic. - Yet, by default the tactic trying to prove obligations is not - aware of the particular theory at hand, and it will fail to solve - most of the obligations generated. - This is normal, it would be very inefficient if Coq were trying to solve - a goal using all lemma ever defined., or even all lemma featuring - [+] in its definition. - Therefore, it can be interesting to define a local custom strategy for - solving obligations specific to our theory at hand. +Equations diag {A n} (v : vec (vec A n) n) : vec A n := +diag (n:=O) vnil := vnil ; +diag (n:=S _) (vcons (vcons a v) v') := + vcons a (diag (vmap vtail v')). + +(** To do so, the pattern-matching compiler behind [Equations] uses unification + with the theory of constructors to discover which cases need to be + considered and which are impossible. + This powerful unification engine running under the hood permits to write + concise code where all uninteresting cases are handled automatically. + Importantly, it relies on the property of no-confusion, that is + that two different constructors of an inductive can not be equal, + here for [nat], [0 = S n -> False]. + The no confusion property can be generated automatically by [Equations] + using the command [Derive]. +*) - In this section, we explain how to do so to for the [gcd] function, - and show how function elimination then enables to prove a few properties - efficiently. +Derive NoConfusion for nat. - TO EXPANSE - To define [gcd x y], we first check if [x] or [y] is [0], and if not - we check if they are equal. +(** You may notice that we have derive the no confusion property for [nat] + after defining [tail] and [diag], even though it supposed the be necessary. + This is because it is already defined for [nat] by default, so + there was actually no need to do derive it in this particular case. - It is terminating as the sum [x + y] is decreasing for the usual - well-founded order on nat, accounted for by [wf (x + y) lt]. + Thanks to [funelim], reasoning for this kind of programs is as usual + to the difference that, as for function definitions, we only need to + deal with the cases that are possible: *) -Equations? gcd (x y : nat) : nat by wf (x + y) lt := -gcd 0 x := x ; -gcd x 0 := x ; -gcd x y with gt_eq_gt_dec x y := { - | inleft (left _) := gcd x (y - x) ; - | inleft (right refl) := x ; - | inright _ := gcd (x - y) y }. +Definition vmap_diag {A B n} (f : A -> B) (v : vec (vec A n) n) : + vmap f (diag v) = diag (vmap (fun v' => vmap f v') v). Proof. - lia. lia. -Abort. + (* We start by induction, simplify and use the induction hypothesis *) + funelim (diag v). reflexivity. simp vmap diag. f_equal. rewrite H. + (* We simplify the goal by collapsing the different [vmap] using [vmap_comp], + and notice the proof boils down to commutativity if [vtail] and [vmap] *) + repeat rewrite vmap_comp. f_equal. apply vmap_cong. + (* There is left to prove that using [vtail] or [vmap] first do no matter *) + intro v2. funelim (vtail v2). simp vmap vtail. reflexivity. +Qed. -(** As we can see, Coq fails to prove the obligations on its own as they - involve basic reasoning on arithmetic, a theory that Coq is unaware of - by default. - This can be checked by using [Show Obligation Tactic] to print the - tactic currently used to solve obligations and inspecting it. -*) -Show Obligation Tactic. +(* TALK ABOUT NO CONFUSION FOR VEC *) -(** The obligations generated are not complicated to prove but tedious, - and they can actually be solved automatically via the arithmetic - solver [lia]. - Therefore, we would like to locally change the tactic solving the - obligations to take into account arithmetic, and try lia. +Derive Signature NoConfusion NoConfusionHom for vec. - To do so, we use the command [ #[local] Obligation Tactic := tac ] - to change locally the tactic solving obligation to a tactic [tac]. - In our case, we choose for [tac] to be the previously used - tactic to which we have added a call to [lia] at the end: +(** ** 3. Unifying Indices and Inaccessible Patterns + + A particularity of indexed inductive type is that during pattern-matching + indices may be particularises to values like variables or terms of + the form [(f (...))], where [f] is not a constructor of an inductive type + like [O] or [S]. + + The most well-known of example of that is equality [| eq A x : A -> Prop |] + that is _parameterized_ by a value [x] of type [A] and _indexed_ + by another value of type [A]. + Its single constructor states that equality is reflexive, so the only way + to build an object of [eq x y] is if [x] is definitionally equal to the + variable [y]. + + [[ + Inductive eq (A : Type) (x : A) : A -> Prop := + | eq_refl : eq A x x. + ]] + + Pattern-matching on the equality then unifies the indice [y] with the + parameter [x], that is to a variable. + Consequently, we have determined the _value_ of the pattern [y], and it is + no longer a candidate for refinement with available constructors like + [0] or [S n]. + Such a pattern is said to be "inaccessible", and needs to be indicated + by writing [?(t)] to tell Equations not to refine it. + + As an example, to prove the symmetry of equality we pattern + match on an equality [H : x = y], which unify [y] the variable [x] + that we indicate by writing [eq_sym x ?(x) eq_refl]. + The goal now being [x = x], it now holds by [eq_refl]. *) -#[local] Obligation Tactic := - simpl in *; - Tactics.program_simplify; - CoreTactics.equations_simpl; - try Tactics.program_solve_wf; - try lia. +Equations eq_sym {A} (x y : A) (H : x = y) : y = x := +eq_sym x ?(x) eq_refl := eq_refl. -(** As we can see by running [Show Obligation Tactic] again, the tactic - has indeed been changed. +(** In practice, when the values determined are variable as in [eq_sym], + the inaccessibility annotation is optional and we can simply write [x] + rather than [?(x)]. *) -Show Obligation Tactic. +Equations eq_trans {A} (x y z : A) (p : x = y) (q : y = z) : x = z := +eq_trans x x x eq_refl eq_refl := eq_refl. -(** We can see our change was useful as [gcd] can now be defined by - well-founded recursion without us having to solve any obligations. +(** For an example, where the [?(t)] notation is needed consider this inductive + definition of the image. + It has one constructor that for all elements [a:A] generates an element + in its image by [f], [Imf f (f a)]. + Intuitively, it means that there is an object in [Imf f x] provided + that [x] is of the form [f a] for some [a]. *) -Equations gcd (x y : nat) : nat by wf (x + y) lt := -gcd 0 x := x ; -gcd x 0 := x ; -gcd x y with gt_eq_gt_dec x y := { - | inleft (left _) := gcd x (y - x) ; - | inleft (right refl) := x ; - | inright _ := gcd (x - y) y }. - - -(** For further examples of how functional elimination works on well-founded - recursion and is useful on complex definitions, we will now show a - few properties of [gcd] +Inductive Imf {A B} (f : A -> B) : B -> Type + := imf (a : A) : Imf f (f a). + +(** Pattern-matching on [im : Imf f t] particularise [t] to be of the form + [f a] for some [a]. + As [f] is not a constructor, [f a] is inaccessible and we need to write + as [?(f a)] in the pattern matching to prevent [Equations] to refine [f] + with available constructors. + In this case, it is essential as [f a] is not a variable. + As an example, we can write a function returning the [a] associated + to on object in the image : *) -Lemma gcd_same x : gcd x x = x. -Proof. - funelim (gcd x x); try lia. reflexivity. -Qed. - -Lemma gcd_spec0 a : gcd a 0 = a. -Proof. - funelim (gcd a 0); reflexivity. -Qed. - -Lemma mod_minus a b : b <> 0 -> b < a -> (a - b) mod b = a mod b. -Proof. - intros. - replace a with ((a - b) + b) at 2 by lia. - rewrite <- Nat.Div0.add_mod_idemp_r; auto. - rewrite Nat.Div0.mod_same; auto. -Qed. - -Lemma gcd_spec1 a b: 0 <> b -> gcd a b = gcd (Nat.modulo a b) b. -Proof. - funelim (gcd a b); intros. - - now rewrite Nat.Div0.mod_0_l. - - reflexivity. - - now rewrite (Nat.mod_small (S n) (S n0)). - - simp gcd; rewrite Heq; simp gcd. - rewrite refl, Nat.Div0.mod_same. - reflexivity. - - simp gcd; rewrite Heq; simp gcd. - rewrite H; auto. rewrite mod_minus; auto. -Qed. \ No newline at end of file +Equations inv {A B} (f : A -> B) (t : B) (im : Imf f t) : A := +inv f ?(f s) (imf f s) := s. From 7fee5fe816c4498cd0f9f3aa6bc9e82586305949 Mon Sep 17 00:00:00 2001 From: thomas-lamiaux Date: Fri, 20 Sep 2024 05:04:50 +0200 Subject: [PATCH 03/12] fix bugs --- src/Tutorial_Equations_indexed.v | 38 +++++++++++++++++--------------- 1 file changed, 20 insertions(+), 18 deletions(-) diff --git a/src/Tutorial_Equations_indexed.v b/src/Tutorial_Equations_indexed.v index 8ea8997f..5dcb85fc 100644 --- a/src/Tutorial_Equations_indexed.v +++ b/src/Tutorial_Equations_indexed.v @@ -88,6 +88,7 @@ Equations vmap {A B} (f : A -> B) (n : nat) (v : vec A n) : vec B n := vmap f 0 vnil := vnil ; vmap f (S n) (vcons a n v) := vcons (f a) n (vmap f n v). + Equations vapp {A} (n : nat) (v : vec A n) (m : nat) (v' : vec A m) : vec A (n+m) := vapp 0 vnil m v' := v'; vapp (S n) (vcons a n v) m v' := vcons a (n+m) (vapp n v m v'). @@ -103,17 +104,17 @@ vapp (S n) (vcons a n v) m v' := vcons a (n+m) (vapp n v m v'). Definition vmap_comp {A B C} (f : A -> B) (g : B -> C) (n : nat) (v : vec A n) : vmap g n (vmap f n v) = vmap (fun a => g (f a)) n v. Proof. - funelim (vmap f n v). + funelim (vmap f n v); simp vmap. - reflexivity. - - simp vmap. f_equal. apply H. + - f_equal. apply H. Qed. -Lemma vmap_rect {A B} (f : A -> B) (g : B -> A) (Hrect : forall (a:A), g (f a) = a) - (n : nat) (v : vec A n) : vmap (fun a => g (f a)) n v = vmap (fun a => a) n v. +Lemma vmap_cong {A B n} (f f': A -> B) (v : vec A n) (Heq : forall (a:A), f a = f' a) + : vmap f n v = vmap f' n v. Proof. - funelim (vmap _ n v); simp vmap. + funelim (vmap f n v); simp vmap. - reflexivity. - - now rewrite Hrect, H. + - now rewrite Heq, (H f'). Qed. (** However, it can make some differences when operations on indices are @@ -130,21 +131,21 @@ Qed. Definition vmap_vapp {A B} (n m : nat) (f : A -> B) (v : vec A n) (v' : vec A m) : vmap f (n+m) (vapp n v m v') = vapp n (vmap f n v) m (vmap f m v'). Proof. - funelim (vmap f n v). + funelim (vmap f n v); simp vapp. - reflexivity. - - simp vapp. - (* Here we can see [simp] fails to simplify [vmap f (S n + m) ...] as - [S n + m] is not of the form [S x] for some [x : nat]. - We need to first simplify [+] using [cbn] : *) + - (* Here we can see [simp] fails to simplify [vmap f (S n + m) ...] as + [S n + m] is not of the form [S x] for some [x : nat]. *) + simp vmap. + (* We need to first simplify [+] using [cbn] : *) cbn. (* We can now simplify *) - simp vmap vapp. f_equal. apply H. + simp vmap vapp. now rewrite H. Abort. (** In practice, indices are mostly inferable, so it is usually possible to make them implicit. It has the advantage to make the code much more concise. - For instance, for [vec], it enables to write much shorte definitions + For instance, for [vec], it enables to write much shorter definitions of [vmap] and [vapp]: *) @@ -227,8 +228,7 @@ vtail (vcons a v) := v. Equations diag {A n} (v : vec (vec A n) n) : vec A n := diag (n:=O) vnil := vnil ; -diag (n:=S _) (vcons (vcons a v) v') := - vcons a (diag (vmap vtail v')). +diag (n:=S _) (vcons (vcons a v) v') := vcons a (diag (vmap vtail _ v')). (** To do so, the pattern-matching compiler behind [Equations] uses unification with the theory of constructors to discover which cases need to be @@ -254,15 +254,17 @@ Derive NoConfusion for nat. deal with the cases that are possible: *) +Arguments vmap {_ _} _ {_} _. + Definition vmap_diag {A B n} (f : A -> B) (v : vec (vec A n) n) : vmap f (diag v) = diag (vmap (fun v' => vmap f v') v). Proof. (* We start by induction, simplify and use the induction hypothesis *) - funelim (diag v). reflexivity. simp vmap diag. f_equal. rewrite H. + funelim (diag v); simp vmap diag. 1: easy. rewrite H. f_equal. (* We simplify the goal by collapsing the different [vmap] using [vmap_comp], and notice the proof boils down to commutativity if [vtail] and [vmap] *) - repeat rewrite vmap_comp. f_equal. apply vmap_cong. - (* There is left to prove that using [vtail] or [vmap] first do no matter *) + rewrite ! vmap_comp. f_equal. apply vmap_cong. + (* There is left to prove by function elimination on [vtail] or [vmap] *) intro v2. funelim (vtail v2). simp vmap vtail. reflexivity. Qed. From 4c1466e5c790539dd9049a88c283d3a0bde5d078 Mon Sep 17 00:00:00 2001 From: thomas-lamiaux Date: Mon, 7 Oct 2024 21:25:35 +0200 Subject: [PATCH 04/12] add text on NoConfusion --- src/Tutorial_Equations_indexed.v | 115 +++++++++++++++++++++++-------- 1 file changed, 87 insertions(+), 28 deletions(-) diff --git a/src/Tutorial_Equations_indexed.v b/src/Tutorial_Equations_indexed.v index 5dcb85fc..af83ebd7 100644 --- a/src/Tutorial_Equations_indexed.v +++ b/src/Tutorial_Equations_indexed.v @@ -85,9 +85,10 @@ Arguments vcons {_} _ _ _. *) Equations vmap {A B} (f : A -> B) (n : nat) (v : vec A n) : vec B n := -vmap f 0 vnil := vnil ; -vmap f (S n) (vcons a n v) := vcons (f a) n (vmap f n v). +vmap f _ vnil := vnil ; +vmap f _ (vcons a n v) := vcons (f a) n (vmap f n v). +Print vmap. Equations vapp {A} (n : nat) (v : vec A n) (m : nat) (v' : vec A m) : vec A (n+m) := vapp 0 vnil m v' := v'; @@ -142,7 +143,10 @@ Proof. simp vmap vapp. now rewrite H. Abort. -(** In practice, indices are mostly inferable, so it is usually possible to +(** This is not a limitaton of [Equations] itself. It is due to how the + [rewrite] tactic behind [simp] unifies terms. + + In practice, indices are mostly inferable, so it is usually possible to make them implicit. It has the advantage to make the code much more concise. For instance, for [vec], it enables to write much shorter definitions @@ -191,16 +195,18 @@ Abort. (** ** 2. The No-Confusion property + *** 2.1 Discarding Impossible Cases + Having information directly part of typing, like the length for vector, can have advantages. - Most noticeably, it can be used to exclude invalid cases. + Most noticeably, it can be used to exclude invalid cases automatically. For instance, consider the function tail that returns the last element. - In the case of list, the [tail] function had to return a term of type + In the case of [list], the [tail] function had to return a term of type [option A] as were no insurance that the input would not be the empty list. This is not necessary for vectors as we can use the indice to ensure there is at least one element by defining tail as a function of type [vec A (S n) -> vec A n]. - This can be implemented very directly with Equations as Equations can + This can be implemented very directly with [Equations] as [Equations] can deduce on its own that the [vnil] case is impossible : *) @@ -222,6 +228,7 @@ vtail (vcons a v) := v. it returns [a] added to the diagonal of vmap [vtail v'], that is [v'] where the first column has been forgotten. + Note, that in this case, pattern match on [n] needs to be added to help Coq see it is strictly decreasing. *) @@ -230,26 +237,7 @@ Equations diag {A n} (v : vec (vec A n) n) : vec A n := diag (n:=O) vnil := vnil ; diag (n:=S _) (vcons (vcons a v) v') := vcons a (diag (vmap vtail _ v')). -(** To do so, the pattern-matching compiler behind [Equations] uses unification - with the theory of constructors to discover which cases need to be - considered and which are impossible. - This powerful unification engine running under the hood permits to write - concise code where all uninteresting cases are handled automatically. - Importantly, it relies on the property of no-confusion, that is - that two different constructors of an inductive can not be equal, - here for [nat], [0 = S n -> False]. - The no confusion property can be generated automatically by [Equations] - using the command [Derive]. -*) - -Derive NoConfusion for nat. - -(** You may notice that we have derive the no confusion property for [nat] - after defining [tail] and [diag], even though it supposed the be necessary. - This is because it is already defined for [nat] by default, so - there was actually no need to do derive it in this particular case. - - Thanks to [funelim], reasoning for this kind of programs is as usual +(** Thanks to [funelim], reasoning for this kind of programs is as usual to the difference that, as for function definitions, we only need to deal with the cases that are possible: *) @@ -269,10 +257,81 @@ Proof. Qed. -(* TALK ABOUT NO CONFUSION FOR VEC *) +(** *** 2.2 The No-Confusion properties + + To do so, the elaboration procedure behind [Equations] relies crucially on + no-confusion properties to deduce which cases are impossible, enabling to + write concise code where all uninteresting cases are handled automatically. + + No confusion properties basically embodies both discrimination and injectivity + of constructors: it asserts which equations are impossible because the head + constructors do not match and if they do simplifies the equations. + + The cases above relies on the no-confusion property for [nat], that given + [n], [m] eturns [True] if [n] and [m] are both [0], [n = m] if they are both + of the form [S n], [S m], and [False] otherwise. + + [Equations] provides a [Derive] command to generate them automatically. + For instance, for [nat], it suffices to write: +*) + +Derive NoConfusion for nat. +Check NoConfusion_nat. + +(** You may have noticed that we have derive the no confusion property for [nat] + after defining [tail] and [diag], even though it supposed the be necessary. + This is because it is already defined for [nat] by default, so there was + actually no need to do derive it in this particular case. -Derive Signature NoConfusion NoConfusionHom for vec. + For index inductive types, they are two kind of no-confusion properties + that can be derived by [Equations]: + - The [NoConfusion] property that enable to distinguish object with different indices. + It takes as argument objects in the total space {n : nat & vec A n}: +*) +Derive NoConfusion for vec. +Check NoConfusion_vec. + +(** + - The [NoConfusionHom] property that enables to disinguish objects with the + same indices, which is useful for simplifying equations: +*) + +Derive NoConfusionHom for vec. +Check NoConfusionHom_vec. + +(** The [NonConfusionHom] property is not derivable for all index inductive types. + It only is when equality of constructors can be reduced to equality of forced + argument, that is indices ??? + + If it not possible to derive it, then [Equations] may need the indices to + satify Uniqueness of Identity Proof asserting that all proofs are equal, i.e. + [UIP : forall (A : Type) (a b : A) (p q : a = b), p = q], to be able to + elaborate the definition to a Coq term. + + It can be proven for some types like [nat], but in the general case, this is + an axiom that is compatible with Coq and classical logical but incosistent + with univalence, so you may not want to admit it globally. + [Equations] offers both choices, you can declare it for a specific type + or assume it globally: +*) + + + + + +(** *** 2.3 Depelim *) + +(** They come with a tactic apply_noconfusion *) + +Section Foo. + (* Context (A : Type). + Context (a b : A).*) + +Definition foo (x y : vec nat 2) (H : x = y) : x = y. + depelim H. +Abort. +End Foo. (** ** 3. Unifying Indices and Inaccessible Patterns From 69e46bf0912daac9b37d698dcbb1c9efd496319c Mon Sep 17 00:00:00 2001 From: thomas-lamiaux Date: Tue, 8 Oct 2024 16:39:56 +0200 Subject: [PATCH 05/12] add text uip and inacessible patterns --- src/Tutorial_Equations_indexed.v | 81 +++++++++++++++++++++----------- 1 file changed, 53 insertions(+), 28 deletions(-) diff --git a/src/Tutorial_Equations_indexed.v b/src/Tutorial_Equations_indexed.v index af83ebd7..7cc49b93 100644 --- a/src/Tutorial_Equations_indexed.v +++ b/src/Tutorial_Equations_indexed.v @@ -64,11 +64,11 @@ Inductive vec A : nat -> Type := Arguments vnil {_}. Arguments vcons {_} _ _ _. -(** The difference between a parameter and an indice is that a parameter is - constant over all the constructors, whereas an indice changes in the +(** The difference between a parameter and an index is that a parameter is + constant over all the constructors, whereas an index changes in the constructor. For instance, in the definition of vectors the type [A] is a parameter - as it is constant in all the constructors, but [n:nat] is an indice as + as it is constant in all the constructors, but [n:nat] is an index as [vcons] relates two different types of the family, [vec A n] and [vec A (S n)]. Reasoning about indexed inductive types like vectors is a bit more @@ -95,7 +95,7 @@ vapp 0 vnil m v' := v'; vapp (S n) (vcons a n v) m v' := vcons a (n+m) (vapp n v m v'). -(** Reasoning on indexed inductive is not very different than reasoning +(** Reasoning on indexed inductive is not very different from reasoning on regular inductive types except that we have to account for indices, which can in some cases cause some overheads. @@ -143,7 +143,7 @@ Proof. simp vmap vapp. now rewrite H. Abort. -(** This is not a limitaton of [Equations] itself. It is due to how the +(** This is not a limitation of [Equations] itself. It is due to how the [rewrite] tactic behind [simp] unifies terms. In practice, indices are mostly inferable, so it is usually possible to @@ -183,7 +183,7 @@ Proof. - reflexivity. - simp vapp'. (* If we think [vmap' f (vcons a ...)] should have been simplified, - we can set an alias to check if the indice is of the form [S x] *) + we can set an alias to check if the index is of the form [S x] *) set (vmap'_ex := @vmap' _ _). (* After inspecting the goal, you can just erase the tactic or unfold the alias *) @@ -203,7 +203,7 @@ Abort. For instance, consider the function tail that returns the last element. In the case of [list], the [tail] function had to return a term of type [option A] as were no insurance that the input would not be the empty list. - This is not necessary for vectors as we can use the indice to ensure + This is not necessary for vectors as we can use the index to ensure there is at least one element by defining tail as a function of type [vec A (S n) -> vec A n]. This can be implemented very directly with [Equations] as [Equations] can @@ -216,8 +216,8 @@ vtail (vcons a v) := v. (** Similarly, we can give a very short definition of a function computing the diagonal of a square matrix of size [n * n] represented as a vector of vector [v : vector (vector A n) n)]. - On the empty matrice it returns the empty list. - On a matrice [(vcons (vcons a v) v')] of size [(S n) x (S n)] representing + On the empty matrix it returns the empty list. + On a matrix [(vcons (vcons a v) v')] of size [(S n) x (S n)] representing [[ | a | v | @@ -264,8 +264,8 @@ Qed. write concise code where all uninteresting cases are handled automatically. No confusion properties basically embodies both discrimination and injectivity - of constructors: it asserts which equations are impossible because the head - constructors do not match and if they do simplifies the equations. + of constructors: they assert which equations are impossible because the head + constructors do not match, and if they do, simplify the equations. The cases above relies on the no-confusion property for [nat], that given [n], [m] eturns [True] if [n] and [m] are both [0], [n = m] if they are both @@ -279,12 +279,13 @@ Derive NoConfusion for nat. Check NoConfusion_nat. (** You may have noticed that we have derive the no confusion property for [nat] - after defining [tail] and [diag], even though it supposed the be necessary. + after defining [tail] and [diag], even though it is supposed to be necessary. This is because it is already defined for [nat] by default, so there was actually no need to do derive it in this particular case. - For index inductive types, they are two kind of no-confusion properties - that can be derived by [Equations]: + [nat] is a very simple inductive type. + In the general case, for index inductive types, they are two kind of no-confusion + properties that can be derived by [Equations]: - The [NoConfusion] property that enable to distinguish object with different indices. It takes as argument objects in the total space {n : nat & vec A n}: *) @@ -301,22 +302,28 @@ Check NoConfusionHom_vec. (** The [NonConfusionHom] property is not derivable for all index inductive types. It only is when equality of constructors can be reduced to equality of forced - argument, that is indices ??? + argument, that is indices ???. + Note, that for most of the basic index inductive types, this is the case, + so it rarely an issue in practice. - If it not possible to derive it, then [Equations] may need the indices to - satify Uniqueness of Identity Proof asserting that all proofs are equal, i.e. + If it is not possible to derive it, then [Equations] may need the indices to + satify Uniqueness of Identity Proof, asserting that all proofs are equal, i.e. [UIP : forall (A : Type) (a b : A) (p q : a = b), p = q], to be able to elaborate the definition to a Coq term. - It can be proven for some types like [nat], but in the general case, this is - an axiom that is compatible with Coq and classical logical but incosistent - with univalence, so you may not want to admit it globally. - [Equations] offers both choices, you can declare it for a specific type - or assume it globally: + UIP holds for some types like [nat], but in the general case, this is an axiom. + It is compatible with Coq and classical logical but inconsistent + with univalence, so you may not want to admit it globally in your development. + Consequently, [Equations] offers both options: you can declare it only for the types + for which you can prove it or need it, or or assume it globally: *) +(* Assuming you can prove it *) +Axiom uip_nat : UIP nat. +Local Existing Instance uip_nat. - +Axiom uipa : forall A, UIP A. +Local Existing Instance uipa. (** *** 2.3 Depelim *) @@ -336,7 +343,7 @@ End Foo. (** ** 3. Unifying Indices and Inaccessible Patterns A particularity of indexed inductive type is that during pattern-matching - indices may be particularises to values like variables or terms of + indices may be particularised to values like variables or terms of the form [(f (...))], where [f] is not a constructor of an inductive type like [O] or [S]. @@ -352,7 +359,7 @@ End Foo. | eq_refl : eq A x x. ]] - Pattern-matching on the equality then unifies the indice [y] with the + Pattern-matching on the equality then unifies the index [y] with the parameter [x], that is to a variable. Consequently, we have determined the _value_ of the pattern [y], and it is no longer a candidate for refinement with available constructors like @@ -371,13 +378,13 @@ eq_sym x ?(x) eq_refl := eq_refl. (** In practice, when the values determined are variable as in [eq_sym], the inaccessibility annotation is optional and we can simply write [x] - rather than [?(x)]. + or a wild card [_] rather than [?(x)]. *) Equations eq_trans {A} (x y z : A) (p : x = y) (q : y = z) : x = z := eq_trans x x x eq_refl eq_refl := eq_refl. -(** For an example, where the [?(t)] notation is needed consider this inductive +(** For an example, where the [?(t)] notation is needed, consider this inductive definition of the image. It has one constructor that for all elements [a:A] generates an element in its image by [f], [Imf f (f a)]. @@ -395,8 +402,26 @@ Inductive Imf {A B} (f : A -> B) : B -> Type with available constructors. In this case, it is essential as [f a] is not a variable. As an example, we can write a function returning the [a] associated - to on object in the image : + to an object in the image : *) Equations inv {A B} (f : A -> B) (t : B) (im : Imf f t) : A := inv f ?(f s) (imf f s) := s. + +(** Be careful that if you forget to mark inaccessible patterns, then [Equations] + will try to match on the patterns, creating potentially pointless branches. + It is fine in theory as the definition obtained will be logically equivalent + provided elaboration succededs, but annoying if you want to extract the code as the definition will be more involved. + + For instance, if we define [vmap''] by matching on [n] without marking the + pattern associated to [n] as inaccessible, we can see at extraction that [Equations] + matched [n] and end up with absurd branch to eliminates, yielding a more complicated + definition than the original [vmap]: +*) + +Equations vmap'' {A B} (f : A -> B) (n : nat) (v : vec A n) : vec B n := +vmap'' f 0 vnil := vnil ; +vmap'' f (S n) (vcons a v) := vcons (f a) (vmap'' f n v). + +Extraction vmap. +Extraction vmap''. \ No newline at end of file From 244b7c1bd7ef2901c19d434ed89dbce9986706eb Mon Sep 17 00:00:00 2001 From: thomas-lamiaux Date: Tue, 8 Oct 2024 17:06:53 +0200 Subject: [PATCH 06/12] first draf --- src/Tutorial_Equations_indexed.v | 44 ++++++++++++++++++++++---------- 1 file changed, 30 insertions(+), 14 deletions(-) diff --git a/src/Tutorial_Equations_indexed.v b/src/Tutorial_Equations_indexed.v index 7cc49b93..109c4a32 100644 --- a/src/Tutorial_Equations_indexed.v +++ b/src/Tutorial_Equations_indexed.v @@ -17,8 +17,11 @@ to particularise indices when matching, and issues that can arise. *** Table of content - - 1. Reasoning about indexed inductive types - - 2. The No-Confusion property + - 1. Basic Reasoning on Indexed Inductive Types + - 2. Advanced Dependent Pattern Matching + - 2.1 Discarding Automatically Impossible Cases + - 2.2 The No-Confusion Properties + - 2.3 The Tactic Depelim - 3. Unifying Indices and Inaccessible Patterns *** Prerequisites: @@ -40,7 +43,7 @@ From Equations Require Import Equations. - (** ** 1. Reasoning about indexed inductive types + (** ** 1. Basic Reasoning on Indexed Inductive Types Indexed inductive types are particular kind of inductive definitions that consist in defining not one single inductive type but a family @@ -193,9 +196,9 @@ Proof. Abort. -(** ** 2. The No-Confusion property +(** ** 2. Advanced Dependent Pattern Matching - *** 2.1 Discarding Impossible Cases + *** 2.1 Discarding Automatically Impossible Cases Having information directly part of typing, like the length for vector, can have advantages. @@ -257,7 +260,7 @@ Proof. Qed. -(** *** 2.2 The No-Confusion properties +(** *** 2.2 The No-Confusion Properties To do so, the elaboration procedure behind [Equations] relies crucially on no-confusion properties to deduce which cases are impossible, enabling to @@ -326,19 +329,32 @@ Axiom uipa : forall A, UIP A. Local Existing Instance uipa. -(** *** 2.3 Depelim *) -(** They come with a tactic apply_noconfusion *) +(** *** 2.3 The Tactic Depelim *) + +(** [Equations] provide a tactic [depelim] to recursively simplify and invert + equations and simplify the goals, which is based on the [NoConfusion] + principles and [Equations] simplification engine. + When index inductive types are involved, it often provides a better simplification + tactic than the default [inversion] tactic. +*) Section Foo. - (* Context (A : Type). - Context (a b : A).*) + Context (A : Type). + Context (a b : A). -Definition foo (x y : vec nat 2) (H : x = y) : x = y. - depelim H. -Abort. +Goal forall (x y : vec A 2), (vcons a (vcons a x) = vcons a (vcons b y)) -> a = b /\ x = y. + intros x y H. depelim H. now split. +Qed. + +Goal forall ( x : vec A 2) z, (vcons a x = z) -> vtail z = x. + intros x z H. depelim H. simp vtail. reflexivity. +Qed. + +Goal forall (x : vec nat 2), (vcons 0 x = vcons 1 x) -> False. + intros x H. depelim H. +Qed. -End Foo. (** ** 3. Unifying Indices and Inaccessible Patterns From 134e8a72d51cf75234958628882ea63ca759006a Mon Sep 17 00:00:00 2001 From: Thomas Lamiaux <85848641+thomas-lamiaux@users.noreply.github.com> Date: Fri, 11 Oct 2024 18:22:11 +0200 Subject: [PATCH 07/12] Update Tutorial_Equations_indexed.v --- src/Tutorial_Equations_indexed.v | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/src/Tutorial_Equations_indexed.v b/src/Tutorial_Equations_indexed.v index 109c4a32..a7dd0a66 100644 --- a/src/Tutorial_Equations_indexed.v +++ b/src/Tutorial_Equations_indexed.v @@ -303,11 +303,10 @@ Check NoConfusion_vec. Derive NoConfusionHom for vec. Check NoConfusionHom_vec. -(** The [NonConfusionHom] property is not derivable for all index inductive types. + (** Though, the [NonConfusionHom] property is derivable for most index inductive types, + it is not the case that is is derivable for all index inductive types. It only is when equality of constructors can be reduced to equality of forced - argument, that is indices ???. - Note, that for most of the basic index inductive types, this is the case, - so it rarely an issue in practice. + argument, that is ??? If it is not possible to derive it, then [Equations] may need the indices to satify Uniqueness of Identity Proof, asserting that all proofs are equal, i.e. @@ -440,4 +439,4 @@ vmap'' f 0 vnil := vnil ; vmap'' f (S n) (vcons a v) := vcons (f a) (vmap'' f n v). Extraction vmap. -Extraction vmap''. \ No newline at end of file +Extraction vmap''. From 698277db9dcaa83da4a53d5433c223fb9f3e3cb5 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Sun, 9 Feb 2025 06:39:17 +0100 Subject: [PATCH 08/12] Typos, rephrasings and more explanations --- src/Tutorial_Equations_indexed.v | 223 +++++++++++++++++++++---------- 1 file changed, 153 insertions(+), 70 deletions(-) diff --git a/src/Tutorial_Equations_indexed.v b/src/Tutorial_Equations_indexed.v index a7dd0a66..9c5275b8 100644 --- a/src/Tutorial_Equations_indexed.v +++ b/src/Tutorial_Equations_indexed.v @@ -48,11 +48,11 @@ From Equations Require Import Equations. Indexed inductive types are particular kind of inductive definitions that consist in defining not one single inductive type but a family of linked inductive types. - The most well-known example of indexed inductive types are vectors. + On of the most well-known examples of indexed inductive types are vectors. Given a fixed parameter [A : Type], vectors define a familly of inductive types [vec A n : Type] indexed by natural numbers [n : nat] representing the lengths of the vectors. - Vectors have two constructor. + The Vector type has two constructors. The first constructor [vnil : vec A 0] represent the empty vector, logically of size [0]. Given an element [a:A] and a vector [v : vec A n] of size [n], the @@ -73,17 +73,20 @@ Arguments vcons {_} _ _ _. For instance, in the definition of vectors the type [A] is a parameter as it is constant in all the constructors, but [n:nat] is an index as [vcons] relates two different types of the family, [vec A n] and [vec A (S n)]. + Indices always appear after the [:] in an inductive type declaration. Reasoning about indexed inductive types like vectors is a bit more involved than for basic inductive types like lists as the indices can matter. Noticeably pattern matching on constructors of indexed inductive types - like [vec n A] may particularise the indices. + like [vec A n] may particularise the indices. For instance, matching a vector [v : vec A n] to [vnil] forces the - value [n] to be [0] and to [vcons] to be of the form [S m] for some integer [m]. + value [n] to be [0] while for [vcons] if forces [n] to be of the form + [S m] for some integer [m]. Consequently, when writing a function on an indexed inductive type, - we must also specify the form of the indices when pattern matching. - + pattern-matching on the inductive type has an effect on other arguments + of the function, specializing them. + For instance, consider the definition of [vmap] and [vapp] : *) @@ -95,8 +98,10 @@ Print vmap. Equations vapp {A} (n : nat) (v : vec A n) (m : nat) (v' : vec A m) : vec A (n+m) := vapp 0 vnil m v' := v'; -vapp (S n) (vcons a n v) m v' := vcons a (n+m) (vapp n v m v'). +vapp (S n') (vcons a n' v) m v' := vcons a (n'+m) (vapp n' v m v'). +(* Here the only two possibly well-typed patterns when considering the [vnil] and [vcons] + constructors are respectively with [n = 0] and [n = S n'] for some fresh [n'] variable. *) (** Reasoning on indexed inductive is not very different from reasoning on regular inductive types except that we have to account for indices, @@ -144,7 +149,7 @@ Proof. cbn. (* We can now simplify *) simp vmap vapp. now rewrite H. -Abort. +Qed. (** This is not a limitation of [Equations] itself. It is due to how the [rewrite] tactic behind [simp] unifies terms. @@ -179,7 +184,7 @@ vapp' (vcons a v) v' := vcons a (vapp' v v'). As an example, let's reprove [vmap_vapp] : *) -Definition vmap_vapp {A B n m }(f : A -> B) (v : vec A n) (v' : vec A m) : +Definition vmap_vapp' {A B n m }(f : A -> B) (v : vec A n) (v' : vec A m) : vmap' f (vapp' v v') = vapp' (vmap' f v) (vmap' f v'). Proof. funelim (vmap' f v). @@ -195,6 +200,20 @@ Proof. simp vmap' vapp'. f_equal. apply H. Abort. +(** An alternative is to change the way [rewrite] looks for matching subterms + in the goal, using the keyed unification strategy. With this setting, [rewrite (e : t = u)] + looks for a syntactic match for the head of [t] in the goal but allows full + conversion between arguments of [t] and the arguments of the matched application + in the goal. This makes [simp] work up-to conversion of the indices. + We can then directly call [congruence] to solve the induction case. *) + +#[local] Set Keyed Unification. + +Definition vmap_vapp_simp {A B n m }(f : A -> B) (v : vec A n) (v' : vec A m) : + vmap' f (vapp' v v') = vapp' (vmap' f v) (vmap' f v'). +Proof. + funelim (vmap' f v); simp vmap' vapp'; [reflexivity|congruence]. +Qed. (** ** 2. Advanced Dependent Pattern Matching @@ -204,8 +223,8 @@ Abort. can have advantages. Most noticeably, it can be used to exclude invalid cases automatically. For instance, consider the function tail that returns the last element. - In the case of [list], the [tail] function had to return a term of type - [option A] as were no insurance that the input would not be the empty list. + In the case of [list], the [tail] function has to return a term of type + [option A] as there is no guarantee that the input is not the empty list. This is not necessary for vectors as we can use the index to ensure there is at least one element by defining tail as a function of type [vec A (S n) -> vec A n]. @@ -229,11 +248,13 @@ vtail (vcons a v) := v. | | ]] - it returns [a] added to the diagonal of vmap [vtail v'], that is + it returns [a] added to the diagonal of [vmap vtail v'], that is [v'] where the first column has been forgotten. - Note, that in this case, pattern match on [n] needs to be added to help - Coq see it is strictly decreasing. + Note, that in this case, pattern matching on [n] needs to be added to help + Coq see it is a strictly decreasing structurally recursive definition on the index. + [vmap vtail v'] can otherwise not be recognized as a syntactic subterm of [v']. + An alternative definition using well founded-recursion is presented below. *) Equations diag {A n} (v : vec (vec A n) n) : vec A n := @@ -253,10 +274,10 @@ Proof. (* We start by induction, simplify and use the induction hypothesis *) funelim (diag v); simp vmap diag. 1: easy. rewrite H. f_equal. (* We simplify the goal by collapsing the different [vmap] using [vmap_comp], - and notice the proof boils down to commutativity if [vtail] and [vmap] *) + and notice the proof boils down to commutativity of [vtail] and [vmap] *) rewrite ! vmap_comp. f_equal. apply vmap_cong. (* There is left to prove by function elimination on [vtail] or [vmap] *) - intro v2. funelim (vtail v2). simp vmap vtail. reflexivity. + intro v2. clear -v2. funelim (vtail v2). simp vmap vtail. reflexivity. Qed. @@ -266,98 +287,144 @@ Qed. no-confusion properties to deduce which cases are impossible, enabling to write concise code where all uninteresting cases are handled automatically. - No confusion properties basically embodies both discrimination and injectivity + No-confusion properties basically embodies both discrimination and injectivity of constructors: they assert which equations are impossible because the head - constructors do not match, and if they do, simplify the equations. + constructors do not match, or if they do match, simplify to equations between the + constructor arguments. - The cases above relies on the no-confusion property for [nat], that given + The cases above rely on the no-confusion property for [nat], that given [n], [m] eturns [True] if [n] and [m] are both [0], [n = m] if they are both of the form [S n], [S m], and [False] otherwise. - [Equations] provides a [Derive] command to generate them automatically. + [Equations] provides a [Derive] command to generate this notion automatically + for each inductive type. For instance, for [nat], it suffices to write: *) Derive NoConfusion for nat. -Check NoConfusion_nat. +Print NoConfusion_nat. -(** You may have noticed that we have derive the no confusion property for [nat] +(** You may have noticed that we have derived the no-confusion property for [nat] after defining [tail] and [diag], even though it is supposed to be necessary. This is because it is already defined for [nat] by default, so there was actually no need to do derive it in this particular case. [nat] is a very simple inductive type. - In the general case, for index inductive types, they are two kind of no-confusion + In the general case, for indexed inductive types, there are two kind of no-confusion properties that can be derived by [Equations]: - - The [NoConfusion] property that enable to distinguish object with different indices. - It takes as argument objects in the total space {n : nat & vec A n}: + - The [NoConfusion] property that enables to distinguish object with different indices. + It takes as argument objects in the total space {n : nat & vec A n} and it is used + to solve general equations between objects in potentially different instances of the + inductive family: *) Derive NoConfusion for vec. Check NoConfusion_vec. (** - - The [NoConfusionHom] property that enables to disinguish objects with the - same indices, which is useful for simplifying equations: + - The [NoConfusionHom] property that enables to distinguish objects with the + same indices (i.e., in the same instance of the inductive family), which + is useful for simplifying homogeneous equations: *) Derive NoConfusionHom for vec. -Check NoConfusionHom_vec. +Print NoConfusionHom_vec. - (** Though, the [NonConfusionHom] property is derivable for most index inductive types, - it is not the case that is is derivable for all index inductive types. - It only is when equality of constructors can be reduced to equality of forced - argument, that is ??? +(** Though, the [NoConfusionHom] property is derivable for many indexed inductive types, + it is not the case that is derivable for all indexed inductive types. + It is derivable only when equality of constructors can be reduced to equality + of the non-forced constructor arguments. For example on vectors, this + corresponds to the fact that + [vcons a n v = vcons a' n v' :> vec A (S n) <-> a = a' /\ v = v' :> vec A n]. If it is not possible to derive it, then [Equations] may need the indices to - satify Uniqueness of Identity Proof, asserting that all proofs are equal, i.e. - [UIP : forall (A : Type) (a b : A) (p q : a = b), p = q], to be able to + satisfy Uniqueness of Identity Proofs, asserting that all equality proofs are + equal, i.e. [UIP : forall (A : Type) (a b : A) (p q : a = b), p = q], to be able to elaborate the definition to a Coq term. - UIP holds for some types like [nat], but in the general case, this is an axiom. - It is compatible with Coq and classical logical but inconsistent - with univalence, so you may not want to admit it globally in your development. + UIP holds for types like [nat] where equality is decidable, but it is not provable + for all types. In particular, it is not provable for [Type] itself. + It can be assumed as an axiom, but be mindful that while this is consistent with Coq's + vanilla theory and classical logic axioms, it is inconsistent with univalence, so you + may not want to admit it globally in your development. Also, as for any axiom, + it will result in stuck computations: [Equations] definitions relying on it will only be + simplifiable using [simp] but no longer compute using e.g. [Eval compute]. + Consequently, [Equations] offers both options: you can declare it only for the types - for which you can prove it or need it, or or assume it globally: + for which you can prove it or need it, or assume it globally: *) -(* Assuming you can prove it *) -Axiom uip_nat : UIP nat. +(** Assuming you can prove it, from e.g. decidability of equality *) +Definition uip_nat : UIP nat := eqdec_uip nat_EqDec. Local Existing Instance uip_nat. +(** Dangerous, incompatible with univalence, and results in stuck computations. *) Axiom uipa : forall A, UIP A. Local Existing Instance uipa. +(** *** 2.3 No-confusion and Dependent Elimination Tactics *) +Require Import Arith. +Section Tactics. - -(** *** 2.3 The Tactic Depelim *) - -(** [Equations] provide a tactic [depelim] to recursively simplify and invert - equations and simplify the goals, which is based on the [NoConfusion] - principles and [Equations] simplification engine. - When index inductive types are involved, it often provides a better simplification - tactic than the default [inversion] tactic. +(** [Equations] provides tactics to access the pattern-matching and simplification + engines directly inside proofs. + When indexed inductive types are involved, it often provides better simplification + tactics than the default [injection] and [inversion] tactics, that can handle + dependent cases. *) -Section Foo. +(** To explicit pattern-matching and control the naming of variables/hypotheses + introduced by an elimination, it is possible to use the + [dependent elimination] tactic, which provides access to the [Equations] + pattern-matching notation inside proofs: *) + + Goal forall a b (x : vec nat 2), (vcons a x = vcons b x) -> a = b. + Proof. + intros a b x H. + (** [x : vec nat 2], so the only possible case to consider is two [vcons] applications + ending with [vnil]. *) + dependent elimination x as [vcons hd (vcons tl vnil)]. + (** [H : vcons a ... = vcons b ...] which implies [a = b]. [noconf H] applies + no-confusion and substitution properties recursively to the type of [H] to + simplify it, resulting in a substitution of [b] by [a] in the goal. *) + noconf H. reflexivity. + Qed. + + (* The [dependent elimination] tactic is robust: it will fail if the + pattern-matching if non-exhaustive or contains unused clauses *) + Goal forall a b (x : vec nat 2), (vcons a x = vcons b x) -> a = b. + Proof. + intros a b x H. + (** [x : vec nat 2], so the only possible case to consider is + two [vcons] applications ending with [vnil]. *) + (* This pattern-matching is non-exhaustive for [x: vec A 2]*) + Fail dependent elimination x as [vcons hd vnil]. + (* This pattern-matching contains an unused clause for [x : vec A 2]*) + Fail dependent elimination x as [vcons hd (vcons tl vnil)|vcons hd vnil]. + Abort. + +(** A more low-level and fragile tactic [depelim] is also available, which can + generate fresh names for the new variables and does not require patterns. *) + Context (A : Type). Context (a b : A). -Goal forall (x y : vec A 2), (vcons a (vcons a x) = vcons a (vcons b y)) -> a = b /\ x = y. - intros x y H. depelim H. now split. -Qed. + Goal forall (x y : vec A 2), (vcons a (vcons a x) = vcons a (vcons b y)) -> a = b /\ x = y. + intros x y H. depelim H. now split. + Qed. -Goal forall ( x : vec A 2) z, (vcons a x = z) -> vtail z = x. - intros x z H. depelim H. simp vtail. reflexivity. -Qed. + Goal forall ( x : vec A 2) z, (vcons a x = z) -> vtail z = x. + intros x z H. depelim H. simp vtail. reflexivity. + Qed. -Goal forall (x : vec nat 2), (vcons 0 x = vcons 1 x) -> False. - intros x H. depelim H. -Qed. + Goal forall (x : vec nat 2), (vcons 0 x = vcons 1 x) -> False. + intros x H. depelim H. + Qed. +End Tactics. (** ** 3. Unifying Indices and Inaccessible Patterns - A particularity of indexed inductive type is that during pattern-matching + A particularity of indexed inductive types is that during pattern-matching indices may be particularised to values like variables or terms of the form [(f (...))], where [f] is not a constructor of an inductive type like [O] or [S]. @@ -366,8 +433,8 @@ Qed. that is _parameterized_ by a value [x] of type [A] and _indexed_ by another value of type [A]. Its single constructor states that equality is reflexive, so the only way - to build an object of [eq x y] is if [x] is definitionally equal to the - variable [y]. + to build an object of [eq x y] (in the empty context) is if [x] is + definitionally equal to the term [y]. [[ Inductive eq (A : Type) (x : A) : A -> Prop := @@ -376,22 +443,23 @@ Qed. Pattern-matching on the equality then unifies the index [y] with the parameter [x], that is to a variable. - Consequently, we have determined the _value_ of the pattern [y], and it is - no longer a candidate for refinement with available constructors like + Consequently, we have determined the _value_ of the pattern [y] to be [x], + and it is no longer a candidate for refinement with available constructors like [0] or [S n]. Such a pattern is said to be "inaccessible", and needs to be indicated - by writing [?(t)] to tell Equations not to refine it. + by writing [?(t)] to tell Equations not to refine it but rather check its + inferrability. As an example, to prove the symmetry of equality we pattern match on an equality [H : x = y], which unify [y] the variable [x] that we indicate by writing [eq_sym x ?(x) eq_refl]. - The goal now being [x = x], it now holds by [eq_refl]. + The goal now being [x = x], it holds by [eq_refl]. *) Equations eq_sym {A} (x y : A) (H : x = y) : y = x := eq_sym x ?(x) eq_refl := eq_refl. -(** In practice, when the values determined are variable as in [eq_sym], +(** In practice, when the values determined are variables as in [eq_sym], the inaccessibility annotation is optional and we can simply write [x] or a wild card [_] rather than [?(x)]. *) @@ -413,9 +481,8 @@ Inductive Imf {A B} (f : A -> B) : B -> Type (** Pattern-matching on [im : Imf f t] particularise [t] to be of the form [f a] for some [a]. As [f] is not a constructor, [f a] is inaccessible and we need to write - as [?(f a)] in the pattern matching to prevent [Equations] to refine [f] - with available constructors. - In this case, it is essential as [f a] is not a variable. + as [?(f a)] in the pattern matching to prevent [Equations] to try to + interpret [f] as a constructor. As an example, we can write a function returning the [a] associated to an object in the image : *) @@ -426,7 +493,7 @@ inv f ?(f s) (imf f s) := s. (** Be careful that if you forget to mark inaccessible patterns, then [Equations] will try to match on the patterns, creating potentially pointless branches. It is fine in theory as the definition obtained will be logically equivalent - provided elaboration succededs, but annoying if you want to extract the code as the definition will be more involved. + provided elaboration succeeded, but annoying if you want to extract the code as the definition will be more involved. For instance, if we define [vmap''] by matching on [n] without marking the pattern associated to [n] as inaccessible, we can see at extraction that [Equations] @@ -440,3 +507,19 @@ vmap'' f (S n) (vcons a v) := vcons (f a) (vmap'' f n v). Extraction vmap. Extraction vmap''. + +(** Using inaccessible patterns hence allows to separate explicitely the subjects of + pattern-matchings and the inferred indices in definitions. The following alternative + definition of the square matrix diagonal pattern-matches only on the [vec] argument, + but uses well-founded recursion on the index [n] to justify termination, as + [vmap vtail v'] is not a subterm of [v']. *) + +Equations diag_wf {A n} (v : vec (vec A n) n) : vec A n by wf n := +diag_wf (n:=?(O)) vnil := vnil ; +diag_wf (n:=?(S _)) (vcons (vcons a v) v') := vcons a (diag_wf (vmap vtail v')). + +(* Again, one can observe the extractions of the two diagonal definitions to see + that [diag_wf] is more efficient, not needing to pattern-match on the indices first. *) + +Extraction diag. +Extraction diag_wf. From 3e6edf0bae78e4cb4be3aaa2e8e533c4afe326de Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 10 Feb 2025 09:50:14 +0100 Subject: [PATCH 09/12] Apply suggestions for @thomas-lamiaux 's review --- src/Tutorial_Equations_indexed.v | 55 +++++++++++++++++++++----------- 1 file changed, 36 insertions(+), 19 deletions(-) diff --git a/src/Tutorial_Equations_indexed.v b/src/Tutorial_Equations_indexed.v index 9c5275b8..c4bb9178 100644 --- a/src/Tutorial_Equations_indexed.v +++ b/src/Tutorial_Equations_indexed.v @@ -1,5 +1,8 @@ (** * Tutorial Equations : Dealing with indexed inductive types + *** Main contributors + - Thomas Lamiaux + - Matthieu Sozeau *** Summary: [Equations] is a plugin for Coq that offers a powerful support @@ -46,10 +49,10 @@ From Equations Require Import Equations. (** ** 1. Basic Reasoning on Indexed Inductive Types Indexed inductive types are particular kind of inductive definitions - that consist in defining not one single inductive type but a family - of linked inductive types. - On of the most well-known examples of indexed inductive types are vectors. - Given a fixed parameter [A : Type], vectors define a familly of inductive + Given a fixed parameter [A : Type], vectors define a family of linked + inductive types. + One of the most well-known examples of indexed inductive types are vectors. + Given a fixed parameter [A : Type], vectors define a family of inductive types [vec A n : Type] indexed by natural numbers [n : nat] representing the lengths of the vectors. The Vector type has two constructors. @@ -68,11 +71,12 @@ Arguments vnil {_}. Arguments vcons {_} _ _ _. (** The difference between a parameter and an index is that a parameter is - constant over all the constructors, whereas an index changes in the - constructor. + constant accros all the return types of the constructors, whereas an index + changes in at least one of the return types. For instance, in the definition of vectors the type [A] is a parameter - as it is constant in all the constructors, but [n:nat] is an index as - [vcons] relates two different types of the family, [vec A n] and [vec A (S n)]. + as it is constant across all the return types: [vec A 0] and [vec A (S n)]. + However, [n:nat] is an index as it is not constant in the returns types: + in the return type of [vnil] it is fixed to [0], and in the return type of [vcons] it is [S n]. Indices always appear after the [:] in an inductive type declaration. Reasoning about indexed inductive types like vectors is a bit more @@ -211,8 +215,9 @@ Abort. Definition vmap_vapp_simp {A B n m }(f : A -> B) (v : vec A n) (v' : vec A m) : vmap' f (vapp' v v') = vapp' (vmap' f v) (vmap' f v'). -Proof. - funelim (vmap' f v); simp vmap' vapp'; [reflexivity|congruence]. + funelim (vmap' f v); simp vmap' vapp'. + - reflexivity. + - congruence. Qed. (** ** 2. Advanced Dependent Pattern Matching @@ -291,9 +296,8 @@ Qed. of constructors: they assert which equations are impossible because the head constructors do not match, or if they do match, simplify to equations between the constructor arguments. - The cases above rely on the no-confusion property for [nat], that given - [n], [m] eturns [True] if [n] and [m] are both [0], [n = m] if they are both + [n], [m] returns [True] if [n] and [m] are both [0], [n = m] if they are both of the form [S n], [S m], and [False] otherwise. [Equations] provides a [Derive] command to generate this notion automatically @@ -313,10 +317,12 @@ Print NoConfusion_nat. In the general case, for indexed inductive types, there are two kind of no-confusion properties that can be derived by [Equations]: - The [NoConfusion] property that enables to distinguish object with different indices. - It takes as argument objects in the total space {n : nat & vec A n} and it is used + It takes as argument objects in the total space [{n : nat & vec A n}] which is generated + once and for all with `Derive Signature for vec`. It enables to solve general equations between objects in potentially different instances of the inductive family: *) +Derive Signature for vec. Derive NoConfusion for vec. Check NoConfusion_vec. @@ -329,12 +335,23 @@ Check NoConfusion_vec. Derive NoConfusionHom for vec. Print NoConfusionHom_vec. -(** Though, the [NoConfusionHom] property is derivable for many indexed inductive types, +(** Note that you can also derive all of them at once using [Derive Signature NoConfusion NoConfusionHom for vec]. *) + +(** While the [NoConfusionHom] property is derivable for many indexed inductive types, it is not the case that is derivable for all indexed inductive types. It is derivable only when equality of constructors can be reduced to equality - of the non-forced constructor arguments. For example on vectors, this - corresponds to the fact that - [vcons a n v = vcons a' n v' :> vec A (S n) <-> a = a' /\ v = v' :> vec A n]. + of the non-forced constructor arguments. A forced argument of a constructor + is a constructor argument (say of variable name [x]) that appears in a pattern + position in an index of the constructor's type conclusion. Patterns are generated + from variables and constructor applications in this case. + + For example on vectors, this corresponds to the fact that for [vcons a n v : vec A (S n)], + [n] appears in a pattern position in [S n]. Intuitively, the value of the *forced* + constructor argument [n] can be inverted from the type [vec A (S n)]. + [NoConfusionHom] for [vcons] proves that + [vcons a n v = vcons a' n v' :> vec A (S n) <-> a = a' /\ v = v' :> vec A n], + i.e. we can eliminate the trivial [n = n] equality on the forced argument [n]. + This ultimately relies on the [UIP] property for [nat] which shows that [forall e : n = n, e = eq_refl n]. If it is not possible to derive it, then [Equations] may need the indices to satisfy Uniqueness of Identity Proofs, asserting that all equality proofs are @@ -389,8 +406,8 @@ Section Tactics. noconf H. reflexivity. Qed. - (* The [dependent elimination] tactic is robust: it will fail if the - pattern-matching if non-exhaustive or contains unused clauses *) + (* The [dependent elimination _ as _] tactic is robust: it will fail if the + given patterns are non-exhaustive or contains unused clauses *) Goal forall a b (x : vec nat 2), (vcons a x = vcons b x) -> a = b. Proof. intros a b x H. From 212a0734a86481aac265719071f432a7442d7842 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 18 Feb 2025 14:01:32 +0100 Subject: [PATCH 10/12] Simpler introduction to [dependent elimination .. as .] --- src/Tutorial_Equations_indexed.v | 30 +++++++++++------------------- 1 file changed, 11 insertions(+), 19 deletions(-) diff --git a/src/Tutorial_Equations_indexed.v b/src/Tutorial_Equations_indexed.v index c4bb9178..d03de9af 100644 --- a/src/Tutorial_Equations_indexed.v +++ b/src/Tutorial_Equations_indexed.v @@ -392,8 +392,18 @@ Section Tactics. (** To explicit pattern-matching and control the naming of variables/hypotheses introduced by an elimination, it is possible to use the [dependent elimination] tactic, which provides access to the [Equations] - pattern-matching notation inside proofs: *) + pattern-matching notation inside proofs. + Note that the syntax of the patterns for [dependent elimination] follows the + syntax of Equation definitions clauses, rather than the Ltac tactics [as] clauses. *) + + Goal forall n m, n + m = m + n. + Proof. + induction n as [|n' IH]; intros m. + dependent elimination m as [O|S m']. + Abort. + (** As for Equations definitions, the patterns should cover solely the possible + values of the hypothesis. *) Goal forall a b (x : vec nat 2), (vcons a x = vcons b x) -> a = b. Proof. intros a b x H. @@ -419,24 +429,6 @@ Section Tactics. Fail dependent elimination x as [vcons hd (vcons tl vnil)|vcons hd vnil]. Abort. -(** A more low-level and fragile tactic [depelim] is also available, which can - generate fresh names for the new variables and does not require patterns. *) - - Context (A : Type). - Context (a b : A). - - Goal forall (x y : vec A 2), (vcons a (vcons a x) = vcons a (vcons b y)) -> a = b /\ x = y. - intros x y H. depelim H. now split. - Qed. - - Goal forall ( x : vec A 2) z, (vcons a x = z) -> vtail z = x. - intros x z H. depelim H. simp vtail. reflexivity. - Qed. - - Goal forall (x : vec nat 2), (vcons 0 x = vcons 1 x) -> False. - intros x H. depelim H. - Qed. - End Tactics. (** ** 3. Unifying Indices and Inaccessible Patterns From 85599a2817b05e00b8e8b81a09c222103c2eddd3 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 18 Feb 2025 14:04:23 +0100 Subject: [PATCH 11/12] Update gitignore --- .gitignore | 1 - 1 file changed, 1 deletion(-) diff --git a/.gitignore b/.gitignore index 91c6a378..8349bcef 100644 --- a/.gitignore +++ b/.gitignore @@ -18,7 +18,6 @@ *.vrb *.bcf *.run.xml -*.html *.css *~ node_modules/ From 873dacf276baf91f5da729a23598ed6ac8e26b9e Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 18 Feb 2025 14:06:01 +0100 Subject: [PATCH 12/12] Add to index.html --- src/index.html | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/index.html b/src/index.html index 494c9548..bb5722c9 100644 --- a/src/index.html +++ b/src/index.html @@ -174,6 +174,12 @@

Equations Tutorials

and source code +
  • + Indexed inductive types and tactics: + interactive version + and + source code +