walker (Sep 26 2022 at 20:14): 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).
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.
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)
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.
walker (Sep 26 2022 at 20:29):Yes they were generated by Equations.
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 := .........
simp and funelim works, and I can see all the Equation defined Lemmas in Search.
walker (Sep 26 2022 at 20:31):in model.v I do:
From Equations Require Import Equations.
From Packagename Require Import terms.
I can see is_weak_value but not the lemmas.
walker (Sep 26 2022 at 20:32):I will try make clean and rebuilt to make sure it is not some cached binaries.
Karl Palmskog (Sep 26 2022 at 20:32):if the file is called Term.v, then the module will be called Term
walker (Sep 26 2022 at 20:34):that was a mistake in my typing here!
walker (Sep 26 2022 at 20:34):but apparently make clean & make fixed it somehow.
walker (Sep 26 2022 at 20:34):once again Thanks a lot @Karl Palmskog & @Paolo Giarrusso
Notification Bot (Sep 26 2022 at 20:34):walker has marked this topic as resolved.
Last updated: Jan 29 2023 at 05:03 UTC