The Coq mailing list

[Yves Bertot <yves.bertot AT inria.fr>]

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.