如何在Coq中明确使用归纳原理？ [英] How to explicitly use an induction principle in coq?

问题描述

我试图用Coq中的归纳原理明确证明命题同一性的对称性，但是我不能像agda中那样用归纳原理做到这一点。我不知道如何在Coq中本地声明变量，也不知道如何展开定义，如下所示。如何获得类似于下面的agda的证明？

I'm trying to prove symmetry of propositional identity with the induction principal explicitly in Coq, but can't do it with the induction principle like I can in agda. I don't know how to locally declare a variable in Coq, nor do I know how to unfold a definition, as you can see below. How can I get a proof that resembles the agda one below?

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以便断言反射性？

This fails, how can I unfold D so that I can just assert reflexivity?

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

我如何适用于正确的论点？我如何才能通过战术在本地断言D和d（是否存在where或（让a = b进入）战术？）
适用于（Id_ind A x（forall a：A，Id A xa-> Prop））。

how do I apply to the correct arguements? How can I locally assert D and d via tactics (is there a where or (let a = b in) tactic ?) apply (Id_ind A x (forall a : A, Id A x a -> Prop)).

这是我要模拟的agda代码

Here is the agda code I'm trying to emulate

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不相等，它们大概是可互换的。

Even though the coq and agda J's aren't equal, they are presumably interderivable.

推荐答案

以 Qed结尾一个证明。使该证明不透明。有时这就是您想要的，但是如果您想要证明的计算内容，则应以 Defined。结尾。

Ending a proof with Qed. makes the proof opaque. Sometimes this is what you want, but if you ever want the computational content of a proof, you should end it with Defined. instead.

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

This should work since now D can be unfolded.

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 时会自动声明）。例如，

---

As for your other questions. You can explicitly use induction in two ways. One is to use Id_rect, Id_rec or Id_ind (these are automatically declared when you define Id). For example,

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.

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

(using some implicit arguments might make this easier to read).

最终，它将转换为match语句，因此您也可以使用它。

Ultimately, this gets converted into a match statement, so you could use that too.

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 可以重写为

---

To declare a local variable in a definition, you can use the let var := term in term form. For example, Id_sym above could be rewritten as

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中明确使用归纳原理？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！