Open sankalpgambhir opened 1 year ago
A comment here mentions that the type alias is equivalent, but there seems to be some weird casting happening in the background.
https://github.com/epfl-lara/lisa/blob/657acdde3aac6f6c52af545238d89c19c3e1e396/lisa-utils/src/main/scala/lisa/utils/tactics/SimpleDeducedSteps.scala#L26
Consider the following:
val testThm = makeTHM("'P('x) ⇒ 'P('f('x)) ⊢ 'P('x) ⇒ 'P('f('x))") { ... } val test1 = makeTHM("'P('x) ⇒ 'P('f('x)) ⊢ 'P('x) ⇒ 'P('f('x))") { have("'P('x) ⇒ 'P('f('x)) ⊢ 'P('x) ⇒ 'P('f('x))") by Rewrite(thm"testThm") } val test2 = makeTHM("'P('x) ⇒ 'P('f('x)) ⊢ 'P('x) ⇒ 'P('f('x))") { have("'P('x) ⇒ 'P('f('x)) ⊢ 'P('x) ⇒ 'P('f('x))") by Restate(thm"testThm") }
test1 compiles and checks through the kernel, while test2 raises a type error:
test1
test2
[error] -- [E134] Type Error: /home/sankalp/projects/lisa/lisa-working2/lisa-examples/src/main/scala/Exercise.scala:31:57 [error] 31 | have("'P('x) ⇒ 'P('f('x)) ⊢ 'P('x) ⇒ 'P('f('x))") by Restate(thm"testThm") [error] | ^^^^^^^ [error] |None of the overloaded alternatives of method apply in object Restate with types [error] | (using proof: lisa.utils.Library#Proof) [error] | (premise: proof.ProofStep | proof.OutsideFact | Int) [error] | (bot: lisa.kernel.proof.SequentCalculus.Sequent): proof.ProofTacticJudgement [error] | (using proof: lisa.utils.Library#Proof) [error] | (bot: lisa.kernel.proof.SequentCalculus.Sequent): proof.ProofTacticJudgement [error] |match arguments (lisa.settheory.SetTheoryLibrary.theory.Theorem) [error] one error found
For reference, here is the type signature of Rewrite:
Rewrite
https://github.com/epfl-lara/lisa/blob/657acdde3aac6f6c52af545238d89c19c3e1e396/lisa-utils/src/main/scala/lisa/utils/tactics/BasicStepTactic.scala#L36
That's a scala 3 bug. Not much to do about it except finding a work arround.
Despite the closing of #120, this one continues to struggle (just tried).
A comment here mentions that the type alias is equivalent, but there seems to be some weird casting happening in the background.
https://github.com/epfl-lara/lisa/blob/657acdde3aac6f6c52af545238d89c19c3e1e396/lisa-utils/src/main/scala/lisa/utils/tactics/SimpleDeducedSteps.scala#L26
Consider the following:
test1
compiles and checks through the kernel, whiletest2
raises a type error:For reference, here is the type signature of
Rewrite
:https://github.com/epfl-lara/lisa/blob/657acdde3aac6f6c52af545238d89c19c3e1e396/lisa-utils/src/main/scala/lisa/utils/tactics/BasicStepTactic.scala#L36