如何在 Coq 中证明递归定义函数的属性

Question

我试图在 Coq 中证明一个叫做 alignof_correct 的引理，它验证我为一个类型定义的 alignof 函数返回一个正值。我已经定义了类型和函数，并导入了 ZArith 库。

Require Import ZArith.

Inductive type :=
| Tstruct : nat -> fieldlist -> type
with fieldlist :=
| Fnil : fieldlist
| Fcons : nat -> type -> fieldlist -> fieldlist.

Fixpoint alignof (ty: type): Z :=
  match ty with
  | Tstruct _ fld => alignof_fields fld
  end
with alignof_fields (fld: fieldlist): Z :=
  match fld with
  | Fnil => 1
  | Fcons _ ty fld' => Z.max (alignof ty) (alignof_fields fld')
  end.

Lemma alignof_fields_correct: forall (fld: fieldlist),
    (alignof_fields fld > 0)%Z.
Proof.
Admitted.

Lemma alignof_correct : forall (ty : type),
  (alignof ty > 0)%Z.
Proof.
  intros ty. induction ty.
  simpl. apply Z.gt_lt_iff. 
  admit.
Admitted.

任何人都可以为我提供一些关于如何证明这些的指导吗？谢谢！

Answer 1

通常的方法是证明互引理：

Lemma alignof_correct : forall (ty : type),
  (alignof ty > 0)%Z
with alignof_fields_correct: forall (fld: fieldlist),
    (alignof_fields fld > 0)%Z.
Proof.
  - intros ty. induction ty;try now reflexivity.
    + simpl. apply IHty.
    + simpl. 
      apply alignof_fields_correct.
  - induction fld.
    + simpl. auto with zarith.
    + simpl.
      auto with zarith.
Qed.

也就是说，第二个证明没有使用互感假设，所以在这种特殊情况下，您可以先单独证明

field

的东西：

Lemma alignof_fields_correct: forall (fld: fieldlist),
    (alignof_fields fld > 0)%Z.
Proof.
  induction fld.
    + simpl. auto with zarith.
    + simpl.
      auto with zarith.
Qed.

Lemma alignof_correct : forall (ty : type),
  (alignof ty > 0)%Z.
Proof.
  intros ty.
  induction ty;try now reflexivity.
  + simpl. apply IHty.
  + simpl. 
    apply alignof_fields_correct.
Qed.

Answer 2

提供的初始示例是为了证明对齐是积极的，Courtieu 的回答有所帮助。而且我意识到这两个定理是相互依赖的，需要用alignof_correct来证明alignof_fields_correct，这不是一个很合适的例子：

Inductive alignof_prop: type -> Z -> Prop :=
  | alignof_Tbool : alignof_prop Tbool 1
  | alignof_Toption : 
    forall ty z,
    alignof_prop ty z ->
    alignof_prop (Toption ty) z
  | alignof_Tstruct : 
    forall i fld z,
    alignof_fields_prop fld z ->
    alignof_prop (Tstruct i fld) z
with alignof_fields_prop: fieldlist -> Z -> Prop :=
  | alignof_fields_nil : 
    alignof_fields_prop Fnil 1
  | alignof_fields_cons : 
    forall i ty fld z1 z2,
    alignof_prop ty z1 ->
    alignof_fields_prop fld z2 ->
    alignof_fields_prop (Fcons i ty fld) (Z.max z1 z2).

所以我们可以得到这个：

Lemma alignof_correct:
  forall ty,
  alignof_prop ty (alignof ty)
  with alignof_fields_correct:
  forall f,
  alignof_fields_prop f (alignof_fields f).
Proof.
  induction ty; simpl; econstructor. auto. apply alignof_fields_correct.
  induction f; simpl; econstructor. apply alignof_correct. auto.
Qed.

附言也许我不太清楚在描述定理时“with”是如何工作的。谁能告诉我在哪里可以找到相关的参考资料？

Answer 3

有一个简单的互感p的例子。 400 个

https://www-sop.inria.fr/members/Yves.Bertot/coqart-chapter14.pdf

最近版本的 Coq 的脚本维护在

https://github.com/coq-community/coq-art/tree/master/ch14_fundations_of_inductive_types/SRC

希望这可能有所帮助。