Better way of writing `Proper` premises in fin sets

Use Proper (.. => impl) instead of Proper (.. => iff) and ∀ x, Proper .. instead of Proper ((=) ==> ..).

The new premises are easier to prove (both solve_proper and manual proof).

This came up in !478 (merged)

changed title from Better way of writing Proper premises to Better way of writing Proper premises in fin sets

added 2 commits

• b4e387e6 - 1 commit from branch master
• 1f6c9330 - Use `Proper (.. => impl)` instead of `Proper (.. => iff)` and `∀ x, Proper ..`...

Compare with previous version

mentioned in merge request !478 (merged)

So the impl instances will always kick in where the iff ones were used?

E.g. if the goal if f x ↔ g x and there is an iff ==> iff instance, does f_equiv still work?

We should document somewhere that Proper should never start with (=) (and never end if iff it seems). Where would be a good place? Somewhere in the iris docs, or a new file in std++?

I don't know what's a good place for this kind of documentation. In general aside from comments, we do not have a good story what's a good place to put std++ specific documentation. In Iris we have a docs folder, which also contains lots of stuff that applies to std++ (the style guide, for instance).

In Iris there is also equalities_and_entailments.md, which talks about Proper. But this seems not entirely in scope for that.

We could have have https://gitlab.mpi-sws.org/iris/docs, which contains files about coding style, setting up editor, use of type classes, etc. This allows us to share documentation for Iris and std++.

A much more lightweight alternative is to add this documentation to Iris, and just link to the (relevant files of the) Iris docs in std++.

A much more lightweight alternative is to add this documentation to Iris, and just link to the (relevant files of the) Iris docs in std++.

Yeah that seems like the best option to me.

mentioned in merge request iris!962 (merged)

Going to merge. Documentation can be discussed in iris!962 (merged)

resolved all threads

added 1 commit

• 7ab1f172 - CHANGELOG.

Compare with previous version

added 1 commit

• 5b97ef36 - CHANGELOG.

Compare with previous version

Oh, I noticed there is no CHANGELOG entry yet. @jung Please review and press merge.

added 1 commit

• 2b50c3dd - CHANGELOG.

Compare with previous version

mentioned in commit e99461ab

merged