Lean Kernel Arena / canonical-min

Checker "canonical-min"

Version: kernel-arena (0acb45d) · 📄 Declaration · 🔗 Source

Canonical-min is a minimal inhabitation solver and type checker for dependent type theory. This checker deserializes lean4export expressions, translates them with CanonicalLean, and checks the supported fragment with CanonicalMin.check.

The implementation is intentionally incomplete and declines declarations it cannot translate or represent.

Soundness (rightfully rejected tests)

28 ✅ 1 ❌ 51 🚫

Completeness (rightfully accepted tests)

42 ✅ 54 ❌ 42 🚫

Corner cases (no outcome prescribed)

18 ✅ 12 🚫

Test Expected Result ⏱️ 🧠
cedar 👍 ✋ 48.4 s 2.5 GB
con-leche 👍 ✋ 30.9 s 1.9 GB
cslib 👍 ✋ 2.22 min 4.8 GB
init 👍 ✋ 19.8 s 1.5 GB
init-prelude 👍 ✋ 604 ms 1.1 GB
mathlib 👍 ✋ 5.70 min 12.1 GB
navier-stokes-euler 👍 🚫 86.3 s 3.8 GB
reachability 👍 ✋ 1.48 s 1.1 GB
std 👍 ✋ 33.5 s 2.0 GB
12 10.5 s 1.1 GB
closure-level-subst ✋ ✋ 387 ms 1.1 GB
constlevels ✋ 🚫 571 ms 1.1 GB
ctor-num-fields ✋ 🚫 389 ms 1.1 GB
eta-ctor-alias ✋ 🚫 387 ms 1.1 GB
forged-quot-ind ✋ 🚫 387 ms 1.1 GB
k-rec-conv ✋ ✋ 390 ms 1.1 GB
large-elim-param ✋ 🚫 387 ms 1.1 GB
large-elim-prop-bool ✋ 🚫 388 ms 1.1 GB
level-imax-leq ✋ ✋ 387 ms 1.1 GB
level-imax-normalization ✋ ✋ 387 ms 1.1 GB
loose-bvar-value ✋ 🚫 550 ms 1.1 GB
nat-rec-k-lie ✋ ✋ 387 ms 1.1 GB
nat-rec-rules ✋ ✋ 387 ms 1.1 GB
nested-name-capture ✋ 🚫 389 ms 1.1 GB
nested-rec-rule-nfields ✋ ✋ 392 ms 1.1 GB
nested-unused-param ✋ 🚫 390 ms 1.1 GB
orphan-rec ✋ 🚫 386 ms 1.1 GB
pi-closure-context ✋ ✋ 387 ms 1.1 GB
proj-non-structure ✋ 🚫 387 ms 1.1 GB
proj-of-imax-prop ✋ 🚫 389 ms 1.1 GB
proj-of-stuck-prop ✋ ✋ 404 ms 1.1 GB
proj-of-subst-prop ✋ ✋ 403 ms 1.1 GB
rec-k-lie ✋ 🚫 388 ms 1.1 GB
rec-missing-ih ✋ ✋ 405 ms 1.1 GB
rec-of-subst-prop ✋ ✋ 404 ms 1.1 GB
unit-rec-rule ✋ 🚫 387 ms 1.1 GB
0 12.0 s 1.1 GB
alg-conv-trans-acc 🤷 ✋ 391 ms 1.1 GB
alg-conv-trans-acc-left 🤷 ✋ 392 ms 1.1 GB
alg-conv-trans-acc-right 🤷 ✋ 392 ms 1.1 GB
alg-conv-trans-quot 🤷 ✋ 390 ms 1.1 GB
alg-conv-trans-quot-left 🤷 ✋ 390 ms 1.1 GB
alg-conv-trans-quot-left-def 🤷 ✋ 388 ms 1.1 GB
alg-conv-trans-quot-right 🤷 👍 387 ms 1.1 GB
eta-ctor 🤷 🚫 389 ms 1.1 GB
eta-rec-struct 🤷 ✋ 388 ms 1.1 GB
eta-rule-k 🤷 ✋ 387 ms 1.1 GB
eta-struct-major-and 🤷 ✋ 387 ms 1.1 GB
eta-struct-major-and-no-whnf 🤷 ✋ 389 ms 1.1 GB
eta-struct-major-no-whnf 🤷 ✋ 389 ms 1.1 GB
eta-unit-like-nested 🤷 🚫 388 ms 1.1 GB
eta-unit-like-pi 🤷 ✋ 387 ms 1.1 GB
eta-unit-like-proof-field 🤷 🚫 387 ms 1.1 GB
eta-unit-like-struct 🤷 🚫 387 ms 1.1 GB
imax-nested-absorption 🤷 ✋ 386 ms 1.1 GB
imax-right-successor 🤷 ✋ 386 ms 1.1 GB
large-elim-maybe-prop 🤷 🚫 387 ms 1.1 GB
let-value-type-mismatch 🤷 ✋ 391 ms 1.1 GB
nested-nonuniform-param 🤷 🚫 387 ms 1.1 GB
nested-redex-aux 🤷 🚫 389 ms 1.1 GB
positivity-whnf 🤷 🚫 387 ms 1.1 GB
proj-maybe-prop 🤷 🚫 387 ms 1.1 GB
proj-maybe-prop-past 🤷 🚫 388 ms 1.1 GB
proof-param-ok 👍 🚫 386 ms 1.1 GB
proof-param-swap 🤷 🚫 386 ms 1.1 GB
subject-reduction-redex 🤷 ✋ 391 ms 1.1 GB
subject-reduction-reduct 🤷 ✋ 391 ms 1.1 GB
vanishing-occurrence 🤷 🚫 387 ms 1.1 GB
3 3.88 s 1.1 GB
extra-rec ✋ 🚫 387 ms 1.1 GB
inductive-undeclared-universe ✋ 🚫 386 ms 1.1 GB
level-index-out-of-order 👍 👍 387 ms 1.1 GB
nat-lit-add 👍 ✋ 389 ms 1.1 GB
nat-lit-add-bad ✋ ✋ 389 ms 1.1 GB
nat-lit-ble 👍 ✋ 395 ms 1.1 GB
nat-lit-sub 👍 ✋ 389 ms 1.1 GB
orphan-ctor ✋ 🚫 387 ms 1.1 GB
proj-of-prop ✋ 🚫 386 ms 1.1 GB
sparse-name-index 👍 👍 388 ms 1.1 GB
2 15.1 s (×11) 1.1 GB
app-lam 👍 ✋ 463 ms 1.1 GB
args-before-unfold 👍 🚫 389 ms 1.1 GB
beta-ladder 👍 ✋ 418 ms 1.1 GB
church-numerals 👍 ✋ 387 ms 1.1 GB
discarded-argument 👍 🚫 388 ms 1.1 GB
discarded-argument-match 👍 🚫 388 ms 1.1 GB
folded-constant-first 👍 🚫 390 ms 1.1 GB
folded-constant-last 👍 🚫 390 ms 1.1 GB
fueled-chain 👍 ✋ 443 ms 1.1 GB
grind-ring-5 👍 ✋ 979 ms 1.1 GB
identical-nesting 👍 🚫 387 ms 1.1 GB
irrelevance-before-evaluation 👍 🚫 387 ms 1.1 GB
irrelevance-refutes 👍 👍 389 ms (×14) 1.1 GB (×16)
let-fold 👍 ✋ 411 ms 1.1 GB
let-ladder 👍 ✋ 417 ms 1.1 GB
magma-list-deep-n21 👍 🚫 456 ms 1.1 GB
magma-list-deep-n36 👍 🚫 460 ms 1.1 GB
magma-list-pair-n21 👍 🚫 421 ms 1.1 GB
magma-list-pair-n7 👍 🚫 422 ms 1.1 GB
magma-string-n4 👍 🚫 1.39 s 1.1 GB
magma-string-pair-n9 👍 🚫 1.38 s 1.1 GB
proj-cheap-struct 👍 🚫 392 ms 1.1 GB
proj-lazy-struct 👍 ✋ 392 ms 1.1 GB
proj-stuck-struct 👍 ✋ 392 ms 1.1 GB
prop-struct-projections 👍 ✋ 413 ms 1.1 GB
refute-cheap-first ✋ 🚫 388 ms 1.1 GB
refute-cheap-last ✋ 🚫 388 ms 1.1 GB
repeated-subproblem 👍 🚫 387 ms 1.1 GB
shared-subterm 👍 🚫 390 ms 1.1 GB
shift-cascade 👍 👍 407 ms (×8.8) 1.1 GB (×16)
unroll-versus-evaluate 👍 🚫 390 ms 1.1 GB
53 54.1 s 1.1 GB
001_basicDef 👍 ✋ 389 ms 1.1 GB
002_badDef ✋ ✋ 387 ms 1.1 GB
003_arrowType 👍 ✋ 386 ms 1.1 GB
004_dependentType 👍 ✋ 386 ms 1.1 GB
005_constType 👍 👍 387 ms 1.1 GB
006_betaReduction 👍 ✋ 387 ms 1.1 GB
007_betaReduction2 👍 👍 386 ms 1.1 GB
008_forallSortWhnf 👍 ✋ 386 ms 1.1 GB
009_forallSortBad ✋ 🚫 386 ms 1.1 GB
010_nonTypeType ✋ 🚫 555 ms 1.1 GB
011_nonTypeAxiom ✋ 👍 389 ms 1.1 GB
012_nonPropThm ✋ ✋ 387 ms 1.1 GB
013_thmProof 👍 👍 387 ms 1.1 GB
014_selfProof ✋ 🚫 387 ms 1.1 GB
015_levelComp1 👍 ✋ 389 ms 1.1 GB
016_levelComp2 👍 ✋ 387 ms 1.1 GB
017_levelComp3 👍 ✋ 389 ms 1.1 GB
018_levelParams 👍 ✋ 387 ms 1.1 GB
019_tut06_bad01 ✋ ✋ 391 ms 1.1 GB
020_levelComp4 👍 ✋ 387 ms 1.1 GB
021_levelComp5 👍 ✋ 389 ms 1.1 GB
022_imax1 👍 ✋ 387 ms 1.1 GB
023_imax2 👍 ✋ 386 ms 1.1 GB
024_levelMaxComm 👍 ✋ 387 ms 1.1 GB
025_levelMaxAssoc 👍 ✋ 388 ms 1.1 GB
026_levelMaxIdem 👍 ✋ 391 ms 1.1 GB
027_levelMaxAbsorb 👍 ✋ 391 ms 1.1 GB
028_inferVar 👍 👍 386 ms 1.1 GB
029_defEqLambda 👍 👍 386 ms 1.1 GB
030_peano1 👍 ✋ 387 ms 1.1 GB
031_peano2 👍 ✋ 387 ms 1.1 GB
032_peano3 👍 ✋ 387 ms 1.1 GB
033_letType 👍 ✋ 387 ms 1.1 GB
034_letTypeDep 👍 ✋ 386 ms 1.1 GB
035_letRed 👍 👍 387 ms 1.1 GB
036_empty 👍 👍 387 ms 1.1 GB
037_boolType 👍 👍 386 ms 1.1 GB
038_twoBool 👍 🚫 387 ms 1.1 GB
039_andType 👍 👍 387 ms 1.1 GB
040_prodType 👍 👍 387 ms 1.1 GB
041_pprodType 👍 👍 387 ms 1.1 GB
042_pUnitType 👍 👍 386 ms 1.1 GB
043_eqType 👍 👍 387 ms 1.1 GB
044_natDef 👍 🚫 387 ms 1.1 GB
045_rbTreeDef 👍 🚫 387 ms 1.1 GB
046_inductBadNonSort ✋ 🚫 386 ms 1.1 GB
047_inductBadNonSort2 ✋ 🚫 389 ms 1.1 GB
048_inductLevelParam ✋ 🚫 389 ms 1.1 GB
049_inductTooFewParams ✋ 🚫 391 ms 1.1 GB
050_inductWrongCtorParams ✋ 🚫 387 ms 1.1 GB
051_inductWrongCtorResParams ✋ 🚫 388 ms 1.1 GB
052_inductWrongCtorResLevel ✋ 🚫 388 ms 1.1 GB
053_inductInIndex ✋ 🚫 386 ms 1.1 GB
054_indNeg ✋ 🚫 387 ms 1.1 GB
055_reduceCtorParam.mk 👍 🚫 386 ms 1.1 GB
056_reduceCtorType.mk ✋ 🚫 386 ms 1.1 GB
057_indNegReducible ✋ 🚫 386 ms 1.1 GB
058_predWithTypeField 👍 🚫 386 ms 1.1 GB
059_typeWithTypeField 👍 🚫 387 ms 1.1 GB
060_typeWithTypeFieldPoly 👍 🚫 386 ms 1.1 GB
061_typeWithTooHighTypeField.mk ✋ 🚫 387 ms 1.1 GB
062_emptyRec 👍 👍 386 ms 1.1 GB
063_boolRec 👍 👍 387 ms 1.1 GB
064_twoBoolRec 👍 🚫 387 ms 1.1 GB
065_andRec 👍 👍 387 ms 1.1 GB
066_prodRec 👍 ✋ 387 ms 1.1 GB
067_pprodRec 👍 ✋ 387 ms 1.1 GB
068_punitRec 👍 ✋ 387 ms 1.1 GB
069_eqRec 👍 👍 387 ms 1.1 GB
070_nRec 👍 🚫 386 ms 1.1 GB
071_rbTreeRef 👍 🚫 387 ms 1.1 GB
072_boolPropRec 👍 🚫 386 ms 1.1 GB
073_BogusRecursor ✋ 🚫 389 ms 1.1 GB
074_existsRec 👍 👍 387 ms 1.1 GB
075_typeSingletonRecReduction 👍 🚫 387 ms 1.1 GB
076_sortElimPropRec 👍 🚫 387 ms 1.1 GB
077_sortElimProp2Rec 👍 🚫 387 ms 1.1 GB
078_boolRecEqns 👍 ✋ 388 ms 1.1 GB
079_prodRecEqns 👍 👍 388 ms 1.1 GB
080_nRecReduction 👍 🚫 387 ms 1.1 GB
081_listRecReduction 👍 👍 390 ms 1.1 GB
082_RBTree.id_spec 👍 🚫 390 ms 1.1 GB
083_And.right 👍 👍 386 ms 1.1 GB
084_Prod.snd 👍 👍 386 ms 1.1 GB
085_PProd.snd 👍 👍 387 ms 1.1 GB
086_PSigma.snd 👍 👍 387 ms 1.1 GB
087_projOutOfRange ✋ 🚫 550 ms 1.1 GB
088_projNotStruct ✋ 🚫 387 ms 1.1 GB
089_projProp1 👍 🚫 387 ms 1.1 GB
090_projProp2 ✋ 🚫 387 ms 1.1 GB
091_projProp3 👍 🚫 387 ms 1.1 GB
092_projProp4 ✋ 🚫 387 ms 1.1 GB
093_projProp5 ✋ 🚫 387 ms 1.1 GB
094_projProp6 ✋ 🚫 387 ms 1.1 GB
095_projDataIndexRec 👍 🚫 387 ms 1.1 GB
096_projIndexData ✋ 🚫 387 ms 1.1 GB
097_projIndexData2 ✋ 🚫 387 ms 1.1 GB
098_projRed 👍 👍 387 ms 1.1 GB
099_ruleK 👍 👍 387 ms 1.1 GB
100_ruleKbad ✋ ✋ 387 ms 1.1 GB
101_ruleKAcc ✋ ✋ 388 ms 1.1 GB
102_aNatLit 👍 👍 387 ms 1.1 GB
103_natLitEq 👍 👍 387 ms 1.1 GB
104_proofIrrelevance 👍 ✋ 387 ms 1.1 GB
105_proofIrrelevanceBad ✋ ✋ 387 ms 1.1 GB
106_proofIrrelevanceWhnf 👍 ✋ 387 ms 1.1 GB
107_proofIrrelevanceUnderBinder 👍 ✋ 386 ms 1.1 GB
108_unitEta1 👍 ✋ 387 ms 1.1 GB
109_unitEta2 👍 ✋ 387 ms 1.1 GB
110_unitEta3 👍 ✋ 387 ms 1.1 GB
111_indexedUnitEta ✋ 🚫 387 ms 1.1 GB
112_structEta 👍 ✋ 388 ms 1.1 GB
113_indexedStructEta ✋ 🚫 387 ms 1.1 GB
114_funEta 👍 👍 387 ms 1.1 GB
115_funEtaDep 👍 👍 387 ms 1.1 GB
116_funEtaBad ✋ ✋ 387 ms 1.1 GB
117_reflOccLeft ✋ 🚫 387 ms 1.1 GB
118_reflOccInIndex ✋ 🚫 386 ms 1.1 GB
119_reduceCtorParamRefl.mk 👍 🚫 386 ms 1.1 GB
120_reduceCtorParamRefl2.mk 👍 🚫 387 ms 1.1 GB
121_rTreeRec 👍 🚫 387 ms 1.1 GB
122_rtreeRecReduction 👍 🚫 387 ms 1.1 GB
123_accRecType 👍 👍 388 ms 1.1 GB
124_accRecReduction 👍 👍 388 ms 1.1 GB
125_accRecNoEta ✋ ✋ 388 ms 1.1 GB
126_quotMkType 👍 👍 387 ms 1.1 GB
127_quotIndType 👍 👍 387 ms 1.1 GB
128_quotLiftType 👍 👍 387 ms 1.1 GB
129_quotSoundType 👍 👍 387 ms 1.1 GB
130_quotLiftReduction 👍 👍 387 ms 1.1 GB
131_quotIndReduction 👍 👍 388 ms 1.1 GB
132_dup_defs ✋ ✋ 243 ms 798.7 MB
133_dup_ind_def ✋ ✋ 243 ms 798.8 MB
134_dup_ctor_def ✋ ✋ 243 ms 798.8 MB
135_dup_rec_def ✋ ✋ 243 ms 798.9 MB
136_misnamed_rec_user ✋ 🚫 386 ms 1.1 GB
137_dup_rec_def2 ✋ ✋ 386 ms 1.1 GB
138_dup_ctor_rec ✋ ✋ 243 ms 798.8 MB
139_DupConCon ✋ ✋ 243 ms 798.7 MB
140_falseFromUnsafe ✋ 🚫 387 ms 1.1 GB
141_falseFromPartial ✋ 🚫 386 ms 1.1 GB