The Coq mailing list

[Sylvain Salvati <sylvain.salvati AT univ-lille.fr>]

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.