The Coq mailing list

[Castéran Pierre <pierre.casteran AT gmail.com>]

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