Определение подкласса с параметрами в Изабель - PullRequest
Новая
       8

Определение подкласса с параметрами в Изабель

0 голосов
/ 26 июня 2018

Документация о классах типов в Изабель (раздел 3.5) объясняет, как определять дополнительные отношения подкласса "по факту", предоставляя доказательства отсутствующих аксиом.Есть ли способ сделать это, когда подкласс добавляет параметры в дополнение к аксиомам?

Например, предположим, что у меня есть следующие классы: 

class setoid =
fixes eq :: "'a ⇒ 'a ⇒ bool" (infix "≈" 50)
assumes eq_refl : "∀x. x ≈ x"
and eq_symm : "∀x y. x ≈ y ⟶ y ≈ x"
and eq_trans : "∀x y z. x ≈ y ⟶ y ≈ z ⟶ x ≈ z"

class preorder =
fixes le :: "'a ⇒ 'a ⇒ bool" (infix "≲" 50)
assumes le_refl : "∀x. x ≲ x"
and le_trans : "∀x y z. x ≲ y ⟶ y ≲ z ⟶ x ≲ z"

Каждый предзаказ должен быть сетоидом, когда мысимметризовать его неравенство: 

definition (in preorder) peq :: "'a ⇒ 'a ⇒ bool"
where "peq x y ≡ (x ≲ y) ∧ (y ≲ x)"

Однако следующее не удается: 

subclass (in preorder) setoid

с ошибкой exception TYPE raised: Class preorder lacks parameter(s) "setoid_class.eq" of setoid.Но я не могу понять синтаксис, чтобы сказать Изабель, что этот пропущенный параметр должен быть отношением peq, которое я определил.

Я могу сделать это, если перейду к локали вместо классов типов (доказательства опущены длякраткость): 

interpretation peq_class : setoid peq
proof
show "∀x. peq x x" sorry
show "∀x y. peq x y ⟶ peq y x" sorry
show "∀x y z. peq x y ⟶ peq y z ⟶ peq x z" sorry
qed

Но это не позволяет мне использовать preorder в качестве setoid, то есть interpretation не действует как subclass или instantiation,Я хочу иметь возможность создавать экземпляр типа как предзаказ, а затем автоматически использовать определения и теоремы о сетоидах для этого типа путем симметризации его неравенства.Как мне этого добиться?

1 Ответ

0 голосов
/ 26 июня 2018

Это ограничение способа реализации классов типов в Изабель.Я не уверен, что следующий обходной путь настолько короткий, насколько это возможно, но он работает: 

class eq =
  fixes eq :: "'a ⇒ 'a ⇒ bool" (infix "≈" 50)

class setoid = eq +
  assumes eq_refl : "∀x. x ≈ x"
    and eq_symm : "∀x y. x ≈ y ⟶ y ≈ x"
    and eq_trans : "∀x y z. x ≈ y ⟶ y ≈ z ⟶ x ≈ z"

class preorder =
  fixes le :: "'a ⇒ 'a ⇒ bool" (infix "≲" 50)
  assumes le_refl : "∀x. x ≲ x"
    and le_trans : "∀x y z. x ≲ y ⟶ y ≲ z ⟶ x ≲ z"

class preorder_setoid = preorder + eq +
  assumes eq_def: "x ≈ y ⟷ (x ≲ y) ∧ (y ≲ x)"

subclass (in preorder_setoid) setoid
  apply standard
  unfolding eq_def
  using le_refl le_trans by auto

Недостатком является то, что вы все равно не можете создать экземпляр preorder a setoidавтоматически, но вы должны сделать это вручную.Для каждого экземпляра preorder вы можете добавить экземпляр preorder_setoid.Все они будут выглядеть одинаково;они должны определять eq в соответствии с eq_def.В этом случае автоматическое подтверждение.

Обновление Как указано в комментариях, константа eq всегда будет интерпретироваться в контексте класса eq;то есть, ничего интересного не может быть доказано без дальнейших аннотаций типов.Можно сказать, что вывод типа сделать лучше: 

setup {*
  Sign.add_const_constraint (@{const_name "eq"}, SOME @{typ "'a::setoid ⇒ 'a ⇒ bool"})
*}
...