Stream: Beginner Questions

Topic: Formalizing implicit assumption from pen and paper

Bob Rubbens (Sep 19 2023 at 08:22):

Hi all,

In a formalization I'm looking at they are making an implicit assumption that I find hard to encode. They define a merge operator "|" for maps from integers to some object. This merging operator is only defined if the key sets of both maps do not overlap, otherwise the results is undefined. After that, they state that, "wherever "|" is used, we implicitly assume the keysets do not overlap". I see three options here if I want to write this in Isabelle:

1. Add some kind of axiom saying, for all p|q, keys(p) does not overlap with keys(q). I haven't tried this yet because I don't really know how to add axioms like this, but I'm afraid that Isabelle's automization will pick this up and use it to complete all remaining proofs (as it's clearly possible to construct a p and q that both map 1 to some object). Will Isabelle indeed do this? Or can I safely add such an axiom? If so, how?
2. Make the partiality explicit, as in, make the type of |: key => key => object option. The downside of that is that now the merge operator doesn't compose nicely with itself anymore.
3. This is what I eventually went with: have the merge operator check if the inputs overlap. If so, it returns "undefined". If they don't overlap, it returns the actual merge of the two maps. This is faithful to the pen and paper formalization, but this does mean I have to write down this disjointness property everywhere. In addition, I have not yet managed to get the simp rules right such that such facts are easily derivable where they are needed. I'm constantly tweaking them, but there seems to be a limit to how much work I can automate away.

Is option 3 the way to go? Or are there other options I might be missing? I'd also be interested to see any formalizations where they also had this problem, to see how they solved it.

Yong Kiam (Sep 19 2023 at 09:15):

what about an option 4: pick a reasonable default for the case where keys overlap (for example, make it equal to the output from q always), in a way that makes as many of your lemmas as easy/unconditional as possible?

Bob Rubbens (Sep 19 2023 at 09:18):

The book relies a bit on commutativity, associativity, which would no longer be the case with such a rule. I think you can probably make it work but then I would worry about my results corresponding to the results in the book...

Mathias Fleury (Sep 19 2023 at 09:20):

Option 1 is never going to work (you need dependent types to do that). If the order is only used for proofs, I would go for option 2 and make the transformation explicit (like value + Max_vaule (lhs)). Otherwise, I would use 3 (because this matches what is happening here: you make explicit something implicit but you do not assume more than before)

Mathias Fleury (Sep 19 2023 at 09:20):

BTW instead of returning undefined, you could just let the merge operator do something, but not caring about the result

Mathias Fleury (Sep 19 2023 at 09:21):

So there is no need for a special case

Bob Rubbens (Sep 19 2023 at 09:22):

Mathias Fleury said:

BTW instead of returning undefined, you could just let the merge operator do something, but not caring about the result

That makes sense. Is there a downside to using undefined?

Mathias Fleury (Sep 19 2023 at 09:22):

I see it the other way around: there is no advantage to using undefined

Yong Kiam (Sep 19 2023 at 09:23):

actually, I now see the advantage of using undefined as the default: the commutativity and associativity laws still hold unconditionally, right?

Mathias Fleury (Sep 19 2023 at 09:23):

Without undefined you save an if

Bob Rubbens (Sep 19 2023 at 09:23):

Hmm, so I don't have to be afraid of my proofs depending on a known constant, instead of an unknown constant...? (Sorry, with Isabelle I'm just never sure about how paranoid I should be)

Mathias Fleury (Sep 19 2023 at 09:25):

Yong Kiam said:

actually, I now see the advantage of using undefined as the default: the commutativity and associativity laws still hold unconditionally, right?

ah that is a good point

Mathias Fleury (Sep 19 2023 at 09:25):

but then instead of undefined you could use some empty value, like done for division

Mathias Fleury (Sep 19 2023 at 09:25):

(1/0 = 0)

Mathias Fleury (Sep 19 2023 at 09:26):

Bob Rubbens said:

Hmm, so I don't have to be afraid of my proofs depending on a known constant, instead of an unknown constant...? (Sorry, with Isabelle I'm just never sure about how paranoid I should be)

in most context, you will anyway that there is no overlap…

Mathias Fleury (Sep 19 2023 at 09:26):

But Yong has a good point! I did not think of that

Bob Rubbens (Sep 19 2023 at 09:27):

I mean, I might forget adding this as an assumption sometimes...

Last updated: Dec 21 2024 at 16:20 UTC