Что такое шаблон типа Quotient в Изабель?

Было бы лучше, если бы вы процитировали немного там, где вы видели фразу. Я знаю сопоставление с образцом и знаю частный тип, но не знаю образца частного.

Я предпочитаю не просить разъяснений, а затем ждать, поэтому я выбираю два из трех слов, тип частного. Если я ошибаюсь, это все равно достойный предмет и большая и важная часть Изабель / HOL.

Существует ключевое слово quotient_type, которое позволяет вам определять новый тип с помощью отношения эквивалентности.

Это часть частного пакета, описанного на странице 248 файла isar-ref.pdf. Есть страница Wiki, Quotient_type.

Более подробное описание дают Брайан Хуфманн и Ондржей Кунчар. Перейдите на веб-страницу Кунчара и просмотрите два файла PDF с заголовком Подъем и перемещение: Модульный дизайн для частных в Isabelle / HOL, которые не совсем то же самое.

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

Целые числа и рациональные числа в HOL являются частными типами, я выбираю один в качестве примера, целые числа

Вы можете начать с просмотра Int.thy.

Для частного типа вам необходимо отношение эквивалентности, которое определяет набор, а intrel - это то, что используется для определения этого набора для типа int.

definition intrel :: "(nat * nat) => (nat * nat) => bool" where
  "intrel = (%(x, y) (u, v). x + v = u + y)"

Это классическое определение целых чисел, основанное на натуральных числах. Целые числа - это упорядоченные пары натуральных чисел (и множества, как я описываю ниже), и они равны по этому определению.

Например, неофициально (2,3) = (4,5), потому что 2 + 5 = 4 + 3.

Я утомляю тебя, а ты ждешь хороших вещей. Вот его часть, использование quotient_type:

quotient_type int = "nat * nat" / "intrel"
  morphisms Rep_Integ Abs_Integ

Эти два морфизма вступают в игру, если вы хотите напрячь свой мозг и действительно понять, что происходит, что я и делаю. quotient_type генерирует множество функций и простых правил, и вам нужно проделать большую работу, чтобы все это найти, например, с помощью команды find_theorems.

Функция Abs преобразует упорядоченную пару в int. Проверьте это:

lemma "Abs_Integ(1,0) = (1::int)"
  by(metis one_int_def) 
  
lemma "Abs_Integ(x,0) + Abs_Integ(y,0) ≥ (0::int)"
  by(smt int_def) 

Они показывают, что int действительно заказанная пара под капотом двигателя.

Теперь я показываю явные типы этих морфизмов вместе с Abs_int и Rep_int, которые показывают int не только как упорядоченную пару, но как набор упорядоченных пар.

term "Abs_int   :: (nat * nat) set => int"  
term "Abs_Integ :: (nat * nat) => int"

term "Rep_int   :: int => (nat * nat) set"
term "Rep_Integ :: int => (nat * nat)"

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

lemma "Abs_Integ(1,0) = Abs_Integ(3,2)"
  by(smt nat.abs_eq split_conv) 
 
lemma "Abs_Integ(4,3) = Abs_Integ(3,2)"
  by(smt nat.abs_eq split_conv)

Чего бы вы ожидали, если бы добавили Abs_Integ(4,3) и Abs_Integ(3,2)? Этот:

lemma "Abs_Integ(2,3) + Abs_Integ(3,4) = Abs_Integ(2 + 3, 3 + 4)"
  by(metis plus_int.abs_eq plus_int_def split_conv)

Этот plus_int в доказательстве определен в Int.thy на строка 44.

lift_definition plus_int :: "int => int => int"
  is "%(x, y) (u, v). (x + u, y + v)"

Что это за подъем? Это привело бы меня к этому объяснению на несколько дней, а я только начинаю его понимать.

find_theorems показывает, что много чего спрятано, как я уже сказал:

thm "plus_int.abs_eq"  

find_theorems name: "Int.plus_int*"

Еще несколько примеров, но они призваны подчеркнуть, что под капотом движка int обратно связывается с классом эквивалентности как набором, где я использую intrel выше, чтобы правильно определить наборы:

term "Abs_int::(nat * nat) set => int"
term "Abs_int {(x,y). x + 3 = 2 + y}" (*(2,3)*)
term "Abs_int {(x,y). x + 4 = 3 + y}" (*(3,4)*)

lemma "Abs_int {(x,y). x + 3 = 2 + y} = Abs_int {(x,y). x + 100 = 99 + y}"
  by(auto)

Это auto доказательство было легким, но в следующем для меня нет волшебства, хотя оно простое.

lemma "Abs_int {(x,y). x + 3 = 2 + y} + Abs_int {(x,y). x + 4 = 3 + y}
        = Abs_int {(x,y). x + 7 = 5 + y}"
apply(auto simp add: plus_int.abs_eq plus_int_def intrel_def)
oops

Может быть, все, что мне нужно сделать, это задействовать что-то, что по умолчанию не является простым правилом.

Если quotient_type не является шаблоном частного типа, о котором вы говорите, по крайней мере, я кое-что понял, увидев все, что find_theorems возвращает о Int.plus_int* выше.