coq - 在 lambda 内根据等价关系重写

Question

问题是，如果我知道forall x, f x ≡ g x(其中QI是某种等价关系，而f,g 是函数)，正确的 Proper 实例是什么，它可以让我用 g 重写 f 在一些更大的由等价关系链接的术语？

假设如果需要的话可以使用功能扩展性 - 我猜这将是必需的？

一些示例代码可以更好地演示问题:

Require Import Setoid.
(** Feel free to assume FunExt *)
Require Import FunctionalExtensionality.
Section FOOBAR.
  Variable T: Type.
  Variable f: T -> T.
  Variable g: T -> T.

  Variable t0: T.
  Variable combiner: (T -> T) -> T -> T.

  Variable equiv: T -> T -> Prop.
  Infix "≡" := equiv (at level 50).

  Axiom equivalence_equiv: Equivalence equiv.


  Axiom F_EQUIV_G_EXT: forall (t: T), f t ≡ g t.

  (** Check that coq can resolve the Equivalence instance **)
  Theorem equivalence_works: t0 ≡ t0.
  Proof.
    reflexivity.
  Qed.

  Theorem rewrite_in_lambda:
    combiner (fun t => f t) t0 ≡
    combiner (fun t => g t) t0.
  Proof.
    intros.
    (* I wish to replace x with y.
    What are the Proper rules  I need for this to happen? *)
    rewrite F_EQUIV_G_EXT.
  Abort.
End FOOBAR.

如果我们可以用 g 替换 f，那么证明就通过了，但我不知道该怎么做。我需要什么额外的能力才能让我的等价关系成功？

Answer 1

解决方案是使用 coq stdlib 中的 pointwise_relation:Link here

我还复制粘贴了定义，以防链接位旋转:

 Definition pointwise_relation (R : relation B) : relation (A -> B) :=
    fun f g => forall a, R (f a) (g a).

因此，我们希望有一个正确的表单实例:

Axiom proper: Proper (pointwise_relation T equiv ==> equiv ==> equiv) combiner.

也就是说，如果第一个函数逐点相等，并且第二个参数相等，则结果相等。

这里是编译的完整代码 list :

Require Import Setoid.
Require Import Relation_Definitions.
Require Import Morphisms.

(** Feel free to assume FunExt *)
Require Import FunctionalExtensionality.
Section FOOBAR.
  Variable T: Type.
  Variable x: T -> T.
  Variable y: T -> T.

  Variable t0: T.
  Variable combiner: (T -> T) -> T -> T.

  Variable equiv: T -> T -> Prop.
  Infix "≡" := equiv (at level 50).

  Axiom equivalence_equiv: Equivalence equiv.
  Axiom proper: Proper (pointwise_relation T equiv ==> equiv ==> equiv) combiner.

  Axiom X_EQUIV_Y_EXT: forall (t: T), x t ≡ y t.

  (** Check that coq can resolve the Equivalence instance **)
  Theorem equivalence_works: t0 ≡ t0.
  Proof.
    reflexivity.
  Qed.

  Theorem rewrite_in_lambda:
    combiner (fun t => x t) t0 ≡
    combiner (fun t => y t) t0.
  Proof.
    intros.
    (* I wish to replace x with y.
    What are the Proper rules  I need for this to happen? *)
    setoid_rewrite X_EQUIV_Y_EXT.
    reflexivity.
  Qed.
End FOOBAR.