I'm trying to prove that a proposition P holds for every element of a type A. Unfortunately, I only know how to prove P for a given a:A if I have access to proofs of P for all a' less than a.
This should be provable by induction on a list containing all elements of A, starting with the smallest element in A and then incrementally proving that P holds for all other elements, but I just can't get it to work.
Formally, the problem is the following:
Parameter A : Type.
Parameter lt : A -> A -> Prop.
Notation "a < b" := (lt a b).
Parameter P : A -> Prop.
Parameter lma : forall a, (forall a', a' < a -> P a') -> P a.
Goal forall a, P a.
I may have made a mistake formalizing this problem. Feel free to assume reasonable constraints on the inputs, e.g. A can be assumed to be enumerable, lt can be transitive, decidable ...
You also have to prove that the relation is well-founded. There's a relevant standard library module. From there, you should prove well_founded A for your A type, and then you can use well_founded_ind to prove P for all values.