Coq에있는 스트림의 간단한 증거

Question

CPDT에서 코드를 작성하면 쉬운 스트림 ones에 대한 속성을 증명하고 싶습니다. 항상 1을 반환합니다.

Eval compute in approx Z ones 5. 
= 1 :: 1 :: 1 :: 1 :: 1 :: nil 
    : list Z 

가 어떻게 작업을 수행합니다,

Fixpoint approx A (s:Stream A) (n:nat) : list A := 
    match n with 
    | O => nil 
    | S p => match s with 
     | Cons h t => h :: approx A t p 
     end 
    end. 

다섯 1의 목록을 가져 오려면 예를 :

CoFixpoint ones : Stream Z := Cons 1 ones. 

또한 CPDT에서, 나는 스트림에서 목록을 검색하려면이 기능을 사용 모든 n에 대해 approx이 주어지면 그 목록에는 1 만 포함될 것임을 증명합니다. 나는 이것을 공식화하는 방법조차 모릅니다. 목록에 nth n list과 같은 도움말 기능을 사용해야하는 경우 요소 번호 n을 list에서 반환합니까? 그리고 그

forall (n length : nat), nth n1 (approx Z ones length) = 1 

(아니면 Zeq 대신 =를 사용합니다.)

내가 올바른 방향을 향하고 있습니까?

Answer 1

나는보기보다 일반적인 관점을 가지고 있다고 생각한다.

Fixpoint fix_all_ones (l: list Z) : Prop := match l with 
    | nil => True 
    | 1%Z :: tl => fix_all_ones tl 
    | _ => False 
end. 

Fixpoint fix_bool_all_ones (l: list Z) : bool := match l with 
    | nil => true 
    | 1%Z :: tl => fix_bool_all_ones tl 
    | _ => false 
end. 

Lemma equiv1 : forall l, all_ones l <-> fix_all_ones l. 
Proof. 
induction l as [ | hd tl hi]; split; intros h; simpl in *. 
- now idtac. 
- now constructor. 
- destruct hd; simpl in *. 
    + now inversion h; subst; clear h. 
    + inversion h; subst; clear h. 
    now apply hi. 
    + now inversion h; subst; clear h. 
- destruct hd; simpl in *. 
    + now case h. 
    + destruct p; simpl in *. 
    * now case h. 
    * now case h. 
    * constructor; now apply hi. 
    + now case h. 
Qed. 

Lemma equiv2 : forall l, fix_all_ones l <-> fix_bool_all_ones l = true. 
Proof. 
induction l as [ | hd tl hi]; split; intros h; simpl in *. 
- reflexivity. 
- now idtac. 
- destruct hd; simpl in *. 
    + now case h. 
    + destruct p; simpl in *. 
    * now case h. 
    * now case h. 
    * now apply hi. 
    + now case h. 
- destruct hd; simpl in *. 
    + discriminate h. 
    + destruct p; simpl in *. 
    * now case h. 
    * now case h. 
    * now apply hi. 
    + discriminate h. 
Qed. 

: 당신이 어떤 상응하는 정의를 여기 all_ones의 더 많은 기능 정의를 선호하는 경우

Inductive all_ones : list Z -> Prop := 
    | nil_is_ones : all_ones nil (* nil is only made of ones *) 
    (* if l is only made of ones, 1 :: l is too *) 
    | cons_is_ones : forall l, all_ones l -> all_ones (cons 1%Z l) 
    (* and these are the only option to build a list only made of ones 
. 

CoFixpoint ones : Stream Z := Cons 1%Z ones. 

Fixpoint approx A (s:Stream A) (n:nat) : list A := 
    match n with 
    | O => nil 
    | S p => match s with 
     | Cons h t => h :: approx A t p 
     end 
    end. 

Lemma approx_to_ones : forall n, all_ones (approx _ ones n). 
Proof. 
induction n as [ | n hi]; simpl in *. 
- now constructor. 
- constructor. 
    now apply hi. 
Qed. 

: 여기에 간다 얼마나이다 (증거는 당신이 모든 것을 볼 확실하게 0 자동화입니다) 최고,

v