0

以下の補題を証明したい。戦術「破壊」を使用しようとしていますが、それを証明できません。そのような補題をどのように証明できるか教えてください。EmptyString については証明できますが、変数 s1 と s2 については証明できません。ありがとう

Inductive nat : Set :=
  | O : nat
  | S : nat -> nat.

  Inductive string : Set :=
  | EmptyString : string
  | String : ascii -> string -> string.

  Fixpoint CompStrings (sa : string) (sb : string) {struct sb}: bool :=
  match sa with
  | EmptyString => match sb with
                  | EmptyString => true
                  | String b sb'=> false
                  end
  | String a sa' => match sb with
                   | EmptyString => false
                   | String b sb'=> CompStrings sa' sb'
                   end
 end.

 Lemma Eq_lenght : forall (s1 s2 : string), 
                 (CompStrings s1 s2) = true -> (Eq_nat (length s1) (length s2)) = true.
4

1 に答える 1

3

まず、スタイルについて議論させてください。関数 CompStrings を次のように記述できます。

Fixpoint CompStrings' (sa : string) (sb : string) {struct sb}: bool :=
  match sa, sb with
  | EmptyString,  EmptyString => true
  | EmptyString,  _
  | _,            EmptyString => false
  | String a sa', String b sb'=> CompStrings sa' sb'
  end.

読みやすいと思います。疑わしい場合に備えて、これがあなたのものと同じであることの証明を次に示します。

Theorem CompStrings'ok: forall sa sb, CompStrings sa sb = CompStrings' sa sb.
Proof.
  intros. destruct sa, sb; simpl; reflexivity.
Qed.

さて、これは二重の答えになります。最初に、証明の方向性を示します。次に、自分で試してみる前に読まないことをお勧めする完全な証拠を示します.

lengthまず、あなたがそれを提供しなかったので、私はこの定義を仮定しました：

Fixpoint length (s: string): nat :=
  match s with
  | EmptyString => O
  | String _ rest => S (length rest)
  end.

そして、Eq_nat も持っていなかったので、長さが命題的に等しいことを証明し始めました。Eq_nat に適応するのはかなり簡単です。

Lemma Eq_length' : forall (s1 s2 : string),
  CompStrings s1 s2 = true ->
  length s1 = length s2.
Proof.
  induction s1.
  (* TODO *)
Admitted.

それではスタートです！帰納的なデータ型 string に関するプロパティを証明したいとします。事は、場合分けで進めたいのですが、destructsだけでは終わらないのです。これが、 で進める理由inductionです。つまり、ことif s1 is the EmptyString, then the property holds、およびことを証明する必要がありますif the property holds for a substring, then it holds for the string with one character added。2 つのケースは非常に単純です。それぞれのケースで、s2 のケース分析 (つまり、 を使用destruct) によって進めることができます。

intros s1 s2 C.する前に私がしなかったことに注意してくださいinduction s1.。s2これが非常に重要な理由は 1 つあります。それを行うと (試してみてください!)、帰納仮説は、特定の について量化されるのではなく、特定の について話すため、制約が強すぎます。帰納法による証明を始めると、これは注意が必要です。したがって、この証明を続けるようにしてください。

Lemma Eq_length'_will_fail : forall (s1 s2 : string),
  CompStrings s1 s2 = true ->
  length s1 = length s2.
Proof.
  intros s1 s2 C. induction s1.
  (* TODO *)
Admitted.

最終的には、特定の について話しているため、帰納仮説を目標に適用できないことがわかりますs2。

この 2 つの演習を試していただければ幸いです。

行き詰まっている場合は、最初の目標を証明する 1 つの方法を次に示します。

カンニングしないでください！:)

Lemma Eq_length' : forall (s1 s2 : string),
  CompStrings s1 s2 = true ->
  length s1 = length s2.
Proof.
  induction s1.
  intros s2 C. destruct s2. reflexivity. inversion C.
  intros s2 C. destruct s2. inversion C. simpl in *. f_equal.
  exact (IHs1 _ C).
Qed.

それをわかりやすい言葉で言えば：

  • forall s2, CompStrings s1 s2 = true -> length s1 = s2s1 の帰納法によってプロパティを証明しましょう:

    • s1 が の場合、EmptyStrings2 の形状を見てみましょう。

      1. s2 が のEmptyString場合、両方の長さが 0 に等しいのでreflexivity.、 ;

      2. s2 は であるString _ _ため、 で示される仮説には矛盾がありinversion C.ます。

    • s1 が の場合、String char1 rest1残りのプロパティが true であると仮定して、s2 の形状を見てみましょう。

      1. s2 は であるEmptyStringため、仮説に矛盾がありinversion C.ます。

      2. s2 は であるためString char2 rest2、length s1 = S (length rest1)でlength s2 = S (length rest2)あることを証明する必要がありS (length rest1) = S (length rest2)ます。また、仮説 C は に簡略化されC: CompStrings rest1 rest2 = trueます。帰納仮説を使用して を証明しlength rest1 = length rest2、その結果を使用して目標を証明する絶好の機会です。

最後のステップでは、 を証明する方法がたくさんあることに注意してくださいS (length rest1) = S (length rest2)。f_equal.そのうちの 1 つは、コンストラクターのパラメーター間のペアワイズ等価性を証明するように要求するwhich を使用しています。rewrite (IHs1 _ C).また、その目標に対して再帰性を使用することもできます。

これがこの特定の目標を解決するだけでなく、帰納法による証明を最初に理解するのに役立つことを願っています!

これを締めくくるために、ここに 2 つの興味深いリンクがあります。

これは帰納法の基本を示しています (「リストに関する帰納法」の段落を参照してください)。

これは、帰納仮説を一般化する理由と方法を私よりもよく説明しています。誘導を開始する前に、タクティック を使用して をゴールにintros s1 s2 C.戻すことで、私が行ったゴールを解決する方法を学びます。s2generalize (dependent)

一般的に、本全体を読むことをお勧めします。テンポが遅く、非常に教訓的です。

于 2012-06-12T22:47:38.877 に答える