
(* This file defines nat_cast, an alternative to eq_rect which works only for type nat instead
   of any type A.
   The motivation behind nat_cast is that it only matches on proofs in contradictory cases,
   so functions using nat_cast can always be run inside Coq using cbv, whereas function using
   eq_rect cannot. *)

Arguments id {A} x.

(* Transport equality, only matching on eq_refl in contradictory cases, to make sure
   terms using this function reduce *)
Fixpoint nat_cast (P : nat -> Type) {n m} : n = m -> P n -> P m.
  refine match n, m return n = m -> P n -> P m with
         | O, O => fun _ => id
         | S n, S m => fun pf => @nat_cast (fun n => P (S n)) n m (f_equal pred pf)
         | _, _ => fun pf => match _ pf : False with end
         end;
    clear; abstract congruence.
Defined. (* thx Jason *)

Lemma nat_cast_eq_rect: forall (P : nat -> Type),
  forall (n m : nat)  (e: n = m) (pn: P n),
  nat_cast P e pn = eq_rect n P pn m e.
Proof.
(* Goal: forall (P : forall _ : nat, Type) (n m : nat) (e : @eq nat n m) (pn : P n), @eq (P m) (@nat_cast P n m e pn) (@eq_rect nat n P pn m e) *)
  destruct e.
(* Goal: forall pn : P n, @eq (P n) (@nat_cast P n n (@eq_refl nat n) pn) (@eq_rect nat n P pn n (@eq_refl nat n)) *)
  revert dependent P; induction n; simpl; intros.
  - reflexivity.
  - rewrite IHn. reflexivity.
Qed. (* thx Clement *)

Lemma nat_cast_proof_irrel: forall (P : nat -> Type),
  forall (n m : nat)  (e1 e2: n = m) (pn: P n),
  nat_cast P e1 pn = nat_cast P e2 pn.
Proof.
  destruct e1.
(* Goal: forall pn : P n, @eq (P n) (@nat_cast P n n (@eq_refl nat n) pn) (@eq_rect nat n P pn n (@eq_refl nat n)) *)
  revert dependent P; induction n; simpl; intros.
  - reflexivity.
  - erewrite IHn. reflexivity.
Qed.

Lemma nat_cast_same: forall (P: nat -> Type) (s: nat) (n: P s),
  nat_cast P eq_refl n = n.
Proof.
(* Goal: @eq (P n1) (@nat_cast P n1 n1 (@eq_refl nat n1) x) (@nat_cast P n1 n1 (@eq_trans nat n1 n1 n1 (@eq_refl nat n1) (@eq_refl nat n1)) x) *)
  intros. rewrite nat_cast_eq_rect. reflexivity.
Qed.

Lemma nat_cast_fuse: forall (P: nat -> Type) (n1 n2 n3: nat) (e12: n1 = n2) (e23: n2 = n3) (x: P n1),
  nat_cast P e23 (nat_cast P e12 x) = nat_cast P (eq_trans e12 e23) x.
Proof.
(* Goal: forall (P : forall _ : nat, Type) (n1 n2 n3 : nat) (e12 : @eq nat n1 n2) (e23 : @eq nat n2 n3) (x : P n1), @eq (P n3) (@nat_cast P n2 n3 e23 (@nat_cast P n1 n2 e12 x)) (@nat_cast P n1 n3 (@eq_trans nat n1 n2 n3 e12 e23) x) *)
  destruct e12.
(* Goal: forall (e23 : @eq nat n1 n3) (x : P n1), @eq (P n3) (@nat_cast P n1 n3 e23 (@nat_cast P n1 n1 (@eq_refl nat n1) x)) (@nat_cast P n1 n3 (@eq_trans nat n1 n1 n3 (@eq_refl nat n1) e23) x) *)
  destruct e23.
(* Goal: forall x : P n1, @eq (P n1) (@nat_cast P n1 n1 (@eq_refl nat n1) (@nat_cast P n1 n1 (@eq_refl nat n1) x)) (@nat_cast P n1 n1 (@eq_trans nat n1 n1 n1 (@eq_refl nat n1) (@eq_refl nat n1)) x) *)
  intros.
(* Goal: @eq (P ni) (@nat_cast P ni ni (@eq_refl nat ni) x) x *)
  rewrite nat_cast_same.
(* Goal: @eq (P n1) (@nat_cast P n1 n1 (@eq_refl nat n1) x) (@nat_cast P n1 n1 (@eq_trans nat n1 n1 n1 (@eq_refl nat n1) (@eq_refl nat n1)) x) *)
  reflexivity.
Qed.

Lemma nat_cast_cast ni no (pf: ni = no) (P: nat -> Type) (x : P ni):
  nat_cast P pf x = match pf in _ = Y return P Y with
                    | eq_refl => x
                    end.
Proof.
(* Goal: @eq (P no) (@nat_cast P ni no pf x) match pf in (eq _ Y) return (P Y) with | eq_refl => x end *)
  destruct pf.
(* Goal: @eq (P ni) (@nat_cast P ni ni (@eq_refl nat ni) x) x *)
  rewrite nat_cast_same.
(* Goal: @eq (P ni) x x *)
  auto.
Qed.
