search

siddhartha-gadgil / ProvingGround

Proving Ground: Tools for Automated Mathematics
http://siddhartha-gadgil.github.io/ProvingGround/
MIT License
203 stars 38 forks source link

Skolemization problem #300

Closed siddhartha-gadgil closed 3 years ago

siddhartha-gadgil commented 3 years ago

The skolem bot on parallel chomping gives an error on input:

βˆ‘((``@a : 𝒰 _0) ↦ ((((𝒰 _0) β†’ (((``@a) , (𝒰 _0)))) , ((``@a) β†’ (Zero))))),{},Vector()

as follows:

completed response "skolemizing goal" of type 
TypeTag[Option[provingground.learning.HoTTMessages.Consequence :: provingground.learning.HoTTMessages.SeekGoal :: shapeless.HNil]] 
to posts of type TypeTag[provingground.learning.HoTTMessages.FailedToProve] with input hash -154113873 with error;
java.util.concurrent.ExecutionException: Boxed Exception
        at scala.concurrent.impl.Promise$.scala$concurrent$impl$Promise$$resolve(Promise.scala:99)
        at scala.concurrent.impl.Promise$Transformation.handleFailure(Promise.scala:407)
        at scala.concurrent.impl.Promise$Transformation.run(Promise.scala:469)
        at scala.concurrent.BatchingExecutor$AbstractBatch.runN(BatchingExecutor.scala:141)
        at scala.concurrent.BatchingExecutor$AsyncBatch.apply(BatchingExecutor.scala:163)
        at scala.concurrent.BatchingExecutor$AsyncBatch.apply(BatchingExecutor.scala:146)
        at scala.concurrent.BlockContext$.usingBlockContext(BlockContext.scala:107)
        at scala.concurrent.BatchingExecutor$AsyncBatch.run(BatchingExecutor.scala:154)
        at java.util.concurrent.ForkJoinTask$RunnableExecuteAction.exec(ForkJoinTask.java:1402)
        at java.util.concurrent.ForkJoinTask.doExec(ForkJoinTask.java:289)
        at java.util.concurrent.ForkJoinPool$WorkQueue.runTask(ForkJoinPool.java:1056)
        at java.util.concurrent.ForkJoinPool.runWorker(ForkJoinPool.java:1692)
        at java.util.concurrent.ForkJoinWorkerThread.run(ForkJoinWorkerThread.java:157)
Caused by: java.lang.AssertionError: assertion failed: 
Cannot conclude: 
(βˆ‘((```@a :  𝒰 _0) ↦ ((((((𝒰 _0) β†’ (```@a)) , ((𝒰 _0) β†’ (𝒰 _0)))) , ((```@a) β†’ (Zero)))))) β†’ (βˆ‘((`$lzcugb_1 :  𝒰 _0) ↦ ((((((𝒰 _0) β†’ (`$lzcugb_1)) , ((𝒰 _0) β†’ (𝒰 _0)))) , ((`$lzcugb_1) β†’ (Zero)))))) 
on βˆ‘((```@a :  𝒰 _0) ↦ ((((((𝒰 _0) β†’ (```@a)) , ((𝒰 _0) β†’(οΏ½οΏ½ _0)))) , ((```@a) β†’ (Zero))))) 
gives βˆ‘((``@a :  𝒰 _0) ↦ ((((𝒰 _0) β†’ (((``@a) , (𝒰 _0)))) , ((``@a) β†’ (Zero)))))
        at scala.Predef$.assert(Predef.scala:282)
        at provingground.learning.HoTTMessages$Consequence.$anonfun$new$4(HoTTMessages.scala:406)
        at provingground.learning.HoTTMessages$Consequence.$anonfun$new$4$adapted(HoTTMessages.scala:403)
        at scala.Option.foreach(Option.scala:437)
        at provingground.learning.HoTTMessages$Consequence.<init>(HoTTMessages.scala:403)
        at provingground.learning.HoTTBot$.$anonfun$skolemBot$3(HoTTBot.scala:637)
        at scala.concurrent.Future$.$anonfun$apply$1(Future.scala:671)
        at scala.concurrent.impl.Promise$Transformation.run(Promise.scala:430)
        ... 10 more
siddhartha-gadgil commented 3 years ago

Isolated the issue, which is with skolemization and/or deriving from this.

import provingground._, learning._, interface._, HoTT._
val A = Type.sym
repl.pprinter.bind(translation.FansiShow.fansiPrint)
val tp = sigma(A)(((Type ->: (A && Type)) && (A ->: Zero) ))
val sk = skolemize(tp)
import HoTTMessages._
val y         = sk.Var
val transform = y :~> fromSkolemized(sk)(y)
val cons = Consequence(sk, tp, Option(ExstFunc(transform)), Context.Empty)