誘導によって2つの固定点関数を証明する

Question

2つの固定点定義を含む一見単純な補助定理に苦しんでいます。次の二つの軸方向カラーライブラリからの定義は以下のとおりです。

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. 

実際の問題：

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. 

通常、私はここにnに誘導することによって進行するであろうが、これは更に多くの私を取得しません。私はここで何かを逃しているように感じる。私もprogram inductionを試しました。

Answer 1

あなたはこれを達成するためにVnth_vmapの簡素化と一般化の誘導を必要とする：

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.