The Coq mailing list

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

Btw, I am wondering if we could have two versions of the same proof, one closed by Qed and the other by Defined, in the Coq standard library, it would make life easier for many people. Depending on the need, they can pick the Qed or Defined. Are there any cons for this, other than duplicating a massive codebase?

Best,

Mukesh

On Sat, Sep 2, 2023 at 6:38 PM mukesh tiwari <mukeshtiwari.iiitm AT gmail.com> wrote:

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