induction integer record in coq

Question

The definition of int comes from compcert,

Record int: Type := mkint { intval: Z; intrange: -1 < intval < modulus }.

I wanna prove foo, suppose that the induction strategy needs to be used, because there is a recursive relationship in P1 and P2, and i is positive in P1 and P2 actually.

From compcert Require Import Integers.

Parameter P1 : int -> Prop.
Parameter P2 : int -> Prop.

Theorem foo: 
    forall i: int,
    (P1 i) -> (P2 i).
Proof.
    destruct i. induction intval.
    admit.
    induction p.
Abort.

If induction p, I need to prove two cases, BinNums.Zpos (BinNums.xI p) and BinNums.Zpos (BinNums.xO p). it is hard to prove, I would like to be able to use int like nat, that is something to prove P1 (i + 1) -> P2 (i + 1) by (P1 i) -> (P2 i)

Any hints? thank you very much!

Answer 1

The fact that you are using int numbers from CompCert makes everything more complicated, because there is too little arithmetic available for this datatype.

If you were using just plain integers of type Z, you would be able to perform the proof you require by using well_founded_induction and Zwf.Zwf_well_founded. Here is an example.

Theorem foo: 
    forall i: Z, (0 <= i)%Z -> P i.
intros i.
induction i using 
  (well_founded_ind (Zwf.Zwf_well_founded 0)).
Print Zwf.
intros ige0.
assert (cases : (i = 0 \/ 0 < i)%Z) by lia.
destruct cases as [case0 | casegt0].
  rewrite case0.
  now apply base_case.
assert (dec : i = ((i - 1) + 1)%Z) by lia.
rewrite dec.
apply rec_case.
apply H.
  unfold Zwf.
  lia.
lia.
Qed.

Now, if we want to make a similar proof using numbers of type int, life is more complicated because these numbers are in a record, and this record contains a field that is a proof. Usually, the value of the proof is irrelevant, only its existence matters, in in this case we would rather have the intval projection be injective. To make it short, I simply place myself in a theoretical setting where this is granted, this well known and acceptable in most use cases. Here is the full example:

Require Import ZArith Zwf.
Require Import Wellfounded.
Require Import Lia.
Require Import ProofIrrelevance.

Open Scope Z_scope.

Parameter modulus : Z.

Hypothesis modulus_gt_0 : 0 < modulus.

Record int : Type := mkint {intval : Z; intrange: -1 < intval < modulus}.

Lemma intval_inj : forall x y : int, intval x = intval y -> x = y.
Proof.
intros [x xp] [y yp]; simpl. 
intros xy; revert xp; rewrite xy; intros xp.
now rewrite (proof_irrelevance _ xp yp).
Qed.

Definition int0 := mkint 0 (conj eq_refl modulus_gt_0).

Parameter P : int -> Prop.

Axiom base_case : P int0.

Lemma modulo_Z_bound (z : Z) : -1 < z mod modulus < modulus.  
Proof.
assert (tmp := Z.mod_pos_bound z modulus modulus_gt_0).
lia.
Qed.

Axiom rec_case : forall x, P x -> P (mkint _ (modulo_Z_bound (intval x + 1))).

Theorem foo: forall i, P i.
intros i; destruct i as [z zbounds].
revert zbounds.
induction z as [z Ih] using (well_founded_ind (Zwf_well_founded 0)).
intros zbounds.
assert (cases : z = 0 \/ 0 < z) by lia.
destruct cases as [case0 | casegt0].
  revert zbounds; rewrite case0.
  intros zbounds; assert (isint0 : {|intval := 0; intrange := zbounds|} = int0).
    now apply intval_inj; simpl.
  now rewrite isint0; apply base_case.
assert (zm1_bounds : -1 < z - 1 < modulus) by lia.
assert (dec : {| intval := z; intrange := zbounds|} =
        mkint _ (modulo_Z_bound (intval (mkint _ zm1_bounds) + 1))).
  apply intval_inj; simpl.
  replace (z - 1 + 1) with z by ring.
  symmetry; apply Z.mod_small; lia.
rewrite dec.
apply rec_case.
apply Ih.
unfold Zwf.
lia.
Qed.

Note that mkint _ (modulo_Z_bound (intval x + 1)) is just a way to write x + 1 when x has type int (with the convention that the successor of the largest number is 0).

There is a way to avoid using the proof_irrelevance axiom, but this would make this answer even longer.