Talia Ringer (Feb 15 2022 at 19:22): 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 ?
Paolo Giarrusso (Feb 15 2022 at 19:26):You still need Scheme; induction works, but not with Combined Scheme.
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
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?
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.
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?
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.
Talia Ringer (Feb 15 2022 at 19:34):Thanks!
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 …).
Paolo Giarrusso (Feb 15 2022 at 19:35):_I_ always want Combined Scheme and pay the boilerplate for it :-| but YMMV
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!)
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).
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: Oct 04 2023 at 18:01 UTC