Algorithmic Equality in the Polymorphic $\lambda$-Calculus

poly-equal-min.lf

tp : type.
arr : {T1:tp}{T2:tp} tp.
all : {T:{ T':tp} tp} tp.
 
tm: type.
lam: {M: tm -> tm} tm.
tlam : {M: tp -> tm} tm.
app: {M1:tm}{M2:tm} tm.
tapp : {M:tm}{T:tp} tm.
 
 
atp : {T1:tp}{T2:tp} type.
aeq: {M1:tp}{M2:tp}  type.
 
atp_arr : {T1:tp}{T2:tp}{S1:tp}{S2:tp}
          {D1:atp T1 T2}
          {D2:atp S1 S2}
          atp (arr T1 S1) (arr T2 S2).
atp_all : {T1:{T1':tp} tp}{T2: {T2':tp} tp}
          {D: {T:tp} atp T T -> atp (T1 T) (T2 T)}
          atp (all ([x] T1 x)) (all ([x] T2 x)).
 
 
ae_a : {M1: tm}{M2: tm}{N1:tm}{N2:tm}
       {D1:aeq M1 N1}{D2:aeq M2 N2}
       aeq (app M1 M2) (app N1 N2).
ae_ta : {M1: tm}{M2: tm}{T1:tp}{T2:tp}
        {D1:aeq M1 M2}{D2:atp T1 T2}
        aeq (tapp M1 T1) (tapp M2 T2).
ae_l : {M: tm -> tm}{N: tm -> tm}
       {D: {z:tm} aeq z z -> aeq (M z) (N z)}
       aeq (lam ([x] M x)) (lam ([x] N x)).
ae_tl : {M: tp -> tm}{N: tp -> tm}
        {D: {z:tp} atp z z -> aeq (M z) (N z)}
        aeq (tlam ([x] M x)) (tlam ([x] N x)).

poly-equal.ath

Specification "poly-equal-min.lf".
 
Schema atpCtx := (t:tp, dt:atp t t).
 
Theorem reflTp : ctx G:atpCtx, forall T,
    {G |- T : tp} => exists D, {G |- D : atp T T}.
induction on 1. intros.
case H1. weaken H2 with atp n n. apply IH to H3 with (G = G, n1:tp, n:atp n1 n1).
exists atp_all T1 T1 D. search.
apply IH to H2. apply IH to H3.
exists atp_arr T1 T1 T2 T2 D D1. search.
exists n1. search.
 
% This schema is fine to use in place of atpCtx for G in reflTp 
Schema aeqCtx := (x:tm, dx:aeq x x);
                 (t:tp, dt:atp t t).
 
Theorem ref : ctx G:aeqCtx, forall M,
  {G |- M : tm} => exists D, {G |- D : aeq M M}.
induction on 1. intros.
case H1.
  apply reflTp to H3. abort.
  
 
% This schema is not fine to use in place of atpCtx for G in reflTp
% If we were to try and prove this in reflTp, the variable case would not be possible!
Schema aeqCtxErr:= (x:tm, dx:aeq x x);
                   (t:tp, dt:atp t t);
                   (t:tp).
 
 
Theorem ref : ctx G:aeqCtxErr, forall M,
  {G |- M : tm} => exists D, {G |- D : aeq M M}.
induction on 1. intros.
case H1.
  % Notice Adelfa reports an error here and does not update the state
  apply reflTp to H3.

LF tp : type =
  | arr : tp -> tp -> tp
  | all : (tp -> tp) -> tp
;
--name tp T a.

LF term: type =
  | app : term -> term -> term
  | lam : (term -> term) -> term
  | tlam: (tp -> term) -> term
  | tapp: term -> tp -> term
;
--name term M x.

LF atp: tp -> tp -> type =
  | at_al : ({a:tp} atp a a -> atp (T a) (S a)) -> atp (all T) (all S)
  | at_arr: atp T1 T2 -> atp S1 S2 -> atp (arr T1 S1) (arr T2 S2)
;
--name atp Q u.

LF aeq: term -> term -> type =
  | ae_a : aeq M1 N1 -> aeq M2 N2 -> aeq (app M1 M2) (app N1 N2)
  | ae_l : ({x:term} aeq x x -> aeq (M x) (N x)) -> aeq (lam (\x. M x)) (lam (\x. N x))
  | ae_tl: ({a:tp} atp a a -> aeq (M a) (N a)) -> aeq (tlam (\a. M a)) (tlam (\a. N a))
  | ae_ta : aeq M N -> atp T S -> aeq (tapp M T) (tapp N S)
;
--name aeq D u.

schema atpCtx = block a:tp , _t:atp a a;

schema aeqCtx    = block (x:term, _u:aeq x x) + block (a:tp, _t:atp a a);
schema aeqCtxErr = block (x:term, _u:aeq x x) + block (a:tp, _t:atp a a) + block (a:tp);

rec reftp : {gamma:atpCtx} {T:[gamma |- tp]} [gamma |- atp T T] =
mlam gamma => mlam T => case [gamma |- T] of
| [gamma |- #p.1] => [gamma |- #p.2]

| [gamma |- all \x. T] =>
  let [gamma, b:block a:tp , _t:atp a a |- D[.., b.1, b.2]] =
         reftp [gamma, b:block a:tp , _t:atp a a] [gamma, b |- T[.., b.1]]
  in
   [gamma |- at_al \x. \w. D]

| [gamma |- arr T S] =>
  let [gamma |- D1] = reftp [gamma] [gamma |- T] in
  let [gamma |- D2] = reftp [gamma] [gamma |- S] in
    [gamma |- at_arr D1 D2]
;

rec ref : {gamma:aeqCtx} {M:[gamma |- term]} [gamma |- aeq M M] =
mlam gamma => mlam M => case [gamma |- M] of
| [gamma |- #p.1] => [gamma |- #p.2]

| [gamma |- lam \x. M] =>
  let [gamma, b:block y:term , _t:aeq y y |- D[.., b.1, b.2]] =
         ref [gamma, b:block y:term , _t:aeq y y] [gamma, b |- M[.., b.1]]
  in
   [gamma |- ae_l \x. \w. D]

| [gamma |- app M1 M2] =>
  let [gamma |- D1] = ref [gamma] [gamma |- M1] in
  let [gamma |- D2] = ref [gamma] [gamma |- M2] in
    [gamma |- ae_a D1 D2]

| [gamma |- tlam \a. M] =>
  let [gamma, b:block a:tp , _t:atp a a |- D[.., b.1, b.2]] =
         ref [gamma, b:block a:tp , _t:atp a a] [gamma, b |- M[.., b.1]]
  in
   [gamma |- ae_tl \x. \w. D]

| [gamma |- tapp M T] =>
  let [gamma |- D1] = ref [gamma] [gamma |- M] in
  let [gamma |- D2] = reftp [gamma] [gamma |- T] in
    [gamma |- ae_ta D1 D2]
;

rec refErr : {gamma:aeqCtxErr} {M:[gamma |- term]} [gamma |- aeq M M] =
mlam gamma => mlam M => case [gamma |- M] of
| [gamma |- #p.1] => [gamma |- #p.2]

| [gamma |- lam \x. M] =>
  let [gamma, b:block y:term , _t:aeq y y |- D[.., b.1, b.2]] =
         ref [gamma, b:block y:term , _t:aeq y y] [gamma, b |- M[.., b.1]]
  in
   [gamma |- ae_l \x. \w. D]

| [gamma |- app M1 M2] =>
  let [gamma |- D1] = ref [gamma] [gamma |- M1] in
  let [gamma |- D2] = ref [gamma] [gamma |- M2] in
    [gamma |- ae_a D1 D2]

| [gamma |- tlam \a. M] =>
  let [gamma, b:block a:tp , _t:atp a a |- D[.., b.1, b.2]] =
         ref [gamma, b:block a:tp , _t:atp a a] [gamma, b |- M[.., b.1]]
  in
   [gamma |- ae_tl \x. \w. D]

| [gamma |- tapp M T] =>
  let [gamma |- D1] = ref [gamma] [gamma |- M] in
  let [gamma |- D2] = reftp [gamma] [gamma |- T] in
    [gamma |- ae_ta D1 D2]
;

$ beluga soundness.bel
## Type Reconstruction begin: soundness.bel ##
## Type Reconstruction done:  soundness.bel ##