0

Coqで次のことを行う方法を見つけようとしています。次のことが証明されたとします。

trans_lemma: a = b -> b = c -> a = c

それを使ってそれを推測したい

b = a -> c = b -> a = c.

「trans_lemma を ... で適用」して、何をしてもうまくいかないようです。変数が同じ順序で一致するように、trans_lemma の方程式を書き直す必要があるようです。レンマを再証明せずにこれを行う簡単な方法はありますか?つまり、式内の方程式に「対称性」戦術を何らかの方法で適用できますか?

（いくつかのイントロと書き直しを使用するだけで、補題を使用せずに必要なものを証明できることはわかっていますが、すでに持っている結果を再利用する構文上の方法があるかどうかを知りたいです。）

4

1 に答える 1

2

補題に魔法のように形を変えるものを適用することはできません。ここでできることは、平等を導入b = aしc =b、次に補題を適用して、の対称性によって簡単に証明できる2つの目標を残すことです=。

一般的に、あなたが望む方法で用語に戦術を適用することはできないと思います。

ここで、いくつかの追加事項があります。

  • ここがCoqの平等である場合=、推移性はシステムによって与えられるため、実際には補題は必要ありません。

  • あなたの補題は多形でなければなりません：trans_lemma : forall {T} (a b c : T), a = b -> b = c -> c = d。たぶん、あなたはセクションにいるのでこれを見せてくれますが、セクションを閉じたら、おそらくその2番目の目標を推測する必要があります。

Transitive（あなたはまた、からの型クラスを再利用することに興味があるかもしれませんCoq.Classes.RelationClasses...）

于 2012-12-27T23:21:57.500 に答える