Dep_rewrite.v

Require Import List Utf8 Vector Fin Psatz.
Import Notations.

Section Iso.

  
  Definition fin (n : nat) : Type := {i | i < n}.

  Theorem fin_to_Fin : ∀ (n : nat), fin n -> Fin.t n.
  Proof.
    (* I can't do induction on Ha *)
    induction n;
    intros [i Ha].
    + abstract nia.
    +
      (* case analysis on i *)
      destruct i as [| i].
      ++
        exact Fin.F1.
      ++
        eapply Arith_prebase.lt_S_n in Ha.
        specialize (IHn (exist _ i Ha)).
        exact (Fin.FS IHn).
  Defined.

 
  
  Theorem Fin_to_fin : ∀ (n : nat), Fin.t n -> fin n.
  Proof.
    induction n; 
    intro fn.
    + refine match fn with end.
    +
      refine 
        (match fn as fn' in Fin.t n' 
          return ∀ (pf : n' = S n), 
          fn = @eq_rect _ n' (fun t => Fin.t t) fn' _ pf -> _ 
        with 
        | Fin.F1 => fun Ha Hb => (exist _ 0 _)
        | Fin.FS fw => fun  Ha Hb => _
        end eq_refl eq_refl).
      ++ abstract nia.
      ++
        (* In this rewrite, I am trying to 
          replace (S n0) by (S n) because 
          (FS t) has type (Fin.t (S n0)) and 
          it's changing the type to (Fin.t (S n))
          so fail is fine.
        *)
        Fail rewrite Ha in Hb.
        (* Lets revert Hb and fw whose 
          types involve n0 
        *)
        revert fw Hb.
         (* WHY DOES THIS REWRITE FAILS?
          Now our goal is general enough 
          where we can replace n0 by n. 
        *)
        Fail rewrite Ha.
        (* even if I generalised Ha *)
        assert (Hb : n0 = n) by nia.
        revert Ha.
        (* Yay! rewrite works *)
        rewrite Hb; clear Hb.
              
  Admitted.