如何在 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.

Courtieu的回答有帮助，但我意识到这两个定理是相互依赖的，有必要用

alignof_correct 

来证明

alignof_fields_correct

，我只是暂时想不出一个很好的例子来说明它......

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

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.