Как доказать равенство невозможно

Question

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

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

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

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

Answer 1

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