Ответ 1
Благодаря Prof. Pierce summer 2012 video 4.1 как Dan Feltey, мы видим, что ключ заключается в том, что теорема, которая должна быть извлечена, должна предоставлять член Type, а не обычный вид предложений, который Prop.
Для конкретной теоремы затронутая конструкция является индуктивным Prop ex и его обозначением exists. Подобно тому, что сделал проф. Пирс, мы можем изложить наши собственные альтернативные определения ex_t и exists_t, которые заменяют вхождения Prop появлением Type.
Вот обычное переопределение ex и exists аналогично тому, как они определены в стандартной библиотеке Coq.
Inductive ex (X:Type) (P : X->Prop) : Prop :=
ex_intro : forall (witness:X), P witness -> ex X P.
Notation "'exists' x : X , p" := (ex _ (fun x:X => p))
(at level 200, x ident, right associativity) : type_scope.
Ниже приведены альтернативные определения.
Inductive ex_t (X:Type) (P : X->Type) : Type :=
ex_t_intro : forall (witness:X), P witness -> ex_t X P.
Notation "'exists_t' x : X , p" := (ex_t _ (fun x:X => p))
(at level 200, x ident, right associativity) : type_scope.
Теперь, к сожалению, необходимо повторить как утверждение, так и доказательство теоремы, используя эти новые определения.
Что в мире??
Почему необходимо сделать повторное утверждение теоремы и повторное доказательство теоремы, которые отличаются только использованием альтернативного определения квантора?
Я надеялся использовать существующую теорему в
Prop, чтобы снова доказать теорему вType. Эта стратегия терпит неудачу, когда Coq отвергает тактику доказательстваinversionдляPropв среде, когда этотPropиспользуетexists, а цель -Type, которая используетexists_t. Coq сообщает: "Ошибка: для инверсии потребуется анализ случаев в сортировке Set, который не разрешен для индуктивного определения ex". Такое поведение произошло в Coq 8.3. Я не уверен, что это все еще встречается в Coq 8.4.Я думаю, что необходимость повторить доказательство действительно глубока, хотя я сомневаюсь, что лично мне вполне удается понять его глубину. Он включает в себя факты, что
Propявляется "нецелесообразным", аTypeне является нецелесообразным, а скорее молчаливо "стратифицированным". Предикативность (если я правильно понимаю) уязвимость к парадоксу Рассела, что множество S множеств, которые не являются членами сами по себе, не может быть членом S, а не член S.Typeизбегает парадокса Рассела, молчаливо создавая последовательность более высоких типов, которые содержат более низкие типы. Поскольку Coq пропитан интерпретацией формул-как-то типов соответствия Карри-Говарда, и, если я получу это право, мы можем даже понять стратификацию типов в Coq как способ избежать неполноты Гёделя, явления, которое выражают некоторые формулы ограничения на такие формулы, как сами по себе, и тем самым становятся непознаваемыми по отношению к их истине или ложности.
Вернемся на планету Земля, вот повторная формулировка теоремы с использованием "exist_t".
Theorem divalg_t : forall n m : nat, exists_t q : nat,
exists_t r : nat, n = plus (mult q m) r.
Как я пропустил доказательство divalg, я также опускаю доказательство divalg_t. Я остановлюсь только на том, что у нас есть счастье, что тактика доказательства, включая "существует" и "инверсия", работает точно так же с нашими новыми определениями "ex_t" и "exist_t".
Наконец, сама добыча выполняется легко.
Extraction Language Haskell.
Extraction "divalg.hs" divalg_t.
В результате файл Haskell содержит ряд определений, суть которых - разумный код. И мне немного мешало мое почти полное незнание языка программирования Haskell. Обратите внимание, что Ex_t_intro создает результат, тип которого ex_t; O и S - это нуль и функция-преемник из арифметики Пеано; beq_nat проверяет числа Пеано для равенства; nat_rec - это функция более высокого порядка, которая повторяет функцию среди своих аргументов. Определение nat_rec здесь не показано. Во всяком случае, он генерируется Coq в соответствии с индуктивным типом "nat", который был определен в Coq.
divalg :: Nat -> Nat -> Ex_t Nat (Ex_t Nat ())
divalg n m =
case m of {
O -> Ex_t_intro O (Ex_t_intro n __);
S m' ->
nat_rec (Ex_t_intro O (Ex_t_intro O __)) (\n' iHn' ->
case iHn' of {
Ex_t_intro q' hq' ->
case hq' of {
Ex_t_intro r' _ ->
let {k = beq_nat r' m'} in
case k of {
True -> Ex_t_intro (S q') (Ex_t_intro O __);
False -> Ex_t_intro q' (Ex_t_intro (S r') __)}}}) n}
Обновление 2013-04-24: теперь я знаю немного больше Haskell. Чтобы помочь другим в чтении извлеченного кода выше, я представляю следующий переписанный вручную код, который, как я утверждаю, эквивалентен и более читабельным. Я также представляю извлеченные определения Nat, O, S и nat_rec, которые я не устранил.
-- Extracted: Natural numbers (non-negative integers)
-- in the manner in which Peano defined them.
data Nat =
O
| S Nat
deriving (Eq, Show)
-- Extracted: General recursion over natural numbers,
-- an interpretation of Nat in the manner of higher-order abstract syntax.
nat_rec :: a1 -> (Nat -> a1 -> a1) -> Nat -> a1
nat_rec f f0 n =
case n of {
O -> f;
S n0 -> f0 n0 (nat_rec f f0 n0)}
-- Given non-negative integers n and m, produce (q, r) with n = q * m + r.
divalg_t :: Nat -> Nat -> (Nat, Nat)
divalg_t n O = (O, n) -- n/0: Define quotient 0, remainder n.
divalg_t n (S m') = divpos n m' -- n/(S m')
where
-- Given non-negative integers n and m',
-- and defining m = m' + 1,
-- produce (q, r) with n = q * m + r
-- so that q = floor (n / m) and r = n % m.
divpos :: Nat -> Nat -> (Nat, Nat)
divpos n m' = nat_rec (O, O) (incrDivMod m') n
-- Given a non-negative integer m' and
-- a pair of non-negative integers (q', r') with r <= m',
-- and defining m = m' + 1,
-- produce (q, r) with q*m + r = q'*m + r' + 1 and r <= m'.
incrDivMod :: Nat -> Nat -> (Nat, Nat) -> (Nat, Nat)
incrDivMod m' _ (q', r')
| r' == m' = (S q', O)
| otherwise = (q', S r')