According to the docs, when I declare a function with Equations, I should get an induction principle `f_ind`

to do inductive proofs about that function. However, such a principle does not seem to be generated for my function. What could be going on here?

My definition looks like this:

```
Equations type_interp (ve : val_or_expr) (A : type) (delta : tyvar_interp) (W : world) :
Prop by wf (type_interp_measure ve A) := { ... }.
```

This is not mutually recursive with anything else, just a plain recursive definition, albeit with a custom measure.

There is a `type_interp_elim`

, but that doesn't seem to be strong enough for inductive reasoning. There's also `type_interp_graph_ind`

but that's not useful, it's about `type_interp_graph`

which seems to be some internal thing.

I can do induction over the measure of course, but it would be much more convenient to have a custom induction principle for my function, given that I have already proven that the measure decreases and it's silly that I have to prove this again for the induction.

looking at `type_interp_elim`

again it provides some of the recursive cases but not enough...

but also the docs say

quations also automatically generates a mutually-inductive relation corre-

sponding to the graph of the programs, whose first inductive is named f_ind. It

automatically shows that the functions respects their graphs (lemma f_ind_fun)

and derives from this proof an elimination principle named f_elim.

so I would expect f_ind to exist, not just f_fun

for instance I have these two cases

```
(** forall case *)
type_interp (inj_val v) (forall: A) delta W =>
exists e, v = TLamV e /\
forall tau : sem_type, type_interp (inj_expr e) A (tau .: delta) W;
(** exists case *)
type_interp (inj_val v) (exists: A) delta W =>
exists v', v = PackV v' /\
exists tau : sem_type, type_interp (inj_val v') A (tau .: delta) W;
```

in `_elim`

, for `exists:`

I get

```
→ (∀ v (A : {bind type}) delta W,
(∀ v' tau,
P (inj_val v') A (tau .: delta) W
(type_interp (inj_val v') A (tau .: delta) W))
→ P (inj_val v) (exists: A)%ty delta W
(∃ v', v = (pack v')%V ∧ (∃ tau, type_interp (inj_val v') A (tau .: delta) W)))
```

which looks good, I get `P`

for some smaller stuff and have to show it for the bigger stuff. for for `forall:`

I just get

```
→ (∀ v (A : {bind type}) delta W,
P (inj_val v) (forall: A)%ty delta W
(∃ e, v = (Lam: e)%V ∧ (∀ tau, type_interp (inj_expr e) A (tau .: delta) W)))
```

which leads to an unprovable goal

for now i am using this rune

```
remember (ve, A) as x.
revert ve A Heqx.
induction (lt_wf_0_projected (B := val_or_expr*type)
(fun '(ve, A) => type_interp_measure ve A) x) as [x _ IH].
```

where `lt_wf_0_projected`

is an std++ lemma, not sure if a similar lemma exists in the stdlib

```
(** Given a measure/size [f : B -> nat], you can do induction on the size of
[b : B] using [induction (lt_wf_0_projected f b)]. *)
Lemma lt_wf_0_projected {B} (f : B -> nat) : well_founded (fun x y => f x < f y).
```

Interesting, if it misses the recursive call in the forall case then it's a bug

The eliminator is indeed the _elim constant

okay so the docs are wrong then?

they say "Equations also automatically generates a mutually-inductive relation corre-

sponding to the graph of the programs, whose first inductive is named f_ind."

but only "f_elim" exists

filed https://github.com/mattam82/Coq-Equations/issues/575 for the docs issue

and filed https://github.com/mattam82/Coq-Equations/issues/576 for the missing recursive call

Last updated: Oct 13 2024 at 01:02 UTC