## Stream: Coq users

### Topic: Prove even number in Prop

#### Julin S (Aug 18 2023 at 10:04):

Hi. I was trying to prove this.

But stuck at the last goal.

``````Inductive even: nat -> Prop :=
| EvenO: even 0
| EvenSS: forall n:nat,
even n -> even (S (S n)).

(* [Nat.even] itself *)
Fixpoint evenb (n:nat): bool :=
match n with
| O => true
| S O => false
| S (S n') => evenb n'
end.

Theorem evenBP: forall n:nat,
evenb n = true -> even n.
Proof.
intros n H.
induction n.
- constructor.
-
``````

The goal at this point was:

``````1 subgoal

n : nat
H : evenb (S n) = true
IHn : evenb n = true -> even n

========================= (1 / 1)

even (S n)
``````

Any idea how this can proceed?

#### Michael Soegtrop (Aug 18 2023 at 10:16):

Direct induction over even things is tricky, since the functions increment in steps of two. You could first prove e.g. that `even (S n) = negb (even n)` this should be easier because it doesn't have premises which are true only in every 2nd iteration. Then you can rewrite with this in H and destruct `evenb n`. The other option is to define a special induction scheme which requires `P 0`, `P 1` and `P n -> P (S (Sn))`.

#### Gaëtan Gilbert (Aug 18 2023 at 10:25):

you need a more complicated induction, `even` goes 2 steps at a time so the induction needs to talk about 2 steps in some way
for instance

``````Require Import Bool.

Inductive even: nat -> Prop :=
| EvenO: even 0
| EvenSS: forall n:nat,
even n -> even (S (S n)).

(* [Nat.even] itself *)
Fixpoint evenb (n:nat): bool :=
match n with
| O => true
| S O => false
| S (S n') => evenb n'
end.

Lemma evenb_S n : evenb (S n) = negb (evenb n).
Proof.
induction n.
- reflexivity.
- rewrite IHn; clear IHn.
symmetry; apply negb_involutive.
Qed.

Theorem evenBP: forall n:nat,
if evenb n then even n else even (pred n).
Proof.
intros n.
induction n.
- simpl;constructor.
- rewrite evenb_S.
destruct (evenb n) eqn:H;simpl;auto.
destruct n.
* inversion H.
* constructor; assumption.
Qed.

(* the proof for this one is a bit simpler: no need for eqn:H in the destruct *)
Theorem evenBP': forall n:nat,
if evenb n then even n else even (S n).
Proof.
intros n.
induction n.
- simpl;constructor.
- rewrite evenb_S.
destruct (evenb n);simpl.
* constructor; assumption.
* assumption.
Qed.
``````

#### James Wood (Aug 18 2023 at 10:28):

I think the alternative to a custom step-by-2 induction is to use mutual induction. You can define `even` mutually with `odd`, and `evenb` mutually with `oddb`, and then do proofs about them simultaneously.

#### James Wood (Aug 18 2023 at 10:29):

Also, you can consider using `Fixpoint` for proofs, as in:

``````Fixpoint evenBP n : evenb n = true -> even n.
Proof.
intro H.
destruct n as [|[|n]].
- constructor.
- inversion H.
- constructor.
apply evenBP.
exact H.
Qed.
``````

#### Paolo Giarrusso (Aug 18 2023 at 10:48):

I've used Fixpoint for proofs, but it's somewhat fragile because guard-checking is deferred and you have "unsafe" hypotheses that automation will use.

IMHO: Do you only need the induction principle once and/or is a fully manual proof appropriate? Then maybe it's a good idea. Otherwise, a bit of extra boilerplate for the principle will make maintenance easier.

#### Julin S (Aug 20 2023 at 11:01):

James Wood said:

Also, you can consider using `Fixpoint` for proofs

In this case, because of the recursive call, we didn't have to use `induction` tactic, right?

And the trick involving `destruct n as [|[|n]]` is new to me.
It takes care of first two case explicitly and then uses n for the remaining cases, is it?
`[||[[|n]]]` allows us to deal with first 3 cases explicitly.

#### Julin S (Aug 20 2023 at 11:02):

Paolo Giarrusso said:

I've used Fixpoint for proofs, but it's somewhat fragile because guard-checking is deferred and you have "unsafe" hypotheses that automation will use.

The first time I tried a fixpoint in proof mode, I was puzzled why the proof couldn't be closed despite having no more goals. Till someone told me about the deferred guardedness thing.

Paolo Giarrusso said:

IMHO: Do you only need the induction principle once and/or is a fully manual proof appropriate? Then maybe it's a good idea. Otherwise, a bit of extra boilerplate for the principle will make maintenance easier.

Yeah, fixpoint like here can make tactics take forbidden paths, I suppose.

#### James Wood (Aug 20 2023 at 11:10):

Julin S said:

In this case, because of the recursive call, we didn't have to use `induction` tactic, right?

Yeah. The Gallina analogue is that you use `Fixpoint` to define `evenb`, rather than doing `Definition evenb (n : nat) : bool := nat_rec ...`. Something has to provide the recursion (via `fix` in the core language), and that can be either `Fixpoint` or `induction`.

Julin S said:

And the trick involving `destruct n as [|[|n]]` is new to me.
It takes care of first two case explicitly and then uses n for the remaining cases, is it?
`[||[[|n]]]` allows us to deal with first 3 cases explicitly.

Have you seen tactics like `induction n as [|n IH].`? In this case, the square brackets are providing names for the newly bound variables in each case/branch of the proof. The extension I used in this case was that you can nest square brackets to do further destruction.

#### James Wood (Aug 20 2023 at 11:15):

I guess this is the relevant part of the manual, though it doesn't seem very digestible aside from the examples: https://coq.inria.fr/refman/proof-engine/tactics.html#intro-patterns .

#### Julin S (Aug 20 2023 at 11:25):

James Wood said:

Have you seen tactics like `induction n as [|n IH].`? In this case, the square brackets are providing names for the newly bound variables in each case/branch of the proof

Yeah, I knew the notation, but didn't realize it could be used like this. :)

#### Julin S (Aug 20 2023 at 11:39):

James Wood said:

I think the alternative to a custom step-by-2 induction is to use mutual induction. You can define `even` mutually with `odd`, and `evenb` mutually with `oddb`, and then do proofs about them simultaneously.

I tried doing this. But couldn't figure how to proceed in the induction step phase:

``````Inductive even: nat -> Prop :=
| EvenO: even 0
| EvenS: forall n:nat,
odd n -> even (S n)
with odd: nat -> Prop :=
| OddS: forall n:nat,
even n -> odd (S n).

Fixpoint evenb (n:nat): bool :=
match n with
| O => true
| S n' => oddb n'
end
with oddb (n:nat): bool :=
match n with
| O => false
| S n' => evenb n'
end.

Definition evenBP (n: nat): evenb n = true -> even n.
Proof.
intros H.
induction n.
- constructor.
- apply EvenS.
``````

The goal at this point was:

``````1 subgoal

n : nat
H : evenb (S n) = true
IHn : evenb n = true -> even n

========================= (1 / 1)

odd n
``````

How can this be proven?

#### Lessness (Aug 20 2023 at 11:55):

Managed to prove this, more general, theorem:
`Definition evenBP (n: nat): (evenb n = true <-> even n) /\ (oddb n = true <-> odd n).`

This should be easier. If necessary, I can post proof too.

#### Julin S (Aug 20 2023 at 12:11):

Lessness said:

Managed to prove this, more general, theorem:
`Definition evenBP (n: nat): (evenb n = true <-> even n) /\ (oddb n = true <-> odd n).`

This should be easier. If necessary, I can post proof too.

Would it be easier? I mean, it consists 4 goals and one of them is the same theorem that I had been trying. Right?

#### Lessness (Aug 20 2023 at 12:15):

Yes, I believe that it should be easier.

I started the proof in such way

``````Definition evenBP (n: nat): (evenb n = true <-> even n) /\ (oddb n = true <-> odd n).
Proof.
induction n; split; intros; split; intros.
``````

And got 8 easy goals.

#### Lessness (Aug 20 2023 at 12:19):

Ah, okay, this is easier than my first idea:

``````Definition evenBP' (n: nat): (evenb n = true -> even n) /\ (oddb n = true -> odd n).
``````

#### James Wood (Aug 20 2023 at 12:20):

Sorry, yeah, the idea is to do the proofs together too, so you need to prove a conjunction.

#### Ana de Almeida Borges (Aug 20 2023 at 15:41):

Julin S said:

Would it be easier? I mean, it consists 4 goals and one of them is the same theorem that I had been trying. Right?

``````The point is that the since the theorem statement is stronger, the induction hypothesis is stronger too. That strong IH makes the whole thing easier to prove.
``````

Last updated: Jun 13 2024 at 19:02 UTC