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

问题描述

我有一个依赖类型，它模拟过渡系统中的有限路径。转换系统有一个函数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.

（“尾部”位是因为这实际上模拟了从开始的路径的头部s除外）。

我已经为可能无限的 PathTail 定义了一个 CoInductive 类型（我会将它贴在底部以便更快地解决问题），并且我有一个函数，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 发生了什么？我知道我没有证据无关紧要，但这是否意味着它们必须相等才能使 conses 相等？还是我误解了命题的基本原理？

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.

标签： coqdependent-type

显然，默认情况下该策略会忽略证明之间的相等性，但您可以使用以下标志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.

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

问题描述

解决方案

推荐阅读