Stream: Coq users

Topic: ✔ Stuck with Program Fixpoint


view this post on Zulip 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).

view this post on Zulip 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?

view this post on Zulip walker (Sep 25 2022 at 21:10):

I am trying to prove a theorem about is_weak_value obligations are fulfilled.

view this post on Zulip Paolo Giarrusso (Sep 25 2022 at 21:10):

Not sure I understand: is this about Next Obligation?

view this post on Zulip Paolo Giarrusso (Sep 25 2022 at 21:10):

the ones after the definition?

view this post on Zulip walker (Sep 25 2022 at 21:10):

missing comma :sweat_smile:

view this post on Zulip Paolo Giarrusso (Sep 25 2022 at 21:11):

aah I see

view this post on Zulip walker (Sep 25 2022 at 21:11):

no, obligations are proven completely.

view this post on Zulip walker (Sep 25 2022 at 21:11):

I am trying to prove equivalence between this function and equivalent inductive definition.

view this post on Zulip Paolo Giarrusso (Sep 25 2022 at 21:11):

that is, _all_ obligations are proven completely

view this post on Zulip Paolo Giarrusso (Sep 25 2022 at 21:11):

okay

view this post on Zulip 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?

view this post on Zulip walker (Sep 25 2022 at 21:12):

yes exactly

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip walker (Sep 25 2022 at 21:14):

alright.

view this post on Zulip 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)

view this post on Zulip Paolo Giarrusso (Sep 25 2022 at 21:14):

see https://github.com/mattam82/Coq-Equations

view this post on Zulip Paolo Giarrusso (Sep 25 2022 at 21:15):

example: https://github.com/mattam82/Coq-Equations/blob/master/examples/wfrec.v#L10-L28

view this post on Zulip walker (Sep 25 2022 at 21:15):

I see, so Equations is the currently community-blessed approach.

view this post on Zulip 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!

view this post on Zulip Paolo Giarrusso (Sep 25 2022 at 21:16):

I'm not a community representative, but IMHO yes :-)

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Sep 25 2022 at 21:27):

Global Obligation Tactic acts on both Require (including through transitive deoendency) and Import btw

view this post on Zulip Paolo Giarrusso (Sep 25 2022 at 21:31):

Fail #[export] Obligation Tactic := idtac. :-(

view this post on Zulip walker (Sep 25 2022 at 21:33):

I am not sure I get the point you are trying to make.

view this post on Zulip Gaëtan Gilbert (Sep 25 2022 at 21:35):

https://github.com/coq/coq/pull/15274

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

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: Mar 28 2024 at 23:01 UTC