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?
The issue is that, for better or for worse, induction seems to assume that its arguments are independent. The solution, then, is to let induction automatically infer l and s from Heql:
Theorem list_nth_rect {A : Type} {l s : list A} (P : list A -> list A -> nat -> Type)
(Pnil : P l nil (length l))
(Pcons : forall i s d (boundi : i < length l), P l s (S i) -> P l ((nth i l d) :: s) i)
(leqs : l = s): P l s 0.
Admitted.
Theorem allLE_countDown a b : allLE (countDown a b) a = true.
remember (countDown a b) as s.
remember s as l.
rewrite Heql.
induction Heql using list_nth_rect;
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 H.
apply leb_correct in H.
simpl; rewrite H; clear H.
assumption.
Qed.
I had to change around the type of list_nth_rect a bit; I hope I haven't made it false.