Chain tactic error messages

[jvierling]

The following code should fail because the hyp is not in the antecedent. The code fails as expected, however the error message is rather meaningless.

import gapt.proofs.Sequent
import gapt.proofs.gaptic.{ Proof, chain, trivial }

import gapt.expr._

object Example extends scala.App {

  val chainProof = Proof(
    ( "a" -> hof"q(f(c))" ) +:
      Sequent()
      :+ ( "hyp" -> hof"!x (q x -> p (f x))" )
      :+ ( "target" -> hof"p(f(f(c)))" ) ) {
      chain( "hyp" ).at( "target" )
      trivial
    }

}

The error output is the following:

Exception in thread "main" gapt.proofs.gaptic.TacticFailureException: Exception when applying ChainTactic(hyp,OnLabel(target),Map()) to proof state with sub goals:
a: q(f(c)): o
:-
hyp: ∀x (q(x) → p(f(x)))
target: p(f(f(c))): o

	at gapt.proofs.gaptic.LemmaMacros$.use(macros.scala:24)
	at Example$.$anonfun$chainProof$1(Example.scala:13)
	at gapt.proofs.gaptic.Proof$Helper.handleTacticBlock(language.scala:67)
	at Example$.delayedEndpoint$Example$1(Example.scala:12)
	at Example$delayedInit$body.apply(Example.scala:6)
	at scala.Function0.apply$mcV$sp(Function0.scala:39)
	at scala.Function0.apply$mcV$sp$(Function0.scala:39)
	at scala.runtime.AbstractFunction0.apply$mcV$sp(AbstractFunction0.scala:17)
	at scala.App.$anonfun$main$1(App.scala:75)
	at scala.App.$anonfun$main$1$adapted(App.scala:75)
	at scala.collection.IterableOnceOps.foreach(IterableOnce.scala:576)
	at scala.collection.IterableOnceOps.foreach$(IterableOnce.scala:574)
	at scala.collection.AbstractIterable.foreach(Iterable.scala:904)
	at scala.App.main(App.scala:75)
	at scala.App.main$(App.scala:73)
	at Example$.main(Example.scala:6)
	at Example.main(Example.scala)
Caused by: gapt.proofs.lk.LKRuleCreationException: Cannot create ContractionLeftRule: Formula ∀x (q(x) → p(f(x))) only found 1 times in antecedent of ∀x (q(x) → p(f(x))),
q(f(c)),
q(f(c))
⊢
∀x (q(x) → p(f(x))),
p(f(f(c))),
∀x (q(x) → p(f(x))).
	at gapt.proofs.lk.rules.ConvenienceConstructor.LKRuleCreationException(ConvenienceConstructor.scala:26)
	at gapt.proofs.lk.rules.ConvenienceConstructor.$anonfun$validateIndices$2(ConvenienceConstructor.scala:118)
	at scala.collection.IterableOnceOps.foreach(IterableOnce.scala:576)
	at scala.collection.IterableOnceOps.foreach$(IterableOnce.scala:574)
	at scala.collection.AbstractIterable.foreach(Iterable.scala:904)
	at scala.collection.IterableOps$WithFilter.foreach(Iterable.scala:874)
	at gapt.proofs.lk.rules.ConvenienceConstructor.validateIndices(ConvenienceConstructor.scala:114)
	at gapt.proofs.lk.rules.ConvenienceConstructor.findAndValidate(ConvenienceConstructor.scala:148)
	at gapt.proofs.lk.rules.ContractionLeftRule$.apply(ContractionLeftRule.scala:47)
	at gapt.proofs.gaptic.tactics.ChainTactic.$anonfun$apply$4(complexTactics.scala:104)
	at gapt.proofs.gaptic.Tactic$$anon$4.$anonfun$apply$7(core.scala:226)
	at scala.util.Either.flatMap(Either.scala:354)
	at gapt.proofs.gaptic.Tactic$$anon$4.apply(core.scala:226)
	at gapt.proofs.gaptic.Tactic$$anon$4.$anonfun$apply$7(core.scala:226)
	at scala.util.Either.flatMap(Either.scala:354)
	at gapt.proofs.gaptic.Tactic$$anon$4.apply(core.scala:226)
	at gapt.proofs.gaptic.Tactical1.apply(core.scala:358)
	at gapt.proofs.gaptic.Tactical1.apply$(core.scala:355)
	at gapt.proofs.gaptic.tactics.ChainTactic.apply(complexTactics.scala:55)
	at gapt.proofs.gaptic.LemmaMacros$.use(macros.scala:19)
	... 16 more

[jvierling]

The chain tactic probably does not check properly that hyp belongs to the antecedent.