coq - coq 中的依赖模式匹配

Question

以下代码(当然不是完整的证明)尝试对依赖产品进行模式匹配:

Record fail : Set :=
  mkFail {
      i : nat ;
      f : forall x, x < i -> nat
    }.

Definition failomat : forall (m : nat) (f : forall x, x < m -> nat), nat.
Proof.
  intros.
  apply 0.
Qed.

Function fail_hard_omat fl : nat := failomat (i fl) (f fl).

Definition failhard fl : fail_hard_omat fl = 0.
refine ((fun fl =>
          match fl with
            | mkFail 0 _ => _
            | mkFail (S n) _ => _
          end) fl).

我尝试执行此操作时遇到的错误是

Toplevel input, characters 0-125:
Error: Illegal application (Type Error): 
The term "mkFail" of type
 "forall i : nat, (forall x : nat, x < i -> nat) -> fail"
cannot be applied to the terms
 "i" : "nat"
 "f0" : "forall x : nat, x < i0 -> nat"
The 2nd term has type "forall x : nat, x < i0 -> nat"
which should be coercible to "forall x : nat, x < i -> nat".

似乎替换没有到达内部类型参数。

Answer 1

在玩过Program 命令后，我设法构建了一个可能适合您的优化，但我并不理解我所做的一切。主要思想是通过引入中间等式来帮助 Coq 进行替换，这些等式将在替换中充当桥梁

    refine ((fun fl =>

    match fl as fl0 return (fl0 = fl -> fail_hard_omat fl0 = 0) with
      | mkFail n bar =>
        match n as n0 return (forall foo: (forall x:nat, x < n0 -> nat), 
           mkFail n0 foo = fl -> fail_hard_omat (mkFail n0 foo) = 0) with 
       | O => _
       | S p => _
       end bar
    end (eq_refl fl) ) fl).

无论如何，我不知道你在这里的目的是什么，但我建议永远不要“手工”编写依赖匹配并依赖 Coq 的策略。在您的情况下，如果您使用 Defined. 而不是 Qed 定义您的 Definition failomat，您将能够展开它，但您不会需要依赖匹配。

希望对你有帮助五、

注意:bar 的两次出现都可以用下划线代替。