Coq生成的归纳原理不像我希望的那样。

Question

为便于理解而编辑的

我试图证明一种特殊类型的树的属性。这棵树如下所示。问题是Coq生成的归纳原理不足以证明树的性质。对于一个更简单的例子，假设下面的类型描述了我所有的“树”：

Inductive prv_tree(E:BES) : statement -> Prop :=
| REFL (G:propVar_relation)(a:Prop) : 
  prv_tree E (G |- a ---> a)
| TRA (G:propVar_relation) (a b c:Prop) :
  prv_tree E (G |- a ---> b) -> prv_tree E (G |- b ---> c) ->
    prv_tree E (G |- a ---> c).

然后，为了证明所有树的稳健性(例如，蕴涵)，我需要证明以下引理：

Lemma soundness: forall E:BES, forall f g:Prop, forall R G:propVar_relation, 
  (prv_tree E (G |- f ---> g)) -> (E,G,R |= f --> g).

我需要在树的结构上应用归纳。但是，如果我执行intros;induction H.，那么第一个子目标是(E,G,R |= f --> g)，即关于f和g所需结构的信息丢失了(我想要(E,G,R |= a --> a))。(此外，在归纳案例中，归纳假设陈述了(E,G,R |= f --> g)，对我来说这似乎很奇怪)。

我尝试过的另一种方法是记住(G |- f ---> g)，保持f和g的结构可用。然后作为intros;remember (G |- f --> g) as stmt in H.induction H.继续证明，然后，我获得目标和环境，就像我对我的基本案例所期望的那样。然而，为了证明TRA案件，我获得了以下证明上下文：

H : prv_tree E (G0 |- a --> b)
H0 : prv_tree E (G0 |- b --> c)
IHprv_tree1 : G0 |- a --> b = G |- f --> g -> (E,G,R |= f --> g)
IHprv_tree2 : G0 |- b --> c = G |- f --> g -> (E,G,R |= f --> g)

虽然我希望归纳假设是

IHprv_tree1 : prv_tree E (G0 |- a --> b) -> (E,G,R |= a --> b)
IHprv_tree2 : prv_tree E (G0 |- b --> c) -> (E,G,R |= b --> c)

旧文本

我试图证明一种特殊类型的树的属性。这棵树可以使用21个不同的规则来构建(我不会在这里重复这些规则)。问题是Coq生成的归纳原理不足以证明树的性质。 这棵树的构造如下 归纳prv_tree (E:BES)：(*BES ->*)语句-> Prop := .(*建设者到这里来*) 其中一个构造函数是 G:propVar_relation，(prv_tree E (makeStatement G A b) -> (prv_tree E(替换c x a) (代替c x b) 我的目标是证明 引理稳健性:对于所有的E:BES，对于所有的f_ g : G:propVar_relation，对于所有的tree:prv_tree E (makeStatement G_F_ g)，rel_cc_on_propForm E (cc_max _ E) G_f_g。 为了做到这一点，我记得makeStatement G f g，因为否则我会丢失f和g结构的信息，然后在树上应用归纳。我已经证明了所有的情况是分开的引理，我可以成功地用在基本的情况下。然而，对于归纳情况，Coq给我的归纳假设是不可用的。 例如，对于前面提到的CTX构造函数，我得到了以下归纳假设： IHP { context := G；stm_l := a；stm_r := b\}={ stm_r context := empty_relation；stm_l :=替换c x a；stm_r :=替换c}\ -> E，cc_max E_x-替换c x_a <，_ empty_relation替换c_x 我不能用。相反，我想要的是 IHP prv_tree E {声上下文:= G；stm_l := a；stm_r := b=} -> }->，cc_max E=--替换c <，_ empty_relation替换c 谁能给我解释一下怎么解决这个问题吗？到目前为止，我已经尝试在prv_tree上定义我自己的归纳原则，但是这会导致同样的问题，所以也许我做错了吗？ CTX在我自己的归纳原则中的陈述如下： (对于a、b、c:propForm，forall x:propVar，forall G:propVar_relation，(prv_tree E{ stm_l context := G；stm_l := a；stm_r := b}) -> P{ := G；stm_l :=替换c；stm_r :=替换c\})

Answer 1

我想我理解你的问题，但我必须填写你问题的全部内容。如果你能想出一个完整的例子，就更容易了，就像@ejgallego建议的那样。

下面是我如何建模您的问题：

Axiom BES : Type.
Axiom propVar_relation : Type.

Inductive statement :=
| Stmt : propVar_relation -> Prop -> Prop -> statement.

Notation "G |- a ---> b" := (Stmt G a b) (at level 50).

Inductive prv_tree(E:BES) : statement -> Prop :=
| REFL (G:propVar_relation)(a:Prop) : 
  prv_tree E (G |- a ---> a)
| TRA (G:propVar_relation) (a b c:Prop) :
  prv_tree E (G |- a ---> b) -> prv_tree E (G |- b ---> c) ->
    prv_tree E (G |- a ---> c).

Lemma soundness: forall (E: BES) (f g:Prop) (R G:propVar_relation),
  (prv_tree E (G |- f ---> g)) -> R = R.

事实上，我们遇到的问题与你在问题中所描述的问题相同。解决方案是在记忆之后和进行归纳之前进行revert。

intros.
remember (G |- f ---> g) as stmt. revert f g R G Heqstmt.
induction H; intros.

现在，归纳假设仍然很奇怪，但它们应该有效。

Answer 2

谢谢你的帮助。最后，我自己找到了解决办法。诀窍是定义一个助手函数h:statement -> Prop，正如归纳原理所期望的那样，并使用该函数代替(E,G,R |= f --> g)。