# 如何解决模式匹配中类型的惰性求值

**URL:** <https://discourse.rocq-prover.org/t/topic/1292>\
**Category:** \[zh\] Rocq 中文\
**Created:** [May 4, 2021, 5:51am UTC](https://discourse.rocq-prover.org/t/topic/1292 "2021-05-04T05:51:57Z")\
**Posts on this page:** 4\
**Page:** 1

<div class="post-metadata">

**Author:** ![hhiim](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/hhiim/32/394_2.png) [@hhiim](https://discourse.rocq-prover.org/u/hhiim)\
**Post date:** [May 4, 2021, 5:51am UTC](https://discourse.rocq-prover.org/t/topic/1292/1 "2021-05-04T05:51:57Z")

</div>

问题如下，请教下怎么解决啊？  
 ![捕获](https://us1.discourse-cdn.com/flex001/uploads/coq/original/1X/b453e55b43c83a65e701419b1ee945e31426043a.png)

---

<div class="post-metadata">

**Author:** ![hhiim](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/hhiim/32/394_2.png) [@hhiim](https://discourse.rocq-prover.org/u/hhiim)\
**Post date:** [May 4, 2021, 6:34am UTC](https://discourse.rocq-prover.org/t/topic/1292/2 "2021-05-04T06:34:27Z")

</div>

![捕获2](https://us1.discourse-cdn.com/flex001/uploads/coq/original/1X/a977539abd17aae3192d4c1ca2ce1b6847dce8d8.png)  
好吧，更正下定义。但依然不通过

---

<div class="post-metadata">

**Author:** ![Lys](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/lys/32/48_2.png) [@Lys](https://discourse.rocq-prover.org/u/Lys)\
**Post date:** [May 4, 2021, 4:18pm UTC](https://discourse.rocq-prover.org/t/topic/1292/3 "2021-05-04T16:18:02Z")

</div>

方便使用[Markdown代码块](https://xianbai.me/learn-md/article/extension/code-blocks-and-highlighting.html)把代码复制过来吗？

---

<div class="post-metadata">

**Author:** ![lastland](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/lastland/32/364_2.png) [@lastland](https://discourse.rocq-prover.org/u/lastland)\
**Post date:** [May 4, 2021, 11:26pm UTC](https://discourse.rocq-prover.org/t/topic/1292/4 "2021-05-04T23:26:07Z")

</div>

这类依赖类型做模式匹配的问题，一般可以通过 eta expansion 来做。这里你的 g 和 h 都依赖于 o，那么可以把 g 和 h 都作为参数挪到 o 的模式匹配的 body 里面。像这样：

```
Fixpoint cy {o : nat} {A B} (f : A -> B) (g : fb A o) (h : fb B o) : Prop :=
  (match o with
   | O => fun (g : fb A O) (h : fb B O) => (f g = h)
   | S n => fun (g : fb A (S n)) (h : fb B (S n)) => forall (P : A), cy f (g P) (h (f P))
   end) g h.

```

我这里的 cy 是你的差异相等，fb 是你的封闭算子。

另外一个我常用的技巧是，在想不出来如何直接定义这类函数时，用 Coq 的 tactics 来做。因为 Coq 的 tactics 挺强大的，有时候会自动帮你做这些比如 eta expansion 这类的活。像这个例子，你可以把 `Fixpoint` 改成 `Definition`，加上返回类型，然后 `induction o`：

```
Definition cy {o : nat} {A B} (f : A -> B) (g : fb A o) (h : fb B o) : Prop.
induction o.
- exact (f g = h). 
- ...
```