У меня есть отношение, которое не является обоснованным, и называем его r1.Он определяется (неявно) как функция:
r1: a' => a' => bool
Однако отмечу, что если я ограничу тип:
r2: b' => b' => bool
где b 'определен как тип a' с дополнительным ограничением, зависящим от r, это отношение на самом деле хорошо обосновано, и я могу использовать это хорошее свойство с теоремами стандартной библиотеки.
Мой пример
Чтобы быть более точным, я использую предикат finite_runs r s, чтобы утверждать, что из состояния s я могу иметь только конечное числопереходы (т.е. отношения, начинающиеся с s, заканчиваются).Конечно, если взять набор всех состояний, из факта finite_runs r s я не могу сделать вывод, что для всех состояний s' у меня есть finite_runs r s'.Однако мне нужно, чтобы это последнее свойство указывало на то, что отношение r является обоснованным во множестве всех состояний.
Но затем я понимаю, что r действительно обоснован, если я ограничу его набором состояний, которые связаны с s в некотором числе состояний.Это легко показать, потому что индуктивное определение finite_runs равно
inductive finite_runs for r where
"(⋀ s'. r s s' ⟹ finite_runs r s') ⟹ finite_runs r s"
Итак, в некоторых доказательствах я хочу использовать информацию, которую дает обоснованность r над множеством {s'. r** s s'}мне.Тем не менее, нет никакой теории в обоснованности, которая могла бы мне помочь.В этом случае я хотел бы сказать, что вышеупомянутый тип b' - это тип a' с дополнительным ограничением, равным {s'. r** s s'}, и затем создать теоремы в Обоснованности для этого отношения.
Как можноЯ ограничиваю домен функции, как в случае выше?