The Coq mailing list

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

C'est typiquement le type de question auquel je réponds, je n'ai lu que les 5 
premières lignes
mais je suis sûr que je connais la réponse.  J'essaie de l'envoyer rapidement.

En attendant, je conseille de regarder 

https://github.com/mattam82/Coq-Equations/blob/aa0311a06c83f3644644d7db56bc230490751339/examples/Basics.v#L506

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.