The Coq mailing list

[mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>]

Hi everyone,

This question piqued my curiosity because we can really write
dependent type programs cleanly using the Equations package. However,
I am curious how closely we can match the Equations solution in
(vanilla) Coq. Here is my effort [1] but I don't feel it's as clean as
the Equations solutions.

Best,
Mukesh

[1] https://gist.github.com/mukeshtiwari/12ed0d69f945e4b6fe5e7895e2665ae3.




On Fri, Feb 3, 2023 at 10:16 AM Sylvain Salvati
<sylvain.salvati AT labri.fr> wrote:
>
> 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.
>