Coq中一个流的简单证明

Question

从CPDT中获取代码，我想证明易流ones的一个属性，它总是返回1。

CoFixpoint ones : Stream Z := Cons 1 ones.

同样在CPDT中，我使用此函数从流中检索列表：

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的列表，例如：

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

我如何证明，对于给定给approx的所有n，列表将只包含1？我甚至不知道该如何表述。我应该为列表使用类似nth n list的帮助函数吗？该函数从list返回元素编号n？而

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

（或者可以使用Zeq而不是=。）

我的方向对吗？

Answer 1

我认为拥有比点式nth列表视图更通用的视图将更容易处理。以下是我的做法（证明是0自动化，以确保你看到一切）：

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. 

如果你更喜欢all_ones的功能性定义，这里有一些等效的定义：

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.

最佳，

V