The Coq mailing list

[Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>]

Function is documented in https://coq.inria.fr/refman/language/gallina-extensions.html#coq:cmd.function

Equations is not builtin so you will need to install it separately: https://github.com/mattam82/Coq-Equations

GitHub - mattam82/Coq-Equations: A function definition package for Coq A function definition package for Coq. Contribute to mattam82/Coq-Equations development by creating an account on GitHub. github.com

IMO, Equations is so much better than Function that Function will be eventually replaced. Last time I checked, Function has glitches like a well-foundedness measure only takes one argument, and there are some other constraints on how the body can be implemented. Equations, on the other hand, even allows you to do mutual recursion with custom measure. It's even better than Agda's pattern matching to some extent.

Thanks,

Jason Hu

https://hustmphrrr.github.io/

---

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Agnishom Chattopadhyay <agnishom AT cmi.ac.in>
Sent: June 2, 2020 12:01 PM
To: coq-club AT inria.fr <coq-club AT inria.fr>
Subject: Re: [Coq-Club] How do I define Fixpoints on Records?

 

Thanks for the quick response!

Can you point me to some documentation for `_equation` or the "Equations" library? I could find the relevant equation by running `Search "equation"` but the documentation I can find does not explain a lot.

On Tue, Jun 2, 2020 at 10:53 AM Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com> wrote:

I believe Function provides `_equation` for you to rewrite.

if you can argue termination, Equations is a much more powerful and flexible solution. Equations has a funelim tactic which allows you to reduce functions in proof mode.

Thanks,

Jason Hu

https://hustmphrrr.github.io/

---

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Agnishom Chattopadhyay <agnishom AT cmi.ac.in>
Sent: June 2, 2020 11:49 AM
To: coq-club AT inria.fr <coq-club AT inria.fr>
Subject: [Coq-Club] How do I define Fixpoints on Records?

 

Hi;

I have a record like this:

Record aggQueue : Type :=
    {
       ff : list B;
       ffA : list B;
       rr : list B;
       rrA : list B;
    }.

I want to define some kind of function on it, like this:

Fixpoint aggFlip (qq : aggQueue)  : aggQueue :=
    match (rr qq) with
    | [] => qq
    | (r :: rs) =>
      aggFlip {|
        ff := r :: (ff qq);
        ffA := (op r (aggff)) :: (ffA qq);
        rr := rs;
        rrA := tl (rrA qq)
      |}
    end.

When I try to define a function on a type expressed as a Record using a standard `Fixpoint` definition, Coq complains that the underlying data type is not recursive inductive.

One way to get around this problem seems to be to use the Function construct. However, when I do so, I cannot prove anything useful about the defined function because when I unfold it inside a proof it is terribly obscured by the surrounding proof terms.

Is there a way to do this cleanly?

--Agnishom