The Coq mailing list

[Sylvain Salvati <sylvain.salvati AT labri.fr>]

Thanks for your answers. Actually, the motivation behind my question is
to use the best tool in coq for teaching the notions of pre- and
post-conditions, variants and so on. I like Function for this purpose as
it limits the coq related technicalities. I was wondering whether
Equations was giving the same comfort with respect to my pedagogic goals
and as I really like the Haskellish syntax it adopts. Passing equality
propositions around as the tutorial pointed by Yves suggests is what Ι
would like to avoid.

All the best,

S.

Théo Winterhalter <theo.winterhalter AT inria.fr> writes:

> 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.