и встал на скользкую дорожку инфиксного использования S-комбинатора

[deniok]

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

Proposition : Set₁
Proposition = Set

_⇒_ : Proposition → Proposition → Proposition
P ⇒ Q = P → Q

data _∨_ (P Q : Proposition) : Proposition where
  injl : P → P ∨ Q
  injr : Q → P ∨ Q

data _∧_ (P Q : Proposition) : Proposition where
  _,_ : P → Q → P ∧ Q

_⇔_ : Proposition → Proposition → Proposition
P ⇔ Q = (P ⇒ Q) ∧ (Q ⇒ P)

Теперь можно доказывать всякие пропозициональные тавтологии. Для чистой импликации

{- комбинатор K -}
⇒-intro : {P Q : Proposition} → 
          P ⇒ Q ⇒ P
⇒-intro p q = p

{- комбинатор S -}
infixl 8 _ˢ_
_ˢ_ : {P Q R : Proposition} → 
           (P ⇒ Q ⇒ R) ⇒ (P ⇒ Q) ⇒ P ⇒ R
_ˢ_ p⇒q⇒r p⇒q p = p⇒q⇒r p (p⇒q p)

{- комбинатор B, известный также как композитор -} 
infixr 9 _∘_
_∘_ : {P Q R : Proposition} → 
           (Q ⇒ R) ⇒ (P ⇒ Q) ⇒ P ⇒ R
_∘_ q⇒r p⇒q p = q⇒r (p⇒q p)

Для дизъюнкции можно определить правила введения (они, естественно, совпадают с конструкторами)

∨-intro₁ : {P Q : Proposition} → 
            P ⇒ P ∨ Q
∨-intro₁ = injl 

∨-intro₂ : {P Q : Proposition} → 
            Q ⇒ P ∨ Q
∨-intro₂ = injr

и правило удаления (элиминатор)

∨-elim : {P Q R : Proposition} → 
          (P ⇒ R) ⇒ (Q ⇒ R) ⇒ P ∨ Q ⇒ R
∨-elim p⇒r q⇒r (injl p) = p⇒r p
∨-elim p⇒r q⇒r (injr q) = q⇒r q

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

Аналогично для конъюнкции

∧-intro : {P Q : Proposition} → 
          P ⇒ Q ⇒ P ∧ Q
∧-intro = _,_ 

∧-elim₁ : {P Q : Proposition} → 
          P ∧ Q ⇒ P
∧-elim₁ (p , _) = p

∧-elim₂ : {P Q : Proposition} → 
          P ∧ Q ⇒ Q
∧-elim₂ (_ , q) = q

(Элиминаторы эти на менее высоколобом языке носят названия fst и snd.)

Теперь можно писать доказательства тавтологий на двух языках. Например, коммутативность конъюнкции: через сопоставление с образцом

∨-comm : {P Q : Proposition} → 
         P ∨ Q ⇒ Q ∨ P
∨-comm (injl p) = injr p
∨-comm (injr q) = injl q

и через интродьюсеры-элиминаторы

∨-comm' : {P Q : Proposition} → 
         P ∨ Q ⇒ Q ∨ P
∨-comm' = ∨-elim ∨-intro₂ ∨-intro₁

УПРАЖНЕНИЕ 1. Докажите двумя способами коммутативность конъюнкции

∧-comm : {P Q : Proposition} → 
         P ∧ Q ⇒ Q ∧ P
∧-comm = {!!}

Докажем теперь ассоциативность дизъюнкции. Сначала паттерн-матчингом:

∨-ass₁ : {P Q R : Proposition} → 
         (P ∨ Q) ∨ R ⇒ P ∨ (Q ∨ R)
∨-ass₁ (injl (injl p)) = injl p
∨-ass₁ (injl (injr q)) = injr (injl q)
∨-ass₁ (injr r)        = injr (injr r)

Перепишем теперь все это на языке интродьюсеров-элиминаторов

∨-ass₁' : {P Q R : Proposition} → 
         (P ∨ Q) ∨ R ⇒ P ∨ (Q ∨ R)
∨-ass₁' = ∨-elim                              -- расщепляем (P ∨ Q) или R
                 (∨-elim                      -- расщепляем P или Q 
                         ∨-intro₁             -- если P, то положить влево
                        (∨-intro₂ ∘ ∨-intro₁) -- если Q, то положить вправо, влево
                 ) 
                 (∨-intro₂ ∘ ∨-intro₂)        -- если R, то положить вправо, вправо

УПРАЖНЕНИЕ 2. Докажите двумя способами ассоциативность дизъюнкции в обратном направлении

∨-ass₂ : {P Q R : Proposition} → 
         P ∨ (Q ∨ R) ⇒ (P ∨ Q) ∨ R
∨-ass₂ = {!!}

Теперь можем написать окончательную формулу (с равносильностью, а не с импликациями)

∨-ass : {P Q R : Proposition} → 
         (P ∨ Q) ∨ R ⇔ P ∨ (Q ∨ R)
∨-ass = ∨-ass₁ , ∨-ass₂

Перейдем к ассоциативности конъюнкции. Первый способ (через сопоставление с образцом), конечно, вне конкуренции

∧-ass₁ : {P Q R : Proposition} → 
         (P ∧ Q) ∧ R ⇒ P ∧ (Q ∧ R)
∧-ass₁ ((p , q) , r) =  p , (q , r)

Второй способ требует нудного использования элиминаторов fst (то есть ∧-elim₁) и snd (∧-elim₂)

∧-ass₁' : {P Q R : Proposition} → 
          (P ∧ Q) ∧ R ⇒ P ∧ (Q ∧ R)
∧-ass₁' x = ∧-intro (∧-elim₁ (∧-elim₁ x)) 
                    (∧-intro (∧-elim₂ (∧-elim₁ x)) 
                             (∧-elim₂ x)
                    ) 

Можно переписать это в бесточечном стиле, используя комбинаторы B и S (то есть доказанные выше теоремы)

∧-ass₁'' : {P Q R : Proposition} → 
           (P ∧ Q) ∧ R ⇒ P ∧ (Q ∧ R)
∧-ass₁'' = ∧-intro ∘ ∧-elim₁ ∘ ∧-elim₁ ˢ (∧-intro ∘ ∧-elim₂ ∘ ∧-elim₁ ˢ ∧-elim₂) 

УПРАЖНЕНИЕ 3. Докажите двумя способами ассоциативность конъюнкции в обратном направлении

∧-ass₂ : {P Q R : Proposition} → 
         P ∧ (Q ∧ R) ⇒ (P ∧ Q) ∧ R
∧-ass₂  = {!!}

Исходник можно поглядеть здесь.

Comments

[dtim.livejournal.com]

Как по-твоему, Agda проще или сложнее для восприятия студентами, чем Coq?

[deni-ok.livejournal.com]

Абстрактному студенту - не знаю. Думаю "математикам" чуть по-легче будет c COQом, а функциональщикам - с Агдой. Ну и по COQ чуть получше с литературой, в смысле толстых книжек, годящихся на роль учебника-справочника.

[dtim.livejournal.com]

Спасибо.