Stream: Coq users

Topic: custom induction principles


view this post on Zulip Vadim Zaliva (Nov 16 2023 at 17:36):

Consider the self-contained example here: https://gist.github.com/vzaliva/9f616fcd49043f5ba390743d1574c4a0. Initially, I defined a type mem_value_indt for which the default induction principle generated by Coq was inadequate. For instance, it did not consider MVarray to be a recursive case. I addressed this with mem_value_indt_induction, which I was able to prove successfully. Similarly, I defined the inductive predicate mem_value_indt_eq for which I attempted to establish a custom induction principle, as I did earlier. However, the proof fails on "Qed" with the message, "Recursive definition of IH is ill-formed. Not enough abstractions in the definition." I never used custom induction principles before and have several questions: 1) Am I doing this right (for these types)? 2) If there is a way to associate my custom induction principle with data type so I do not need to specify it each time in induction tactics. 3) Does the principle generated byScheme Induction differs from the one generated by default? 4) Perhaps providing a measure function to fix tactics in the prove above will fix the error?

view this post on Zulip Gaëtan Gilbert (Nov 16 2023 at 17:39):

the error is because you need to intro at least n after fix f n

view this post on Zulip Théo Winterhalter (Nov 16 2023 at 17:39):

One way to have Coq pick it up by default is to first tell Coq not to generate the bogus induction principle, and then proceed to name your custom one has Coq would have done.

view this post on Zulip Vadim Zaliva (Nov 16 2023 at 17:40):

@Théo Winterhalter how to tell it not to generate one? use Variant instead of Inductive and when define following _ind naming convention?

view this post on Zulip Gaëtan Gilbert (Nov 16 2023 at 17:41):

Lemma foo : unit -> nat -> nat.
Proof.
  fix f 2.
  intros x;destruct x;intros n;exact 0. (* bad: destruct x before intros n *)
  Fail Qed.

view this post on Zulip Théo Winterhalter (Nov 16 2023 at 17:43):

Vadim Zaliva said:

Théo Winterhalter how to tell it not to generate one? use Variant instead of Inductive and when define following _ind naming convention?

I'm guessing Unset Elimination Schemes. https://coq.inria.fr/refman/proofs/writing-proofs/reasoning-inductives.html#coq:flag.Elimination-Schemes

view this post on Zulip Théo Winterhalter (Nov 16 2023 at 17:44):

Variant would work, but also it doesn't allow you to have recursive types, so it only works when you don't care about induction.

view this post on Zulip Vadim Zaliva (Nov 16 2023 at 17:46):

@Gaëtan Gilbert if I modify my example to do intros x y H; fix IH 3 I am getting "Error: Not enough products."

view this post on Zulip Meven Lennon-Bertrand (Nov 16 2023 at 17:49):

Yes, Unset Elimination Schemes. is the way to go. Basically, if the automatically generated induction principle for foo is rubbish, the usual yoga is:

Unset Elimination Scheme.

Inductive foo  :  :=

.

Set Elimination Schemes.

Lemma foo_rec :  :=  .
(* If you need other induction principles in other sorts, define foo_rect, foo_ind… accordingly *)

The Scheme command, when used with non-mutual inductive types is afaik what Coq uses internally to generate the induction principle. In the case of mutual ones, it gives a bit more flexibility to define different version of mutual induction principles. It is too weak for nested inductive types, where you have to do things by hand (sadly).

view this post on Zulip Vadim Zaliva (Nov 16 2023 at 17:57):

@Gaëtan Gilbert also in mem_value_indt_induction proof I used fix IH 1 before doing intros x and it worked.

view this post on Zulip Gaëtan Gilbert (Nov 16 2023 at 18:20):

Vadim Zaliva said:

Gaëtan Gilbert if I modify my example to do intros x y H; fix IH 3 I am getting "Error: Not enough products."

that's not how it should be, it should be fix IH 3;intros x y H

view this post on Zulip Gaëtan Gilbert (Nov 16 2023 at 18:22):

Vadim Zaliva said:

Gaëtan Gilbert also in mem_value_indt_induction proof I used fix IH 1 before doing intros x and it worked.

you do fix IH 1; destruct m with the goal forall m, ... so destruct m does the intro (equivalent to intros m;destruct m)

view this post on Zulip Vadim Zaliva (Nov 16 2023 at 18:44):

@Gaëtan Gilbert thank you so much! it worked. Now I would love to understand why :)


Last updated: Jun 13 2024 at 19:02 UTC