Функтороподобная конструкция в Изабель / Изаре - PullRequest
Новая
       33

Функтороподобная конструкция в Изабель / Изаре

2 голосов
/ 06 марта 2019

Вот небольшая теорема в математике:

Предположим, что u не является элементом A, а v не является элементом B, а f является инъективной функцией от A до B. Пусть A '= Aunion {u} и B '= B union {v}, и определим g: A' -> B 'с помощью g (x) = f (x), если x находится в A, и g (u) = v. Тогда gтакже инъективен.

Если бы я писал код, подобный OCaml, я бы представлял A и B как типы, а f как функцию A-> B, что-то вроде 

module type Q = 
  sig
   type 'a
   type 'b
   val f: 'a -> 'b
  end

, а затем определял быfunctor 

module Extend (M : Q) : Q = 
  struct
    type a = OrdinaryA of M.a | ExoticA
    type b = OrdinaryB of M.b | ExoticB
    let f x = match x with
        OrdinaryA t -> OrdinaryB ( M.f t)
      | Exotic A -> ExoticB
  end;;

, и моя теорема будет состоять в том, что если Q.f инъективен, то и 1012 *, где я надеюсь, что синтаксис получился более или менее правильным.

Я бы хотел сделать то же самое в Изабель / Изаре.Обычно это означало бы написать что-то вроде 

definition injective :: "('a  ⇒ 'b)  ⇒ bool"
  where "injective f  ⟷ ( ∀ P Q.  (f(P) = f(Q)) ⟷ (P = Q))" 

proposition: "injective f ⟹ injective (Q(f))"

и Q - это что-то.Я не знаю, как сделать в Изабелле одну операцию, аналогичную функтору Q в OCaml, которая создает два новых типа данных и функцию между ними.Доказательство инъективности выглядит так, как будто это было бы довольно просто - просто разделение на четыре случая.Но я хотел бы помочь определить новую функцию, которую я назвал Q f, учитывая функцию f.

1 Ответ

1 голос
/ 06 марта 2019

Вот решение. Я пытался сделать «определение» для функции Q, но не смог этого сделать; вместо этого, создавая константу Q (построенную по сильной аналогии с map), позвольте мне сформулировать и доказать теорему: 

theory Extensions
  imports Main
begin
text ‹We show that if we have f: 'a → 'b that's injective, and we extend 
both the domain and codomain types by a new element, and extend f in the 
obvious way, then the resulting function is still injective.›
  definition injective :: "('a  ⇒ 'b)  ⇒ bool"
    where "injective f  ⟷ ( ∀ P Q.  (f(P) = f(Q)) ⟷ (P = Q))" 

datatype 'a extension = Ordinary 'a | Exotic

fun Q ::  "('a  ⇒ 'b) ⇒ (('a extension)  ⇒ ('b extension))"  where 
   "Q f (Ordinary u) = Ordinary (f u)" |
   "Q f (Exotic) = Exotic"

lemma "⟦injective f⟧ ⟹ injective (Q f)"
  by (smt Q.elims extension.distinct(1) extension.inject injective_def)

end
...