Leibniz.v

From Stdlib Require Import Utf8.


Section Equality.

  (* https://xavierleroy.org/CdF/2018-2019/10.pdf *)
  Definition Leibniz_eq {A : Type} (x y : A) : Prop :=
    ∀ (P : A -> Prop), P x <-> P y.
    
  Theorem Leibniz_equality_forward {A : Type} : 
    ∀ (x y : A), x = y -> Leibniz_eq x y.
  Proof.
    intros * ha.
    refine match ha in _ = y' return Leibniz_eq x y' 
    with 
    | eq_refl => ltac:(firstorder) 
    end.
  Qed.
  


  Theorem Leibniz_equality_backward {A : Type} : 
    ∀ (x y : A), Leibniz_eq x y -> x = y.
   Proof.
    intros * ha *.
    eapply ha. 
    exact eq_refl.
  Defined.
  
End Equality.