Stream: Coq users

Topic: Coq generates non-fix induction schemes under existential


view this post on Zulip Lef Ioannidis (Oct 20 2023 at 14:33):

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.

view this post on Zulip Paolo Giarrusso (Oct 20 2023 at 15:21):

is this the same problem as recursion under list in inductives?

view this post on Zulip Paolo Giarrusso (Oct 20 2023 at 15:22):

I agree that a warning would be nice

view this post on Zulip Paolo Giarrusso (Oct 20 2023 at 15:24):

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.

view this post on Zulip Lef Ioannidis (Oct 20 2023 at 16:01):

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?

view this post on Zulip Paolo Giarrusso (Oct 20 2023 at 16:58):

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.

view this post on Zulip Dominique Larchey-Wendling (Oct 21 2023 at 09:06):

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.

view this post on Zulip Karl Palmskog (Oct 21 2023 at 09:15):

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

view this post on Zulip Lef Ioannidis (Oct 22 2023 at 19:22):

I see -- indeed ex is an inductive definition which makes ceua 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!

view this post on Zulip Paolo Giarrusso (Oct 23 2023 at 09:42):

@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