CODEWITHSUNDEEP
coqproofinduction
Flo
Flo

Reputation: 41

Using Omega to prove a lemma in Coq

I am trying to make a proof in Coq using Omega. I spent a lot of time on it, but nothing came to me. I have to say I am new in Coq, so I am not at ease with this kind of language, and I do not have much experience. But I am working on it.

Here's the code I have to prove:

Require Import Arith Omega.

Fixpoint div2 (n : nat) :=
 match n with
   S (S p) => S (div2 p)
 | _ => 0
 end.

Fixpoint mod2 (n : nat) :=
 match n with
   S (S p) => mod2 p
 | x => x
 end.

To make this proof, I thought it would help to prove by induction this lemma first:

Lemma div2_eq : forall n, 2 * div2 n + mod2 n = n.

Then this one, using omega and div2_eq :

Lemma div2_le : forall n, div2 n <= n.

But I did not manage to go further.

Does anyone know what to do?

Upvotes: 3

Views: 896

Answers (1)

user1861759
user1861759

Reputation:

You can easily derive induction principles from the functions div2 and mod2 like so:

Functional Scheme div2_ind := Induction for div2 Sort Prop.
Functional Scheme mod2_ind := Induction for mod2 Sort Prop.

div2_ind and mod2_ind have more or less types:

forall P1,
  P1 0 0 ->
  P1 1 0 ->
  (forall n1, P1 n1 (div2 n1) -> P1 (S (S n1)) (S (div2 n1))) ->
  forall n1, P1 n1 (div2 n1)

forall P1,
  P1 0 0 ->
  P1 1 1 ->
  (forall n1, P1 n1 (mod2 n1) -> P1 (S (S n1)) (mod2 n1)) ->
  forall n1, P1 n1 (mod2 n1)

To apply these theorems you can conveniently write functional induction (div2 n) or functional induction (mod2 n) where you might usually write induction n.

But a stronger induction principle is associated with these functions:

Lemma nat_ind_alt : forall P1 : nat -> Prop,
  P1 0 ->
  P1 1 ->
  (forall n1, P1 n1 -> P1 (S (S n1))) ->
  forall n1, P1 n1.
Proof.
intros P1 H1 H2 H3. induction n1 as [[| [| n1]] H4] using lt_wf_ind.
  info_auto.
  info_auto.
  info_auto.
Qed.

In fact, the domain of any function is a clue to a useful induction principle. For example, the induction principle associated to the domain of the functions plus : nat -> nat -> nat and mult : nat -> nat -> nat is just structural induction. Which makes me wonder why Functional Scheme doesn't just generate these more general principles instead.

In any case, the proofs of your theorems then become:

Lemma div2_eq : forall n, 2 * div2 n + mod2 n = n.
Proof.
induction n as [| | n1 H1] using nat_ind_alt.
  simpl in *. omega.
  simpl in *. omega.
  simpl in *. omega.
Qed.

Lemma div2_le : forall n, div2 n <= n.
Proof.
induction n as [| | n1 H1] using nat_ind_alt.
  simpl. omega.
  simpl. omega.
  simpl. omega.
Qed.

You should familiarize yourself with functional induction, but more importantly, you should really familiarize yourself with well-founded induction.

Upvotes: 4

Related Questions