Library Eqle.diag_nat_inv

Require Import Utf8.

Inductive diag : nat → nat → Prop :=
| dia0 : diag 0 0
| diaS x y : diag x y → diag (S x) (S y).

Inductive is_dia0 : diag 0 0 → Prop := ii00 : is_dia0 dia0.
Inductive is_diaS x y : diag (S x) (S y) → Prop :=
  iiSS : ∀ (d : diag x y), is_diaS x y (diaS x y d).
Inductive no_diag x y : diag x y → Prop := .
Definition diag_inv {x y} (d : diag x y) :
  match x, y return diag x y → Prop with
  | 0, 0 ⇒ is_dia0
  | S x, S y ⇒ is_diaS x y
  | x, y ⇒ no_diag x y
  end d.
Proof. destruct d; constructor. Qed.

Lemma diag_refl {x} : diag x x.
Proof. induction x as [ | x IHx]; constructor. apply IHx. Defined.

Lemma eq_diag {x y} (e : x = y) : diag x y.
Proof. case e. apply diag_refl. Defined.

Lemma diag_back {x} : ∀ {y}, diag x y → x = y.
Proof.
  induction x as [ | x IHx]; destruct y as [ | y];
    intro d; destruct (diag_inv d).
  - reflexivity.
  - apply f_equal, (IHx y d).
Defined.

Lemma diag_back_isrefl {x} : ∀ (d : diag x x), eq_refl = diag_back d.
Proof.
  induction x as [ | x IHx]; simpl; intro d.
  - destruct (diag_inv d). reflexivity.
  - destruct (diag_inv d) as [d]. case (IHx d). cbn. reflexivity.
Qed.

Lemma diag_mono {x y} (e : x = y) : e = diag_back (eq_diag e).
Proof.
  destruct e. destruct x as [ | x]; simpl.
  + destruct (diag_inv dia0); reflexivity.
  + destruct (diag_inv (diaS x x diag_refl)) as [d]. case (diag_back_isrefl d); reflexivity.
Qed.

Corollary UIP_nat_smallinv (x: nat) (e : x = x) : eq_refl = e.
Proof. rewrite (diag_mono e). apply diag_back_isrefl. Qed.

Fixpoint unique_diag x y (d : diag x y) : ∀ d', d = d'.
Proof.
  destruct d as [ | x y d]; intro d'.
  - destruct (diag_inv d'). reflexivity.
  - destruct (diag_inv d') as [d']. apply f_equal, (unique_diag x y d d').
Qed.


Fixpoint diagTF (x y : nat) : Prop :=
  match x, y with
  | 0, 0 ⇒ True
  | S x, S y ⇒ diagTF x y
  | _, _ ⇒ False
  end.


Definition diagTF_refl {x} : diagTF x x.
Proof. induction x as [ | x IHx]; cbn; [ exact I | exact IHx]. Defined.

Definition eq_diagTF {x y} (e : x = y) : diagTF x y.
Proof. case e. apply diagTF_refl. Defined.

Definition diagTF_back {x y} : ∀ (tf : diagTF x y), x = y.
Proof.
  revert y; induction x as [ | x IHx];
    intro y; destruct y as [ |y] ; cbn; intro tf; try destruct tf.
  - reflexivity.
  - apply f_equal, IHx, tf.
Defined.

Definition diagTF_back_isrefl {x} : ∀ (tf : diagTF x x), eq_refl = diagTF_back tf.
Proof.
  induction x as [ | x IHx]; simpl; intro tf.
  - case tf; reflexivity.
  - case (IHx tf). cbn. reflexivity.
Qed.

Lemma diagTF_mono {x y} (e : x = y) : e = diagTF_back (eq_diagTF e).
Proof.
  destruct e. destruct x as [ | x]; simpl.
  + reflexivity.
  + case (diagTF_back_isrefl diagTF_refl). reflexivity.
Qed.

Corollary UIP_diagTF (x: nat) (e : x = x) : eq_refl = e.
Proof. rewrite (diagTF_mono e). apply diagTF_back_isrefl. Qed.

Corollary UIP_diagTF2 (x y: nat) (e e' : x = y) : e = e'.
Proof. revert e'. case e. apply UIP_diagTF. Qed.

Fixpoint diagTF_unique (x y : nat) : ∀ (d d' : diagTF x y), d = d' :=
  match x, y return ∀ (d d' : diagTF x y), d = d' with
  | 0, 0 ⇒ λ d d', match d, d' with I, I ⇒ eq_refl end
  | S x, S y ⇒ λ d d', diagTF_unique x y d d'
  | _, _ ⇒ λ d, match d with end
  end.

Corollary UIP_diagTF2_alt (x y: nat) (e e' : x = y) : e = e'.
Proof. rewrite (diagTF_mono e), (diagTF_mono e'). apply f_equal, diagTF_unique. Qed.




Lemma UIP_refl_nat (n:nat) (e : n = n) : e = eq_refl.
Proof.
  induction n as [|n IHn].
  - change (match 0 as n return 0 = n → Prop with
            | 0 ⇒ fun e ⇒ e = eq_refl
            | _ ⇒ fun _ ⇒ False
            end e).
    destruct e; reflexivity.
  - specialize IHn with (f_equal pred e).
    change eq_refl with (f_equal S (@eq_refl _ n)).
    rewrite <- IHn; clear IHn.
    change (match S n as n' return S n = n' → Prop with
            | 0 ⇒ fun _ ⇒ False
            | S n' ⇒ fun e ⇒
                e = f_equal S (f_equal pred e)
            end e).
  pattern (S n) at 2 3, e.
  destruct e; reflexivity.
Defined.