%{
==Atoms==
}%
atm : type.  %name atm P.
%block atm_blk : block {p : atm}.
%worlds (atm_blk) (atm).


%{
==S4 Modal Logic==
}%

%{
===Propositions===
}%
prop : type.   %name prop A.

atom : atm -> prop.
arr : prop -> prop -> prop.
box : prop -> prop.
dia : prop -> prop.

%worlds (atm_blk) (prop).


%{
===Judgments===
}%
conclusion : type.    %name conclusion J. 
conclusion/true : prop -> conclusion.
conclusion/poss : prop -> conclusion.

conc : conclusion -> type.    %name conc D.
%abbrev true : prop -> type = [a] conc (conclusion/true a).
%abbrev poss : prop -> type = [a] conc (conclusion/poss a).

local : (true A -> conc J) -> type.    %name local Dloc.

local/var : local ([x] x).
local/base : local ([x] D).

%{
}%
arrI : {D : true A -> true B} local D -> true (arr A B).

local/arrI : local ([x] arrI ([y] D x y) _)
	      <- ({y} local ([x] D x y)).


%{
}%
arrE : true (arr A B) -> true A -> true B.

local/arrE : local ([x] arrE (D1 x) (D2 x))
	      <- local([x] D1 x)
	      <- local ([x] D2 x).


%{
}%
boxI : true A -> true (box A).


%{
}%
boxE : true (box A) -> (true A -> conc J) -> conc J.

local/boxE : local ([x] boxE (D1 x) ([u] D2 x u))
	      <- local ([x] D1 x)
	      <- ({u} local ([x] D2 x u)).


%{
}%
possI : true A -> poss A.

local/possI : local ([x] possI (D x))
	       <- local ([x] D x).


%{
}%
diaI : poss A -> true (dia A).

local/diaI : local ([x] diaI (D x))
	      <- local ([x] D x).


%{
}%
diaE : true (dia A) -> {D : true A -> poss C} local D -> poss C.

local/diaE : local ([x] diaE (D1 x) ([y] D2 y) _)
	      <- local ([x] D1 x).


%{
}%
%block true_blk : some {A : prop} block {x : true A}.
%worlds (atm_blk | true_blk) (conc _) (local _).





%{
==Lax Logic==
}%

%{
===Propositions===
}%
lprop : type.

latom : atm -> lprop.
larr : lprop -> lprop -> lprop.
lcirc : lprop -> lprop.

%worlds (atm_blk) (lprop).


%{
===Judgments===
}%
lconclusion : type.
lconclusion/ltrue : lprop -> lconclusion.
lconclusion/llax : lprop -> lconclusion.

lconc : lconclusion -> type.
%abbrev ltrue : lprop -> type = [a] lconc (lconclusion/ltrue a).  %% If I remove these, I get definition violation.
%abbrev llax : lprop -> type = [a] lconc (lconclusion/llax a).

%{
}%
larrI : (ltrue A -> ltrue B) -> ltrue (larr A B).
larrE : ltrue (larr A B) -> ltrue A -> ltrue B.
llaxI : ltrue A -> llax A.
lcircI : llax A -> ltrue (lcirc A).
lcircE : ltrue (lcirc A) -> (ltrue A -> llax C) -> llax C.

%{
}%
%block ltrue_blk : some {A : lprop} block {x : ltrue A}.
%worlds (atm_blk | ltrue_blk) (lconc _).




%{
==Translation from lax logic to S4==
}%



trans-lprop : lprop -> prop -> type.
%mode trans-lprop +A' -A.

trans-lprop/latom : trans-lprop (latom P) (atom P).

trans-lprop/larr : trans-lprop (larr A' B') (arr (box A) B)
		    <- trans-lprop A' A
		    <- trans-lprop B' B.

trans-lprop/lcirc : trans-lprop (lcirc A') (dia (box A))
		     <- trans-lprop A' A.

%worlds (atm_blk) (trans-lprop _ _).
%total A' (trans-lprop A' _).



can-trans-lprop : {A' : lprop} trans-lprop A' A -> type.
%mode can-trans-lprop +A' -D.

- : can-trans-lprop (latom P) trans-lprop/latom.

- : can-trans-lprop (larr A' B') (trans-lprop/larr Db Da)
     <- can-trans-lprop A' (Da : trans-lprop A' A)
     <- can-trans-lprop B' (Db : trans-lprop B' B).

- : can-trans-lprop (lcirc A') (trans-lprop/lcirc Da)
     <- can-trans-lprop A' (Da : trans-lprop A' A).

%worlds (atm_blk) (can-trans-lprop _ _).
%total A' (can-trans-lprop A' _).


prop-eq : prop -> prop -> type.

prop-eq/refl : prop-eq A A.

%worlds (atm_blk) (prop-eq _ _).



arr-compat : prop-eq A A' -> prop-eq B B' -> prop-eq (arr A B) (arr A' B') -> type.
%mode arr-compat +Eqa +Eqb -Eqab.

- : arr-compat prop-eq/refl prop-eq/refl prop-eq/refl.

%worlds (atm_blk) (arr-compat _ _ _).
%total {} (arr-compat _ _ _).


box-compat : prop-eq A A' -> prop-eq (box A) (box A') -> type.
%mode box-compat +Eqa -Eqba.

- : box-compat prop-eq/refl prop-eq/refl.

%worlds (atm_blk) (box-compat _ _).
%total {} (box-compat _ _).


dia-compat : prop-eq A A' -> prop-eq (dia A) (dia A') -> type.
%mode dia-compat +Eqa -Eqda.

- : dia-compat prop-eq/refl prop-eq/refl.

%worlds (atm_blk) (dia-compat _ _). 
%total {} (dia-compat _ _).







true-resp : true A -> prop-eq A A' -> true A' -> type.
%mode true-resp +D +Eq -E.

- : true-resp D prop-eq/refl D.

%worlds (atm_blk | true_blk) (true-resp _ _ _).
%total {} (true-resp _ _ _). 


trans-lprop-unique : trans-lprop A' A1 -> trans-lprop A' A2 -> prop-eq A1 A2 -> type.
%mode trans-lprop-unique +D1 +D2 -Eq. 

- : trans-lprop-unique trans-lprop/latom trans-lprop/latom prop-eq/refl.

- : trans-lprop-unique
     (trans-lprop/larr 
	(Db : trans-lprop B' B1)
	(Da : trans-lprop A' A1))
     (trans-lprop/larr
	(Db' : trans-lprop B' B2)
	(Da' : trans-lprop A' A2))
     Eqbab
     <- trans-lprop-unique Da Da' (Eqa : prop-eq A1 A2)
     <- trans-lprop-unique Db Db' (Eqb : prop-eq B1 B2)
     <- box-compat Eqa (Eqba : prop-eq (box A1) (box A2))
     <- arr-compat Eqba Eqb (Eqbab : prop-eq (arr (box A1) B1) (arr (box A2) B2)).

- : trans-lprop-unique 
     (trans-lprop/lcirc 
	(Da : trans-lprop A' A1))
     (trans-lprop/lcirc 
	(Da' : trans-lprop A' A2))
     Eqdba
     <- trans-lprop-unique Da Da' (Eqa : prop-eq A1 A2)
     <- box-compat Eqa (Eqba : prop-eq (box A1) (box A2))
     <- dia-compat Eqba (Eqdba : prop-eq (dia (box A1)) (dia (box A2))).

%worlds (atm_blk) (trans-lprop-unique _ _ _).
%total D1 (trans-lprop-unique D1 _ _).



trans-ltrue+ : ltrue A' -> trans-lprop A' A -> true A -> type.
%mode trans-ltrue+ +D +E -F.
trans-ltrue- : ltrue A' -> trans-lprop A' A -> true A -> type.
%mode trans-ltrue- +D -E -F. 
trans-llax : llax A' -> trans-lprop A' A -> poss (box A) -> type. 
%mode trans-llax +D -E -F.

- : trans-ltrue+ 
     (D : ltrue A')
     (Ea : trans-lprop A' A1)
     F'
     <- trans-ltrue- D (Ea' : trans-lprop A' A2) (F : true A2)
     <- trans-lprop-unique Ea' Ea (Eqa : prop-eq A2 A1)
     <- true-resp F Eqa (F' : true A1).

- : trans-ltrue- 
     (larrI ([x' : ltrue A'] D x' : ltrue B')) 
     (trans-lprop/larr Eb Ea) 
     (arrI
	([x] boxE x ([u] F u)) 
	(local/boxE ([u] local/base) local/var))
     <- can-trans-lprop A' (Ea : trans-lprop A' A)
     <- ({x' : ltrue A'} {u : true A} trans-ltrue- x' Ea u
	   -> trans-ltrue- (D x') (Eb : trans-lprop B' B) (F u : true B)).

- : trans-ltrue- 
     (larrE 
	(D1 : ltrue (larr A' B'))
	(D2 : ltrue A'))
     Eb
     (arrE F1 (boxI F2))
     <- trans-ltrue- D1 (trans-lprop/larr (Eb : trans-lprop B' B) (Ea : trans-lprop A' A)) (F1 : true (arr (box A) B))
     <- trans-ltrue+ D2 Ea (F2 : true A).

- : trans-ltrue- 
     (lcircI (D : llax A'))
     (trans-lprop/lcirc Ea) 
     (diaI F)
     <- trans-llax D (Ea : trans-lprop A' A) (F : poss (box A)).

- : trans-llax 
     (llaxI (D : ltrue A'))
     Ea
     (possI (boxI F))
     <- trans-ltrue- D (Ea : trans-lprop A' A) (F : true A).

- : trans-llax 
     (lcircE 
	(D1 : ltrue (lcirc A'))
	([x' : ltrue A'] D2 x' : llax C'))
     Ec 
     (diaE 
	F1
	([x] boxE x ([u] F2 u)) 
	(local/boxE ([u] local/base) local/var)) 
     <- trans-ltrue- D1 (trans-lprop/lcirc (Ea : trans-lprop A' A)) (F1 : true (dia (box A)))
     <- ({x' : ltrue A'} {u : true A} trans-ltrue- x' Ea u 
	   -> trans-llax (D2 x') (Ec : trans-lprop C' C) (F2 u : poss (box C))).

%block trans-ltrue-_blk : some {A' : lprop} {A : prop} {Ea : trans-lprop A' A}
			  block {x' : ltrue A'} {u : true A} {trans-ltrue-/x' : trans-ltrue- x' Ea u}.
%worlds (atm_blk | trans-ltrue-_blk) (trans-ltrue- _ _ _) (trans-llax _ _ _) (trans-ltrue+ _ _ _). 
%total (D1 D2 D3) (trans-ltrue- D1 _ _) (trans-llax D2 _ _) (trans-ltrue+ D3 _ _).








%{
==Translation from S4 to lax logic==
}%




trans-prop : prop -> lprop -> type.
%mode trans-prop +A -A'.

trans-prop/atom : trans-prop (atom P) (latom P).
trans-prop/arr : trans-prop (arr A B) (larr A' B')
		  <- trans-prop A A'
		  <- trans-prop B B'.
trans-prop/box : trans-prop (box A) A'
		  <- trans-prop A A'.
trans-prop/dia : trans-prop (dia A) (lcirc A')
		  <- trans-prop A A'.

%worlds (atm_blk) (trans-prop _ _).
%total A (trans-prop A _).


can-trans-prop : {A} trans-prop A A' -> type.
%mode can-trans-prop +A -D.

- : can-trans-prop (atom P) trans-prop/atom.

- : can-trans-prop (arr A B) (trans-prop/arr Db Da)
     <- can-trans-prop A Da
     <- can-trans-prop B Db.

- : can-trans-prop (box A) (trans-prop/box Da)
     <- can-trans-prop A Da.

- : can-trans-prop (dia A) (trans-prop/dia Da)
     <- can-trans-prop A Da.

%worlds (atm_blk) (can-trans-prop _ _).
%total A (can-trans-prop A _).


lprop-eq : lprop -> lprop -> type.

lprop-eq/refl : lprop-eq A A.

%worlds (atm_blk) (lprop-eq _ _).


larr-compat : lprop-eq A A' -> lprop-eq B B' -> lprop-eq (larr A B) (larr A' B') -> type.
%mode larr-compat +Da +Db -Dab.

- : larr-compat lprop-eq/refl lprop-eq/refl lprop-eq/refl.

%worlds (atm_blk) (larr-compat _ _ _).
%total {} (larr-compat _ _ _).


lcirc-compat : lprop-eq A A' -> lprop-eq (lcirc A) (lcirc A') -> type.
%mode lcirc-compat +Da -Dca.

- : lcirc-compat lprop-eq/refl lprop-eq/refl. 

%worlds (atm_blk) (lcirc-compat _ _).
%total {} (lcirc-compat _ _).







ltrue-resp : ltrue A -> lprop-eq A A' -> ltrue A' -> type.
%mode ltrue-resp +D +E -F.

- : ltrue-resp D lprop-eq/refl D.

%worlds (atm_blk | ltrue_blk) (ltrue-resp _ _ _).
%total {} (ltrue-resp _ _ _).



trans-prop-unique : trans-prop A A' -> trans-prop A A'' -> lprop-eq A' A'' -> type.
%mode trans-prop-unique +D1 +D2 -E.

- : trans-prop-unique trans-prop/atom trans-prop/atom lprop-eq/refl.

- : trans-prop-unique (trans-prop/arr Db Da) (trans-prop/arr Eb Ea) Eqab
     <- trans-prop-unique Da Ea Eqa
     <- trans-prop-unique Db Eb Eqb
     <- larr-compat Eqa Eqb Eqab. 

- : trans-prop-unique (trans-prop/box Da) (trans-prop/box Ea) Eqa 
     <- trans-prop-unique Da Ea Eqa.

- : trans-prop-unique (trans-prop/dia Da) (trans-prop/dia Ea) Eqca
     <- trans-prop-unique Da Ea Eqa
     <- lcirc-compat Eqa Eqca.

%worlds (atm_blk) (trans-prop-unique _ _ _).
%total D1 (trans-prop-unique D1 _ _).


trans-true+ : true A -> trans-prop A A' -> ltrue A' -> type.
%mode trans-true+ +D +E -F.
trans-true- : true A -> trans-prop A A' -> ltrue A' -> type.
%mode trans-true- +D -E -F.
trans-poss : poss A -> trans-prop A A' -> llax A' -> type.
%mode trans-poss +D -E -F.

- : trans-true+ D Ea F'
     <- trans-true- D (Ea' : trans-prop A A'') (F : ltrue A'')
     <- trans-prop-unique Ea' Ea Eqa
     <- ltrue-resp F Eqa F'.

- : trans-true- (arrI ([x] D x) _) (trans-prop/arr Eb Ea) (larrI ([x'] F x'))
     <- can-trans-prop _ Ea 
     <- ({x} {x'} trans-true- x Ea x' -> trans-true- (D x) Eb (F x')). 

- : trans-true- 
     (arrE 
	(D1 : true (arr A B))
	(D2 : true A)) 
     Eb
     (larrE 
	(F1 : ltrue (larr A' B'))
	(F2 : ltrue A'))
     <- trans-true- 
	D1
	(trans-prop/arr 
	   (Eb : trans-prop B B')
	   (Ea : trans-prop A A'))
	(F1 : ltrue (larr A' B'))
     <- trans-true+ 
	D2
	(Ea : trans-prop A A')
	(F2 : ltrue A').

- : trans-true- (boxI D) (trans-prop/box Ea) F
     <- trans-true- D Ea F.

- : trans-true- (boxE D1 ([u] D2 u)) Ec (F2 F1)
     <- trans-true- D1 (trans-prop/box Ea) F1
     <- ({u} {u'} trans-true- u Ea u' -> trans-true- (D2 u) Ec (F2 u')).

- : trans-true- (diaI D) (trans-prop/dia Ea) (lcircI F)
     <- trans-poss D Ea F.

- : trans-poss (possI D) Ea (llaxI F)
     <- trans-true- D Ea F.

- : trans-poss (boxE D1 ([u] D2 u)) Ec (F2 F1)
     <- trans-true- D1 (trans-prop/box Ea) F1
     <- ({u} {u'} trans-true- u Ea u' -> trans-poss (D2 u) Ec (F2 u')).

- : trans-poss (diaE D1 ([x] D2 x) _) Ec (lcircE F1 ([x'] F2 x'))
     <- trans-true- D1 (trans-prop/dia Ea) F1 
     <- ({x} {x'} trans-true- x Ea x' -> trans-poss (D2 x) Ec (F2 x')).

%block trans-true-_blk : some {A : prop} {A' : lprop} {Ea : trans-prop A A'} 
			block {x : true A} {x' : ltrue A'} {trans-true-/x : trans-true- x Ea x'}.
%worlds (atm_blk | trans-true-_blk) (trans-true+ _ _ _) (trans-true- _ _ _) (trans-poss _ _ _).
%total (D1 D2 D3) (trans-true- D1 _ _) (trans-poss D2 _ _) (trans-true+ D3 _ _).