0

文字列の「再帰性」プロパティを証明したいと思います。証明の進め方を教えていただけませんか。これが私のコードです：

    Fixpoint beq_str (sa sb : String.string) {struct sb}: bool := 
   match sa, sb with
 | EmptyString, EmptyString  => true
 | EmptyString, String b sb' => false
 | String a sa', EmptyString => false
 | String a sa', String b sb'=> match (ascii_dec a b) with 
                                | left _ => beq_str sa' sb'
                                | right _ => false
                                end
 end.
 (* compares two string names [n1] and [n2] of type [id'] - returs bool. *) 
 Definition beq_names n1 n2 :=
  match (n1, n2) with
    (name s1, name s2) => beq_str s1 s2
  end.

 Theorem reflexivty : forall i,
  true = beq_str i i.
Proof.
  intros. induction i.
  auto.  simpl. Admitted.
4

1 に答える 1

1

宿題か自主研究かわからない...

Theorem beq_str_refl : forall i,
  true = beq_str i i.
Proof.
  induction 0; simpl; try (rewrite <- IHi; case (ascii_dec a a));
  try reflexivity; intro C; elimtype False; apply C; reflexivity.
Qed.

これは機能するはずです。

これが宿題であなたが怠け者である場合、あなたの家庭教師はうまくいけばこれを拒否するでしょう。自分で理解して証明したい場合は、必要な構成要素がそこにあります。それを分解して、現在の証明状態で断片を投げてください。

この証明には2つの厄介なことがあります。最初のものはを取り除くこと(ascii_dec a a)です。（ケース分析は機能しaません。）全体に対してケース分析を実行して（つまり(ascii_dec a a)）、2つのサブゴールを取得します。1つは仮説を追加し、もう1つは。a = aを使用しa <> aます。

2番目の問題は、以前にそれを行ったことがない限り、矛盾を処理している可能性があります。

a <> aと同等a = a -> Falseです。 a = a定義上trueであり、型の値を作成できますFalse（矛盾-Falseコンストラクターはありません）。これにより、現在の目標を捨てて（true = falseとにかく証明することは不可能です）、その不可能なFalse値を構築することができます。

elimtype FalseCoqに、のケース分析で続行することを伝えてくださいFalse。Falseコンストラクターがないため、これにより、値を構築するという単一の目標が残りますFalse。通常、それは不可能ですが、仮説の間に矛盾があります。 applyこの矛盾（C上記の私の証明スクリプトで名前が付けられています）とあなたがしなければならないのはa = a、から続くshowだけですreflexivity。

ステップスルーできる、より読みやすいバージョンを次に示します。

Theorem beq_str_refl : forall i, true = beq_str i i.
  intro i. induction i as [ | a i IHi ].
    (* base case: Empty String *) reflexivity.
    (* inductive case: *) simpl. rewrite <- IHi.
      (* do case analysis on ascii_dec (or {a=a}+{a<>a}) *)
      destruct (ascii_dec a a) as [ Heq | C ].
      (* {a =  a} *) reflexivity.
      (* {a <> a} *) unfold not in C. elimtype False. apply C. reflexivity.

矛盾を処理する別の方法：

(* just a quick nonsensical goal *)
Theorem foo: forall i, i <> i -> 2 + 2 = 5.
  intros i C.
  (* explicitly construct a 'False' value *)
  assert False as H.
    apply C. reflexivity.
  (* 'inversion' generates one goal per possible constructor *)
  (* as False has no constructors, this gives 0 subgoals, finishing the proof *)
  inversion H.
Qed.
于 2012-07-09T19:58:51.280 に答える