Help with strong induction

Question

I have the following definition of divisibility by 3.

Inductive div3 : nat -> Prop :=
| div0 : div3 0
| divS : forall n : nat, div3_2 n -> div3 (S n)
with div3_2 : nat -> Prop :=
| div2 : div3_2 2
| div2S : forall n : nat, div3_1 n -> div3_2 (S n)
with div3_1 : nat -> Prop :=
| div1 : div3_1 1
| div1S : forall n : nat, div3 n -> div3_1 (S n).

How can I go about proving the following lemma?

Lemma practice : forall n : nat, div3 n -> exists m, n = 3 * m.

Answer 1

As div3 is defined using a mutual inductive definition with div3_1 and div3_2. The stronger statement you may try to prove is

Lemma practice : 
  (forall n : nat, div3 n -> exists m, n = 3 * m) /\
  (forall n : nat, div3_1 n -> exists m, n = 3 * m + 1) /\
  (forall n : nat, div3_2 n -> exists m, n = 3 * m + 2).

Answer 2

A possible solution is to prove a slightly modified version of practice by a single induction on n, using inversion tactics.

Lemma practice n : 
   (div3 n -> exists m, n = 3 * m) /\
   (div3_1 n -> exists m, n = S (3 * m)) /\
   (div3_2 n -> exists m, n = 2 + 3 * m ).
Proof. 
  induction n. 
  - repeat split; now exists 0. 
  -  destruct IHn as [H0 [H1 H2]]; repeat split.
     + inversion_clear 1.  
       destruct (H2 H3) as [x Hx]; exists (S x); subst; ring. 
     + inversion  1. 
        * subst n; exists 0; ring. 
        * subst n0; destruct (H0 H4) as [x Hx]; exists x; now subst. 
     + inversion 1.
       * subst n ; now exists 0. 
       * destruct (H1 H4) as [x Hx];  subst ; exists x; ring. 
Qed.

For a better understanding, you may replace the use of inversion with diy "inversion lemmas" .

Lemma div3_inv n : div3 n -> n = 0 \/ exists p, n = S p /\ div3_2 p.
Proof. 
  destruct 1 as [|n Hn].
  - now left.   
  - right; exists n; auto. 
Qed. 

(* ... *)