0

为便于理解而编辑

我试图证明一种特殊类型树的属性。这棵树如下所示。问题是 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 生成的归纳原理不足以证明树的属性。

树的构造如下

Inductive prv_tree (E:BES): (*BES ->*) statement -> Prop := 
.... (*constructors go here*).

这些构造函数之一是

CTX: forall a b c:propForm, forall x:propVar, forall G:propVar_relation,
  (prv_tree E (makeStatement G a b) -> 
    (prv_tree E (makeStatement G (replace c x a) (replace c x b))))

我的目标是证明

Lemma soundness: forall E:BES, forall f g:propForm, forall G:propVar_relation, 
  forall 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 |} =
  {| context := empty_relation; stm_l := replace c x a;
  stm_r := replace c x b |} ->
    E, cc_max E |- replace c x a <,_ empty_relation replace c x b

我不能使用。相反，我想要类似的东西

IHP prv_tree E {| context := G; stm_l := a; stm_r := b |} ->
  E, cc_max E |- replace c x a <,_ empty_relation replace c x b

有人可以向我解释如何解决这个问题吗？到目前为止，我已经尝试在 prv_tree 上定义自己的归纳原理，但是这会导致相同的问题，所以也许我做错了？

我自己的归纳原理中对 CTX 的表述如下：

  (forall a b c:propForm, forall x:propVar, forall G:propVar_relation, 
    (prv_tree E {| context := G; stm_l := a; stm_r := b |} ) ->
      P {| context := G; stm_l := replace c x a; stm_r := replace c x b |})
4

2 回答 2

0

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

于 2016-02-11T14:18:38.803 回答
0

我想我理解你的问题，但我必须完整填写你的问题。正如@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.

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

于 2016-02-11T13:52:55.820 回答