Proof Assistants Stack Exchange is a question and answer site for mathematicians and computer scientists who develop and use proof assistants. It only takes a minute to sign up.
Sign up to join this community
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.
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).
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.
(* ... *)
