Блог

 1 subgoal
a, b : Tipe
H : TApp a b = a
______________________________________(1/1)
False
  

(где TApp — конструктор)

В Idris это может быть доказано с помощью Refl => impossible , но мне не удалось написать какое-либо доказательство для этого в Coq.

Есть ли простой способ доказать это?

Вы можете доказать это с помощью induction a. . Идея заключается в том, что принцип индукции для Tipe кодирует тот факт, что его значения имеют конечный размер, в то время как TApp a b = a предположение позволяет вам построить бесконечное значение, но это несколько косвенные следствия из имеющихся у вас необработанных фактов, следовательно, вам нужно немного поработать над этим. Расширение Coq для вывода и использования таких лемм происходит-проверка автоматически, безусловно, была бы возможна.