Могу ли я извлечь Coq-доказательство в качестве функции Haskell?

Ответ 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')

Ответ 2

Текущая копия Software Foundations от 25 июля 2012 года довольно кратко объясняет это в последней главе " Extraction2". Ответ заключается в том, что это, безусловно, можно сделать, например:

Extraction Language Haskell
Extraction "divalg.hs" divalg

Необходим еще один трюк. Вместо Prop, divalg должен быть Type. В противном случае он будет удален в процессе извлечения.

Э-э, @Правильно, я не ответил на этот вопрос, потому что не знаю, как объяснить, как проф. Пирс выполнил это в своем NormInType.v варианте его Norm.v и MoreStlc.v.

ОК, здесь остальная часть моего частичного ответа в любом случае.

Здесь, где "divalg" появляется выше, необходимо будет предоставить список всех предложений, разделенных пробелами (каждый из них должен быть переопределен как Type, а не Prop), на котором полагается divalg. Для подробного, интересного и рабочего примера извлечения доказательств можно обратиться к главе Extraction2, упомянутой выше. Этот пример извлекается в OCaml, но адаптация его для Haskell - это просто вопрос использования Extraction Language Haskell, как указано выше.

В частности, причина, по которой я провел некоторое время, не зная вышеприведенного ответа, заключается в том, что я использовал копию Software Foundations от 14 октября 2010 года, которую я загрузил в 2011 году.