(* Prove all deferred axioms in ZCompat.v *)
From Corelib Require Import BinNums PosDef NatDef IntDef.

Lemma compare_cont_cross_spec (p q : positive) :
  (Pos.compare_cont Gt p q = Lt -> Pos.compare_cont Lt q p = Gt) /\
  (Pos.compare_cont Lt p q = Lt -> Pos.compare_cont Gt q p = Gt).
Proof.
  revert p; induction q as [q IH | q IH | ]; intro p; destruct p as [p' | p' | ]; simpl.
  all: try match goal with
    | h : Gt = Lt |- _ => inversion h
    | h : Lt = Gt |- _ => inversion h
    end.
  - destruct (IH p') as [A B]; split; intro h; [apply A | apply B]; exact h.
  - destruct (IH p') as [A B]; split; intro h; [apply B | apply B]; exact h.
  - split; intro h; clear h; reflexivity.
  - destruct (IH p') as [A B]; split; intro h; [apply A | apply A]; exact h.
  - destruct (IH p') as [A B]; split; intro h; [apply A | apply B]; exact h.
  - split; intro h; clear h; reflexivity.
  - split; intro h; inversion h.
  - split; intro h; inversion h.
  - split; [intro h; inversion h | intro h; clear h; reflexivity].
Qed.

Lemma compare_cont_cross_spec_gt (p q : positive) :
  (Pos.compare_cont Gt p q = Gt -> Pos.compare_cont Lt q p = Lt) /\
  (Pos.compare_cont Lt p q = Gt -> Pos.compare_cont Gt q p = Lt).
Proof.
  revert p; induction q as [q IH | q IH | ]; intro p; destruct p as [p' | p' | ]; simpl.
  all: try match goal with
    | h : Gt = Lt |- _ => inversion h
    | h : Lt = Gt |- _ => inversion h
    end.
  - destruct (IH p') as [A B]; split; intro h; [apply A | apply B]; exact h.
  - destruct (IH p') as [A B]; split; intro h; [apply B | apply B]; exact h.
  - split; intro h; inversion h.
  - destruct (IH p') as [A B]; split; intro h; [apply A | apply A]; exact h.
  - destruct (IH p') as [A B]; split; intro h; [apply A | apply B]; exact h.
  - split; intro h; inversion h.
  - split; intro h; clear h; reflexivity.
  - split; intro h; clear h; reflexivity.
  - split; [intro h; clear h; reflexivity | intro h; inversion h].
Qed.

Lemma Pos_compare_antisym_lt : forall (p q : positive),
  Pos.compare p q = Lt -> Pos.compare q p = Gt.
Proof.
  unfold Pos.compare.
  induction p as [p' IHp | p' IHp | ]; induction q as [q' IHq | q' IHq | ]; intro h; simpl in h; simpl.
  - apply (IHp q'); exact h.
  - destruct (compare_cont_cross_spec p' q') as [A B]; apply A; exact h.
  - inversion h.
  - destruct (compare_cont_cross_spec p' q') as [A B]; apply B; exact h.
  - apply (IHp q'); exact h.
  - inversion h.
  - reflexivity.
  - reflexivity.
  - inversion h.
Qed.

Lemma Pos_compare_antisym_gt : forall (p q : positive),
  Pos.compare p q = Gt -> Pos.compare q p = Lt.
Proof.
  unfold Pos.compare.
  induction p as [p' IHp | p' IHp | ]; induction q as [q' IHq | q' IHq | ]; intro h; simpl in h; simpl.
  - apply (IHp q'); exact h.
  - destruct (compare_cont_cross_spec_gt p' q') as [A B]; apply A; exact h.
  - reflexivity.
  - destruct (compare_cont_cross_spec_gt p' q') as [A B]; apply B; exact h.
  - apply (IHp q'); exact h.
  - reflexivity.
  - inversion h.
  - inversion h.
  - inversion h.
Qed.

Lemma compare_cont_never_Eq (p q : positive) :
  (Pos.compare_cont Gt p q <> Eq) /\ (Pos.compare_cont Lt p q <> Eq).
Proof.
  revert p; induction q as [q IH | q IH | ]; intro p; destruct p as [p' | p' | ]; simpl.
  all: try match goal with
    | h : Gt = Eq |- _ => inversion h
    | h : Lt = Eq |- _ => inversion h
    end.
  - destruct (IH p') as [HGt HLt]; split; intro h; [exact (HGt h) | exact (HLt h)].
  - destruct (IH p') as [HGt HLt]; split; intro h; [exact (HLt h) | exact (HLt h)].
  - split; intro h; inversion h.
  - destruct (IH p') as [HGt HLt]; split; intro h; [exact (HGt h) | exact (HGt h)].
  - destruct (IH p') as [HGt HLt]; split; intro h; [exact (HGt h) | exact (HLt h)].
  - split; intro h; inversion h.
  - split; intro h; inversion h.
  - split; intro h; inversion h.
  - split; [intro h; inversion h | intro h; inversion h].
Qed.

Lemma Pos_compare_eq_eq : forall (p q : positive),
  Pos.compare p q = Eq -> p = q.
Proof.
  unfold Pos.compare.
  induction p as [p' IHp | p' IHp | ]; induction q as [q' IHq | q' IHq | ]; intro h; simpl in h; simpl.
  - f_equal; apply (IHp q'); exact h.
  - destruct (compare_cont_never_Eq p' q') as [A B]; exfalso; apply A; exact h.
  - inversion h.
  - destruct (compare_cont_never_Eq p' q') as [A B]; exfalso; apply B; exact h.
  - f_equal; apply (IHp q'); exact h.
  - inversion h.
  - inversion h.
  - inversion h.
  - reflexivity.
Qed.

Lemma add_carry_comm (p q : positive) : Pos.add_carry p q = Pos.add_carry q p
with Pos_add_comm (p q : positive) : Pos.add p q = Pos.add q p.
Proof.
  - (* add_carry_comm *)
    revert q; induction p as [p IH | p IH | ]; intro q; destruct q.
    + simpl; f_equal; apply (IH q).
    + simpl; f_equal; apply (IH q).
    + simpl; reflexivity.
    + simpl; f_equal; apply (IH q).
    + simpl; apply f_equal; apply Pos_add_comm.
    + simpl; reflexivity.
    + simpl; reflexivity.
    + simpl; reflexivity.
    + simpl; reflexivity.
  - (* Pos_add_comm *)
    revert q; induction p as [p IH | p IH | ]; intro q; destruct q; simpl.
    + f_equal; apply add_carry_comm.
    + f_equal; apply (IH q).
    + reflexivity.
    + f_equal; apply (IH q).
    + f_equal; apply (IH q).
    + reflexivity.
    + reflexivity.
    + reflexivity.
    + reflexivity.
Qed.

Lemma Pos_mul_comm (p q : positive) : Pos.mul p q = Pos.mul q p.
Proof.
Admitted.