From 770b2cc7f577ca039042d5e574f0bf8151c52a05 Mon Sep 17 00:00:00 2001 From: thomas-lamiaux Date: Tue, 14 May 2024 02:48:57 +0200 Subject: [PATCH 01/34] draft tuto Equations wf --- src/Tutorial_Equations_wf.v | 726 ++++++++++++++++++++++++++++++++++++ 1 file changed, 726 insertions(+) create mode 100644 src/Tutorial_Equations_wf.v diff --git a/src/Tutorial_Equations_wf.v b/src/Tutorial_Equations_wf.v new file mode 100644 index 0000000..e53f283 --- /dev/null +++ b/src/Tutorial_Equations_wf.v @@ -0,0 +1,726 @@ +(* 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: + - When matching on terms, it can happen that we loose information relevant + to termination. + In Section 2.1, 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.2, 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 The inspect method + - 2.2 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. + + + *** The syntactic guard condition is limited + + As a first example, 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) : option 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)) l]. + We can prove that [filter] do not increase the size of a list, and hence + that the recursive call is indeed performed on a smaller instance, and + that nubBy is terminating. + But, 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 (a :: l) => a :: nubBy eq (filter (fun b => negb (eq a b)) l). + +(** Furthermore, opposite to functions like [ack] or [nubBy], some recursive + functions are simply not naturally defined by structural recursion. + A prime example is the Euclidean algorithm computing the gcd of + [x] and [y] assuming that [x > y]. + It performs recursion on [x mod y] which is not a function of + any recursively smaller arguments, as [gcd] do not match any inputs. + It is well-founded and terminating for [lt], as we have tested + that [y > 0] and that in this case we can prove that [x mod y < y]. + Consequently, there is no hope for a syntactic guard to accept [gcd] as + its definition fully relies on theoretic reason to ensure termination. +*) + +Fail Equations gcd (x y : nat) : nat := +gcd x y with Nat.eq_dec y 0 => { + | left _ => x + | right _ => gcd y (x mod y) +}. + +(** *** Well-founded recursion + + It would be limitating if all this kind of functions could not be defined. + Fortunately, they can be using well-founded recursion. + + Given a well-founded relation [R : A -> A -> Type], defining a function + [f] by well-founded on [a : A] basically consists in defining [f] assuming that + [f] is defined for all [a'] smaller than [a], that is such that [R a a']. + When particularise to natural numbers and [<], this concept is sometimes + known as "strong recursion / induction": when defining [f n] one asummes + that [f] is defined for all smaller natural numbers [n' < n]. + + There are several methods to define functions by well-founded recursion using Coq. + They all have there pros and cons, but as a general rules defining functions + and reasonning using well-founded recursion can be tedious. + + For instance, the [Fix] construction of the standard library, that is a + type theoretic translation of the concept of well-founded recursion: + + [[ + Fix : ∀ [A : Type] [R : A -> A -> Prop], well_founded R -> + ∀ P : A -> Type, (∀ x : A, (∀ y : A, R y x -> P y) -> P x) -> + ∀ x : A, P x + ]] + + Defining a function [gcd] directly with [Fix] as below has several disadvantages. + The function is much less transparent than a usual definition by [Fixpoint] + as: + - there is an explicit fixpoint combinator [Fix] in the definition + - it forced us curryfication and the order of the arguments has changed + - there is no explicit proof appearing in the definition of the function + as we must proof that recusive call are indeed smaller, here through + the lemma [gcd_oblig] + + It also makes it harder to reason about as the recursion scheme is no + longer trivial. + Moreover, as we had to use curryfication in our definition, we may need + the axiom of function extentionality to reason about [gcd_Fix]. + +*) + +Lemma gcd_oblig: forall (a b: nat) (NE: b <> 0), lt (a mod b) b. +Proof. +Admitted. + +Definition gcd_Fix (x y : nat) : nat := + Fix lt_wf (fun _ => nat -> nat) + (fun (b: nat) (gcd_Fix: forall b', b' < b -> nat -> nat) (a: nat) => + match Nat.eq_dec b 0 with + | left EQ => a + | right NE => gcd_Fix (a mod b) (gcd_oblig a b NE) b + end) + y x. + +(** Consequently, Equations provide a built-in mechanism to help us + write functions by well-founded recursion. +*) + + +(** ** 1.2 Basic definitions and reasoning + + To define a function by well-founded recursion with Equations, one must + add the command [by wf x R] where [x] is the term decreasing, + and [R] 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. + +(** 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. + + 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]. + + If we try to define the function [nubBy] like that, it seems that all is + well and that the definition is accepted. +*) + +Equations nubBy {A} (eq : A -> A -> bool) (l : list A) : list A by wf (length l) lt := +nubBy eq [] => []; +nubBy eq (a :: l) => a :: nubBy eq (filter (fun b => negb (eq a b)) l). + +(** Yet, if we try to use the function [nubBy], e.g. to prove a property + about it, we get the error message "The reference nubBy was not found + in the current environment." +*) + +Fail Lemma In_nubBy {A} (eq : A -> A -> bool) (l : list A) (a : A) + : In a (nubBy eq l) -> In a l. + +(** The reason is that Coq can not prove on its own that the recursive + call is performed on a smaller instance. + 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. + Consequently, there is an obligation left to solve, and [nubBy] is not + definied as long as we have not solve it. + + You can check if there is any obligations left to prove and display them + using the command [Obligations]. +*) + +Obligations. + +(** To prove the remaining obligations, you can use the command [Next Obligations]. + It will get the first obligation left to solve, and creates a corresponding + goal to solve. + + For instance, in the case of [nubBy], it display the only obligation + left to solve [length (filter ... l) < length (a::l)]. + You can then solve it using the usual proof mode and tactics: +*) + +Next Obligation. +Proof. + eapply Nat.le_lt_trans. + - apply filter_length_le. + - auto with arith. +Qed. + +(** As we can see, it was indeed the only obligation as [Next Obligation] fails. + Moreover, we can see that [nubBy] is now defined as [In_nubBy] is well-typed. +*) + +Fail Next Obligation. + +Lemma In_nubBy {A} (eq : A -> A -> bool) (l : list A) (a : A) + : In a (nubBy eq l) -> In a l. +Abort. + +(** Unshelving and proving the obligations one by one using [Next Obligation] + can be tedious. + Consequently, the package [Equations] enables to automatically unshelve + all obligations and enter proof mode by starting the definition by + [Equations?] rather than by [Equations]. + See for instance, [nubBy] below. +*) + +Equations? nubBy' {A} (eq : A -> A -> bool) (l : list A) : list A by wf (length l) lt := +nubBy' eq [] => []; +nubBy' eq (a :: l) => a :: nubBy' eq (filter (fun b => negb (eq a b)) l). +Proof. + eapply Nat.le_lt_trans. + - apply filter_length_le. + - auto with arith. +Defined. + +(** This is a powerful feature as compared to the [Fix] definition of section 1.1, + we do not have to prove before the definition as lemma that each recursive + call are performed on deacreasing arguments. + More, the lemmas are not part of the definition of the function, making + the code easier to read. + Instead, we can just write our definition directly as we would like to, + before taking care of the non trivial goals. + + Though, note that [Equations?] triggers a warning when used on a definition + that leaves no obligations unsolved. + It is because for technical reasons, [Equations?] can not check if they + are at least obligation left to solve before openning the proof mode. + Hence, when there is no obligation proof mode is open for nothing, and + as to be closed by hand using [Qed] or [Defined] as it can be seen bellow. + As it is easy to forget, a warning is raised. + + In practice, if you wish to automatically test if obligations are + left to solve and unshelved them if so, you can start all your definitions + with [Equations?] and remove the [?] if the warning is set. +*) + +Equations? foo (n : nat) : nat := +foo _ => 0. +Qed. + + +(** 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 a a); destruct Heq as [_ Heqx]. + specialize (Heqx eq_refl); rewrite Heqx in Hneqx. + inversion Hneqx. + -- assumption. +Qed. + + +(** As exercices you can try to define the [gcd] function. + You should need the lemma Nat.mod_upper_bound. + *) +Equations? gcd (x y : nat) : nat by wf y lt := +gcd x y with Nat.eq_dec y 0 => { + | left _ => x + | right _ => gcd y (x mod y) +}. Proof. now apply Nat.mod_upper_bound. Qed. + +(* Propperties gcd ? *) + +Lemma mul_gcd (k x y : nat) : x > y -> gcd (k * x) (k * y) = k * (gcd x y). +Proof. + intro H. funelim (gcd x y); simp gcd. + - rewrite e. rewrite Nat.mul_0_r. cbn. reflexivity. +Admitted. + +(** ** 2. Different methods to work with well-founded recursion + + ** 2.1 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.2 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 df654981be077c469454b95c496d92a9f6d86bc5 Mon Sep 17 00:00:00 2001 From: thomas-lamiaux Date: Tue, 14 May 2024 21:52:00 +0200 Subject: [PATCH 02/34] some work --- src/Tutorial_Equations_wf.v | 181 +++++++++++++++++++----------------- 1 file changed, 98 insertions(+), 83 deletions(-) diff --git a/src/Tutorial_Equations_wf.v b/src/Tutorial_Equations_wf.v index e53f283..ced532b 100644 --- a/src/Tutorial_Equations_wf.v +++ b/src/Tutorial_Equations_wf.v @@ -48,7 +48,7 @@ Arguments to_fill {_}. 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 + in the tutorial Equations: Basics Not needed: - This tutorial discuss well-founded recursion but no prior knowledge @@ -101,11 +101,11 @@ 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 : + This function is clearly terminating using the lexicographic order: [(n,m) { Fortunately, they can be using well-founded recursion. Given a well-founded relation [R : A -> A -> Type], defining a function - [f] by well-founded on [a : A] basically consists in defining [f] assuming that + [f] by well-founded recursion on [a : A] basically consists in defining [f] assuming that [f] is defined for all [a'] smaller than [a], that is such that [R a a']. When particularise to natural numbers and [<], this concept is sometimes known as "strong recursion / induction": when defining [f n] one asummes that [f] is defined for all smaller natural numbers [n' < n]. There are several methods to define functions by well-founded recursion using Coq. - They all have there pros and cons, but as a general rules defining functions + They all have their pros and cons, but as a general rules defining functions and reasonning using well-founded recursion can be tedious. - For instance, the [Fix] construction of the standard library, that is a - type theoretic translation of the concept of well-founded recursion: + For instance, consider the [Fix] construction of the standard library, + which is a direct type theoretic definition of the concept of well-founded recursion: [[ Fix : ∀ [A : Type] [R : A -> A -> Prop], well_founded R -> @@ -186,20 +186,7 @@ gcd x y with Nat.eq_dec y 0 => { ∀ x : A, P x ]] - Defining a function [gcd] directly with [Fix] as below has several disadvantages. - The function is much less transparent than a usual definition by [Fixpoint] - as: - - there is an explicit fixpoint combinator [Fix] in the definition - - it forced us curryfication and the order of the arguments has changed - - there is no explicit proof appearing in the definition of the function - as we must proof that recusive call are indeed smaller, here through - the lemma [gcd_oblig] - - It also makes it harder to reason about as the recursion scheme is no - longer trivial. - Moreover, as we had to use curryfication in our definition, we may need - the axiom of function extentionality to reason about [gcd_Fix]. - + We can use it to define [gcd] as: *) Lemma gcd_oblig: forall (a b: nat) (NE: b <> 0), lt (a mod b) b. @@ -215,33 +202,61 @@ Definition gcd_Fix (x y : nat) : nat := end) y x. -(** Consequently, Equations provide a built-in mechanism to help us - write functions by well-founded recursion. + +(** However, doing so has several disadvantages. + The function is much less transparent than a usual definition by [Fixpoint] + as: + - there is an explicit fixpoint combinator [Fix] in the definition + - it forced us to use curryfication and the order of the arguments has changed + - there is are explicit proof appearing in the definition of the function, + here through [gcd_oblig], as we must provide a proof that recusive call + are indeed smaller. + It can also make it harder to reason about as the recursion scheme is no + longer trivial. + Moreover, as we had to use curryfication in our definition, we may need + the axiom of function extentionality to reason about [gcd_Fix]. + + Consequently, Equations provide a built-in mechanism to help us + write functions and reason by well-founded recursion. *) (** ** 1.2 Basic definitions and reasoning - To define a function by well-founded recursion with Equations, one must - add the command [by wf x R] where [x] is the term decreasing, - and [R] 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. + To define a function by well-founded recursion with Equations, one must add + after the type of the function, the command [by wf x R] where [x] is the term + decreasing, and [R] the well-founded relation for which [x] decreases. + + For instance, 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. + We hence, need to write: + + [[ + Equations last {A} (l : list A) : option A by wf (length l) lt := + ]] + + Equations will then automatically: + - 1. Check for a proof that [R] is a well-founded in a type classes + specific to [Equations] logically named [WellFounded] + - 2. Try to prove that the recursive call are made on decreasing arguments, + and if it can not do it on its own, it will generate a proof obligation + i.e. intuitively a goal for the user to fill. + + This enables to separate the proofs that the recursive call are smaller + from the definition of the function, making it easier to read 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. + left for the user to solve, and we refer to section 1.3 for more involved + examples with non trivial obligations. + + Let's first consider the definition of [last] that we can define by + well-founded recursion by adding [by wf (length l) lt]. + [Equations] will then creates one obligation per recursive call and + try to solve them. + In the case of [last], it creates the obligation [length (a'::l) < length (a::a'::l)] + which as we can check can be solved automatically. *) Equations last {A} (l : list A) : option A by wf (length l) lt := @@ -249,8 +264,11 @@ 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 +(** Defining [last] by well-founded recursion is hence effortless and the + the definition is as legible as we would hope. + + Moreover, 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 @@ -290,13 +308,13 @@ Proof. - 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)) A -> bool) (l : list A) (a : A) call is performed on a smaller instance. 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. + Property that is not trivial, and that Coq can not prove on its own, + nor look for on its own without any indications. Consequently, there is an obligation left to solve, and [nubBy] is not definied as long as we have not solve it. @@ -445,13 +465,9 @@ Proof. - auto with arith. Defined. -(** This is a powerful feature as compared to the [Fix] definition of section 1.1, - we do not have to prove before the definition as lemma that each recursive - call are performed on deacreasing arguments. - More, the lemmas are not part of the definition of the function, making - the code easier to read. - Instead, we can just write our definition directly as we would like to, - before taking care of the non trivial goals. +(** This is a powerful feature as compared to the [Fix] definition of section 1.1: + the code is perfectly legible, in particular the body of the function and + the proof are clearly separated. Though, note that [Equations?] triggers a warning when used on a definition that leaves no obligations unsolved. @@ -460,18 +476,17 @@ Defined. Hence, when there is no obligation proof mode is open for nothing, and as to be closed by hand using [Qed] or [Defined] as it can be seen bellow. As it is easy to forget, a warning is raised. - - In practice, if you wish to automatically test if obligations are - left to solve and unshelved them if so, you can start all your definitions - with [Equations?] and remove the [?] if the warning is set. *) Equations? foo (n : nat) : nat := foo _ => 0. Qed. +(** In practice, if you wish to automatically test if obligations are + left to solve and unshelved them if so, you can just start all your definitions + with [Equations?] and remove the [?] if the warning is triggered. -(** Reasoning on functions defined by well-founded recursion with + 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. @@ -515,7 +530,7 @@ gcd x y with Nat.eq_dec y 0 => { | right _ => gcd y (x mod y) }. Proof. now apply Nat.mod_upper_bound. Qed. -(* Propperties gcd ? *) +(* Properties gcd ? *) Lemma mul_gcd (k x y : nat) : x > y -> gcd (k * x) (k * y) = k * (gcd x y). Proof. @@ -528,7 +543,7 @@ Admitted. ** 2.1 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 + relevant to 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 @@ -609,25 +624,25 @@ End Inspect. 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 + Yet, without surprise, 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 + This is normal, as 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, + In this section, we explain how to do so to for a [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. - + We can define a [gcd] function that does not require the assumption that + [x > y] as below, by first checking if [x] or [y] is [0], and otherwise + compare [x] and [y], and recall [gcd] with [x - y] or [y - x] depending + which is the greater. 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]. + well-founded order on [nat], accounted for by [wf (x + y) lt]. *) Equations? gcd (x y : nat) : nat by wf (x + y) lt := @@ -651,7 +666,7 @@ Abort. Show Obligation Tactic. (** The obligations generated are not complicated to prove but tedious, - and they can actually be solved automatically via the arithmetic + 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. @@ -691,7 +706,7 @@ gcd x y with gt_eq_gt_dec x 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] + few properties of [gcd]. *) Lemma gcd_same x : gcd x x = x. From 2a530ec881e8cf76d2d7bea0a7dfd7117d0be33d Mon Sep 17 00:00:00 2001 From: thomas-lamiaux Date: Thu, 16 May 2024 00:22:42 +0200 Subject: [PATCH 03/34] implement new contribution guidelines --- src/Tutorial_Equations_basics.v | 10 +++++----- src/Tutorial_Equations_wf.v | 12 ++++++------ 2 files changed, 11 insertions(+), 11 deletions(-) diff --git a/src/Tutorial_Equations_basics.v b/src/Tutorial_Equations_basics.v index af4ae8d..e4e6a4b 100644 --- a/src/Tutorial_Equations_basics.v +++ b/src/Tutorial_Equations_basics.v @@ -47,14 +47,14 @@ Arguments to_fill {_}. -(** * 1. Basic definitions and reasoning +(** ** 1. Basic definitions and reasoning Let's start by importing the package: *) From Equations Require Import Equations. -(** ** 1.1 Defining functions by dependent pattern matching +(** *** 1.1 Defining functions by dependent pattern matching In its simplest form, [Equations] provides a practical interface to define functions on inductive types by pattern matching and recursion @@ -211,7 +211,7 @@ Succeed Example testing : fold_right Nat.mul 1 (1::2::3::4::[]) = 24 := eq_refl. *) -(** ** 1.2 Reasoning with Equations *) +(** *** 1.2 Reasoning with Equations *) (** Now that we have seen how to define basic functions, we need to understand how to reason about them. @@ -468,7 +468,7 @@ Admitted. -(** * 2. With clauses +(** ** 2. With clauses The structure of real programs is generally richer than a simple case tree on the original arguments. @@ -611,7 +611,7 @@ Succeed Example testing : -(** * 3. Where Clauses +(** ** 3. Where Clauses As discussed, it often happens that we need to compute intermediate terms which is the purpose of the [with] clause. diff --git a/src/Tutorial_Equations_wf.v b/src/Tutorial_Equations_wf.v index ced532b..7ded516 100644 --- a/src/Tutorial_Equations_wf.v +++ b/src/Tutorial_Equations_wf.v @@ -70,9 +70,9 @@ Import ListNotations. -(** * 1. Defining and reasoning using well-founded recursion +(** ** 1. Defining and reasoning using well-founded recursion - ** 1.1 Introduction to 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 @@ -221,7 +221,7 @@ Definition gcd_Fix (x y : nat) : nat := *) -(** ** 1.2 Basic definitions and reasoning +(** *** 1.2 Basic definitions and reasoning To define a function by well-founded recursion with Equations, one must add after the type of the function, the command [by wf x R] where [x] is the term @@ -377,7 +377,7 @@ Proof. Admitted. -(** ** 1.3 Well-founded recursion and Obligations +(** *** 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 @@ -540,7 +540,7 @@ Admitted. (** ** 2. Different methods to work with well-founded recursion - ** 2.1 The inspect method + *** 2.1 The inspect method When defining a functions, it can happen that we loose information relevant to termination when matching a value, and that we then get @@ -619,7 +619,7 @@ Section Inspect. End Inspect. -(** ** 2.2 Personalising the tactic proving obligations +(** *** 2.2 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 From 597b43c0ca202534ac924934cf3448cae3e66976 Mon Sep 17 00:00:00 2001 From: thomas-lamiaux Date: Fri, 17 May 2024 20:43:22 +0200 Subject: [PATCH 04/34] edit Contribting >> talk about issues --- CONTRIBUTING.md | 33 ++++++++++++++++++++++++++++----- 1 file changed, 28 insertions(+), 5 deletions(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 73c5802..4d71bff 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -104,8 +104,33 @@ Doing so only takes a bit more time when writing a tutorial but saves a lot of t that will not have to chase information in different other tutorials, tutorials which could in turn refer to other tutorials. It also eases maintenance as one does not need to worry about potential modifications to other tutorials. +### Discuss Recurring Issues + +When writing a tutorial, it often happens to be confronted to something that +does not work as easily as expected due to limitations of a feature or genuine bugs. +In this case, often people decide not to mention the problem as they plan / +it is planned to fix the problem. +The issue is that most times, it turns out that it is actually not that easy to fix +nor that fast, and meanwhile users are left with a solution. +Worse, not only they are not told how to go around the problem, +but they are not even warned that a problem may rise up. +This can be particularly limiting for non expert users, that may not be able +to identify the problem and manage to go around it on their own. + +This issue is particularly relevant in our case, as the documentation is aimed +at the general public and is indexed on the Coq platform versions, +that do not change everyday. + +> [!IMPORTANT] +> Consequently, it is really important to mention in tutorials issues that +> often come up with a feature, and to provide as reasonable solution as possible. + +The tutorials can later be modified once the fix are effective. + + ### Adding Exercises -As tutorials are meant for studying, do not hesitate to add some exercises for the users to try, e.g. functions or properties to prove or finish. +As tutorials are meant for studying, do not hesitate to add some exercises +for the users to try, e.g. functions or properties to prove or finish. In general, we recommend to provide at least definitions prefilled with typing information like: ``` @@ -115,13 +140,11 @@ Lemma map_app {A B} (f : A -> B) (l l' : list A) : map f (l ++ l') = map f l + m Proof. Admitted. ``` -To do so, you can add the following code at the beginning of the tutorial. -It creates an axiom `to_fill` and hides it so that it is does not appear in the body of the tutorial. +To do so, you can add the following code at the beginning of the tutorial, +that creates an axiom that can fill any goal. ``` -(* begin hide *) Axiom to_fill : forall A, A. Arguments to_fill {_}. -(* end hide *) ``` You can also provides tests for the users to be able to check if their definition works. From 39fad41dcd5799775c9b517304969be4401d0c1b Mon Sep 17 00:00:00 2001 From: thomas-lamiaux Date: Fri, 17 May 2024 21:03:05 +0200 Subject: [PATCH 05/34] edits contrib + readme --- CONTRIBUTING.md | 12 ++++++------ README.md | 10 ++++++++-- 2 files changed, 14 insertions(+), 8 deletions(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 4d71bff..7b961cb 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -13,6 +13,10 @@ There are different possible ways to contribute depending on your time and techn - There is technical work to be done on the (interactive) web interface side +> [!WARNING] +> Before starting to work on something and invest time into it, check if it is not already existing, +> or if someone hasn't already started working on it, either by creating a discussion on the [Zulip stream](https://coq.zulipchat.com/#narrow/stream/437203-Platform-docs) or a draft pull request about it. + ### Writing Tutorials and How-tos If you have an idea for a tutorial or how-to, you can create a discussion on the dedicated [Zulip stream](https://coq.zulipchat.com/#narrow/stream/437203-Platform-docs) to get feedback on your idea, through the writing and to reach others that may be interested. @@ -23,10 +27,6 @@ Equation, you can create a discussion in the associated stream. Once you have a plan and some content, you can create a draft pull request to make your code accessible and get feedback on it while you (and others) progress on it. -> [!WARNING] -> Before starting to work on a tutorial or a how-to and invest time into it, check if it is not already existing, -> or if someone hasn't already started working on it, either by creating a discussion on the [Zulip stream](https://coq.zulipchat.com/#narrow/stream/437203-Platform-docs) or a draft pull request about it. - > [!WARNING] > Lots of stuff have already be written about Coq, it can make sense to reuse some of the content. > If you wish to do so, be careful that you are indeed allowed by the copyright owners or the content licenses. @@ -124,8 +124,8 @@ that do not change everyday. > [!IMPORTANT] > Consequently, it is really important to mention in tutorials issues that > often come up with a feature, and to provide as reasonable solution as possible. - -The tutorials can later be modified once the fix are effective. +> The tutorials can always be modified once the fix are effective, but meanwhile +> users have solutions. ### Adding Exercises diff --git a/README.md b/README.md index 3f12a8f..3d010dc 100644 --- a/README.md +++ b/README.md @@ -76,11 +76,16 @@ of tutorials and how-tos it could be interesting to have. This list is not fixed and will necessarily evolve through discussions with the community and experience, but it should already give an idea of the potential of this project. -The project can already been discussed on the dedicated [Zulip stream](https://coq.zulipchat.com/#narrow/stream/437203-Platform-docs). +> [!IMPORTANT] +> The project can already been discussed on the dedicated [Zulip stream](https://coq.zulipchat.com/#narrow/stream/437203-Platform-docs). Among others, you can find there +> - Information about [new tutorials and how-tos](https://coq.zulipchat.com/#narrow/stream/437203-Coq-Platform-docs/topic/New.20Tutorials.20and.20How-to.20to.20check.20out) +> - A [wishlist](https://coq.zulipchat.com/#narrow/stream/437203-Coq-Platform-docs/topic/Wishlist.20Tutorials) to tell us what you need + We will also soon submit a Coq Enhancement Proposal. + ### How to contribute to the documentation There is a lot of work to be done before having a comprehensive documentation for Coq and its Platform, and we welcome contributions. @@ -91,7 +96,8 @@ There are different possible ways to contribute depending on your time and techn - There is a lot of tutorials and how-tos to write, both about Coq and plugins in its Platform - There is technical work to be done on the (interactive) web interface side -For more information on how to contribute, please check the [Contribution Guidelines](CONTRIBUTING.md). +> [!IMPORTANT] +> For more information on how to contribute, please check the [Contribution Guidelines](CONTRIBUTING.md). From 2fca3ef7c3a562b8a19f3fd27e64c15f38e361dc Mon Sep 17 00:00:00 2001 From: Thomas Lamiaux <85848641+thomas-lamiaux@users.noreply.github.com> Date: Fri, 17 May 2024 21:18:30 +0200 Subject: [PATCH 06/34] Update README.md --- README.md | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/README.md b/README.md index 3d010dc..4fd149d 100644 --- a/README.md +++ b/README.md @@ -76,13 +76,13 @@ of tutorials and how-tos it could be interesting to have. This list is not fixed and will necessarily evolve through discussions with the community and experience, but it should already give an idea of the potential of this project. -> [!IMPORTANT] -> The project can already been discussed on the dedicated [Zulip stream](https://coq.zulipchat.com/#narrow/stream/437203-Platform-docs). Among others, you can find there -> - Information about [new tutorials and how-tos](https://coq.zulipchat.com/#narrow/stream/437203-Coq-Platform-docs/topic/New.20Tutorials.20and.20How-to.20to.20check.20out) -> - A [wishlist](https://coq.zulipchat.com/#narrow/stream/437203-Coq-Platform-docs/topic/Wishlist.20Tutorials) to tell us what you need - We will also soon submit a Coq Enhancement Proposal. +> [!NOTE] +> For more information about project and to participate in disccusions, please checkout on the dedicated [Zulip stream](https://coq.zulipchat.com/#narrow/stream/437203-Platform-docs). +> Among others, you can find there information about [new tutorials and how-tos](https://coq.zulipchat.com/#narrow/stream/437203-Coq-Platform-docs/topic/New.20Tutorials.20and.20How-to.20to.20check.20out), and a [wishlist](https://coq.zulipchat.com/#narrow/stream/437203-Coq-Platform-docs/topic/Wishlist.20Tutorials) to tell us what you need + + From 13ef8abd94280d072d8d6af25c7d91ffa1166da5 Mon Sep 17 00:00:00 2001 From: Thomas Lamiaux <85848641+thomas-lamiaux@users.noreply.github.com> Date: Fri, 17 May 2024 21:28:04 +0200 Subject: [PATCH 07/34] Update CONTRIBUTING.md --- CONTRIBUTING.md | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 7b961cb..ab90c5c 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -13,7 +13,7 @@ There are different possible ways to contribute depending on your time and techn - There is technical work to be done on the (interactive) web interface side -> [!WARNING] +> [!TIP] > Before starting to work on something and invest time into it, check if it is not already existing, > or if someone hasn't already started working on it, either by creating a discussion on the [Zulip stream](https://coq.zulipchat.com/#narrow/stream/437203-Platform-docs) or a draft pull request about it. @@ -82,7 +82,7 @@ As examples, we have been working on new tutorials for the package Equations. The first one is complete and can be checked out [here](src/Tutorial_Equations_basics.v). -### Horizontality +### Writing Horizontal Tutorials Tutorials do not necessarily need to be long, nor should aim to present all the aspects of a feature in one unique tutorial. @@ -104,7 +104,7 @@ Doing so only takes a bit more time when writing a tutorial but saves a lot of t that will not have to chase information in different other tutorials, tutorials which could in turn refer to other tutorials. It also eases maintenance as one does not need to worry about potential modifications to other tutorials. -### Discuss Recurring Issues +### Discussing Recurring Issues When writing a tutorial, it often happens to be confronted to something that does not work as easily as expected due to limitations of a feature or genuine bugs. @@ -118,10 +118,10 @@ This can be particularly limiting for non expert users, that may not be able to identify the problem and manage to go around it on their own. This issue is particularly relevant in our case, as the documentation is aimed -at the general public and is indexed on the Coq platform versions, +at the general public, and is indexed on the versions of Coq platform that do not change everyday. -> [!IMPORTANT] +> [!NOTE] > Consequently, it is really important to mention in tutorials issues that > often come up with a feature, and to provide as reasonable solution as possible. > The tutorials can always be modified once the fix are effective, but meanwhile From 5ffb2f4d5c9a53073b895edfbbeee93fa5038af9 Mon Sep 17 00:00:00 2001 From: thomas-lamiaux Date: Sat, 18 May 2024 02:27:32 +0200 Subject: [PATCH 08/34] fix ack --- src/Tutorial_Equations_wf.v | 86 +++++++++++++++++++++++++++++-------- 1 file changed, 69 insertions(+), 17 deletions(-) diff --git a/src/Tutorial_Equations_wf.v b/src/Tutorial_Equations_wf.v index 7ded516..c7dc13c 100644 --- a/src/Tutorial_Equations_wf.v +++ b/src/Tutorial_Equations_wf.v @@ -313,7 +313,7 @@ Qed. as both [<] are. You can define the lexicographic order and automatically derive a proof it is well-founded using the function [Equations.Prop.Subterm.lexprod]. - As we can see, with this order, once again no obligations are generated as + As we can see, with this order, once again no obligations are left to prove as Coq can prove on its own that [(m, (ack (S m) n)) Date: Sat, 18 May 2024 02:50:22 +0200 Subject: [PATCH 09/34] fix file --- src/Tutorial_Equations_wf.v | 41 +++++++++++-------------------------- 1 file changed, 12 insertions(+), 29 deletions(-) diff --git a/src/Tutorial_Equations_wf.v b/src/Tutorial_Equations_wf.v index c7dc13c..649e160 100644 --- a/src/Tutorial_Equations_wf.v +++ b/src/Tutorial_Equations_wf.v @@ -163,19 +163,19 @@ gcd x y with Nat.eq_dec y 0 => { (** *** Well-founded recursion - It would be limitating if all this kind of functions could not be defined. + It would be limiting if all this kind of functions could not be defined. Fortunately, they can be using well-founded recursion. Given a well-founded relation [R : A -> A -> Type], defining a function [f] by well-founded recursion on [a : A] basically consists in defining [f] assuming that [f] is defined for all [a'] smaller than [a], that is such that [R a a']. When particularise to natural numbers and [<], this concept is sometimes - known as "strong recursion / induction": when defining [f n] one asummes + known as "strong recursion / induction": when defining [f n] one assumes that [f] is defined for all smaller natural numbers [n' < n]. There are several methods to define functions by well-founded recursion using Coq. They all have their pros and cons, but as a general rules defining functions - and reasonning using well-founded recursion can be tedious. + and reasoning using well-founded recursion can be tedious. For instance, consider the [Fix] construction of the standard library, which is a direct type theoretic definition of the concept of well-founded recursion: @@ -209,12 +209,12 @@ Definition gcd_Fix (x y : nat) : nat := - there is an explicit fixpoint combinator [Fix] in the definition - it forced us to use curryfication and the order of the arguments has changed - there is are explicit proof appearing in the definition of the function, - here through [gcd_oblig], as we must provide a proof that recusive call + here through [gcd_oblig], as we must provide a proof that recursive calls are indeed smaller. It can also make it harder to reason about as the recursion scheme is no longer trivial. Moreover, as we had to use curryfication in our definition, we may need - the axiom of function extentionality to reason about [gcd_Fix]. + the axiom of function extensionally to reason about [gcd_Fix]. Consequently, Equations provide a built-in mechanism to help us write functions and reason by well-founded recursion. @@ -335,7 +335,7 @@ Proof. Abort. (** The reason is that [funelim] does much more than just applying [ack_elim]. - In particualar, it does diverse generalisation and simplification that pose + In particular, it does diverse generalisation and simplification that pose problem here. This a known issue and it is currently being investigated and fixed. @@ -389,13 +389,13 @@ Qed. unify [n] with [n0] which then creates a loop. The simplest method to go around this issue is to given [n] by hand. - This way it can not be infered wrong, and rewrites work: + This way it can not be inferred wrong, and rewrites work: *) Definition ack_incr {m n} : ack m n < ack m (n+1). Proof. apply ack_elim; intros. - Fail progress simp ack. Fail rewrite ack_equation_1. - (* It failed because it infered [n] wrong *) + (* It failed because it inferred [n] wrong *) (* To prevent that, we give it by hand *) rewrite (ack_equation_1 (n0 + 1)). rewrite Nat.add_comm. auto with arith. @@ -404,7 +404,7 @@ Proof. Qed. -(** As exercices, you can try to: +(** As exercises, 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 @@ -466,7 +466,7 @@ Fail Lemma In_nubBy {A} (eq : A -> A -> bool) (l : list A) (a : A) Property that is not trivial, and that Coq can not prove on its own, nor look for on its own without any indications. Consequently, there is an obligation left to solve, and [nubBy] is not - definied as long as we have not solve it. + defined as long as we have not solve it. You can check if there is any obligations left to prove and display them using the command [Obligations]. @@ -524,7 +524,7 @@ Defined. Though, note that [Equations?] triggers a warning when used on a definition that leaves no obligations unsolved. It is because for technical reasons, [Equations?] can not check if they - are at least obligation left to solve before openning the proof mode. + are at least obligation left to solve before opening the proof mode. Hence, when there is no obligation proof mode is open for nothing, and as to be closed by hand using [Qed] or [Defined] as it can be seen bellow. As it is easy to forget, a warning is raised. @@ -573,23 +573,6 @@ Proof. Qed. -(** As exercices you can try to define the [gcd] function. - You should need the lemma Nat.mod_upper_bound. - *) -Equations? gcd (x y : nat) : nat by wf y lt := -gcd x y with Nat.eq_dec y 0 => { - | left _ => x - | right _ => gcd y (x mod y) -}. Proof. now apply Nat.mod_upper_bound. Qed. - -(* Properties gcd ? *) - -Lemma mul_gcd (k x y : nat) : x > y -> gcd (k * x) (k * y) = k * (gcd x y). -Proof. - intro H. funelim (gcd x y); simp gcd. - - rewrite e. rewrite Nat.mul_0_r. cbn. reflexivity. -Admitted. - (** ** 2. Different methods to work with well-founded recursion *** 2.1 The inspect method @@ -757,7 +740,7 @@ gcd x y with gt_eq_gt_dec x y := { (** For further examples of how functional elimination works on well-founded - recursion and is useful on complex definitions, we will now show a + recursion and how useful it is on complex definitions, we will now show a few properties of [gcd]. *) From dd94445341c7e38140c4e38ff05de7db323badea Mon Sep 17 00:00:00 2001 From: thomas-lamiaux Date: Sat, 18 May 2024 02:57:53 +0200 Subject: [PATCH 10/34] moved to_fill --- src/Tutorial_Equations_basics.v | 10 +++------- src/Tutorial_Equations_wf.v | 7 ++----- 2 files changed, 5 insertions(+), 12 deletions(-) diff --git a/src/Tutorial_Equations_basics.v b/src/Tutorial_Equations_basics.v index e4e6a4b..9aeb30c 100644 --- a/src/Tutorial_Equations_basics.v +++ b/src/Tutorial_Equations_basics.v @@ -1,10 +1,3 @@ -(* begin hide *) -Axiom to_fill : forall A, A. -Arguments to_fill {_}. -(* end hide *) - - - (** * Tutorial Equations : Basic Definitions and Reasoning with Equations *** Summary @@ -54,6 +47,9 @@ Arguments to_fill {_}. From Equations Require Import Equations. +Axiom to_fill : forall A, A. +Arguments to_fill {_}. + (** *** 1.1 Defining functions by dependent pattern matching In its simplest form, [Equations] provides a practical interface to diff --git a/src/Tutorial_Equations_wf.v b/src/Tutorial_Equations_wf.v index 649e160..454d5ff 100644 --- a/src/Tutorial_Equations_wf.v +++ b/src/Tutorial_Equations_wf.v @@ -1,8 +1,3 @@ -(* begin hide *) -Axiom to_fill : forall A, A. -Arguments to_fill {_}. -(* end hide *) - (** * Well-founded Recursion using Equations *** Summary @@ -68,6 +63,8 @@ From Equations Require Import Equations. From Coq Require Import List Arith Lia. Import ListNotations. +Axiom to_fill : forall A, A. +Arguments to_fill {_}. (** ** 1. Defining and reasoning using well-founded recursion From 11965de760093649252d704e00e0c4ed14989984 Mon Sep 17 00:00:00 2001 From: Thomas Lamiaux <85848641+thomas-lamiaux@users.noreply.github.com> Date: Tue, 28 May 2024 19:58:45 +0200 Subject: [PATCH 11/34] Fix typos from code review Co-authored-by: Meven Lennon-Bertrand <58942857+MevenBertrand@users.noreply.github.com> --- src/Tutorial_Equations_wf.v | 142 ++++++++++++++++++------------------ 1 file changed, 71 insertions(+), 71 deletions(-) diff --git a/src/Tutorial_Equations_wf.v b/src/Tutorial_Equations_wf.v index 454d5ff..89e98df 100644 --- a/src/Tutorial_Equations_wf.v +++ b/src/Tutorial_Equations_wf.v @@ -23,9 +23,9 @@ In Section 2.1, 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, + that we are left with easy theory-specific obligations to solve, for instance basic arithmetic on lists. - In section 2.2, we explain how to adapt locally the tactic trying to + In section 2.2, we explain how to locally adapt the tactic trying to solve obligations to deal with such goals. *** Table of content @@ -41,17 +41,17 @@ *** 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 + - We assume basic knowledge of Coq, and of defining functions by recursion + - We assume basic knowledge of the Equations plugin, 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 + - This tutorial discusses well-founded recursion but no prior knowledge + about it is required: we will explain the concept - 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 + Coq's obligation mechanism, but no previous knowledge about it is needed + - To simplify proofs involving arithmetics, we use the automation + tactics [lia] and [auto with arith], but they can be used as black boxes Installation: - Equations is available by default in the Coq Platform @@ -72,11 +72,11 @@ Arguments to_fill {_}. *** 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 + To ensure they are, Coq checks that they satisfy a 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 + trivial size argument and some mathematical reasoning, that Coq's syntactic guard fails to see as such on its own. @@ -89,7 +89,7 @@ Arguments to_fill {_}. [ 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. + and only remembers [l] as a smaller subterm. *) Fail Equations last {A} (l : list A) : option A := @@ -98,7 +98,7 @@ 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: + We can show that this function is terminating by using the lexicographic order: [(n,m) negb (eq x y)) l]. - We can prove that [filter] do not increase the size of a list, and hence + We can prove that [filter] does not increase the size of a list, and hence that the recursive call is indeed performed on a smaller instance, and that nubBy is terminating. - But, without surprise, it can not be checked automatically using Coq's + But, without surprise, it cannot be checked automatically using Coq's syntactic guard as it involves mathematical reasoning on [filter]. *) @@ -140,14 +140,14 @@ Fail Equations nubBy {A} (eq : A -> A -> bool) (l : list A) : list A := nubBy eq [] => []; nubBy eq (a :: l) => a :: nubBy eq (filter (fun b => negb (eq a b)) l). -(** Furthermore, opposite to functions like [ack] or [nubBy], some recursive +(** Furthermore, in contrast to to functions like [ack] or [nubBy], some recursive functions are simply not naturally defined by structural recursion. A prime example is the Euclidean algorithm computing the gcd of [x] and [y] assuming that [x > y]. It performs recursion on [x mod y] which is not a function of - any recursively smaller arguments, as [gcd] do not match any inputs. + any recursively smaller arguments, as [gcd] does not match any inputs. It is well-founded and terminating for [lt], as we have tested - that [y > 0] and that in this case we can prove that [x mod y < y]. + that [y > 0] and we can prove that [x mod y < y]. Consequently, there is no hope for a syntactic guard to accept [gcd] as its definition fully relies on theoretic reason to ensure termination. *) @@ -160,15 +160,15 @@ gcd x y with Nat.eq_dec y 0 => { (** *** Well-founded recursion - It would be limiting if all this kind of functions could not be defined. - Fortunately, they can be using well-founded recursion. + It would be limiting if functions of this kind could not be defined. + Fortunately, they can be, using well-founded recursion. Given a well-founded relation [R : A -> A -> Type], defining a function - [f] by well-founded recursion on [a : A] basically consists in defining [f] assuming that - [f] is defined for all [a'] smaller than [a], that is such that [R a a']. - When particularise to natural numbers and [<], this concept is sometimes + [f] by well-founded recursion on [a : A] consists in defining [f] assuming that + [f] is defined for all [a'] smaller than [a], that is such that [R a' a]. + When particularised to natural numbers and [<], this concept is sometimes known as "strong recursion / induction": when defining [f n] one assumes - that [f] is defined for all smaller natural numbers [n' < n]. + that [f] is defined/proven for all smaller natural numbers [n' < n]. There are several methods to define functions by well-founded recursion using Coq. They all have their pros and cons, but as a general rules defining functions @@ -205,10 +205,10 @@ Definition gcd_Fix (x y : nat) : nat := as: - there is an explicit fixpoint combinator [Fix] in the definition - it forced us to use curryfication and the order of the arguments has changed - - there is are explicit proof appearing in the definition of the function, - here through [gcd_oblig], as we must provide a proof that recursive calls + - explicit proofs appear in the definition of the function, + here through [gcd_oblig], as we must prove that recursive calls are indeed smaller. - It can also make it harder to reason about as the recursion scheme is no + It can also make it harder to reason about the function, as the recursion scheme is no longer trivial. Moreover, as we had to use curryfication in our definition, we may need the axiom of function extensionally to reason about [gcd_Fix]. @@ -220,7 +220,7 @@ Definition gcd_Fix (x y : nat) : nat := (** *** 1.2 Basic definitions and reasoning - To define a function by well-founded recursion with Equations, one must add + To define a function by well-founded recursion with Equations, one must add, after the type of the function, the command [by wf x R] where [x] is the term decreasing, and [R] the well-founded relation for which [x] decreases. @@ -234,13 +234,13 @@ Definition gcd_Fix (x y : nat) : nat := ]] Equations will then automatically: - - 1. Check for a proof that [R] is a well-founded in a type classes - specific to [Equations] logically named [WellFounded] - - 2. Try to prove that the recursive call are made on decreasing arguments, - and if it can not do it on its own, it will generate a proof obligation - i.e. intuitively a goal for the user to fill. + - 1. Search for a proof that [R] is well-founded, using type classes from a database + specific to [Equations] suitably named [WellFounded] + - 2. Try to prove that the recursive calls are done on decreasing arguments, + and if it cannot do it on its own, it will generate a proof obligation + i.e. a goal for the user to fill. - This enables to separate the proofs that the recursive call are smaller + This allows to separate the proofs that the recursive call are smaller from the definition of the function, making it easier to read while dealing automatically with trivial cases. @@ -248,12 +248,12 @@ Definition gcd_Fix (x y : nat) : nat := left for the user to solve, and we refer to section 1.3 for more involved examples with non trivial obligations. - Let's first consider the definition of [last] that we can define by - well-founded recursion by adding [by wf (length l) lt]. + Let us first consider the definition of [last] that we can define by + well-founded recursion, adding the following indication: [by wf (length l) lt]. [Equations] will then creates one obligation per recursive call and try to solve them. In the case of [last], it creates the obligation [length (a'::l) < length (a::a'::l)] - which as we can check can be solved automatically. + which as we can check is solved automatically. *) Equations last {A} (l : list A) : option A by wf (length l) lt := @@ -262,23 +262,23 @@ last (a::nil) := Some a; last (a::(a'::l)) := last (a'::l). (** Defining [last] by well-founded recursion is hence effortless and the - the definition is as legible as we would hope. + definition is as legible as we would hope. - Moreover, thanks to functional elimination through [funelim], we can reason - about function defined by well-founded recursion without having to repeat + Moreover, thanks to functional induction through [funelim], we can reason + about functions 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 + For instance, let us 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. + As we can see, the condition [l <> nil] has correctly been + particularised and quantified. *) Definition exists_last {A} (l : list A) (Hneq : l <> nil) : @@ -307,12 +307,12 @@ Qed. (** Let's now consider the Ackerman function which is decreasing according to the usual lexicographic order on [nat * nat], [(<,<)] which is accessible - as both [<] are. + as [<] is, and the lexicographic combination of well-founded relations is too. You can define the lexicographic order and automatically derive a proof it is well-founded using the function [Equations.Prop.Subterm.lexprod]. As we can see, with this order, once again no obligations are left to prove as Coq can prove on its own that [(m, (ack (S m) n)) a :: nubBy eq (filter (fun b => negb (eq a b)) l). Fail Lemma In_nubBy {A} (eq : A -> A -> bool) (l : list A) (a : A) : In a (nubBy eq l) -> In a l. -(** The reason is that Coq can not prove on its own that the recursive +(** The reason is that Coq cannot prove on its own that the recursive call is performed on a smaller instance. 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 prove on its own, + Property that is not trivial, and that Coq cannot prove on its own, nor look for on its own without any indications. Consequently, there is an obligation left to solve, and [nubBy] is not defined as long as we have not solve it. @@ -520,10 +520,10 @@ Defined. Though, note that [Equations?] triggers a warning when used on a definition that leaves no obligations unsolved. - It is because for technical reasons, [Equations?] can not check if they - are at least obligation left to solve before opening the proof mode. + It is because for technical reasons, [Equations?] cannot check if there + is at least on obligation left to solve before opening the proof mode. Hence, when there is no obligation proof mode is open for nothing, and - as to be closed by hand using [Qed] or [Defined] as it can be seen bellow. + has to be closed by hand using [Qed] or [Defined] as can be seen below. As it is easy to forget, a warning is raised. *) @@ -532,7 +532,7 @@ foo _ => 0. Qed. (** In practice, if you wish to automatically test if obligations are - left to solve and unshelved them if so, you can just start all your definitions + left to solve and unshelve them if so, you can just start all your definitions with [Equations?] and remove the [?] if the warning is triggered. Reasoning on functions defined by well-founded recursion with @@ -574,7 +574,7 @@ Qed. *** 2.1 The inspect method - When defining a functions, it can happen that we loose information + When defining a function, it can happen that we loose information relevant to termination when matching a value, and that we then get stuck trying to prove termination. @@ -597,8 +597,8 @@ Section Inspect. [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 + with a with clause, if there is one [Some p] then return [p] added to the + chain starting with [p], i.e., our recursive call [f_sequence p], and otherwise stop the computation. *) @@ -612,8 +612,8 @@ Section Inspect. (* 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 +(** Unfortunately, as we can see, if done so we generate an unprovable + obligation as we do not 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, @@ -631,7 +631,7 @@ Section Inspect. [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 ? + [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], @@ -654,7 +654,7 @@ End Inspect. (** *** 2.2 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 + functions that share a common theory, e.g, they involve basic arithmetic. Yet, without surprise, by default the tactic trying to prove obligations is not aware of the particular theory at hand, and it will fail to solve @@ -704,7 +704,7 @@ Show Obligation Tactic. 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]. + to locally change 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: From 162bf2fa3aaf7ce1d28a889a452139eab1ae7c76 Mon Sep 17 00:00:00 2001 From: thomas-lamiaux Date: Sun, 9 Jun 2024 02:04:02 +0200 Subject: [PATCH 12/34] add file on obligations --- src/Tutorial_Equations_Obligations.v | 299 +++++++++++++++++++++++++++ src/Tutorial_Equations_wf.v | 97 ++------- 2 files changed, 313 insertions(+), 83 deletions(-) create mode 100644 src/Tutorial_Equations_Obligations.v diff --git a/src/Tutorial_Equations_Obligations.v b/src/Tutorial_Equations_Obligations.v new file mode 100644 index 0000000..ce6e9c3 --- /dev/null +++ b/src/Tutorial_Equations_Obligations.v @@ -0,0 +1,299 @@ +(** * 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 discuss how it interface with [Program] to help write programs. + + 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: + - When matching on terms, it can happen that we loose information relevant + to termination. + In Section 2.1, 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.2, we explain how to locally adapt the tactic trying to + solve obligations to deal with such goals. + + *** Table of content + + - 1. Equations and Obligations + - 1.1 Obligations + - 1.2 Proving obligations with Program + - 1.3 Using [Equations?] + - 2. Personalising the tactic solving Obligations + + *** Prerequisites + + Needed: + - We assume basic knowledge of Coq, and of defining functions by recursion + - We assume basic knowledge of the Equations plugin, e.g, as presented + in the tutorial Equations: Basics + + Not needed: + - This tutorial discusses well-founded recursion but no prior knowledge + about it is required: we will explain the concept + + Installation: + - Equations is available by default in the Coq Platform + - Otherwise, it is available via opam under the name coq-equations + +*) + + +From Coq Require Import List. +Import ListNotations. + +From Equations Require Import Equations. + +Axiom to_fill : forall A, A. +Arguments to_fill {_}. + + +(** ** 1. Equations and Obligations + + *** 1.1 Obligations + + In some cases, when defining functions, we may have to prove properties. + There can be many reasons for that. Among others, the data structure under + consideration may can include invariants that we must prove to be preserved + when defining functions. + + For instance, vectors of size [n] can be defined as lists of length [n], + that is, as a list [l] with a proof that [length l = n]. +*) + +Definition vec A n := { l : list A | length l = n }. + +(** To define a function [vec A n -> vec A m], one has to explain how the + function acts on lists, and to prove that the resulting list is of size + [m] providing the original one is of size [n]. + + For instance, to define a concatation function on vectors + [vapp : vec A n -> vec A m -> vec A (n + m)], as done below, one has to: + - specify that the concatenation of [l] and [l'] is [app l l'] and, + - prove that [legnth (ln ++ lm) = n + m] which is done below by the + term [eq_trans (app_length ln lm) (f_equal2 Nat.add Hn Hm)] +*) + +Equations vapp {A n m} (v1 : vec A n) (v2 : vec A m) : vec A (n + m) := +vapp (exist _ ln Hn) (exist _ lm Hm) := + (exist _ (app ln lm) + (eq_trans (app_length ln lm) (f_equal2 Nat.add Hn Hm))). + +(** Yet, in most cases, when defining a function, we do not want to write down + the proofs directly as terms. There are many reasons for that: + - in practice, proof terms can be arbitrarily large and complex making it + tedious if not impossible to write them down directly as a terms + - even if we could, this can easily make the function completely illegible + - in case of changes, it is not possible to replay a term proof as we can + replay a tactic script in order to adpat it, making functions harder + to modify and maintain + + Therefore, we would much rather like to build our terms using the proof mode. + This is exactly what [Program] and obligations enables us to do. + At every point in a definition we can: + - 1. write down a wildcard "_" instead of a term + - 2. it will then create an obligation, intuitively a goal left to solve + to complete the definition + - 3. will try to simplify it and solve it using a tactic, here custom to [Equations] + - 4. if they are any obligations left to solve, we can prove them using + the proof mode and tactics + + For instance, we can define a function [vmap f n : vec A n -> vec A n] + by using a whildcard `_` where a proof of [length (map f ln) = n] + is expected in order to prove it using the proof mode and tactics: +*) + +Equations vmap {A B n} (f : A -> B) (v : vec A n) : vec B n := +vmap f (exist _ ln Hn) := exist _ (map f ln) _ . + +(** However, be careful that [vmap] is not defined until the obligations + remaining have been solved. + Trying to prove a property about [vmap] before will therefore return + that [vmap] was not find in the environnement: +*) + +Fail Definition vmap_comp {A B C n} (g : B -> C) (f : A -> B) (v : vec A n) + : vmap g (vmap f n v) = vmap (fun x => g (f x)) v. + + +(** *** 1.2 Solving obligations + + There are two different methods to solve the remaining obligations. + + You can solve the obligations one by one using the command [Next Obligations]. + Doing so for [vmap] display the goal [length (map f ln) = length ln], + which we can then solve using tactics. + You may be surprised it is not [length (map f n) = n]. It is because + [Equations] custom solving tactic has pre-simplified the goal for us. +*) + +Next Obligation. + apply map_length. +Qed. + +(** Using [Next Obligation] has the advantage that once an obligation has been + solved, [Program] retries automatically to prove the remaining obligations. + It can be practical when TODO. + + Note, that it can be useful to add [Fail Next Obligation] once all + obligations have been solved. + This way, if a change somewhere now leaves an obligation unsolved, we can + easily track down the issue to the culprit definition. + + Alternatively, it is possible to use the keyword [Equations?] to automatically + unshelve all obligations, that is enter the proof mode and create a goal + for each of the obligations remaining. + + For an example, we can redefine [vmap] using it: +*) + +Equations? vmap' {A B n} (f : A -> B) (v : vec A n) : vec B n := +vmap' f (exist _ ln Hn) := exist _ (map f ln) _ . +Proof. + apply map_length. +Defined. + +(** Though, note that [Equations?] triggers a warning when used on a definition + that leaves no obligations unsolved. + It is because for technical reasons, [Equations?] cannot check if there + is at least on obligation left to solve before opening the proof mode. + Hence, when there is no obligation proof mode is open for nothing, and + has to be closed by hand using [Qed] or [Defined] as it can be seen below. + As it is easy to forget, a warning is raised. +*) + +Equations? vnil {A} : vec A 0 := +vnil := exist _ nil eq_refl. +Defined. + + +(** ** 2. Equations' solving tactic + + As mentionned, [Equations] automatically tried to solve obligations. + It does so using a custom strategy basically simplifying the goals and + running a solver. + It can be viewed with the following command: +*) + +Show Obligation Tactic. + +(** 2.1 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 involve basic arithmetic. + This theory cannot not be guessed from the basic automation tactic, + so may be personalising a tactic to handle this particular theory. + + This can be done using the command [ #[local] Obligation Tactic := tac ] + to locally change the tactic solving obligation to a tactic [tac]. + + For an example, consider a [gcd] function defined by well-founded recursion. + There are two obligations left to prove corresponding proofs that recursive + call are indeed smaller. Each of them corresponds to basic reasonning about + aritmetics, and can hence be solved with the solver [lia]. +*) + +Require Import Arith Lia. + +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. + +(** Therefore, we would like to locally change the tactic solving the + obligations to take into account arithmetic, and try [lia]. + We do so by simply trying it after the curreny solving tactic, + i.e. the one displayed by [Show Obligation Tactic]. + As we can see by running again [Show Obligation Tactic], it has indeed been + added, and [gcd] is now accepted directly. +*) + +#[local] Obligation Tactic := + simpl in *; + Tactics.program_simplify; + CoreTactics.equations_simpl; + try Tactics.program_solve_wf; + try lia. + +Show Obligation Tactic. + +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 + }. + +(** 2.2 Wha to do if goals are oversimplified + + In some cases, it can happen that [Equations]' solving tactic is too abrut + and oversimply goals and ended up getting us stuck. + In this case, it can be useful to set the solving tactic to the identify. + + For an example, let's define a function + [vzip : vec A n -> vec B n -> vec (A * B) n] without using [list_prod]. + In all cases where a proof is expected we create an obligation, and uses + the proof mode to handle the reasonning on arithmetics. + We also use obligations to disregard the case [nil (b::lb)] and [(a::la) nil]. + + As it can be seen below, [Equations] can automatically with the first three + goal, and first ask us which integer is used [n] the first. + TODO ?? +*) + + Equations? vzip {A B n} (va : vec A n) (vb : vec B n) : vec (A * B) n := + vzip (exist _ [] ea) (exist _ [] eb) => exist _ [] _; + vzip (exist _ [] ea) (exist _ (b::lb) eb) => _; + vzip (exist _ (a::la) ea) (exist _ [] eb) => _; + vzip (exist _ (a::la) ea) (exist _ (b::lb) eb) + with vzip (exist _ la _) (exist _ lb _ ) := { + | exist _ l _ => exist _ ((a,b)::l) _ + }. + Proof. + - exact (length lb). + - + Abort. + + +(** Consequently, it can be easier to change the tactic locally to TODO *) +#[local] Obligation Tactic := idtac. + +Equations? vzip {A B n} (va : vec A n) (vb : vec B n) : vec (A * B) n := +vzip (exist _ [] ea) (exist _ [] eb) => exist _ [] _; +vzip (exist _ [] ea) (exist _ (b::lb) eb) => _; +vzip (exist _ (a::la) ea) (exist _ [] eb) => _; +vzip (exist _ (a::la) ea) (exist _ (b::lb) eb) + with vzip (exist _ la _) (exist _ lb _ ) := { + | exist _ l _ => exist _ ((a,b)::l) _ + }. +Proof. + - exact ea. + - cbn in *. rewrite <- ea in eb; inversion eb. + - cbn in *. rewrite <- ea in eb; inversion eb. + - destruct n. 1: inversion ea. exact n. + - destruct n; inversion ea. reflexivity. + - destruct n; inversion eb. reflexivity. + - destruct n; inversion ea. cbn. rewrite e, H0. reflexivity. +Defined. \ No newline at end of file diff --git a/src/Tutorial_Equations_wf.v b/src/Tutorial_Equations_wf.v index 89e98df..99787ad 100644 --- a/src/Tutorial_Equations_wf.v +++ b/src/Tutorial_Equations_wf.v @@ -22,11 +22,7 @@ to termination. In Section 2.1, 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.2, we explain how to locally adapt the tactic trying to - solve obligations to deal with such goals. + - *** Table of content @@ -36,7 +32,7 @@ - 1.3 Well-founded recursion and Obligations - 2. Different methods to work with well-founded recursion - 2.1 The inspect method - - 2.2 Personalising the tactic proving obligations + - 2.2 ??? *** Prerequisites @@ -44,6 +40,7 @@ - We assume basic knowledge of Coq, and of defining functions by recursion - We assume basic knowledge of the Equations plugin, e.g, as presented in the tutorial Equations: Basics + - Not needed: - This tutorial discusses well-founded recursion but no prior knowledge @@ -651,91 +648,25 @@ Section Inspect. End Inspect. -(** *** 2.2 Personalising the tactic proving obligations - - When working, it is common to be dealing with a particular class of - functions that share a common theory, e.g, they involve basic - arithmetic. - Yet, without surprise, 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, as 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 a [gcd] function, - and show how function elimination then enables to prove a few properties - efficiently. - - We can define a [gcd] function that does not require the assumption that - [x > y] as below, by first checking if [x] or [y] is [0], and otherwise - compare [x] and [y], and recall [gcd] with [x - y] or [y - x] depending - which is the greater. - 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]. -*) +(* +For an example, consider a [gcd] function that does not require the assumption that +[x > y] as below, by first checking if [x] or [y] is [0], and otherwise +compare [x] and [y], and recall [gcd] with [x - y] or [y - x] depending +which is the greater. +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 }. +| inleft (left _) := gcd x (y - x) ; +| inleft (right refl) := x ; +| inright _ := gcd (x - y) y }. Proof. - lia. lia. +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 locally change 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 how useful it is on complex definitions, we will now show a few properties of [gcd]. From 09640bc8ff27e2a1e245ca93e37bf76176864782 Mon Sep 17 00:00:00 2001 From: thomas-lamiaux Date: Sun, 9 Jun 2024 02:11:37 +0200 Subject: [PATCH 13/34] typos --- src/Tutorial_Equations_Obligations.v | 67 +++++++++++----------------- 1 file changed, 26 insertions(+), 41 deletions(-) diff --git a/src/Tutorial_Equations_Obligations.v b/src/Tutorial_Equations_Obligations.v index ce6e9c3..98df003 100644 --- a/src/Tutorial_Equations_Obligations.v +++ b/src/Tutorial_Equations_Obligations.v @@ -1,39 +1,25 @@ -(** * Well-founded Recursion using Equations +(** * Equations and Obligations *** Summary [Equations] is a plugin for %\cite{Coq}% that offers a powerful support for writing functions by dependent pattern matching. - In this tutorial, we discuss how it interface with [Program] to help write programs. - - 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: - - When matching on terms, it can happen that we loose information relevant - to termination. - In Section 2.1, 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.2, we explain how to locally adapt the tactic trying to - solve obligations to deal with such goals. + In this tutorial, we discuss how it interface with [Program] to help write + programs using obligations. + + In section 1, we recall the concept of obligation and how they interface with [Equations]. + In Section 2, we explain how [Equations]' obligation solving tactic. + *** Table of content - 1. Equations and Obligations - 1.1 Obligations - - 1.2 Proving obligations with Program - - 1.3 Using [Equations?] - - 2. Personalising the tactic solving Obligations + - 1.2 Solving obligations + - 2. Equations' solving tactic + - 2.1 Personalizing the tactic proving obligations + - 2.2 What to do if goals are oversimplified + *** Prerequisites @@ -43,8 +29,6 @@ in the tutorial Equations: Basics Not needed: - - This tutorial discusses well-founded recursion but no prior knowledge - about it is required: we will explain the concept Installation: - Equations is available by default in the Coq Platform @@ -81,10 +65,10 @@ Definition vec A n := { l : list A | length l = n }. function acts on lists, and to prove that the resulting list is of size [m] providing the original one is of size [n]. - For instance, to define a concatation function on vectors + For instance, to define a concatenation function on vectors [vapp : vec A n -> vec A m -> vec A (n + m)], as done below, one has to: - specify that the concatenation of [l] and [l'] is [app l l'] and, - - prove that [legnth (ln ++ lm) = n + m] which is done below by the + - prove that [length (ln ++ lm) = n + m] which is done below by the term [eq_trans (app_length ln lm) (f_equal2 Nat.add Hn Hm)] *) @@ -99,7 +83,7 @@ vapp (exist _ ln Hn) (exist _ lm Hm) := tedious if not impossible to write them down directly as a terms - even if we could, this can easily make the function completely illegible - in case of changes, it is not possible to replay a term proof as we can - replay a tactic script in order to adpat it, making functions harder + replay a tactic script in order to adapt it, making functions harder to modify and maintain Therefore, we would much rather like to build our terms using the proof mode. @@ -113,7 +97,7 @@ vapp (exist _ ln Hn) (exist _ lm Hm) := the proof mode and tactics For instance, we can define a function [vmap f n : vec A n -> vec A n] - by using a whildcard `_` where a proof of [length (map f ln) = n] + by using a wildcard `_` where a proof of [length (map f ln) = n] is expected in order to prove it using the proof mode and tactics: *) @@ -147,7 +131,8 @@ Qed. (** Using [Next Obligation] has the advantage that once an obligation has been solved, [Program] retries automatically to prove the remaining obligations. - It can be practical when TODO. + It can be practical when proofs are simple but requires for a evariable + to be solved to proceed first. Note, that it can be useful to add [Fail Next Obligation] once all obligations have been solved. @@ -183,7 +168,7 @@ Defined. (** ** 2. Equations' solving tactic - As mentionned, [Equations] automatically tried to solve obligations. + As mentioned, [Equations] automatically tried to solve obligations. It does so using a custom strategy basically simplifying the goals and running a solver. It can be viewed with the following command: @@ -191,20 +176,20 @@ Defined. Show Obligation Tactic. -(** 2.1 Personalising the tactic proving obligations +(** 2.1 Personalizing 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 involve basic arithmetic. This theory cannot not be guessed from the basic automation tactic, - so may be personalising a tactic to handle this particular theory. + so may be personalizing a tactic to handle this particular theory. This can be done using the command [ #[local] Obligation Tactic := tac ] to locally change the tactic solving obligation to a tactic [tac]. For an example, consider a [gcd] function defined by well-founded recursion. There are two obligations left to prove corresponding proofs that recursive - call are indeed smaller. Each of them corresponds to basic reasonning about - aritmetics, and can hence be solved with the solver [lia]. + call are indeed smaller. Each of them corresponds to basic reasoning about + arithmetics, and can hence be solved with the solver [lia]. *) Require Import Arith Lia. @@ -222,7 +207,7 @@ Abort. (** Therefore, we would like to locally change the tactic solving the obligations to take into account arithmetic, and try [lia]. - We do so by simply trying it after the curreny solving tactic, + We do so by simply trying it after the current solving tactic, i.e. the one displayed by [Show Obligation Tactic]. As we can see by running again [Show Obligation Tactic], it has indeed been added, and [gcd] is now accepted directly. @@ -246,7 +231,7 @@ gcd x y with gt_eq_gt_dec x y := { | inright _ := gcd (x - y) y }. -(** 2.2 Wha to do if goals are oversimplified +(** 2.2 What to do if goals are oversimplified In some cases, it can happen that [Equations]' solving tactic is too abrut and oversimply goals and ended up getting us stuck. @@ -255,7 +240,7 @@ gcd x y with gt_eq_gt_dec x y := { For an example, let's define a function [vzip : vec A n -> vec B n -> vec (A * B) n] without using [list_prod]. In all cases where a proof is expected we create an obligation, and uses - the proof mode to handle the reasonning on arithmetics. + the proof mode to handle the reasoning on arithmetics. We also use obligations to disregard the case [nil (b::lb)] and [(a::la) nil]. As it can be seen below, [Equations] can automatically with the first three From f5406894c167df16cd044e26b4e6ed3684e444ee Mon Sep 17 00:00:00 2001 From: thomas-lamiaux Date: Sun, 9 Jun 2024 15:36:27 +0200 Subject: [PATCH 14/34] edits obligations --- src/Tutorial_Equations_Obligations.v | 81 ++++++++++++++++++---------- 1 file changed, 52 insertions(+), 29 deletions(-) diff --git a/src/Tutorial_Equations_Obligations.v b/src/Tutorial_Equations_Obligations.v index 98df003..4c71a22 100644 --- a/src/Tutorial_Equations_Obligations.v +++ b/src/Tutorial_Equations_Obligations.v @@ -8,7 +8,7 @@ programs using obligations. In section 1, we recall the concept of obligation and how they interface with [Equations]. - In Section 2, we explain how [Equations]' obligation solving tactic. + In Section 2, we discuss [Equations]' obligation solving tactic. *** Table of content @@ -50,7 +50,7 @@ Arguments to_fill {_}. *** 1.1 Obligations - In some cases, when defining functions, we may have to prove properties. + In some cases, to define functions we may have to prove properties. There can be many reasons for that. Among others, the data structure under consideration may can include invariants that we must prove to be preserved when defining functions. @@ -68,8 +68,8 @@ Definition vec A n := { l : list A | length l = n }. For instance, to define a concatenation function on vectors [vapp : vec A n -> vec A m -> vec A (n + m)], as done below, one has to: - specify that the concatenation of [l] and [l'] is [app l l'] and, - - prove that [length (ln ++ lm) = n + m] which is done below by the - term [eq_trans (app_length ln lm) (f_equal2 Nat.add Hn Hm)] + - provide a proof term that [length (ln ++ lm) = n + m], which is done + below by the term [eq_trans (app_length ln lm) (f_equal2 Nat.add Hn Hm)]. *) Equations vapp {A n m} (v1 : vec A n) (v2 : vec A m) : vec A (n + m) := @@ -78,38 +78,62 @@ vapp (exist _ ln Hn) (exist _ lm Hm) := (eq_trans (app_length ln lm) (f_equal2 Nat.add Hn Hm))). (** Yet, in most cases, when defining a function, we do not want to write down - the proofs directly as terms. There are many reasons for that: + the proofs directly as terms, as we did above. + There are many reasons for that: - in practice, proof terms can be arbitrarily large and complex making it - tedious if not impossible to write them down directly as a terms + tedious if not impossible to write them down directly as terms - even if we could, this can easily make the function completely illegible - in case of changes, it is not possible to replay a term proof as we can replay a tactic script in order to adapt it, making functions harder - to modify and maintain + to adapt Therefore, we would much rather like to build our terms using the proof mode. This is exactly what [Program] and obligations enables us to do. - At every point in a definition we can: - - 1. write down a wildcard "_" instead of a term + At every point in a definition, it enables us: + - 1. write down a wildcard [_] instead of a term - 2. it will then create an obligation, intuitively a goal left to solve to complete the definition - - 3. will try to simplify it and solve it using a tactic, here custom to [Equations] + - 3. it will try to simplify the obligations and solve them using a tactic, + in our case, using a tactic specific to [Equations] - 4. if they are any obligations left to solve, we can prove them using - the proof mode and tactics + the proof mode and tactics using [Next Obligation] or [Equations?] that + we discuss in section 1.2 - For instance, we can define a function [vmap f n : vec A n -> vec A n] - by using a wildcard `_` where a proof of [length (map f ln) = n] - is expected in order to prove it using the proof mode and tactics: + + For instance, we can define a function [vapp n m : vec A n -> vec A m -> vec A (n+m)] + using a wildcard [_] where a proof of [length (app ln lm) = n + m] + is expected to prove it using tactics: *) -Equations vmap {A B n} (f : A -> B) (v : vec A n) : vec B n := -vmap f (exist _ ln Hn) := exist _ (map f ln) _ . +Equations vapp' {A n m} (v1 : vec A n) (v2 : vec A m) : vec A (n + m) := +vapp' (exist _ ln Hn) (exist _ lm Hm) := exist _ (app ln lm) _. +Next Obligation. + apply app_length. +Qed. + +(** As you can see, this very pratical however, you should be aware of + three basic pitfalls that: -(** However, be careful that [vmap] is not defined until the obligations - remaining have been solved. - Trying to prove a property about [vmap] before will therefore return - that [vmap] was not find in the environnement: + 1. As you may have noticed the goal to prove was not [length (app ln lm) = n + m] + as expected, but [length (app ln lm) = length ln + length lm]. + It is because [Equations] custom solving tactic has already pre-simplified + the goal for us. In can be an issue in some cases, and we discuss it in + section 2.1. + + 2. Technically, you can use a wildcard [_] for any term, even for one + relevant to the definition and computation like [app ln lm] . + Yet, it generally it is a bad idea as automation could then infer + something random that matches the type expected. + + 3. Be aware that a definition is not defined until the all its associated + obligations have been solved. Trying to refer to it before that, we + consequently return that the defintion was not found. + For instance, consider the unfinished definition of [vmap] with a wildcar [_] *) +Equations vmap {A B n} (f : A -> B) (v : vec A n) : vec B n := +vmap f (exist _ ln Hn) := exist _ (map f ln) _ . + Fail Definition vmap_comp {A B C n} (g : B -> C) (f : A -> B) (v : vec A n) : vmap g (vmap f n v) = vmap (fun x => g (f x)) v. @@ -120,9 +144,7 @@ Fail Definition vmap_comp {A B C n} (g : B -> C) (f : A -> B) (v : vec A n) You can solve the obligations one by one using the command [Next Obligations]. Doing so for [vmap] display the goal [length (map f ln) = length ln], - which we can then solve using tactics. - You may be surprised it is not [length (map f n) = n]. It is because - [Equations] custom solving tactic has pre-simplified the goal for us. + which we can then solve using tactics.. *) Next Obligation. @@ -132,7 +154,7 @@ Qed. (** Using [Next Obligation] has the advantage that once an obligation has been solved, [Program] retries automatically to prove the remaining obligations. It can be practical when proofs are simple but requires for a evariable - to be solved to proceed first. + to be solved first to be able to proceed. Note, that it can be useful to add [Fail Next Obligation] once all obligations have been solved. @@ -184,12 +206,13 @@ Show Obligation Tactic. so may be personalizing a tactic to handle this particular theory. This can be done using the command [ #[local] Obligation Tactic := tac ] - to locally change the tactic solving obligation to a tactic [tac]. + that changes locally the tactic solving obligation to [tac]. For an example, consider a [gcd] function defined by well-founded recursion. - There are two obligations left to prove corresponding proofs that recursive - call are indeed smaller. Each of them corresponds to basic reasoning about - arithmetics, and can hence be solved with the solver [lia]. + There are two obligations left to prove corresponding to proofs that the recursive + call are indeed performed on smaller instance. + Each of them corresponds to basic reasoning about arithmetics, and can + be solved with the solver [lia]. *) Require Import Arith Lia. @@ -234,7 +257,7 @@ gcd x y with gt_eq_gt_dec x y := { (** 2.2 What to do if goals are oversimplified In some cases, it can happen that [Equations]' solving tactic is too abrut - and oversimply goals and ended up getting us stuck. + and oversimply goals, or mis-specialised and ended up getting us stuck. In this case, it can be useful to set the solving tactic to the identify. For an example, let's define a function From f7df1fc2d91353ab0ed58a2137ca565c5f893fd4 Mon Sep 17 00:00:00 2001 From: thomas-lamiaux Date: Sun, 9 Jun 2024 18:01:32 +0200 Subject: [PATCH 15/34] Major refactoring of tuto wf: -> Seperate section 1 in two sections "Intro to wf" and "wf and Equations" -> Remove the last example from the file, and ack from 1.2 -> Remove content that is now in tuto obligations --- src/Tutorial_Equations_wf.v | 645 ++++++++++++------------------------ 1 file changed, 212 insertions(+), 433 deletions(-) diff --git a/src/Tutorial_Equations_wf.v b/src/Tutorial_Equations_wf.v index 99787ad..2487965 100644 --- a/src/Tutorial_Equations_wf.v +++ b/src/Tutorial_Equations_wf.v @@ -7,46 +7,38 @@ 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: - - When matching on terms, it can happen that we loose information relevant - to termination. - In Section 2.1, we show an example of that and discuss the inspect - method as a possible solution to this problem. - - + In section 1, we explain the interrests and the principle of well-founded recursion. + We then explain in section 2, how to define functions and how to reason about + them using well-founded recursion and [Equations]. + In some cases, applying well-founded recursion can fail because information + relevant to termination gets lost during recurion. + In section 3, we discuss two such cases an how to go around the issues. *** 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 The inspect method - - 2.2 ??? + - 1. Introduction to well-founded recursion + - 1.1 The syntactic guard condition is limited + - 1.2 Well-founded recursion + 2. Well-founded recursion and Equations + 2.1 Using a size argument + 2.2 Using a mesure + 2.3 Using a lexicographic order + 2.4 Using a custom well-founded relation + 2.5 Using the subterm relation ??? + - 3. Different tricks to work with well-founded recursion + - 3.1 The inspect method + - 3.2 map thing ??? *** Prerequisites Needed: - We assume basic knowledge of Coq, and of defining functions by recursion - - We assume basic knowledge of the Equations plugin, e.g, as presented - in the tutorial Equations: Basics - - + - We assume basic knowledge of the Equations plugin and of obligations, e.g, + as presented in the tutorials Equations: Basics and Equations: Obligations Not needed: - This tutorial discusses well-founded recursion but no prior knowledge about it is required: we will explain the concept - - 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 automation tactics [lia] and [auto with arith], but they can be used as black boxes @@ -64,84 +56,47 @@ Axiom to_fill : forall A, A. Arguments to_fill {_}. -(** ** 1. Defining and reasoning using well-founded recursion - - *** 1.1 Introduction to well-founded recursion +(** ** 1. Introduction to well-founded recursion For Coq to be consistent, all functions must be terminating. - To ensure they are, Coq checks that they satisfy a syntactic + To ensure they are, Coq checks that they satisfy 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's syntactic - guard fails to see as such on its own. - - - *** The syntactic guard condition is limited - - As a first example, 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 remembers [l] as a smaller subterm. -*) + Very roughly, the guard condition basically checks that all recursive call + are performed on syntactically smaller instance. + Though, while practical and powerful, this syntactic criterion is by nature + limited and not complete: it can happen that functions can be proven terminating + using size and mathematical arguments even though the guard fails to them as such. -Fail Equations last {A} (l : list A) : option 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. - We can show that this function is terminating by using the lexicographic order: - [(n,m) negb (eq x y)) l]. - We can prove that [filter] does not increase the size of a list, and hence - that the recursive call is indeed performed on a smaller instance, and - that nubBy is terminating. - But, without surprise, it cannot be checked automatically using Coq's - syntactic guard as it involves mathematical reasoning on [filter]. + on the list [filter (fun y => negb (eq x y)) l]. This prevent the syntactic + from checking it is indeed smaller, and is hence rejected. + Yet, we can prove that [filter] does not increase the size of a list, and hence + that the recursive call is indeed performed on a "smaller" instance than [l] + and that [nubBy] is terminating. *) Fail Equations nubBy {A} (eq : A -> A -> bool) (l : list A) : list A := nubBy eq [] => []; nubBy eq (a :: l) => a :: nubBy eq (filter (fun b => negb (eq a b)) l). -(** Furthermore, in contrast to to functions like [ack] or [nubBy], some recursive - functions are simply not naturally defined by structural recursion. +(** Furthermore, it can also happen that the recursive structure of a definition + do not follow the inductive structure of any datatypes, but instead + fully rely on semantic arguments to decide which recursive call to + perform, logically preventing the guard condition from checking it. + A prime example is the Euclidean algorithm computing the gcd of [x] and [y] assuming that [x > y]. - It performs recursion on [x mod y] which is not a function of + It performs recursion on [x mod y] which is not a subterm of any recursively smaller arguments, as [gcd] does not match any inputs. It is well-founded and terminating for [lt], as we have tested that [y > 0] and we can prove that [x mod y < y]. @@ -149,18 +104,31 @@ nubBy eq (a :: l) => a :: nubBy eq (filter (fun b => negb (eq a b)) l). its definition fully relies on theoretic reason to ensure termination. *) -Fail Equations gcd (x y : nat) : nat := -gcd x y with Nat.eq_dec y 0 => { +Fail Equations gcd (x y : nat) (H : x > y) : nat := +gcd x y H with Nat.eq_dec y 0 => { | left _ => x | right _ => gcd y (x mod y) }. -(** *** Well-founded recursion - It would be limiting if functions of this kind could not be defined. - Fortunately, they can be, using well-founded recursion. +(** *** 1.2 Well-founded recursion + + It would be limiting if this kind of functions could not be defined. + Fortunately, they can be using well-founded recursion. + + ### TODO MAKE CLEAN ### + - Given a well-founded relation [R : A -> A -> Type], defining a function + Informally, well-founded recursion bascially amounts to justifying termination by: + - providing a "well-founded" relation [R : A -> A -> Prop], intuitively an + order like [<] on natural numbers for which it is impossible to deacrease infinitely + - proving that all the recursive calls are performed on smaller arguments according + [R] + + More formally, a relation [R : A -> A -> Prop] is "well-founded" when + + + Given a well-founded relation [R : A -> A -> Prop], defining a function [f] by well-founded recursion on [a : A] consists in defining [f] assuming that [f] is defined for all [a'] smaller than [a], that is such that [R a' a]. When particularised to natural numbers and [<], this concept is sometimes @@ -215,94 +183,149 @@ Definition gcd_Fix (x y : nat) : nat := *) -(** *** 1.2 Basic definitions and reasoning +(** ** 2. Well-founded recursion and Equations - To define a function by well-founded recursion with Equations, one must add, - after the type of the function, the command [by wf x R] where [x] is the term + To define a function by well-founded recursion with Equations, one must add + after the type of the function [by wf x R], where [x] is the term decreasing, and [R] the well-founded relation for which [x] decreases. - For instance, 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. - We hence, need to write: + For instance, the function [nubBy] terminates as the size of the list decrease + in each recursive call according to the usual strict order [<] on [nat], [lt] in Coq. + We hence, need to write [wf (size l) l] to define it by well-founded recursion: [[ - Equations last {A} (l : list A) : option A by wf (length l) lt := + Equations nubBy {A} (eq : A -> A -> bool) (l : list A) : list A by wf (size l) lt := ]] Equations will then automatically: - - 1. Search for a proof that [R] is well-founded, using type classes from a database + - 1. Search for a proof that [R] is well-founded, using type classes (a database) specific to [Equations] suitably named [WellFounded] - - 2. Try to prove that the recursive calls are done on decreasing arguments, - and if it cannot do it on its own, it will generate a proof obligation - i.e. a goal for the user to fill. + - 2. It will then create an obligation to prove that each recursive call + is performed on decreasing arguments, try to prove it automatically, + and if it cannot do it on its own leave it to us to prove This allows to separate the proofs that the recursive call are smaller - from the definition of the function, making it easier to read while dealing - automatically with trivial cases. - - In this section, we focus on simple examples where no obligations are - left for the user to solve, and we refer to section 1.3 for more involved - examples with non trivial obligations. - - Let us first consider the definition of [last] that we can define by - well-founded recursion, adding the following indication: [by wf (length l) lt]. - [Equations] will then creates one obligation per recursive call and - try to solve them. - In the case of [last], it creates the obligation [length (a'::l) < length (a::a'::l)] - which as we can check is solved automatically. + from the definition of the function, making it easier to read and define + while dealing automatically with trivial cases. + Moreover, it enables us to prove arguments directly in the proof mode using + tactics. + + ** 2.1 Using a size argument + + 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]. *) -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). - -(** Defining [last] by well-founded recursion is hence effortless and the - definition is as legible as we would hope. - - Moreover, thanks to functional induction through [funelim], we can reason - about functions 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 us 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] has correctly been - particularised and quantified. +Equations? nubBy {A} (eq : A -> A -> bool) (l : list A) : list A by wf (length l) lt := +nubBy eq [] => []; +nubBy eq (a :: l) => a :: nubBy eq (filter (fun b => negb (eq a b)) l). +Proof. + eapply Nat.le_lt_trans. + - apply filter_length_le. + - auto with arith. +Qed. + + +(** 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. *) -Definition exists_last {A} (l : list A) (Hneq : l <> nil) : - { a : A & last l = (Some a)}. +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 a a); destruct Heq as [_ Heqx]. + specialize (Heqx eq_refl); rewrite Heqx in Hneqx. + inversion Hneqx. + -- assumption. +Qed. + +(** ** 2.2 Using a mesure + + For an example, consider a [gcd] function that does not require the assumption that + [x > y] as below, by first checking if [x] or [y] is [0], and otherwise + compare [x] and [y], and recall [gcd] with [x - y] or [y - x] depending + which is the greater. + 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. - funelim (last l); simp last. - - specialize (Hneq eq_refl) as []. - - exists a. reflexivity. - - apply X. discriminate. -Defined. +lia. lia. +Abort. -(** Similarly, we can prove that [last] respects [app] in a suitable way. +(** For further examples of how functional elimination works on well-founded + recursion and how useful it is on complex definitions, we will now show a + few properties of [gcd]. *) -Definition last_app {A} (l l': list A) (Hneq : l' <> nil) : - last (l ++ l') = last l'. +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 (last l); cbn; autorewrite with last. + 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. - - funelim (last l'); simp last. - -- specialize (Hneq eq_refl) as []. - -- reflexivity. - -- reflexivity. - - apply H. assumption. + - 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. -(** Let's now consider the Ackerman function which is decreasing according to + + +(** ** 2.3 Using a lexicographic order + + Let's now consider the Ackerman function which is decreasing according to the usual lexicographic order on [nat * nat], [(<,<)] which is accessible as [<] is, and the lexicographic combination of well-founded relations is too. You can define the lexicographic order and automatically derive a proof @@ -333,33 +356,14 @@ Abort. problem here. This a known issue and it is currently being investigated and fixed. - There are two main solutions to go around similar issue depending on your case: - - If your pattern is fully generic, i.e. of the form [ack m n], you can - apply the [ack_elim] lemma directly. - Though note, that in this case you may need to generalise the goal by hand, - in particular by equalities (e.g. using the remember tactic) if the function - call being eliminated is not made of distinct variables. - - If your pattern is partially specialised like [ack 1 n], it is better to - finish reproducing the pattern using [induction]. - Indeed, [ack_elim] "reproduces" the full pattern, that is, it generalise [1] - and tries to prove [ack m n = 2 + n] by induction, creating cases like - [ack (S m) n] which clearly are not warranted here. - - For instance, let us prove [ack1 : ack 1 n = 2 + n]: -*) + There are two main solutions to go around similar issue depending on your case. -Definition ack1 {n} : ack 1 n = 2 + n. -Proof. - (* If we apply [ack_elim], we get unwarranted cases *) - apply ack_elim. - Restart. - (* So we reproduce the pattern with induction *) - induction n. all: simp ack. - - reflexivity. - - rewrite IHn. reflexivity. -Qed. - -(* For general patterns, applying [ack_elim] directly works *) + If your pattern is fully generic, i.e. of the form [ack m n], you can + apply the [ack_elim] lemma directly. + Though note, that in this case you may need to generalise the goal by hand, + in particular by equalities (e.g. using the remember tactic) if the function + call being eliminated is not made of distinct variables. +*) Definition ack_min {m n} : n < ack m n. Proof. apply ack_elim; intros. @@ -368,215 +372,42 @@ Proof. - eapply Nat.le_lt_trans; eassumption. Qed. -(** Let us now mention an issue due to [rewrite] that can sometimes come up. - - If we try to prove [ack_incr] below by induction, in the base case, we have to prove - that [S n0 < ack 0 (n0 + 1)] which should be simple as [ack 0 (n0 + 1)] is equal - to [S (n0 + 1)], and clearly [S n0 < S (n0 + 1)]. - Yet, surprisingly [simp ack] fails to simplify [ack 0 (n0 + 1)] to [S (n0 + 1)]. - The reason is that [simp ack] relies on [rewrite] to simplify the goal, - and in this particular case it behaves unexpectedly. - Rewriting by the first equation associated to ack [ack_equation_1 : forall (n : nat), - ack 0 n = S n], which is what should be done, fails saying there is a loop. - The reason is that rather than unifying [n] with [n0 + 1], for a reason - or another, [rewrite] ends up converting [S n] to [ack 0 n] and - unify [n] with [n0] which then creates a loop. - - The simplest method to go around this issue is to give [n] by hand. - This way it can not be inferred wrong, and rewrites work: -*) -Definition ack_incr {m n} : ack m n < ack m (n+1). -Proof. - apply ack_elim; intros. - - Fail progress simp ack. Fail rewrite ack_equation_1. - (* It failed because it inferred [n] wrong *) - (* To prevent that, we give it by hand *) - rewrite (ack_equation_1 (n0 + 1)). - rewrite Nat.add_comm. auto with arith. - - rewrite Nat.add_comm. simp ack. apply ack_min. - - rewrite Nat.add_comm. simp ack. apply ack_min. -Qed. - - -(** As exercises, 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 +(** However, if your pattern is partially specialised like [ack 1 n], + it is better to finish reproducing the pattern using [induction]. + Indeed, [ack_elim] "reproduces" the full pattern, that is, it generalise [1] + and tries to prove [ack m n = 2 + n] by induction, creating cases like + [ack (S m) n] which clearly are not warranted here. *) -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]}}. -Proof. -Admitted. - - -(** *** 1.3 Well-founded recursion and Obligations - - For a more involved example where Coq cannot prove on its own that the - recursive call are performed on smaller arguments, let us consider the - [nubBy] function. - - 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]. - - If we try to define the function [nubBy] like that, it seems that all is - well and that the definition is accepted. -*) - -Equations nubBy {A} (eq : A -> A -> bool) (l : list A) : list A by wf (length l) lt := -nubBy eq [] => []; -nubBy eq (a :: l) => a :: nubBy eq (filter (fun b => negb (eq a b)) l). - -(** Yet, if we try to use the function [nubBy], e.g. to prove a property - about it, we get the error message "The reference nubBy was not found - in the current environment." -*) - -Fail Lemma In_nubBy {A} (eq : A -> A -> bool) (l : list A) (a : A) - : In a (nubBy eq l) -> In a l. - -(** The reason is that Coq cannot prove on its own that the recursive - call is performed on a smaller instance. - 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 cannot prove on its own, - nor look for on its own without any indications. - Consequently, there is an obligation left to solve, and [nubBy] is not - defined as long as we have not solve it. - - You can check if there is any obligations left to prove and display them - using the command [Obligations]. -*) - -Obligations. - -(** To prove the remaining obligations, you can use the command [Next Obligations]. - It will get the first obligation left to solve, and creates a corresponding - goal to solve. - - For instance, in the case of [nubBy], it display the only obligation - left to solve [length (filter ... l) < length (a::l)]. - You can then solve it using the usual proof mode and tactics: -*) - -Next Obligation. +Definition ack1 {n} : ack 1 n = 2 + n. Proof. - eapply Nat.le_lt_trans. - - apply filter_length_le. - - auto with arith. + (* If we apply [ack_elim], we get unwarranted cases *) + apply ack_elim. + Restart. + (* So we reproduce the pattern with induction *) + induction n. all: simp ack. + - reflexivity. + - rewrite IHn. reflexivity. Qed. -(** As we can see, it was indeed the only obligation as [Next Obligation] fails. - Moreover, we can see that [nubBy] is now defined as [In_nubBy] is well-typed. -*) -Fail Next Obligation. -Lemma In_nubBy {A} (eq : A -> A -> bool) (l : list A) (a : A) - : In a (nubBy eq l) -> In a l. -Abort. + (** ** 2.4 Using a custom well-founded relation *) -(** Unshelving and proving the obligations one by one using [Next Obligation] - can be tedious. - Consequently, the package [Equations] enables to automatically unshelve - all obligations and enter proof mode by starting the definition by - [Equations?] rather than by [Equations]. - See for instance, [nubBy] below. -*) + (* ### TODO ### *) -Equations? nubBy' {A} (eq : A -> A -> bool) (l : list A) : list A by wf (length l) lt := -nubBy' eq [] => []; -nubBy' eq (a :: l) => a :: nubBy' eq (filter (fun b => negb (eq a b)) l). -Proof. - eapply Nat.le_lt_trans. - - apply filter_length_le. - - auto with arith. -Defined. - -(** This is a powerful feature as compared to the [Fix] definition of section 1.1: - the code is perfectly legible, in particular the body of the function and - the proof are clearly separated. - - Though, note that [Equations?] triggers a warning when used on a definition - that leaves no obligations unsolved. - It is because for technical reasons, [Equations?] cannot check if there - is at least on obligation left to solve before opening the proof mode. - Hence, when there is no obligation proof mode is open for nothing, and - has to be closed by hand using [Qed] or [Defined] as can be seen below. - As it is easy to forget, a warning is raised. -*) +(** ** 2.5 Using the subterm relation *) -Equations? foo (n : nat) : nat := -foo _ => 0. -Qed. - -(** In practice, if you wish to automatically test if obligations are - left to solve and unshelve them if so, you can just start all your definitions - with [Equations?] and remove the [?] if the warning is triggered. - 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 a a); 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 The inspect method +(** ** 3. Different methods to work with well-founded recursion When defining a function, it can happen that we loose information relevant to termination when matching a value, and that we then get stuck trying to prove termination. + In this section, we discuss two such example an methods to go around the issue. - In this section, we discuss such an example, and explain a solution to - this problem using the function [inspect]. + *** 3.1 The inspect method 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)] @@ -609,7 +440,7 @@ Section Inspect. (* What to do now ? *) Abort. -(** Unfortunately, as we can see, if done so we generate an unprovable +(** Unfortunately, as we can see, doing so we generate an unprovable obligation as we do not remember information about the call to [f n] being equal to [Some p] in the recursive call [f_sequence p]. @@ -648,57 +479,5 @@ Section Inspect. End Inspect. -(* -For an example, consider a [gcd] function that does not require the assumption that -[x > y] as below, by first checking if [x] or [y] is [0], and otherwise -compare [x] and [y], and recall [gcd] with [x - y] or [y - x] depending -which is the greater. -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. - -(** For further examples of how functional elimination works on well-founded - recursion and how useful it is 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 +(** 2.2 ### TODO ### +*) \ No newline at end of file From f63b2e4c8aeb04d0ab0f96769d122413dde58eae Mon Sep 17 00:00:00 2001 From: thomas-lamiaux Date: Mon, 10 Jun 2024 01:36:54 +0200 Subject: [PATCH 16/34] work on 2.1 2.2 2.3 --- src/Tutorial_Equations_wf.v | 176 ++++++++++++++++++++++-------------- 1 file changed, 106 insertions(+), 70 deletions(-) diff --git a/src/Tutorial_Equations_wf.v b/src/Tutorial_Equations_wf.v index 2487965..1159c7a 100644 --- a/src/Tutorial_Equations_wf.v +++ b/src/Tutorial_Equations_wf.v @@ -21,7 +21,7 @@ - 1.2 Well-founded recursion 2. Well-founded recursion and Equations 2.1 Using a size argument - 2.2 Using a mesure + 2.2 Using a measure 2.3 Using a lexicographic order 2.4 Using a custom well-founded relation 2.5 Using the subterm relation ??? @@ -121,7 +121,7 @@ gcd x y H with Nat.eq_dec y 0 => { Informally, well-founded recursion bascially amounts to justifying termination by: - providing a "well-founded" relation [R : A -> A -> Prop], intuitively an - order like [<] on natural numbers for which it is impossible to deacrease infinitely + order like [<] on natural numbers for which it is impossible to decrease infinitely - proving that all the recursive calls are performed on smaller arguments according [R] @@ -210,15 +210,30 @@ Definition gcd_Fix (x y : nat) : nat := Moreover, it enables us to prove arguments directly in the proof mode using tactics. + In the following, we assume basic knowledge of obligations as discussed + in the (short) tutorial Equations: obligations. + ** 2.1 Using a size argument - 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]. + The most basic method to define a function by well-founded recursion is to + define a size function, and to prove that the size decrease with each + recursive call for the usual strict order [<] on natural numbers. + + This method is already enough to define the function [nubBy], that + recursively filters out the duplicates of a list, by well-founded recursion. + Indeed, the size of a list is its length, and the only recursive call + performed by [nubBy] is on [filter (fun y => negb (eq x y)) l]. + As [filter] can only remove elements, its length is indeed strictly smaller + than [l], and the function is terminating. + + To define [nubBy] using [Equations] and well-founded recursion, it suffices to + add [wf (length l) lt] after typing to indicate on which term, here [length l], and + for which well-founded relation, here [< := lt], we are doing the well-founded recursion on. + An obligation corresponding to proving that the recursive call is smaller, + that is [length (filter (fun y => negb (eq x y)) l) < length l], is created. + As [Equations] can not solve on its own, it then left to us to solve. + Using the keyword [Equations?], it is automatically unshelved, + and we simply have to prove it using tactics. *) Equations? nubBy {A} (eq : A -> A -> bool) (l : list A) : list A by wf (length l) lt := @@ -231,13 +246,18 @@ Proof. Qed. -(** 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. +(** Compared to other methods, reasoning on functions defined with well-founded + recursion with [Equations], is no different than on regular functions. + Using function elimination ([funelim]) we can prove our + properties directly according to the pattern of our definition. + In particular, we do not have to do proofs by reproducing the proof structure + used to prove that the function is well-founded. + It is particularly interresting as it enables to completely hide from the users + , actually you can see no trace of it in the defintion, and to reason about + functions following the recursive call, that is directly as we think about them? - As examples, we show how to prove in a few lines that [nubBy] do - remove all duplicates. + This is a very powerful technic that, for instance, enables us 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) @@ -258,21 +278,35 @@ Proof. - specialize (H Heq). simp nubBy. constructor. -- intros Hi. apply In_nubBy in Hi. - apply filter_In in Hi as [_ Hneqx]. + apply filter_In in Hi as [Hl Hneqx]. specialize (Heq a a); destruct Heq as [_ Heqx]. specialize (Heqx eq_refl); rewrite Heqx in Hneqx. inversion Hneqx. -- assumption. Qed. -(** ** 2.2 Using a mesure +(** ** 2.2 Using a measure + + The size method described above is particular case of a more general scheme + that consist in using a measure: that is a function depending on + the arguments to [nat], so that it decrease in each recursive call. - For an example, consider a [gcd] function that does not require the assumption that - [x > y] as below, by first checking if [x] or [y] is [0], and otherwise + For an example, consider a [gcd] function that does not require the assumption + that [x > y], by first checking if [x] or [y] is [0], and otherwise compare [x] and [y], and recall [gcd] with [x - y] or [y - x] depending which is the greater. - 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]. *) + We can not prove it is terminating either by looking if [x] or [y] decrease + (the size of a number is the number itsefl) as we don't know upahead which + of [x] or [y] is bigger. + However, we can use that the measure [x + y] is decreasing for the usual + well-founded order on [nat], as if [x] and [y] are strictly greater than [0], + than [x + y > x + (y - x) = y] and [x + y > y + (x - y) = y]. + + We can define [gcd] by well-founded recursion by adding [wf (x + y) lt]. + We then get two obligations corresponding to the recursive goals, which + are basic arithmetic goals and can be solved using [lia]. + +*) Equations? gcd (x y : nat) : nat by wf (x + y) lt := gcd 0 x := x ; @@ -282,8 +316,8 @@ gcd x y with gt_eq_gt_dec x y := { | inleft (right refl) := x ; | inright _ := gcd (x - y) y }. Proof. -lia. lia. -Abort. + all: lia. +Defined. (** For further examples of how functional elimination works on well-founded recursion and how useful it is on complex definitions, we will now show a @@ -292,21 +326,17 @@ Abort. Lemma gcd_same x : gcd x x = x. Proof. - funelim (gcd x x); try lia. reflexivity. + funelim (gcd x x). all: try lia. reflexivity. Qed. Lemma gcd_spec0 a : gcd a 0 = a. Proof. - funelim (gcd a 0); reflexivity. + funelim (gcd a 0). all: 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. +Admitted. Lemma gcd_spec1 a b: 0 <> b -> gcd a b = gcd (Nat.modulo a b) b. Proof. @@ -314,84 +344,91 @@ Proof. - now rewrite Nat.Div0.mod_0_l. - reflexivity. - now rewrite (Nat.mod_small (S n) (S n0)). - - simp gcd; rewrite Heq; simp gcd. + - rewrite <- Heqcall. rewrite refl, Nat.Div0.mod_same. reflexivity. - - simp gcd; rewrite Heq; simp gcd. - rewrite H; auto. rewrite mod_minus; auto. + - rewrite <- Heqcall. rewrite H; auto. + rewrite mod_minus; auto. Qed. - (** ** 2.3 Using a lexicographic order - Let's now consider the Ackerman function which is decreasing according to - the usual lexicographic order on [nat * nat], [(<,<)] which is accessible - as [<] is, and the lexicographic combination of well-founded relations is too. - You can define the lexicographic order and automatically derive a proof - it is well-founded using the function [Equations.Prop.Subterm.lexprod]. - As we can see, with this order, once again no obligations are left to prove as - Coq can prove on its own that [(m, (ack (S m) n)) A -> Prop] and [ B -> Prop], + [(a,b) option A] that for any [(a :A)] - return a strictly smaller element if there is one. + returns [None] or a strictly smaller element. This situation is axiomatised by the following context : *) @@ -420,13 +457,12 @@ 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]. +(** In this case, given an element (a : A), we may be interested in computing + the decreasing chain starting from [a] specified by [f]. 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 return [p] added to the - chain starting with [p], i.e., our recursive call [f_sequence p], and otherwise + with a [with] clause, if there is one [Some p] then return [p] added to the + chain starting with [p], i.e. added to [f_sequence p], and otherwise stop the computation. *) From c51538c288d8587a10425d0956a6f58bda7a26cf Mon Sep 17 00:00:00 2001 From: Thomas Lamiaux <85848641+thomas-lamiaux@users.noreply.github.com> Date: Mon, 10 Jun 2024 18:13:24 +0200 Subject: [PATCH 17/34] Apply suggestions from code review Co-authored-by: Meven Lennon-Bertrand <58942857+MevenBertrand@users.noreply.github.com> --- src/Tutorial_Equations_Obligations.v | 41 +++++++++++++++------------- 1 file changed, 22 insertions(+), 19 deletions(-) diff --git a/src/Tutorial_Equations_Obligations.v b/src/Tutorial_Equations_Obligations.v index 4c71a22..8f7104a 100644 --- a/src/Tutorial_Equations_Obligations.v +++ b/src/Tutorial_Equations_Obligations.v @@ -111,24 +111,24 @@ Next Obligation. apply app_length. Qed. -(** As you can see, this very pratical however, you should be aware of - three basic pitfalls that: +(** As you can see, this is very practical, however, you should be aware of + three basic pitfalls: 1. As you may have noticed the goal to prove was not [length (app ln lm) = n + m] as expected, but [length (app ln lm) = length ln + length lm]. - It is because [Equations] custom solving tactic has already pre-simplified + This is because [Equations]' custom solving tactic has already pre-simplified the goal for us. In can be an issue in some cases, and we discuss it in section 2.1. 2. Technically, you can use a wildcard [_] for any term, even for one relevant to the definition and computation like [app ln lm] . - Yet, it generally it is a bad idea as automation could then infer + Yet, it is generally a bad idea as automation could then infer something random that matches the type expected. - 3. Be aware that a definition is not defined until the all its associated + 3. Be aware that a definition is not defined until all its associated obligations have been solved. Trying to refer to it before that, we consequently return that the defintion was not found. - For instance, consider the unfinished definition of [vmap] with a wildcar [_] + For instance, consider the unfinished definition of [vmap] with a wildcard [_] *) Equations vmap {A B n} (f : A -> B) (v : vec A n) : vec B n := @@ -144,7 +144,7 @@ Fail Definition vmap_comp {A B C n} (g : B -> C) (f : A -> B) (v : vec A n) You can solve the obligations one by one using the command [Next Obligations]. Doing so for [vmap] display the goal [length (map f ln) = length ln], - which we can then solve using tactics.. + which we can then solve using tactics. *) Next Obligation. @@ -153,7 +153,7 @@ Qed. (** Using [Next Obligation] has the advantage that once an obligation has been solved, [Program] retries automatically to prove the remaining obligations. - It can be practical when proofs are simple but requires for a evariable + It can be practical when proofs are simple but requires for a variable to be solved first to be able to proceed. Note, that it can be useful to add [Fail Next Obligation] once all @@ -177,8 +177,8 @@ Defined. (** Though, note that [Equations?] triggers a warning when used on a definition that leaves no obligations unsolved. It is because for technical reasons, [Equations?] cannot check if there - is at least on obligation left to solve before opening the proof mode. - Hence, when there is no obligation proof mode is open for nothing, and + is at least one obligation left to solve before opening the proof mode. + Hence, when there is no obligation proof mode is opened for nothing, and has to be closed by hand using [Qed] or [Defined] as it can be seen below. As it is easy to forget, a warning is raised. *) @@ -190,7 +190,7 @@ Defined. (** ** 2. Equations' solving tactic - As mentioned, [Equations] automatically tried to solve obligations. + As mentioned, [Equations] automatically tries to solve obligations. It does so using a custom strategy basically simplifying the goals and running a solver. It can be viewed with the following command: @@ -202,13 +202,13 @@ Show Obligation Tactic. When working, it is common to be dealing with a particular class of functions that shares a common theory, e.g, they involve basic arithmetic. - This theory cannot not be guessed from the basic automation tactic, - so may be personalizing a tactic to handle this particular theory. + This theory cannot not be guessed by the basic automation tactic, + so one may want a personalized tactic to handle a particular theory. This can be done using the command [ #[local] Obligation Tactic := tac ] - that changes locally the tactic solving obligation to [tac]. + that locally changes the tactic solving obligation to [tac]. - For an example, consider a [gcd] function defined by well-founded recursion. + For example, consider a [gcd] function defined by well-founded recursion. There are two obligations left to prove corresponding to proofs that the recursive call are indeed performed on smaller instance. Each of them corresponds to basic reasoning about arithmetics, and can @@ -229,7 +229,7 @@ Proof. Abort. (** Therefore, we would like to locally change the tactic solving the - obligations to take into account arithmetic, and try [lia]. + obligations to take into account arithmetic, and try the [lia] tactic. We do so by simply trying it after the current solving tactic, i.e. the one displayed by [Show Obligation Tactic]. As we can see by running again [Show Obligation Tactic], it has indeed been @@ -257,10 +257,13 @@ gcd x y with gt_eq_gt_dec x y := { (** 2.2 What to do if goals are oversimplified In some cases, it can happen that [Equations]' solving tactic is too abrut - and oversimply goals, or mis-specialised and ended up getting us stuck. - In this case, it can be useful to set the solving tactic to the identify. + and oversimplies goals, or mis-specialised and ends up getting us stuck. + The automation can also become slow, and one might want to diagnose this. + In any of these cases, it can be useful to set the solving tactic to the identity. + That way, the obligation one gets is the raw one generated by [Equations] + without processing, which can then be "manually" explored. - For an example, let's define a function + For example, let us define a function [vzip : vec A n -> vec B n -> vec (A * B) n] without using [list_prod]. In all cases where a proof is expected we create an obligation, and uses the proof mode to handle the reasoning on arithmetics. From 5e872635b2871b59b19d1d8a5de526d58b701fdd Mon Sep 17 00:00:00 2001 From: thomas-lamiaux Date: Mon, 10 Jun 2024 18:13:41 +0200 Subject: [PATCH 18/34] typos --- src/Tutorial_Equations_Obligations.v | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/Tutorial_Equations_Obligations.v b/src/Tutorial_Equations_Obligations.v index 4c71a22..d169319 100644 --- a/src/Tutorial_Equations_Obligations.v +++ b/src/Tutorial_Equations_Obligations.v @@ -89,13 +89,13 @@ vapp (exist _ ln Hn) (exist _ lm Hm) := Therefore, we would much rather like to build our terms using the proof mode. This is exactly what [Program] and obligations enables us to do. - At every point in a definition, it enables us: - - 1. write down a wildcard [_] instead of a term - - 2. it will then create an obligation, intuitively a goal left to solve + At every point in a definition, it allows us to write down a wildcard [_] instead of a term, + it will then: + - 1. create an obligation, intuitively a goal left to solve to complete the definition - - 3. it will try to simplify the obligations and solve them using a tactic, + - 2. try to simplify the obligations and solve them using a tactic, in our case, using a tactic specific to [Equations] - - 4. if they are any obligations left to solve, we can prove them using + - 3. if they are any obligations left to solve, enable us to prove them using the proof mode and tactics using [Next Obligation] or [Equations?] that we discuss in section 1.2 @@ -127,7 +127,7 @@ Qed. 3. Be aware that a definition is not defined until the all its associated obligations have been solved. Trying to refer to it before that, we - consequently return that the defintion was not found. + consequently trigger the error the defintion was not found. For instance, consider the unfinished definition of [vmap] with a wildcar [_] *) From 6c6b586c90cc471eff002d5ed86e213bec380f18 Mon Sep 17 00:00:00 2001 From: thomas-lamiaux Date: Mon, 10 Jun 2024 22:22:57 +0200 Subject: [PATCH 19/34] add example linear search --- src/Tutorial_Equations_wf.v | 106 +++++++++++++++++++++++++++++++++++- 1 file changed, 104 insertions(+), 2 deletions(-) diff --git a/src/Tutorial_Equations_wf.v b/src/Tutorial_Equations_wf.v index efa1e04..deb483d 100644 --- a/src/Tutorial_Equations_wf.v +++ b/src/Tutorial_Equations_wf.v @@ -429,9 +429,111 @@ Proof. Qed. - (** ** 2.4 Using a custom well-founded relation *) +(** ** 2.4 Using a custom well-founded relation + + In some cases, there is no basic order that easily enables to define a + function by well-founded recursion. + In this case, it can be interresting to: + - 1. Define your own relation [R : A -> A -> Prop] + - 2. Prove it is well-founded [wf_R : well_founded R] + - 3. Declare it as an instance so that Equations can find it with + [Instance name : WellFounded R := wf_R]. + + For instance, suppose we have an infinite sequence [f : nat -> bool] of booleans, + such that we know logically that there is at least one that is true + [h : exists n : nat, f n = true]. + This is represented by this context: + *) + + Section LinearSearch. + + Context (f : nat -> bool). + Context (h : exists n : nat, f n = true). + +(** Knowing there is an [n : nat] such that [f n = true], we would like to + actually compute one. + Intuitively, we should be able to just try them one by one starting from 0 + until we find one, and it should terminate as we know there exists one. + However, it is not clear which classical meseaure or order to use to + justify this idea. We will hence use a custom one. + + We define a relation [R : nat -> nat -> nat] such that [n] is "smaller" than + "m" when [n = 1 + m] and that all booleans before [m] are [false], + i.e [forall k, k <= m -> f k = false]. +*) + + Definition R n m := (forall k, k <= m -> f k = false) /\ n = S m. + +(** Knowing that the previous booleans have been [false] enables us to prove + that [R] is well-founed when combined with [h]. + We ommit the proof here because it is a bit long, and not very interresting + for our purpose. + *) + + Lemma wf_R : (exists n : nat, f n = true) -> well_founded R. + Proof. + Admitted. + +(** Having proven it is well-founded, we declare it as an instance of the database + [WellFounded] so that [Equations] can find it automaticaly when using the + keyword [wf x R]. +*) + + Instance wfR : WellFounded R := wf_R h. + +(** We are not ready to define our function by well-founded recursion. + Though, we want to start a computation, to define our function by well-founded + recursion we need to start at a generic point [m : nat], to actually have + an object to do a recursion on. + + Here, for technical reason we use the [inspect] method to remember the value of [f m]. + Here, it is not necessary to understand it for our purpose, and we refer to + section 2.1 for more details on the method. + *) + + Definition inspect {A} (a : A) : {b | a = b} := exist _ a eq_refl. + + Notation "x 'eqn:' p" := (exist _ x p) (only parsing, at level 20). + + Equations? exists_nat (m : nat) (H : forall n, n < m -> f n = false) : + {n : nat | f n = true} by wf m R := + exists_nat m H with inspect (f m) :={ + | true eqn:p => (exist _ m p) + | false eqn:p => exists_nat (S m) _ + }. + Proof. + - inversion H0; auto. + - unfold R. split. 2: reflexivity. + intros k ikm. inversion ikm. 1: assumption. + subst. apply H. auto with arith. + Qed. + + Theorem linear_search : {n : nat | f n = true}. + Proof. + unshelve eapply (exists_nat 0). + intros n Hn0; inversion Hn0. + Qed. + +End LinearSearch. + + + + (** EXERCISE + + Deduce the theorem from it. + + **) + + Theorem linear_search : + (exists n : nat, f n = true) -> {n : nat | f n = true}. + Proof. + intros h. + eapply exists_nat with (m := 0). + - assumption. + - intuition lia. + Qed. - (* ### TODO ### *) +End LinearSearch. (** ** 2.5 Using the subterm relation *) From 6554b539f925e8daa72162599e232d8aa72459b5 Mon Sep 17 00:00:00 2001 From: thomas-lamiaux Date: Tue, 11 Jun 2024 20:00:51 +0200 Subject: [PATCH 20/34] some work --- src/Tutorial_Equations_Obligations.v | 59 +++++++++++++------- src/Tutorial_Equations_wf.v | 83 +++++++++++++++++++--------- 2 files changed, 95 insertions(+), 47 deletions(-) diff --git a/src/Tutorial_Equations_Obligations.v b/src/Tutorial_Equations_Obligations.v index 566f316..a62e57b 100644 --- a/src/Tutorial_Equations_Obligations.v +++ b/src/Tutorial_Equations_Obligations.v @@ -259,47 +259,64 @@ gcd x y with gt_eq_gt_dec x y := { In some cases, it can happen that [Equations]' solving tactic is too abrut and oversimplies goals, or mis-specialised and ends up getting us stuck. The automation can also become slow, and one might want to diagnose this. - In any of these cases, it can be useful to set the solving tactic to the identity. - That way, the obligation one gets is the raw one generated by [Equations] - without processing, which can then be "manually" explored. + In any of these cases, it can be useful to set the solving tactic locally to the identity. + That way, the obligations one gets is the raw ones generated by [Equations] + without preprocessing, which can then be "manually" explored. - For example, let us define a function - [vzip : vec A n -> vec B n -> vec (A * B) n] without using [list_prod]. + + ### THAT IS NOT A GOOD EXAMPLE ! FIND SOMETHIGN BETTER + + + + As it is not easy to provide a minimal working example, we are going to + voluntarily use a badly coded one. + + Let us define a function [vzip : vec A n -> vec B n -> vec (A * B) n] without using [list_prod] + nor matching directly on [n]. In all cases where a proof is expected we create an obligation, and uses the proof mode to handle the reasoning on arithmetics. We also use obligations to disregard the case [nil (b::lb)] and [(a::la) nil]. As it can be seen below, [Equations] can automatically with the first three goal, and first ask us which integer is used [n] the first. - TODO ?? *) +Arguments exist [_] {_} _ _. + Equations? vzip {A B n} (va : vec A n) (vb : vec B n) : vec (A * B) n := - vzip (exist _ [] ea) (exist _ [] eb) => exist _ [] _; - vzip (exist _ [] ea) (exist _ (b::lb) eb) => _; - vzip (exist _ (a::la) ea) (exist _ [] eb) => _; - vzip (exist _ (a::la) ea) (exist _ (b::lb) eb) - with vzip (exist _ la _) (exist _ lb _ ) := { - | exist _ l _ => exist _ ((a,b)::l) _ + vzip (exist [] ea) (exist [] eb) => exist [] _; + vzip (exist [] ea) (exist (b::lb) eb) => _; + vzip (exist (a::la) ea) (exist [] eb) => _; + vzip (exist (a::la) ea) (exist (b::lb) eb) + with vzip (exist la _) (exist lb _ ) := { + | exist l _ => exist ((a,b)::l) _ }. Proof. - - exact (length lb). - - + - (* n has been automatically substituted by Equations and is no + longer accessible,so we do the recall on [length b] instead *) + exact (length lb). + - now destruct H. + - now destruct H. + - destruct H; cbn in *. auto. + (* It is not accepted by the guard condition because we lost on the way + the link between [n] and [length lb] *) + Fail Defined. Abort. (** Consequently, it can be easier to change the tactic locally to TODO *) #[local] Obligation Tactic := idtac. -Equations? vzip {A B n} (va : vec A n) (vb : vec B n) : vec (A * B) n := -vzip (exist _ [] ea) (exist _ [] eb) => exist _ [] _; -vzip (exist _ [] ea) (exist _ (b::lb) eb) => _; -vzip (exist _ (a::la) ea) (exist _ [] eb) => _; -vzip (exist _ (a::la) ea) (exist _ (b::lb) eb) - with vzip (exist _ la _) (exist _ lb _ ) := { - | exist _ l _ => exist _ ((a,b)::l) _ +#[tactic="idtac"] Equations? vzip {A B n} (va : vec A n) (vb : vec B n) : vec (A * B) n := +vzip (exist [] ea) (exist [] eb) => exist [] _; +vzip (exist [] ea) (exist (b::lb) eb) => False_rect _ _; +vzip (exist (a::la) ea) (exist [] eb) => False_rect _ _ ; +vzip (n := S n) (exist (a::la) ea) (exist (b::lb) eb) + with vzip (exist la _) (exist lb _ ) := { + | exist l _ => exist ((a,b)::l) _ }. Proof. + all: try auto. - exact ea. - cbn in *. rewrite <- ea in eb; inversion eb. - cbn in *. rewrite <- ea in eb; inversion eb. diff --git a/src/Tutorial_Equations_wf.v b/src/Tutorial_Equations_wf.v index deb483d..ed5ccce 100644 --- a/src/Tutorial_Equations_wf.v +++ b/src/Tutorial_Equations_wf.v @@ -445,7 +445,7 @@ Qed. This is represented by this context: *) - Section LinearSearch. + Module LinearSearch. Context (f : nat -> bool). Context (h : exists n : nat, f n = true). @@ -482,9 +482,6 @@ Qed. Instance wfR : WellFounded R := wf_R h. (** We are not ready to define our function by well-founded recursion. - Though, we want to start a computation, to define our function by well-founded - recursion we need to start at a generic point [m : nat], to actually have - an object to do a recursion on. Here, for technical reason we use the [inspect] method to remember the value of [f m]. Here, it is not necessary to understand it for our purpose, and we refer to @@ -495,6 +492,11 @@ Qed. Notation "x 'eqn:' p" := (exist _ x p) (only parsing, at level 20). +(** Though, we want to start a computation at 0, to define our function + by well-founded recursion we need to start at a generic point [m : nat], + to actually have a term to do our recursion on: +*) + Equations? exists_nat (m : nat) (H : forall n, n < m -> f n = false) : {n : nat | f n = true} by wf m R := exists_nat m H with inspect (f m) :={ @@ -516,27 +518,9 @@ Qed. End LinearSearch. - - - (** EXERCISE - - Deduce the theorem from it. - - **) - - Theorem linear_search : - (exists n : nat, f n = true) -> {n : nat | f n = true}. - Proof. - intros h. - eapply exists_nat with (m := 0). - - assumption. - - intuition lia. - Qed. - -End LinearSearch. - (** ** 2.5 Using the subterm relation *) +(* TODO *) (** ** 3. Different methods to work with well-founded recursion @@ -544,7 +528,9 @@ End LinearSearch. When defining a function, it can happen that we loose information relevant to termination when matching a value, and that we then get stuck trying to prove termination. + In this section, we discuss two such example an methods to go around the issue. + Note, the inspect method was already used in section 2.4. *** 3.1 The inspect method @@ -554,7 +540,7 @@ End LinearSearch. This situation is axiomatised by the following context : *) -Section Inspect. +Module 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). @@ -608,14 +594,59 @@ Section Inspect. to fill. *) - Equations f_sequence (a : A) : list A by wf a lt := + 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 }. + Proof. + apply decr_f. assumption. + Qed. End Inspect. (** 2.2 ### TODO ### -*) \ No newline at end of file +*) + +Section Map_in. + Context {A : Type}. + (* Context (eq : A -> A -> bool). *) + + Inductive RoseTree : Type := + | leaf : A -> RoseTree + | node : list RoseTree -> RoseTree. + + Equations sizeRT (t : RoseTree) : nat := + sizeRT (leaf a) := 1; + sizeRT (node l) := 1 + list_sum (map sizeRT l). + + Equations eqList {X} (l l' : list X) (eq : forall x : X, In x l -> X -> bool) : bool := + eqList [] [] _ := true; + eqList (a::l) (a'::l') eq := andb (eq a _ a') (eqList l l' (fun x Inl y => eq x _ y)); + eqList _ _ _ := false. + + + Definition list_sum_ine (x : nat) (l : list nat) : In x l -> x < 1 + list_sum l. + Admitted. + + #[tactic="idtac"] Equations? eqRT (eq : A -> A -> bool) (t t': RoseTree) : bool by wf (sizeRT t) lt := + eqRT eq (leaf a) (leaf a') := eq a a'; + eqRT eq (node l) (node l') := eqList l l' (fun l Inl l' => eqRT eq l l') ; + eqRT eq _ _ := false. + Proof. + simp sizeRT. apply list_sum_ine. apply in_map. assumption. + Qed. + + Equations? filterRT (p : RoseTree -> bool) (t : RoseTree) : RoseTree := + filterRT p (leaf a) with p (leaf a) := { + | true => leaf a + | false => node [] + }; + filterRT p (node l) := node (filter p l). + Defined. + + Equations? nubByRT (eq : A -> A -> bool) (t : RoseTree) : RoseTree := + nubByRT eq (leaf a) := leaf a; + nubByRT eq (node l) := node (nubBy (fun x y => negb (eqRT eq x y)) l). + Defined. \ No newline at end of file From c2dbc807892803a812cd6ed9dec507c673de0c89 Mon Sep 17 00:00:00 2001 From: thomas-lamiaux Date: Tue, 11 Jun 2024 22:52:49 +0200 Subject: [PATCH 21/34] added comments printing obligations --- src/Tutorial_Equations_Obligations.v | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/src/Tutorial_Equations_Obligations.v b/src/Tutorial_Equations_Obligations.v index a62e57b..245b564 100644 --- a/src/Tutorial_Equations_Obligations.v +++ b/src/Tutorial_Equations_Obligations.v @@ -89,8 +89,8 @@ vapp (exist _ ln Hn) (exist _ lm Hm) := Therefore, we would much rather like to build our terms using the proof mode. This is exactly what [Program] and obligations enables us to do. - At every point in a definition, it allows us to write down a wildcard [_] instead of a term, - it will then: + At every point in a definition, it allows us to write down a wildcard [_] + instead of a term, it will then: - 1. create an obligation, intuitively a goal left to solve to complete the definition - 2. try to simplify the obligations and solve them using a tactic, @@ -137,6 +137,12 @@ vmap f (exist _ ln Hn) := exist _ (map f ln) _ . Fail Definition vmap_comp {A B C n} (g : B -> C) (f : A -> B) (v : vec A n) : vmap g (vmap f n v) = vmap (fun x => g (f x)) v. +(** Obligations are not well displayed by all IDE. If it the case, you can always + print them using [Obligations of name_obligations]. + For instance, for [vmap]: +*) +Obligations of vmap_obligations. + (** *** 1.2 Solving obligations @@ -179,7 +185,7 @@ Defined. It is because for technical reasons, [Equations?] cannot check if there is at least one obligation left to solve before opening the proof mode. Hence, when there is no obligation proof mode is opened for nothing, and - has to be closed by hand using [Qed] or [Defined] as it can be seen below. + has to be closed by hand using [Qed] (for proof irrelevant content) as it can be seen below. As it is easy to forget, a warning is raised. *) From 7fa2b6454b20e14304cd7cc2464e291c86f993d5 Mon Sep 17 00:00:00 2001 From: thomas-lamiaux Date: Tue, 11 Jun 2024 23:12:41 +0200 Subject: [PATCH 22/34] edits 2.2 --- src/Tutorial_Equations_Obligations.v | 69 +++------------------------- 1 file changed, 7 insertions(+), 62 deletions(-) diff --git a/src/Tutorial_Equations_Obligations.v b/src/Tutorial_Equations_Obligations.v index 245b564..833a445 100644 --- a/src/Tutorial_Equations_Obligations.v +++ b/src/Tutorial_Equations_Obligations.v @@ -118,7 +118,7 @@ Qed. as expected, but [length (app ln lm) = length ln + length lm]. This is because [Equations]' custom solving tactic has already pre-simplified the goal for us. In can be an issue in some cases, and we discuss it in - section 2.1. + section 2.2. 2. Technically, you can use a wildcard [_] for any term, even for one relevant to the definition and computation like [app ln lm] . @@ -269,65 +269,10 @@ gcd x y with gt_eq_gt_dec x y := { That way, the obligations one gets is the raw ones generated by [Equations] without preprocessing, which can then be "manually" explored. + In this case, a useful trick is to use an attribute to set the obligation + tactic to [idtac] only for the definition at hand, using the scheme + [ #[tactic="idtac"] Equations? name ...]. - ### THAT IS NOT A GOOD EXAMPLE ! FIND SOMETHIGN BETTER - - - - As it is not easy to provide a minimal working example, we are going to - voluntarily use a badly coded one. - - Let us define a function [vzip : vec A n -> vec B n -> vec (A * B) n] without using [list_prod] - nor matching directly on [n]. - In all cases where a proof is expected we create an obligation, and uses - the proof mode to handle the reasoning on arithmetics. - We also use obligations to disregard the case [nil (b::lb)] and [(a::la) nil]. - - As it can be seen below, [Equations] can automatically with the first three - goal, and first ask us which integer is used [n] the first. -*) - -Arguments exist [_] {_} _ _. - - Equations? vzip {A B n} (va : vec A n) (vb : vec B n) : vec (A * B) n := - vzip (exist [] ea) (exist [] eb) => exist [] _; - vzip (exist [] ea) (exist (b::lb) eb) => _; - vzip (exist (a::la) ea) (exist [] eb) => _; - vzip (exist (a::la) ea) (exist (b::lb) eb) - with vzip (exist la _) (exist lb _ ) := { - | exist l _ => exist ((a,b)::l) _ - }. - Proof. - - (* n has been automatically substituted by Equations and is no - longer accessible,so we do the recall on [length b] instead *) - exact (length lb). - - now destruct H. - - now destruct H. - - destruct H; cbn in *. auto. - (* It is not accepted by the guard condition because we lost on the way - the link between [n] and [length lb] *) - Fail Defined. - Abort. - - -(** Consequently, it can be easier to change the tactic locally to TODO *) -#[local] Obligation Tactic := idtac. - -#[tactic="idtac"] Equations? vzip {A B n} (va : vec A n) (vb : vec B n) : vec (A * B) n := -vzip (exist [] ea) (exist [] eb) => exist [] _; -vzip (exist [] ea) (exist (b::lb) eb) => False_rect _ _; -vzip (exist (a::la) ea) (exist [] eb) => False_rect _ _ ; -vzip (n := S n) (exist (a::la) ea) (exist (b::lb) eb) - with vzip (exist la _) (exist lb _ ) := { - | exist l _ => exist ((a,b)::l) _ - }. -Proof. - all: try auto. - - exact ea. - - cbn in *. rewrite <- ea in eb; inversion eb. - - cbn in *. rewrite <- ea in eb; inversion eb. - - destruct n. 1: inversion ea. exact n. - - destruct n; inversion ea. reflexivity. - - destruct n; inversion eb. reflexivity. - - destruct n; inversion ea. cbn. rewrite e, H0. reflexivity. -Defined. \ No newline at end of file + Unfortunately, at the moment we do not have a simple enough minimal working + example. If you have one, do not hesitate to create a PR. +*) \ No newline at end of file From 01761ff81a52712e1c80300f46e3e0f669d70e1a Mon Sep 17 00:00:00 2001 From: thomas-lamiaux Date: Wed, 12 Jun 2024 03:54:12 +0200 Subject: [PATCH 23/34] content section 2.2 --- src/Tutorial_Equations_wf.v | 79 ++++++++++++++++++++++++++----------- 1 file changed, 57 insertions(+), 22 deletions(-) diff --git a/src/Tutorial_Equations_wf.v b/src/Tutorial_Equations_wf.v index ed5ccce..90ced76 100644 --- a/src/Tutorial_Equations_wf.v +++ b/src/Tutorial_Equations_wf.v @@ -24,10 +24,9 @@ 2.2 Using a measure 2.3 Using a lexicographic order 2.4 Using a custom well-founded relation - 2.5 Using the subterm relation ??? - 3. Different tricks to work with well-founded recursion - 3.1 The inspect method - - 3.2 map thing ??? + - 3.2 Improving recursion hypotheses *** Prerequisites @@ -606,12 +605,23 @@ Module Inspect. End Inspect. -(** 2.2 ### TODO ### +(** 2.2 Improving recursion hypotheses + + In some cases, most particularly when using a size or measure, + it can happen that when defining a function by well-founded recursion, + we forget that [x] is a subterm of a larger term [Y], + and then we get stuck proving that "[size x < size Y]". + In this case, a possible solution is to define a custom function to "carry" + the information that [x] is a subterm of [Y], so it is available when + trying to prove it is well-founded. + + For an example, consider RoseTrees, trees with finite subtrees represented + by the constructor [node : list RoseTree -> RoseTree.] + Let's also define the usual size function on it, and an equality test on lists. *) Section Map_in. Context {A : Type}. - (* Context (eq : A -> A -> bool). *) Inductive RoseTree : Type := | leaf : A -> RoseTree @@ -621,32 +631,57 @@ Section Map_in. sizeRT (leaf a) := 1; sizeRT (node l) := 1 + list_sum (map sizeRT l). - Equations eqList {X} (l l' : list X) (eq : forall x : X, In x l -> X -> bool) : bool := + Equations eqList {X} (l l' : list X) (eq : X -> X -> bool) : bool := eqList [] [] _ := true; - eqList (a::l) (a'::l') eq := andb (eq a _ a') (eqList l l' (fun x Inl y => eq x _ y)); + eqList (a::l) (a'::l') eq := andb (eq a a') (eqList l l' eq); eqList _ _ _ := false. +(** Having define an equality test on list, we would like to define an equality + test on RoseTree. + For technical reasons, the straigthfoward definition is not accepted by Coq + before Coq v8.20, so we need well-founded recursion on the size of RoseTress + to define the equality test. + if you are using a subsequent version, assume you need it for pedagogical purposes. + + If we try to define the equality test naively as below, [Equations] generates + the obligation [sizeRT l < 1 + list_sum (map sizeRT lt0)] corresponding to + the case where [lt := l :: _]. + This is obviously true, but we are stuck trying to prove it as we do not + remember that [l] in in [lt]: +*) + + Equations? eqRT (eq : A -> A -> bool) (t t': RoseTree) : bool by wf (sizeRT t) lt := + eqRT eq (leaf a) (leaf a') := eq a a'; + eqRT eq (node lt) (node lt') := eqList lt lt' (fun l l' => eqRT eq l l') ; + eqRT eq _ _ := false. + Proof. + simp sizeRT. + (* What to do know ? We have forgotten that x is in l, + and hence that sizeRT l < 1 + list_sum (map sizeRT l0) *) + Abort. + +(** To go around this kind of issues, a general method is to strengthen the + function that goes through the structure to remember that [x] in a subterm of [Y]. + In our case, it means stengthening [eqList] so that to remember that [l] is + a subterm of [lt0], i.e. that [l] is in [lt0]. + To do so, we ask for the input of the equality test [eq] of [eqList] + to adittionaly be in in [l], i.e. [eq : forall x : X, In x l -> X -> bool]. + This way, in the case (lt0 := l :: _) we rememeber [In l lt0]. + Doing so, it is now possible to define [eqRT] by well-founded on the size: +*) + + Equations eqList' {X} (l l' : list X) (eq : forall x : X, In x l -> X -> bool) : bool := + eqList' [] [] _ := true; + eqList' (a::l) (a'::l') eq := andb (eq a _ a') (eqList' l l' (fun x Inl y => eq x _ y)); + eqList' _ _ _ := false. Definition list_sum_ine (x : nat) (l : list nat) : In x l -> x < 1 + list_sum l. Admitted. - #[tactic="idtac"] Equations? eqRT (eq : A -> A -> bool) (t t': RoseTree) : bool by wf (sizeRT t) lt := + Equations? eqRT (eq : A -> A -> bool) (t t': RoseTree) : bool by wf (sizeRT t) lt := eqRT eq (leaf a) (leaf a') := eq a a'; - eqRT eq (node l) (node l') := eqList l l' (fun l Inl l' => eqRT eq l l') ; + eqRT eq (node lt) (node lt') := eqList' lt lt' (fun l Inl l' => eqRT eq l l') ; eqRT eq _ _ := false. Proof. simp sizeRT. apply list_sum_ine. apply in_map. assumption. - Qed. - - Equations? filterRT (p : RoseTree -> bool) (t : RoseTree) : RoseTree := - filterRT p (leaf a) with p (leaf a) := { - | true => leaf a - | false => node [] - }; - filterRT p (node l) := node (filter p l). - Defined. - - Equations? nubByRT (eq : A -> A -> bool) (t : RoseTree) : RoseTree := - nubByRT eq (leaf a) := leaf a; - nubByRT eq (node l) := node (nubBy (fun x y => negb (eqRT eq x y)) l). - Defined. \ No newline at end of file + Qed. \ No newline at end of file From 4fa0bcf091e852d2f072680dc313d3e3cdc817e5 Mon Sep 17 00:00:00 2001 From: thomas-lamiaux Date: Wed, 12 Jun 2024 03:55:07 +0200 Subject: [PATCH 24/34] removed section 2.2 by lack of example --- src/Tutorial_Equations_wf.v | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/src/Tutorial_Equations_wf.v b/src/Tutorial_Equations_wf.v index 90ced76..15c5d35 100644 --- a/src/Tutorial_Equations_wf.v +++ b/src/Tutorial_Equations_wf.v @@ -517,10 +517,6 @@ Qed. End LinearSearch. -(** ** 2.5 Using the subterm relation *) - -(* TODO *) - (** ** 3. Different methods to work with well-founded recursion @@ -605,7 +601,7 @@ Module Inspect. End Inspect. -(** 2.2 Improving recursion hypotheses +(** 3.2 Improving recursion hypotheses In some cases, most particularly when using a size or measure, it can happen that when defining a function by well-founded recursion, From c70a734703caf0c6e2a2c2fe12bcc926b9686c3a Mon Sep 17 00:00:00 2001 From: thomas-lamiaux Date: Wed, 12 Jun 2024 05:21:05 +0200 Subject: [PATCH 25/34] typos --- src/Tutorial_Equations_wf.v | 42 ++++++++++++++++++------------------- 1 file changed, 21 insertions(+), 21 deletions(-) diff --git a/src/Tutorial_Equations_wf.v b/src/Tutorial_Equations_wf.v index 15c5d35..7390584 100644 --- a/src/Tutorial_Equations_wf.v +++ b/src/Tutorial_Equations_wf.v @@ -7,12 +7,12 @@ 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 interrests and the principle of well-founded recursion. + In section 1, we explain the interests and the principle of well-founded recursion. We then explain in section 2, how to define functions and how to reason about them using well-founded recursion and [Equations]. In some cases, applying well-founded recursion can fail because information - relevant to termination gets lost during recurion. - In section 3, we discuss two such cases an how to go around the issues. + relevant to termination gets lost during recursion. + In section 3, we discuss two such cases a how to go around the issues. *** Table of content @@ -38,7 +38,7 @@ Not needed: - This tutorial discusses well-founded recursion but no prior knowledge about it is required: we will explain the concept - - To simplify proofs involving arithmetics, we use the automation + - To simplify proofs involving arithmetic, we use the automation tactics [lia] and [auto with arith], but they can be used as black boxes Installation: @@ -69,7 +69,7 @@ Arguments to_fill {_}. *** 1.1 The syntactic guard condition is limited - A commen pitfall is when a recursive call is ofuscated, that is when + A common pitfall is when a recursive call is obfuscated, that is when it is not performed directly on a subterm [x], but on a subterm to which a function has been applied [f x], preventing the syntactic guard from checking that it is still indeed smaller. @@ -77,7 +77,7 @@ Arguments to_fill {_}. For instance, consider the function [nubBy] that given an equality test recursively filters out the duplicates of a list. The recursive call is not performed on the recursive argument [l] but - on the list [filter (fun y => negb (eq x y)) l]. This prevent the syntactic + on the list [filter (fun y => negb (eq x y)) l]. This prevents the syntactic from checking it is indeed smaller, and is hence rejected. Yet, we can prove that [filter] does not increase the size of a list, and hence that the recursive call is indeed performed on a "smaller" instance than [l] @@ -118,7 +118,7 @@ gcd x y H with Nat.eq_dec y 0 => { ### TODO MAKE CLEAN ### - Informally, well-founded recursion bascially amounts to justifying termination by: + Informally, well-founded recursion basically amounts to justifying termination by: - providing a "well-founded" relation [R : A -> A -> Prop], intuitively an order like [<] on natural numbers for which it is impossible to decrease infinitely - proving that all the recursive calls are performed on smaller arguments according @@ -251,8 +251,8 @@ Qed. properties directly according to the pattern of our definition. In particular, we do not have to do proofs by reproducing the proof structure used to prove that the function is well-founded. - It is particularly interresting as it enables to completely hide from the users - , actually you can see no trace of it in the defintion, and to reason about + It is particularly interesting as it enables to completely hide from the users + , actually you can see no trace of it in the definition, and to reason about functions following the recursive call, that is directly as we think about them? This is a very powerful technic that, for instance, enables us to prove in a @@ -295,7 +295,7 @@ Qed. compare [x] and [y], and recall [gcd] with [x - y] or [y - x] depending which is the greater. We can not prove it is terminating either by looking if [x] or [y] decrease - (the size of a number is the number itsefl) as we do not know upahead which + (the size of a number is the number itself) as we do not know up-ahead which of [x] or [y] is bigger. However, we can use that the measure [x + y] is decreasing for the usual well-founded order on [nat], as if [x] and [y] are strictly greater than [0], @@ -356,11 +356,11 @@ Qed. Not all definitions can be proven terminating using a measure and the strict order [<] on [nat]. In some cases, it is more practical to use a different well-founded order. In particular, when a function involves recursion on different arguments but - not all recursive arguments are smaller at once, it can be pratical to use a + not all recursive arguments are smaller at once, it can be practical to use a lexicographic order [ A -> Prop] and [ B -> Prop], [(a,b) A -> Prop] - 2. Prove it is well-founded [wf_R : well_founded R] - 3. Declare it as an instance so that Equations can find it with @@ -453,7 +453,7 @@ Qed. actually compute one. Intuitively, we should be able to just try them one by one starting from 0 until we find one, and it should terminate as we know there exists one. - However, it is not clear which classical meseaure or order to use to + However, it is not clear which classical measure or order to use to justify this idea. We will hence use a custom one. We define a relation [R : nat -> nat -> nat] such that [n] is "smaller" than @@ -464,8 +464,8 @@ Qed. Definition R n m := (forall k, k <= m -> f k = false) /\ n = S m. (** Knowing that the previous booleans have been [false] enables us to prove - that [R] is well-founed when combined with [h]. - We ommit the proof here because it is a bit long, and not very interresting + that [R] is well-founded when combined with [h]. + We omit the proof here because it is a bit long, and not very interesting for our purpose. *) @@ -474,7 +474,7 @@ Qed. Admitted. (** Having proven it is well-founded, we declare it as an instance of the database - [WellFounded] so that [Equations] can find it automaticaly when using the + [WellFounded] so that [Equations] can find it automatically when using the keyword [wf x R]. *) @@ -634,7 +634,7 @@ Section Map_in. (** Having define an equality test on list, we would like to define an equality test on RoseTree. - For technical reasons, the straigthfoward definition is not accepted by Coq + For technical reasons, the straigthforward definition is not accepted by Coq before Coq v8.20, so we need well-founded recursion on the size of RoseTress to define the equality test. if you are using a subsequent version, assume you need it for pedagogical purposes. @@ -658,11 +658,11 @@ Section Map_in. (** To go around this kind of issues, a general method is to strengthen the function that goes through the structure to remember that [x] in a subterm of [Y]. - In our case, it means stengthening [eqList] so that to remember that [l] is + In our case, it means strengthening [eqList] so that to remember that [l] is a subterm of [lt0], i.e. that [l] is in [lt0]. To do so, we ask for the input of the equality test [eq] of [eqList] - to adittionaly be in in [l], i.e. [eq : forall x : X, In x l -> X -> bool]. - This way, in the case (lt0 := l :: _) we rememeber [In l lt0]. + to additionally be in in [l], i.e. [eq : forall x : X, In x l -> X -> bool]. + This way, in the case (lt0 := l :: _) we remember [In l lt0]. Doing so, it is now possible to define [eqRT] by well-founded on the size: *) From 07b975f4fd323273edceb7f6fc5be5674c672ffe Mon Sep 17 00:00:00 2001 From: thomas-lamiaux Date: Wed, 12 Jun 2024 05:58:44 +0200 Subject: [PATCH 26/34] more typos --- src/Tutorial_Equations_Obligations.v | 8 ++++---- src/Tutorial_Equations_wf.v | 14 +++++++------- 2 files changed, 11 insertions(+), 11 deletions(-) diff --git a/src/Tutorial_Equations_Obligations.v b/src/Tutorial_Equations_Obligations.v index 833a445..f9cd2b3 100644 --- a/src/Tutorial_Equations_Obligations.v +++ b/src/Tutorial_Equations_Obligations.v @@ -95,7 +95,7 @@ vapp (exist _ ln Hn) (exist _ lm Hm) := to complete the definition - 2. try to simplify the obligations and solve them using a tactic, in our case, using a tactic specific to [Equations] - - 3. if they are any obligations left to solve, enable us to prove them using + - 3. if there are any obligations left to solve, enable us to prove them using the proof mode and tactics using [Next Obligation] or [Equations?] that we discuss in section 1.2 @@ -120,10 +120,10 @@ Qed. the goal for us. In can be an issue in some cases, and we discuss it in section 2.2. - 2. Technically, you can use a wildcard [_] for any term, even for one - relevant to the definition and computation like [app ln lm] . + 2. Technically, you can use a wildcard [_] for any term, even for one that + is relevant (i.e. not a proof) to the definition and computation like [app ln lm]. Yet, it is generally a bad idea as automation could then infer - something random that matches the type expected. + something random that by concidence happens to match the expected type. 3. Be aware that a definition is not defined until all its associated obligations have been solved. Trying to refer to it before that, we diff --git a/src/Tutorial_Equations_wf.v b/src/Tutorial_Equations_wf.v index 7390584..b4da1da 100644 --- a/src/Tutorial_Equations_wf.v +++ b/src/Tutorial_Equations_wf.v @@ -58,7 +58,7 @@ Arguments to_fill {_}. (** ** 1. Introduction to well-founded recursion For Coq to be consistent, all functions must be terminating. - To ensure they are, Coq checks that they satisfy a complex syntactic + To ensure there are, Coq checks that they satisfy a complex syntactic criterion named the guard condition. Very roughly, the guard condition basically checks that all recursive call are performed on syntactically smaller instance. @@ -230,7 +230,7 @@ Definition gcd_Fix (x y : nat) : nat := for which well-founded relation, here [< := lt], we are doing the well-founded recursion on. An obligation corresponding to proving that the recursive call is smaller, that is [length (filter (fun y => negb (eq x y)) l) < length l], is created. - As [Equations] can not solve on its own, it then left to us to solve. + As [Equations] cannot solve on its own, it then left to us to solve. Using the keyword [Equations?], it is automatically unshelved, and we simply have to prove it using tactics. *) @@ -256,7 +256,7 @@ Qed. functions following the recursive call, that is directly as we think about them? This is a very powerful technic that, for instance, enables us to prove in a - few lines that [nubBy] do remove all duplicates; + few lines that [nubBy] does remove all duplicates; *) Lemma In_nubBy {A} (eq : A -> A -> bool) (l : list A) (a : A) @@ -294,7 +294,7 @@ Qed. that [x > y], by first checking if [x] or [y] is [0], and otherwise compare [x] and [y], and recall [gcd] with [x - y] or [y - x] depending which is the greater. - We can not prove it is terminating either by looking if [x] or [y] decrease + We cannot prove it is terminating either by looking if [x] or [y] decrease (the size of a number is the number itself) as we do not know up-ahead which of [x] or [y] is bigger. However, we can use that the measure [x + y] is decreasing for the usual @@ -544,8 +544,8 @@ Module Inspect. the decreasing chain starting from [a] specified by [f]. 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 return [p] added to the - chain starting with [p], i.e. added to [f_sequence p], and otherwise + with a [with] clause, if there is one [Some p] then returns [p] added to the + chain starting with [p], i.e., our recursive call [f_sequence p], and otherwise stop the computation. *) @@ -559,7 +559,7 @@ Module Inspect. (* What to do now ? *) Abort. -(** Unfortunately, as we can see, doing so we generate an unprovable +(** Unfortunately, as we can see, by doing so we generate an unprovable obligation as we do not remember information about the call to [f n] being equal to [Some p] in the recursive call [f_sequence p]. From 1ef2a483f23a53526f914fa45ea0e3684a155ddf Mon Sep 17 00:00:00 2001 From: thomas-lamiaux Date: Wed, 12 Jun 2024 13:11:27 +0200 Subject: [PATCH 27/34] work 1.2 --- src/Tutorial_Equations_wf.v | 110 +++++++++++++++++++++++------------- 1 file changed, 70 insertions(+), 40 deletions(-) diff --git a/src/Tutorial_Equations_wf.v b/src/Tutorial_Equations_wf.v index b4da1da..8e9c364 100644 --- a/src/Tutorial_Equations_wf.v +++ b/src/Tutorial_Equations_wf.v @@ -51,9 +51,6 @@ From Equations Require Import Equations. From Coq Require Import List Arith Lia. Import ListNotations. -Axiom to_fill : forall A, A. -Arguments to_fill {_}. - (** ** 1. Introduction to well-founded recursion @@ -112,28 +109,58 @@ gcd x y H with Nat.eq_dec y 0 => { (** *** 1.2 Well-founded recursion + **** Informally + It would be limiting if this kind of functions could not be defined. Fortunately, they can be using well-founded recursion. - ### TODO MAKE CLEAN ### - + Informally, defining a function [f] by well-founded recursion basically + amounts to a usual definition expect that we justify termination by: + - Providing a "well-founded" relation [R : A -> A -> Prop], informally a relation + for which there is no infinitely decreasing sequence. + For instance, the strict order on [nat], [< : nat : -> nat -> nat] is well-founded + as starting from [m] it impossible to decrease infinitely, there is a point + at which you must reach [0]. + - Proving that all the recursive calls are performed on smaller arguments + according to [R] + + This enables us to justify termination of our function [f] as it is impossible + to decrease forever and all recrusive call are smaller, so whatever the input [f] + must terminate at a point or another. + + **** More Formally + + Defining a well-founded relation by "no having infinitely decreasing sequence" + is not very useful as #TODO + Consequently, in type theory, we use a slighlty stronger notion, that is + "accessibility", to define a well-founded relations [R : A -> A -> Prop]. + An element [a : A] is accessible for [R], denoted [Acc R a] when for + all [a' : A] smaller than [a], [a'] is itself accessible. + Intuitevely, it ensures constructively that they are no decreasing sequence + as the only ways for an element [a] to be accessible are that: + - 1. There are no elements smaller than [a], so you cannot decrease further + - 2. All elements smaller than [a] are accessible, so there are no infinitely + decreasing sequence from them, and hence from [a]. +*) +Print Acc. - Informally, well-founded recursion basically amounts to justifying termination by: - - providing a "well-founded" relation [R : A -> A -> Prop], intuitively an - order like [<] on natural numbers for which it is impossible to decrease infinitely - - proving that all the recursive calls are performed on smaller arguments according - [R] - More formally, a relation [R : A -> A -> Prop] is "well-founded" when +(** We then say a relation is well-founded, when forall (a : A), [R] is + accessible at [a], i.e. [Acc R a]. + It ensures that wherever we start at, we can not decrease forever. +*) +Print well_founded. - Given a well-founded relation [R : A -> A -> Prop], defining a function +(** Given a well-founded relation [R : A -> A -> Prop], defining a function [f] by well-founded recursion on [a : A] consists in defining [f] assuming that [f] is defined for all [a'] smaller than [a], that is such that [R a' a]. When particularised to natural numbers and [<], this concept is sometimes known as "strong recursion / induction": when defining [f n] one assumes that [f] is defined/proven for all smaller natural numbers [n' < n]. + **** In practice + There are several methods to define functions by well-founded recursion using Coq. They all have their pros and cons, but as a general rules defining functions and reasoning using well-founded recursion can be tedious. @@ -163,22 +190,24 @@ Definition gcd_Fix (x y : nat) : nat := end) y x. - (** However, doing so has several disadvantages. - The function is much less transparent than a usual definition by [Fixpoint] - as: + + The function is much less transparent than a usual definition by [Fixpoint] as: - there is an explicit fixpoint combinator [Fix] in the definition - it forced us to use curryfication and the order of the arguments has changed - - explicit proofs appear in the definition of the function, - here through [gcd_oblig], as we must prove that recursive calls - are indeed smaller. - It can also make it harder to reason about the function, as the recursion scheme is no - longer trivial. - Moreover, as we had to use curryfication in our definition, we may need + - explicit proofs appears directly in the definition of the function (though Program can help) + + Moreover, behind the scene the function is defined by recursion on the + accessibility proof, which forces us in turn to do a recursion on the + accessibility proof to reason about the function. + It makes harder to reason about the function, as the recursion + scheme no longer follow the intuitive definition. + Furthermore, as we had to use curryfication in our definition, we may need the axiom of function extensionally to reason about [gcd_Fix]. - Consequently, Equations provide a built-in mechanism to help us - write functions and reason by well-founded recursion. + + Considering this different defaults, Equations provides a built-in mechanism + to help us write functions and reason by well-founded recursion. *) @@ -186,14 +215,17 @@ Definition gcd_Fix (x y : nat) : nat := To define a function by well-founded recursion with Equations, one must add after the type of the function [by wf x R], where [x] is the term - decreasing, and [R] the well-founded relation for which [x] decreases. + decreasing, and [R] the well-founded relation for which [x] decreases, + and then define the function as usual. For instance, the function [nubBy] terminates as the size of the list decrease in each recursive call according to the usual strict order [<] on [nat], [lt] in Coq. We hence, need to write [wf (size l) l] to define it by well-founded recursion: [[ - Equations nubBy {A} (eq : A -> A -> bool) (l : list A) : list A by wf (size l) lt := + Equations nubBy {A} (eq : A -> A -> bool) (l : list A) : list A by wf (length l) lt := + nubBy ... := usual_def; + nubBy ... := usual_def. ]] Equations will then automatically: @@ -203,11 +235,10 @@ Definition gcd_Fix (x y : nat) : nat := is performed on decreasing arguments, try to prove it automatically, and if it cannot do it on its own leave it to us to prove - This allows to separate the proofs that the recursive call are smaller + This allows to write our definition transparently and directly as we would like to. + In particular, it enables to separete the proofs that the recursive call are smaller from the definition of the function, making it easier to read and define while dealing automatically with trivial cases. - Moreover, it enables us to prove arguments directly in the proof mode using - tactics. In the following, we assume basic knowledge of obligations as discussed in the (short) tutorial Equations: obligations. @@ -247,15 +278,14 @@ Qed. (** Compared to other methods, reasoning on functions defined with well-founded recursion with [Equations], is no different than on regular functions. - Using function elimination ([funelim]) we can prove our - properties directly according to the pattern of our definition. - In particular, we do not have to do proofs by reproducing the proof structure - used to prove that the function is well-founded. - It is particularly interesting as it enables to completely hide from the users - , actually you can see no trace of it in the definition, and to reason about - functions following the recursive call, that is directly as we think about them? - - This is a very powerful technic that, for instance, enables us to prove in a + Using function elimination ([funelim]) we can prove our properties directly + according to the pattern of our definition. + In particular, we do not have to do proofs by recursion on the proof + that the relation is well-founded. + It is important as it enables to completely hide well-founded recursion + from the users and to reason about our function directly as we think about it. + + This is a very powerful method that, for instance, enables us to prove in a few lines that [nubBy] does remove all duplicates; *) @@ -385,9 +415,9 @@ ack (S m) (S n) := ack m (ack (S m) n). (** In principle, we should be able to reason about [ack] as usual using [funelim]. - Unfortunately, in this particular case, [funelim] runs for ever wish you can - checkout by uncommenting the following code. - It is a known issue currently being fixed due to oversimplification done + Unfortunately, in this particular case, [funelim] runs forever which you can + check out below. + It is a known issue currently being fixed due to oversimplification being done by [funelim]. *) From 59f92a5954d706fd8fc0bd3c17de02f51fecc4b8 Mon Sep 17 00:00:00 2001 From: thomas-lamiaux Date: Wed, 12 Jun 2024 13:37:30 +0200 Subject: [PATCH 28/34] clean up --- src/Tutorial_Equations_wf.v | 68 +++++++++++++++++++------------------ 1 file changed, 35 insertions(+), 33 deletions(-) diff --git a/src/Tutorial_Equations_wf.v b/src/Tutorial_Equations_wf.v index 8e9c364..6687af5 100644 --- a/src/Tutorial_Equations_wf.v +++ b/src/Tutorial_Equations_wf.v @@ -5,14 +5,14 @@ [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. + define function using well-founded recursion and to reason about them. In section 1, we explain the interests and the principle of well-founded recursion. We then explain in section 2, how to define functions and how to reason about them using well-founded recursion and [Equations]. In some cases, applying well-founded recursion can fail because information - relevant to termination gets lost during recursion. - In section 3, we discuss two such cases a how to go around the issues. + relevant to termination get lost during recursion. + In section 3, we discuss two such cases a how to go around them. *** Table of content @@ -48,20 +48,21 @@ *) From Equations Require Import Equations. -From Coq Require Import List Arith Lia. +From Coq Require Import List Arith Nat Lia. Import ListNotations. (** ** 1. Introduction to well-founded recursion For Coq to be consistent, all functions must be terminating. - To ensure there are, Coq checks that they satisfy a complex syntactic + To ensure they are, Coq checks that they satisfy a complex syntactic criterion named the guard condition. Very roughly, the guard condition basically checks that all recursive call - are performed on syntactically smaller instance. + are performed on syntactically smaller instances. Though, while practical and powerful, this syntactic criterion is by nature limited and not complete: it can happen that functions can be proven terminating - using size and mathematical arguments even though the guard fails to them as such. + using size arguments and mathematical reasoning, even though the guard fails + to them as such. *** 1.1 The syntactic guard condition is limited @@ -75,7 +76,7 @@ Import ListNotations. test recursively filters out the duplicates of a list. The recursive call is not performed on the recursive argument [l] but on the list [filter (fun y => negb (eq x y)) l]. This prevents the syntactic - from checking it is indeed smaller, and is hence rejected. + from checking it is indeed smaller, and it is hence rejected. Yet, we can prove that [filter] does not increase the size of a list, and hence that the recursive call is indeed performed on a "smaller" instance than [l] and that [nubBy] is terminating. @@ -100,13 +101,12 @@ nubBy eq (a :: l) => a :: nubBy eq (filter (fun b => negb (eq a b)) l). its definition fully relies on theoretic reason to ensure termination. *) -Fail Equations gcd (x y : nat) (H : x > y) : nat := -gcd x y H with Nat.eq_dec y 0 => { +Fail Equations gcd (x y : nat) : nat := +gcd x y with eq_dec y 0 => { | left _ => x | right _ => gcd y (x mod y) }. - (** *** 1.2 Well-founded recursion **** Informally @@ -119,7 +119,7 @@ gcd x y H with Nat.eq_dec y 0 => { - Providing a "well-founded" relation [R : A -> A -> Prop], informally a relation for which there is no infinitely decreasing sequence. For instance, the strict order on [nat], [< : nat : -> nat -> nat] is well-founded - as starting from [m] it impossible to decrease infinitely, there is a point + as starting from [m : nat], it impossible to decrease infinitely, there is a point at which you must reach [0]. - Proving that all the recursive calls are performed on smaller arguments according to [R] @@ -130,10 +130,11 @@ gcd x y H with Nat.eq_dec y 0 => { **** More Formally - Defining a well-founded relation by "no having infinitely decreasing sequence" + Defining a well-founded relation by "not having infinitely decreasing sequence" is not very useful as #TODO - Consequently, in type theory, we use a slighlty stronger notion, that is - "accessibility", to define a well-founded relations [R : A -> A -> Prop]. + Consequently, in type theory, we use the slighlty stronger notion of + "accessibility" to define a well-founded relations [R : A -> A -> Prop]. + An element [a : A] is accessible for [R], denoted [Acc R a] when for all [a' : A] smaller than [a], [a'] is itself accessible. Intuitevely, it ensures constructively that they are no decreasing sequence @@ -142,8 +143,8 @@ gcd x y H with Nat.eq_dec y 0 => { - 2. All elements smaller than [a] are accessible, so there are no infinitely decreasing sequence from them, and hence from [a]. *) -Print Acc. +Print Acc. (** We then say a relation is well-founded, when forall (a : A), [R] is accessible at [a], i.e. [Acc R a]. @@ -184,29 +185,29 @@ Admitted. Definition gcd_Fix (x y : nat) : nat := Fix lt_wf (fun _ => nat -> nat) (fun (b: nat) (gcd_Fix: forall b', b' < b -> nat -> nat) (a: nat) => - match Nat.eq_dec b 0 with + match eq_dec b 0 with | left EQ => a | right NE => gcd_Fix (a mod b) (gcd_oblig a b NE) b end) y x. -(** However, doing so has several disadvantages. +(** However, doing so has several disadvantages: The function is much less transparent than a usual definition by [Fixpoint] as: - there is an explicit fixpoint combinator [Fix] in the definition - it forced us to use curryfication and the order of the arguments has changed - - explicit proofs appears directly in the definition of the function (though Program can help) - - Moreover, behind the scene the function is defined by recursion on the - accessibility proof, which forces us in turn to do a recursion on the - accessibility proof to reason about the function. - It makes harder to reason about the function, as the recursion - scheme no longer follow the intuitive definition. - Furthermore, as we had to use curryfication in our definition, we may need + - explicit proofs now appears directly in the definition of the function + (though [Program] can help for that) + + It also makes it harder to reason about the function as the function is + defined behind the scene by recursion on the accessibility proof. + Indeed, in turn, it forces to do a recursion on the accessibility proof to + reason about the function, which no longer corresponds to the way we think about + our function. + Moreover, as we had to use curryfication in our definition, we may need the axiom of function extensionally to reason about [gcd_Fix]. - - Considering this different defaults, Equations provides a built-in mechanism + To go arounf this different issues, Equations provides a built-in mechanism to help us write functions and reason by well-founded recursion. *) @@ -216,7 +217,7 @@ Definition gcd_Fix (x y : nat) : nat := To define a function by well-founded recursion with Equations, one must add after the type of the function [by wf x R], where [x] is the term decreasing, and [R] the well-founded relation for which [x] decreases, - and then define the function as usual. + and then define the function **as usual**. For instance, the function [nubBy] terminates as the size of the list decrease in each recursive call according to the usual strict order [<] on [nat], [lt] in Coq. @@ -236,12 +237,13 @@ Definition gcd_Fix (x y : nat) : nat := and if it cannot do it on its own leave it to us to prove This allows to write our definition transparently and directly as we would like to. - In particular, it enables to separete the proofs that the recursive call are smaller - from the definition of the function, making it easier to read and define + In particular, we not need to alter the structure of the definition to + get it accepted, and it enables to separate the proofs that the recursive + call are smaller from the definition, making it easier to read and define while dealing automatically with trivial cases. In the following, we assume basic knowledge of obligations as discussed - in the (short) tutorial Equations: obligations. + in the (short) tutorial Equations: Obligations. ** 2.1 Using a size argument @@ -367,7 +369,7 @@ Lemma mod_minus a b : b <> 0 -> b < a -> (a - b) mod b = a mod b. Proof. Admitted. -Lemma gcd_spec1 a b: 0 <> b -> gcd a b = gcd (Nat.modulo a b) b. +Lemma gcd_spec1 a b: 0 <> b -> gcd a b = gcd (a mod b) b. Proof. funelim (gcd a b); intros. - now rewrite Nat.Div0.mod_0_l. From 1d0bb327a1a6696c117d4d92c97b07e29246b7ec Mon Sep 17 00:00:00 2001 From: thomas-lamiaux Date: Wed, 12 Jun 2024 15:11:21 +0200 Subject: [PATCH 29/34] clean up --- src/Tutorial_Equations_wf.v | 218 ++++++++++++++++++------------------ 1 file changed, 108 insertions(+), 110 deletions(-) diff --git a/src/Tutorial_Equations_wf.v b/src/Tutorial_Equations_wf.v index 6687af5..c85c276 100644 --- a/src/Tutorial_Equations_wf.v +++ b/src/Tutorial_Equations_wf.v @@ -20,10 +20,9 @@ - 1.1 The syntactic guard condition is limited - 1.2 Well-founded recursion 2. Well-founded recursion and Equations - 2.1 Using a size argument - 2.2 Using a measure - 2.3 Using a lexicographic order - 2.4 Using a custom well-founded relation + 2.1 Using a measure + 2.2 Using a lexicographic order + 2.3 Using a custom well-founded relation - 3. Different tricks to work with well-founded recursion - 3.1 The inspect method - 3.2 Improving recursion hypotheses @@ -242,17 +241,20 @@ Definition gcd_Fix (x y : nat) : nat := call are smaller from the definition, making it easier to read and define while dealing automatically with trivial cases. - In the following, we assume basic knowledge of obligations as discussed - in the (short) tutorial Equations: Obligations. + In the following, we assume basic knowledge of obligations and [Equations] + works together as discussed in the (short) tutorial Equations: Obligations. - ** 2.1 Using a size argument + ** 2.1 Using a measure - The most basic method to define a function by well-founded recursion is to - define a size function, and to prove that the size decrease with each - recursive call for the usual strict order [<] on natural numbers. + The most basic (and actually very versatile) method to define a function by well-founded + recursion is to define a measure into [nat] to use the well-founded order [<], + that is a function [m : ... -> nat] depending on the arguments, + and to prove the measure deacreses in each recursive call. - This method is already enough to define the function [nubBy], that - recursively filters out the duplicates of a list, by well-founded recursion. + This simplest example is to use size function on the inductive type at hand, + for instance one counting the number of constructors. + Is already enough to define the function [nubBy], that recursively filters + out the duplicates of a list, by well-founded recursion. Indeed, the size of a list is its length, and the only recursive call performed by [nubBy] is on [filter (fun y => negb (eq x y)) l]. As [filter] can only remove elements, its length is indeed strictly smaller @@ -316,15 +318,9 @@ Proof. -- assumption. Qed. -(** ** 2.2 Using a measure - - The size method described above is particular case of a more general scheme - that consist in using a measure: that is a function depending on - the arguments to [nat], so that it decrease in each recursive call. - - For an example, consider a [gcd] function that does not require the assumption - that [x > y], by first checking if [x] or [y] is [0], and otherwise - compare [x] and [y], and recall [gcd] with [x - y] or [y - x] depending +(** For a slighlty more involved consider a [gcd] function that does not require + the assumption that [x > y], by first checking if [x] or [y] is [0], and otherwise + compare [x] and [y], and recall [gcd] with [x - y] or [y - x] depending on which is the greater. We cannot prove it is terminating either by looking if [x] or [y] decrease (the size of a number is the number itself) as we do not know up-ahead which @@ -336,7 +332,6 @@ Qed. We can define [gcd] by well-founded recursion by adding [wf (x + y) lt]. We then get two obligations corresponding to the recursive goals, which are basic arithmetic goals and can be solved using [lia]. - *) Equations? gcd (x y : nat) : nat by wf (x + y) lt := @@ -383,7 +378,7 @@ Proof. Qed. -(** ** 2.3 Using a lexicographic order +(** ** 2.2 Using a lexicographic order Not all definitions can be proven terminating using a measure and the strict order [<] on [nat]. In some cases, it is more practical to use a different well-founded order. @@ -460,7 +455,7 @@ Proof. Qed. -(** ** 2.4 Using a custom well-founded relation +(** ** 2.3 Using a custom well-founded relation In some cases, there is no basic order that easily enables to define a function by well-founded recursion. @@ -476,10 +471,10 @@ Qed. This is represented by this context: *) - Module LinearSearch. +Module LinearSearch. - Context (f : nat -> bool). - Context (h : exists n : nat, f n = true). +Context (f : nat -> bool). +Context (h : exists n : nat, f n = true). (** Knowing there is an [n : nat] such that [f n = true], we would like to actually compute one. @@ -493,7 +488,7 @@ Qed. i.e [forall k, k <= m -> f k = false]. *) - Definition R n m := (forall k, k <= m -> f k = false) /\ n = S m. +Definition R n m := (forall k, k <= m -> f k = false) /\ n = S m. (** Knowing that the previous booleans have been [false] enables us to prove that [R] is well-founded when combined with [h]. @@ -501,16 +496,16 @@ Qed. for our purpose. *) - Lemma wf_R : (exists n : nat, f n = true) -> well_founded R. - Proof. - Admitted. +Lemma wf_R : (exists n : nat, f n = true) -> well_founded R. +Proof. +Admitted. (** Having proven it is well-founded, we declare it as an instance of the database [WellFounded] so that [Equations] can find it automatically when using the keyword [wf x R]. *) - Instance wfR : WellFounded R := wf_R h. +Instance wfR : WellFounded R := wf_R h. (** We are not ready to define our function by well-founded recursion. @@ -519,33 +514,33 @@ Qed. section 2.1 for more details on the method. *) - Definition inspect {A} (a : A) : {b | a = b} := exist _ a eq_refl. +Definition inspect {A} (a : A) : {b | a = b} := exist _ a eq_refl. - Notation "x 'eqn:' p" := (exist _ x p) (only parsing, at level 20). +Notation "x 'eqn:' p" := (exist _ x p) (only parsing, at level 20). (** Though, we want to start a computation at 0, to define our function by well-founded recursion we need to start at a generic point [m : nat], to actually have a term to do our recursion on: *) - Equations? exists_nat (m : nat) (H : forall n, n < m -> f n = false) : - {n : nat | f n = true} by wf m R := - exists_nat m H with inspect (f m) :={ - | true eqn:p => (exist _ m p) - | false eqn:p => exists_nat (S m) _ - }. - Proof. - - inversion H0; auto. - - unfold R. split. 2: reflexivity. - intros k ikm. inversion ikm. 1: assumption. - subst. apply H. auto with arith. - Qed. - - Theorem linear_search : {n : nat | f n = true}. - Proof. - unshelve eapply (exists_nat 0). - intros n Hn0; inversion Hn0. - Qed. +Equations? exists_nat (m : nat) (H : forall n, n < m -> f n = false) : + {n : nat | f n = true} by wf m R := +exists_nat m H with inspect (f m) :={ + | true eqn:p => (exist _ m p) + | false eqn:p => exists_nat (S m) _ +}. +Proof. +- inversion H0; auto. +- unfold R. split. 2: reflexivity. + intros k ikm. inversion ikm. 1: assumption. + subst. apply H. auto with arith. +Qed. + +Theorem linear_search : {n : nat | f n = true}. +Proof. + unshelve eapply (exists_nat 0). + intros n Hn0; inversion Hn0. +Qed. End LinearSearch. @@ -567,10 +562,10 @@ End LinearSearch. This situation is axiomatised by the following context : *) -Module Inspect. +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). +Context {A : Type} {lt : A -> A -> Prop} `{WellFounded A lt}. +Context (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 decreasing chain starting from [a] specified by [f]. @@ -581,15 +576,15 @@ Module Inspect. 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. +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, by doing so we generate an unprovable obligation as we do not remember information about the call to [f n] being @@ -602,9 +597,9 @@ Module Inspect. elements [(a, eq_refl) : {b : A | a = b}]. *) - Definition inspect {A} (a : A) : {b | a = b} := exist _ a eq_refl. +Definition inspect {A} (a : A) : {b | a = b} := exist _ a eq_refl. - Notation "x 'eqn:' p" := (exist _ x p) (only parsing, at level 20). +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], @@ -621,14 +616,14 @@ Module Inspect. 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 - }. - Proof. - apply decr_f. assumption. - Qed. +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 + }. +Proof. + apply decr_f. assumption. +Qed. End Inspect. @@ -648,21 +643,22 @@ End Inspect. Let's also define the usual size function on it, and an equality test on lists. *) -Section Map_in. - Context {A : Type}. +Section EqIn. + +Context {A : Type}. - Inductive RoseTree : Type := - | leaf : A -> RoseTree - | node : list RoseTree -> RoseTree. +Inductive RoseTree : Type := +| leaf : A -> RoseTree +| node : list RoseTree -> RoseTree. - Equations sizeRT (t : RoseTree) : nat := - sizeRT (leaf a) := 1; - sizeRT (node l) := 1 + list_sum (map sizeRT l). +Equations sizeRT (t : RoseTree) : nat := +sizeRT (leaf a) := 1; +sizeRT (node l) := 1 + list_sum (map sizeRT l). - Equations eqList {X} (l l' : list X) (eq : X -> X -> bool) : bool := - eqList [] [] _ := true; - eqList (a::l) (a'::l') eq := andb (eq a a') (eqList l l' eq); - eqList _ _ _ := false. +Equations eqList {X} (l l' : list X) (eq : X -> X -> bool) : bool := +eqList [] [] _ := true; +eqList (a::l) (a'::l') eq := andb (eq a a') (eqList l l' eq); +eqList _ _ _ := false. (** Having define an equality test on list, we would like to define an equality test on RoseTree. @@ -678,15 +674,15 @@ Section Map_in. remember that [l] in in [lt]: *) - Equations? eqRT (eq : A -> A -> bool) (t t': RoseTree) : bool by wf (sizeRT t) lt := - eqRT eq (leaf a) (leaf a') := eq a a'; - eqRT eq (node lt) (node lt') := eqList lt lt' (fun l l' => eqRT eq l l') ; - eqRT eq _ _ := false. - Proof. - simp sizeRT. - (* What to do know ? We have forgotten that x is in l, - and hence that sizeRT l < 1 + list_sum (map sizeRT l0) *) - Abort. +Equations? eqRT (eq : A -> A -> bool) (t t': RoseTree) : bool by wf (sizeRT t) lt := +eqRT eq (leaf a) (leaf a') := eq a a'; +eqRT eq (node lt) (node lt') := eqList lt lt' (fun l l' => eqRT eq l l') ; +eqRT eq _ _ := false. +Proof. + simp sizeRT. + (* What to do know ? We have forgotten that x is in l, + and hence that sizeRT l < 1 + list_sum (map sizeRT l0) *) +Abort. (** To go around this kind of issues, a general method is to strengthen the function that goes through the structure to remember that [x] in a subterm of [Y]. @@ -698,18 +694,20 @@ Section Map_in. Doing so, it is now possible to define [eqRT] by well-founded on the size: *) - Equations eqList' {X} (l l' : list X) (eq : forall x : X, In x l -> X -> bool) : bool := - eqList' [] [] _ := true; - eqList' (a::l) (a'::l') eq := andb (eq a _ a') (eqList' l l' (fun x Inl y => eq x _ y)); - eqList' _ _ _ := false. - - Definition list_sum_ine (x : nat) (l : list nat) : In x l -> x < 1 + list_sum l. - Admitted. - - Equations? eqRT (eq : A -> A -> bool) (t t': RoseTree) : bool by wf (sizeRT t) lt := - eqRT eq (leaf a) (leaf a') := eq a a'; - eqRT eq (node lt) (node lt') := eqList' lt lt' (fun l Inl l' => eqRT eq l l') ; - eqRT eq _ _ := false. - Proof. - simp sizeRT. apply list_sum_ine. apply in_map. assumption. - Qed. \ No newline at end of file +Equations eqList' {X} (l l' : list X) (eq : forall x : X, In x l -> X -> bool) : bool := +eqList' [] [] _ := true; +eqList' (a::l) (a'::l') eq := andb (eq a _ a') (eqList' l l' (fun x Inl y => eq x _ y)); +eqList' _ _ _ := false. + +Definition list_sum_ine (x : nat) (l : list nat) : In x l -> x < 1 + list_sum l. +Admitted. + +Equations? eqRT (eq : A -> A -> bool) (t t': RoseTree) : bool by wf (sizeRT t) lt := +eqRT eq (leaf a) (leaf a') := eq a a'; +eqRT eq (node lt) (node lt') := eqList' lt lt' (fun l Inl l' => eqRT eq l l') ; +eqRT eq _ _ := false. +Proof. + simp sizeRT. apply list_sum_ine. apply in_map. assumption. +Qed. + +End EqIn. \ No newline at end of file From 315900809455f6125c9fc62e82011b6ccd6fef0b Mon Sep 17 00:00:00 2001 From: Thomas Lamiaux <85848641+thomas-lamiaux@users.noreply.github.com> Date: Wed, 19 Jun 2024 14:36:49 +0200 Subject: [PATCH 30/34] Apply suggestions from code review Co-authored-by: Meven Lennon-Bertrand <58942857+MevenBertrand@users.noreply.github.com> --- src/Tutorial_Equations_wf.v | 163 ++++++++++++++++++------------------ 1 file changed, 80 insertions(+), 83 deletions(-) diff --git a/src/Tutorial_Equations_wf.v b/src/Tutorial_Equations_wf.v index c85c276..c08f4a1 100644 --- a/src/Tutorial_Equations_wf.v +++ b/src/Tutorial_Equations_wf.v @@ -54,14 +54,14 @@ Import ListNotations. (** ** 1. Introduction to well-founded recursion For Coq to be consistent, all functions must be terminating. - To ensure they are, Coq checks that they satisfy a complex syntactic + To ensure they are, Coq checks that they satisfy a syntactic criterion named the guard condition. - Very roughly, the guard condition basically checks that all recursive call - are performed on syntactically smaller instances. - Though, while practical and powerful, this syntactic criterion is by nature + Roughly, the guard condition checks that all recursive calls are performed + on arguments syntactically detected to be subterms of the original argument. + While practical and powerful, this syntactic criterion is by nature limited and not complete: it can happen that functions can be proven terminating using size arguments and mathematical reasoning, even though the guard fails - to them as such. + to see them as such. *** 1.1 The syntactic guard condition is limited @@ -71,11 +71,11 @@ Import ListNotations. function has been applied [f x], preventing the syntactic guard from checking that it is still indeed smaller. - For instance, consider the function [nubBy] that given an equality - test recursively filters out the duplicates of a list. + For instance, consider the function [nubBy] below, that + filters out the duplicates of a list. The recursive call is not performed on the recursive argument [l] but - on the list [filter (fun y => negb (eq x y)) l]. This prevents the syntactic - from checking it is indeed smaller, and it is hence rejected. + on the list [filter (fun y => negb (eq x y)) l]. This is too much for the guard + and the function is hence rejected. Yet, we can prove that [filter] does not increase the size of a list, and hence that the recursive call is indeed performed on a "smaller" instance than [l] and that [nubBy] is terminating. @@ -90,12 +90,11 @@ nubBy eq (a :: l) => a :: nubBy eq (filter (fun b => negb (eq a b)) l). fully rely on semantic arguments to decide which recursive call to perform, logically preventing the guard condition from checking it. - A prime example is the Euclidean algorithm computing the gcd of - [x] and [y] assuming that [x > y]. - It performs recursion on [x mod y] which is not a subterm of - any recursively smaller arguments, as [gcd] does not match any inputs. - It is well-founded and terminating for [lt], as we have tested - that [y > 0] and we can prove that [x mod y < y]. + A prime example is Euclide's algorithm computing the gcd of + [x] and [y]. + It performs recursion on [x mod y], which is not a subterm of the inputs. + Yet, it is terminating, because the sum of the two arguments is a sequence + of natural numbers, which strictly decreases and thus cannot go forever. Consequently, there is no hope for a syntactic guard to accept [gcd] as its definition fully relies on theoretic reason to ensure termination. *) @@ -113,8 +112,8 @@ gcd x y with eq_dec y 0 => { It would be limiting if this kind of functions could not be defined. Fortunately, they can be using well-founded recursion. - Informally, defining a function [f] by well-founded recursion basically - amounts to a usual definition expect that we justify termination by: + Informally, defining a function [f] by well-founded recursion + amounts to a usual definition, except that we justify termination by: - Providing a "well-founded" relation [R : A -> A -> Prop], informally a relation for which there is no infinitely decreasing sequence. For instance, the strict order on [nat], [< : nat : -> nat -> nat] is well-founded @@ -123,20 +122,21 @@ gcd x y with eq_dec y 0 => { - Proving that all the recursive calls are performed on smaller arguments according to [R] - This enables us to justify termination of our function [f] as it is impossible - to decrease forever and all recrusive call are smaller, so whatever the input [f] - must terminate at a point or another. + This allows us to justify termination of our function [f]: since each recursive call + is on a smaller argument, an infinite sequence of recursive calls would give an + infinitely decreasing sequence according to [R], which by assumption cannot exist. **** More Formally - Defining a well-founded relation by "not having infinitely decreasing sequence" - is not very useful as #TODO - Consequently, in type theory, we use the slighlty stronger notion of - "accessibility" to define a well-founded relations [R : A -> A -> Prop]. + In a type theory like Coq's, however, defining a well-founded relation as one + "not having infinitely decreasing sequence" is slightly too weak too use properly. + Instead, we use the stronger notion of "accessibility" to define + well-founded relations [R : A -> A -> Prop]. This is classically equivalent to having no + infinite decreasing sequence, but in an inductive definition which is much easier to use. - An element [a : A] is accessible for [R], denoted [Acc R a] when for - all [a' : A] smaller than [a], [a'] is itself accessible. - Intuitevely, it ensures constructively that they are no decreasing sequence + An element [a : A] is accessible for [R], denoted [Acc R a] when + all [a' : A] smaller than [a], [a'] are themselves accessible. + Intuitively, it constructively ensures that they are no decreasing sequence as the only ways for an element [a] to be accessible are that: - 1. There are no elements smaller than [a], so you cannot decrease further - 2. All elements smaller than [a] are accessible, so there are no infinitely @@ -145,9 +145,9 @@ gcd x y with eq_dec y 0 => { Print Acc. -(** We then say a relation is well-founded, when forall (a : A), [R] is - accessible at [a], i.e. [Acc R a]. - It ensures that wherever we start at, we can not decrease forever. +(** We then say a relation is well-founded, when [forall (a : A), Acc R a], that is + when all inhabitants of [A] are accessible. + It ensures that wherever we start at, we cannot decrease forever. *) Print well_founded. @@ -155,14 +155,14 @@ Print well_founded. (** Given a well-founded relation [R : A -> A -> Prop], defining a function [f] by well-founded recursion on [a : A] consists in defining [f] assuming that [f] is defined for all [a'] smaller than [a], that is such that [R a' a]. - When particularised to natural numbers and [<], this concept is sometimes + When specialized to natural numbers and [<], this concept is sometimes known as "strong recursion / induction": when defining [f n] one assumes that [f] is defined/proven for all smaller natural numbers [n' < n]. **** In practice There are several methods to define functions by well-founded recursion using Coq. - They all have their pros and cons, but as a general rules defining functions + They all have their pros and cons, but as a general rule defining functions and reasoning using well-founded recursion can be tedious. For instance, consider the [Fix] construction of the standard library, @@ -192,21 +192,19 @@ Definition gcd_Fix (x y : nat) : nat := (** However, doing so has several disadvantages: - The function is much less transparent than a usual definition by [Fixpoint] as: + The function is much less readable than a usual definition by [Fixpoint] as: - there is an explicit fixpoint combinator [Fix] in the definition - - it forced us to use curryfication and the order of the arguments has changed + - we are forced to use curryfication and change the order of arguments - explicit proofs now appears directly in the definition of the function (though [Program] can help for that) - It also makes it harder to reason about the function as the function is - defined behind the scene by recursion on the accessibility proof. - Indeed, in turn, it forces to do a recursion on the accessibility proof to - reason about the function, which no longer corresponds to the way we think about + It also makes it harder to reason about the function as it forces to use recursion + on the accessibility proof, which no longer corresponds to the way we think about our function. Moreover, as we had to use curryfication in our definition, we may need the axiom of function extensionally to reason about [gcd_Fix]. - To go arounf this different issues, Equations provides a built-in mechanism + To go around these different issues, Equations provides a built-in mechanism to help us write functions and reason by well-founded recursion. *) @@ -214,13 +212,13 @@ Definition gcd_Fix (x y : nat) : nat := (** ** 2. Well-founded recursion and Equations To define a function by well-founded recursion with Equations, one must add - after the type of the function [by wf x R], where [x] is the term - decreasing, and [R] the well-founded relation for which [x] decreases, + after the type of the function [by wf x R], where [x] is the decreasing + term, and [R] the well-founded relation for which [x] decreases, and then define the function **as usual**. For instance, the function [nubBy] terminates as the size of the list decrease in each recursive call according to the usual strict order [<] on [nat], [lt] in Coq. - We hence, need to write [wf (size l) l] to define it by well-founded recursion: + We hence need to write [wf (size l) l] to define it by well-founded recursion: [[ Equations nubBy {A} (eq : A -> A -> bool) (l : list A) : list A by wf (length l) lt := @@ -231,15 +229,15 @@ Definition gcd_Fix (x y : nat) : nat := Equations will then automatically: - 1. Search for a proof that [R] is well-founded, using type classes (a database) specific to [Equations] suitably named [WellFounded] - - 2. It will then create an obligation to prove that each recursive call + - 2. Create an obligation to prove that each recursive call is performed on decreasing arguments, try to prove it automatically, - and if it cannot do it on its own leave it to us to prove + and if it cannot do it on its own leave it for us to prove This allows to write our definition transparently and directly as we would like to. - In particular, we not need to alter the structure of the definition to - get it accepted, and it enables to separate the proofs that the recursive + In particular, we do not need to alter the structure of the definition to + get it accepted, and it allows us to separate the proofs that the recursive call are smaller from the definition, making it easier to read and define - while dealing automatically with trivial cases. + while automatically dealing with trivial cases. In the following, we assume basic knowledge of obligations and [Equations] works together as discussed in the (short) tutorial Equations: Obligations. @@ -249,22 +247,22 @@ Definition gcd_Fix (x y : nat) : nat := The most basic (and actually very versatile) method to define a function by well-founded recursion is to define a measure into [nat] to use the well-founded order [<], that is a function [m : ... -> nat] depending on the arguments, - and to prove the measure deacreses in each recursive call. + and to prove the measure decreases in each recursive call. - This simplest example is to use size function on the inductive type at hand, - for instance one counting the number of constructors. + A simple example is the size of an inductive value, i.e. the maximal number of nested constructors. Is already enough to define the function [nubBy], that recursively filters out the duplicates of a list, by well-founded recursion. Indeed, the size of a list is its length, and the only recursive call performed by [nubBy] is on [filter (fun y => negb (eq x y)) l]. - As [filter] can only remove elements, its length is indeed strictly smaller - than [l], and the function is terminating. + As [filter] can only remove elements, its length is indeed smaller + than [l]'s, and the function is terminating. To define [nubBy] using [Equations] and well-founded recursion, it suffices to add [wf (length l) lt] after typing to indicate on which term, here [length l], and - for which well-founded relation, here [< := lt], we are doing the well-founded recursion on. + for which well-founded relation, here [lt] (the relation behind the notation [<]), + we wish to use well-founded recursion. An obligation corresponding to proving that the recursive call is smaller, - that is [length (filter (fun y => negb (eq x y)) l) < length l], is created. + that is [length (filter (fun y => negb (eq x y)) l) < length (a :: l)], is created. As [Equations] cannot solve on its own, it then left to us to solve. Using the keyword [Equations?], it is automatically unshelved, and we simply have to prove it using tactics. @@ -280,17 +278,16 @@ Proof. Qed. -(** Compared to other methods, reasoning on functions defined with well-founded +(** Reasoning on functions defined with well-founded recursion with [Equations], is no different than on regular functions. Using function elimination ([funelim]) we can prove our properties directly according to the pattern of our definition. - In particular, we do not have to do proofs by recursion on the proof - that the relation is well-founded. - It is important as it enables to completely hide well-founded recursion - from the users and to reason about our function directly as we think about it. + In particular, we do not have to do proofs by well-founded induction. + This completely hides well-founded recursion and allows us to reason + about our function directly as we think about it. This is a very powerful method that, for instance, enables us to prove in a - few lines that [nubBy] does remove all duplicates; + few lines that [nubBy] does remove all duplicates. *) Lemma In_nubBy {A} (eq : A -> A -> bool) (l : list A) (a : A) @@ -320,16 +317,16 @@ Qed. (** For a slighlty more involved consider a [gcd] function that does not require the assumption that [x > y], by first checking if [x] or [y] is [0], and otherwise - compare [x] and [y], and recall [gcd] with [x - y] or [y - x] depending on - which is the greater. - We cannot prove it is terminating either by looking if [x] or [y] decrease - (the size of a number is the number itself) as we do not know up-ahead which + compares [x] and [y], and recalls [gcd] with [x - y] or [y - x] depending on + which is greater. + We cannot prove it is terminating either by looking if [x] or [y] decreases + (the size of a number is the number itself) as we do not know upfront which of [x] or [y] is bigger. However, we can use that the measure [x + y] is decreasing for the usual well-founded order on [nat], as if [x] and [y] are strictly greater than [0], - than [x + y > x + (y - x) = y] and [x + y > y + (x - y) = y]. + then [x + y > x + (y - x) = y] and [x + y > y + (x - y) = y]. - We can define [gcd] by well-founded recursion by adding [wf (x + y) lt]. + We can define [gcd] by well-founded recursion by annotating the definition with [wf (x + y) lt]. We then get two obligations corresponding to the recursive goals, which are basic arithmetic goals and can be solved using [lia]. *) @@ -387,7 +384,7 @@ Qed. lexicographic order [ A -> Prop] and [ B -> Prop], [(a,b) A -> Prop] @@ -507,7 +504,7 @@ Admitted. Instance wfR : WellFounded R := wf_R h. -(** We are not ready to define our function by well-founded recursion. +(** We are now ready to define our function by well-founded recursion. Here, for technical reason we use the [inspect] method to remember the value of [f m]. Here, it is not necessary to understand it for our purpose, and we refer to @@ -518,7 +515,7 @@ Definition inspect {A} (a : A) : {b | a = b} := exist _ a eq_refl. Notation "x 'eqn:' p" := (exist _ x p) (only parsing, at level 20). -(** Though, we want to start a computation at 0, to define our function +(** Even though we want to start a computation at 0, to define our function by well-founded recursion we need to start at a generic point [m : nat], to actually have a term to do our recursion on: *) @@ -547,12 +544,12 @@ End LinearSearch. (** ** 3. Different methods to work with well-founded recursion - When defining a function, it can happen that we loose information + When defining a function, it can happen that we lose information relevant to termination when matching a value, and that we then get stuck trying to prove termination. In this section, we discuss two such example an methods to go around the issue. - Note, the inspect method was already used in section 2.4. + Note that the inspect method was already used in section 2.4. *** 3.1 The inspect method @@ -569,11 +566,11 @@ Context (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 decreasing chain starting from [a] specified by [f]. - 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 the - chain starting with [p], i.e., our recursive call [f_sequence p], and otherwise - stop the computation. + Naively, we would like to do it as follows: + first, we check if there is an element smaller than [a] by matching [f a] + with a [with] clause; if there is none, then we stop the computation, otherwise + we get [Some p] and we returns [p] added to the chain starting with [p], + i.e., our recursive call [f_sequence p]. *) Equations? f_sequence (a : A) : list A by wf a lt := @@ -616,7 +613,7 @@ Notation "x 'eqn:' p" := (exist _ x p) (only parsing, at level 20). to fill. *) -Equations? f_sequence (a : A) : list A by wf a lt := +#[tactic="idtac"] 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 @@ -668,10 +665,10 @@ eqList _ _ _ := false. if you are using a subsequent version, assume you need it for pedagogical purposes. If we try to define the equality test naively as below, [Equations] generates - the obligation [sizeRT l < 1 + list_sum (map sizeRT lt0)] corresponding to + the obligation [sizeRT l < 1 + list_sum (map sizeRT lt)] corresponding to the case where [lt := l :: _]. This is obviously true, but we are stuck trying to prove it as we do not - remember that [l] in in [lt]: + remember that [l] is in [lt]: *) Equations? eqRT (eq : A -> A -> bool) (t t': RoseTree) : bool by wf (sizeRT t) lt := @@ -681,16 +678,16 @@ eqRT eq _ _ := false. Proof. simp sizeRT. (* What to do know ? We have forgotten that x is in l, - and hence that sizeRT l < 1 + list_sum (map sizeRT l0) *) + and hence that sizeRT l < 1 + list_sum (map sizeRT lt) *) Abort. (** To go around this kind of issues, a general method is to strengthen the function that goes through the structure to remember that [x] in a subterm of [Y]. In our case, it means strengthening [eqList] so that to remember that [l] is - a subterm of [lt0], i.e. that [l] is in [lt0]. + in [lt]. To do so, we ask for the input of the equality test [eq] of [eqList] to additionally be in in [l], i.e. [eq : forall x : X, In x l -> X -> bool]. - This way, in the case (lt0 := l :: _) we remember [In l lt0]. + This way, in the case (lt := l :: _) we remember [In l lt]. Doing so, it is now possible to define [eqRT] by well-founded on the size: *) From f9ee8e28ab57c7881629f38266cb8bf2b5bf01d3 Mon Sep 17 00:00:00 2001 From: Thomas Lamiaux <85848641+thomas-lamiaux@users.noreply.github.com> Date: Wed, 19 Jun 2024 14:39:04 +0200 Subject: [PATCH 31/34] Update src/Tutorial_Equations_wf.v Co-authored-by: Meven Lennon-Bertrand <58942857+MevenBertrand@users.noreply.github.com> --- src/Tutorial_Equations_wf.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Tutorial_Equations_wf.v b/src/Tutorial_Equations_wf.v index c08f4a1..8861928 100644 --- a/src/Tutorial_Equations_wf.v +++ b/src/Tutorial_Equations_wf.v @@ -398,7 +398,7 @@ Qed. To define [ack] by well-founded recursion, it suffices to add [(lexprod _ _ lt lt)]. The function [lexprod] builds the lexicographic order and derive a proof that it is well-founded provided that both order are. - As we can see, with this order, the obligations generated turns out to be + As we can see, with this order, the obligations generated turn out to be simple enough to be automatically dealt with by [Equations]. *) From 169591a98c70d9caaaaae24089902ada6a81d890 Mon Sep 17 00:00:00 2001 From: thomas-lamiaux Date: Thu, 20 Jun 2024 22:45:33 +0200 Subject: [PATCH 32/34] edits custom wf --- src/Tutorial_Equations_wf.v | 73 +++++++++++++++++++++++++------------ 1 file changed, 49 insertions(+), 24 deletions(-) diff --git a/src/Tutorial_Equations_wf.v b/src/Tutorial_Equations_wf.v index 8861928..97de12c 100644 --- a/src/Tutorial_Equations_wf.v +++ b/src/Tutorial_Equations_wf.v @@ -388,8 +388,15 @@ Qed. call to be smaller. Moreover, [ bool). -Context (h : exists n : nat, f n = true). +Context (h : exists m : nat, f m = true). -(** Knowing there is an [n : nat] such that [f n = true], we would like to +(** Knowing there exists an [m : nat] such that [f m = true], we would like to actually compute one. Intuitively, we should be able to just try them one by one starting from 0 - until we find one, and it should terminate as we know there exists one. - However, it is not clear which classical measure or order to use to - justify this idea. We will hence use a custom one. - - We define a relation [R : nat -> nat -> nat] such that [n] is "smaller" than - "m" when [n = 1 + m] and that all booleans before [m] are [false], - i.e [forall k, k <= m -> f k = false]. + until we find one, and it should terminate as we know there exists a [m] such + that [f m = true]. + However, it is not clear which classical measure or relation to use to + formalise this intuition. We will hence use a custom relation [R n m]. + + We want to distinguish whether [n < m] or [m <= n]: + - When [m <= n], we do not care about [Acc n] as we are supposed to have already found [m]. + As we know that [f m = true], to discard these cases automatically, we add + [forall k, k <= m -> f k = false] to the relation to get [f m = false]. + - By the previous point, we know that [Acc m]. + Consequently, to prove [Acc n] when [n < m], we want to reason by induction + on [k := m - n]. To do so, we add [n = S m] to the relation. + + This gives us the following relation and proof of our intuition: *) Definition R n m := (forall k, k <= m -> f k = false) /\ n = S m. -(** Knowing that the previous booleans have been [false] enables us to prove - that [R] is well-founded when combined with [h]. - We omit the proof here because it is a bit long, and not very interesting - for our purpose. - *) +Lemma wf_R_m_le m (h : f m = true) : forall n, m <= n -> Acc R n. +Proof. + intros n H. constructor. intros ? [h' ?]. + specialize (h' m ltac:(auto)). + congruence. +Qed. +Lemma wf_R_lt_m m (h : f m = true) : forall n, n < m -> Acc R n. +Proof. + intros n H. assert (Acc R m) by (eapply wf_R_m_le; eauto). + rewrite <- (Nat.sub_add n m ltac:(lia)) in *. + set (k := m - n) in *; clearbody k. clear h H. + induction k. + - easy. + - apply IHk. constructor. intros ? [? ->]. assumption. +Qed. + +(** We can now prove that the realtion is well-founded: *) Lemma wf_R : (exists n : nat, f n = true) -> well_founded R. Proof. -Admitted. + intros [m h] n. destruct (le_lt_dec m n). + - eapply wf_R_m_le; eassumption. + - eapply wf_R_lt_m; eassumption. +Qed. (** Having proven it is well-founded, we declare it as an instance of the database [WellFounded] so that [Equations] can find it automatically when using the @@ -613,7 +642,7 @@ Notation "x 'eqn:' p" := (exist _ x p) (only parsing, at level 20). to fill. *) -#[tactic="idtac"] Equations f_sequence (a : A) : list A by wf a lt := +#[tactic="idtac"] 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 @@ -657,12 +686,8 @@ eqList [] [] _ := true; eqList (a::l) (a'::l') eq := andb (eq a a') (eqList l l' eq); eqList _ _ _ := false. -(** Having define an equality test on list, we would like to define an equality - test on RoseTree. - For technical reasons, the straigthforward definition is not accepted by Coq - before Coq v8.20, so we need well-founded recursion on the size of RoseTress - to define the equality test. - if you are using a subsequent version, assume you need it for pedagogical purposes. +(** For pedagogical purposes, having define an equality test on list, we would + like to define an equality test on RoseTree using well-founded recursion. If we try to define the equality test naively as below, [Equations] generates the obligation [sizeRT l < 1 + list_sum (map sizeRT lt)] corresponding to From ca5047b845caee3ad90072b4044726da9d9e032e Mon Sep 17 00:00:00 2001 From: Thomas Lamiaux <85848641+thomas-lamiaux@users.noreply.github.com> Date: Fri, 21 Jun 2024 14:04:03 +0200 Subject: [PATCH 33/34] Update Tutorial_Equations_wf.v Co-authored-by: Meven Lennon-Bertrand <58942857+MevenBertrand@users.noreply.github.com> --- src/Tutorial_Equations_wf.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Tutorial_Equations_wf.v b/src/Tutorial_Equations_wf.v index 97de12c..829dd40 100644 --- a/src/Tutorial_Equations_wf.v +++ b/src/Tutorial_Equations_wf.v @@ -388,7 +388,7 @@ Qed. call to be smaller. Moreover, [ Date: Fri, 21 Jun 2024 14:04:14 +0200 Subject: [PATCH 34/34] Update Tutorial_Equations_wf.v Co-authored-by: Meven Lennon-Bertrand <58942857+MevenBertrand@users.noreply.github.com> --- src/Tutorial_Equations_wf.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Tutorial_Equations_wf.v b/src/Tutorial_Equations_wf.v index 829dd40..83a2985 100644 --- a/src/Tutorial_Equations_wf.v +++ b/src/Tutorial_Equations_wf.v @@ -396,7 +396,7 @@ ack 0 n := S n; ack (S m) 0 := ack m 1; ack (S m) (S n) := ack m (ack (S m) n). -(** Indeed, is terminating as the recursive call are all smaller for the +(** Indeed, it is terminating as the recursive call are all smaller for the lexicographic order, which is essential to deal with the last case: - [(m,0)