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).
what are you trying to prove? Is this a theorem about is_weak_value
, or the obligations for its definition? Which obligation?
I am trying to prove a theorem about is_weak_value
obligations are fulfilled.
Not sure I understand: is this about Next Obligation
?
the ones after the definition?
missing comma :sweat_smile:
aah I see
no, obligations are proven completely.
I am trying to prove equivalence between this function and equivalent inductive definition.
that is, _all_ obligations are proven completely
okay
aah I see: you'd like to reduce is_weak_value M (gvar x) = true
to the right-hand side?
yes exactly
in general, simpl
can't simplify well-founded recursive functions: the reduction equations you want are not definitional.
something/somebody needs to prove unfolding lemmas instead, and Program
does not do that. I recommend using Equations
instead.
alright.
(technically, Function
also proves unfolding lemmas, but it's a much older package and isn't actively maintained, hence I suggest Equations
)
see https://github.com/mattam82/Coq-Equations
example: https://github.com/mattam82/Coq-Equations/blob/master/examples/wfrec.v#L10-L28
I see, so Equations is the currently community-blessed approach.
Paolo Giarrusso said:
example: https://github.com/mattam82/Coq-Equations/blob/master/examples/wfrec.v#L10-L28
This is exactly what I needed!
I'm not a community representative, but IMHO yes :-)
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 Obligation
s.
Global Obligation Tactic acts on both Require (including through transitive deoendency) and Import btw
Fail #[export] Obligation Tactic := idtac.
:-(
I am not sure I get the point you are trying to make.
https://github.com/coq/coq/pull/15274
I think I will need to first go though the Equations tutorial book before I can use it properly.
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
.
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
Program
did that automatically, but the downside was that many pattern matches suffered a quadratic blow-up "just in case" somebody needed the equality
So through some miracle I was able to prove the theorem (by half baked understanding of simp/autorewrite tactic).
The problem is all the lemmas created by Equations are local and I am not sure how to overwrite that.
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)
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.
Yes they were generated by Equations.
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.
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.
I will try make clean and rebuilt to make sure it is not some cached binaries.
if the file is called Term.v
, then the module will be called Term
that was a mistake in my typing here!
but apparently make clean & make fixed it somehow.
once again Thanks a lot @Karl Palmskog & @Paolo Giarrusso
walker has marked this topic as resolved.
Last updated: Oct 01 2023 at 18:01 UTC