The Coq mailing list

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

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