coq - 为什么有时我可以通过引理证明目标，但不能直接证明？

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

@Vinz 回答解释了原因，并建议 Set Printing All.这显示了区别是什么。问题是 simpl.简化了 match 的返回类型.使用 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 .
它操作 mult_n_O 1 的类型成为 0=0通过使用 generalize .它使用 set修改术语的隐含部分，例如 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.