Ich kämpfe mit scheinbar einfachen Lemma, die 2 Fixpunktdefinitionen beinhaltet. Die folgenden zwei axiale Definitionen von Farbbibliothek:zwei Fixpoint-Funktionen durch Induktion beweisen
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.
Das eigentliche 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.
Normalerweise würde ich durch Induktion über n
hier gehen, aber dies wird bekommt mich nicht viel weiter. Ich fühle mich, als würde ich hier etwas vermissen. Ich habe auch versucht program induction
hier.
Dank! Ich habe etwas Neues gelernt! (Induktion n in b, bc, bc1 | - * ') – krokodil