在选项类型下表示“几乎正确”

Question

假设我们有一个类型为A并具有等价关系(===) : A -> A -> Prop的类型。

最重要的是功能f : A -> option A。

[碰巧此功能f相对于Proper几乎是equiv。 “几乎”是指：

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

换句话说，如果f在两个输入上都成功，则保留了该关系，但是f可能仍然在一个输入上失败而在另一个输入上成功。我想简洁地表达这个概念，但是在尝试时提出了一些问题。

我看到了该问题的三种解决方案：

1. 保留所有内容。不要使用类型类，证明上面的引理。这看起来不太好，因为x = Some y之类的前提条件的泛滥，在证明引理时会产生复杂性。

2. Proper ((===) ==> equiv_if_Some) f的定义如下，可以证明equiv_if_Some：

   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.
   

   这里的一个问题是，这不再是等价关系（它不是可传递的。）>]

3. 如果使用某些合理的Almost_Proper ((===) ==> (===)) f类，可能会证明Almost_Proper。我不确定这将如何工作。

表达此概念的最佳方法是什么？我倾向于第二个，但也许还有更多选择？

对于变体2和3，我描述的关系是否存在预先存在的通用名称（因此可能是预先定义的名称）？ （equiv_if_Some和Almost_Proper）

假设我们有一个具有等价关系（===）的类型A：A-> A->对它的支持。最重要的是，有一个函数f：A->选项A。碰巧这个函数f是“几乎” ...

Answer 1

2如果简化了您的证明。