Using Omega to prove a lemma in Coq

Link:: https://stackoverflow.com/q/13690147

Display all goals and responses

Question

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.

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.forall n : nat, 2 * div2 n + mod2 n = n

Then this one, using omega and div2_eq:

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

But I did not manage to go further.

Does anyone know what to do?

Answer

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

Require Import FunInd.

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:

div2_ind
     : forall P : nat -> nat -> Prop,
       (forall n : nat, n = 0 -> P 0 0) ->
       (forall n n0 : nat, n = S n0 -> n0 = 0 -> P 1 0) ->
       (forall n n0 : nat,
        n = S n0 ->
        forall p : nat,
        n0 = S p ->
        P p (div2 p) -> P (S (S p)) (S (div2 p))) ->
       forall n : nat, P n (div2 n)mod2_ind
     : forall P : nat -> nat -> Prop,
       (forall n : nat, n = 0 -> P 0 n) ->
       (forall n n0 : nat, n = S n0 -> n0 = 0 -> P 1 n) ->
       (forall n n0 : nat,
        n = S n0 ->
        forall p : nat,
        n0 = S p ->
        P p (mod2 p) -> P (S (S p)) (mod2 p)) ->
       forall n : nat, P n (mod2 n)

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.forall P1 : nat -> Prop,
P1 0 ->
P1 1 ->
(forall n1 : nat, P1 n1 -> P1 (S (S n1))) ->
forall n1 : nat, P1 n1
Proof.forall P1 : nat -> Prop,
P1 0 ->
P1 1 ->
(forall n1 : nat, P1 n1 -> P1 (S (S n1))) ->
forall n1 : nat, P1 n1
  intros P1 H1 H2 H3.P1: nat -> Prop
H1: P1 0
H2: P1 1
H3: forall n1 : nat, P1 n1 -> P1 (S (S n1))
forall n1 : nat, P1 n1 induction n1 as [[| [| n1]] H4] using lt_wf_ind.P1: nat -> Prop
H1: P1 0
H2: P1 1
H3: forall n1 : nat, P1 n1 -> P1 (S (S n1))
H4: forall m : nat, m < 0 -> P1 m
P1 0
P1: nat -> Prop
H1: P1 0
H2: P1 1
H3: forall n1 : nat, P1 n1 -> P1 (S (S n1))
H4: forall m : nat, m < 1 -> P1 m
P1 1
P1: nat -> Prop
H1: P1 0
H2: P1 1
H3: forall n1 : nat, P1 n1 -> P1 (S (S n1))
n1: nat
H4: forall m : nat, m < S (S n1) -> P1 m
P1 (S (S n1))
  -P1: nat -> Prop
H1: P1 0
H2: P1 1
H3: forall n1 : nat, P1 n1 -> P1 (S (S n1))
H4: forall m : nat, m < 0 -> P1 m
P1 0 info_auto.(* info auto: *)
assumption.
  -P1: nat -> Prop
H1: P1 0
H2: P1 1
H3: forall n1 : nat, P1 n1 -> P1 (S (S n1))
H4: forall m : nat, m < 1 -> P1 m
P1 1 info_auto.(* info auto: *)
assumption.
  -P1: nat -> Prop
H1: P1 0
H2: P1 1
H3: forall n1 : nat, P1 n1 -> P1 (S (S n1))
n1: nat
H4: forall m : nat, m < S (S n1) -> P1 m
P1 (S (S n1)) info_auto.(* info auto: *)
simple apply H3.
 simple apply H4.
  unfold lt (in core).
   simple apply le_S (in core).
    simple apply le_n (in core).
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:

Require Import Lia.

Lemma div2_eq : forall n, 2 * div2 n + mod2 n = n.forall n : nat, 2 * div2 n + mod2 n = n
Proof.forall n : nat, 2 * div2 n + mod2 n = n
  induction n as [| | n1 H1] using nat_ind_alt.2 * div2 0 + mod2 0 = 0
2 * div2 1 + mod2 1 = 1
n1: nat
H1: 2 * div2 n1 + mod2 n1 = n1
2 * div2 (S (S n1)) + mod2 (S (S n1)) = S (S n1)
  -2 * div2 0 + mod2 0 = 0 simpl in *.0 = 0 lia.
  -2 * div2 1 + mod2 1 = 1 simpl in *.1 = 1 lia.
  -n1: nat
H1: 2 * div2 n1 + mod2 n1 = n1
2 * div2 (S (S n1)) + mod2 (S (S n1)) = S (S n1) simpl in *.n1: nat
H1: div2 n1 + (div2 n1 + 0) + mod2 n1 = n1
S (div2 n1 + S (div2 n1 + 0) + mod2 n1) = S (S n1) lia.
Qed.

Lemma div2_le : forall n, div2 n <= n.forall n : nat, div2 n <= n
Proof.forall n : nat, div2 n <= n
  induction n as [| | n1 H1] using nat_ind_alt.div2 0 <= 0
div2 1 <= 1
n1: nat
H1: div2 n1 <= n1
div2 (S (S n1)) <= S (S n1)
  -div2 0 <= 0 simpl.0 <= 0 lia.
  -div2 1 <= 1 simpl.0 <= 1 lia.
  -n1: nat
H1: div2 n1 <= n1
div2 (S (S n1)) <= S (S n1) simpl.n1: nat
H1: div2 n1 <= n1
S (div2 n1) <= S (S n1) lia.
Qed.

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