努力扩展功能 [英] Struggling with functional extensionality

问题描述

我已经在Coq编程了几个月了。特别是，我对函数随处可见的函数式编程证明感兴趣（光学，状态monad 等）。从这个意义上讲，处理功能扩展性已变得至关重要，尽管这很烦人。为了说明这种情况，让我们假设 Monad 的简单化（仅定义了一条定律）：

I've been programming in Coq for a few months now. Particularly, I'm interested in functional programming proofs where functions arise everywhere (optics, state monad, etc.). In this sense, dealing with functional extensionality has become essential, though extremely annoying. To illustrate the situation, let us assume a simplication of Monad (just one law defined):

Class Monad (m : Type -> Type) :=
{ ret : forall {X}, X -> m X
; bind : forall {A B}, m A -> (A -> m B) -> m B
}.
Notation "ma >>= f" := (bind ma f) (at level 50, left associativity).

Class MonadLaws m `{Monad m} :=
{ right_id : forall X (p : m X), p >>= ret = p }.

现在，我想证明链接多个 ret s到程序 p 应该等同于相同的程序：

Now, I'd like to prove that chaining several rets to a program p should be equivalent to the very same program:

Example ugly_proof :
  forall m `{MonadLaws m} A (p : m A), 
    p >>= (fun a1 => ret a1 >>= (fun a2 => ret a2 >>= ret)) = p.
Proof.
  intros.
  destruct H0 as [r_id].

  assert (J : (fun a2 : A => ret a2 >>= ret) =
              (fun a2 : A => ret a2)).
  { auto using functional_extensionality. }
  rewrite J.

  assert (K : (fun a1 : A => ret a1 >>= (fun a2 : A => ret a2)) =
              (fun a1 : A => ret a1)).
  { auto using functional_extensionality. }
  rewrite K.

  now rewrite r_id.
Qed.

证明是正确的，但是迭代的断言模式非常麻烦。确实，当事情变得更加复杂时，这变得不切实际，正如您在此证明（证明仿射遍历在合成过程中是封闭的）。

The proof is correct, but the iterative assert pattern makes it very cumbersome. Indeed, it becomes impractical when things get more complex, as you can find in this proof (which evidences that an affine traversal is closed under composition).

话虽如此，实现此目标的最佳方法是什么前述证明？周围是否有任何项目或文章（比这一个更容易接近）功能扩展性可以作为参考？

Having said so, what is the best way of implementing the aforementioned proof? Is there any project or article (more approachable than this one) around functional extensionality to be taken as reference?

推荐答案

有一种方法使用 setoid_rewrite 策略（我尝试在此答案中进行演示）：

There is an approach with setoid_rewrite tactic (I tried to demostrate it in this answer):

Require Import Coq.Logic.FunctionalExtensionality.
Require Import Coq.Setoids.Setoid.
Require Import Coq.Classes.Morphisms.

Generalizable All Variables.

Instance pointwise_eq_ext {A B : Type} `(sb : subrelation B RB eq)
  : subrelation (pointwise_relation A RB) eq.
Proof. intros f g Hfg. apply functional_extensionality. intro x; apply sb, (Hfg x). Qed.

Example easy_proof `{ml : MonadLaws m} `{p : m A} :
  p >>= (fun a1 => ret a1 >>= (fun a2 => ret a2 >>= ret)) = p.
Proof. now repeat setoid_rewrite right_id. Qed.  

阅读材料：

• 对类型类和关系的温和介绍Coq ，由PierreCastéran& Matthieu Sozeau

• A Gentle Introduction to Type Classes and Relations in Coq by Pierre Castéran & Matthieu Sozeau

Matthieu Sozeau的类型理论中的广义重写的新视角

这篇关于努力扩展功能的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！