Coq：文字列に関連するステートメントを証明する方法は？

Question

私はstring aを持っていて、string bと比較して、等価がstring cの場合はstring xです。私は、仮説ではfun x <= fun cだと知っています。これを証明するにはどうしたらいいですか？ funは、stringを取り込み、natを返す関数です。

fun (if a == b then c else x) <= S (fun c) 

ロジックは明らかですが、私はcoqのif文を分割できません。どんな助けもありがとう。

ありがとうございます！

Answer 1

if-then-else文を書くことができる場合は、テスト式a == bが2つのコンストラクタ（たとえばbool）または（sumbool）を持つ型にあることを意味します。まず、タイプがboolと仮定します。その場合、証明の最善の方法は次のコマンドを入力することです。

case_eq (a == b); intros hyp_ab. 

これは2つの目標を生成します。最初のものでは、テストが成功し、目標の結論は次のような形状を（されたif-then-elseがその後、ブランチで置き換えられる）があることを主張する仮説

hyp_ab : a == b = true 

を持っています。

楽しい< C =のS（楽しいc）の第二の目標で

、あなたは仮説

hyp_ab : a == b = false 

を持っています

となり、目的の結論は次のような形になります（if-then-elseはelseブランチに置き換えられます）。

fun x <= S (fun c) 

あなたはそこから移動することができます。

一方、CoqからのStringライブラリは、戻り値タイプ{a = b}+{a <> b}を持つ関数string_decを持っています。動作は、使用するだけで簡単に、私は上記のものにかなり近くなる

destruct (a == b) as [hyp_ab | hyp_ab]. 

：あなたの表記a == bがstring_dec a bのためにかなりの表記がある場合は、次のような戦術を使用することをお勧めします。直感的に

、されたif-then-else文のあなたの理由は、あなたが個別に2つの実行パスを勉強にあなたを導きcase_eq、destruct、またはcaseのようなコマンドを使用し、あなたがそれぞれを取った理由を仮説に覚えていますこれらの実行パスのうちの1つです。

Answer 2

多くの状況でうまく機能する一般的な「ビュー」パターンを指摘しているイヴェスの答えは、ケース分析が必要であった。私はmath-compでビルトインサポートを使用しますが、そのテクニックはそれに特有のものではありません。あなたが次のステップに到着するcase_eq + simplを使用することができ、今

From mathcomp Require Import all_ssreflect. 

Variables (T : eqType) (a b : T). 
Lemma u : (if a == b then 0 else 1) = 2. 
Proof. 

;：

のは、あなたの最初の目標を想定してみましょうただし、より特殊化された「表示」補助儀を使用して照合することもできます。 if_specがどこにある

ifP : forall (A : Type) (b : bool) (vT vF : A), 
     if_spec b vT vF (b = false) b (if b then vT else vF) 

：たとえば、あなたがifPを使用することができ

Inductive if_spec (A : Type) (b : bool) (vT vF : A) (not_b : Prop) : bool -> A -> Set := 
    IfSpecTrue : b -> if_spec b vT vF not_b true vT 
    | IfSpecFalse : not_b -> if_spec b vT vF not_b false vF 

少し混乱見えること、重要なビットは、タイプファミリーbool -> A -> Setのパラメータです。最初の練習問題は "ifP補題を証明する"です。私達は私達の証明でifPを使用する場合

実際、我々が得る：私たちは何も指定する必要はありませんでした

case: ifP. 
Goal 1: (a == b) = true -> 0 = 2 
Goal 2: (a == b) = false -> 1 = 2 

注意！実際、形式{ A } + { B }の補題は、このビューパターンの特殊なケースに過ぎません。このトリックは他の多くの状況で機能します。例えば、ブール値の等価性と命題1を関連付ける仕様を持つeqPも使用できます。そうした場合：

case: eqP. 

を、あなたが取得します：

Goal 1: a = b -> 0 = 2 
Goal 2: a <> b -> 1 = 2 

非常に便利です。実際、eqPは基本的にtype_dec原則の一般的なバージョンです。