Problems defining ABS_CONV

ghost commented 10 years ago

Trying to write general conversions, I need to implement ABS_CONV. Here's a first attempt:

val absConv = conv => tm =>
  match tm
    case 'x ↦ ‹f› x' =>
      val cthms
      context
        let x:'‹x›'
        val norm = normalize '‹f› ‹x›'
        cthms = (match (term norm)
                   case '‹_› = ‹rhs›' =>
                     for cthm in conv rhs do
                       transitive [norm,cthm])
      for cthm in cthms do
        abstract cthm
    case _ => []

There are several problems here. Firstly, the type of the fresh variable x needs to match the variable bound by the lambda abstraction. I cannot compute this type in general and ask fresh to deliver me a variable of that type.

Second, the match will succeed against arbitrary functions. So = is matched setting f to be the term x ↦ (=) x This is undesirable. Perhaps we could have a destabs following destcomb?

phlegmaticprogrammer commented 10 years ago

Hi Phil, have not seen this update before. I think there are no email notifications on an edit, so if you make important changes, please don't edit, but just add a new comment!

Yeah, it looks like we need a destabs function. I am currently adding it.

ghost commented 10 years ago

Apologies for the changes.

Along with destabs, can we have typeof, desttype and also allow the function fresh to take an optional type argument for the fresh variable?

phlegmaticprogrammer commented 10 years ago

I've added a new destabs function: https://github.com/proofpeer/proofpeer-proofscript/wiki/The-ProofScript-Proof-Language, examples are at the end of https://github.com/proofpeer/proofpeer-proofscript/blob/master/scripts/examples/Logic.thy

ghost commented 10 years ago

Since destabs is given me a context value, I do not currently need the other functions. My absConv function works!

proofpeer / proofpeer-proofscript

Problems defining ABS_CONV #32