An impredicative definition of equality

Consider the following impredicative definition of Leibniz equality :
Section impredicative_eq.
 Variable A : Set.
 
 Set Implicit Arguments.

 Definition impredicative_eq (a b:A) : Prop := forall P:A -> Prop, P a -> P b.
Prove the following theorems (load library Relations before)
 Theorem impredicative_eq_sym : symmetric A impredicative_eq.

 Theorem impredicative_eq_refl : reflexive A impredicative_eq. 

 Theorem impredicative_eq_trans :  transitive A impredicative_eq.

 Theorem impredicative_eq_equiv : equiv A impredicative_eq.

 Theorem impredicative_eq_least :
  forall R:relation A, reflexive A R -> inclusion A impredicative_eq R.

 Theorem impredicative_eq_eq : forall a b:A, impredicative_eq a b -> a = b.

 Theorem eq_impredicative_eq : forall a b:A, a = b -> impredicative_eq a b.

 Theorem impredicative_eq_ind :
  forall (x:A) (P:A -> Prop), P x -> forall y:A, impredicative_eq x y -> P y.

Solution

leibniz.v
See also Some remarks


Going home
Pierre Castéran