The Coq mailing list

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

Hi everyone,

I spoke too early and my solution, turning every Qed into Defined, works.  Here is the proof [1].

Best,

Mukesh

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

On Sat, Sep 2, 2023 at 3:13 PM Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr> wrote:

Hi all,

My 2 cents. Why not write all_parse_trees

as a fully specified term, relating the output

to the input in a way that characterizes the

output uniquely, ie

all_parse_trees : forall (l :  list A) (n : nat) (p : Regex * nat) -> { o : list parse_tree | all_parse_trees_spec l n p o }

If all_parse_trees_spec mimics the computation of all_parse_trees at the level of Prop,

this is usually an easy task to fullfil.

Then prove properties of all_parse_trees from that spec. In general, this works

around having to evaluate the proofs of the propositions that contribute to the proof

of the Acc(essibility) argument.

D.

---

De: "mukesh tiwari" <mukeshtiwari.iiitm AT gmail.com>
À: "coq-club" <coq-club AT inria.fr>
Envoyé: Samedi 2 Septembre 2023 13:20:08
Objet: Re: [Coq-Club] Non obvious recursion (Issue with Function + Can't unfold Program Fixpoint)

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