I have an induction scheme for a vector holding a leb value (x <= y),
Definition vector_ind_with_leb : forall (A : Type) (P : forall n y: nat, y <= n -> vector A n -> Prop),
(forall (n : nat) (y : nat) (H : S y <= S n) (a : A) (v : vector A n),
P n y (le_S_n _ _ H) v -> P (S n) (S y) H (insert a v)) ->
(forall (n : nat) (H : 0 <= S n) (a : A) (v : vector A n),
P (S n) 0 H (insert a v)) ->
(forall (y : nat) (H : 0 <= 0), P 0 0 H (empty A)) -> forall (n : nat) (y : nat) (Heq : y <= n) (v : vector A n), P n y Heq v.
have : forall n, 0 <= S n -> 0 <= n.
auto with arith.
move => P' A P H K K'.
refine ( fix Ffix (x : nat) (y : nat) (Heq : y <= x) (x0 : vector _ x) {struct x0} :
P x y Heq x0 := _).
destruct x0.
destruct y.
refine (K n Heq a _).
refine (H n _ Heq a _ (Ffix _ y _ x0)).
have : forall y, y <= 0 -> y = 0.
auto with arith.
move => F'.
set only_0 := F' _ Heq.
destruct y.
refine (K' 0 Heq).
inversion Heq.
Show Proof.
Defined.
I have to prove something like that:
Theorem update_vector_correctly : forall {A} n y (x : vector A (S n)) (H : S n >= S y) v, get_value (set_value x (S y) v) (S y) = Some v.
So I got three cases.
when (for y and n),
S y <= S n.
0 <= S n.
0 <= 0.
However if you notice the case 3, for example is an absurd, once 0 <> S n, for all n, so I have to remember that (S n) is a succ number.
When I use this : remember (S n).
I get :
H : 0 <= 0
Heqn0 : 0 = S n
But in the first case I get :
H0 : n1 = S n -> get_value (set_value v0 y0 v) y0 = Some v
Heqn0 : S n1 = S n
which is neither a false case or true case.
The problem is that my hypothesis is n, but I have to return a P (S n) _ _ (next _ _), therefore an equality relation doesn't walk "together" the induction, in the end remember always get a weird problem.
The solution is to generalize dependent n between the remember and the induction. The problem that you are running into is as follows:
You have that n1 = S n for a given n, and you want to induct over n1 (actually over the vector, but that doesn't matter for our purposes). Coq first generalizes your goal over everything that depends on n1 (including the proof that n1 = S n). But this is the wrong induction hypothesis; you are not trying to prove your statement by induction only when n1 is the successor of this particular n. Instead you want to prove your statement when n1 is the successor of any n, and hence you must generalize over n before performing induction.
As an alternative, in this case, you could first prove that S n <> 0, and then you don't need to remember anything, as your third case will already have an absurd hypothesis.