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?
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))
.
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.
I think the alternative to a custom stepby2 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.
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.
I've used Fixpoint for proofs, but it's somewhat fragile because guardchecking 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.
James Wood said:
Also, you can consider using
Fixpoint
for proofs
Thanks, hadn't thought of that.
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.
Paolo Giarrusso said:
I've used Fixpoint for proofs, but it's somewhat fragile because guardchecking 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.
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.
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/proofengine/tactics.html#intropatterns .
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. :)
James Wood said:
I think the alternative to a custom stepby2 induction is to use mutual induction. You can define
even
mutually withodd
, andevenb
mutually withoddb
, 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?
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.
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?
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.
Ah, okay, this is easier than my first idea:
Definition evenBP' (n: nat): (evenb n = true > even n) /\ (oddb n = true > odd n).
Sorry, yeah, the idea is to do the proofs together too, so you need to prove a conjunction.
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