phlegmaticprogrammer
commented
9 years ago This is actually a bug in KernelImpl.findCommonAncestors
Closed phlegmaticprogrammer closed 9 years ago
phlegmaticprogrammer
commented
9 years ago This is actually a bug in KernelImpl.findCommonAncestors
Hey man. I'm having trouble understanding how contexts work in proofscript. I'm trying to implement a matching modus ponens rule. I've attached a couple of files.
The function "matcher" takes a term pattern t and a pattern u and a list of constants in t which are taken to be "variables". It then produces an instantiation of these variables θ such that t[θ] = u.
The function "matchmp" then takes an implication and a bunch of antecedents, and does matching modus ponens. The code works, but I'm not sure why I have to use "theorem" in the body of matchmp. I wanted to just write
def matchmp (imp <+ ants) = def matchmp1 [imp,ant] = def mp ['∀ x. ‹imp› x',vs] = val (ctx,x,imp) = destabs imp context
return mp (imp,vs +> x)
mp ['‹p› → ‹q›',vs] =
val inst =
for bnd in matcher (term ant,p,vs) do
match bnd
case [x,v] => x
case v => v
modusponens (ant,instantiate ([imp] ++ inst))
mp (imp,[])
for ant in ants do
imp = matchmp1 (imp,ant)
imp
but when I do that, it complains on the second trip round that last for loop, using the second antecedent, something about there not being a common ancestor context in the line
modusponens (ant,instantiate ([imp] ++ inst))
Using theorem as in the attached file seems to fix this, but I don't understand why.