I have been having some problems with dependent induction because a "weak hypothesis".
For example :
I have a dependent complete foldable list :
Inductive list (A : Type) (f : A -> A -> A) : A -> Type :=
|Acons : forall {x x'' : A} (y' : A) (cons' : list f (f x x'')), list f (f (f x x'') y')
|Anil : forall (x: A) (y : A), list f (f x y).
And a function that a return the applied fold value from inductive type list and other function that forces a computation of these values through a matching.
Definition v'_list {X} {f : X -> X -> X} {y : X} (A : list f y) := y.
Fixpoint fold {A : Type} {Y : A} (z : A -> A -> A) (d' : list z Y) :=
match d' return A with
|Acons x y => z x (@fold _ _ z y)
|Anil _ x y => z x y
end.
Clearly, that's function return the same value if have the same dependent typed list and prove this don't should be so hard.
Theorem listFold_eq : forall {A : Type} {Y : A} (z : A -> A -> A) (d' : list z Y), fold d' = v'_list d'.
intros.
generalize dependent Y.
dependent induction d'.
(.. so ..)
Qed.
My problem is that dependent definition generates for me a weak hypothesis.
Because i have something like that in the most proof that i use dependent definitions, the problem of proof above:
A : Type
z : A -> A -> A
x, x'', y' : A
d' : list z (z x x'')
IHd' : fold d' = v'_list d'
______________________________________(1/2)
fold (Acons y' d') = v'_list (Acons y' d')
Even i have a polymorphic definition in (z x x'') i can't apply IHd' in my goal.
My question if have a way of define more "powerful" and polymorphic induction, instead of working crazy rewriting terms that sometimes struggling me.
If you do
simpl.
unfold v'_list.
You can see that you're almost there (you can finish with rewriting), but the arguments of z are in the wrong order, because list and fold don't agree on the way the fold should go.
On an unrelated note, Acons could quantify over a single x, replacing f x x'' with just x.