The Coq mailing list

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

Hi everyone,

I was under the impression that Agnishom's code is not simplifying because of the opaque proof terms but I was wrong because I have turned every Qed into Defined [1] involved in the proof of wellfounded [3] and it is still not simplifying [2]. Now, I am curious about how to prove this theorem [2].

Best,

Mukesh

[1] https://gist.github.com/mukeshtiwari/09e2278a1b5eb8ac23b47397ec044a12#file-agnishom-v-L13-L122

[2] https://gist.github.com/mukeshtiwari/09e2278a1b5eb8ac23b47397ec044a12#file-agnishom-v-L252

[3] https://gist.github.com/mukeshtiwari/09e2278a1b5eb8ac23b47397ec044a12#file-agnishom-v-L180

On Sat, Sep 2, 2023 at 9:53 AM Castéran Pierre <pierre.casteran AT gmail.com> wrote:

A version using Equations is on https://gist.github.com/Casteran/cb26e7fa8b185aa7f99f8b8048c6658e 

The remaining  Admitted should be trivial (just converting the well-roundedness of your order into an instance).

Pierre

Le 2 sept. 2023 à 03:26, Agnishom Chattopadhyay <agnishom AT cmi.ac.in> a écrit :

Hi all;

I have a function I am trying to define whose well-foundedness is not obvious. I am trying to do it in two different ways: (1) using Program Fixpoint and (2) using Function. In both cases, I am using the fixannot {wf ...}

However,

(1) When I try Program Fixpoint, the function can be defined. But it is opaque to `simpl`. How do I get around this? I need to be able to prove things about this function.

(2) When I use Function, I am getting a strange error message. The error message is not helpful because it references some variable names which I have not used.

Here is the Coq code: https://gist.github.com/Agnishom/1150d29732a6c727396fb6c118dbf375

Any help with this would be appreciated. I originally posted this on StackExchange, but I am corssposting here because I think this would be better suited for a threaded discussion rather than a Q/A style one.

Thanks!

--Agnishom