Eq

Eq.v

(* https://coq.inria.fr/distrib/current/refman/Reference-Manual022.html *)
Class Eq (A : Type) := {
  eqb : A -> A -> bool ;
  eqb_leibniz : forall x y, eqb x y = true -> x = y ;
  leibniz_eqb : forall x y, x = y -> eqb x y = true }.

Instance Eq_nat : Eq nat :=
  { eqb x y := beq_nat x y }.
(* eqb_leibniz *)
  intros. apply beq_nat_true. apply H.
(* leibniz_eqb *)
  induction x as [|x'].
    intros.
    rewrite <- H. reflexivity.
    intros. destruct y as [|y'].
      inversion H.
      simpl. apply IHx'. inversion H. reflexivity.
Defined.

Fixpoint beq_list {X : Type} {eq : Eq X} (xs ys : list X) : bool :=
  match (xs, ys) with
    | ([]   , []   ) => true
    | ([]   , _::_ ) => false
    | (_::_ , []   ) => false
    | (x::xt, y::yt) =>
      if eqb x y
      then beq_list xt yt
      else false
  end.

Instance Eq_list {X : Type} {eq : Eq X} : Eq (list X) :=
  { eqb xs ys := beq_list xs ys }.
Proof.
(* eqb_leibniz *)
  induction x as [|n ns].
  Case "x = []".
    intros.
    destruct y as [|m ms].
    SCase "y = []".
      reflexivity.
    SCase "y = m::ms".
      inversion H.
  Case "x = n::ns".
    destruct y as [|m ms].
    SCase "y = []".
      intros.
      inversion H.
    SCase "y = m::ms".
      intros.
      inversion H.
      destruct (eqb n m) eqn:Heqb.
      Focus 2.
      SSCase "false".
        inversion H1.
      SSCase "true".
        apply eqb_leibniz in Heqb.
        rewrite Heqb.
        apply IHns in H1.
        rewrite H1.
        reflexivity.
(* leibniz_eqb *)
  induction x as [|x xt].
    intros. rewrite <- H. reflexivity.
    intros. simpl. destruct y as [|y yt].
      inversion H.
      destruct (eqb x y) eqn:eqb_x_y.
        apply IHxt. inversion H. reflexivity.
        inversion H. inversion eqb_x_y.
        apply leibniz_eqb in H1. rewrite H1 in H3. inversion H3.
Defined.