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 ?

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

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

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?

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

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?

if yes, you’ll need to state a combined theorem, prove it via `Combined Scheme`

, and then derive the two weakening theorems.

Thanks!

if no, you can just prove weakening for typing using `induction HT using typing_mut_ind`

(generated with `Scheme typing_mut_ind with …`

).

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

@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!)

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).

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