How to express that one element of an inductive relation can't be derived from another in Coq?

Question

This is slightly different from simple implication, as shown in this toy example.

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).

Given this definition, we have three provable statements: R 2 3, R 3 5, and (R 2 3) -> (R 3 5). What I'm looking for is some way to formulate the following: "there does not exist a derivation path (i.e. a sequence of inductive constructor applications) that starts at R 2 3 and ends at R 3 5.

Is there a way to do this in Coq?

Answer 1

Here is a suggestion for how you can define a derivation path. I don't know that this is the best way, but it's what I came up with.

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.

You can probably simplify this proof, and avoid lia if you want.