Доказательство коиндуктивного свойства (лексическое упорядочение транзитивно) в Coq

Question

Я пытаюсь доказать первый пример в "Практической коиндукции" в Coq. Первый пример - доказать, что лексикографическое упорядочение бесконечных потоков целых чисел транзитивно.

Я не смог сформулировать доказательства, чтобы обойти условие Охраняемости

Вот мое развитие до сих пор. Сначала просто обычное определение бесконечных потоков. Тогда определение лексикографического порядка называется lex, И в итоге несостоятельное доказательство теоремы транзитивности.

Require Import Omega.

Section stream.
  Variable A:Set.

  CoInductive Stream : Set :=
  | Cons : A -> Stream -> Stream.

  Definition head (s : Stream) :=
    match s with Cons a s' => a end.

  Definition tail (s : Stream) :=
    match s with Cons a s' => s' end.

  Lemma cons_ht: forall s, Cons (head s) (tail s) = s.
    intros. destruct s. reflexivity. Qed.

End stream.

Implicit Arguments Cons [A].
Implicit Arguments head [A].
Implicit Arguments tail [A].
Implicit Arguments cons_ht [A].

CoInductive lex s1 s2 : Prop :=
  is_le :   head s1 <= head s2 ->
            (head s1 = head s2 -> lex (tail s1) (tail s2)) ->
            lex s1 s2.


Lemma lex_helper: forall s1 s2,  
        head s1 = head s2 -> 
        lex (Cons (head s1) (tail s1)) (Cons (head s2) (tail s2)) -> 
        lex (tail s1) (tail s2).
Proof. intros; inversion H0; auto. Qed.

Вот лемма, которую я хочу доказать. Я начинаю с подготовки цели, чтобы я мог применить конструктор, надеясь, что в конечном итоге смогу использовать "гипотезу" из cofix,

Lemma lex_lemma : forall s1 s2 s3, lex s1 s2 -> lex s2 s3 -> lex s1 s3.
  intros s1 s2 s3 lex12 lex23.
  cofix.
  rewrite  <- (cons_ht s1).
  rewrite  <- (cons_ht s3).
  assert (head s1 <= head s3) by (inversion lex12; inversion lex23; omega).
  apply is_le; auto.

  simpl; intros. inversion lex12; inversion lex23.
  assert (head s2 = head s1) by omega.

  rewrite <- H0, H5 in *.
  assert (lex (tail s1) (tail s2)) by (auto).
  assert (lex (tail s2) (tail s3)) by (auto).

  apply lex_helper.
  auto.
  repeat rewrite cons_ht.
  Guarded.

Как мне продолжить отсюда? Спасибо за любые подсказки!

• РЕДАКТИРОВАТЬ

Благодаря полезному и поучительному ответу Артура (как всегда!) Я тоже смог завершить доказательство. Я даю свою версию ниже для справки.

Lemma lex_lemma : forall s1 s2 s3, lex s1 s2 -> lex s2 s3 -> lex s1 s3.
  cofix.
  intros s1 s2 s3 lex12 lex23.
  inversion lex12; inversion lex23.
  rewrite  <- (cons_ht s1).
  rewrite  <- (cons_ht s3).
  constructor; simpl.
  inversion lex12; inversion lex23; omega.
  intros; eapply lex_lemma; [apply H0 | apply H2]; omega.
Qed.

Я использую cons_ht лемма "расширить" значение s1 а также s3, Определение lex здесь (с head а также tail) ближе к дословной формулировке в Практической коиндукции. Артур использует более элегантную технику, которая заставляет Coq автоматически расширять значения - намного приятнее!

Answer 1

Одна проблема с вашими доказательствами заключается в том, что вы позвонили cofix слишком поздно, после s1 s2 s3 был введен. Как следствие, коиндуктивная гипотеза, которую вы получаете, lex s1 s2, не очень полезен: чтобы применить его, оставаясь охраняемым, как вы упомянули, мы должны сделать это после применения конструктора lex, Однако после этого нам нужно будет показать в какой-то момент, что lex (tail s1) (tail s3) имеет место, где гипотеза, представленная cofix не могу сделать ничего хорошего.

Чтобы решить эту проблему, нам нужно выполнить вызов cofix прежде чем вводить переменные, чтобы выдвигаемая им гипотеза была достаточно общей. Я позволил себе переформулировать ваше определение lex, так что в таком доказательстве легче манипулировать:

CoInductive lex : Stream nat -> Stream nat -> Prop :=
| le_head n1 n2 s1 s2 : n1 < n2 -> lex (Cons n1 s1) (Cons n2 s2)
| le_tail n s1 s2 : lex s1 s2 -> lex (Cons n s1) (Cons n s2).

Lemma lex_trans : forall s1 s2 s3, lex s1 s2 -> lex s2 s3 -> lex s1 s3.
Proof.
  cofix.
  intros s1 s2 s3 lex12 lex23.
  inversion lex12; subst; clear lex12;
  inversion lex23; subst; clear lex23;
  try (apply le_head; omega).
  apply le_tail; eauto.
Qed.

Теперь гипотеза имеет вид

forall s1 s2 s3, lex s1 s2 -> lex s2 s3 -> lex s1 s3

который может быть легко применен к хвосту наших потоков, пока полученное приложение охраняется.