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?