-- This file:
--   http://angg.twu.net/AGDA/Logic1.agda.html
--   http://angg.twu.net/AGDA/Logic1.agda
--           (find-angg "AGDA/Logic1.agda")
-- Author: Eduardo Ochs <eduardoochs@gmail.com>
-- Version: 20220101
-- Public domain.
--
-- ;; (find-angg "AGDA/find-agdatype.el")
-- (load       "~/AGDA/find-agdatype.el")
--
-- (find-eev "eev-pdflike.el" "change-default-viewer")
-- (defalias 'find-pdf-page 'find-pdftoolsr-page)
-- (defalias 'find-pdf-page 'find-xpdf-page)
--
-- (defun a () (interactive) (find-angg "AGDA/Logic1.agda"))

-- «.simple-1-2»	(to "simple-1-2")
-- «.distrib-1»		(to "distrib-1")

-- Based on: (find-agdagitfile "examples/lib/Logic/Base.agda")
-- (favp 34 "comma-categories")
-- (favp 35 "comma-categories" "witness")
-- (fava    "comma-categories" "witness")

module Logic1 where


infix 60 ¬_
infix 30 _∧_
infix 20 _∨_

-- And:
--
data _∧_ (P Q : Set) : Set where
  pair : P → Q → P ∧ Q

proj1 : {P Q : Set} → (P ∧ Q) → P
proj1 {P} {Q} (pair <P> <Q>) = <P>
proj2 : {P Q : Set} → (P ∧ Q) → Q
proj2 {P} {Q} (pair <P> <Q>) = <Q>

-- True:
--
data True : Set where
  tt : True

-- Or:
--
data _∨_ (P Q : Set) : Set where
  ∨-IL : P → P ∨ Q
  ∨-IR : Q → P ∨ Q

inL : {P Q : Set} → P → (P ∨ Q)
inL {P} {Q} <P> = ∨-IL <P>
inR : {P Q : Set} → Q → (P ∨ Q)
inR {P} {Q} <Q> = ∨-IR <Q>

[,] : {P Q R : Set} → (P → R) → (Q → R) → (P ∨ Q → R)
[,] {P} {Q} {R} <P→R> <Q→R> (∨-IL <P>) = <P→R> <P>
[,] {P} {Q} {R} <P→R> <Q→R> (∨-IR <Q>) = <Q→R> <Q>

-- False:
--
data False : Set where

elim-False : {A : Set} → False → A
elim-False ()

-- Not:
--
¬_ : Set → Set
¬ P = P → False

-- Biimplication:
-- ?

-- Exists:
--
data ∃ {A : Set} (P : A → Set) : Set where
  ∃-I : (a : A) → P a → ∃ P

-- Forall:
--
∏ : {A : Set} (P : A → Set) → Set
∏ {A} P = (a : A) → P a

-- (find-angg ".emacs.agda" "plfa9")
-- (find-angg ".emacs.agda" "plfa9" "Quantifiers")
-- (find-plfa9page)
-- (find-plfa9text)


--------------------/


-- «simple-1-2»  (to ".simple-1-2")
-- (al1p 1 "simple")
-- (al1a   "simple")
-- (set-frame-font "Inconsolata 16")
-- (set-frame-font "Monospace 12")




simple1 : {P Q R : Set} → (P ∧ Q) → (Q → R) → (P ∧ R)
simple1 {P} {Q} {R} <P∧Q> <Q→R> = <P∧R>
  where
    <P> : P
    <P> = proj1 <P∧Q>
    <Q> : Q
    <Q> = proj2 <P∧Q>
    <R> : R
    <R> = <Q→R> <Q>
    <P∧R> : P ∧ R
    <P∧R> = pair <P> <R>

simple2 : {P Q R : Set} → (Q → R) → (P ∧ Q → P ∧ R)
simple2  {P} {Q} {R} <Q→R>     <P∧Q> = <P∧R>
-- i.e., {P} {Q} {R} <Q→R> = λ <P∧Q> → <P∧R>
  where
    <P> : P
    <P> = proj1 <P∧Q>
    <Q> : Q
    <Q> = proj2 <P∧Q>
    <R> : R
    <R> = <Q→R> <Q>
    <P∧R> : P ∧ R
    <P∧R> = pair <P> <R>


-- «distrib-1»  (to ".distrib-1")
-- (al1p 2 "distributivity1")
-- (al1a   "distributivity1")
-- (set-frame-font "Monospace 12")

distrib1 : {P Q R : Set} → (P ∧ R ∨ Q ∧ R) → ((P ∨ Q) ∧ R)
distrib1 {P} {Q} {R} <P∧R∨Q∧R> = <[P∨Q]∧R>
  where
    <[P∧R]→[P∨Q]∧R]> : (P ∧ R) → ((P ∨ Q) ∧ R)
    <[P∧R]→[P∨Q]∧R]> <P∧R> = <[P∨Q]∧R>1
      where
        <P>        : P
        <P>        = proj1 <P∧R>
        <P∨Q>      : P ∨ Q
        <P∨Q>      = inL {P} {Q} <P>
        <R>        : R
        <R>        = proj2 <P∧R>
        <[P∨Q]∧R>1 : (P ∨ Q) ∧ R
        <[P∨Q]∧R>1 = pair <P∨Q> <R>

    <[Q∧R]→[P∨Q]∧R]> : (Q ∧ R) → ((P ∨ Q) ∧ R)
    <[Q∧R]→[P∨Q]∧R]> <Q∧R> = <[P∨Q]∧R>1
      where
        <Q>        : Q
        <Q>        = proj1 <Q∧R>
        <P∨Q>      : P ∨ Q
        <P∨Q>      = inR {P} {Q} <Q>
        <R>        : R
        <R>        = proj2 <Q∧R>
        <[P∨Q]∧R>1 : (P ∨ Q) ∧ R
        <[P∨Q]∧R>1 = pair <P∨Q> <R>

    <[P∧R∨Q∧R]→[P∨Q]∧R]> : (P ∧ R ∨ Q ∧ R) → ((P ∨ Q) ∧ R)
    <[P∧R∨Q∧R]→[P∨Q]∧R]> = [,] <[P∧R]→[P∨Q]∧R]>
                               <[Q∧R]→[P∨Q]∧R]>

    <[P∨Q]∧R> : (P ∨ Q) ∧ R
    <[P∨Q]∧R> = <[P∧R∨Q∧R]→[P∨Q]∧R]> <P∧R∨Q∧R>



-- postulate
--   ∀-distrib-× : ∀ {A : Set} {P Q : A → Set} →
--     (∀ (a : A) → P a × Q a) ≃ (∀ (a : A) → P a) × (∀ (a : A) → Q a)

-- (find-plfafile "src/plfa/part1/Quantifiers.lagda.md" "Exercise `∀-distrib-×`")
-- (find-plfa9page 3 "Exercise -distrib-")
-- (find-plfa9text 3 "Exercise -distrib-")

∀∧→∧∀ : {A : Set} {P Q : A → Set}
        → (∀ (a : A) → P a  ∧              Q a)
        → (∀ (a : A) → P a) ∧ (∀ (a : A) → Q a)
∀∧→∧∀ {A} {P} {Q} <∀a⇒Pa∧Qa> = pair <∀a⇒Pa> <∀a⇒Qa>
  where
    <∀a⇒Pa> : ∀ (a : A) → P a
    <∀a⇒Pa> a = proj1 (<∀a⇒Pa∧Qa> a)
    <∀a⇒Qa> : ∀ (a : A) → Q a
    <∀a⇒Qa> a = proj2 (<∀a⇒Pa∧Qa> a)

∧∀→∀∧ : {A : Set} {P Q : A → Set}
        → (∀ (a : A) → P a) ∧ (∀ (a : A) → Q a)
        → (∀ (a : A) → P a  ∧              Q a)
∧∀→∀∧ {A} {P} {Q} (pair <∀a⇒Pa> <∀a⇒Qa>) = <∀a⇒Pa∧Qa>
  where
    <∀a⇒Pa∧Qa> : (∀ (a : A) → P a ∧ Q a)
    <∀a⇒Pa∧Qa> a = pair (<∀a⇒Pa> a) (<∀a⇒Qa> a)



{-
-- (find-es "agda" "agda-user-manual")
-- (find-efunctiondescr 'agda2-mode)

* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
export LC_ALL=en_GB.UTF-8
agda -v 2 Logic1.agda  | tee /tmp/o

* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
rm -Rv ~/AGDA/HTML/
mkdir  ~/AGDA/HTML/
cd     ~/AGDA/HTML/
cd ~/AGDA/
agda --html --html-dir=HTML/ Logic1.agda

# (find-fline "~/AGDA/HTML/")



# (find-es "agda" "loading-process")

stack exec --       agda --compile Logic1.agda
./Logic1
                    agda --compile Logic1.agda
agda --ghc-dont-call-ghc --compile Logic1.agda

agda  --help
stack --help
# agda -i. -i/usr/share/agda-stdlib --interactive Logic1.agda
# :load Logic1.agda
# :?
# (find-es "agda" "generating-latex")
# (find-agdausermanualpage (+ 4 194) "4.6 Generating HTML")
# (find-agdausermanualtext (+ 4 194) "4.6 Generating HTML")
# (find-agdausermanualpage (+ 4 195) "4.7 Generating LaTeX")
# (find-agdausermanualtext (+ 4 195) "4.7 Generating LaTeX")
# (find-agdausermanualpage (+ 4 95) "3.19.3 Literate Agda")
# (find-agdausermanualtext (+ 4 95) "3.19.3 Literate Agda")


-}



-- Local Variables:
-- coding:  utf-8-unix
-- End: