PropCalculusMini.agda

{-
Определим на Агде интуиционистскую логику высказываний 
-}

module PropCalculusMini where

{-
Задаём стандартные приоритеты и ассоциативность 
для логических связок
-}
infixr 0 _⇒_ _⇔_
infixr 1 _∨_
infixr 2 _∧_
--infix  3 ¬_

{-
Соответствие Карри-Ховарда позволяет нам отождествить
высказывания с типами.
-}
Proposition : Set₁
Proposition = Set

{-
Доказательства отождествляются с термами. 
Если мы предъявляем терм некоторого типа,
то тем самым мы даем доказательство 
соответствующего высказывания.

Доказуемость высказывания определяется 
населенностью (или обитаемостью) типа.
-}

{- 
Импликация изоморфна пространству функций. 
Высказывание P ⇒ Q доказано, 
если предъявляется функция, 
переводящая доказательство P в доказательство Q.
 -}
_⇒_ : Proposition → Proposition → Proposition
P ⇒ Q = P → Q

{- 
Дизъюнкция изоморфна размеченному объединению.  
Высказывание P ∨ Q доказано, 
если предъявлено одно из двух доказательств: 
либо для P, либо для Q.
-}
data _∨_ (P Q : Proposition) : Proposition where
  injl : P → P ∨ Q
  injr : Q → P ∨ Q

{- 
Конъюнкция изоморфна паре.
Высказывание P ∧ Q доказано,
если предъявлена пара доказательств: 
одно для P, другое для Q. 
-}
data _∧_ (P Q : Proposition) : Proposition where
  _,_ : P → Q → P ∧ Q

{-
Логическая эквивалентность 
определяется через импликацию и конъюнкцию.
-}
_⇔_ : Proposition → Proposition → Proposition
P ⇔ Q = (P ⇒ Q) ∧ (Q ⇒ P)


--------------------------------------------------------

{-
Теперь можно доказывать 
всевозможные интуиционистские тавтологии.
-}

------ ИМПЛИКАЦИОЛОГИЯ ------
{- 
Можно вывести аксиомы для импликации, 
имеющие место в исчислении высказываний гильбертовского типа,
поскольку у нас есть механизм абстрагирования 
либо через лямбды, 
либо (как здесь) через связывание с простым образцом
-}
{- комбинатор K, аксиома 1 -}
⇒-intro : {P Q : Proposition} → 
          P ⇒ Q ⇒ P
⇒-intro p q = p
--axiom₁ = ⇒-intro

{- комбинатор S, аксиома 2 -}
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)
--⇒-elim = _ˢ_
--axiom₂ = ⇒-elim


{- Рефлексивность импликации -}
⇒-refl : {P : Proposition} → 
          P ⇒ P
⇒-refl p = p

{- Ещё ряд общеизвестных и полезных теорем -}
flip : {P Q R : Proposition} → 
           (P ⇒ Q ⇒ R) ⇒ Q ⇒ P ⇒ R
flip p⇒q⇒r q p = p⇒q⇒r p q

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


------ ДИЗЪЮНКЦИОЛОГИЯ ------
{- 
Аксиомы 6 и 7 (введения дизъюнкции) 
гильбертовского исчисления высказываний -
это в точности конструкторы размеченного объединения. 
-}
∨-intro₁ : {P Q : Proposition} → 
            P ⇒ P ∨ Q
∨-intro₁ = injl 

∨-intro₂ : {P Q : Proposition} → 
            Q ⇒ P ∨ Q
∨-intro₂ = injr
{- 
Аксиома 8, иногда называемая <<разбор случаев>>.
Сопоставление с образцом позволяет написать 
ее доказательство.
-}
∨-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

{-
Теоремы можем доказывать двумя способами.
Во-первых, можно использовать всю мощь сопоставления с образцом Агды.
Во-вторых, можно ограничиться правилами введения и удаления связок,
выступающих в роли аксиом для исчисления высказываний в стиле Гильберта.
Второй способ был полезней при проверке домашних заданий 
и, к моему удивлению, оказался не сильно длиннее.
Единственное дополнение к аксиомам, которое я использовал - 
закон композиции (комбинатор B).
-}

{- Коммутативность дизъюнкции -}
∨-comm : {P Q : Proposition} → 
         P ∨ Q ⇒ Q ∨ P
∨-comm = ∨-elim ∨-intro₂ ∨-intro₁
--∨-comm (injl p) = injr p
--∨-comm (injr q) = injl q

{- 
Ассоциативность дизъюнкции.
В отличие от данных выше доказательств 
структурно симметричных утверждений
здесь следует приводить доказательства <<в обе стороны>>. 
-}
∨-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₁ = ∨-elim                             -- расщепляем (P ∨ Q) или R
                (∨-elim                     -- расщепляем P или Q 
                        ∨-intro₁            -- если P, то положить влево
                       (∨-intro₂ ∘ ∨-intro₁) -- если Q, то положить вправо, влево
                ) 
                (∨-intro₂ ∘ ∨-intro₂)        -- если R, то положить вправо, вправо

∨-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₂


------ КОНЪЮНКЦИОЛОГИЯ ------
{- Проекции пары, известные как fst и snd,
задают аксиомы 3 и 4 гильбертовского исчисления высказываний. 
Сопоставление с образцом легко позволяет написать 
их доказательство.
 -}
∧-elim₁ : {P Q : Proposition} → 
          P ∧ Q ⇒ P
∧-elim₁ (p , _) = p

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

{- 
Аксиома 5 (введение конъюнкции) 
это в точности конструктор пары. 
 -}
∧-intro : {P Q : Proposition} → 
          P ⇒ Q ⇒ P ∧ Q
∧-intro = _,_ 

{- Каррирование и декаррирование -}
curry : {P Q R : Proposition} → 
           (P ∧ Q ⇒ R) ⇒ P ⇒ Q ⇒ R
curry p∧q⇒r p q = p∧q⇒r (∧-intro p q)

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

{- Транзитивность импликации -}
⇒-trans : {P Q R : Proposition} → 
           (P ⇒ Q) ∧ (Q ⇒ R) ⇒ P ⇒ R
⇒-trans [p⇒q]∧[q⇒r] p = ∧-elim₂ [p⇒q]∧[q⇒r] (∧-elim₁ [p⇒q]∧[q⇒r] p)
--⇒-trans (p⇒q , q⇒r) p = q⇒r (p⇒q p)

{- Коммутативность конъюнкции -}
∧-comm : {P Q : Proposition} → 
         P ∧ Q ⇒ Q ∧ P
∧-comm = {!!}
{- 
Ассоциативность конъюнкции.
-}
∧-ass₁ : {P Q R : Proposition} → 
         (P ∧ Q) ∧ R ⇒ P ∧ (Q ∧ R)
∧-ass₁ = ∧-intro ∘ ∧-elim₁ ∘ ∧-elim₁ ˢ (∧-intro ∘ ∧-elim₂ ∘ ∧-elim₁ ˢ ∧-elim₂) 
--∧-ass₁ = (∧-intro ∘ ∧-elim₁ ∘ ∧-elim₁) ˢ ((∧-intro ∘ ∧-elim₂ ∘ ∧-elim₁) ˢ ∧-elim₂) 
{-
∧-ass₁ [p∧q]∧r = ∧-intro (∧-elim₁ (∧-elim₁ [p∧q]∧r)) 
                        (∧-intro (∧-elim₂ (∧-elim₁ [p∧q]∧r)) 
                                 (∧-elim₂ [p∧q]∧r)

                        ) 
-}
--∧-ass₁ ((p , q) , r) =  p , (q , r)

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

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