coq - 在 Coq 中如何表达归纳关系的一个元素不能从另一个元素推导出来？

Question

这与简单暗示略有不同，如这个玩具示例所示。

Inductive R : nat -> nat -> Prop :=
  | Base1: R 0 1
  | Base2: R 0 2
  | Ind: forall n m,
    R n m -> R (n+1) (m+1).

根据这个定义，我们有三个可证明的陈述:R 2 3、R 3 5 和 (R 2 3) -> (R 3 5 )。我正在寻找的是某种表达以下内容的方法:“不存在从 R 2 3 开始并在 结束的推导路径(即一系列归纳构造函数应用程序) R 3 5。

有没有办法在 Coq 中做到这一点？

Answer 1

这里是关于如何定义派生路径的建议。我不知道这是最好的方法，但这是我想到的。

Require Import List Lia.
Import ListNotations.

Inductive evidence :=
  | B1 : evidence
  | B2 : evidence
  | Step : nat -> nat -> evidence.

Inductive R : nat -> nat -> list evidence -> Prop :=
  | Base1 : R 0 1 [B1]
  | Base2 : R 0 2 [B2]
  | Ind : forall n m es, R n m es -> R (n+1) (m+1) (Step n m :: es).


Lemma R_B2 (n : nat) (es : list evidence) : R n (n + 2) es -> In B2 es.
Proof.
  generalize dependent n.
  induction es as [|e es' IHes'].
  - now intros Rnn2nil; inversion Rnn2nil.
  - intros n Rnn2.
    case es' as [| e' es''].
    + inversion Rnn2.
      * now left.
      * now inversion H2.
    + inversion Rnn2.
      right.
      apply (IHes' n0).
      now replace (n0 + 2) with m by lia.
Qed.

您可能可以简化此证明，并根据需要避免使用 lia。