I think this is a bug -- or at least I would prefer to get a warning rather than Coq generating a non-sense induction scheme then have to debug it in the proof.

If you have an inductive predicate and call it recursively under an existential quantifier, Coq will just drop the recursive call completely with no warning. Here's an example

```
Section Foo.
Context {T: Type} {ktrans: T -> T -> Prop}.
Notation MP := (T -> Prop).
(* Exists strong until *)
Inductive ceu(p q: MP): MP :=
| MatchE: forall m,
q m ->
ceu p q m
| StepE: forall m,
p m ->
(exists m', ktrans m m' /\ (ceu p q) m') ->
ceu p q m.
Print ceu_ind.
```

The generated `ceu_ind`

is not even a fixpoint.

```
ceu_ind =
fun (p q P : MP) (f : forall m : T, q m -> P m)
(f0 : forall m : T,
p m -> (exists m' : T, ktrans m m' /\ ceu p q m') -> P m)
(t : T) (c : ceu p q t) =>
match c in (ceu _ _ t0) return (P t0) with
| MatchE _ _ m x => f m x
| StepE _ _ m x x0 => f0 m x x0
end
: forall p q P : MP,
(forall m : T, q m -> P m) ->
(forall m : T,
p m -> (exists m' : T, ktrans m m' /\ ceu p q m') -> P m) ->
forall t : T, ceu p q t -> P t
```

Here's a hand-written induction scheme `ceu_ind' `

that is more reasonable. I understand autogenerating those schemes is not always possible, my question is -- can we add a warning, like "the generated induction scheme ceu_ind is probably not what you want to do proofs by induction"

```
Definition ceu_ind':
forall [p q: MP] (P : MP),
(forall m, q m -> P m) -> (* base *)
(forall m,
p m -> (* [p] now*)
(exists m', ktrans m m' /\ ceu p q m') ->
(exists m', ktrans m m' /\ P m') ->
P m) ->
forall m, ceu p q m -> P m :=
fun p q P Hbase Hstep =>
fix F (t : T) (c : ceu p q t) {struct c}: P t :=
match c with
| MatchE _ _ m y => Hbase m y
| @StepE _ _ m y (ex_intro _ m' (conj tr h)) =>
Hstep m y (ex_intro _ m' (conj tr h)) (ex_intro _ m' (conj tr (F m' h)))
end.
End Foo.
```

is this the same problem as recursion under `list`

in inductives?

I agree that a warning would be nice

and just to be clear, changing `StepE`

as follow would fix the problem easily here right? One can still define `StepE`

by currying `StepE'`

appropriately

```
StepE': forall m m',
p m ->
ktrans m m' ->
ceu p q m' ->
ceu p q m.
```

I think you are right, defining as StepE' would be equivalent. Unsure if this is due to the simplicity of the example or it's always possible to push the existential quantifiers outside like this. I would guess no, as one can have arbitrary nest quantifiers.

But then I can ask the opposite question, why do two seemingly equivalent definitions (StepE, StepE') produce vastly different induction hypotheses?

It's basically a limitation of the compilation strategy, IIUC https://hal.inria.fr/hal-01897468 implements a better one (but I only glanced the abstract).

The generator of induction principles cannot handle recursive occurrences under _any_ type constructor — the canonical example is `List`

. One reason is in that case, generating the induction principle needs to reuse the type `Forall`

, or generate a variant `ForallT`

living in `Type`

.

You can search "Nested Inductive Types" in http://adam.chlipala.net/cpdt/html/Cpdt.InductiveTypes.html for more discussion.

`exists`

is notation for the inductive type family `ex`

. So what you define is a nested inductive. Coq does not generate good recursors for nested inductive because they generally involve writing additional utility inductive predicates. The case of hydras is illustrative: `Inductive hydra := list hydra`

.

there is an old out-of-date plugin that generates good induction principles for nested inductives: https://github.com/coq-contribs/nfix

However, the consensus in the community seems to be that people should roll their own induction principles using `Scheme`

or by defining them fully manually, like here

I see -- indeed `ex`

is an inductive definition which makes `ceu`

a mutual inductive predicate. My only push back with putting `ex`

in the same bag as `list`

and hand-rolled inductive definitions, is that `ex`

is not a library, it's part of Coq so special-treating it might not be completely unreasonable.

But regardless, my question has been answered and I thank you!

@Lef Ioannidis both ex and list are equally "libraries" or "part of Coq" in about the same way? And just FYI, ceu is nested not mutual, that'll matter when reading about them

Last updated: Jun 23 2024 at 04:03 UTC