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