Создание типа данных с неравенствами в Изабель

Question

Я очень плохо знаком с Изабель и пытаюсь реализовать такой тип данных, как

тип данных фрукты = яблоко | Бананы | Мускусная дыня

(выбор слов здесь неуместен, чтобы не путать его с попыткой сделать что-то еще)

Тем не менее, важно отметить, что Apple ≤ Banana ≤ Cantaloupe.

Как лучше всего реализовать Изабель? Будет ли уместным тип данных?

Бонусный вопрос: как вы могли бы создать переменную, чтобы быть одним из этих 3 вариантов?

Answer 1

О вашем главном вопросе.

Я предполагаю, что вы хотите указать порядок вручную, т.е. вы хотите изложить все случаи. Если вас устраивает стандартный лексикографический порядок, есть запись AFP, которая способна сделать это автоматически.

Да, правильный способ реализации того, что вы хотите - начать с типа данных. Затем вам нужно будет определить ≤ оператор. Для этого вам нужно создать экземпляр класса. Первые два раздела в документации классов типов дадут вам представление о том, как это работает. Для вашего примера это будет выглядеть примерно так:

instantiation fruit :: linorder begin

fun less_fruit where
"Apple < Apple ⟷ False" |
"Apple < _ ⟷ True" |
"Banana < Apple ⟷ False" |
"Banana < Banana ⟷ False" |
"Banana < _ ⟷ True" |
"Cantaloupe < _ ⟷ False"

definition less_eq_fruit :: "fruit ⇒ fruit ⇒ bool" where
[simp]: "less_eq_fruit x y ⟷ x = y ∨ x < y"

instance sorry

end

Наконец, вам придется выполнить доказательство экземпляра, а именно: вам нужно показать, что определенные вами операторы действительно образуют линейный порядок. В приведенном выше примере я обманул, используя sorry команда.

Способ сделать это правильно напрямую приводит к вашему бонусному вопросу.

Вы можете создать переменные, используя cases тактика. Посмотрите это в действии для доказательства экземпляра:

instance proof
  fix x y :: fruit
  show "(x < y) = (x ≤ y ∧ ¬ y ≤ x)"
    by (cases x; cases y; simp)
next
   (* more stuff to prove here *)
qed

cases Метод принимает имя переменной и разбивает текущую цель на несколько случаев (здесь: три). ; Оператор (последовательная композиция) применяет первый метод и применяет второй метод ко всем новым подцелям. Наконец, все можно решить с помощью simp,