I am struggling with seemingly simple lemma which involves 2 fixpoint definitions. The following two are axially definitions from CoLoR library:
From Coq Require Import Vector Program.
Import VectorNotations.
Program Fixpoint Vnth {A:Type} {n} (v : t A n) : forall i, i < n -> A :=
match v with
| nil _ => fun i ip => !
| cons _ x _ v' => fun i =>
match i with
| 0 => fun _ => x
| S j => fun H => Vnth v' j _
end
end.
Admit Obligations.
Fixpoint Vmap {A B : Type} (f: A -> B) n (v : t A n) : t B n :=
match v with
| nil _ => nil _
| cons _ a _ v' => cons _ (f a) _ (Vmap f _ v')
end.
The actual problem:
Fixpoint Ind (n:nat) {A:Type} (f:A -> A -> A)
(initial: A) (v: A) {struct n} : t A n
:=
match n with
| O => []
| S p => cons _ initial _ (Vmap (fun x => f x v) _ (Ind p f initial v))
end.
Lemma Foo {A: Type} (n : nat) (f : A -> A -> A) (initial v : A)
(b : nat) (bc : S b < n) (bc1 : b < n)
: Vnth (Ind n f initial v) _ bc = f (Vnth (Ind n f initial v) _ bc1) v.
Proof.
Qed.
Normally I would proceed by induction on n
here but this does not gets me much further. I feel like I am missing something here. I also tried program induction
here.
You need simplification of Vnth_vmap and a generalized induction to achieve this:
From Coq Require Import Vector Program.
Import VectorNotations.
Program Fixpoint Vnth {A:Type} {n} (v : t A n) : forall i, i < n -> A :=
match v with
| nil _ => fun i ip => !
| cons _ x _ v' => fun i =>
match i with
| 0 => fun _ => x
| S j => fun H => Vnth v' j _
end
end.
Admit Obligations.
Fixpoint Vmap {A B : Type} (f: A -> B) n (v : t A n) : t B n :=
match v with
| nil _ => nil _
| cons _ a _ v' => cons _ (f a) _ (Vmap f _ v')
end.
Lemma Vnth_vmap {A B i n p} (v : t A n) f : Vnth (Vmap (B:=B) f n v) i p = f (Vnth v i p).
Proof.
induction i in n, p, v |- *. destruct v. inversion p.
simpl. reflexivity.
destruct v. simpl. bang.
simpl.
rewrite IHi. f_equal. f_equal.
(* Applies proof-irrelevance, might also be directly provable when giving the proofs in Vnth *) pi.
Qed.
Fixpoint Ind (n:nat) {A:Type} (f:A -> A -> A)
(initial: A) (v: A) {struct n} : t A n
:=
match n with
| O => []
| S p => cons _ initial _ (Vmap (fun x => f x v) _ (Ind p f initial v))
end.
Lemma Foo {A: Type} (n : nat) (f : A -> A -> A) (initial v : A)
(b : nat) (bc : S b < n) (bc1 : b < n)
: Vnth (Ind n f initial v) _ bc = f (Vnth (Ind n f initial v) _ bc1) v.
Proof.
induction n in b, bc, bc1 |- *; simpl.
- bang.
- rewrite Vnth_vmap. f_equal.
destruct b.
+ destruct n. simpl. bang. simpl. reflexivity.
+ rewrite Vnth_vmap. apply IHn.
Qed.