CanonicalDedukti.lp

/* Canonical Dedukti in LambdaPi

   An encoding of (my interpretation of) "Canonical Dedukti" by Thiago Felicissimo in LambdaPi

   All credit goes to Thiago, all blame goes to me
   -- Jesper, 2022-10-19
*/

/* syntactic classes */

constant symbol dkClass : TYPE;


/* pre-terms (indexed by their syntactic class) */

injective symbol dkPreTerm : dkClass → TYPE;


/* pre-types (indexed by the syntactic class of their elements) */

constant symbol dkPreType : dkClass → TYPE;


/* bidirectional typing judgements */

constant symbol ⇒ : Π [a] (t : dkPreTerm a) (A : dkPreType a), TYPE;
constant symbol ⇐ : Π [a] (t : dkPreTerm a) (A : dkPreType a), TYPE;

notation ⇒ infix 5;
notation ⇐ infix 5;

constant symbol embed : Π [Aa] [A : dkPreType Aa] [t : dkPreTerm Aa], t ⇒ A → t ⇐ A;


/* Dedukti sorts (type or kind) */ 

constant symbol dkSort : TYPE;
constant symbol dkSortType : dkSort;
constant symbol dkSortKind : dkSort;

constant symbol hasSort : Π [Aa], dkPreType Aa → dkSort → TYPE;


/* Type kind */

constant symbol dkTy          : dkClass;
constant symbol dkType        : dkPreType dkTy;
constant symbol hasSortDkType : hasSort dkType dkSortKind;

symbol dkErase        : dkPreTerm dkTy → dkClass;
injective symbol dkEl : Π (t : dkPreTerm dkTy), dkPreType (dkErase t);
constant symbol hasSortSort : Π [A], A ⇒ dkType → hasSort (dkEl A) dkSortType;


/* pi type */ 

constant symbol →c : dkClass → dkClass → dkClass;
notation →c infix right 20;
rule dkPreTerm ($a →c $b) ↪ dkPreTerm $a → dkPreTerm $b;

constant symbol dkPi : Π [Aa], Π A : dkPreType Aa,
                       Π [Ba], Π (B : dkPreTerm Aa → dkPreType Ba),
                       dkPreType (Aa →c Ba);

constant symbol hasSortDkPi : 
  Π [Aa Ba s] [A : dkPreType Aa] [B : dkPreTerm Aa → dkPreType Ba],
  hasSort A dkSortType →
  (Π [x], x ⇒ A → hasSort (B x) s) → 
  hasSort (dkPi A B) s;
constant symbol inferDkApp : 
  Π [Aa Ba] [A : dkPreType Aa] [B : dkPreTerm Aa → dkPreType Ba] 
    [t : dkPreTerm (Aa →c Ba)] [u : dkPreTerm Aa],
  t ⇒ dkPi A B → 
  u ⇐ A →
  t u ⇒ B u;
symbol checkDkAbs : 
  Π [Aa Ba] [A : dkPreType Aa] [B : dkPreTerm Aa → dkPreType Ba] 
    [t : dkPreTerm (Aa →c Ba)],
    (Π [x], x ⇒ A → t x ⇐ B x) →
    (λ x, t x) ⇐ dkPi A B;


/* example: a small language with Pi, Sigma, Bool, and So */

constant symbol tm : dkClass;
constant symbol ty : dkClass;

symbol Type : dkPreTerm dkTy;
rule dkErase Type ↪ dkTy;
constant symbol inferType : Type ⇒ dkType;

injective symbol ∙ : dkPreTerm (ty →c dkTy);
rule dkErase (∙ $A) ↪ tm;
constant symbol infer∙ : Π A, ∙ A ⇒ dkType;

injective symbol Pi    : dkPreTerm (ty →c (tm →c ty) →c ty);
injective symbol Sigma : dkPreTerm (ty →c (tm →c ty) →c ty);
constant  symbol Bool  : dkPreTerm ty;
injective symbol So    : dkPreTerm (tm →c ty);

symbol lam  : dkPreTerm ((tm →c tm) →c tm);
symbol app  : dkPreTerm (tm →c tm →c tm);
symbol pair : dkPreTerm (tm →c tm →c tm);
symbol fst  : dkPreTerm (tm →c tm);
symbol snd  : dkPreTerm (tm →c tm);
symbol tru  : dkPreTerm tm;
symbol fls  : dkPreTerm tm;
symbol ite  : dkPreTerm (tm →c tm →c tm →c tm);
symbol oh   : dkPreTerm tm;

rule app (lam $u) $v ↪ $u $v;
rule fst (pair $u $v) ↪ $u;
rule snd (pair $u $v) ↪ $v;
rule ite tru $u $v ↪ $u;
rule ite fls $u $v ↪ $v;

symbol inferPi    : Π A B, ∙ (Pi A B) ⇒ dkEl Type;
symbol inferSigma : Π A B, ∙ (Sigma A B) ⇒ dkEl Type; 
symbol inferBool  : ∙ Bool ⇒ dkEl Type;
symbol inferSo    : Π b, (b ⇒ dkEl (∙ Bool)) → ∙ (So b) ⇒ dkEl Type; 

symbol checkLam : 
  Π [A : dkPreTerm ty] [B : dkPreTerm (tm →c ty)] [u : dkPreTerm (tm →c tm)],
  (Π [x], x ⇒ (dkEl (∙ A)) → u x ⇐ dkEl (∙ (B x))) → 
  lam u ⇐ dkEl (∙ (Pi A B));
symbol inferApp : 
  Π [A : dkPreTerm ty] [B : dkPreTerm (tm →c ty)] [u v : dkPreTerm tm],
  u ⇒ dkEl (∙ (Pi A B)) →
  v ⇐ dkEl (∙ A) → 
  app u v ⇒ dkEl (∙ (B u));

symbol checkPair : Π [A B u v],
  u ⇐ dkEl (∙ A) →
  v ⇐ dkEl (∙ (B u)) → 
  pair u v ⇐ dkEl (∙ (Sigma A B));
symbol inferFst : Π [A B u],
  u ⇒ dkEl (∙ (Sigma A B)) →
  fst u ⇒ dkEl (∙ A);
symbol inferSnd : Π [A B u],
  u ⇒ dkEl (∙ (Sigma A B)) →
  snd u ⇒ dkEl (∙ (B (fst u)));

symbol inferTru : tru ⇒ dkEl (∙ Bool);
symbol inferFls : fls ⇒ dkEl (∙ Bool);

symbol checkIte : Π [A b u v],
  b ⇐ dkEl (∙ Bool) →
  u ⇐ dkEl (∙ A) →
  v ⇐ dkEl (∙ A) →
  ite b u v ⇐ dkEl (∙ A);

symbol inferOh : oh ⇒ dkEl (∙ (So tru));

symbol example_id : Π [A], lam (λ x, x) ⇐ dkEl (∙ (Pi A (λ _, A)))
  ≔ λ _, checkLam (λ _ x, embed x);

symbol not : dkPreTerm tm ≔ lam (λ b, ite b fls tru);

symbol example_not : not ⇐ dkEl (∙ (Pi Bool (λ _, Bool)))
  ≔ checkLam (λ _ b, checkIte (embed b) (embed inferFls) (embed (inferTru)));

symbol example_So_not_false : oh ⇒ dkEl (∙ (So (app not fls)))
  ≔ inferOh; 

/*

Further things to try:

- Extend the example with universes
- Allow the symbols Type and ∙ to be a pretype instead of a preterm
- Separate preterms into checkable and inferable syntax (⇒ make embed implicit)

*/