add some union_with lemmas

These are taken verbatim from Perennial, where they already existed and I just needed both of them. So there is clearly some need here.

But the lemmas are kind of weird so I am open for discussions for how to better provide them.

• The first has a very specific lemma statement with this λ x' _, Some x'. This arises from lookup_union on maps.

• The second is the same as left_id, but never in a hundred years would I have realized I can use that LeftId instance. union_with is not a binary operator; I think we need a readable lemma that shows up in SearchAbout union_with None. Yes LeftId does show up in that search but I doubt many people will realize that it is useful in this situation -- I have skipped over it myself.

  Basically: not everything that can be written as LeftId / RightId, should be written that way. IMO we should only use these classes for things that are actually binary operators, written with infix notation. I don't object to instances also existing in other cases, but those instances should only exist in addition to regular lemmas, not instead of them.

changed the description

I have no objections to any of these lemmas, but I think it would be good to have both the left and right variants, and hopefully also have them for intersection_with, union, and intersection (on option).

added 1 commit

• 3fa1aa25 - more union_with and union lemmas; adjust lookup_union stmt

Compare with previous version

added 1 commit

• 5c2d08be - more union_with and union lemmas; adjust lookup_union stmt

Compare with previous version

Oh I didn't even see union on option. We can write lookup_union in a much nicer way with that.

I added the union_with and union lemmas. Here I think LeftId/RightId actually makes sense, since ∪ is a binary operator.

I won't have time to look into intersection.

I won't have time to look into intersection.

I see we also don't have lookup_intersection for maps. Maybe just make an issue that we should add these lemmas someday.

added 1 commit

• 66520de3 - add some option union lemmas, and use it in lookup_union

Compare with previous version

mentioned in issue #166 (closed)

added 1 commit

• a050beda - use option_ prefix consistently

Compare with previous version

added 1 commit

• b0f8e96c - use option_ prefix consistently

Compare with previous version

resolved all threads

mentioned in merge request !449 (merged)

resolved all threads

added 98 commits

• 66520de3...20813c6c - 97 commits from branch master
• 38f8c4fc - add some option union lemmas, and use it in lookup_union

Compare with previous version