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

[zh] Coq 中文
1

问题如下，请教下怎么解决啊？
捕获

2

捕获2
好吧，更正下定义。但依然不通过

3

方便使用Markdown代码块把代码复制过来吗？

4

这类依赖类型做模式匹配的问题，一般可以通过 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). 
- ...
2 Likes