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.
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.