Stream: Coq users

Topic: Mutual induction question


view this post on Zulip Talia Ringer (Feb 15 2022 at 19:22):

Is there a way to get Coq to define mutual induction principles automatically, and then apply them with the induction tactic? Or do you still need to use Scheme and define your own automation as in CPDT: http://adam.chlipala.net/cpdt/html/InductiveTypes.html ?

view this post on Zulip Paolo Giarrusso (Feb 15 2022 at 19:26):

You still need Scheme; induction works, but not with Combined Scheme.

view this post on Zulip Paolo Giarrusso (Feb 15 2022 at 19:27):

But if you need all the "clauses" of your proof rather than just for some main type, you want combined scheme

view this post on Zulip Talia Ringer (Feb 15 2022 at 19:28):

Paolo Giarrusso said:

But if you need all the "clauses" of your proof rather than just for some main type, you want combined scheme

can you explain what you mean by this?

view this post on Zulip Paolo Giarrusso (Feb 15 2022 at 19:31):

let me try again; suppose you have a mutually inductive for, dunno, typing and subtyping, and want to prove weakening.

view this post on Zulip Paolo Giarrusso (Feb 15 2022 at 19:32):

Weakening for typing requires proving weakening for subtyping in a mutual induction, but do you want to state weakening for subtyping, say to use it elsewhere?

view this post on Zulip Paolo Giarrusso (Feb 15 2022 at 19:33):

if yes, you’ll need to state a combined theorem, prove it via Combined Scheme, and then derive the two weakening theorems.

view this post on Zulip Talia Ringer (Feb 15 2022 at 19:34):

Thanks!

view this post on Zulip Paolo Giarrusso (Feb 15 2022 at 19:34):

if no, you can just prove weakening for typing using induction HT using typing_mut_ind (generated with Scheme typing_mut_ind with …).

view this post on Zulip Paolo Giarrusso (Feb 15 2022 at 19:35):

_I_ always want Combined Scheme and pay the boilerplate for it :-| but YMMV

view this post on Zulip Talia Ringer (Feb 17 2022 at 22:48):

@Paolo Giarrusso this was _extremely_ useful, thanks. We got the right induction principle going today (though, boy, without support from induction, passing in the right motives by hand is hard!)

view this post on Zulip Paolo Giarrusso (Feb 17 2022 at 22:59):

I'm happy it helped! Re motives that's true... I sometimes have used definitions to help apply infer the motives — a goal like(∀ e T (HT : Γ t⊢ₜ e : T), fundamental_typed_def HT) ∧ ..., where fundamental_typed_def is essentially the motive, is easier to match against (∀ e T (HT : Γ t⊢ₜ e : T), P HT) ∧ .... I'm not sure if the game is that worthwhile, tho you do write the statement twice instead of three times (and you could maybe get to write it once using ltac:(eval red in ... ) to unfold fundamental_typed_def in the extracted statement). Here's an example:

https://github.com/Blaisorblade/dot-iris/blob/7a9ae517196631ee65b9820806bcab517192a1f3/theories/Dot/fundamental.v#L23-L41
https://github.com/Blaisorblade/dot-iris/blob/7a9ae517196631ee65b9820806bcab517192a1f3/theories/Dot/fundamental.v#L88-L100

(induction principle from https://github.com/Blaisorblade/dot-iris/blob/7a9ae517196631ee65b9820806bcab517192a1f3/theories/Dot/typing/typing.v#L109-L112).

view this post on Zulip Talia Ringer (Feb 17 2022 at 23:41):

Makes sense! Yeah we ended up having to solve a difficult unification problem to start the proof, but then after that the proof was very nice


Last updated: Jun 20 2024 at 11:02 UTC