-- This file:
--   http://angg.twu.net/IDRIS/HAJ.idr.html
--   http://angg.twu.net/IDRIS/HAJ.idr
--           (find-angg "IDRIS/HAJ.idr")
-- Author: Eduardo Ochs <eduardoochs@gmail.com>
--
-- An implementation in Idris of the Heyting Algebras with
-- J-operators of these two papers:
--   (find-math-b-links "zhas-for-children-2" "2017planar-has-1")
--   (find-math-b-links "zhas-for-children-2" "2020J-ops-new")
--   (find-pdf-page "~/LATEX/2017planar-has-1.pdf")
--   (find-pdf-page "~/LATEX/2017planar-has-1.pdf" 20 "HAs: tree rules")
--   (find-pdf-page "~/LATEX/2017planar-has-1.pdf" 22 "HAs: intros and elims")
--   (find-pdf-page "~/LATEX/2020J-ops-new.pdf")
--   (find-pdf-page "~/LATEX/2020J-ops-new.pdf" 8 "J-ops: J1, J2, J3")
--   (find-pdf-page "~/LATEX/2020J-ops-new.pdf" 9 "J-ops: basic derived rules")
--   http://angg.twu.net/LATEX/2017planar-has-1.pdf#page=20
--   http://angg.twu.net/LATEX/2017planar-has-1.pdf#page=22
--   http://angg.twu.net/LATEX/2020J-ops-new.pdf#page=8
--   http://angg.twu.net/LATEX/2020J-ops-new.pdf#page=9
--   http://angg.twu.net/math-b.html#zhas-for-children-2
--
-- Date: 2020dec22
-- Status: ex-broken

record HAJ where
  constructor MkHAJ
  o_H : Type
  le : o_H -> o_H -> Type
  refl : (p : o_H) -> le p p
  trans : {p, q, r : o_H} -> le p q -> le q r -> le p r
  antisym : {p, q : o_H} -> le p q -> le q p -> p = q
  top, bot : o_H
  and, or, imp : o_H -> o_H -> o_H
  --
  ande1 : {p, q, r : o_H} -> le p (and q r) -> le p q
  ande2 : {p, q, r : o_H} -> le p (and q r) -> le p r
  andi  : {p, q, r : o_H} -> le p q -> le p r -> le p (and q r)
  --
  ore1 : {p, q, r : o_H} -> le (or p q) r -> le p r
  ore2 : {p, q, r : o_H} -> le (or p q) r -> le q r
  ori3 : {p, q, r : o_H} -> le p r -> le q r -> le (or p q) r
  --
  impe : {p, q, r : o_H} -> le p (imp q r) -> le (and p q) r
  impi : {p, q, r : o_H} -> le (and p q) r -> le p (imp q r)
  --
  o_J : o_H -> o_H
  o_J1 : {p : o_H} -> le p (o_J p)
  o_J2 : {p : o_H} -> (o_J p) = (o_J (o_J p))
  o_J3 : {p, q : o_H} -> and (o_J p) (o_J q) = o_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)*


myHAJ : HAJ
tv_P      : o_H myHAJ
tv_Q      : o_H myHAJ
tv_PandQ  : myHAJ.and tv_P tv_Q
prf_PandQ : tv_PandQ


-- (find-eepitch-intro "3. Test blocks")
--
{-
* (eepitch-shell2)
* (eepitch-kill)
* (eepitch-shell2)
idris2 HAJ.idr
:r

:t tv_P
:t tv_Q
:t myHAJ.and


:t myP
:t HAJ.and
:t HAJ.and myHAJ
:t HAJ.and myHAJ myP myQ
:t HAJ.and {myHAJ}

:t myp
:t and myp myq
:t and
:t HAJ.and
:t HAJ.and myp myq
and myhaj
and myhaj myp myq
:t and myhaj myp myq


:r
:?

-- Error:
-- 1/1: Building HAJ (HAJ.idr)
-- HAJ.idr:28:3--28:3:Parse error: Expected end of input (next tokens:
-- [symbol _, identifier H, symbol :, identifier Type, identifier le,
-- symbol :, symbol _, identifier H, symbol ->, symbol _])

-}
{-
-- This file compiles without errors in Idris 1.3.2...
-- Test:

* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
idris HAJ.idr
:t myhaj
:t o_H myhaj
:r

-}