Сильная индукция в списках

Question

Я пытаюсь доказать, что предложение P выполняется для каждого элемента типа A, К сожалению, я знаю только как доказать P для данного a:A если у меня есть доступ к доказательствам P для всех a' меньше, чем a,

Это должно быть доказано введением в список, содержащий все элементы Aначиная с самого маленького элемента в A а затем постепенно доказывая, что P относится ко всем другим элементам, но я просто не могу заставить его работать.

Формально проблема заключается в следующем:

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.

Возможно, я допустил ошибку, формализовав эту проблему. Не стесняйтесь принимать разумные ограничения на входы, например A можно считать перечисляемым, lt может быть переходным, разрешимым...

Answer 1

Вы также должны доказать, что отношения являются обоснованными. Там есть соответствующий стандартный модуль библиотеки. Оттуда вы должны доказать well_founded A для тебя A типа, а затем вы можете использовать well_founded_ind чтобы доказать P для всех значений.

Answer 2

Это выглядит как обоснованная индукция. Если вы можете доказать, что ваш lt функция обоснована, тогда ваша цель становится тривиальной. Вы можете найти пример таких доказательств на натуральных здесь