为什么我有时可以通过引理而不是直接证明一个目标？

Question

考虑下面定义的函数。它的作用并不重要。

Require Import Ring.
Require Import Vector.
Require Import ArithRing.

Fixpoint
  ScatHUnion_0 {A} (n:nat) (pad:nat) : t A n -> t (option A) ((S pad) * n).
 refine (
  match n return (t A n) -> (t (option A) ((S pad)*n)) with
  | 0 => fun _ =>  (fun H => _)(@nil (option A))
  | S p =>
    fun a =>
      let foo := (@ScatHUnion_0 A p pad (tl a)) in
      (fun H => _) (cons _ (Some (hd a)) _ (append (const None pad) foo))
  end
   ).
 rewrite  <-(mult_n_O (S pad)); auto.
 replace  (S pad * S p) with ( (S (pad + S pad * p)) ); auto; ring.
Defined.

我要证明

Lemma test0:  @ScatHUnion_0 nat 0 0 ( @nil nat) = ( @nil (option nat)).

完成后

  simpl. unfold eq_rect_r. unfold eq_rect.

目标是

         match mult_n_O 1 in (_ = y) return (t (option nat) y) with
         | eq_refl => nil (option nat)
         end = nil (option nat)

当试图用

完成它时

  apply trans_eq with (Vector.const (@None nat) (1 * 0)); auto.
  destruct (mult_n_O 1); auto.

destruct 不起作用（请参阅下面的错误消息）。但是，如果我首先在引理中证明完全相同的目标，甚至在证明中使用 assert，我可以应用并解决它，如下所示：

Lemma test1:  @ScatHUnion_0 nat 0 0 ( @nil nat) = ( @nil (option nat)).
  simpl. unfold eq_rect_r. unfold eq_rect.

  assert (
      match mult_n_O 1 in (_ = y) return (t (option nat) y) with
        | eq_refl => nil (option nat)
      end = nil (option nat)
    ) as H.
  {
    apply trans_eq with (Vector.const (@None nat) (1 * 0)); auto.
    destruct (mult_n_O 1); auto.
  }
    apply H.
Qed.

谁能解释一下这是为什么，遇到这种情况应该怎么想？

在 Coq 8.4 中出现错误

      Toplevel input, characters 0-21:
      Error: Abstracting over the terms "n" and "e" leads to a term
      "fun (n : nat) (e : 0 = n) =>
       match e in (_ = y) return (t (option nat) y) with
       | eq_refl => nil (option nat)
       end = const None n" which is ill-typed.

在 Coq 8.5 中我得到错误

      Error: Abstracting over the terms "n" and "e" leads to a term
      fun (n0 : nat) (e0 : 0 = n0) =>
      match e0 in (_ = y) return (t (option nat) y) with
      | eq_refl => nil (option nat)
      end = const None n0
      which is ill-typed.
      Reason is: Illegal application: 
      The term "@eq" of type "forall A : Type, A -> A -> Prop"
      cannot be applied to the terms
       "t (option nat) 0" : "Set"
       "match e0 in (_ = y) return (t (option nat) y) with
        | eq_refl => nil (option nat)
        end" : "t (option nat) n0"
       "const None n0" : "t (option nat) n0"
      The 2nd term has type "t (option nat) n0" which should be coercible to
       "t (option nat) 0".

Answer 1

我会说这是因为依赖类型，在这两种情况下你实际上并没有证明完全相同的东西（尝试 Set Printing All. 查看隐式类型和隐藏信息）。

这样的 destruct 失败的事实通常是由于依赖项会引入错误类型的术语 at，并且您必须更精确地确定要破坏的内容（这里没有秘密，它在以个案为基础）。通过提取子引理，您可能已经删除了麻烦的依赖性，现在可以进行 destruct 操作了。

Answer 2

@Vinz 回答解释了原因，并建议 Set Printing All. 这表明了区别所在。问题是 simpl. 简化了 match 的 return 类型。使用 unfold ScatHUnion_0. 而不是 simpl. 使我能够直接在目标上使用 destruct。

从根本上说，我的麻烦源于我想要让类型系统相信 0=0 与 0=1*0 相同。（顺便说一句，我仍然不知道这样做的最佳方法。）我使用 mult_n_O 来证明这一点，但它是不透明的，所以类型系统在检查这两种类型时无法展开它等于。

当我用我自己的 Fixpoint 变体（不是不透明的）替换它时，

Fixpoint mult_n_O n: 0 = n*0 :=
    match n as n0 return (0 = n0 * 0) with
  | 0 => eq_refl
  | S n' => mult_n_O n'
  end.

并在 ScatHUnion_0 的定义中使用它，引理很容易证明：

Lemma test0:  @ScatHUnion_0 nat 0 0 ( @nil nat) = ( @nil (option nat)).
  reflexivity.
Qed.

附加评论：

这是一个适用于原始不透明 mult_n_O 定义的证明。它基于 proof by Jason Gross。它通过使用 generalize 将 mult_n_O 1 的类型操纵为 0=0。它使用set修饰term的隐含部分，比如eq_refl中的类型，只有在Set Printing All.命令之后才可见。 change也可以，但是replace和rewrite好像做不到。

Lemma test02:
  match mult_n_O 1 in (_ = y) return (t (option nat) y) with
    | eq_refl => nil (option nat)
  end = nil (option nat).
Proof.
  Set Printing All.
  generalize (mult_n_O 1 : 0=0).
  simpl.
  set (z:=0) at 2 3.
  change (nil (option nat)) with (const (@None nat) z) at 2.
  destruct e.
  reflexivity.
Qed.

更新：感谢 coq-club 的人们，这里有一个更简单的证明。

Lemma test03:
  match mult_n_O 1 in (_ = y) return (t (option nat) y) with
    | eq_refl => nil (option nat)
  end = nil (option nat).
Proof.
  replace (mult_n_O 1) with (@eq_refl nat 0);
  auto using Peano_dec.UIP_nat.
Qed.

为什么我有时可以通过引理而不是直接证明一个目标？

Why can I sometimes prove a goal via a lemma, but not directly?

coq