Stream: Coq users

Topic: ✔ Stuck with Program Fixpoint


view this post on Zulip walker (Sep 26 2022 at 20:14):

So through some miracle I was able to prove the theorem (by half baked understanding of simp/autorewrite tactic).

view this post on Zulip walker (Sep 26 2022 at 20:15):

The problem is all the lemmas created by Equations are local and I am not sure how to overwrite that.

view this post on Zulip walker (Sep 26 2022 at 20:16):

I usually have file for code that extracts (I hope that Equations will not end up being extraction disaster) and another file for all theorems/lemmas. and when I import the file that contains the Equations definitions, I cannot access any of the lemmas (hence simp does not work)

view this post on Zulip Karl Palmskog (Sep 26 2022 at 20:26):

Equations names all its lemmas by predictable suffixes to the name you pass to it. If your Equations definition is called my_def, I suggest you do something like Search "my_def". to see lemmas/terms available that were generated by Equations.

view this post on Zulip walker (Sep 26 2022 at 20:29):

Yes they were generated by Equations.

view this post on Zulip walker (Sep 26 2022 at 20:30):

in file called Term.v
I do the following

Equations is_weak_value (globs: stringmap Term) (t: Term): bool by wf (size globs) lt := .........

view this post on Zulip walker (Sep 26 2022 at 20:31):

simp and funelim works, and I can see all the Equation defined Lemmas in Search.

view this post on Zulip walker (Sep 26 2022 at 20:31):

in model.v I do:

From Equations Require Import Equations.
From Packagename Require Import terms.

view this post on Zulip walker (Sep 26 2022 at 20:31):

I can see is_weak_value but not the lemmas.

view this post on Zulip walker (Sep 26 2022 at 20:32):

I will try make clean and rebuilt to make sure it is not some cached binaries.

view this post on Zulip Karl Palmskog (Sep 26 2022 at 20:32):

if the file is called Term.v, then the module will be called Term

view this post on Zulip walker (Sep 26 2022 at 20:34):

that was a mistake in my typing here!

view this post on Zulip walker (Sep 26 2022 at 20:34):

but apparently make clean & make fixed it somehow.

view this post on Zulip walker (Sep 26 2022 at 20:34):

once again Thanks a lot @Karl Palmskog & @Paolo Giarrusso

view this post on Zulip Notification Bot (Sep 26 2022 at 20:34):

walker has marked this topic as resolved.


Last updated: Jan 29 2023 at 05:03 UTC