и встал на скользкую дорожку инфиксного использования 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]

Спасибо.

[nealar.livejournal.com]

Ну наконец-то я знаю агдочку в достаточной степени, чтобы читать такое без запинки!

[deni-ok.livejournal.com]

Упражнения выполнены успешно? :)

[nealar.livejournal.com]

Вот щаз займусь. :)

[thedeemon.livejournal.com]

>Докажите двумя способами

А потом сделайте два доказательства равности тех двух доказательств и постройте гомотопию между этими двумя равенствами...

[deni-ok.livejournal.com]

Если не говорить --without-K, то агдин паттерн-матчинг схлопывает все доказательства пропозиционального равенства в одно:

data _≡_ {A : Set} : A → A → Set where
  refl : ∀ x → x ≡ x

-- можем доказать единственность доказательства равенства
-- uniqueness of identity proofs, uip
uip : {A : Set} (x y : A) (p q : x ≡ y) →  p ≡ q
uip .x .x (refl x) (refl .x)  = refl (refl x)

И никаких гомотопий :)

[sassa-nf.livejournal.com]

while we are on this topic, можно спросить, какая разница между

data _==_ {A : Set} : A -> A -> Set where
  refl : forall x -> x == x

и

data _==_ {A : Set} (x : A) : A -> Set where
  refl : x == x

? (кроме формы конструктора, конечно; я имею в виду именно reasoning, который Агда сможет или не сможет выполнять? Или с этой т.з. совершенно всё равно?)

[deni-ok.livejournal.com]

data _≡_ {A : Set} : A → A → Set where
  refl : ∀ x → x ≡ x

data _≐_ {A : Set} (x : A) : A → Set where
  refl' : x ≐ x

lem1 : {A : Set} (x y : A) →  x ≡ y → x ≐ y
lem1 x .x (refl .x) = refl'

lem2 : {A : Set} (x y : A) →  x ≐ y → x ≡ y
lem2 x .x refl' = refl x

:)

Конфлюэнтность же никто не отменял. Тайпчекер приводит то, что требуется уравнять, к нормальной форме, тупо пользуясь definitional equality там, где это возможно, и сравнивает. В первом случае от делает это в трех местах

ex : (x : ℕ) → zero + suc x ≡ suc (zero + x)
ex x = refl (zero + zero + suc x)

, а во втором в двух. Но нормальная форма единственна (suc x), поэтому разницы нет.

[sassa-nf.livejournal.com]

ок, значит, в обоих случаях мы говорим об одинаковом типе _==_(x y). а на практике что удобней?

[deni-ok.livejournal.com]

Безаргументный конструктор короче, поэтому в большинстве случаев удобнее (так в стандартной библиотеке и сделано). Единственное исключение - хитрые случаи, полезно/хочется видеть аппликативную структуру refl. Сравни, например

uip : {A : Set} (x y : A) (p q : x ≡ y) →  p ≡ q
uip x .x (refl .x) (refl .x)  = refl (refl x)

и

uip' : {A : Set} (x y : A) (p q : x ≐ y) →  p ≐ q
uip' x .x refl' refl'  = refl'

Хотя в первом случае в правой части можно вместо точного выражения, которое нам дает Агси (C-c C-a), написать

uip : {A : Set} (x y : A) (p q : x ≡ y) →  p ≡ q
uip x .x (refl .x) (refl .x)  = refl _

(Это справа вообще всегда можно делать с refl, потому что понятно, что туда пропишется NF из типа.)

[deni-ok.livejournal.com]

Кстати странно, если включить

{-# OPTIONS --without-K #-}

то сообщения об ошибках для uip и uip' будут разные. Надо бы в исходники посмотреть, что там как.

[deni-ok.livejournal.com]

Кстати, этот вопрос актуален в контексте попыток совместить Агду с унивалентностью:
https://lists.chalmers.se/pipermail/agda/2014/006347.html

[sassa-nf.livejournal.com]

ну почему же, в последнем задании целых три доказательства. Что это нам даёт? А теперь нужно строить гомотопию между гомотопиями между этими доказательствами равенств.

[deni-ok.livejournal.com]

Ну и мы довольно быстро приходим к тому, что число шагов меньше бесконечности нас не устраивает, так что минимально адекватными являются (∞,1)-категории :)

[blog.songnic.ru (from livejournal.com)]

+один...