Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
-- 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: