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