1

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?

3 Answers 3

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

1

It may also be interesting to look at the elimination principles generated by Coq, and play with Check. With your definition:

Check eq_ind.
(*
eq_ind
     : forall (X : Type) (P : X -> X -> Prop),
       (forall x : X, P x x) -> forall y y0 : X, eq y y0 -> P y y0
*) 

Check fun (X: Type)(Q: X -> Prop) =>
        eq_ind _ (fun x y  => Q x -> Q y) (fun x Hx => Hx). 

fun (X : Type) (Q : X -> Prop) =>
eq_ind X (fun x y : X => Q x -> Q y) (fun (x : X) (Hx : Q x) => Hx)
     : forall (X : Type) (Q : X -> Prop) (y y0 : X), eq y y0 -> Q y -> Q y0

You may also compare this version of eq with Coq's Logic.eq(cf. Li-yao Xia's answer) by asking for the type of Logic.eq_ind. Please note also there is no eq_rec nor eq_rect with your definition (in contrast to Logic.eq)

0
Definition equality__leibniz_equality'' (X : Type) (x y: X) (H : x == y) (P : X -> Prop)
  : P x -> P y :=
    match H with
    | eq_refl x0 => id
    end.
                                            
Lemma equality__leibniz_equality''' : forall (X : Type) (x y: X),
    x == y -> forall P:X -> Prop, P x -> P y.
Proof.
  exact equality__leibniz_equality''.
Qed.   
1
  • Your answer could be improved with additional supporting information. Please edit to add further details, such as citations or documentation, so that others can confirm that your answer is correct. You can find more information on how to write good answers in the help center.
    – Community Bot
    Nov 4 at 13:51

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.