namespace http://cds.omdoc.org/urtheories❚

/T LLF_P as introduced by Honsell, Liquori, Maksimovi, Scagnetto in
A logical framework for modeling external evidence, side conditions, and proof irrelevance using monads❚

import rules scala://externals.lf.mmt.kwarc.info❚
import lfrules scala://lf.mmt.kwarc.info❚

theory Locks =
   // Lp p a b <T> is the type \mathcal{L}^p_{a,b}[T] from the paper.❙
   locktype # Lp 1 2 3 < 4 > ❙
   // Lm p a b <t> is the term \mathcal{L}^p_{a,b}[t] from the paper.❙
   lockterm # Lm 1 2 3 < 4 > ❙
   // U <t> for t:Lp p a b <T> is the term \mathcal{U}^p_{a,b}[t] from the paper.
      U is unary here because p, a, and b can be inferred from t.❙
   unlock # U < 1 > ❙                                           
   
   // Convenience operator to bundle p, a, b into a single object.
   key # K 1 2 3❙

   // The typing rules.❙
   rule rules?InferLockType❙
   rule rules?InferLockTerm❙
   rule rules?InferUnlock❙
   rule rules?TypingLock❙
   rule rules?EqualityLock❙
   rule rules?UnlockLock❙
❚

theory LLFP =
   include ?LF❙
   include ?Locks❙
❚

theory CallByValueExample : ?LLFP =
   /T following Section 5.1 of the paper: call-by-value reduction ❙

   /T untyped λ calculus ❙
   term : type❙
   app : term ⟶ term ⟶ term ❘ # 1 @ 2 prec 50❙
   lam : (term ⟶ term) ⟶ term❘ # λ 1❙

   /T natural numbers ❙
   nat : type❙
   z : nat❙
   S : nat ⟶ nat❙
   
   /T free variables using natural numbers❙
   free : nat ⟶ term❘# ' 1 prec 100❙

   /T equality judgment and its rules ❙
   eq : term ⟶ term ⟶ type❘ # 1 ≐ 2 ❘ role Judgment❙
   refl : {M} M ≐ M❘# refl 1❙
   symm : {M,N} M ≐ N ⟶ N ≐ M❙
   trans : {M,N,P} M ≐ N ⟶ N ≐ P ⟶ M ≐ P❙
   eq_app: {M,N,X,Y} M ≐ N ⟶ X ≐ Y ⟶ M@X ≐ N@Y❘ # eq_app 5 6❙

   /T We declare a single constant Val for the side condition and one rule that implements it.
      The condition Val N term checks if N:term is an abstraction or a free variable ❙
   Val❙
   rule rules?ValRule❙
   
   /T reduction rules using Val condition❙
   betav : {M,N} Lp Val N term <(λ M)@N ≐ (M N)>❘ # betav 1 2❙
   csiv : {M,N}({x} Lp Val x term <(M x) ≐ (N x)>) ⟶ (λ M) ≐ (λ N)❘ # csiv 3❙
   
   /T example from the end of the section ❙
   t1 = λ[x] 'z @ ((λ[y] y) @ x)❙
   t2 = λ[x] 'z @ x❙
   goal = t1 ≐ t2❙

   /T The following check succeeds without ever calling the ValRule because the unlock is under a lock.❙
   check: goal ❘
     = csiv [x] Lm Val x term <
       eq_app (refl 'z) U<betav ([y] y) x>
     >❙

   /T The following example does not guard the unlock but still succeeds because 'n is indeed a value.❙
   check2 = [n] eq_app (refl 'z) U<betav ([y] y) 'n>❙

   /T The following negative example fails because x is any term and thus not necessarily a value.❙
   // fail   = [x] eq_app (refl 'z) U<betav ([y] y) x>❙
❚

/T An alternative formulation that uses polymorphpic LF to define most of the typing rules in the logical framework.
   That corresponds to the Coq implementation of LLF_P by Honsell et al.❚
theory LLFP2 : ur:?PLF =
  PROP : type❙
  DED : PROP ⟶ type❙
  rule lfrules?TermIrrelevanceRule DED❙
  
  Lock : {p: PROP} (DED p ⟶ type) ⟶ type❘# L 1 2❙
  lock : {p: PROP} {a: DED p ⟶ type} ({p} a p) ⟶ L p a❘# l 1 3❙
  unlock : {p, a: DED p ⟶ type} L p a ⟶ {w:DED p} a w❘# U 3❙
❚

theory LinearLogic : ?LLFP2 =
  o : type❙
  ded : o ⟶ type❘# ded 1 prec -5❙
  
  linear: {a,b} (ded a ⟶ ded b) ⟶ PROP❘# linear 3❙  
  
  lolli : o ⟶ o ⟶ o❘# 1 ⊸ 2❙
  lolliI : {A,B} {p:ded A ⟶ ded B} L (linear p) [q] ded A ⊸ B❙
❚