問題タブ [ltac]

Ltac プロシージャの途中で変数の値 (仮説、戦術、用語) を出力する方法はありますか?

次の例を検討してください。

apply H失敗します

したがって、ここで適用するために戦術を使用できることを知っています。または、この他のスタックオーバーフローの質問exists 1+2+3に基づいて、前方推論を使用してそれを実存的な形にするためのより複雑な方法があります。H

しかし、明示的でなくても、統一時に存在変数をインスタンス化できるスマートな戦術があると思いますか?

match goal withユーザー定義のタクティックで( を使用して) パターン マッチングを行う場合、 を使用?xして Gallina タームをバインドし、後で参照できるようにします。このような識別子を 1 つの句で複数... ?x ... ?y ...使用することも ( )、同じ識別子を使用して ( ... ?x ... ?x ...)、句が一致するためには、同じ Gallina 用語がこれら 2 つの位置に出現する必要があることを示すこともできます。ある意味で、これは「同一性」要件との可能な一致を制限します。それは便利ですが、「別の」要件を提示できる方が便利です (sic)。... ?x ... ?y ...用語がバインドされ、区別可能であることを要求する?xフォーム?yのmatch-clause を記述する方法はありますか?

区別可能とは、必ずしも等しくないことを意味するわけではなく、単に異なることを意味します (それらの名前 [または表現] は一致しません)。たとえば、2 つの用語があるとしa,b:Cます。この 2 つの項は、命題 を証明できるという意味では等しいかもしれませんが、a = bそれは私の目的には関係ありません。と をa互いにb区別できるのは、それらの名前が異なることです。

?xでは、2 つのメタ変数と?y異なる用語をバインドする必要があるという要件を課して、パターン マッチを行うことはできますか?

これを何らかの文脈で説明するために、ペア、射影を定義し、R(適切に型付けされた) 二項関係を定義したとします。私の仮定では、どういうわけか次の2つになったとします。

私は自分のタクティックに match のみHでH'. そのためのトリックはありますか？

のみに一致する方法がない場合は、と(または再び)にバインドするH場合、おそらく両方に一致させることができます。しかし、次に、match-clause の右側で、「are-they-different? 」を実行したいと思います。とと doの間をチェックして、2 つが文字通り同じ用語をバインドする場合に備えます。a?xca?yxyidtac