Stream: Coq users

Topic: Prove even number in Prop


view this post on Zulip 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?

view this post on Zulip 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)).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Julin S (Aug 20 2023 at 11:01):

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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 .

view this post on Zulip 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. :)

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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