Stream: General

Topic: Generalising to subset


view this post on Zulip 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?

view this post on Zulip Manuel Eberl (Aug 13 2020 at 09:04):

Yeah that's what types-to-sets does

view this post on Zulip Manuel Eberl (Aug 13 2020 at 09:04):

probably not worth it in this case though

view this post on Zulip 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

view this post on Zulip Lukas Stevens (Aug 13 2020 at 10:06):

Is Types_To_Sets something you could use in the distribution?

view this post on Zulip Lukas Stevens (Aug 13 2020 at 10:07):

Asking because it introduces additional axioms

view this post on Zulip Manuel Eberl (Aug 13 2020 at 11:28):

I think the jury is still out on that.

view this post on Zulip Manuel Eberl (Aug 13 2020 at 11:29):

But I think there probably wouldn't be too much opposition to it

view this post on Zulip Manuel Eberl (Aug 13 2020 at 11:29):

regardless, I doubt it's worth it for your example

view this post on Zulip Manuel Eberl (Aug 13 2020 at 11:30):

the proofs are probably pretty simple

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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:).

view this post on Zulip Manuel Eberl (Aug 13 2020 at 12:02):

I don't think you want to open that can of worms

view this post on Zulip 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:

view this post on Zulip 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

view this post on Zulip Lukas Stevens (Aug 13 2020 at 12:08):

I think you can't have both at the same time :D

view this post on Zulip 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.

view this post on Zulip Manuel Eberl (Aug 13 2020 at 12:09):

I'm curious what Mikhail Chekhov is up to with types-to-sets…


Last updated: Aug 15 2022 at 02:13 UTC