IndProp: prove that Prop is not provable

Question

The task.

Suppose we give Coq the following definition:

Inductive R2 : nat -> list nat -> Prop :=
| c1 : R2 0 []
| c2 : forall n l, R2 n l -> R2 (S n) (n :: l)
| c3 : forall n l, R2 (S n) l -> R2 n l.

Which of the following propositions are provable?

I proved 2 out of 3.

Example Example_R21 : R2 2 [1;0].
Proof.
  apply c2. apply c2. apply c1.
Qed.

Example Example_R22 : R2 1 [1;2;1;0].
Proof.
  repeat constructor.
Qed.

The 3-rd is not provable, because c3 will only increase n, and it will never be equal to the head of list + 1. But how to formally prove that it is not provable?

Example Example_R23 : not (R2 6 [3;2;1;0]).
Proof.

Qed.

Update 1

Fixpoint gen (n: nat) : list nat :=
  match n with
  | 0 => []
  | S n' => (n' :: gen n')
  end.

Lemma R2_gen : forall (n : nat) (l : list nat), R2 n l -> l = gen n.
Proof.
  intros n l H. induction H.
  - simpl. reflexivity.
  - simpl. rewrite IHR2. reflexivity.
  - simpl in IHR2. ?

Answer 1

You have to proceed by induction on the R2. Basically, if you have R2 6 (3 :: _), then it must be a c3 (no other constructor fits), so it contains an R2 7 (3 :: _), which must also be c3, which contains R2 8 (3 :: _), etc. This chain is infinite, so you'll never reach the end. Therefore, you can use False as the goal of the induction and you will never reach the base case where you actually have to produce False. It is not enough to just use inversion. Inversion is really just one step of the needed induction, and induction on any of the other things in the context doesn't help.

During the induction, the first parameter will vary. Specifically, it will always be more than S 3 (that's what lets us rule out the other constructors), so we need to generalize with respect to k where the first parameter is always 5 + k (starting with k = 1 for our case where we have 6).

Example Example_R23 : not (R2 6 [3;2;1;0]).
Proof.
  set (xs := [2; 1; 0]).
  change 6 with (5 + 1).
  set (x := 3). (* sets are not strictly needed, but help clean things up *)
  generalize 1 as k.
  intros k.
  (* Everything up to here is just generalizing over k *)
  remember (S (S x) + k) as n eqn:prf_n.
  remember (x :: xs) as l eqn:prf_l.
  intros no.
  revert k prf_n prf_l.
  induction no as [ | n' l' _ _ | n' l' _ rec_no]
  ; intros k prf_n prf_l.
  - discriminate.
  - injection prf_l as -> ->.
    discriminate.
  - subst.
    (* Everything up to here is combined inversion and induction *)
    eapply rec_no.
    + apply plus_n_Sm.
    + reflexivity.
Defined.

We can reduce this proof immensely by using the experimental dependent induction tactic, which replaces the middle, inversiony part.

Example Example_R23 : not (R2 6 [3;2;1;0]).
Proof.
  set (xs := [2; 1; 0]).
  change 6 with (5 + 1).
  set (x := 3).
  generalize 1 as k.
  intros k no.
  dependent induction no generalizing k.
  eapply IHno.
  - apply plus_n_Sm.
  - reflexivity.
Defined.

Another form of cleanup would be extracting the generalized proof out into a lemma:

Lemma R2_head x k xs : ~R2 (S (S x) + k) (x :: xs).
Proof.
  intros no.
  dependent induction no generalizing k.
  - clear no IHno. (* Another "infinite chain" contradiction *)
    rename x into prf_x, x0 into x.
    induction x as [ | x rec_x].
    + discriminate.
    + injection prf_x.
      apply rec_x.
  - eapply IHno.
    + apply plus_n_Sm.
    + reflexivity.
Defined.
Example Example_R232 : not (R2 6 [3;2;1;0]) := R2_head 3 _ _.

Answer 2

not A is A -> False. You should introduce the absurd hypothesis and reason by cases on it (see the inversion tactic).

Answer 3

You could write a function to generate the list from the nat parameter (let's call it gen) and prove R2 n l -> l = gen n. From that, you can prove your proposition by showing that l <> gen n.

Answer 4

Here is a simple proof that uses the goal generalization technique.

First, we prove a more general property than we actually are posed with.

From Coq Require Import Lia.

Lemma R2_len n l : R2 n l -> n <= length l.
Proof. induction 1; simpl; lia. Qed.

Now our example is a simple concrete instance of the more general property.

Example Example_R23 : not (R2 6 [3;2;1;0]).
Proof. intros H%R2_len; simpl in H; lia. Qed.

Answer 5

This is equivalent to @HTNW's proof

Lemma R2_head' {a n l}: R2 a (n::l) -> a <= S n.
  intros H; dependent induction H; 
    try pose proof (IHR2 _ _ eq_refl); lia.
Qed.
  
Example Example_R23 : not (R2 6 [3;2;1;0]).
Proof. intros C; pose proof (R2_head' C); lia. Qed.