Stream: Coq users

Topic: Fast hnf relexivity proof


view this post on Zulip Matthieu Sozeau (Nov 17 2020 at 11:18):

I have a value to compute that's really fast to get through hnf but takes ages with any other reduction strategy (cbn/lazy/vm/native). Is there a trick to produce a proof of t = hnf taccepted by the kernel just as fast? I can't think of any way to do it currently.

view this post on Zulip Gaëtan Gilbert (Nov 17 2020 at 12:56):

Does the order matter? ie maybe hnf t = t is faster

view this post on Zulip Gaëtan Gilbert (Nov 17 2020 at 12:56):

or maybe some reduction strat commands

view this post on Zulip Matthieu Sozeau (Nov 17 2020 at 12:56):

But we don't carry them to the kernel right?

view this post on Zulip Gaëtan Gilbert (Nov 17 2020 at 12:58):

Strategy and Opaque/Transparent go in the oracle used by kernel conversion

view this post on Zulip Pierre-Marie Pédrot (Nov 17 2020 at 12:58):

If you ask me, it's a good thing that hnf is not part of the kernel.

view this post on Zulip Matthieu Sozeau (Nov 17 2020 at 12:59):

Ah you mean an unfolding strategy, sorry I misunderstood

view this post on Zulip Matthieu Sozeau (Nov 17 2020 at 13:00):

Pierre-Marie Pédrot said:

If you ask me, it's a good thing that hnf is not part of the kernel.

TCB-wise I understand, but its still a pity my tactic takes 3sec and Qed 1 min

view this post on Zulip Pierre-Marie Pédrot (Nov 17 2020 at 13:01):

You might hack your way around adding enough casts here and there...

view this post on Zulip Matthieu Sozeau (Nov 17 2020 at 13:14):

Hmm, I found another way by changing the big proof term I got by an opaque thing.


Last updated: Jan 31 2023 at 12:01 UTC