关于等价关系在 lambda 中重写

Question

问题是，如果我知道forall x, f x ≡ g x（其中≡是某种等价关系，而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.

如果我们可以将 f 替换为 g，则证明通过，但我不确定该怎么做。要使我的等价关系成功，我需要什么额外的力量？

Answer 1

解决方案是使用来自 coq stdlib 的 pointwise_relation：Link here

我还复制粘贴了定义以防 link bitrots:

 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.

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

这里是编译的完整代码清单：

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.

关于等价关系在 lambda 中重写

rewrite within lambda with respect to an equivalence relation

coq

coq-tactic