Performing double induction in Welder

Question

I'm trying to proof a property by double induction using Welder. The definitions are taken from here. A related question that gives more details of the theory can be found here. Anyways I just need some portion to show my problem:

Basically, I'm working with expressions that take the form of an integer, POP(i,p) and POW(i,p,q). There is a property of normality on them call it n. I want to proof that if n(x) && n(y) then n(x+y).

Let's look at the specific case x = POP(i,p), y = POP(j,q) then x+y is defined as follows:

if i = j then pop(i,p+q)
if i > j then pop(j,POP(i-j,p)+q)
if i < j then pop(i,POP(j-i,q)+p)

where pop is a function that mimics POP constructs with some slight differences.

I perform the proof by double induction in Welder as follows:

def property(x: Expr) = {
  forall("y" :: shf){ case (y) => 
    (n(x) && n(y)) ==> n(x+y)
  } 
}
structuralInduction(property _, "x" :: shf) { case (ihs1, goal1) =>
  val xi = ihs1.expression
  xi match{
  ...

The relevant case I want to focus is the following:

case C(`POP_ID`,i,pshf) =>
  def popproperty(y: Expr) = { 
    n(y) ==> n(xi+y) 
  }
  structuralInduction(popproperty _, "y" :: shf) { case (ihs2, goal2) =>
   val yi = ihs2.expression
   implI(n(yi)){ axioms2 =>
    yi match{
     case C(`constshfID`, fc) => andI(ihs1.hypothesis(pshf),axioms1)
     case C(`POP_ID`,j,qshf) => 
      andI(
       implE(forallE(normpop1Lemma)(i,normadd(pshf,qshf)))( g => 
        andI(implE(forallE(ihs1.hypothesis(pshf))(qshf))( g => 
         andI(axioms1,axioms2)), axioms1, axioms2)),
       implI(i > j){ gt => 
        implE(forallE(normpop1Lemma)(i,normadd(POP(i-j,pshf),qshf)))( g => 
         andI(implE(ihs2.hypothesis(qshf))(g => axioms2),axioms1,axioms2,gt))                            
       },
       implI(i < j){ lt => 
        implE(forallE(normpop1Lemma)(i,normadd(POP(j-i,pshf),qshf)))( g => 
         andI(implE(ihs2.hypothesis(qshf))(g => axioms2),axioms1,axioms2,lt))
                            
    }
   )

Here normpop1Lemma states that for having n(pop(i,p)) you need i to be natural and p normal. However, I find that the second case is not proved. In fact I would need to generalize the second property to

def popproperty(y: Expr) = { 
  forall("x" :: shf){
   n(y) ==> n(x+y) 
  }
}

but then am I not breaking induction? Can I actually solve the cases i > j and i < j by doing so? (more to come while I experiment)

Edit

Currently, I can induct first on y and then on x and for the POP-POP case I can show the cases where i = j and i > j but the i < j is not. I thought it could work by using that POP(j-i,q) + p = p + POP(j-i,q) but it doesn't.

Instead, now I'm trying to proof two different properties assuming in each that the one of the cases cannot hold (either the i < j or the i > j).

score 1 · Accepted Answer · answered May 21 '17 at 15:53

Hmm, I would expect your proof to look something more like this:

structuralInduction((x: Expr) =>
  forall("y" :: shf)(y => (n(x) && n(y)) ==> n(x+y)), "x" :: shf
) { case (ihs1, g1) =>
  structuralInduction((y: Expr) =>
    (n(ihs1.expression) && n(y)) ==> n(ihs1.expression+y), "y" :: shf
  ) { case (ihs2, g2) =>
    implI(n(ihs1.expression) && n(ihs2.expression)) { normalXY =>
      (ihs1.expression, ihs2.expression) match {
        case (C(`POP_ID`,i,pshf), C(`POP_ID`,j,qshf)) => andI(
           ... // case (i == j)
           ... // case (i > j)
           implI(i < j) { iLtJ =>
             andI(
               ... // stuff using normprop1Lemma
               implE(forallE(ihs1.hypothesis(pshf))(normadd(POP(j-i,qshf)) {
                 g => // the reason why n(normadd(POP(j-i,qshf)) and n(pshf)
               },
               ... // invoke some lemma showing x+y == y+x
             )
           }
        )
      }
    }
  }
}

Here we use the induction hypothesis from the outer induction since we're performing induction on p \in x. I assume normprop1Lemma is telling you that normadd(POP(j-i,qshf)) is in normal form. You will probably need some lemma stating that p \in x is in normal form if x is in normal form.

Hope this helps!

Performing double induction in Welder

1 Answers1