|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
-- This file:
-- http://angg.twu.net/IDRIS/Logic.idr.html
-- http://angg.twu.net/IDRIS/Logic.idr
-- (find-angg "IDRIS/Logic.idr")
-- Version: 2019nov19
-- "PH1" is this paper:
-- http://angg.twu.net/math-b.html#zhas-for-children-2
-- http://angg.twu.net/LATEX/2017planar-has-1.pdf
-- "PH2" is this draft - the (jop ...) links point to it:
-- http://angg.twu.net/LATEX/2019J-ops.pdf
--
-- (find-idrisdoccpage (+ 1 16) "\\x => val")
-- (find-idrisdocctext (+ 1 16) "\\x => val")
-- (find-idrisdoccpage (+ 1 19) "let bindings")
-- (find-idrisdocctext (+ 1 19) "let bindings")
-- (find-idrisdoccpage (+ 1 134) "5 Theorem Proving")
--
-- The convention here is that, for example, _P:Type and __P:_P, i.e.,
-- the prefix "_" means "the space of proofs of" and
-- the prefix "__" means "a proof of"...
-- «.ph1-page-22» (to "ph1-page-22")
-- «.ph1-page-23» (to "ph1-page-23")
-- «.iff» (to "iff")
-- «.HAs-with-J-ops» (to "HAs-with-J-ops")
{-
-- «ph1-page-22» (to ".ph1-page-22")
-- This is a translation to Idris of this proof in page 22 of PH1:
-- (ph1p 22 "natural-deduction")
-- (ph1 "natural-deduction")
--
-- [P]^1 P->Q [P]^1 P->R
-- ----------- -----------
-- Q R
-- ---------------
-- Q&R
-- --------1
-- P->(Q&R)
--
-- ^ND-1
__PtoQ_PtoR_to_PtoQaR : (_P -> _Q) -> (_P -> _R) -> (_P -> Pair _Q _R)
__PtoQ_PtoR_to_PtoQaR __PtoQ __PtoR = \ __P => let
__Q = __PtoQ __P
__R = __PtoR __P
__QaR = (__Q, __R) in
__QaR
-- «ph1-page-23» (to ".ph1-page-23")
-- This is a translation of the proof in the middle of p.23 of PH1:
-- (ph1p 23 "natural-deduction" "^distr-weird-1")
-- (ph1 "natural-deduction" "^distr-weird-1")
--
-- (PvQ)&R (PvQ)&R
-- -------(&E_2) -------(&E_2)
-- [P]^1 R [Q]^1 R
-- ----------(&I) -----------(&I)
-- (PvQ)&R P&R Q&R
-- -------(&E_1) ------------(vI_1) -----------(vI_2)
-- PvQ (P&R)v(Q&R) (P&R)v(Q&R)
-- ----------------------------------------------(vE);1
-- (P&R)v(Q&R)
--
-- ^distr-weird-1
__PoQaR_to_PaRoQaR : (Pair (Either _P _Q) _R) -> (Either (Pair _P _R) (Pair _Q _R))
__PoQaR_to_PaRoQaR __PoQaR = let
__PoQ = fst __PoQaR
__R = snd __PoQaR
__P_to_PaRoQaR = \ __P => let
__PaR = (__P, __R)
__PaQoQvR_1 = Left __PaR in
__PaQoQvR_1
__Q_to_PaRoQaR = \ __Q => let
__QaR = (__Q, __R)
__PaQoQvR_2 = Right __QaR in
__PaQoQvR_2
__PoQ_to_PaRoQaR = either __P_to_PaRoQaR __Q_to_PaRoQaR
__PaRoQvR = __PoQ_to_PaRoQaR __PoQ in
__PaRoQvR
-}
{-
-- «iff» (to ".iff")
Iff : Type -> Type -> Type
Iff _P _Q = Pair (_P -> _Q) (_Q -> _P)
-}
{-
* (eepitch-to-buffer "*idris-repl*")
Nat -> Nat
(Nat -> Nat, Nat -> Nat)
Pair (Nat -> Nat) (Nat -> Nat)
Iff Nat Nat
(+ 1)
the (Nat -> Nat) (+ 1)
the (Iff Nat Nat) ((+ 1), (+ 2))
fst (the (Iff Nat Nat) ((+ 1), (+ 2)))
-}
-- «HAs-with-J-ops» (to ".HAs-with-J-ops")
-- (find-idrisgitfile "libs/contrib/Decidable/Order.idr" "interface Preorder")
-- (find-angg "IDRIS/Tut.idr" "records")
-- (find-idrisdoccpage (+ 1 17) "Records")
-- (find-idrisdocctext (+ 1 17) "Records")
record HAJ where
constructor MkHAJ
_H : Type
le : _H -> _H -> Type
refl : (p : _H) -> le p p
trans : {p, q, r : _H} -> le p q -> le q r -> le p r
antisym : {p, q : _H} -> le p q -> le q p -> p = q
top, bot : _H
and, or, imp : _H -> _H -> _H
--
ande1 : {p, q, r : _H} -> le p (and q r) -> le p q
ande2 : {p, q, r : _H} -> le p (and q r) -> le p r
andi : {p, q, r : _H} -> le p q -> le p r -> le p (and q r)
--
ore1 : {p, q, r : _H} -> le (or p q) r -> le p r
ore2 : {p, q, r : _H} -> le (or p q) r -> le q r
ori3 : {p, q, r : _H} -> le p r -> le q r -> le (or p q) r
--
impe : {p, q, r : _H} -> le p (imp q r) -> le (and p q) r
impi : {p, q, r : _H} -> le (and p q) r -> le p (imp q r)
--
_J : _H -> _H
_J1 : {p : _H} -> le p (_J p)
_J2 : {p : _H} -> (_J p) = (_J (_J p))
_J3 : {p, q : _H} -> and (_J p) (_J q) = _J (and p q)
-- (ph1 "logic-in-HAs")
-- (ph1p 18 "logic-in-HAs")
-- (ph1p 19 "logic-in-HAs" "...can be rewritten as tree rules as:")
-- http://angg.twu.net/LATEX/2017planar-has-1.pdf
--
-- P<=Q&R P<=Q&R P<=Q P<=R
-- ------ande1 ------ande2 -----------andi
-- P<=Q P<=R P<=Q&R
--
-- PvQ<=R PvQ<=R P<=R Q<=R
-- ------ore1 ------ore2 -----------ori
-- P<=R Q<=R PvQ<=R
--
-- P<=Q->R P&Q<=R
-- -------impe -------impi
-- P&Q<=R P<=Q->R
--
-- -----J1 ------J1 ------------J3
-- P<=P* P*=P** P*&Q*=(P&Q)*
-- "PH2" is this draft - the (jop ...) links point to it:
-- http://angg.twu.net/LATEX/2019J-ops.pdf
-- (jopp 6 "J-operators")
-- (jol "J-operators")
--
-- ------------refl
-- P*&Q*<=P*&Q*
-- ------------J3 ------------ande2
-- (P&Q)*=P*&Q* P*&Q*<=Q*
-- ---------------------------
-- (P&Q)*<=Q*
--
-- ^Mop
--
--
mop1 : {haj : HAJ} -> (p,q : _H haj) -> Nat
mop1 p q = let
plep = refl haj p
in 42
foo1 : (haj : HAJ) -> Type
foo1 haj = _H haj
foo2 : (haj : HAJ) -> (p,q,r : _H haj) -> Nat
foo2 haj p q r = 42
foo3 : (haj : HAJ) -> (p,q,r : _H haj) -> {pleq : le haj p q} -> Nat
foo3 haj p q r = 42
foo4 : {haj : HAJ} -> {p,q : _H haj} -> {pleq : le haj p q} -> Nat
foo4 = 42
-- foo1 h p q r = 42
-- foo1 HAJ -> Type
-- foor a = 42
{-
* (eepitch-to-buffer "*idris-repl*")
HAJ
MkHAJ
foo1
\haj : HAJ => 2
\haj : HAJ => le haj
\haj:HAJ => let h = _H haj in h
\haj:HAJ => let h = _H haj in h
-}
-- NOT YET!!!
-- After that I want to try to implement in Idris the Heyting Algebra
-- with J-operators described here, and translate to Idris some of the
-- proof trees in the paper - esp. the "Basic derived rules" in p.2...
--
-- http://angg.twu.net/LATEX/2019J-ops.pdf
-- I found an implementation in Idris of Heyting Algebras:
-- (find-es "idris" "idris-heyting-algebra")
-- but I don't know how reliable it is - see:
-- https://github.com/Risto-Stevcev/idris-heyting-algebra/issues/2
-- https://github.com/Risto-Stevcev/idris-heyting-algebra/issues/2#issuecomment-554748819
-- and it uses MANY features that I still don't understand.
-- Juan, do you have any idea on how to implement HAs and HAs with
-- J-operators in Idris in a more elementary way?
{-
* (eepitch-to-buffer "*idris-repl*")
woo Nat Int (2, -3)
-}