Proof objects in the identity type

Question

I'm reading through software foundation and they define equality as

Inductive eq {X:Type} : X -> X -> Prop :=
  | eq_refl : forall x, eq x x.

Notation "x == y" := (eq x y)
                       (at level 70, no associativity)
                     : type_scope.

I've been able to prove equality__leibniz_equality using tactics

Lemma equality__leibniz_equality : forall (X : Type) (x y: X),
  x == y -> forall P:X->Prop, P x -> P y.
Proof.
  intros X x y H P evP. destruct H. apply evP.
Qed.

However I also wanted to construct the proof object. This is what I tried:

Definition equality__leibniz_equality' : forall (X : Type) (x y: X),
  x == y -> forall P:X->Prop, P x -> P y :=
  fun (X:Type) (x y: X) (H: x==y) (P:X->Prop) (evP: P x) =>
  match H with
  | eq_refl a => evP
  end.

While destruct H worked in my first proof, because the tactic immediately repaced y by x, however pattern matching eq_refl a does not seem to have a similar effect, so that it seems that the information that x=y=a is lost, and I get stucked. Is there a way to construct the proof object?

Answer 1

Definition equality__leibniz_equality' : forall (X : Type) (x y: X),
  x == y -> forall P:X->Prop, P x -> P y :=
  fun (X:Type) (x y: X) (H: x==y) (P:X->Prop) =>
  match H with
  | eq_refl a => fun evP => evP
  end.

A better definition of eq which makes your definition pass is:

Inductive eq {X:Type} (x : X) : X -> Prop :=
  | eq_refl : eq x x.

You can use Print to look at the definition of any identifier. Or end the proof with Defined instead of Qed to compute with it or unfold it in another proof.