CoqでLeibniz EqなQを書いてみる

Q.v

Require Import ZArith Znumtheory.

Open Scope Z_scope.

Section ZP.

  Record ZP := zp { quot : Z; denom : positive }.

  Definition ZP_eq (x y : ZP) :=
    quot x * (Zpos (denom y)) = quot y * (Zpos (denom x)).

  Section cancel.

    Variable x : ZP.

    Definition q := quot x.
    Definition d := denom x.

    Definition n := Zgcd q (Zpos d).

    Definition q' := q / n.
    Definition d' := (Zpos d) / n.

    Lemma n_pos: n > 0.
    Proof.
      specialize (Zgcd_is_pos q (Zpos d)).
      assert (Zgcd q (Zpos d) <> 0).
      intro. apply Zgcd_inv_0_r in H.
      congruence. unfold n. omega.
    Qed.

    Lemma dn'_n: d' * n = Zpos d.
    Proof.
      unfold d'. rewrite Zmult_comm. symmetry. apply Zdivide_Zdiv_eq.
      specialize n_pos. omega.
      assert (Zis_gcd q (Zpos d) n).
      unfold n. apply Zgcd_is_gcd.
      destruct H. auto.
    Qed.

    Lemma d'_pos : d' > 0.
    Proof.
      assert (d' * n  > 0).
      rewrite dn'_n.
      auto with zarith.
      apply Zmult_gt_0_reg_l with n.
      apply n_pos.
      rewrite Zmult_comm.
      auto.
    Qed.

    Definition d'' :=
      match d' with
      | Zpos p => p
      | Z0 => 1%positive
      | Zneg p => 1%positive
      end.

    Lemma d'_d'': d' = Zpos d''.
    Proof.
      specialize d'_pos.
      unfold d''.
      destruct d'.
      omega.
      auto.
      assert (Zneg p < 0). apply Zlt_neg_0. omega.
    Qed.

    Definition canceled := zp q' d''.

    Lemma ZP_eq_canceled: ZP_eq x canceled.
    Proof.
      unfold ZP_eq.
      simpl.
      rewrite <- d'_d''.
      apply Zmult_reg_r with n.
      specialize n_pos. omega.
      rewrite <- Zmult_assoc.
      rewrite dn'_n.
      replace (q' * Zpos (denom x) * n) with (q' * n * Zpos (denom x)).
      replace (q' * n) with q.
      auto.
      unfold q'. rewrite Zmult_comm.
      apply Zdivide_Zdiv_eq.
      specialize n_pos. omega.
      assert (Zis_gcd q (Zpos d) n).
      unfold n. apply Zgcd_is_gcd.
      destruct H. auto.
      rewrite <- Zmult_assoc. rewrite  (Zmult_comm n). auto with zarith.
    Qed.

    Lemma canceled_relprime: rel_prime (quot canceled) (Zpos (denom canceled)).
    Proof.
      simpl. unfold q'. rewrite <- d'_d''. unfold d'.
      apply Zis_gcd_rel_prime.
      auto with zarith.
      specialize n_pos. omega.
      unfold n. apply Zgcd_is_gcd.
    Qed.

    Lemma canceled_gcd: Zgcd (quot canceled) (Zpos (denom canceled)) = 1.
    Proof.
      destruct (Zgcd_1_rel_prime (quot canceled) (Zpos (denom canceled))).
      auto using canceled_relprime.
    Qed.

  End cancel.

  Lemma ZP_eq_refl: forall x, ZP_eq x x.
  Proof.
    destruct x. unfold ZP_eq. simpl. auto.
  Qed.

  Lemma ZP_eq_symm: forall x y, ZP_eq x y -> ZP_eq y x.
  Proof.
    destruct x; destruct y; unfold ZP_eq; simpl; auto with zarith.
  Qed.

  Lemma ZP_eq_trans: forall x y z, ZP_eq x y -> ZP_eq y z -> ZP_eq x z.
  Proof.
    destruct x as [a b]; destruct y as [c d]; destruct z as [e f];
      unfold ZP_eq; simpl.
    intros.
    apply Zmult_reg_r with (Zpos d).
    congruence.
    rewrite (Zmult_comm a).
    rewrite (Zmult_comm e).
    rewrite <- Zmult_assoc.
    rewrite <- Zmult_assoc.
    rewrite H. rewrite <- H0.
    ring.
  Qed.

  Lemma ZP_eq_canceled_eq: forall x y, ZP_eq x y -> canceled x = canceled y.
  Proof.
    intros.
    assert (ZP_eq (canceled x) (canceled y)).
    apply ZP_eq_trans with x.
    apply ZP_eq_symm.
    apply ZP_eq_canceled.
    apply ZP_eq_trans with y.
    auto.
    apply ZP_eq_canceled.
    generalize (canceled_relprime x).
    generalize (canceled_relprime y).
    destruct (canceled x) as [a b]. destruct (canceled) as [c d].
    intros.
    unfold ZP_eq in H0. simpl in *.
    destruct (rel_prime_cross_prod a (Zpos b) c (Zpos d)); auto with zarith.
    rewrite <- (Zmult_comm c). auto.
    congruence.
  Qed.

  Lemma canceled_idem: forall x, canceled (canceled x) = canceled x.
  Proof.
    intros. apply ZP_eq_canceled_eq.
    apply ZP_eq_symm.
    apply ZP_eq_canceled.
  Qed.

  Definition ZP_eq_dec: forall (x y : ZP), { x = y } + { x <> y }.
  Proof.
    repeat decide equality.
  Defined.

End ZP.

Section equality.

  Variable T: Type.
  Hypothesis T_eq_dec: forall (x y: T), { x = y } + { x <> y }.

  Definition eqv (x y: T) :=
    if T_eq_dec x y then true else false.

  Theorem T_eq_irrelevance: forall (x y: T) (e e': x = y), e = e'.
  Proof.
    intros x y.
    set (proj z e := match T_eq_dec x z with
                     | left e0 => e0
                     | right _ => e
                     end).
    cut (forall e e', proj y e = proj y e' -> e = e').
    unfold proj.
    intros Hinj e e'.
    apply Hinj.
    destruct (T_eq_dec x y); [reflexivity|contradiction].
    set (join y z (e: x = z) := eq_trans (z:=y) (eq_sym e)).
    assert (forall e, join y x (proj x (eq_refl x)) (proj y e) = e).
    destruct e.
    generalize (proj x (eq_refl x)).
    generalize x at -1.
    intro y.
    destruct e.
    simpl. auto.
    intros.
    rewrite <- (H e). rewrite <- (H e').
    rewrite H0. auto.
  Qed.

End equality.

Record Q := qbuild { qx : ZP; _ : canceled qx = qx }.
Definition Qmake' (x: ZP) : Q :=
  qbuild (canceled_idem (canceled x)).
Definition Qmake (quot: Z) (denom: positive) : Q :=
  Qmake' (zp quot denom).
Definition Qquot (q: Q) := quot (qx q).
Definition Qdenom (q: Q) := denom (qx q).

Definition Q_eq_dec: forall (x y: Q), { x = y } + { x <> y }.
Proof.
  destruct x as [x Hx].
  destruct y as [y Hy].
  destruct (ZP_eq_dec x y); [left|right].
  refine (
    match e in (_ = y) return 
      forall H: canceled y = y, qbuild Hx = qbuild H with
    | eq_refl => _
    end Hy).
  intro Hx'.
  assert (Heq: Hx = Hx').
  apply T_eq_irrelevance.
  apply ZP_eq_dec.
  f_equal. auto.
  intro.
  injection H.
  auto.
Qed.

Theorem ZP_eq_Q_eq: forall (x y: ZP), ZP_eq x y <-> Qmake' x = Qmake' y.
Proof.
  intros.
  split.
  intro.
  unfold Qmake'.
  specialize (ZP_eq_canceled_eq H).
  intro Heq.
  refine (
    match Heq in (_ = y) return
      forall H: ZP_eq (canceled x) y,
        qbuild (canceled_idem (canceled x)) = qbuild (canceled_idem y) with
    | eq_refl => fun _ => eq_refl _
    end _).
  rewrite Heq. apply ZP_eq_refl.
  intro.
  unfold Qmake' in H.
  assert (canceled (canceled x) = (canceled (canceled y))).
  inversion H. unfold canceled in *. congruence.
  apply ZP_eq_trans with (canceled (canceled x)).
  apply ZP_eq_trans with (canceled x); apply ZP_eq_canceled.
  apply ZP_eq_symm. rewrite H0.
  apply ZP_eq_trans with (canceled y); apply ZP_eq_canceled.
Qed.