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

user_1995587 0
Viewed 75

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?

induction coq
1 Answers

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.

user_23054580
Related