Equality in the Untyped Lambda Calculus

This page contains a solution to a problem set out in the paper “The Next 700 Challenge Problems for Reasoning with Higher-Order Abstract Syntax Representations ” by Felty et al.

This benchmark provides a specification for the untyped $\lambda$ -calculus with two forms of equality: algorithmic and declarative.

The full solutions are provided in equal-untyped.lf and equal-untyped.ath.

equal-untyped.lf


tm: type.
lam: {M: tm -> tm} tm.
app: {M1:tm}{M2:tm} tm.
 
aeq: tm -> tm -> type.
deq: tm -> tm -> type.
 
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_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)).
 
de_a : {M1:tm}{M2:tm}{N1:tm}{N2:tm}
       {D1: deq M1 N1}{D2: deq M2 N2}
       deq (app M1 M2) (app N1 N2).
de_l : {M: tm -> tm}{N: tm -> tm}
       {D: {z:tm} deq z z -> deq (M z) (N z)}
       deq (lam ([x] M x)) (lam ([x] N x)).
de_s : {M:tm}{N:tm}
       {D: deq M N}
       deq N M.
de_t : {M1:tm}{M2:tm}{M3:tm}
       {D1: deq M1 M2}
       {D2: deq M2 M3}
       deq M1 M3.
de_r : {M:tm} deq M M.

The benchmark also defines two different context schemas to be used:

equal-untyped.ath


Schema xaG := (x: tm,a: aeq x x).
Schema daG := (x:tm, a:aeq x x, u:deq x x).

One wishes to prove three properties about algorithmic equality in isolation:

Reflexivity

equal-untyped.ath


Theorem reflG: ctx G:xaG, forall T, {G |- T : tm} => exists D, {G |- D : aeq T T}
induction on 1 intros case H1 (keep)
%app
apply IH to H2
apply IH to H3
exists ae_a M1 M2 M1 M2 D D1
search
%lam
weaken H2 with aeq n n
apply IH to H3 with (G = G, n1: tm, n:aeq n1 n1)
prune H2
exists ae_l M M D
search
%var
exists n1 search

Symmetry

equal-untyped.ath


Theorem symG: ctx G:xaG, forall T1 T2 Q,
  {G |- Q : aeq T1 T2} => exists D, {G |- D : aeq T2 T1}
induction on 1intros case H1(keep)
%lam
apply IH to H4 with (G = G, n1: tm, n: aeq n1 n1)
prune H5
exists (ae_l N M D1)
search
%app
apply IH to H6
apply IH to H7
exists (ae_a N1 N2 M1 M2 D D3)
search
%var
exists n1 search

Transitivity

equal-untyped.ath


Theorem tranG: ctx G:xaG, forall M1 M2 M3 D1 D2,
  {G |- D1: aeq M1 M2} => {G |- D2: aeq M2 M3} => exists D3, {G |- D3: aeq M1 M3}
induction on 1 intros
case H1 (keep)
%lam
case H2
apply IH to H5 H8 with (G = G, n1:tm, n: aeq n1 n1)
prune H9
exists ae_l M M4 D1 search
%app
case H2
apply IH to H7 H13
apply IH to H8 H14
exists ae_a M4 M5 N3 N4 D1 D2 search
%var
case H2
exists n1 search

Now, one wishes to show that algorithmic equality is complete with respect to declarative equality. In other words “If two terms are declaratively equal, then they are algorithmically equal.” This would entail analyzing the cases in which the terms under consideration are equal by reflexivity, symmetry, and transitivity. Then, one must prove that these properties hold for algorithmic equality. However, we have already shown these properties to hold in our above theorems.

The wrinkle is that these properties were proven with a context variable circumscribed by xaG which has the shape (x:tm, a:aeq x x), and in order to reason about declarative equality we must have the context variable circumscribed by daG which has the shape (x:tm, a:aeq x x, u:deq x x). Schema subsumption will allow Adelfa to realize that this extended shape’s entry u: deq x x cannot impact the theorems reflG, tranG, or symG, and we can use them directly in daG.

equal-untyped.ath


Theorem ceqG: ctx G:daG, forall M N D1,
  {G |- D1: deq M N} => exists D2, {G |- D2 : aeq M N}
induction on 1
intros case H1 (keep) apply reflG to H2 exists D search
apply IH to H5
apply IH to H6
apply tranG to H7 H8 exists D5 search
apply IH to H4
apply symG to H5 exists D1 search
weaken H4 with aeq n2 n2
ctxpermute H5 to G, n2: tm, n4: aeq n2 n2, n3:deq n2 n2
apply IH to H6 with (G = G, n1:tm, n2:aeq n1 n1, n:deq n1 n1)
prune H7
strengthen H7
exists ae_l M1 N1 ([x][y] D2 y x) search
apply IH to H6 apply IH to H7
exists ae_a M1 M2 N1 N2 D1 D4 search
exists n1 search