У меня возникли некоторые проблемы с зависимой индукцией из-за «слабой гипотезы».
Например:
У меня есть полный список зависимых складок:
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).
И функция, которая возвращает примененное значение сгиба из списка индуктивных типов и другую функцию, которая вызывает вычисление этих значений посредством сопоставления.
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.
Очевидно, что эта функция возвращает то же значение, если имеет то же самоезависимый типизированный список и доказать, что это не должно быть так сложно.
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.
Моя проблема в том, что зависимое определение порождает для меня слабую гипотезу.
Потому что у меня есть что-то подобное вБольшинство доказательств того, что я использую зависимые определения, проблема доказательства выше:
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')
Даже если у меня есть полиморфное определение в (zx x ''), я не могу применить IHd 'в своей цели.
Мой вопрос, если у меня есть способ определить более «мощную» и полиморфную индукцию, вместо того, чтобы работать с сумасшедшими терминами переписывания, которые иногда мне мешают.