coq induction with passing in equality

Question

I have a list with a known value and want to induct on it, keeping track of what the original list was, and referring to it by element. That is, I need to refer to it by l[i] with varying i instead of just having (a :: l).

I tried to make an induction principle to allow me to do that. Here is a program with all of the unnecessary Theorems replaced with Admitted, using a simplified example. The objective is to prove allLE_countDown using countDown_nth, and have list_nth_rect in a convenient form. (The theorem is easy to prove directly without any of those.)

Require Import Arith.
Require Import List.

Definition countDown1 := fix f a i := match i with
| 0 => nil
| S i0 => (a + i0) :: f a i0
end.

(* countDown from a number to another, excluding greatest. *)
Definition countDown a b := countDown1 b (a - b).

Theorem countDown_nth a b i d (boundi : i < length (countDown a b))
    : nth i (countDown a b) d = a - i - 1.
Admitted.

Definition allLE := fix f l m := match l with
| nil => true
| a :: l0 => if Nat.leb a m then f l0 m else false
end.

Definition drop {A} := fix f (l : list A) n := match n with
| 0 => l
| S a => match l with
  | nil => nil
  | _ :: l2 => f l2 a
  end
end.

Theorem list_nth_rect_aux {A : Type} (P : list A -> list A -> nat -> Type)
    (Pnil : forall l, P l nil (length l))
    (Pcons : forall i s l d (boundi : i < length l), P l s (S i) -> P l ((nth i l d) :: s) i)
    l s i (size : length l = i + length s) (sub : s = drop l i) : P l s i.
Admitted.

Theorem list_nth_rect {A : Type} (P : list A -> list A -> nat -> Type)
    (Pnil : forall l, P l nil (length l))
    (Pcons : forall i s l d (boundi : i < length l), P l s (S i) -> P l ((nth i l d) :: s) i)
    l s (leqs : l = s): P l s 0.
Admitted.

Theorem allLE_countDown a b : allLE (countDown a b) a = true.
  remember (countDown a b) as l.
  refine (list_nth_rect (fun l s _ => l = countDown a b -> allLE s a = true) _ _ l l eq_refl Heql);
    intros; subst; [ apply eq_refl | ].
  rewrite countDown_nth; [ | apply boundi ].
  pose proof (Nat.le_sub_l a (i + 1)).
  rewrite Nat.sub_add_distr in H0.
  apply leb_correct in H0.
  simpl; rewrite H0; clear H0.
  apply (H eq_refl).
Qed.

So, I have list_nth_rect and was able to use it with refine to prove the theorem by referring to the nth element, as desired. However, I had to construct the Proposition P myself. Normally, you'd like to use induction.

This requires distinguishing which elements are the original list l vs. the sublist s that is inducted on. So, I can use remember.

Theorem allLE_countDown a b : allLE (countDown a b) a = true.
  remember (countDown a b) as s.
  remember s as l.
  rewrite Heql.

This puts me at

  a, b : nat
  s, l : list nat
  Heql : l = s
  Heqs : l = countDown a b
  ============================
  allLE s a = true

However, I can't seem to pass the equality as I just did above. When I try

  induction l, s, Heql using list_nth_rect.

I get the error

Error: Abstracting over the terms "l", "s" and "0" leads to a term
fun (l0 : list ?X133@{__:=a; __:=b; __:=s; __:=l; __:=Heql; __:=Heqs})
  (s0 : list ?X133@{__:=a; __:=b; __:=s; __:=l0; __:=Heql; __:=Heqs})
  (_ : nat) =>
(fun (l1 l2 : list nat) (_ : l1 = l2) =>
 l1 = countDown a b -> allLE l2 a = true) l0 s0 Heql
which is ill-typed.
Reason is: Illegal application: 
The term
 "fun (l l0 : list nat) (_ : l = l0) =>
  l = countDown a b -> allLE l0 a = true" of type
 "forall l l0 : list nat, l = l0 -> Prop"
cannot be applied to the terms
 "l0" : "list nat"
 "s0" : "list nat"
 "Heql" : "l = s"
The 3rd term has type "l = s" which should be coercible to 
"l0 = s0".

So, how can I change the induction principle such that it works with the induction tactic? It looks like it's getting confused between the outer variables and the ones inside the function. But, I don't have a way to talk about the inner variables that aren't in scope. It's very strange, since invoking it with refine works without issues. I know for match, there's as clauses, but I can't figure out how to apply that here. Or, is there a way to make list_nth_rect use P l l 0 and still indicate which variables correspond to l and s?

Answer 1

First, you can prove this result much more easily by reusing more basic ones. Here's a version based on definitions of the ssreflect library:

From mathcomp
Require Import ssreflect ssrfun ssrbool ssrnat eqtype seq.

Definition countDown n m := rev (iota m (n - m)).

Lemma allLE_countDown n m : all (fun k => k <= n) (countDown n m).
Proof.
rewrite /countDown all_rev; apply/allP=> k; rewrite mem_iota.
have [mn|/ltnW] := leqP m n.
  by rewrite subnKC //; case/andP => _; apply/leqW.
by rewrite -subn_eq0 => /eqP ->; rewrite addn0 ltnNge andbN.
Qed.

Here, iota n m is the list of m elements that counts starting from n, and all is a generic version of your allLE. Similar functions and results exist in the standard library.

Back to your original question, it is true that sometimes we need to induct on a list while remembering the entire list we started with. I don't know if there is a way to get what you want with the standard induction tactic; I didn't even know that it had a multi-argument variant. When I want to prove P l using this strategy, I usually proceed as follows:

1. Find a predicate Q : nat -> Prop such that Q (length l) implies P l. Typically, Q n will have the form n <= length l -> R (take n l) (drop n l), where R : list A -> list A -> Prop.

2. Prove Q n for all n by induction.