使用 eq_rect 的路径归纳

Question

根据 Homotopy Type Theory（第 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.

相反，我未能从 eq_rect 构造 path_induction。可能吗？如果不是，平等的正确归纳原则是什么？我认为这些原则是机械地从 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.

Answer 1

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

使用 eq_rect 的路径归纳

Path induction using eq_rect

coq

homotopy-type-theory