Настройка зависимых типов функциональных пространств
Предположим, у нас есть следующее определение, которое представляет ограниченное целое число в интервале Clopen <a, b),
def zbound (x₁ x₂ : ℤ) :=
{ n : ℤ // x₁ ≤ n ∧ n < x₂ }
Теперь я хочу функциональное пространство от zbound x₁ x₂ в bool упакован с доказательством x₁ < x₂, так что диапазон правильно представлен.
structure bounded_f (x₁ x₂ : ℤ) :=
(map : zbound x₁ x₂ → bool)
(prf : x₁ < x₂)
Проблема сейчас в следующем. Я хотел бы иметь функцию обновления сортов, которая обрабатывает bounded_f как map и обновляет его, чтобы вернуть true для определенного значения xв противном случае, и это важно, делегирует функциональность оригиналу bounded_f,
def inject_true {x₁ x₂} (x : ℤ) (f : bounded_f x₁ x₂) :
bounded_f (min x₁ x) (max x x₂) :=
⟨λ⟨x', prf⟩, if x = x' then true else f.map ⟨x', sorry⟩, _⟩
Полученная функция должна иметь измененное пространство определения, а именно, она больше не работает в ограниченном диапазоне от x₁ в x₂, а скорее на диапазоне от min x₁ x в max x x₂, Интуитивно понятно, что это просто расширяет диапазон, необходимый для нового обновления.
К сожалению, я понятия не имею, что поставить вместо sorry в тех случаях, когда x меньше, чем нижняя граница или больше, чем верхняя граница. Моя проблема в том, что Лин хочет, чтобы я показал:
x₁ ≤ x' ∧ x' < x₂
Это, однако, не так, так как я бы предпочел расширенный диапазон, чем исходный. Что-то не так с подачей заявки? f.map сразу и мне нужно... как-то изменить?