在破坏 coq 相等性时证明（不完全）无关紧要

Question

我有一个从属类型，它模拟过渡系统中的有限路径。转换系统有一个函数 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 开始的路径的头部之外的所有内容）。

我已经为可能无限的 PathTail 定义了 CoInductive 类型（我将它放在底部以便更快地解决问题）并且我有一个函数 fpt_to_pt 来转换FinPathTail 变成了 PathTail。这应该 "obviously" 是单射的，所以我想证明这种形式的引理：

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 的归纳法来证明这一点时，我很快就遇到了双方都已知的情况。目标最终看起来像：

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 发生了什么？我知道我没有证据无关紧要，但这是否意味着它们必须相等才能使 cons 相等？还是我误解了命题的一些基本内容？

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.

Answer 1

显然 injection 策略默认忽略证明之间的相等性，但您可以使用 Keep Proof Equalities flag:

覆盖此行为

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.

在破坏 coq 相等性时证明（不完全）无关紧要

Proof (not-quite) irrelevance when when destructing coq equality

coq

dependent-type