Lukas Stevens (Aug 13 2020 at 08:33): Lukas Stevens (Aug 13 2020 at 08:33):Consider the locale comp_fun_commute: it fixes f and assumes f x o f y = f y o f x.What I want to have is comp_fun_commute_on that fixes f and A and assumes x ∈ A ⟹ y ∈ A ⟹ f y ∘ f x = f x ∘ f y. Is there a trick to generalise the first locale to the second one, without changing all the theorems and proofs?
Manuel Eberl (Aug 13 2020 at 09:04):Yeah that's what types-to-sets does
Manuel Eberl (Aug 13 2020 at 09:04):probably not worth it in this case though
Manuel Eberl (Aug 13 2020 at 09:05):you might be able to do some trickery like artificially defining a new f relativised to A that returns some dummy value for everything not in A, perhaps, and thus fulfils the equality on the entire type
Lukas Stevens (Aug 13 2020 at 10:06):Is Types_To_Sets something you could use in the distribution?
Lukas Stevens (Aug 13 2020 at 10:07):Asking because it introduces additional axioms
Manuel Eberl (Aug 13 2020 at 11:28):I think the jury is still out on that.
Manuel Eberl (Aug 13 2020 at 11:29):But I think there probably wouldn't be too much opposition to it
Manuel Eberl (Aug 13 2020 at 11:29):regardless, I doubt it's worth it for your example
Manuel Eberl (Aug 13 2020 at 11:30):the proofs are probably pretty simple
Manuel Eberl (Aug 13 2020 at 11:30):and you'd probably have to restate the theorems in their relativised form anyway if you wanted to lift them over with types-to-sets, so that still involves significant boilerplate
Lukas Stevens (Aug 13 2020 at 11:54):The most annoying thing in my example is that you have to duplicate most theorems since you need to generalise the carrier A to A' and assume A' ⊆ A every time the theorem is proved by induction.
Lukas Stevens (Aug 13 2020 at 11:57):Use types to sets is really a lot more elegant in this case (provided I can get the setup to work :laughter_tears:).
Manuel Eberl (Aug 13 2020 at 12:02):I don't think you want to open that can of worms
Kevin Kappelmann (Aug 13 2020 at 12:06):I remember a person saying that it is a bit worrying that there is (barely) anyone left knowing how to use types to sets - do not discourage the volunteer :laughter_tears:
Manuel Eberl (Aug 13 2020 at 12:07):I said we should have people who know how to use it, I didn't say we /should/ actually use it. :P
Lukas Stevens (Aug 13 2020 at 12:08):I think you can't have both at the same time :D
Manuel Eberl (Aug 13 2020 at 12:09):Well, feel free to play around with it. But I'm pretty sure it is not worth the effort for your use case, even if there were not the additional obstacle of you having to learn how to use it first.
Manuel Eberl (Aug 13 2020 at 12:09):I'm curious what Mikhail Chekhov is up to with types-to-sets…
Last updated: Dec 21 2024 at 12:33 UTC