Индуктивный предикат с параметрами типа в Isabelle

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

В Coq я бы сделал что-то вроде этого:

Inductive monoid (τ : Type) (op: τ -> τ -> τ) (i: τ): Prop :=
| axioms: (forall (e: τ), op e i = e) ->
          (forall (e: τ), op i e = e) ->
          monoid τ op i.

Я не знаю, как сделать то же самое в Изабель. Концептуально я подумал о чем-то вроде этого:

inductive 'a monoid "('a ⇒ 'a ⇒ 'a) ⇒ 'a ⇒ bool" for f i where
  axioms: "⟦f e i = e; f i e = e⟧ ⇒ monoid f i"

Но это неверно для Изабель.

Как мне определить индуктивные предикаты с типизированными параметрами в Isabelle?


type-parameter coq isabelle
person Alex    schedule 12.02.2015    source источник

Ответы (1)


arrow_upward
9
arrow_downward

Я мало что знаю о Coq, но система шрифтов Изабель совсем другая. Значения Isabelle не принимают «параметры типа», а типы Isabelle не принимают «параметры значения».

В Изабель ваш пример представляет собой простое полиморфное определение, которое можно сделать следующим образом:

inductive monoid :: "('a ⇒ 'a ⇒ 'a) ⇒ 'a ⇒ bool" for f i where
  axioms: "⟦f e i = e; f i e = e⟧ ⟹ monoid f i"

Я должен указать, что это означает, что если существует хотя бы один e, для которого это верно, у вас есть моноид. Вероятно, вы хотели написать

inductive monoid :: "('a ⇒ 'a ⇒ 'a) ⇒ 'a ⇒ bool" for f i where
  axioms: "⟦⋀e. f e i = e; ⋀e. f i e = e⟧ ⟹ monoid f i"

Здесь e определяется количественно в предположениях, то есть законы должны выполняться для всех e, чтобы образовался моноид.

Выполнение этого как индуктивного определения возможно и имеет то преимущество, что оно автоматически генерирует соответствующие правила введения / исключения (и дает возможность генерировать больше с помощью inductive_cases). Однако есть и другие способы.

Использование определения

Однако вы также можете написать это как простое определение:

definition monoid :: "('a ⇒ 'a ⇒ 'a) ⇒ 'a ⇒ bool" where
  "monoid f i = ((∀e. f e i = e) ∧ (∀e. f i e = e))"

Это дает вам определение monoid как лемму monoid_def. Если вам нужны правила введения / исключения, вы должны вывести их самостоятельно.

Использование локали

Третье и, вероятно, наиболее подходящее решение - это locales. Локаль - это способ сохранения определенных фиксированных переменных и предположений в контексте, а причина - в этом контексте. В следующем примере показано, как определить моноид как локаль, получить леммы в этой локали, а затем интерпретировать локаль для конкретного примера моноида (а именно списки) и использовать леммы, которые мы доказали для них в локали.

locale monoid =
  fixes i :: 'a and f :: "'a ⇒ 'a ⇒ 'a"
  assumes left_neutral:  "f i e = e"
      and right_neutral: "f e i = e"
begin
  lemma neutral_unique_left:
    assumes "⋀e. f i' e = e"
    shows   "i' = i"
  proof-
    from right_neutral have "i' = f i' i" by simp
    also from assms have "f i' i = i" by simp
    finally show "i' = i" .
  qed
end

thm monoid.neutral_unique_left
(* Output: monoid i f ⟹ (⋀e. f i' e = e) ⟹ i' = i *)

(* Let's interpret our monoid for the type "'a list", with [] 
   as neutral element and concatenation (_ @ _) as the operation. *)
interpretation list_monoid: monoid "[]" "λxs ys. xs @ ys"
  by default simp_all

thm list_monoid.neutral_unique_left
(* Output: (⋀e. i' @ e = e) ⟹ i' = [] *)

Использование класса типа

Четвертая возможность, которая похожа на локали, - это возможность классов типов. Isabelle поддерживает классы типов (например, классы в Haskell, хотя и более строгие), и вы можете создать класс типа monoid, а затем создать его экземпляр для конкретных типов, таких как nat, int, 'a list и т. Д.

Дополнительная информация

Для получения дополнительной информации об индуктивных предикатах, локали и классах типов см. Документацию по этим инструментам: http://isabelle.in.tum.de/documentation.html

person Manuel Eberl    schedule 12.02.2015