Coq_dep_to_math_comp.v

Require Import Field_theory 
  Ring_theory List NArith 
  Ring Field Utf8 Lia 
  Coq.Arith.PeanoNat
  Vector Fin Lia.
From mathcomp Require Import 
  all_ssreflect algebra.matrix
  algebra.ssralg.


(* These two are just need because it's 
    opaque in library *)
Lemma introT : 
  forall (P : Prop) (b : bool), 
  reflect P b -> P -> b.
Proof.
  intros ? ? Hr Hp.
  case b eqn:Ht.
  constructor.
  inversion Hr as [_ | Hrt].
  unfold not in Hrt.
  specialize (Hrt Hp).
  exfalso.
  exact Hrt.
Defined.

Lemma elimT :
  forall (P : Prop) (b : bool), 
  reflect P b -> b -> P.
Proof.
  intros ? ? Hr H.
  case b eqn:Hb.
  inversion Hr as [Hrt | _].
  exact Hrt.
  refine (match H with end).
Defined.


Definition finite_to_ord {n} (f : Fin.t n) : 'I_n.
  destruct (to_nat f) as [m Hm].
  apply (@introT _ _ ltP) in Hm.
  apply (Ordinal Hm).
Defined.



Definition ord_to_finite {n} (x : 'I_n) : Fin.t n.
  have Hx: x < n by [].
  apply (@elimT _ _ ltP) in Hx.
  apply (of_nat_lt Hx).
Defined.

Lemma fin_inv_0 (i : Fin.t 0) : False.
Proof. refine (match i with end). Defined.

Lemma fin_inv_S (n : nat) (i : Fin.t (S n)) :
  (i = Fin.F1) + {i' | i = Fin.FS i'}.
Proof.
  refine (match i with
          | Fin.F1 _ => _
          | Fin.FS _ _ => _
          end); eauto.
Defined.


Lemma finite_to_ord_correctness n (i : Fin.t n) :
    ord_to_finite (finite_to_ord i) = i.
Proof.
  induction n.
  + inversion i.
  + pose proof fin_inv_S _ i as [-> | (i' & ->)].
    ++ cbn; reflexivity.
    ++  specialize (IHn i').
        unfold 
        finite_to_ord,
        ord_to_finite,
        ssr_have in * |- *.
        (* Thing below lead to off by one term in goal *)
        cbn in * |- *.          
        destruct (to_nat i') as [a Ha].
        cbn.
        f_equal.
        cbn in *.
        Check Lt.lt_S_n.
Admitted.

  Lemma ord_to_finite_correctness n (i : 'I_n) :
    finite_to_ord (ord_to_finite i) = i.
  Proof.
    apply (@ordinal_ind n 
      (fun i => finite_to_ord (ord_to_finite i) = i)).
    induction n.
    + intros m Hi.
      (* I can't discharge it! *)
      admit.
    + destruct m;
      intros Hi. 
      ++ cbn.
        (* Hi should be (erefl true) 
          becuase it's a decidable 
          proposition
          but how I can infer that *)   
        f_equal.
        admit.
      ++ (* From Hi *)
        cbn.
        unfold finite_to_ord.
        destruct to_nat.
        (* Now, I don't know how to prove this! *)
          

       
  Admitted.