Уничтожение равенства зависимых записей в coq - PullRequest
Новая
       28

Уничтожение равенства зависимых записей в coq

0 голосов
/ 07 февраля 2019

Учитывая зависимый тип записи: 

Record FinPath : Type := mkPath { fp_head : S i;
                                  fp_tail : FinPathTail fp_head
                                }.

и два равных объекта типа Path, я бы хотел сделать вывод, что их головы и хвосты равны.Проблема в том, что я быстро получаю что-то такого вида: 

fpH : {| path_head := fp_head fp; path_tail := fpt_to_pt (fp_tail fp) |} =
      {| path_head := fp_head fp'; path_tail := fpt_to_pt (fp_tail fp') |}

Используя тактику впрыска, я могу вывести это fp_head fp = fp_head fp', а также этот термин: 

existT (fun path_head : S i => PathTail path_head) (fp_head fp)
       (fpt_to_pt (fp_tail fp)) =
existT (fun path_head : S i => PathTail path_head) (fp_head fp')
       (fpt_to_pt (fp_tail fp'))

Предполагая разрешимостьS i, обычно я хотел бы использовать inj_pair2_eq_dec, но в данном случае это неприменимо, потому что fp_head fp и fp_head fp' не совпадают синтаксически.Я также не могу переписать их так, чтобы они были такими же, потому что перезапись с помощью fp_head fp' = fp_head fp оставила бы правую часть неправильно напечатанной.

Как я могу продолжить отсюда?Есть ли какая-нибудь более умная версия inj_pair2_eq_dec, которая каким-то образом использует (несинтаксическое) базовое равенство, а не требует, чтобы основания сигма-типов были равны?

Редактировать : Думая об этомнемного сложнее, я понимаю, что не имеет смысла спрашивать, что хвосты равны (так как они разных типов).Но можно ли доказать некоторую форму равенства Лейбница между ними на основе eq_rect?

1 Ответ

0 голосов
/ 08 февраля 2019

Подобные проблемы объясняют, почему многие предпочитают избегать зависимых типов в Coq.Я отвечу на ваш вопрос в случае сигма-типа Coq {x : T & S x}, который можно обобщить для других зависимых записей.

Мы можем выразить равенство, которому зависимый компонент пары должен удовлетворять, через приведениефункция: 

Definition cast {T} (S : T -> Type) {a b : T} (p : a = b) : S a -> S b :=
  match p with eq_refl => fun a => a end.

Definition eq_sig T (S : T -> Type) (a b : T) x y
  (p : existT S a x = existT S b y) :
  {q : a = b & cast S q x = y} :=
  match p in _ = z return {q : a = projT1 z & cast S q x = projT2 z} with
  | eq_refl => existT _ eq_refl eq_refl
  end.

Функция cast позволяет использовать равенство p : a = b для приведения от S a к S b.Лемма eq_sig, которую я определил с помощью проверочного термина, говорит, что при равенстве p между двумя зависимыми парами existT S a x и existT S b y я могу создать другую зависимую пару, содержащую:

  1. Равенство q : a = b и

  2. доказательство того, что x и y равны после приведения .

С аналогичным определением мы можем предоставить принцип доказательства "индукции" при доказательстве равенства между зависимыми парами: 

Definition eq_sig_elim T (S : T -> Type) (a b : T) x y
  (p : existT S a x = existT S b y) :
  forall (R : forall c, S c -> Prop), R a x -> R b y :=
  match p in _ = z return forall (R : forall c, S c -> Prop), R a x -> R _ (projT2 z) with
  | eq_refl => fun R H => H
  end.

Форма леммы аналогичнаeq_sig, но на этот раз он говорит, что при наличии такого равенства мы можем доказать произвольный зависимый предикат R b y, предоставив доказательство R a x.

Используя такоезависимые принципы могут быть неудобными.Задача состоит в том, чтобы найти такой R, который позволит вам выразить вашу цель: в приведенном выше типе результата тип второго аргумента R является параметрическим по отношению к первому аргументу.Во многих случаях, представляющих интерес, первый компонент второго члена, y, не является переменной, но имеет особую форму, которая может помешать прямому обобщению.

...