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

Question

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

В 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?

Answer 1

Я не очень разбираюсь в Coq, но система типа Isabelle очень отличается. Значения Isabelle не принимают «параметры типа», а типы 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. Если вам нужны правила введения/исключения, вы должны сами их вывести.

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

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

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