search

JetBrains / Arend

The Arend Proof Assistant
https://arend-lang.github.io/
Apache License 2.0
690 stars 33 forks source link

Exception in thread "main" java.lang.IllegalStateException #345

Closed sxhya closed 2 months ago

sxhya commented 2 months ago

Exception:

Exception in thread "main" java.lang.IllegalStateException
    at org.arend.core.subst.ListLevels.makeSubstitution(ListLevels.java:32)
    at org.arend.core.definition.ClassField.getType(ClassField.java:59)
    at org.arend.core.expr.visitor.GetTypeVisitor.visitFieldCall(GetTypeVisitor.java:266)
    at org.arend.core.expr.visitor.GetTypeVisitor.visitFieldCall(GetTypeVisitor.java:28)
    at org.arend.core.expr.FieldCallExpression.accept(FieldCallExpression.java:94)
    at org.arend.core.expr.Expression.getType(Expression.java:136)
    at org.arend.core.expr.Expression.getType(Expression.java:140)
    at org.arend.core.expr.visitor.NormalizeVisitor.evalFieldCall(NormalizeVisitor.java:818)
    at org.arend.core.expr.visitor.NormalizeVisitor.visitFieldCall(NormalizeVisitor.java:840)
    at org.arend.core.expr.visitor.NormalizeVisitor.visitFieldCall(NormalizeVisitor.java:36)
    at org.arend.core.expr.FieldCallExpression.accept(FieldCallExpression.java:94)
    at org.arend.core.expr.visitor.NormalizeVisitor.visitApp(NormalizeVisitor.java:44)
    at org.arend.core.expr.visitor.NormalizeVisitor.visitApp(NormalizeVisitor.java:36)
    at org.arend.core.expr.AppExpression.accept(AppExpression.java:78)
    at org.arend.core.expr.visitor.NormalizeVisitor.visitApp(NormalizeVisitor.java:44)
    at org.arend.core.expr.visitor.NormalizeVisitor.visitApp(NormalizeVisitor.java:36)
    at org.arend.core.expr.AppExpression.accept(AppExpression.java:78)
    at org.arend.core.expr.Expression.normalize(Expression.java:286)
    at org.arend.core.expr.Expression.getPiParameters(Expression.java:589)
    at org.arend.typechecking.result.TypecheckingResult.getImplicitParameters(TypecheckingResult.java:69)
    at org.arend.typechecking.implicitargs.StdImplicitArgsInference.inferTail(StdImplicitArgsInference.java:935)
    at org.arend.typechecking.visitor.CheckTypeVisitor.tResultToResult(CheckTypeVisitor.java:583)
    at org.arend.typechecking.visitor.CheckTypeVisitor.visitApp(CheckTypeVisitor.java:3451)
    at org.arend.typechecking.visitor.CheckTypeVisitor.visitApp(CheckTypeVisitor.java:3368)
    at org.arend.typechecking.visitor.CheckTypeVisitor.visitApp(CheckTypeVisitor.java:92)
    at org.arend.term.concrete.Concrete$AppExpression.accept(Concrete.java:477)
    at org.arend.typechecking.visitor.CheckTypeVisitor.checkExpr(CheckTypeVisitor.java:993)
    at org.arend.typechecking.visitor.CheckTypeVisitor.checkArgument(CheckTypeVisitor.java:1245)
    at org.arend.typechecking.implicitargs.StdImplicitArgsInference.inferArg(StdImplicitArgsInference.java:229)
    at org.arend.typechecking.implicitargs.StdImplicitArgsInference.infer(StdImplicitArgsInference.java:717)
    at org.arend.typechecking.visitor.CheckTypeVisitor.visitApp(CheckTypeVisitor.java:3420)
    at org.arend.typechecking.visitor.CheckTypeVisitor.visitApp(CheckTypeVisitor.java:3368)
    at org.arend.typechecking.visitor.CheckTypeVisitor.visitApp(CheckTypeVisitor.java:92)
    at org.arend.term.concrete.Concrete$AppExpression.accept(Concrete.java:477)
    at org.arend.typechecking.visitor.CheckTypeVisitor.checkType(CheckTypeVisitor.java:1135)
    at org.arend.typechecking.visitor.CheckTypeVisitor.visitSigmaParameter(CheckTypeVisitor.java:2689)
    at org.arend.typechecking.visitor.CheckTypeVisitor.visitSigmaParameters(CheckTypeVisitor.java:2679)
    at org.arend.typechecking.visitor.CheckTypeVisitor.visitSigma(CheckTypeVisitor.java:2668)
    at org.arend.typechecking.visitor.CheckTypeVisitor.visitSigma(CheckTypeVisitor.java:92)
    at org.arend.term.concrete.Concrete$SigmaExpression.accept(Concrete.java:1218)
    at org.arend.typechecking.visitor.CheckTypeVisitor.checkExpr(CheckTypeVisitor.java:993)
    at org.arend.typechecking.visitor.CheckTypeVisitor.typecheck(CheckTypeVisitor.java:596)
    at org.arend.typechecking.visitor.CheckTypeVisitor.typecheck(CheckTypeVisitor.java:92)
    at org.arend.lib.meta.ExtMeta$ExtGenerator.generate(ExtMeta.java:554)
    at org.arend.lib.meta.ExtMeta$1.invokeMeta(ExtMeta.java:814)
    at org.arend.typechecking.visitor.CheckTypeVisitor.invokeMeta(CheckTypeVisitor.java:3184)
    at org.arend.typechecking.visitor.CheckTypeVisitor.checkMeta(CheckTypeVisitor.java:3248)
    at org.arend.typechecking.visitor.CheckTypeVisitor.visitReference(CheckTypeVisitor.java:2033)
    at org.arend.typechecking.visitor.CheckTypeVisitor.visitReference(CheckTypeVisitor.java:2028)
    at org.arend.typechecking.visitor.CheckTypeVisitor.visitReference(CheckTypeVisitor.java:92)
    at org.arend.term.concrete.Concrete$ReferenceExpression.accept(Concrete.java:666)
    at org.arend.typechecking.visitor.CheckTypeVisitor.checkExpr(CheckTypeVisitor.java:993)
    at org.arend.typechecking.visitor.CheckTypeVisitor.visitLam(CheckTypeVisitor.java:2418)
    at org.arend.typechecking.visitor.CheckTypeVisitor.lambda$visitLam$1(CheckTypeVisitor.java:2497)
    at org.arend.typechecking.visitor.CheckTypeVisitor.visitLam(CheckTypeVisitor.java:2579)
    at org.arend.typechecking.visitor.CheckTypeVisitor.visitLam(CheckTypeVisitor.java:2613)
    at org.arend.typechecking.visitor.CheckTypeVisitor.visitLam(CheckTypeVisitor.java:92)
    at org.arend.term.concrete.Concrete$LamExpression.accept(Concrete.java:1050)
    at org.arend.typechecking.visitor.CheckTypeVisitor.checkExpr(CheckTypeVisitor.java:993)
    at org.arend.typechecking.visitor.CheckTypeVisitor.checkArgument(CheckTypeVisitor.java:1245)
    at org.arend.typechecking.implicitargs.StdImplicitArgsInference.inferArg(StdImplicitArgsInference.java:181)
    at org.arend.typechecking.implicitargs.StdImplicitArgsInference.infer(StdImplicitArgsInference.java:717)
    at org.arend.typechecking.visitor.CheckTypeVisitor.visitApp(CheckTypeVisitor.java:3420)
    at org.arend.typechecking.visitor.CheckTypeVisitor.visitApp(CheckTypeVisitor.java:3368)
    at org.arend.typechecking.visitor.CheckTypeVisitor.visitApp(CheckTypeVisitor.java:92)
    at org.arend.term.concrete.Concrete$AppExpression.accept(Concrete.java:477)
    at org.arend.typechecking.visitor.CheckTypeVisitor.checkExpr(CheckTypeVisitor.java:993)
    at org.arend.typechecking.visitor.CheckTypeVisitor.typecheck(CheckTypeVisitor.java:596)
    at org.arend.typechecking.visitor.CheckTypeVisitor.typecheck(CheckTypeVisitor.java:92)
    at org.arend.lib.meta.ExtMeta.invokeMeta(ExtMeta.java:810)
    at org.arend.typechecking.visitor.CheckTypeVisitor.invokeMeta(CheckTypeVisitor.java:3184)
    at org.arend.typechecking.visitor.CheckTypeVisitor.invokeDeferredMetas(CheckTypeVisitor.java:1055)
    at org.arend.typechecking.visitor.CheckTypeVisitor.finalize(CheckTypeVisitor.java:1108)
    at org.arend.typechecking.visitor.DefinitionTypechecker.typecheckFunctionBody(DefinitionTypechecker.java:1684)
    at org.arend.typechecking.visitor.DefinitionTypechecker.visitFunction(DefinitionTypechecker.java:173)
    at org.arend.typechecking.visitor.DefinitionTypechecker.visitFunction(DefinitionTypechecker.java:64)
    at org.arend.term.concrete.Concrete$BaseFunctionDefinition.accept(Concrete.java:2551)
    at org.arend.term.concrete.Concrete$Definition.accept(Concrete.java:2100)
    at org.arend.typechecking.order.listener.TypecheckingOrderingListener.unitFound(TypecheckingOrderingListener.java:243)
    at org.arend.typechecking.order.Ordering.unitFound(Ordering.java:189)
    at org.arend.typechecking.order.Ordering.unitFound(Ordering.java:24)
    at org.arend.typechecking.order.TarjanSCC.doOrderRecursively(TarjanSCC.java:54)
    at org.arend.typechecking.order.TarjanSCC.order(TarjanSCC.java:24)
    at org.arend.typechecking.order.Ordering.order(Ordering.java:120)
    at org.arend.typechecking.order.Ordering.orderModule(Ordering.java:87)
    at org.arend.typechecking.order.Ordering.orderModule(Ordering.java:94)
    at org.arend.typechecking.order.Ordering.orderModules(Ordering.java:77)
    at org.arend.library.BaseLibrary.orderModules(BaseLibrary.java:138)
    at org.arend.library.BaseLibrary.orderModules(BaseLibrary.java:143)
    at org.arend.typechecking.order.listener.TypecheckingOrderingListener.lambda$typecheckLibrary$2(TypecheckingOrderingListener.java:126)
    at org.arend.typechecking.computation.ComputationRunner.run(ComputationRunner.java:48)
    at org.arend.typechecking.computation.BooleanComputationRunner.run(BooleanComputationRunner.java:8)
    at org.arend.typechecking.order.listener.TypecheckingOrderingListener.typecheckLibrary(TypecheckingOrderingListener.java:126)
    at org.arend.typechecking.order.listener.TypecheckingOrderingListener.typecheckLibrary(TypecheckingOrderingListener.java:130)
    at org.arend.frontend.BaseCliFrontend.run(BaseCliFrontend.java:552)
    at org.arend.frontend.ConsoleMain.main(ConsoleMain.java:6)

Reproducer:

\import Arith.Fin(FinLinearOrder)
\import Category
\import Equiv (Equiv, QEquiv)
\import Function ()
\import HLevel
\import Logic
\import Meta
\import Order.PartialOrder
\import Paths
\import Paths.Meta
\import Set
\import Set.Category
\import Set.Fin
\open FinLinearOrder

\func <=-monotone {n m : Nat} (f : Fin n -> Fin m) : \Prop => \Pi {a b : Fin n} -> a <= b -> f a <= f b

\func <=-monotone-unique {n : Nat} {f : Iso {SimplexPrecatI} {n} {n}} : f.f = SimplexHom.id n => run {
  ext,
  ext,
  \lam k => {?}
}
\class SimplexHom \extends SetHom
  | dom : Nat
  | codom : Nat
  | Dom => \new BaseSet (Fin dom)
  | Cod => \new BaseSet (Fin codom)
  | monotone : <=-monotone func \where {
  \func id (n : Nat) : SimplexHom => \new SimplexHom {
    | dom => n
    | codom => n
    | func => Function.id
    | monotone => Function.id
  }
}

\class SimplexPrecat \extends Precat
  | Ob => Nat
  | Hom n m => SimplexHom {
    | dom => n
    | codom => m
  }
  | id _ => \new SimplexHom {
    | func x => x
    | monotone eq => eq
  }
  | o (f, f-monotone) (g, g-monotone) => \new SimplexHom {
    | func => f Function.o g
    | monotone eq => f-monotone (g-monotone eq)
  }
  | id-left => idp
  | id-right => idp
  | o-assoc => idp

\instance SimplexPrecatI : SimplexPrecat

\class SimplexCat \extends Cat, SimplexPrecat

\lemma Simplex_iso {n m : Nat} (iso : Iso {SimplexPrecatI} {n} {m}) : n = m => FinSet.FinCardBij (\new Equiv {
  | f => Iso.f {iso}
  | ret => Iso.hinv {iso}
  | sec => Iso.hinv {iso}
  | ret_f y => pmap {SimplexHom { | dom => n | codom => n } } {Fin n} (\lam h => func {h} y) (Iso.hinv_f {iso})
  | f_sec y => pmap {SimplexHom { | dom => m | codom => m } } {Fin m} (\lam h => func {h} y) (Iso.f_hinv {iso})
})

\func iso_iso {n : Nat} : isProp (Iso {SimplexPrecatI} {n} {n}) => isContr=>isProp (\new Contr {
  | center => SimplexHom.id n
  | contraction a => ext {?}
})

\instance SimplexCatI : SimplexCat
  | univalence {n} {m} => \new QEquiv {
    | ret iso => Simplex_iso iso
    | ret_f _ => set-pi
    | f_sec iso => transport (\lam k => isProp (Iso {SimplexPrecatI} {n} {k})) (Simplex_iso iso) (iso_iso {n}) _ _
  }