Простое доказательство потока единиц в 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

Как мне доказать, что для всех n дано approx, список будет содержать только 1? Я даже не уверен, как это сформулировать. Должен ли я использовать функцию помощи, как nth n list для списков, которые возвращают номер элемента n от list? И это

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.

Лучший,

В