Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.