LogoAdelfa
ExamplesLambda calculus

ORBI Benchmarks

This page contains benchmarks set out in the paper "The Next 700 Challenge Problems for Reasoning with Higher-Order Abstract Syntax Representations" by Felty et al.[1]

Although partially completed, we intend to continue adding more benchmarks to this page.

Equality of Untyped Lambda Calculus

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.
equal-untyped.ath
Specification "equal-untyped.lf".

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

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.
%ctx
exists n1. search.

Theorem symG: ctx G:xaG, forall T1 T2 Q,
  {G |- Q : aeq T1 T2} => exists D, {G |- D : aeq T2 T1}.
induction on 1.intros. 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.
%context
exists n1. search.

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.
%ctx
case H2.
exists n1. search.

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.

Theorem seqG : ctx G:daG, forall M N D1,
  {G |- D1: aeq M N} => exists D2, {G |- D2: deq M N}.
induction on 1.
intros. case H1 (keep).
weaken H4 with deq n2 n2.
apply IH to H5 with (G = G, n1:tm, n2:aeq n1 n1, n:deq n1 n1).
prune H6.
ctxpermute H6 to G, n1:tm, n:deq n1 n1, n2:aeq n1 n1.
strengthen H7.
exists de_l M1 N1 D2. search.
apply IH to H6. apply IH to H7.
exists de_a M1 M2 N1 N2 D1 D4. search.
exists n2. search.

Theorem substG: ctx G:xaG, forall M1: o -> o M2: o -> o N1 N2 D1: o -> o -> o D2,
  {G |- [x][y] D1 x y : {x:tm}{y:aeq x x} aeq (M1 x) (M2 x)} => {G |- D2: aeq N1 N2}
    => exists D3, {G |- D3 : aeq (M1 N1) (M2 N2)}.
induction on 1.
intros.
case H1 (keep).
ctxpermute H5 to G, n4:tm, n5:aeq n4 n4, n:tm, n1:aeq n n.
weaken H2 with tm.
weaken H7 with aeq n6 n6.
apply IH to H6 H8 with (G = G, n1:tm, n:aeq n1 n1).
prune H9.
inst H3 with n = N1.
inst H4 with n = N2.
strengthen H10.
strengthen H11.
prune H5.
exists ae_l (M3 N1) (M4 N2) D3.
assert {G, n:tm |- M3 N1 n : tm}.
  ctxpermute H10 to G, n2:tm, n1:aeq N1 N1.
  strengthen H12.
  search.
assert {G, n:tm |- M4 N2 n : tm}.
  ctxpermute H11 to G, n3:tm, n1:aeq N2 N2.
  strengthen H13.
  search.
search.
apply IH to H7 H2.
apply IH to H8 H2.
exists ae_a (M3 N1) (M4 N1) (M5 N2) (M6 N2) (D1 n1 n) (D5 n1 n). search.
exists D2. search.
exists n3. search.

References

  1. [1] Felty, A.P., Momigliano, A., Pientka, B.: The Next 700 Challenge Problems for Reasoning with Higher-Order Abstract Syntax Representations. Journal of Automated Reasoning. 55, 307ā€“372 (2015). https://doi.org/10.1007/s10817-015-9327-3ā .

On this page

Equality of Untyped Lambda Calculus