3

Coqの「実践的結合」の最初の例を証明しようとしています。最初の例は、整数の無限ストリームの辞書編集順序が推移的であることを証明することです。

Guardedness 条件を回避するための証明を定式化できていません

これが私のこれまでの開発です。まず、無限ストリームの通常の定義です。次に、 と呼ばれる辞書編集順序の定義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.

ここから先はどうすればいいですか？ヒントをありがとう！

  • 編集

Arthur の (いつものように!) 有益で啓発的な回答のおかげで、私も証明を完成させることができました。参考までに私のバージョンを以下に示します。 

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の値を「拡張」します。ここ (と)の定義は、実用的結合の逐語的な定式化により近いです。Arthur は、Coq が値を自動的に拡張する、より洗練された手法を使用しています。s1s3lexheadtail

4

1 に答える 1

5

あなたの証拠の問題の 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

結果のアプリケーションが保護されている限り、ストリームの末尾に簡単に適用できます。

于 2015-03-19T02:33:58.923 に答える