Coq: выполнение инверсии на Prop для Set, когда есть только один случай - PullRequest
Новая
       74

Coq: выполнение инверсии на Prop для Set, когда есть только один случай

0 голосов
/ 27 августа 2018

Предположим, у меня есть некоторый язык программирования с отношением "имеет тип" и отношением "маленький шаг". 

Inductive type : Set :=
| Nat : type
| Bool : type.

Inductive tm : Set :=
| num : nat -> tm
| plus : tm -> tm -> tm
| lt : tm -> tm -> tm
| ifthen : tm -> tm -> tm -> tm.

Inductive hasType : tm -> type -> Prop :=
| hasTypeNum :
    forall n, hasType (num n) Nat
| hasTypePlus:
    forall tm1 tm2,
      hasType tm1 Nat ->
      hasType tm2 Nat ->
      hasType (plus tm1 tm2) Nat
| hasTypeLt:
    forall tm1 tm2,
      hasType tm1 Nat ->
      hasType tm2 Nat ->
      hasType (lt tm1 tm2) Bool
| hasTypeIfThen:
    forall tm1 tm2 tm3,
      hasType tm1 Bool ->
      hasType tm2 Nat ->
      hasType tm3 Nat ->
      hasType (ifthen tm1 tm2 tm3) Nat.

Inductive SmallStep : tm -> tm -> Prop :=
  ...

Definition is_value (t : tm) := ...

Ключевая деталь здесь заключается в том, что для каждого варианта термина есть только один возможный вариант HasType, который мог бы соответствовать.

Предположим, что я хочу доказать лемму о прогрессе, но я также хочу иметь возможность извлечь из этого интерпретатора. 

Lemma progress_interp: 
  forall tm t, 
  hasType tm t -> 
  (is_value tm = false) -> 
  {tm2 | SmallStep tm tm2}.
intro; induction tm0; intros; inversion H.

Это дает ошибку Inversion would require case analysis on sort Set which is not allowed for inductive definition hasType.

Я понимаю, почему это происходит: inversion выполняет анализ регистра для значения вида Prop, что мы не можем сделать, поскольку оно стирается в извлеченном коде.

Но, поскольку существует взаимно-однозначное соответствие между вариантами терминов и правилами деривации типов, нам фактически не нужно выполнять какой-либо анализ во время выполнения.

В идеале, я мог бы применить несколько лемм, которые выглядят так: 

plusInv: forall e t, hasType e t ->
  (forall e1 e2, e = plus e1 e2 -> hasType e1 Nat /\ hasType e2 Nat ).

где будет лемма, подобная этой, для каждого случая (или отдельная лемма, которая является соединением этих случаев).

Я посмотрел на Derive Inversion, но, похоже, он не выполняет то, что я ищу здесь, хотя, возможно, я не правильно понимаю.

Есть ли способ сделать такой "анализ случая, когда есть только один случай?" Или чтобы получить равенства, подразумеваемые доказательством Prop, чтобы я мог записать только возможные случаи в моем извлеченном интерпретаторе? Может ли вывод этих лемм быть автоматизирован с помощью Ltac или механизма получения?

Ответы [ 2 ]

0 голосов
/ 28 августа 2018

Лемма plus_inv может быть получена путем анализа случая для типа tm вместо анализа случая для типа hasType. 

Lemma plus_inv : forall e t, hasType e t ->
  (forall e1 e2, e = plus e1 e2 -> hasType e1 Nat /\ hasType e2 Nat ).
Proof.
intros e; case e; try (intros; discriminate).
intros e1 e2 t h; inversion h; intros e5 e6 heq; inversion heq; subst; auto.
Qed.

Доказательство вашей главной цели progress_interp, вероятно, может быть выполнено по индукции также структура tm. Это равносильно написанию вашего интерпретатора напрямую как рекурсивная функция галлины.

У вашего вопроса есть вторая часть: это можно автоматизировать. Ответ да, наверное. Я предлагаю использовать для этого либо пакет template-coq , либо пакет elpi . Оба пакета доступны как пакеты opam.

0 голосов
/ 27 августа 2018

Я думаю, eexists справится: экзистенциальная переменная должна быть заполнена в какой-то момент во время доказательства в сигма-типе (где вы можете свободно использовать inversion в гипотезе hasType).

...