如何在 coq 中明确使用归纳原理？

Question

我试图用 Coq 中的归纳原理显式证明命题恒等式的对称性，但不能像在 agda 中那样用归纳原理来证明。我不知道如何在 Coq 中局部声明变量，也不知道如何展开定义，如下所示。我怎样才能得到类似于下面的 agda 的证明？

Inductive Id (A : Type) (x : A) : A -> Type :=
  | refl : Id A x x.

(* trivial with induction *)
Theorem symId {A} {x y} : Id A x y -> Id A y x.
Proof.
  intros.
  induction H.
  apply refl.
Qed.

Check Id_ind.
(* Id_ind *)
(*      : forall (A : Type) (x : A) (P : forall a : A, Id A x a -> Prop), *)
(*        P x (refl A x) -> forall (y : A) (i : Id A x y), P y i *)

Theorem D {A} (x y : A) : Id A x y -> Prop.
Proof.
  intros.
  apply (Id A y x).
Qed.

Theorem d {A} (x : A) : D x x (refl A x).
Proof.
  apply refl.
Admitted.

这失败了，我如何展开 D 以便我可以断言自反性？

Theorem symId' {A} {x y} : Id A x y -> Id A y x.
Proof.
  intros.

如何申请正确的论点？我如何通过策略在本地断言 D 和 d（是否有 where 或（let a = b in）策略？） apply (Id_ind A x (forall a : A, Id A x a -> Prop)).

这是我要模拟的 agda 代码

data I (A : Set) (a : A) : A → Set where
r : I A a a

J2 : {A : Set} → (D : (x y : A) → (I A x y) →  Set)
  →  (d : (a : A) → (D a a r )) → (x y : A) → (p : I A x y) → D x y p
J2 D d x .x r = d x

refl-I : {A : Set} → (x : A) → I A x x
refl-I x = r

symm-I : {A : Set} → (x y : A) → I A x y → I A y x
symm-I {A} x y p = J2 D d x y p
  where
    D : (x y : A) → I A x y → Set
    D x y p = I A y x
    d : (a : A) → D a a r
    d a = r

尽管 coq 和 agda J 不相等，但它们可能是可互导的。

Answer 1

以 Qed. 结束证明会使证明变得不透明。有时这是你想要的，但如果你想要证明的计算内容，你应该以 Defined. 结尾。

这应该可以，因为现在 D 可以展开了。

Inductive Id (A : Type) (x : A) : A -> Type :=
  | refl : Id A x x.

(* trivial with induction *)
Theorem symId {A} {x y} : Id A x y -> Id A y x.
Proof.
  intros.
  induction H.
  apply refl.
Qed.

Check Id_ind.
(* Id_ind *)
(*      : forall (A : Type) (x : A) (P : forall a : A, Id A x a -> Prop), *)
(*        P x (refl A x) -> forall (y : A) (i : Id A x y), P y i *)

Theorem D {A} (x y : A) : Id A x y -> Prop.
Proof.
  intros.
  apply (Id A y x).
Defined.

Theorem d {A} (x : A) : D x x (refl A x).
Proof.
  apply refl.
Qed.

关于你的其他问题。您可以通过两种方式显式地使用归纳法。一种是使用 Id_rect、Id_rec 或 Id_ind（这些在您定义 Id 时会自动声明）。例如，

Definition Id_sym {A: Type} {x y: A}: Id A x y -> Id A y x :=
Id_ind A x (fun y' _ => Id A y' x) (refl A x) y.

（使用一些隐式参数可能会使它更易于阅读）。

最终，这会转换为匹配语句，因此您也可以使用它。

Definition Id_sym' {A: Type} {x y: A} (p: Id A x y): Id A y x :=
  match p with
  | refl _ _ => refl _ _
  end.

要在定义中声明局部变量，可以使用let var := term in term 形式。例如，上面的 Id_sym 可以改写为

Definition Id_sym'' {A: Type} {x y: A}: Id A x y -> Id A y x :=
let P := (fun y' _ => Id A y' x) in
Id_ind A x P (refl A x) y.

如何在 coq 中明确使用归纳原理？

How to explicitly use an induction principle in coq?

equality

coq

agda

coq-tactic

homotopy-type-theory