在焊机中进行双重感应

Question

我试图通过使用焊机的双重归纳来证明一个属性。定义取自此处。可以在此处找到提供有关该理论更多详细信息的相关问题。无论如何，我只需要一些部分来显示我的问题：

基本上，我正在使用采用整数，POP(i,p)和POW(i,p,q)形式的表达式。他们身上有一种正常性，称之为n。我想证明，如果n(x) && n(y)那么n(x+y).

让我们看一下具体情况x = POP(i,p)，y = POP(j,q)然后x+y定义如下：

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)

其中pop是一个模仿POP构造的函数，但有一些细微的差异。

我在焊机中通过双感应进行证明，如下所示：

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{
...

我想重点介绍的相关案例如下：

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))

}
)

在这里，normpop1Lemma指出，要拥有n(pop(i,p))，你需要i自然和p正常。但是，我发现第二种情况没有得到证实。事实上，我需要将第二个属性推广到

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

但是我不是打破了感应吗？我真的可以解决i > j和i < j的情况吗？(更多内容将在我实验时推出)

编辑

目前，我可以先在 y 上引入，然后在 x 上引入，对于 POP-POP 案例，我可以显示i = j和i > j但i < j不是的情况。我认为它可以通过使用该POP(j-i,q) + p = p + POP(j-i,q)起作用，但事实并非如此。

相反，现在我试图证明两个不同的属性，假设每个属性中的一个情况不能成立(i < j或i > j)。

Answer 1

嗯，我希望你的证明看起来像这样：

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
)
}
)
}
}
}
}

在这里，我们使用来自外部归纳的归纳假设，因为我们在p in x上执行归纳。我假设normprop1Lemma告诉你normadd(POP(j-i,qshf))是正常形式的。您可能需要一些引理，说明如果p in x处于正常形式x则处于正常形式。

希望这有帮助！