Доказательство (не совсем) неактуальность, когда при разрушении coq равенства - PullRequest
Новая
       51

Доказательство (не совсем) неактуальность, когда при разрушении coq равенства

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

У меня есть зависимый тип, который моделирует конечный путь в переходной системе.Система переходов имеет функцию R, которая выдает предложение о том, существует ли грань между состояниями s и s' с меткой a.Тип конечного пути: 

  Inductive FinPathTail (s : S i) :=
  | FPTNil: FinPathTail s
  | FPTCons (a : Act i) (s' : S i) : R i s a s' ->
                                     FinPathTail s' -> FinPathTail s.

(бит "tail" потому, что он фактически моделирует все, кроме заголовка пути, начинающегося с s).

Я определилтип CoInductive для возможно бесконечного PathTail (я добавлю его внизу, чтобы быстрее добраться до вопроса), и у меня есть функция fpt_to_pt, чтобы преобразовать FinPathTail в PathTail.Это "очевидно" должно быть инъективным, поэтому я хотел доказать лемму этого вида: 

Lemma fpt_to_pt_inj {s : S i} (fpt fpt' : FinPathTail s)
  : (forall s s' : S i, {s = s'} + {s <> s'}) ->
    fpt_to_pt fpt = fpt_to_pt fpt' -> fpt = fpt'.

Пытаясь доказать это индукцией по fpt, я быстро добираюсь до случая, когда обе стороныИзвестно, что conses.В итоге цель выглядит примерно так: 

PTCons s a s' r (fpt_to_pt fpt) = PTCons s a2 s'2 r2 (fpt_to_pt fpt') ->
FPTCons s a s' r fpt = FPTCons s a2 s'2 r2 fpt'

, которую я хотел бы разложить с помощью тактики injection.Результат заканчивается так: 

existT (fun s'0 : S i => PathTail s'0) s' (fpt_to_pt fpt) =
existT (fun s'0 : S i => PathTail s'0) s'2 (fpt_to_pt fpt') ->
s' = s'2 -> a = a2 -> FPTCons s a s' r fpt = FPTCons s a2 s'2 r2 fpt'

и, используя тактику inversion_sigma, я могу преобразовать его в: 

B : s' = s'2
C : a = a2
A0 : s' = s'2
A1 : eq_rect s' (fun a : S i => PathTail a) (fpt_to_pt fpt) s'2 A0 = fpt_to_pt fpt'

Я думаю, я понимаю, почему мне нужна разрешимость для исходного домена,чтобы использовать inj_pair2_eq_dec.Что я не понимаю: что случилось с r и r2?Я понимаю, что у меня нет доказательств несоответствия, но разве это не означает, что они должны быть равны, чтобы совпадения были равны?Или я неправильно понимаю что-то фундаментальное в предложениях?

PS: Вот общее определение PathTail: 

CoInductive PathTail (s : S i) :=
| PTNil: PathTail s
| PTCons (a : Act i) (s' : S i) : R i s a s' -> PathTail s' -> PathTail s.

1 Ответ

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

Очевидно, что тактика injection игнорирует равенства между доказательствами по умолчанию, но вы можете переопределить это поведение с помощью флага Keep Proof Equalities : 

Inductive foo : nat -> Prop :=
| Foo (n : nat) : foo n.

Inductive bar :=
| Bar (n : nat) : foo n -> bar.

Lemma test n nn m mm : Bar n nn = Bar m mm -> False.
Proof.
intros H. injection H. (* No equality generated. *)
Abort.

Set Keep Proof Equalities.

Lemma test n nn m mm : Bar n nn = Bar m mm -> False.
Proof.
intros H. injection H. (* Equality generated. *)
Abort.
...