Переписать совпадение с одной ветвью, которая не зависит от сопоставленного значения - PullRequest
Новая
       4

Переписать совпадение с одной ветвью, которая не зависит от сопоставленного значения

1 голос
/ 14 января 2020

Я хочу показать следующее: 

match H in (_ = y) return y with
  | eq_refl => exist (fun n' : nat => n' < n) x0 l
  end = exist (fun n' : nat => n' < n) x0 l

В моем контексте: 

H : ltn n = ltn n
n : nat
x0 : nat
l : x0 < n

Где 

Definition ltn (n : nat) : Type := {n' | n' < n}.

Я не могу уничтожить на H, потому что результирующий термин был бы неправильно напечатан, но кажется очевидным, что равенство имеет место, потому что единственно возможная ветвь из соответствия не зависит от того, что сопоставляется.

1 Ответ

1 голос
/ 26 января 2020

Проблема (как вы сказали) в том, что Coq не может уничтожить H, поскольку это переменная без «соответствий» и определение равенства (которое вы используете) основано на нормализации и проверке строк, вы не сможете управлять этим , В любом случае, без аксиом вы не можете уничтожить экземпляр равенства, учитывая, что вы подразумеваете, что все равенства равны (дефиниционные определения). Смысл рассмотрения всех равенств как «равных» предполагает, что ваше ядро ​​ имеет расширенную типизацию . Для совместимости с другими теориями типов (такими как теория гомотопических типов) Coq не позволяет вам упоминать UIP без аксиомы. Аксиома UIP и аксиома К очень связаны. Вы можете просто экспортировать аксиомы из стандартной библиотеки Coq . 

Theorem exact_eq : forall (n' n x0 : nat) (l : x0 < n) (H : {n' | n' < n} = {n' | n' < n}),
 match H in (_ = y) return y with
  | eq_refl => exist (fun n' : nat => n' < n) x0 l
  end = exist (fun n' : nat => n' < n) x0 l.

intros.
(*UIP_refl : forall (H : x = x), H = erefl x*) 
by set(@UIP_refl _ _ H); subst.
Qed.
...