The Coq mailing list

[Théo Winterhalter <theo.winterhalter AT inria.fr>]

To complement Yves’s answer I would like to point out that this is not a 
shortcoming of Equations vs Function or Program. Function or Program would 
systematically use this kind of pattern (or the convoy pattern) to keep the 
most information in the obligations. However, when it is unnecessary it 
pollutes the terms so Equations gives you more control on which information 
you want to keep or not.

> On 3 Feb 2023, at 09:32, Yves Bertot <yves.bertot AT inria.fr> wrote:
> 
> Sorry for my previous answer in French, I thought I was answering only to 
> Sylvain.
> 
> Here is an example, that should correspond to Sylvain's need.  I devised it 
> by
> simply copying a few lines from 
> https://github.com/mattam82/Coq-Equations/blob/aa0311a06c83f3644644d7db56bc230490751339/examples/Basics.v#L506,
> 
> ======================================
> Require Import Arith.
> From Equations Require Import Equations.
> 
> 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 division (a b : nat) (p: 0 < b) : (nat*nat)%type by wf a lt :=
>  division a b p with inspect (a <? b) => {
>      | true eqn: _ =>  (0,a)
>      | false eqn: cmp_eqn =>  let (q,r) := division (a - b) b p in
>                  (S q,r)
>    }.
> Next Obligation.
> =======================================
> The next goal contains an extra assumption cmp_eqn, which should help 
> finishing the proof.
> 
> Yves
> 
> 
> ----- Original Message -----
>> From: "Sylvain Salvati" <sylvain.salvati AT univ-lille.fr>
>> To: "coq-club" <coq-club AT inria.fr>
>> Sent: Thursday, February 2, 2023 10:32:40 PM
>> Subject: [Coq-Club] Functions and equations
> 
>> Dear Coq-Club,
>> 
>> I have been trying the Equations module to define and prove simple
>> algorithms. When defining division by substraction, I have stumbled into
>> a difficulty (see code below). While with a definition based on
>> Function, the statement to prove termination uses the assumption that a
>> <? b = false, it is not the case with the Equation based definition. It
>> is a pity as it is then impossible to prove termination. I am wondering
>> whether there is some way to have Equations behave similarly to
>> Function.
>> 
>> Cheers,
>> 
>> S.
>> 
>> 
>> 
>> Require Import Arith FunInd Recdef.
>> From Equations Require Import Equations.
>> 
>> Function division (a b: nat) (p: 0 < b) {measure id a}:  (nat*nat) :=
>> if a <? b
>> then (0,a)
>> else
>>   let (q,r) := division (a - b) b p in
>>   (S q,r).
>> Proof.
>>   intros a b p_pos eq_test.
>>   apply Nat.sub_lt ; trivial.
>>   now rewrite Nat.ltb_ge in eq_test.
>> Defined.
>> 
>> 
>> Equations division (a b : nat) (p: 0 < b) : (nat*nat)%type by wf a lt :=
>> division a b p with a <? b => {
>>     | true =>  (0,a)
>>     | false =>  let (q,r) := division (a - b) b p in
>>                 (S q,r)
>>   }.
>> Next Obligation.