walker (Sep 25 2022 at 21:05): walker (Sep 25 2022 at 21:05):I have a definitionthat looks like
Program Fixpoint is_weak_value (globs: stringmap Term) (t: Term) {measure (size globs) }: bool :=
match t with
....
| gvar x => match globs !! x with
| Some t => is_weak_value (delete x globs) t
| None => false
end
.....
end.
I truncated the useless parts because code won't run anyways without copying lots of stuff.
So I discovered program_simpl which solved is_weak_value M t = true for all t values exept gvar
In gvar it is stuck at is_weak_value M (gvar x) = true which is not ideal. I would have hoped to get the internal match statement which will be trivial to solve on my end.
I tried simpl/unfold but neither worked, I thought Set Program Cases. would help but it didn't.
Also at this stage I wanted to ask Program Fixpoint is the correct way to do what I am trying to (recursive function with no clear structural decreasing member).
Paolo Giarrusso (Sep 25 2022 at 21:08):what are you trying to prove? Is this a theorem about is_weak_value, or the obligations for its definition? Which obligation?
walker (Sep 25 2022 at 21:10):I am trying to prove a theorem about is_weak_value obligations are fulfilled.
Paolo Giarrusso (Sep 25 2022 at 21:10):Not sure I understand: is this about Next Obligation?
Paolo Giarrusso (Sep 25 2022 at 21:10):the ones after the definition?
walker (Sep 25 2022 at 21:10):missing comma :sweat_smile:
Paolo Giarrusso (Sep 25 2022 at 21:11):aah I see
walker (Sep 25 2022 at 21:11):no, obligations are proven completely.
walker (Sep 25 2022 at 21:11):I am trying to prove equivalence between this function and equivalent inductive definition.
Paolo Giarrusso (Sep 25 2022 at 21:11):that is, _all_ obligations are proven completely
Paolo Giarrusso (Sep 25 2022 at 21:11):okay
Paolo Giarrusso (Sep 25 2022 at 21:12):aah I see: you'd like to reduce is_weak_value M (gvar x) = true to the right-hand side?
walker (Sep 25 2022 at 21:12):yes exactly
Paolo Giarrusso (Sep 25 2022 at 21:13):in general, simpl can't simplify well-founded recursive functions: the reduction equations you want are not definitional.
Paolo Giarrusso (Sep 25 2022 at 21:13):something/somebody needs to prove unfolding lemmas instead, and Program does not do that. I recommend using Equations instead.
walker (Sep 25 2022 at 21:14):alright.
Paolo Giarrusso (Sep 25 2022 at 21:14):(technically, Function also proves unfolding lemmas, but it's a much older package and isn't actively maintained, hence I suggest Equations)
Paolo Giarrusso (Sep 25 2022 at 21:14):see https://github.com/mattam82/Coq-Equations
Paolo Giarrusso (Sep 25 2022 at 21:15):example: https://github.com/mattam82/Coq-Equations/blob/master/examples/wfrec.v#L10-L28
walker (Sep 25 2022 at 21:15):I see, so Equations is the currently community-blessed approach.
walker (Sep 25 2022 at 21:15):Paolo Giarrusso said:
example: https://github.com/mattam82/Coq-Equations/blob/master/examples/wfrec.v#L10-L28
This is exactly what I needed!
Paolo Giarrusso (Sep 25 2022 at 21:16):I'm not a community representative, but IMHO yes :-)
Paolo Giarrusso (Sep 25 2022 at 21:20):As a warning: stdpp sets Global Obligation Tactic := idtac, while Equations has a bunch of choices depending how you load it:
https://github.com/mattam82/Coq-Equations/blob/acf7fbcfd8387dcc069ffa4124d439936ea3d50b/theories/Prop/Equations.v#L20-L21
https://github.com/mattam82/Coq-Equations/blob/a65e6511038bfc33ed87b8526b5a3e4e3041b1a8/theories/Type/Loader.v#L28
So importing equations first or last will change your Obligations.
Gaëtan Gilbert (Sep 25 2022 at 21:27):Global Obligation Tactic acts on both Require (including through transitive deoendency) and Import btw
Paolo Giarrusso (Sep 25 2022 at 21:31):Fail #[export] Obligation Tactic := idtac. :-(
walker (Sep 25 2022 at 21:33):I am not sure I get the point you are trying to make.
Gaëtan Gilbert (Sep 25 2022 at 21:35):https://github.com/coq/coq/pull/15274
walker (Sep 25 2022 at 21:38):I think I will need to first go though the Equations tutorial book before I can use it properly.
walker (Sep 25 2022 at 21:39):is_weak_value _ (gvar x) with globs !! x :=
{ | Some t => is_weak_value (delete x globs) t
| None => false
};
Equation generated the correct obligation here:
size (delete x globs) < size globs
But it missed a very important piece of information which is assuming that globs !! x = Some t.
Paolo Giarrusso (Sep 25 2022 at 22:41):you might need the "inspect pattern" here
https://github.com/mattam82/Coq-Equations/blob/82dc46c6c0ed1e28436ab48f8a28fe7618f2da40/examples/Basics.v#L527-L538
compared to the example, Definition inspect is now part of the library itself:
https://github.com/mattam82/Coq-Equations/blob/f9befb9ab5bbaddb50014151dd07757f53dc797a/theories/Prop/Logic.v
Paolo Giarrusso (Sep 25 2022 at 22:42):Program did that automatically, but the downside was that many pattern matches suffered a quadratic blow-up "just in case" somebody needed the equality
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: Oct 01 2023 at 18:01 UTC