Abstracting patterns in induction rule for inductive predicates for Coq

Link:: https://stackoverflow.com/q/60027551

Display all goals and responses

Question

Consider the following proposition in Coq:

Require Import List.
Import ListNotations.

Inductive subseq : list nat -> list nat -> Prop :=
 | nil_s : forall (l: list nat), subseq nil l
 | cons_in l1 l2 x (H: subseq l1 l2) : subseq (x :: l1) (x :: l2)
 | cons_nin l1 l2 x (H: subseq l1 l2) : subseq l1 (x :: l2).

Lemma subseq_remove_rewritten: forall (x: nat) (l1' l1 l2 : list nat),
    subseq l1' l2 -> l1' = (x :: l1) -> subseq l1 l2.forall (x : nat) (l1' l1 l2 : list nat),
subseq l1' l2 -> l1' = x :: l1 -> subseq l1 l2
Proof.forall (x : nat) (l1' l1 l2 : list nat),
subseq l1' l2 -> l1' = x :: l1 -> subseq l1 l2
  intros x l1' l1 l2 H1 H2.x: nat
l1', l1, l2: list nat
H1: subseq l1' l2
H2: l1' = x :: l1
subseq l1 l2 induction H1.x: nat
l1, l: list nat
H2: [] = x :: l1
subseq l1 l
x: nat
l1, l0, l2: list nat
x0: nat
H1: subseq l0 l2
H2: x0 :: l0 = x :: l1
IHsubseq: l0 = x :: l1 -> subseq l1 l2
subseq l1 (x0 :: l2)
x: nat
l1, l0, l2: list nat
x0: nat
H1: subseq l0 l2
H2: l0 = x :: l1
IHsubseq: l0 = x :: l1 -> subseq l1 l2
subseq l1 (x0 :: l2)
  -x: nat
l1, l: list nat
H2: [] = x :: l1
subseq l1 l discriminate.
  -x: nat
l1, l0, l2: list nat
x0: nat
H1: subseq l0 l2
H2: x0 :: l0 = x :: l1
IHsubseq: l0 = x :: l1 -> subseq l1 l2
subseq l1 (x0 :: l2) injection H2 as H3 H4.x: nat
l1, l0, l2: list nat
x0: nat
H1: subseq l0 l2
H3: x0 = x
H4: l0 = l1
IHsubseq: l0 = x :: l1 -> subseq l1 l2
subseq l1 (x0 :: l2) rewrite H4 in H1.x: nat
l1, l0, l2: list nat
x0: nat
H1: subseq l1 l2
H3: x0 = x
H4: l0 = l1
IHsubseq: l0 = x :: l1 -> subseq l1 l2
subseq l1 (x0 :: l2) apply cons_nin.x: nat
l1, l0, l2: list nat
x0: nat
H1: subseq l1 l2
H3: x0 = x
H4: l0 = l1
IHsubseq: l0 = x :: l1 -> subseq l1 l2
subseq l1 l2 apply H1.
  -x: nat
l1, l0, l2: list nat
x0: nat
H1: subseq l0 l2
H2: l0 = x :: l1
IHsubseq: l0 = x :: l1 -> subseq l1 l2
subseq l1 (x0 :: l2) apply IHsubseq in H2.x: nat
l1, l0, l2: list nat
x0: nat
H1: subseq l0 l2
H2: subseq l1 l2
IHsubseq: l0 = x :: l1 -> subseq l1 l2
subseq l1 (x0 :: l2) apply cons_nin.x: nat
l1, l0, l2: list nat
x0: nat
H1: subseq l0 l2
H2: subseq l1 l2
IHsubseq: l0 = x :: l1 -> subseq l1 l2
subseq l1 l2 apply H2.
Qed.

Lemma subseq_remove: forall (x: nat) (l1 l2 : list nat),
  subseq (x :: l1) l2 -> subseq l1 l2.forall (x : nat) (l1 l2 : list nat),
subseq (x :: l1) l2 -> subseq l1 l2
Proof.forall (x : nat) (l1 l2 : list nat),
subseq (x :: l1) l2 -> subseq l1 l2
  intros x l1 l2 H.x: nat
l1, l2: list nat
H: subseq (x :: l1) l2
subseq l1 l2
  apply subseq_remove_rewritten with (x:=x) (l1':=x :: l1).x: nat
l1, l2: list nat
H: subseq (x :: l1) l2
subseq (x :: l1) l2
x: nat
l1, l2: list nat
H: subseq (x :: l1) l2
x :: l1 = x :: l1
  -x: nat
l1, l2: list nat
H: subseq (x :: l1) l2
subseq (x :: l1) l2 apply H.
  -x: nat
l1, l2: list nat
H: subseq (x :: l1) l2
x :: l1 = x :: l1 reflexivity.
Qed.

I worked in Isabelle before Coq. There originally, the induction tactic could not solve directly this goal and the trick was to come up with a lemma like subseq_remove_rewritten and then prove the original goal. This is the situation in the manual Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Later, the tactic became smarter and one can write patterns in which to abstract on. So the proof is written like this:

lemma
  assumes "subseq (x # l1) l2"
  shows "subseq l1 l2"
  using assms
  apply(induction "x # l1" "l2" rule: subseq.induct)
    apply simp
   apply(intro subseq.intros(3),simp)
  by (intro subseq.intros(3))

I was wondering if Coq has a similar way to avoid proving a lemma like subseq_remove_rewritten and go directly to prove subseq_remove.

Answer

You can use the dependent induction tactic (documented here). For example:

Require Import Coq.Lists.List.
Import ListNotations.
Require Import Coq.Program.Equality. (* Needed to use the tactic *)

Inductive subseq : list nat -> list nat -> Prop :=
| nil_s : forall (l: list nat), subseq nil l
| cons_in l1 l2 x (H: subseq l1 l2) : subseq (x :: l1) (x :: l2)
| cons_nin l1 l2 x (H: subseq l1 l2) : subseq l1 (x :: l2).

Lemma subseq_remove: forall (x: nat) (l1 l2 : list nat),
  subseq (x :: l1) l2 -> subseq l1 l2.forall (x : nat) (l1 l2 : list nat),
subseq (x :: l1) l2 -> subseq l1 l2
Proof.forall (x : nat) (l1 l2 : list nat),
subseq (x :: l1) l2 -> subseq l1 l2
  intros x l1 l2 H.x: nat
l1, l2: list nat
H: subseq (x :: l1) l2
subseq l1 l2 dependent induction H generalizing x.l1, l2: list nat
x: nat
H: subseq l1 l2
IHsubseq: forall x : nat,
l1 = x :: l1 -> subseq l1 l2
subseq l1 (x :: l2)
l1: list nat
x: nat
l2: list nat
x0: nat
H: subseq (x :: l1) l2
IHsubseq: forall x0 : nat,
x :: l1 = x0 :: l1 -> subseq l1 l2
subseq l1 (x0 :: l2)
  -l1, l2: list nat
x: nat
H: subseq l1 l2
IHsubseq: forall x : nat,
l1 = x :: l1 -> subseq l1 l2
subseq l1 (x :: l2) now apply cons_nin.
  -l1: list nat
x: nat
l2: list nat
x0: nat
H: subseq (x :: l1) l2
IHsubseq: forall x0 : nat,
x :: l1 = x0 :: l1 -> subseq l1 l2
subseq l1 (x0 :: l2) eauto using cons_nin.
Qed.

Unfortunately, though this tactic has been around for a while, it is still described as experimental in the reference manual, and I don't know if the Coq developers have any plans of improving it in the future. It has a few deficiencies, such as not allowing the user to name the variables and hypotheses used in the induction proof. I personally prefer to add the equality assumptions to the proof myself, as in your first attempt, or to reformulate the definition of subseq as a Fixpoint, so that you can invert the hypothesis by simplification. For example:

Require Import Coq.Lists.List.
Import ListNotations.

Fixpoint subseq (l1 l2 : list nat) : Prop :=
  match l1, l2 with
  | [], _ => True
  | x1 :: l1, [] => False
  | x1 :: l1, x2 :: l2 => x1 = x2 /\ subseq l1 l2 \/ subseq (x1 :: l1) l2
  end.

Lemma subseq_nin x2 l1 l2 : subseq l1 l2 -> subseq l1 (x2 :: l2).x2: nat
l1, l2: list nat
subseq l1 l2 -> subseq l1 (x2 :: l2)
Proof.x2: nat
l1, l2: list nat
subseq l1 l2 -> subseq l1 (x2 :: l2) destruct l1 as [|x1 l1]; simpl; eauto. Qed.

Lemma subseq_remove : forall (x : nat) (l1 l2 : list nat),
  subseq (x :: l1) l2 -> subseq l1 l2.forall (x : nat) (l1 l2 : list nat),
subseq (x :: l1) l2 -> subseq l1 l2
Proof.forall (x : nat) (l1 l2 : list nat),
subseq (x :: l1) l2 -> subseq l1 l2
  intros x l1 l2 H.x: nat
l1, l2: list nat
H: subseq (x :: l1) l2
subseq l1 l2
  induction l2 as [|x2 l2 IH]; try easy.x: nat
l1: list nat
x2: nat
l2: list nat
H: subseq (x :: l1) (x2 :: l2)
IH: subseq (x :: l1) l2 -> subseq l1 l2
subseq l1 (x2 :: l2)
  destruct H as [[<- H]|H]; eauto using subseq_nin.
Qed.