Anton Golov (they/them) (Nov 27 2022 at 15:20): Anton Golov (they/them) (Nov 27 2022 at 15:20):Hi, I have some inductive data types with some inductive predicates defined on them, like
Inductive foo : X → Prop :=
| A_foo x : foo x → foo (A x)
| B_foo : foo B
| ...
For a single data type X this is fine, but when I have multiple data types X, Y, Z that means I end up with many predicates X_foo, Y_foo, Z_foo, which is a bit ugly.
I was hoping I could do something like
Class Foo (S : Set) := foo : S → Prop.
Global Arguments foo {_} {_} / _ : assert.
Inductive X_foo : Foo X :=
| ... same rules with X_foo ...
Global Existing Instance X_foo.
This sort of works, but when I do any kind of reasoning with it I end up with half my goals/hypotheses being foo and the other half being X_foo, because my lemmas are stated in terms of foo, but any unfolding reveals the X_foousage in recursive positions. This means that eauto works very poorly, since e.g. inductive hypotheses don't match syntactically.
Is there any nice way to deal with this? Or should I just use X_foo throughout and not try to use typeclasses for this?
Paolo Giarrusso (Nov 27 2022 at 17:34):one thing that might help is that unlike eauto, typeclasses eauto can unfold definitions... OTOH, that won't fix other tactics and goal display...
Paolo Giarrusso (Nov 27 2022 at 17:39):one possible strategy is to _not_ unfold foo in simpl, but for that you'd want to use foo instead of X_foo everywhere, even in A_foo. Which seems to work automatically!
Paolo Giarrusso (Nov 27 2022 at 17:41):self-contained example:
From Coq Require Import Utf8.
Inductive X := A (x : X) | B.
Class Foo (S : Set) := foo : S → Prop.
Global Arguments foo {_} {_} _ : assert.
Inductive X_foo : Foo X :=
| A_foo x : foo x → foo (A x)
| B_foo : foo B.
Global Existing Instance X_foo.
the trick is that X_foo is already used as an instance in recursive calls (which I wasn't sure about).
More in general, local assumptions of typeclass type are always considered as instances; I wasn't sure X_foo would be treated as a local assumption, but it makes sense.
Would tactics unfold foo? Seems not: I tested destruct, inversion, simpl and cbn. Even inversion seems well-behaved on such an inductive!
Goal ∀ x, foo (A x) -> foo x.
Proof.
Fail progress simpl.
Fail progress cbn.
inversion_clear 1. Show. easy.
Qed.
"use the typeclass in recursive occurrences" is an idea that I've also used elsewhere for _fixpoints_ (https://github.com/Blaisorblade/dot-iris/blob/63ea484cc5a55adecd60165422eb570f9fde2ecc/theories/Dot/syn/syn.v#L141); but here with inductives it seems to work even better! Would you let me know if you run into issues with this?
Anton Golov (they/them) (Nov 27 2022 at 18:43):Thanks, this is really interesting! In particular, I didn't expect that definition of X_foo to compile at all. I'm a bit confused, why does it? Is it parametrised over an instance of Foo X, which is then trivially satisfied once we make X_foo such an instance?
Anton Golov (they/them) (Nov 27 2022 at 18:44):I'll give this a shot and I'll check out typeclasses eauto, thanks!
Anton Golov (they/them) (Nov 27 2022 at 18:51):I think this works to some degree, but it doesn't play well with Hint Constructors X_foo. (since that uses those hints for X_foo x but not foo x. I suppose I could introduce an X_foo x → foo x lemma that would solve that, though, but any other suggestions are welcome
Paolo Giarrusso (Nov 27 2022 at 19:20):since that uses those hints for X_foo x but not foo x
That's not what I see with the code I posted. Note that my suggestion should avoid the need for typeclasses eauto; both eauto and typeclasses eauto work correctly:
Create HintDb foo.
#[export] Hint Constructors X_foo : foo.
Print HintDb foo.
Goal foo (A B).
Succeed now typeclasses eauto with foo.
eauto with foo.
Qed.
Even with core
#[export] Hint Constructors X_foo : core.
Print HintDb core.
Goal foo (A B).
Succeed now typeclasses eauto with core.
eauto.
Qed.
and that example should also work with Global instead of #[export]
Paolo Giarrusso (Nov 27 2022 at 19:24):Is it parametrised over an instance of Foo X, which is then trivially satisfied once we make X_foo such an instance?
No no: X_foo is just used as an instance in its own definition. Global Existing Instance X_foo. is irrelevant here.
Enable Printing Implicits, then
About A_foo .
(*
A_foo : ∀ x : X, @foo X X_foo x → @foo X X_foo (A x)
A_foo is not universe polymorphic
Arguments A_foo x _
Expands to: Constructor ind_tc.A_foo
*)
No no: X_foo is just used as an instance in its own definition.
Ah, thanks, I see! Interesting that that's allowed, I hadn't realised
Anton Golov (they/them) (Nov 27 2022 at 19:30):Huh, that's strange, your example with foo works but in my code a similar construction doesn't (but does if I add those lemmas), let me see what could be wrong.
Anton Golov (they/them) (Nov 27 2022 at 19:50):Oh, I found my issue! I'd forgotten to update not only the parameters but also the return types of A_foo and other constructors. With that corrected it works as expected
Anton Golov (they/them) (Nov 27 2022 at 19:51):Thanks again! Interesting that Coq allows defining things like this, I'd always assumed that the right-hand side of a constructor has to really be the type in question in some very strong sense
Notification Bot (Nov 27 2022 at 20:07):Anton Golov (they/them) has marked this topic as resolved.
Notification Bot (Nov 27 2022 at 20:57):Anton Golov (they/them) has marked this topic as unresolved.
Anton Golov (they/them) (Nov 27 2022 at 21:00):Actually, follow-up question on this: is there anything similar I can do with Fixpoints? I was hoping for something like
Class Bar (S : Set) := bar : S → S.
Global Arguments bar {_} {_} _.
Fixpoint X_bar : Bar X := match ... end.
This doesn't work, though, as the fixpoint needs a parameter (so I can't put the match in a lambda).
Is there any standard way of solving this?
Paolo Giarrusso (Nov 27 2022 at 22:25):see https://github.com/Blaisorblade/dot-iris/blob/63ea484cc5a55adecd60165422eb570f9fde2ecc/theories/Dot/syn/syn.v#L140-L215, as mentioned above...
but there is one extra downside:
Paolo Giarrusso (Nov 27 2022 at 22:29):In that fixpoint, recursive occurrences of Rename tm use tm_rename, while occurrences outside will use rename_tm.
I recall Existing Instance tm_rename. fails, because tm_rename's type isn't literally Rename tm but only convertible to it.
However, what should work is Hint Extern 0 (Rename tm) => apply tm_rename : typeclass_instances.. Using an hint in typeclass_instances is very similar to using an instance (except if apply differs), but it's more flexible.
Paolo Giarrusso (Nov 27 2022 at 22:31):I should say that I have _not_ had many problems with the tm_rename vs rename_tm mismatch in that project, but it's probably some amount of luck.
Anton Golov (they/them) (Nov 27 2022 at 22:34):Sorry, missed that, that makes sense.
I guess there may be fewer issues because it disappears after simplifying one step, which is where the mismatch usually caused issues for me.
Cool, this looks like it should work!
Paolo Giarrusso (Nov 27 2022 at 22:54):Good point; I'm not sure that will always happen automatically, but sth like Arguments rename_tm /. should make help simpl/cbn do it :-)
Anton Golov (they/them) (Nov 27 2022 at 23:05):Oh, neat, I'm still figuring out Arguments, I'll give that a try
Last updated: Oct 01 2023 at 18:01 UTC