2

根据同伦类型理论（第 49 页），这是相等的完整归纳原理：

Definition path_induction (A : Type) (C : forall x y : A, (x = y) -> Type)
           (c : forall x : A, C x x eq_refl) (x y : A) (prEq : x = y)
  : C x y prEq :=
  match prEq with
  | eq_refl => c x
  end.

我对HoTT不太了解，但我确实看到路径归纳比eq_rect：

Lemma path_ind_stronger : forall (A : Type) (x y : A) (P : A -> Type)
                            (prX : P x) (prEq : x = y),
    eq_rect x P prX y prEq =
    path_induction A (fun x y pr => P x -> P y) (fun x pr => pr) x y prEq prX.
Proof.
  intros. destruct prEq. reflexivity.
Qed.

相反，我未能path_induction从eq_rect. 可能吗 ？如果不是，平等的正确归纳原则是什么？Inductive我认为这些原则是从类型定义中机械地派生出来的。

编辑

多亏了下面的答案，关于相等的完整归纳原则可以由

Scheme eq_rect_full := Induction for eq Sort Prop.

然后我们得到相反的，

Lemma eq_rect_full_works : forall (A : Type) (C : forall x y : A, (x = y) -> Prop)
                             (c : forall x : A, C x x eq_refl) (x y : A)
                             (prEq : x = y),
    path_induction A C c x y prEq
    = eq_rect_full A x (fun y => C x y) (c x) y prEq.
Proof.
  intros. destruct prEq. reflexivity.
Qed.
4

1 回答 1

3

我认为你指的是这样一个事实，即结果类型path_induction提到了被破坏的路径，而其中的一个eq_rect没有。这种省略是归纳命题的默认设置（与 发生的情况相反Type），因为额外的论点通常不用于证明无关的发展。不过，您可以使用以下命令指示 Coq 生成更完整的归纳原理Scheme：https ://coq.inria.fr/distrib/current/refman/user-extensions/proof-schemes.html?highlight=minimality 。（Minimality变体是默认情况下用于命题的变体。）

于 2018-09-02T14:55:17.607 回答