и встал на скользкую дорожку инфиксного использования S-комбинатора
Читая в прошедшем семестре курс матлогики, придумывал разные задачки для практики и многие решал (для себя) на Агде. Сейчас сел все это упорядочивать. Обнаружил, что сопоставление с образцом, конечно же, обыгрывает явные элиминаторы по выразительности при записи доказательств, но элиминаторы иногда сопротивляются довольно успешно.
Вот, скажем, исчисление высказываний.
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₂ = {!!}
Исходник можно поглядеть здесь.
Вот, скажем, исчисление высказываний.
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₂ = {!!}
Исходник можно поглядеть здесь.