How to explicitly use an induction principle in coq?

Question

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.

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.

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)).

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

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

SCappella SCappella · Accepted Answer · 2020-04-26T00:56:11

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.

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.

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).

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.

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.

How to explicitly use an induction principle in coq?

1 Answers