How to proof recursively defined functions' prop in Coq

Question

I am trying to prove a lemma called alignof_correct in Coq, which verifies that the alignof function I defined for a type returns a positive value. I have defined the types and the function, and imported the ZArith library.

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_correct : forall (ty : type),
  (alignof ty > 0)%Z.
Proof.
  intros ty. induction ty.
  simpl. apply Z.gt_lt_iff. 
  admit.
Admitted.

Can anyone provide me with some guidance on how to prove these? Thank you!!

Answer 1

The usual way is to prove mutual lemmas:

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.

That said the second proof does not make use of the mutual induction hypothesis so in this particular case you can prove the field stuff alone first:

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.