Search code examples
coqtypeclassconceptual

Expressing "almost Properness" under option type

Suppose we have a type A with an equivalence relation (===) : A -> A -> Prop on it.

On top of that there is a function f : A -> option A.

It so happens that this function f is "almost" Proper with respect to equiv. By "almost" I mean the following:

Lemma almost_proper :
  forall a1 a2 b1 b2 : A,
    a1 === a2 ->
    f a1 = Some b1 -> f a2 = Some b2 ->
    b1 === b2.

In other words, if f succeeds on both inputs, the relation is preserved, but f might still fail on one and succeed on the other. I would like to express this concept concisely but came up with a few questions when trying to do so.

I see three solutions to the problem:

  1. Leave everything as is. Do not use typeclasses, prove lemmas like the one above. This doesn't look good, because of the proliferation of preconditions like x = Some y, which create complications when proving lemmas.

  2. It is possible to prove Proper ((===) ==> equiv_if_Some) f when equiv_if_Some is defined as follows:

    Inductive equiv_if_Some {A : Type} {EqA : relation A} `{Equivalence A EqA} : relation (option A) :=
| equiv_Some_Some : forall a1 a2, a1 === a2 -> equiv_if_Some (Some a1) (Some a2)
| equiv_Some_None : forall a, equiv_if_Some (Some a) None
| equiv_None_Some : forall a, equiv_if_Some None (Some a)
| equiv_None_None : equiv_if_Some None None.

    One problem here is that this is no longer an equivalence relation (it is not transitive).

  3. It might be possible to prove Almost_Proper ((===) ==> (===)) f if some reasonable Almost_Proper class is used. I am not sure how that would work.

What would be the best way to express this concept? I am leaning toward the second one, but perhaps there are more options?

For variants 2 and 3, are there preexisting common names (and therefore possibly premade definitions) for the relations I describe? (equiv_if_Some and Almost_Proper)

Solution

  • 2 if it simplifies your proofs.

    The fact that it's not an equivalence relation is not a deal breaker, but it does limit the contexts in which it can be used.

    equiv_if_Some might be nicer to define as an implication (similar to how it appears in the almost_proper lemma) than as an inductive type.

    You may also consider using other relations (as an alternative to, or in combination with equiv_if_Some):

    • A partial order, that can only relate None to Some but not Some to None
    • A partial equivalence relation, that can only relate Somes.