array_set.v

Require Import Coq.Vectors.Vector.
Require Import Program.
Notation vec := Vector.t.
Notation Vnth := Vector.nth.

Notation Vnil := (@Vector.nil _).
Notation Vcons := (@Vector.cons _).
Notation Vmap := Vector.map.

Notation fin_rect2 := Fin.rect2.
Notation FS_inj := Fin.FS_inj.
Notation fin := Fin.t.
Notation FinLR := Fin.L_R.
Notation FinFS := Fin.FS.
Notation FinF1 := Fin.F1.


Lemma array_set : forall {A} {n : nat} (a : vec A n) (b : fin n) (d : A),
                    {c | forall q, ((q = b) -> Vnth c q = d) /\ ((q <> b) -> Vnth c q = Vnth a q)}.
Proof.
  intros A n a b d.
  dependent induction a.
  - inversion b.
  - dependent induction b.
    + exists (Vcons d n a).
      intros q.
      split.
      * intros eq.
        rewrite eq.
        auto.
      * intros neq.
        dependent induction q.
        contradict neq.
        reflexivity.
        auto.
    + assert (X : {c' : vec A n | forall q : fin n, (q = b -> Vnth c' q = d) /\ (q <> b -> Vnth c' q = Vnth a q)}).
      * apply IHa.
      * elim X.
        -- intros c' c'x.
           exists (Vcons h n c').
           intros q.
           split.
           ++ intros eq.
              rewrite -> eq.
              apply c'x.
              auto.
           ++ intros neq.
              dependent induction q.
              reflexivity.
              assert (neq2 : q <> b).
              ** contradict neq.
                 f_equal.
                 exact neq.
              ** apply c'x.
                 apply neq2.
Defined.