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つになったとします。
H : R (proj1 (pair a b)) c
H' : R (proj1 (pair a b)) a
私は自分のタクティックに match のみHでH'. そのためのトリックはありますか？
のみに一致する方法がない場合は、と(または再び)にバインドするH場合、おそらく両方に一致させることができます。しかし、次に、match-clause の右側で、「are-they-different? 」を実行したいと思います。とと doの間をチェックして、2 つが文字通り同じ用語をバインドする場合に備えます。a?xca?yxyidtac