유도로 두 고정 점 함수를 증명합니다.

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.