Coq中的从属模式匹配 [英] Dependent pattern matching in coq

问题描述

以下代码（当然不是完整的证明）试图对从属产品进行模式匹配：

The following code (which is of course not a complete proof) tries to do pattern matching on a dependent product:

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).

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

The error I get when trying to execute this is

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".

替换似乎无法达到内部类型参数。

It seems that the substitution somehow does not reach the inner type parameters.

推荐答案

在使用 Program 命令后，我设法建立了一个适合您的优化程序，但是我不明白我所做的一切。主要思想是通过引入将在替代中充当桥梁的中间等式来帮助Coq进行替代

After playing with the Program command I managed to build a refine that might suites you, but I don't understand everything I did. The main idea is to help Coq with the substitution by introducing intermediate equalities that will serve as brige within the substitution

    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定义了定义故障诊断， code>，您将能够展开它，并且不需要依赖匹配。

Anyway, I don't know what your purpose here is, but I advise never write dependent match "by hand" and rely on Coq's tactics. In your case, if you define your Definition failomat with Defined. instead of Qed, you will be able to unfold it and you won't need dependent matching.

希望它会有所帮助，
V。

Hope it helps, V.

注意：两个 bar 都可以用下划线代替。

Note: both occurences of bar can be replaced by an underscore.

这篇关于Coq中的从属模式匹配的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！