代码之家 › 专栏 › 技术社区 › Siddharth Bhat

关于等价关系的lambda重写

coq-tactic coq

Siddharth Bhat · 技术社区 · 7 年前

问题是,如果我知道 forall x, f x â¡ g x (何处) â¡ 是一些等价关系,并且 f , g ,是函数),正确的是 Proper 允许我重写的实例 f 具有 G 在一些较大的术语中由等价关系联系起来?

假设如果需要的话,函数扩展性是可用的——我猜这需要哪个?

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

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 ,但我不知道该怎么做。我需要什么额外的权力来实现这个等价关系呢?

1 回复 | 直到 7 年前

Siddharth Bhat 7 年前

解决办法是 pointwise_relation 来自COQ Stdlib: 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.

也就是说,如果第一个函数是逐点相等的,而第二个参数是相等的,则结果是相等的。

以下是编译的完整代码列表:

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.