Hello,

I'm wondering what's the best way to prove this seemingly trivial
theorem (in Coq):

Theorem even_double : forall x:nat,
evenb (double x 0) = true.

The other definitions are:

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

Fixpoint double (x y : nat) : nat :=
match x with
| O => y
| S x' => double x' (S (S y))
end.

Everything seems to be straightforward. The only twist is that double
has an accumulator. This is the first theorem in my learning process
where I found that I definitely needed a lemma. The question is, which
lemma is the best one to use?


-- Yin
_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
)

Hello,

I'm wondering what's the best way to prove this seemingly trivial
theorem (in Coq):

Theorem even_double : forall x:nat,
evenb (double x 0) = true.

The other definitions are:

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

Fixpoint double (x y : nat) : nat :=
match x with
| O => y
| S x' => double x' (S (S y))
end.

Everything seems to be straightforward. The only twist is that double
has an accumulator. This is the first theorem in my learning process
where I found that I definitely needed a lemma. The question is, which
lemma is the best one to use?


-- Yin
_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
)
Yin,
The lemma you want is the generalization of your theorem over the value of the accumulator:

Lemma even_double : forall x n,
evenb n = true -> evenb (double x n) = true.

Proving this is now a simple induction on x, and specializing n to 0 afterward is of course trivial.
I'm not sure what other lemma(s) one might choose instead of this; maybe that double x n = (double x 0) + n and then that the sum of even nats is even? But the first thing is much simpler.
--Jamie

----- Original Message -----
From: "Yin ****" <>
To: "IUCS Programming Languages"
Sent: Saturday, April 28, 2012 12:07:47 PM GMT -05:00 US/Canada Eastern
Subject: [pl-wonks] soliciting proofs for a trivial theorem

Hello,

I'm wondering what's the best way to prove this seemingly trivial
theorem (in Coq):

Theorem even_double : forall x:nat,
evenb (double x 0) = true.

The other definitions are:

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

Fixpoint double (x y : nat) : nat :=
match x with
| O => y
| S x' => double x' (S (S y))
end.

Everything seems to be straightforward. The only twist is that double
has an accumulator. This is the first theorem in my learning process
where I found that I definitely needed a lemma. The question is, which
lemma is the best one to use?


-- Yin
_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
)

Hello,

I'm wondering what's the best way to prove this seemingly trivial
theorem (in Coq):

Theorem even_double : forall x:nat,
evenb (double x 0) = true.

The other definitions are:

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

Fixpoint double (x y : nat) : nat :=
match x with
| O => y
| S x' => double x' (S (S y))
end.

Everything seems to be straightforward. The only twist is that double
has an accumulator. This is the first theorem in my learning process
where I found that I definitely needed a lemma. The question is, which
lemma is the best one to use?


-- Yin
_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
)
Yin,
The lemma you want is the generalization of your theorem over the value of the accumulator:

Lemma even_double : forall x n,
evenb n = true -> evenb (double x n) = true.

Proving this is now a simple induction on x, and specializing n to 0 afterward is of course trivial.
I'm not sure what other lemma(s) one might choose instead of this; maybe that double x n = (double x 0) + n and then that the sum of even nats is even? But the first thing is much simpler.
--Jamie

----- Original Message -----
From: "Yin ****" <>
To: "IUCS Programming Languages"
Sent: Saturday, April 28, 2012 12:07:47 PM GMT -05:00 US/Canada Eastern
Subject: [pl-wonks] soliciting proofs for a trivial theorem

Hello,

I'm wondering what's the best way to prove this seemingly trivial
theorem (in Coq):

Theorem even_double : forall x:nat,
evenb (double x 0) = true.

The other definitions are:

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

Fixpoint double (x y : nat) : nat :=
match x with
| O => y
| S x' => double x' (S (S y))
end.

Everything seems to be straightforward. The only twist is that double
has an accumulator. This is the first theorem in my learning process
where I found that I definitely needed a lemma. The question is, which
lemma is the best one to use?


-- Yin
_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
)
Thank you James. The lemma works.

I'm not sure if I got the optimal sequence of tactics though. I had to
induct on x first, then to 'intros' twice at two branches. Otherwise
the induction hypothesis will not be universally quantified. I would
appreciate a neater way to deal with this.

Here is my little ugly proof of the lemma:

Lemma even_y : forall x y : nat,
evenb y = true -> evenb (double x y) = true.

Proof.
induction x.
intros.
simpl.
apply H.
intros.
simpl.
apply IHx.
simpl.
apply H.
Qed.

The theorem is trivially proved using this lemma:

Theorem even_double : forall x:nat,
evenb (double x 0) = true.
Proof.
intros.
apply even_y.
reflexivity.
Qed.


I also found another lemma that works:

Lemma even_ss : forall x y : nat,
evenb (double x y) = evenb (double x (S (S y))).

It makes the proof of the theorem a little longer though:

Theorem even_double : forall x:nat,
evenb (double x 0) = true.
Proof.
Restart.
intros.
induction x.
reflexivity.
simpl.
rewrite <- even_ss.
apply IHx.
Qed.


I'll appreciate any other tricks. Thank you.


-- Yin


On Sat, Apr 28, 2012 at 12:25 PM, James T. Perconti
<> wrote:
> Yin,
>  The lemma you want is the generalization of your theorem over the value of the accumulator:
>
> Lemma even_double : forall x n,
>  evenb n = true -> evenb (double x n) = true.
>
> Proving this is now a simple induction on x, and specializing n to 0 afterward is of course trivial.
>  I'm not sure what other lemma(s) one might choose instead of this; maybe that double x n = (double x 0) + n and then that the sum of even nats is even?  But the first thing is much simpler.
>  --Jamie
>
> ----- Original Message -----
> From: "Yin ****" <>
> To: "IUCS Programming Languages"
> Sent: Saturday, April 28, 2012 12:07:47 PM GMT -05:00 US/Canada Eastern
> Subject: [pl-wonks] soliciting proofs for a trivial theorem
>
> Hello,
>
> I'm wondering what's the best way to prove this seemingly trivial
> theorem (in Coq):
>
> Theorem even_double : forall x:nat,
>  evenb (double x 0) = true.
>
> The other definitions are:
>
> Fixpoint evenb (n:nat) : bool :=
>  match n with
>    | O => true
>    | S O => false
>    | S (S n') => evenb n'
>  end.
>
> Fixpoint double (x y : nat) : nat :=
>  match x with
>    | O => y
>    | S x' => double x' (S (S y))
>  end.
>
> Everything seems to be straightforward. The only twist is that double
> has an accumulator. This is the first theorem in my learning process
> where I found that I definitely needed a lemma. The question is, which
> lemma is the best one to use?
>
>
> -- Yin
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

Hello,

I'm wondering what's the best way to prove this seemingly trivial
theorem (in Coq):

Theorem even_double : forall x:nat,
evenb (double x 0) = true.

The other definitions are:

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

Fixpoint double (x y : nat) : nat :=
match x with
| O => y
| S x' => double x' (S (S y))
end.

Everything seems to be straightforward. The only twist is that double
has an accumulator. This is the first theorem in my learning process
where I found that I definitely needed a lemma. The question is, which
lemma is the best one to use?


-- Yin
_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
)
Yin,
The lemma you want is the generalization of your theorem over the value of the accumulator:

Lemma even_double : forall x n,
evenb n = true -> evenb (double x n) = true.

Proving this is now a simple induction on x, and specializing n to 0 afterward is of course trivial.
I'm not sure what other lemma(s) one might choose instead of this; maybe that double x n = (double x 0) + n and then that the sum of even nats is even? But the first thing is much simpler.
--Jamie

----- Original Message -----
From: "Yin ****" <>
To: "IUCS Programming Languages"
Sent: Saturday, April 28, 2012 12:07:47 PM GMT -05:00 US/Canada Eastern
Subject: [pl-wonks] soliciting proofs for a trivial theorem

Hello,

I'm wondering what's the best way to prove this seemingly trivial
theorem (in Coq):

Theorem even_double : forall x:nat,
evenb (double x 0) = true.

The other definitions are:

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

Fixpoint double (x y : nat) : nat :=
match x with
| O => y
| S x' => double x' (S (S y))
end.

Everything seems to be straightforward. The only twist is that double
has an accumulator. This is the first theorem in my learning process
where I found that I definitely needed a lemma. The question is, which
lemma is the best one to use?


-- Yin
_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
)
Thank you James. The lemma works.

I'm not sure if I got the optimal sequence of tactics though. I had to
induct on x first, then to 'intros' twice at two branches. Otherwise
the induction hypothesis will not be universally quantified. I would
appreciate a neater way to deal with this.

Here is my little ugly proof of the lemma:

Lemma even_y : forall x y : nat,
evenb y = true -> evenb (double x y) = true.

Proof.
induction x.
intros.
simpl.
apply H.
intros.
simpl.
apply IHx.
simpl.
apply H.
Qed.

The theorem is trivially proved using this lemma:

Theorem even_double : forall x:nat,
evenb (double x 0) = true.
Proof.
intros.
apply even_y.
reflexivity.
Qed.


I also found another lemma that works:

Lemma even_ss : forall x y : nat,
evenb (double x y) = evenb (double x (S (S y))).

It makes the proof of the theorem a little longer though:

Theorem even_double : forall x:nat,
evenb (double x 0) = true.
Proof.
Restart.
intros.
induction x.
reflexivity.
simpl.
rewrite <- even_ss.
apply IHx.
Qed.


I'll appreciate any other tricks. Thank you.


-- Yin


On Sat, Apr 28, 2012 at 12:25 PM, James T. Perconti
<> wrote:
> Yin,
>  The lemma you want is the generalization of your theorem over the value of the accumulator:
>
> Lemma even_double : forall x n,
>  evenb n = true -> evenb (double x n) = true.
>
> Proving this is now a simple induction on x, and specializing n to 0 afterward is of course trivial.
>  I'm not sure what other lemma(s) one might choose instead of this; maybe that double x n = (double x 0) + n and then that the sum of even nats is even?  But the first thing is much simpler.
>  --Jamie
>
> ----- Original Message -----
> From: "Yin ****" <>
> To: "IUCS Programming Languages"
> Sent: Saturday, April 28, 2012 12:07:47 PM GMT -05:00 US/Canada Eastern
> Subject: [pl-wonks] soliciting proofs for a trivial theorem
>
> Hello,
>
> I'm wondering what's the best way to prove this seemingly trivial
> theorem (in Coq):
>
> Theorem even_double : forall x:nat,
>  evenb (double x 0) = true.
>
> The other definitions are:
>
> Fixpoint evenb (n:nat) : bool :=
>  match n with
>    | O => true
>    | S O => false
>    | S (S n') => evenb n'
>  end.
>
> Fixpoint double (x y : nat) : nat :=
>  match x with
>    | O => y
>    | S x' => double x' (S (S y))
>  end.
>
> Everything seems to be straightforward. The only twist is that double
> has an accumulator. This is the first theorem in my learning process
> where I found that I definitely needed a lemma. The question is, which
> lemma is the best one to use?
>
>
> -- Yin
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

I just proved it with
induction x; intros; simpl; auto.
Perhaps you have not learned about ; yet? It applies a tactic to all subgoals generated by its left-hand side.
--Jamie

----- Original Message -----
From: "Yin ****" <>
To: "IUCS Programming Languages"
Sent: Saturday, April 28, 2012 1:24:44 PM GMT -05:00 US/Canada Eastern
Subject: Re: [pl-wonks] soliciting proofs for a trivial theorem

Thank you James. The lemma works.

I'm not sure if I got the optimal sequence of tactics though. I had to
induct on x first, then to 'intros' twice at two branches. Otherwise
the induction hypothesis will not be universally quantified. I would
appreciate a neater way to deal with this.

Here is my little ugly proof of the lemma:

Lemma even_y : forall x y : nat,
evenb y = true -> evenb (double x y) = true.

Proof.
induction x.
intros.
simpl.
apply H.
intros.
simpl.
apply IHx.
simpl.
apply H.
Qed.

The theorem is trivially proved using this lemma:

Theorem even_double : forall x:nat,
evenb (double x 0) = true.
Proof.
intros.
apply even_y.
reflexivity.
Qed.


I also found another lemma that works:

Lemma even_ss : forall x y : nat,
evenb (double x y) = evenb (double x (S (S y))).

It makes the proof of the theorem a little longer though:

Theorem even_double : forall x:nat,
evenb (double x 0) = true.
Proof.
Restart.
intros.
induction x.
reflexivity.
simpl.
rewrite <- even_ss.
apply IHx.
Qed.


I'll appreciate any other tricks. Thank you.


-- Yin


On Sat, Apr 28, 2012 at 12:25 PM, James T. Perconti
<> wrote:
> Yin,
>  The lemma you want is the generalization of your theorem over the value of the accumulator:
>
> Lemma even_double : forall x n,
>  evenb n = true -> evenb (double x n) = true.
>
> Proving this is now a simple induction on x, and specializing n to 0 afterward is of course trivial.
>  I'm not sure what other lemma(s) one might choose instead of this; maybe that double x n = (double x 0) + n and then that the sum of even nats is even?  But the first thing is much simpler.
>  --Jamie
>
> ----- Original Message -----
> From: "Yin ****" <>
> To: "IUCS Programming Languages"
> Sent: Saturday, April 28, 2012 12:07:47 PM GMT -05:00 US/Canada Eastern
> Subject: [pl-wonks] soliciting proofs for a trivial theorem
>
> Hello,
>
> I'm wondering what's the best way to prove this seemingly trivial
> theorem (in Coq):
>
> Theorem even_double : forall x:nat,
>  evenb (double x 0) = true.
>
> The other definitions are:
>
> Fixpoint evenb (n:nat) : bool :=
>  match n with
>    | O => true
>    | S O => false
>    | S (S n') => evenb n'
>  end.
>
> Fixpoint double (x y : nat) : nat :=
>  match x with
>    | O => y
>    | S x' => double x' (S (S y))
>  end.
>
> Everything seems to be straightforward. The only twist is that double
> has an accumulator. This is the first theorem in my learning process
> where I found that I definitely needed a lemma. The question is, which
> lemma is the best one to use?
>
>
> -- Yin
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

Hello,

I'm wondering what's the best way to prove this seemingly trivial
theorem (in Coq):

Theorem even_double : forall x:nat,
evenb (double x 0) = true.

The other definitions are:

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

Fixpoint double (x y : nat) : nat :=
match x with
| O => y
| S x' => double x' (S (S y))
end.

Everything seems to be straightforward. The only twist is that double
has an accumulator. This is the first theorem in my learning process
where I found that I definitely needed a lemma. The question is, which
lemma is the best one to use?


-- Yin
_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
)
Yin,
The lemma you want is the generalization of your theorem over the value of the accumulator:

Lemma even_double : forall x n,
evenb n = true -> evenb (double x n) = true.

Proving this is now a simple induction on x, and specializing n to 0 afterward is of course trivial.
I'm not sure what other lemma(s) one might choose instead of this; maybe that double x n = (double x 0) + n and then that the sum of even nats is even? But the first thing is much simpler.
--Jamie

----- Original Message -----
From: "Yin ****" <>
To: "IUCS Programming Languages"
Sent: Saturday, April 28, 2012 12:07:47 PM GMT -05:00 US/Canada Eastern
Subject: [pl-wonks] soliciting proofs for a trivial theorem

Hello,

I'm wondering what's the best way to prove this seemingly trivial
theorem (in Coq):

Theorem even_double : forall x:nat,
evenb (double x 0) = true.

The other definitions are:

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

Fixpoint double (x y : nat) : nat :=
match x with
| O => y
| S x' => double x' (S (S y))
end.

Everything seems to be straightforward. The only twist is that double
has an accumulator. This is the first theorem in my learning process
where I found that I definitely needed a lemma. The question is, which
lemma is the best one to use?


-- Yin
_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
)
Thank you James. The lemma works.

I'm not sure if I got the optimal sequence of tactics though. I had to
induct on x first, then to 'intros' twice at two branches. Otherwise
the induction hypothesis will not be universally quantified. I would
appreciate a neater way to deal with this.

Here is my little ugly proof of the lemma:

Lemma even_y : forall x y : nat,
evenb y = true -> evenb (double x y) = true.

Proof.
induction x.
intros.
simpl.
apply H.
intros.
simpl.
apply IHx.
simpl.
apply H.
Qed.

The theorem is trivially proved using this lemma:

Theorem even_double : forall x:nat,
evenb (double x 0) = true.
Proof.
intros.
apply even_y.
reflexivity.
Qed.


I also found another lemma that works:

Lemma even_ss : forall x y : nat,
evenb (double x y) = evenb (double x (S (S y))).

It makes the proof of the theorem a little longer though:

Theorem even_double : forall x:nat,
evenb (double x 0) = true.
Proof.
Restart.
intros.
induction x.
reflexivity.
simpl.
rewrite <- even_ss.
apply IHx.
Qed.


I'll appreciate any other tricks. Thank you.


-- Yin


On Sat, Apr 28, 2012 at 12:25 PM, James T. Perconti
<> wrote:
> Yin,
>  The lemma you want is the generalization of your theorem over the value of the accumulator:
>
> Lemma even_double : forall x n,
>  evenb n = true -> evenb (double x n) = true.
>
> Proving this is now a simple induction on x, and specializing n to 0 afterward is of course trivial.
>  I'm not sure what other lemma(s) one might choose instead of this; maybe that double x n = (double x 0) + n and then that the sum of even nats is even?  But the first thing is much simpler.
>  --Jamie
>
> ----- Original Message -----
> From: "Yin ****" <>
> To: "IUCS Programming Languages"
> Sent: Saturday, April 28, 2012 12:07:47 PM GMT -05:00 US/Canada Eastern
> Subject: [pl-wonks] soliciting proofs for a trivial theorem
>
> Hello,
>
> I'm wondering what's the best way to prove this seemingly trivial
> theorem (in Coq):
>
> Theorem even_double : forall x:nat,
>  evenb (double x 0) = true.
>
> The other definitions are:
>
> Fixpoint evenb (n:nat) : bool :=
>  match n with
>    | O => true
>    | S O => false
>    | S (S n') => evenb n'
>  end.
>
> Fixpoint double (x y : nat) : nat :=
>  match x with
>    | O => y
>    | S x' => double x' (S (S y))
>  end.
>
> Everything seems to be straightforward. The only twist is that double
> has an accumulator. This is the first theorem in my learning process
> where I found that I definitely needed a lemma. The question is, which
> lemma is the best one to use?
>
>
> -- Yin
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

I just proved it with
induction x; intros; simpl; auto.
Perhaps you have not learned about ; yet? It applies a tactic to all subgoals generated by its left-hand side.
--Jamie

----- Original Message -----
From: "Yin ****" <>
To: "IUCS Programming Languages"
Sent: Saturday, April 28, 2012 1:24:44 PM GMT -05:00 US/Canada Eastern
Subject: Re: [pl-wonks] soliciting proofs for a trivial theorem

Thank you James. The lemma works.

I'm not sure if I got the optimal sequence of tactics though. I had to
induct on x first, then to 'intros' twice at two branches. Otherwise
the induction hypothesis will not be universally quantified. I would
appreciate a neater way to deal with this.

Here is my little ugly proof of the lemma:

Lemma even_y : forall x y : nat,
evenb y = true -> evenb (double x y) = true.

Proof.
induction x.
intros.
simpl.
apply H.
intros.
simpl.
apply IHx.
simpl.
apply H.
Qed.

The theorem is trivially proved using this lemma:

Theorem even_double : forall x:nat,
evenb (double x 0) = true.
Proof.
intros.
apply even_y.
reflexivity.
Qed.


I also found another lemma that works:

Lemma even_ss : forall x y : nat,
evenb (double x y) = evenb (double x (S (S y))).

It makes the proof of the theorem a little longer though:

Theorem even_double : forall x:nat,
evenb (double x 0) = true.
Proof.
Restart.
intros.
induction x.
reflexivity.
simpl.
rewrite <- even_ss.
apply IHx.
Qed.


I'll appreciate any other tricks. Thank you.


-- Yin


On Sat, Apr 28, 2012 at 12:25 PM, James T. Perconti
<> wrote:
> Yin,
>  The lemma you want is the generalization of your theorem over the value of the accumulator:
>
> Lemma even_double : forall x n,
>  evenb n = true -> evenb (double x n) = true.
>
> Proving this is now a simple induction on x, and specializing n to 0 afterward is of course trivial.
>  I'm not sure what other lemma(s) one might choose instead of this; maybe that double x n = (double x 0) + n and then that the sum of even nats is even?  But the first thing is much simpler.
>  --Jamie
>
> ----- Original Message -----
> From: "Yin ****" <>
> To: "IUCS Programming Languages"
> Sent: Saturday, April 28, 2012 12:07:47 PM GMT -05:00 US/Canada Eastern
> Subject: [pl-wonks] soliciting proofs for a trivial theorem
>
> Hello,
>
> I'm wondering what's the best way to prove this seemingly trivial
> theorem (in Coq):
>
> Theorem even_double : forall x:nat,
>  evenb (double x 0) = true.
>
> The other definitions are:
>
> Fixpoint evenb (n:nat) : bool :=
>  match n with
>    | O => true
>    | S O => false
>    | S (S n') => evenb n'
>  end.
>
> Fixpoint double (x y : nat) : nat :=
>  match x with
>    | O => y
>    | S x' => double x' (S (S y))
>  end.
>
> Everything seems to be straightforward. The only twist is that double
> has an accumulator. This is the first theorem in my learning process
> where I found that I definitely needed a lemma. The question is, which
> lemma is the best one to use?
>
>
> -- Yin
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

I had been trying not to use anything fancy (like auto), but I would
try ';'. I guess I can think of it as a join point for branches? Thank
you.


-- Yin


On Sat, Apr 28, 2012 at 1:35 PM, James T. Perconti <> wrote:
> I just proved it with
>   induction x; intros; simpl; auto.
> Perhaps you have not learned about ; yet?  It applies a tactic to all subgoals generated by its left-hand side.
>  --Jamie
>
> ----- Original Message -----
> From: "Yin ****" <>
> To: "IUCS Programming Languages"
> Sent: Saturday, April 28, 2012 1:24:44 PM GMT -05:00 US/Canada Eastern
> Subject: Re: [pl-wonks] soliciting proofs for a trivial theorem
>
> Thank you James. The lemma works.
>
> I'm not sure if I got the optimal sequence of tactics though. I had to
> induct on x first, then to 'intros' twice at two branches. Otherwise
> the induction hypothesis will not be universally quantified. I would
> appreciate a neater way to deal with this.
>
> Here is my little ugly proof of the lemma:
>
> Lemma even_y : forall x y : nat,
>  evenb y = true -> evenb (double x y) = true.
>
> Proof.
>  induction x.
>  intros.
>  simpl.
>  apply H.
>  intros.
>  simpl.
>  apply IHx.
>  simpl.
>  apply H.
> Qed.
>
> The theorem is trivially proved using this lemma:
>
> Theorem even_double : forall x:nat,
>  evenb (double x 0) = true.
> Proof.
>  intros.
>  apply even_y.
>  reflexivity.
> Qed.
>
>
> I also found another lemma that works:
>
> Lemma even_ss : forall x y : nat,
>  evenb (double x y) = evenb (double x (S (S y))).
>
> It makes the proof of the theorem a little longer though:
>
> Theorem even_double : forall x:nat,
>  evenb (double x 0) = true.
> Proof.
>  Restart.
>  intros.
>  induction x.
>  reflexivity.
>  simpl.
>  rewrite <- even_ss.
>  apply IHx.
> Qed.
>
>
> I'll appreciate any other tricks. Thank you.
>
>
> -- Yin
>
>
> On Sat, Apr 28, 2012 at 12:25 PM, James T. Perconti
> <> wrote:
>> Yin,
>>  The lemma you want is the generalization of your theorem over the value of the accumulator:
>>
>> Lemma even_double : forall x n,
>>  evenb n = true -> evenb (double x n) = true.
>>
>> Proving this is now a simple induction on x, and specializing n to 0 afterward is of course trivial.
>>  I'm not sure what other lemma(s) one might choose instead of this; maybe that double x n = (double x 0) + n and then that the sum of even nats is even?  But the first thing is much simpler.
>>  --Jamie
>>
>> ----- Original Message -----
>> From: "Yin ****" <>
>> To: "IUCS Programming Languages"
>> Sent: Saturday, April 28, 2012 12:07:47 PM GMT -05:00 US/Canada Eastern
>> Subject: [pl-wonks] soliciting proofs for a trivial theorem
>>
>> Hello,
>>
>> I'm wondering what's the best way to prove this seemingly trivial
>> theorem (in Coq):
>>
>> Theorem even_double : forall x:nat,
>>  evenb (double x 0) = true.
>>
>> The other definitions are:
>>
>> Fixpoint evenb (n:nat) : bool :=
>>  match n with
>>    | O => true
>>    | S O => false
>>    | S (S n') => evenb n'
>>  end.
>>
>> Fixpoint double (x y : nat) : nat :=
>>  match x with
>>    | O => y
>>    | S x' => double x' (S (S y))
>>  end.
>>
>> Everything seems to be straightforward. The only twist is that double
>> has an accumulator. This is the first theorem in my learning process
>> where I found that I definitely needed a lemma. The question is, which
>> lemma is the best one to use?
>>
>>
>> -- Yin
>> _______________________________________________
>> PL-wonks mailing list
>> PL-
>> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>> _______________________________________________
>> PL-wonks mailing list
>> PL-
>> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

Hello,

I'm wondering what's the best way to prove this seemingly trivial
theorem (in Coq):

Theorem even_double : forall x:nat,
evenb (double x 0) = true.

The other definitions are:

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

Fixpoint double (x y : nat) : nat :=
match x with
| O => y
| S x' => double x' (S (S y))
end.

Everything seems to be straightforward. The only twist is that double
has an accumulator. This is the first theorem in my learning process
where I found that I definitely needed a lemma. The question is, which
lemma is the best one to use?


-- Yin
_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
)
Yin,
The lemma you want is the generalization of your theorem over the value of the accumulator:

Lemma even_double : forall x n,
evenb n = true -> evenb (double x n) = true.

Proving this is now a simple induction on x, and specializing n to 0 afterward is of course trivial.
I'm not sure what other lemma(s) one might choose instead of this; maybe that double x n = (double x 0) + n and then that the sum of even nats is even? But the first thing is much simpler.
--Jamie

----- Original Message -----
From: "Yin ****" <>
To: "IUCS Programming Languages"
Sent: Saturday, April 28, 2012 12:07:47 PM GMT -05:00 US/Canada Eastern
Subject: [pl-wonks] soliciting proofs for a trivial theorem

Hello,

I'm wondering what's the best way to prove this seemingly trivial
theorem (in Coq):

Theorem even_double : forall x:nat,
evenb (double x 0) = true.

The other definitions are:

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

Fixpoint double (x y : nat) : nat :=
match x with
| O => y
| S x' => double x' (S (S y))
end.

Everything seems to be straightforward. The only twist is that double
has an accumulator. This is the first theorem in my learning process
where I found that I definitely needed a lemma. The question is, which
lemma is the best one to use?


-- Yin
_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
)
Thank you James. The lemma works.

I'm not sure if I got the optimal sequence of tactics though. I had to
induct on x first, then to 'intros' twice at two branches. Otherwise
the induction hypothesis will not be universally quantified. I would
appreciate a neater way to deal with this.

Here is my little ugly proof of the lemma:

Lemma even_y : forall x y : nat,
evenb y = true -> evenb (double x y) = true.

Proof.
induction x.
intros.
simpl.
apply H.
intros.
simpl.
apply IHx.
simpl.
apply H.
Qed.

The theorem is trivially proved using this lemma:

Theorem even_double : forall x:nat,
evenb (double x 0) = true.
Proof.
intros.
apply even_y.
reflexivity.
Qed.


I also found another lemma that works:

Lemma even_ss : forall x y : nat,
evenb (double x y) = evenb (double x (S (S y))).

It makes the proof of the theorem a little longer though:

Theorem even_double : forall x:nat,
evenb (double x 0) = true.
Proof.
Restart.
intros.
induction x.
reflexivity.
simpl.
rewrite <- even_ss.
apply IHx.
Qed.


I'll appreciate any other tricks. Thank you.


-- Yin


On Sat, Apr 28, 2012 at 12:25 PM, James T. Perconti
<> wrote:
> Yin,
>  The lemma you want is the generalization of your theorem over the value of the accumulator:
>
> Lemma even_double : forall x n,
>  evenb n = true -> evenb (double x n) = true.
>
> Proving this is now a simple induction on x, and specializing n to 0 afterward is of course trivial.
>  I'm not sure what other lemma(s) one might choose instead of this; maybe that double x n = (double x 0) + n and then that the sum of even nats is even?  But the first thing is much simpler.
>  --Jamie
>
> ----- Original Message -----
> From: "Yin ****" <>
> To: "IUCS Programming Languages"
> Sent: Saturday, April 28, 2012 12:07:47 PM GMT -05:00 US/Canada Eastern
> Subject: [pl-wonks] soliciting proofs for a trivial theorem
>
> Hello,
>
> I'm wondering what's the best way to prove this seemingly trivial
> theorem (in Coq):
>
> Theorem even_double : forall x:nat,
>  evenb (double x 0) = true.
>
> The other definitions are:
>
> Fixpoint evenb (n:nat) : bool :=
>  match n with
>    | O => true
>    | S O => false
>    | S (S n') => evenb n'
>  end.
>
> Fixpoint double (x y : nat) : nat :=
>  match x with
>    | O => y
>    | S x' => double x' (S (S y))
>  end.
>
> Everything seems to be straightforward. The only twist is that double
> has an accumulator. This is the first theorem in my learning process
> where I found that I definitely needed a lemma. The question is, which
> lemma is the best one to use?
>
>
> -- Yin
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

I just proved it with
induction x; intros; simpl; auto.
Perhaps you have not learned about ; yet? It applies a tactic to all subgoals generated by its left-hand side.
--Jamie

----- Original Message -----
From: "Yin ****" <>
To: "IUCS Programming Languages"
Sent: Saturday, April 28, 2012 1:24:44 PM GMT -05:00 US/Canada Eastern
Subject: Re: [pl-wonks] soliciting proofs for a trivial theorem

Thank you James. The lemma works.

I'm not sure if I got the optimal sequence of tactics though. I had to
induct on x first, then to 'intros' twice at two branches. Otherwise
the induction hypothesis will not be universally quantified. I would
appreciate a neater way to deal with this.

Here is my little ugly proof of the lemma:

Lemma even_y : forall x y : nat,
evenb y = true -> evenb (double x y) = true.

Proof.
induction x.
intros.
simpl.
apply H.
intros.
simpl.
apply IHx.
simpl.
apply H.
Qed.

The theorem is trivially proved using this lemma:

Theorem even_double : forall x:nat,
evenb (double x 0) = true.
Proof.
intros.
apply even_y.
reflexivity.
Qed.


I also found another lemma that works:

Lemma even_ss : forall x y : nat,
evenb (double x y) = evenb (double x (S (S y))).

It makes the proof of the theorem a little longer though:

Theorem even_double : forall x:nat,
evenb (double x 0) = true.
Proof.
Restart.
intros.
induction x.
reflexivity.
simpl.
rewrite <- even_ss.
apply IHx.
Qed.


I'll appreciate any other tricks. Thank you.


-- Yin


On Sat, Apr 28, 2012 at 12:25 PM, James T. Perconti
<> wrote:
> Yin,
>  The lemma you want is the generalization of your theorem over the value of the accumulator:
>
> Lemma even_double : forall x n,
>  evenb n = true -> evenb (double x n) = true.
>
> Proving this is now a simple induction on x, and specializing n to 0 afterward is of course trivial.
>  I'm not sure what other lemma(s) one might choose instead of this; maybe that double x n = (double x 0) + n and then that the sum of even nats is even?  But the first thing is much simpler.
>  --Jamie
>
> ----- Original Message -----
> From: "Yin ****" <>
> To: "IUCS Programming Languages"
> Sent: Saturday, April 28, 2012 12:07:47 PM GMT -05:00 US/Canada Eastern
> Subject: [pl-wonks] soliciting proofs for a trivial theorem
>
> Hello,
>
> I'm wondering what's the best way to prove this seemingly trivial
> theorem (in Coq):
>
> Theorem even_double : forall x:nat,
>  evenb (double x 0) = true.
>
> The other definitions are:
>
> Fixpoint evenb (n:nat) : bool :=
>  match n with
>    | O => true
>    | S O => false
>    | S (S n') => evenb n'
>  end.
>
> Fixpoint double (x y : nat) : nat :=
>  match x with
>    | O => y
>    | S x' => double x' (S (S y))
>  end.
>
> Everything seems to be straightforward. The only twist is that double
> has an accumulator. This is the first theorem in my learning process
> where I found that I definitely needed a lemma. The question is, which
> lemma is the best one to use?
>
>
> -- Yin
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

I had been trying not to use anything fancy (like auto), but I would
try ';'. I guess I can think of it as a join point for branches? Thank
you.


-- Yin


On Sat, Apr 28, 2012 at 1:35 PM, James T. Perconti <> wrote:
> I just proved it with
>   induction x; intros; simpl; auto.
> Perhaps you have not learned about ; yet?  It applies a tactic to all subgoals generated by its left-hand side.
>  --Jamie
>
> ----- Original Message -----
> From: "Yin ****" <>
> To: "IUCS Programming Languages"
> Sent: Saturday, April 28, 2012 1:24:44 PM GMT -05:00 US/Canada Eastern
> Subject: Re: [pl-wonks] soliciting proofs for a trivial theorem
>
> Thank you James. The lemma works.
>
> I'm not sure if I got the optimal sequence of tactics though. I had to
> induct on x first, then to 'intros' twice at two branches. Otherwise
> the induction hypothesis will not be universally quantified. I would
> appreciate a neater way to deal with this.
>
> Here is my little ugly proof of the lemma:
>
> Lemma even_y : forall x y : nat,
>  evenb y = true -> evenb (double x y) = true.
>
> Proof.
>  induction x.
>  intros.
>  simpl.
>  apply H.
>  intros.
>  simpl.
>  apply IHx.
>  simpl.
>  apply H.
> Qed.
>
> The theorem is trivially proved using this lemma:
>
> Theorem even_double : forall x:nat,
>  evenb (double x 0) = true.
> Proof.
>  intros.
>  apply even_y.
>  reflexivity.
> Qed.
>
>
> I also found another lemma that works:
>
> Lemma even_ss : forall x y : nat,
>  evenb (double x y) = evenb (double x (S (S y))).
>
> It makes the proof of the theorem a little longer though:
>
> Theorem even_double : forall x:nat,
>  evenb (double x 0) = true.
> Proof.
>  Restart.
>  intros.
>  induction x.
>  reflexivity.
>  simpl.
>  rewrite <- even_ss.
>  apply IHx.
> Qed.
>
>
> I'll appreciate any other tricks. Thank you.
>
>
> -- Yin
>
>
> On Sat, Apr 28, 2012 at 12:25 PM, James T. Perconti
> <> wrote:
>> Yin,
>>  The lemma you want is the generalization of your theorem over the value of the accumulator:
>>
>> Lemma even_double : forall x n,
>>  evenb n = true -> evenb (double x n) = true.
>>
>> Proving this is now a simple induction on x, and specializing n to 0 afterward is of course trivial.
>>  I'm not sure what other lemma(s) one might choose instead of this; maybe that double x n = (double x 0) + n and then that the sum of even nats is even?  But the first thing is much simpler.
>>  --Jamie
>>
>> ----- Original Message -----
>> From: "Yin ****" <>
>> To: "IUCS Programming Languages"
>> Sent: Saturday, April 28, 2012 12:07:47 PM GMT -05:00 US/Canada Eastern
>> Subject: [pl-wonks] soliciting proofs for a trivial theorem
>>
>> Hello,
>>
>> I'm wondering what's the best way to prove this seemingly trivial
>> theorem (in Coq):
>>
>> Theorem even_double : forall x:nat,
>>  evenb (double x 0) = true.
>>
>> The other definitions are:
>>
>> Fixpoint evenb (n:nat) : bool :=
>>  match n with
>>    | O => true
>>    | S O => false
>>    | S (S n') => evenb n'
>>  end.
>>
>> Fixpoint double (x y : nat) : nat :=
>>  match x with
>>    | O => y
>>    | S x' => double x' (S (S y))
>>  end.
>>
>> Everything seems to be straightforward. The only twist is that double
>> has an accumulator. This is the first theorem in my learning process
>> where I found that I definitely needed a lemma. The question is, which
>> lemma is the best one to use?
>>
>>
>> -- Yin
>> _______________________________________________
>> PL-wonks mailing list
>> PL-
>> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>> _______________________________________________
>> PL-wonks mailing list
>> PL-
>> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

Hi Yin,

How about this lemma?

Lemma double_s : forall x y:nat, double (S x) y = S (S (double x y)).

The proof for this one is just by induction on x, and then for the main
theorem, you basically have induction on x, with one rewrite. Both proofs
are short and straightforward. Perhaps this is what you were looking
for? Here are my proofs:

Lemma double_s : forall x y:nat, double (S x) y = S (S (double x y)).
Proof.
intros x.
induction x.
reflexivity.

intros y.
simpl.
apply IHx.
Qed.

Theorem even_double : forall x:nat, evenb (double x 0) = true.
Proof.
induction x.
reflexivity.

rewrite double_s.
simpl.
apply IHx.
Qed.


-Rebecca


On Sat, Apr 28, 2012 at 1:45 PM, Yin **** <> wrote:

> I had been trying not to use anything fancy (like auto), but I would
> try ';'. I guess I can think of it as a join point for branches? Thank
> you.
>
>
> -- Yin
>
>
> On Sat, Apr 28, 2012 at 1:35 PM, James T. Perconti <>
> wrote:
> > I just proved it with
> > induction x; intros; simpl; auto.
> > Perhaps you have not learned about ; yet? It applies a tactic to all
> subgoals generated by its left-hand side.
> > --Jamie
> >
> > ----- Original Message -----
> > From: "Yin ****" <>
> > To: "IUCS Programming Languages"
> > Sent: Saturday, April 28, 2012 1:24:44 PM GMT -05:00 US/Canada Eastern
> > Subject: Re: [pl-wonks] soliciting proofs for a trivial theorem
> >
> > Thank you James. The lemma works.
> >
> > I'm not sure if I got the optimal sequence of tactics though. I had to
> > induct on x first, then to 'intros' twice at two branches. Otherwise
> > the induction hypothesis will not be universally quantified. I would
> > appreciate a neater way to deal with this.
> >
> > Here is my little ugly proof of the lemma:
> >
> > Lemma even_y : forall x y : nat,
> > evenb y = true -> evenb (double x y) = true.
> >
> > Proof.
> > induction x.
> > intros.
> > simpl.
> > apply H.
> > intros.
> > simpl.
> > apply IHx.
> > simpl.
> > apply H.
> > Qed.
> >
> > The theorem is trivially proved using this lemma:
> >
> > Theorem even_double : forall x:nat,
> > evenb (double x 0) = true.
> > Proof.
> > intros.
> > apply even_y.
> > reflexivity.
> > Qed.
> >
> >
> > I also found another lemma that works:
> >
> > Lemma even_ss : forall x y : nat,
> > evenb (double x y) = evenb (double x (S (S y))).
> >
> > It makes the proof of the theorem a little longer though:
> >
> > Theorem even_double : forall x:nat,
> > evenb (double x 0) = true.
> > Proof.
> > Restart.
> > intros.
> > induction x.
> > reflexivity.
> > simpl.
> > rewrite <- even_ss.
> > apply IHx.
> > Qed.
> >
> >
> > I'll appreciate any other tricks. Thank you.
> >
> >
> > -- Yin
> >
> >
> > On Sat, Apr 28, 2012 at 12:25 PM, James T. Perconti
> > <> wrote:
> >> Yin,
> >> The lemma you want is the generalization of your theorem over the
> value of the accumulator:
> >>
> >> Lemma even_double : forall x n,
> >> evenb n = true -> evenb (double x n) = true.
> >>
> >> Proving this is now a simple induction on x, and specializing n to 0
> afterward is of course trivial.
> >> I'm not sure what other lemma(s) one might choose instead of this;
> maybe that double x n = (double x 0) + n and then that the sum of even nats
> is even? But the first thing is much simpler.
> >> --Jamie
> >>
> >> ----- Original Message -----
> >> From: "Yin ****" <>
> >> To: "IUCS Programming Languages"
> >> Sent: Saturday, April 28, 2012 12:07:47 PM GMT -05:00 US/Canada Eastern
> >> Subject: [pl-wonks] soliciting proofs for a trivial theorem
> >>
> >> Hello,
> >>
> >> I'm wondering what's the best way to prove this seemingly trivial
> >> theorem (in Coq):
> >>
> >> Theorem even_double : forall x:nat,
> >> evenb (double x 0) = true.
> >>
> >> The other definitions are:
> >>
> >> Fixpoint evenb (n:nat) : bool :=
> >> match n with
> >> | O => true
> >> | S O => false
> >> | S (S n') => evenb n'
> >> end.
> >>
> >> Fixpoint double (x y : nat) : nat :=
> >> match x with
> >> | O => y
> >> | S x' => double x' (S (S y))
> >> end.
> >>
> >> Everything seems to be straightforward. The only twist is that double
> >> has an accumulator. This is the first theorem in my learning process
> >> where I found that I definitely needed a lemma. The question is, which
> >> lemma is the best one to use?
> >>
> >>
> >> -- Yin
> >> _______________________________________________
> >> PL-wonks mailing list
> >> PL-
> >> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
> >> _______________________________________________
> >> PL-wonks mailing list
> >> PL-
> >> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
> >
> > _______________________________________________
> > PL-wonks mailing list
> > PL-
> > http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
> >
> > _______________________________________________
> > PL-wonks mailing list
> > PL-
> > http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>

Hello,

I'm wondering what's the best way to prove this seemingly trivial
theorem (in Coq):

Theorem even_double : forall x:nat,
evenb (double x 0) = true.

The other definitions are:

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

Fixpoint double (x y : nat) : nat :=
match x with
| O => y
| S x' => double x' (S (S y))
end.

Everything seems to be straightforward. The only twist is that double
has an accumulator. This is the first theorem in my learning process
where I found that I definitely needed a lemma. The question is, which
lemma is the best one to use?


-- Yin
_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
)
Yin,
The lemma you want is the generalization of your theorem over the value of the accumulator:

Lemma even_double : forall x n,
evenb n = true -> evenb (double x n) = true.

Proving this is now a simple induction on x, and specializing n to 0 afterward is of course trivial.
I'm not sure what other lemma(s) one might choose instead of this; maybe that double x n = (double x 0) + n and then that the sum of even nats is even? But the first thing is much simpler.
--Jamie

----- Original Message -----
From: "Yin ****" <>
To: "IUCS Programming Languages"
Sent: Saturday, April 28, 2012 12:07:47 PM GMT -05:00 US/Canada Eastern
Subject: [pl-wonks] soliciting proofs for a trivial theorem

Hello,

I'm wondering what's the best way to prove this seemingly trivial
theorem (in Coq):

Theorem even_double : forall x:nat,
evenb (double x 0) = true.

The other definitions are:

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

Fixpoint double (x y : nat) : nat :=
match x with
| O => y
| S x' => double x' (S (S y))
end.

Everything seems to be straightforward. The only twist is that double
has an accumulator. This is the first theorem in my learning process
where I found that I definitely needed a lemma. The question is, which
lemma is the best one to use?


-- Yin
_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
)
Thank you James. The lemma works.

I'm not sure if I got the optimal sequence of tactics though. I had to
induct on x first, then to 'intros' twice at two branches. Otherwise
the induction hypothesis will not be universally quantified. I would
appreciate a neater way to deal with this.

Here is my little ugly proof of the lemma:

Lemma even_y : forall x y : nat,
evenb y = true -> evenb (double x y) = true.

Proof.
induction x.
intros.
simpl.
apply H.
intros.
simpl.
apply IHx.
simpl.
apply H.
Qed.

The theorem is trivially proved using this lemma:

Theorem even_double : forall x:nat,
evenb (double x 0) = true.
Proof.
intros.
apply even_y.
reflexivity.
Qed.


I also found another lemma that works:

Lemma even_ss : forall x y : nat,
evenb (double x y) = evenb (double x (S (S y))).

It makes the proof of the theorem a little longer though:

Theorem even_double : forall x:nat,
evenb (double x 0) = true.
Proof.
Restart.
intros.
induction x.
reflexivity.
simpl.
rewrite <- even_ss.
apply IHx.
Qed.


I'll appreciate any other tricks. Thank you.


-- Yin


On Sat, Apr 28, 2012 at 12:25 PM, James T. Perconti
<> wrote:
> Yin,
>  The lemma you want is the generalization of your theorem over the value of the accumulator:
>
> Lemma even_double : forall x n,
>  evenb n = true -> evenb (double x n) = true.
>
> Proving this is now a simple induction on x, and specializing n to 0 afterward is of course trivial.
>  I'm not sure what other lemma(s) one might choose instead of this; maybe that double x n = (double x 0) + n and then that the sum of even nats is even?  But the first thing is much simpler.
>  --Jamie
>
> ----- Original Message -----
> From: "Yin ****" <>
> To: "IUCS Programming Languages"
> Sent: Saturday, April 28, 2012 12:07:47 PM GMT -05:00 US/Canada Eastern
> Subject: [pl-wonks] soliciting proofs for a trivial theorem
>
> Hello,
>
> I'm wondering what's the best way to prove this seemingly trivial
> theorem (in Coq):
>
> Theorem even_double : forall x:nat,
>  evenb (double x 0) = true.
>
> The other definitions are:
>
> Fixpoint evenb (n:nat) : bool :=
>  match n with
>    | O => true
>    | S O => false
>    | S (S n') => evenb n'
>  end.
>
> Fixpoint double (x y : nat) : nat :=
>  match x with
>    | O => y
>    | S x' => double x' (S (S y))
>  end.
>
> Everything seems to be straightforward. The only twist is that double
> has an accumulator. This is the first theorem in my learning process
> where I found that I definitely needed a lemma. The question is, which
> lemma is the best one to use?
>
>
> -- Yin
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

I just proved it with
induction x; intros; simpl; auto.
Perhaps you have not learned about ; yet? It applies a tactic to all subgoals generated by its left-hand side.
--Jamie

----- Original Message -----
From: "Yin ****" <>
To: "IUCS Programming Languages"
Sent: Saturday, April 28, 2012 1:24:44 PM GMT -05:00 US/Canada Eastern
Subject: Re: [pl-wonks] soliciting proofs for a trivial theorem

Thank you James. The lemma works.

I'm not sure if I got the optimal sequence of tactics though. I had to
induct on x first, then to 'intros' twice at two branches. Otherwise
the induction hypothesis will not be universally quantified. I would
appreciate a neater way to deal with this.

Here is my little ugly proof of the lemma:

Lemma even_y : forall x y : nat,
evenb y = true -> evenb (double x y) = true.

Proof.
induction x.
intros.
simpl.
apply H.
intros.
simpl.
apply IHx.
simpl.
apply H.
Qed.

The theorem is trivially proved using this lemma:

Theorem even_double : forall x:nat,
evenb (double x 0) = true.
Proof.
intros.
apply even_y.
reflexivity.
Qed.


I also found another lemma that works:

Lemma even_ss : forall x y : nat,
evenb (double x y) = evenb (double x (S (S y))).

It makes the proof of the theorem a little longer though:

Theorem even_double : forall x:nat,
evenb (double x 0) = true.
Proof.
Restart.
intros.
induction x.
reflexivity.
simpl.
rewrite <- even_ss.
apply IHx.
Qed.


I'll appreciate any other tricks. Thank you.


-- Yin


On Sat, Apr 28, 2012 at 12:25 PM, James T. Perconti
<> wrote:
> Yin,
>  The lemma you want is the generalization of your theorem over the value of the accumulator:
>
> Lemma even_double : forall x n,
>  evenb n = true -> evenb (double x n) = true.
>
> Proving this is now a simple induction on x, and specializing n to 0 afterward is of course trivial.
>  I'm not sure what other lemma(s) one might choose instead of this; maybe that double x n = (double x 0) + n and then that the sum of even nats is even?  But the first thing is much simpler.
>  --Jamie
>
> ----- Original Message -----
> From: "Yin ****" <>
> To: "IUCS Programming Languages"
> Sent: Saturday, April 28, 2012 12:07:47 PM GMT -05:00 US/Canada Eastern
> Subject: [pl-wonks] soliciting proofs for a trivial theorem
>
> Hello,
>
> I'm wondering what's the best way to prove this seemingly trivial
> theorem (in Coq):
>
> Theorem even_double : forall x:nat,
>  evenb (double x 0) = true.
>
> The other definitions are:
>
> Fixpoint evenb (n:nat) : bool :=
>  match n with
>    | O => true
>    | S O => false
>    | S (S n') => evenb n'
>  end.
>
> Fixpoint double (x y : nat) : nat :=
>  match x with
>    | O => y
>    | S x' => double x' (S (S y))
>  end.
>
> Everything seems to be straightforward. The only twist is that double
> has an accumulator. This is the first theorem in my learning process
> where I found that I definitely needed a lemma. The question is, which
> lemma is the best one to use?
>
>
> -- Yin
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

I had been trying not to use anything fancy (like auto), but I would
try ';'. I guess I can think of it as a join point for branches? Thank
you.


-- Yin


On Sat, Apr 28, 2012 at 1:35 PM, James T. Perconti <> wrote:
> I just proved it with
>   induction x; intros; simpl; auto.
> Perhaps you have not learned about ; yet?  It applies a tactic to all subgoals generated by its left-hand side.
>  --Jamie
>
> ----- Original Message -----
> From: "Yin ****" <>
> To: "IUCS Programming Languages"
> Sent: Saturday, April 28, 2012 1:24:44 PM GMT -05:00 US/Canada Eastern
> Subject: Re: [pl-wonks] soliciting proofs for a trivial theorem
>
> Thank you James. The lemma works.
>
> I'm not sure if I got the optimal sequence of tactics though. I had to
> induct on x first, then to 'intros' twice at two branches. Otherwise
> the induction hypothesis will not be universally quantified. I would
> appreciate a neater way to deal with this.
>
> Here is my little ugly proof of the lemma:
>
> Lemma even_y : forall x y : nat,
>  evenb y = true -> evenb (double x y) = true.
>
> Proof.
>  induction x.
>  intros.
>  simpl.
>  apply H.
>  intros.
>  simpl.
>  apply IHx.
>  simpl.
>  apply H.
> Qed.
>
> The theorem is trivially proved using this lemma:
>
> Theorem even_double : forall x:nat,
>  evenb (double x 0) = true.
> Proof.
>  intros.
>  apply even_y.
>  reflexivity.
> Qed.
>
>
> I also found another lemma that works:
>
> Lemma even_ss : forall x y : nat,
>  evenb (double x y) = evenb (double x (S (S y))).
>
> It makes the proof of the theorem a little longer though:
>
> Theorem even_double : forall x:nat,
>  evenb (double x 0) = true.
> Proof.
>  Restart.
>  intros.
>  induction x.
>  reflexivity.
>  simpl.
>  rewrite <- even_ss.
>  apply IHx.
> Qed.
>
>
> I'll appreciate any other tricks. Thank you.
>
>
> -- Yin
>
>
> On Sat, Apr 28, 2012 at 12:25 PM, James T. Perconti
> <> wrote:
>> Yin,
>>  The lemma you want is the generalization of your theorem over the value of the accumulator:
>>
>> Lemma even_double : forall x n,
>>  evenb n = true -> evenb (double x n) = true.
>>
>> Proving this is now a simple induction on x, and specializing n to 0 afterward is of course trivial.
>>  I'm not sure what other lemma(s) one might choose instead of this; maybe that double x n = (double x 0) + n and then that the sum of even nats is even?  But the first thing is much simpler.
>>  --Jamie
>>
>> ----- Original Message -----
>> From: "Yin ****" <>
>> To: "IUCS Programming Languages"
>> Sent: Saturday, April 28, 2012 12:07:47 PM GMT -05:00 US/Canada Eastern
>> Subject: [pl-wonks] soliciting proofs for a trivial theorem
>>
>> Hello,
>>
>> I'm wondering what's the best way to prove this seemingly trivial
>> theorem (in Coq):
>>
>> Theorem even_double : forall x:nat,
>>  evenb (double x 0) = true.
>>
>> The other definitions are:
>>
>> Fixpoint evenb (n:nat) : bool :=
>>  match n with
>>    | O => true
>>    | S O => false
>>    | S (S n') => evenb n'
>>  end.
>>
>> Fixpoint double (x y : nat) : nat :=
>>  match x with
>>    | O => y
>>    | S x' => double x' (S (S y))
>>  end.
>>
>> Everything seems to be straightforward. The only twist is that double
>> has an accumulator. This is the first theorem in my learning process
>> where I found that I definitely needed a lemma. The question is, which
>> lemma is the best one to use?
>>
>>
>> -- Yin
>> _______________________________________________
>> PL-wonks mailing list
>> PL-
>> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>> _______________________________________________
>> PL-wonks mailing list
>> PL-
>> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

Hi Yin,

How about this lemma?

Lemma double_s : forall x y:nat, double (S x) y = S (S (double x y)).

The proof for this one is just by induction on x, and then for the main
theorem, you basically have induction on x, with one rewrite. Both proofs
are short and straightforward. Perhaps this is what you were looking
for? Here are my proofs:

Lemma double_s : forall x y:nat, double (S x) y = S (S (double x y)).
Proof.
intros x.
induction x.
reflexivity.

intros y.
simpl.
apply IHx.
Qed.

Theorem even_double : forall x:nat, evenb (double x 0) = true.
Proof.
induction x.
reflexivity.

rewrite double_s.
simpl.
apply IHx.
Qed.


-Rebecca


On Sat, Apr 28, 2012 at 1:45 PM, Yin **** <> wrote:

> I had been trying not to use anything fancy (like auto), but I would
> try ';'. I guess I can think of it as a join point for branches? Thank
> you.
>
>
> -- Yin
>
>
> On Sat, Apr 28, 2012 at 1:35 PM, James T. Perconti <>
> wrote:
> > I just proved it with
> > induction x; intros; simpl; auto.
> > Perhaps you have not learned about ; yet? It applies a tactic to all
> subgoals generated by its left-hand side.
> > --Jamie
> >
> > ----- Original Message -----
> > From: "Yin ****" <>
> > To: "IUCS Programming Languages"
> > Sent: Saturday, April 28, 2012 1:24:44 PM GMT -05:00 US/Canada Eastern
> > Subject: Re: [pl-wonks] soliciting proofs for a trivial theorem
> >
> > Thank you James. The lemma works.
> >
> > I'm not sure if I got the optimal sequence of tactics though. I had to
> > induct on x first, then to 'intros' twice at two branches. Otherwise
> > the induction hypothesis will not be universally quantified. I would
> > appreciate a neater way to deal with this.
> >
> > Here is my little ugly proof of the lemma:
> >
> > Lemma even_y : forall x y : nat,
> > evenb y = true -> evenb (double x y) = true.
> >
> > Proof.
> > induction x.
> > intros.
> > simpl.
> > apply H.
> > intros.
> > simpl.
> > apply IHx.
> > simpl.
> > apply H.
> > Qed.
> >
> > The theorem is trivially proved using this lemma:
> >
> > Theorem even_double : forall x:nat,
> > evenb (double x 0) = true.
> > Proof.
> > intros.
> > apply even_y.
> > reflexivity.
> > Qed.
> >
> >
> > I also found another lemma that works:
> >
> > Lemma even_ss : forall x y : nat,
> > evenb (double x y) = evenb (double x (S (S y))).
> >
> > It makes the proof of the theorem a little longer though:
> >
> > Theorem even_double : forall x:nat,
> > evenb (double x 0) = true.
> > Proof.
> > Restart.
> > intros.
> > induction x.
> > reflexivity.
> > simpl.
> > rewrite <- even_ss.
> > apply IHx.
> > Qed.
> >
> >
> > I'll appreciate any other tricks. Thank you.
> >
> >
> > -- Yin
> >
> >
> > On Sat, Apr 28, 2012 at 12:25 PM, James T. Perconti
> > <> wrote:
> >> Yin,
> >> The lemma you want is the generalization of your theorem over the
> value of the accumulator:
> >>
> >> Lemma even_double : forall x n,
> >> evenb n = true -> evenb (double x n) = true.
> >>
> >> Proving this is now a simple induction on x, and specializing n to 0
> afterward is of course trivial.
> >> I'm not sure what other lemma(s) one might choose instead of this;
> maybe that double x n = (double x 0) + n and then that the sum of even nats
> is even? But the first thing is much simpler.
> >> --Jamie
> >>
> >> ----- Original Message -----
> >> From: "Yin ****" <>
> >> To: "IUCS Programming Languages"
> >> Sent: Saturday, April 28, 2012 12:07:47 PM GMT -05:00 US/Canada Eastern
> >> Subject: [pl-wonks] soliciting proofs for a trivial theorem
> >>
> >> Hello,
> >>
> >> I'm wondering what's the best way to prove this seemingly trivial
> >> theorem (in Coq):
> >>
> >> Theorem even_double : forall x:nat,
> >> evenb (double x 0) = true.
> >>
> >> The other definitions are:
> >>
> >> Fixpoint evenb (n:nat) : bool :=
> >> match n with
> >> | O => true
> >> | S O => false
> >> | S (S n') => evenb n'
> >> end.
> >>
> >> Fixpoint double (x y : nat) : nat :=
> >> match x with
> >> | O => y
> >> | S x' => double x' (S (S y))
> >> end.
> >>
> >> Everything seems to be straightforward. The only twist is that double
> >> has an accumulator. This is the first theorem in my learning process
> >> where I found that I definitely needed a lemma. The question is, which
> >> lemma is the best one to use?
> >>
> >>
> >> -- Yin
> >> _______________________________________________
> >> PL-wonks mailing list
> >> PL-
> >> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
> >> _______________________________________________
> >> PL-wonks mailing list
> >> PL-
> >> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
> >
> > _______________________________________________
> > PL-wonks mailing list
> > PL-
> > http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
> >
> > _______________________________________________
> > PL-wonks mailing list
> > PL-
> > http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>


That's a very nice lemma! How did you thought of it?


-- Yin


On Sat, Apr 28, 2012 at 3:24 PM, Rebecca Swords <> wrote:
> Hi Yin,
>
> How about this lemma?
>
> Lemma double_s : forall x y:nat, double (S x) y = S (S (double x y)).
>
> The proof for this one is just by induction on x, and then for the main
> theorem, you basically have induction on x, with one rewrite. Both proofs
> are short and straightforward. Perhaps this is what you were looking
> for? Here are my proofs:
>
> Lemma double_s : forall x y:nat, double (S x) y = S (S (double x y)).
> Proof.
>   intros x.
>   induction x.
>   reflexivity.
>
>   intros y.
>   simpl.
>   apply IHx.
> Qed.
>
> Theorem even_double : forall x:nat, evenb (double x 0) = true.
> Proof.
>   induction x.
>   reflexivity.
>
>   rewrite double_s.
>   simpl.
>   apply IHx.
> Qed.
>
>
> -Rebecca
>
>
> On Sat, Apr 28, 2012 at 1:45 PM, Yin **** <> wrote:
>>
>> I had been trying not to use anything fancy (like auto), but I would
>> try ';'. I guess I can think of it as a join point for branches? Thank
>> you.
>>
>>
>> -- Yin
>>
>>
>> On Sat, Apr 28, 2012 at 1:35 PM, James T. Perconti <>
>> wrote:
>> > I just proved it with
>> >   induction x; intros; simpl; auto.
>> > Perhaps you have not learned about ; yet?  It applies a tactic to all
>> > subgoals generated by its left-hand side.
>> >  --Jamie
>> >
>> > ----- Original Message -----
>> > From: "Yin ****" <>
>> > To: "IUCS Programming Languages"
>> > Sent: Saturday, April 28, 2012 1:24:44 PM GMT -05:00 US/Canada Eastern
>> > Subject: Re: [pl-wonks] soliciting proofs for a trivial theorem
>> >
>> > Thank you James. The lemma works.
>> >
>> > I'm not sure if I got the optimal sequence of tactics though. I had to
>> > induct on x first, then to 'intros' twice at two branches. Otherwise
>> > the induction hypothesis will not be universally quantified. I would
>> > appreciate a neater way to deal with this.
>> >
>> > Here is my little ugly proof of the lemma:
>> >
>> > Lemma even_y : forall x y : nat,
>> >  evenb y = true -> evenb (double x y) = true.
>> >
>> > Proof.
>> >  induction x.
>> >  intros.
>> >  simpl.
>> >  apply H.
>> >  intros.
>> >  simpl.
>> >  apply IHx.
>> >  simpl.
>> >  apply H.
>> > Qed.
>> >
>> > The theorem is trivially proved using this lemma:
>> >
>> > Theorem even_double : forall x:nat,
>> >  evenb (double x 0) = true.
>> > Proof.
>> >  intros.
>> >  apply even_y.
>> >  reflexivity.
>> > Qed.
>> >
>> >
>> > I also found another lemma that works:
>> >
>> > Lemma even_ss : forall x y : nat,
>> >  evenb (double x y) = evenb (double x (S (S y))).
>> >
>> > It makes the proof of the theorem a little longer though:
>> >
>> > Theorem even_double : forall x:nat,
>> >  evenb (double x 0) = true.
>> > Proof.
>> >  Restart.
>> >  intros.
>> >  induction x.
>> >  reflexivity.
>> >  simpl.
>> >  rewrite <- even_ss.
>> >  apply IHx.
>> > Qed.
>> >
>> >
>> > I'll appreciate any other tricks. Thank you.
>> >
>> >
>> > -- Yin
>> >
>> >
>> > On Sat, Apr 28, 2012 at 12:25 PM, James T. Perconti
>> > <> wrote:
>> >> Yin,
>> >>  The lemma you want is the generalization of your theorem over the
>> >> value of the accumulator:
>> >>
>> >> Lemma even_double : forall x n,
>> >>  evenb n = true -> evenb (double x n) = true.
>> >>
>> >> Proving this is now a simple induction on x, and specializing n to 0
>> >> afterward is of course trivial.
>> >>  I'm not sure what other lemma(s) one might choose instead of this;
>> >> maybe that double x n = (double x 0) + n and then that the sum of even nats
>> >> is even?  But the first thing is much simpler.
>> >>  --Jamie
>> >>
>> >> ----- Original Message -----
>> >> From: "Yin ****" <>
>> >> To: "IUCS Programming Languages"
>> >> Sent: Saturday, April 28, 2012 12:07:47 PM GMT -05:00 US/Canada Eastern
>> >> Subject: [pl-wonks] soliciting proofs for a trivial theorem
>> >>
>> >> Hello,
>> >>
>> >> I'm wondering what's the best way to prove this seemingly trivial
>> >> theorem (in Coq):
>> >>
>> >> Theorem even_double : forall x:nat,
>> >>  evenb (double x 0) = true.
>> >>
>> >> The other definitions are:
>> >>
>> >> Fixpoint evenb (n:nat) : bool :=
>> >>  match n with
>> >>    | O => true
>> >>    | S O => false
>> >>    | S (S n') => evenb n'
>> >>  end.
>> >>
>> >> Fixpoint double (x y : nat) : nat :=
>> >>  match x with
>> >>    | O => y
>> >>    | S x' => double x' (S (S y))
>> >>  end.
>> >>
>> >> Everything seems to be straightforward. The only twist is that double
>> >> has an accumulator. This is the first theorem in my learning process
>> >> where I found that I definitely needed a lemma. The question is, which
>> >> lemma is the best one to use?
>> >>
>> >>
>> >> -- Yin
>> >> _______________________________________________
>> >> PL-wonks mailing list
>> >> PL-
>> >> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>> >> _______________________________________________
>> >> PL-wonks mailing list
>> >> PL-
>> >> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>> >
>> > _______________________________________________
>> > PL-wonks mailing list
>> > PL-
>> > http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>> >
>> > _______________________________________________
>> > PL-wonks mailing list
>> > PL-
>> > http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>>
>> _______________________________________________
>> PL-wonks mailing list
>> PL-
>> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>
>
>
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>

_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

Hello,

I'm wondering what's the best way to prove this seemingly trivial
theorem (in Coq):

Theorem even_double : forall x:nat,
evenb (double x 0) = true.

The other definitions are:

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

Fixpoint double (x y : nat) : nat :=
match x with
| O => y
| S x' => double x' (S (S y))
end.

Everything seems to be straightforward. The only twist is that double
has an accumulator. This is the first theorem in my learning process
where I found that I definitely needed a lemma. The question is, which
lemma is the best one to use?


-- Yin
_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
)
Yin,
The lemma you want is the generalization of your theorem over the value of the accumulator:

Lemma even_double : forall x n,
evenb n = true -> evenb (double x n) = true.

Proving this is now a simple induction on x, and specializing n to 0 afterward is of course trivial.
I'm not sure what other lemma(s) one might choose instead of this; maybe that double x n = (double x 0) + n and then that the sum of even nats is even? But the first thing is much simpler.
--Jamie

----- Original Message -----
From: "Yin ****" <>
To: "IUCS Programming Languages"
Sent: Saturday, April 28, 2012 12:07:47 PM GMT -05:00 US/Canada Eastern
Subject: [pl-wonks] soliciting proofs for a trivial theorem

Hello,

I'm wondering what's the best way to prove this seemingly trivial
theorem (in Coq):

Theorem even_double : forall x:nat,
evenb (double x 0) = true.

The other definitions are:

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

Fixpoint double (x y : nat) : nat :=
match x with
| O => y
| S x' => double x' (S (S y))
end.

Everything seems to be straightforward. The only twist is that double
has an accumulator. This is the first theorem in my learning process
where I found that I definitely needed a lemma. The question is, which
lemma is the best one to use?


-- Yin
_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
)
Thank you James. The lemma works.

I'm not sure if I got the optimal sequence of tactics though. I had to
induct on x first, then to 'intros' twice at two branches. Otherwise
the induction hypothesis will not be universally quantified. I would
appreciate a neater way to deal with this.

Here is my little ugly proof of the lemma:

Lemma even_y : forall x y : nat,
evenb y = true -> evenb (double x y) = true.

Proof.
induction x.
intros.
simpl.
apply H.
intros.
simpl.
apply IHx.
simpl.
apply H.
Qed.

The theorem is trivially proved using this lemma:

Theorem even_double : forall x:nat,
evenb (double x 0) = true.
Proof.
intros.
apply even_y.
reflexivity.
Qed.


I also found another lemma that works:

Lemma even_ss : forall x y : nat,
evenb (double x y) = evenb (double x (S (S y))).

It makes the proof of the theorem a little longer though:

Theorem even_double : forall x:nat,
evenb (double x 0) = true.
Proof.
Restart.
intros.
induction x.
reflexivity.
simpl.
rewrite <- even_ss.
apply IHx.
Qed.


I'll appreciate any other tricks. Thank you.


-- Yin


On Sat, Apr 28, 2012 at 12:25 PM, James T. Perconti
<> wrote:
> Yin,
>  The lemma you want is the generalization of your theorem over the value of the accumulator:
>
> Lemma even_double : forall x n,
>  evenb n = true -> evenb (double x n) = true.
>
> Proving this is now a simple induction on x, and specializing n to 0 afterward is of course trivial.
>  I'm not sure what other lemma(s) one might choose instead of this; maybe that double x n = (double x 0) + n and then that the sum of even nats is even?  But the first thing is much simpler.
>  --Jamie
>
> ----- Original Message -----
> From: "Yin ****" <>
> To: "IUCS Programming Languages"
> Sent: Saturday, April 28, 2012 12:07:47 PM GMT -05:00 US/Canada Eastern
> Subject: [pl-wonks] soliciting proofs for a trivial theorem
>
> Hello,
>
> I'm wondering what's the best way to prove this seemingly trivial
> theorem (in Coq):
>
> Theorem even_double : forall x:nat,
>  evenb (double x 0) = true.
>
> The other definitions are:
>
> Fixpoint evenb (n:nat) : bool :=
>  match n with
>    | O => true
>    | S O => false
>    | S (S n') => evenb n'
>  end.
>
> Fixpoint double (x y : nat) : nat :=
>  match x with
>    | O => y
>    | S x' => double x' (S (S y))
>  end.
>
> Everything seems to be straightforward. The only twist is that double
> has an accumulator. This is the first theorem in my learning process
> where I found that I definitely needed a lemma. The question is, which
> lemma is the best one to use?
>
>
> -- Yin
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

I just proved it with
induction x; intros; simpl; auto.
Perhaps you have not learned about ; yet? It applies a tactic to all subgoals generated by its left-hand side.
--Jamie

----- Original Message -----
From: "Yin ****" <>
To: "IUCS Programming Languages"
Sent: Saturday, April 28, 2012 1:24:44 PM GMT -05:00 US/Canada Eastern
Subject: Re: [pl-wonks] soliciting proofs for a trivial theorem

Thank you James. The lemma works.

I'm not sure if I got the optimal sequence of tactics though. I had to
induct on x first, then to 'intros' twice at two branches. Otherwise
the induction hypothesis will not be universally quantified. I would
appreciate a neater way to deal with this.

Here is my little ugly proof of the lemma:

Lemma even_y : forall x y : nat,
evenb y = true -> evenb (double x y) = true.

Proof.
induction x.
intros.
simpl.
apply H.
intros.
simpl.
apply IHx.
simpl.
apply H.
Qed.

The theorem is trivially proved using this lemma:

Theorem even_double : forall x:nat,
evenb (double x 0) = true.
Proof.
intros.
apply even_y.
reflexivity.
Qed.


I also found another lemma that works:

Lemma even_ss : forall x y : nat,
evenb (double x y) = evenb (double x (S (S y))).

It makes the proof of the theorem a little longer though:

Theorem even_double : forall x:nat,
evenb (double x 0) = true.
Proof.
Restart.
intros.
induction x.
reflexivity.
simpl.
rewrite <- even_ss.
apply IHx.
Qed.


I'll appreciate any other tricks. Thank you.


-- Yin


On Sat, Apr 28, 2012 at 12:25 PM, James T. Perconti
<> wrote:
> Yin,
>  The lemma you want is the generalization of your theorem over the value of the accumulator:
>
> Lemma even_double : forall x n,
>  evenb n = true -> evenb (double x n) = true.
>
> Proving this is now a simple induction on x, and specializing n to 0 afterward is of course trivial.
>  I'm not sure what other lemma(s) one might choose instead of this; maybe that double x n = (double x 0) + n and then that the sum of even nats is even?  But the first thing is much simpler.
>  --Jamie
>
> ----- Original Message -----
> From: "Yin ****" <>
> To: "IUCS Programming Languages"
> Sent: Saturday, April 28, 2012 12:07:47 PM GMT -05:00 US/Canada Eastern
> Subject: [pl-wonks] soliciting proofs for a trivial theorem
>
> Hello,
>
> I'm wondering what's the best way to prove this seemingly trivial
> theorem (in Coq):
>
> Theorem even_double : forall x:nat,
>  evenb (double x 0) = true.
>
> The other definitions are:
>
> Fixpoint evenb (n:nat) : bool :=
>  match n with
>    | O => true
>    | S O => false
>    | S (S n') => evenb n'
>  end.
>
> Fixpoint double (x y : nat) : nat :=
>  match x with
>    | O => y
>    | S x' => double x' (S (S y))
>  end.
>
> Everything seems to be straightforward. The only twist is that double
> has an accumulator. This is the first theorem in my learning process
> where I found that I definitely needed a lemma. The question is, which
> lemma is the best one to use?
>
>
> -- Yin
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

I had been trying not to use anything fancy (like auto), but I would
try ';'. I guess I can think of it as a join point for branches? Thank
you.


-- Yin


On Sat, Apr 28, 2012 at 1:35 PM, James T. Perconti <> wrote:
> I just proved it with
>   induction x; intros; simpl; auto.
> Perhaps you have not learned about ; yet?  It applies a tactic to all subgoals generated by its left-hand side.
>  --Jamie
>
> ----- Original Message -----
> From: "Yin ****" <>
> To: "IUCS Programming Languages"
> Sent: Saturday, April 28, 2012 1:24:44 PM GMT -05:00 US/Canada Eastern
> Subject: Re: [pl-wonks] soliciting proofs for a trivial theorem
>
> Thank you James. The lemma works.
>
> I'm not sure if I got the optimal sequence of tactics though. I had to
> induct on x first, then to 'intros' twice at two branches. Otherwise
> the induction hypothesis will not be universally quantified. I would
> appreciate a neater way to deal with this.
>
> Here is my little ugly proof of the lemma:
>
> Lemma even_y : forall x y : nat,
>  evenb y = true -> evenb (double x y) = true.
>
> Proof.
>  induction x.
>  intros.
>  simpl.
>  apply H.
>  intros.
>  simpl.
>  apply IHx.
>  simpl.
>  apply H.
> Qed.
>
> The theorem is trivially proved using this lemma:
>
> Theorem even_double : forall x:nat,
>  evenb (double x 0) = true.
> Proof.
>  intros.
>  apply even_y.
>  reflexivity.
> Qed.
>
>
> I also found another lemma that works:
>
> Lemma even_ss : forall x y : nat,
>  evenb (double x y) = evenb (double x (S (S y))).
>
> It makes the proof of the theorem a little longer though:
>
> Theorem even_double : forall x:nat,
>  evenb (double x 0) = true.
> Proof.
>  Restart.
>  intros.
>  induction x.
>  reflexivity.
>  simpl.
>  rewrite <- even_ss.
>  apply IHx.
> Qed.
>
>
> I'll appreciate any other tricks. Thank you.
>
>
> -- Yin
>
>
> On Sat, Apr 28, 2012 at 12:25 PM, James T. Perconti
> <> wrote:
>> Yin,
>>  The lemma you want is the generalization of your theorem over the value of the accumulator:
>>
>> Lemma even_double : forall x n,
>>  evenb n = true -> evenb (double x n) = true.
>>
>> Proving this is now a simple induction on x, and specializing n to 0 afterward is of course trivial.
>>  I'm not sure what other lemma(s) one might choose instead of this; maybe that double x n = (double x 0) + n and then that the sum of even nats is even?  But the first thing is much simpler.
>>  --Jamie
>>
>> ----- Original Message -----
>> From: "Yin ****" <>
>> To: "IUCS Programming Languages"
>> Sent: Saturday, April 28, 2012 12:07:47 PM GMT -05:00 US/Canada Eastern
>> Subject: [pl-wonks] soliciting proofs for a trivial theorem
>>
>> Hello,
>>
>> I'm wondering what's the best way to prove this seemingly trivial
>> theorem (in Coq):
>>
>> Theorem even_double : forall x:nat,
>>  evenb (double x 0) = true.
>>
>> The other definitions are:
>>
>> Fixpoint evenb (n:nat) : bool :=
>>  match n with
>>    | O => true
>>    | S O => false
>>    | S (S n') => evenb n'
>>  end.
>>
>> Fixpoint double (x y : nat) : nat :=
>>  match x with
>>    | O => y
>>    | S x' => double x' (S (S y))
>>  end.
>>
>> Everything seems to be straightforward. The only twist is that double
>> has an accumulator. This is the first theorem in my learning process
>> where I found that I definitely needed a lemma. The question is, which
>> lemma is the best one to use?
>>
>>
>> -- Yin
>> _______________________________________________
>> PL-wonks mailing list
>> PL-
>> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>> _______________________________________________
>> PL-wonks mailing list
>> PL-
>> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

Hi Yin,

How about this lemma?

Lemma double_s : forall x y:nat, double (S x) y = S (S (double x y)).

The proof for this one is just by induction on x, and then for the main
theorem, you basically have induction on x, with one rewrite. Both proofs
are short and straightforward. Perhaps this is what you were looking
for? Here are my proofs:

Lemma double_s : forall x y:nat, double (S x) y = S (S (double x y)).
Proof.
intros x.
induction x.
reflexivity.

intros y.
simpl.
apply IHx.
Qed.

Theorem even_double : forall x:nat, evenb (double x 0) = true.
Proof.
induction x.
reflexivity.

rewrite double_s.
simpl.
apply IHx.
Qed.


-Rebecca


On Sat, Apr 28, 2012 at 1:45 PM, Yin **** <> wrote:

> I had been trying not to use anything fancy (like auto), but I would
> try ';'. I guess I can think of it as a join point for branches? Thank
> you.
>
>
> -- Yin
>
>
> On Sat, Apr 28, 2012 at 1:35 PM, James T. Perconti <>
> wrote:
> > I just proved it with
> > induction x; intros; simpl; auto.
> > Perhaps you have not learned about ; yet? It applies a tactic to all
> subgoals generated by its left-hand side.
> > --Jamie
> >
> > ----- Original Message -----
> > From: "Yin ****" <>
> > To: "IUCS Programming Languages"
> > Sent: Saturday, April 28, 2012 1:24:44 PM GMT -05:00 US/Canada Eastern
> > Subject: Re: [pl-wonks] soliciting proofs for a trivial theorem
> >
> > Thank you James. The lemma works.
> >
> > I'm not sure if I got the optimal sequence of tactics though. I had to
> > induct on x first, then to 'intros' twice at two branches. Otherwise
> > the induction hypothesis will not be universally quantified. I would
> > appreciate a neater way to deal with this.
> >
> > Here is my little ugly proof of the lemma:
> >
> > Lemma even_y : forall x y : nat,
> > evenb y = true -> evenb (double x y) = true.
> >
> > Proof.
> > induction x.
> > intros.
> > simpl.
> > apply H.
> > intros.
> > simpl.
> > apply IHx.
> > simpl.
> > apply H.
> > Qed.
> >
> > The theorem is trivially proved using this lemma:
> >
> > Theorem even_double : forall x:nat,
> > evenb (double x 0) = true.
> > Proof.
> > intros.
> > apply even_y.
> > reflexivity.
> > Qed.
> >
> >
> > I also found another lemma that works:
> >
> > Lemma even_ss : forall x y : nat,
> > evenb (double x y) = evenb (double x (S (S y))).
> >
> > It makes the proof of the theorem a little longer though:
> >
> > Theorem even_double : forall x:nat,
> > evenb (double x 0) = true.
> > Proof.
> > Restart.
> > intros.
> > induction x.
> > reflexivity.
> > simpl.
> > rewrite <- even_ss.
> > apply IHx.
> > Qed.
> >
> >
> > I'll appreciate any other tricks. Thank you.
> >
> >
> > -- Yin
> >
> >
> > On Sat, Apr 28, 2012 at 12:25 PM, James T. Perconti
> > <> wrote:
> >> Yin,
> >> The lemma you want is the generalization of your theorem over the
> value of the accumulator:
> >>
> >> Lemma even_double : forall x n,
> >> evenb n = true -> evenb (double x n) = true.
> >>
> >> Proving this is now a simple induction on x, and specializing n to 0
> afterward is of course trivial.
> >> I'm not sure what other lemma(s) one might choose instead of this;
> maybe that double x n = (double x 0) + n and then that the sum of even nats
> is even? But the first thing is much simpler.
> >> --Jamie
> >>
> >> ----- Original Message -----
> >> From: "Yin ****" <>
> >> To: "IUCS Programming Languages"
> >> Sent: Saturday, April 28, 2012 12:07:47 PM GMT -05:00 US/Canada Eastern
> >> Subject: [pl-wonks] soliciting proofs for a trivial theorem
> >>
> >> Hello,
> >>
> >> I'm wondering what's the best way to prove this seemingly trivial
> >> theorem (in Coq):
> >>
> >> Theorem even_double : forall x:nat,
> >> evenb (double x 0) = true.
> >>
> >> The other definitions are:
> >>
> >> Fixpoint evenb (n:nat) : bool :=
> >> match n with
> >> | O => true
> >> | S O => false
> >> | S (S n') => evenb n'
> >> end.
> >>
> >> Fixpoint double (x y : nat) : nat :=
> >> match x with
> >> | O => y
> >> | S x' => double x' (S (S y))
> >> end.
> >>
> >> Everything seems to be straightforward. The only twist is that double
> >> has an accumulator. This is the first theorem in my learning process
> >> where I found that I definitely needed a lemma. The question is, which
> >> lemma is the best one to use?
> >>
> >>
> >> -- Yin
> >> _______________________________________________
> >> PL-wonks mailing list
> >> PL-
> >> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
> >> _______________________________________________
> >> PL-wonks mailing list
> >> PL-
> >> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
> >
> > _______________________________________________
> > PL-wonks mailing list
> > PL-
> > http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
> >
> > _______________________________________________
> > PL-wonks mailing list
> > PL-
> > http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>


That's a very nice lemma! How did you thought of it?


-- Yin


On Sat, Apr 28, 2012 at 3:24 PM, Rebecca Swords <> wrote:
> Hi Yin,
>
> How about this lemma?
>
> Lemma double_s : forall x y:nat, double (S x) y = S (S (double x y)).
>
> The proof for this one is just by induction on x, and then for the main
> theorem, you basically have induction on x, with one rewrite. Both proofs
> are short and straightforward. Perhaps this is what you were looking
> for? Here are my proofs:
>
> Lemma double_s : forall x y:nat, double (S x) y = S (S (double x y)).
> Proof.
>   intros x.
>   induction x.
>   reflexivity.
>
>   intros y.
>   simpl.
>   apply IHx.
> Qed.
>
> Theorem even_double : forall x:nat, evenb (double x 0) = true.
> Proof.
>   induction x.
>   reflexivity.
>
>   rewrite double_s.
>   simpl.
>   apply IHx.
> Qed.
>
>
> -Rebecca
>
>
> On Sat, Apr 28, 2012 at 1:45 PM, Yin **** <> wrote:
>>
>> I had been trying not to use anything fancy (like auto), but I would
>> try ';'. I guess I can think of it as a join point for branches? Thank
>> you.
>>
>>
>> -- Yin
>>
>>
>> On Sat, Apr 28, 2012 at 1:35 PM, James T. Perconti <>
>> wrote:
>> > I just proved it with
>> >   induction x; intros; simpl; auto.
>> > Perhaps you have not learned about ; yet?  It applies a tactic to all
>> > subgoals generated by its left-hand side.
>> >  --Jamie
>> >
>> > ----- Original Message -----
>> > From: "Yin ****" <>
>> > To: "IUCS Programming Languages"
>> > Sent: Saturday, April 28, 2012 1:24:44 PM GMT -05:00 US/Canada Eastern
>> > Subject: Re: [pl-wonks] soliciting proofs for a trivial theorem
>> >
>> > Thank you James. The lemma works.
>> >
>> > I'm not sure if I got the optimal sequence of tactics though. I had to
>> > induct on x first, then to 'intros' twice at two branches. Otherwise
>> > the induction hypothesis will not be universally quantified. I would
>> > appreciate a neater way to deal with this.
>> >
>> > Here is my little ugly proof of the lemma:
>> >
>> > Lemma even_y : forall x y : nat,
>> >  evenb y = true -> evenb (double x y) = true.
>> >
>> > Proof.
>> >  induction x.
>> >  intros.
>> >  simpl.
>> >  apply H.
>> >  intros.
>> >  simpl.
>> >  apply IHx.
>> >  simpl.
>> >  apply H.
>> > Qed.
>> >
>> > The theorem is trivially proved using this lemma:
>> >
>> > Theorem even_double : forall x:nat,
>> >  evenb (double x 0) = true.
>> > Proof.
>> >  intros.
>> >  apply even_y.
>> >  reflexivity.
>> > Qed.
>> >
>> >
>> > I also found another lemma that works:
>> >
>> > Lemma even_ss : forall x y : nat,
>> >  evenb (double x y) = evenb (double x (S (S y))).
>> >
>> > It makes the proof of the theorem a little longer though:
>> >
>> > Theorem even_double : forall x:nat,
>> >  evenb (double x 0) = true.
>> > Proof.
>> >  Restart.
>> >  intros.
>> >  induction x.
>> >  reflexivity.
>> >  simpl.
>> >  rewrite <- even_ss.
>> >  apply IHx.
>> > Qed.
>> >
>> >
>> > I'll appreciate any other tricks. Thank you.
>> >
>> >
>> > -- Yin
>> >
>> >
>> > On Sat, Apr 28, 2012 at 12:25 PM, James T. Perconti
>> > <> wrote:
>> >> Yin,
>> >>  The lemma you want is the generalization of your theorem over the
>> >> value of the accumulator:
>> >>
>> >> Lemma even_double : forall x n,
>> >>  evenb n = true -> evenb (double x n) = true.
>> >>
>> >> Proving this is now a simple induction on x, and specializing n to 0
>> >> afterward is of course trivial.
>> >>  I'm not sure what other lemma(s) one might choose instead of this;
>> >> maybe that double x n = (double x 0) + n and then that the sum of even nats
>> >> is even?  But the first thing is much simpler.
>> >>  --Jamie
>> >>
>> >> ----- Original Message -----
>> >> From: "Yin ****" <>
>> >> To: "IUCS Programming Languages"
>> >> Sent: Saturday, April 28, 2012 12:07:47 PM GMT -05:00 US/Canada Eastern
>> >> Subject: [pl-wonks] soliciting proofs for a trivial theorem
>> >>
>> >> Hello,
>> >>
>> >> I'm wondering what's the best way to prove this seemingly trivial
>> >> theorem (in Coq):
>> >>
>> >> Theorem even_double : forall x:nat,
>> >>  evenb (double x 0) = true.
>> >>
>> >> The other definitions are:
>> >>
>> >> Fixpoint evenb (n:nat) : bool :=
>> >>  match n with
>> >>    | O => true
>> >>    | S O => false
>> >>    | S (S n') => evenb n'
>> >>  end.
>> >>
>> >> Fixpoint double (x y : nat) : nat :=
>> >>  match x with
>> >>    | O => y
>> >>    | S x' => double x' (S (S y))
>> >>  end.
>> >>
>> >> Everything seems to be straightforward. The only twist is that double
>> >> has an accumulator. This is the first theorem in my learning process
>> >> where I found that I definitely needed a lemma. The question is, which
>> >> lemma is the best one to use?
>> >>
>> >>
>> >> -- Yin
>> >> _______________________________________________
>> >> PL-wonks mailing list
>> >> PL-
>> >> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>> >> _______________________________________________
>> >> PL-wonks mailing list
>> >> PL-
>> >> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>> >
>> > _______________________________________________
>> > PL-wonks mailing list
>> > PL-
>> > http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>> >
>> > _______________________________________________
>> > PL-wonks mailing list
>> > PL-
>> > http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>>
>> _______________________________________________
>> PL-wonks mailing list
>> PL-
>> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>
>
>
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>

_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

Thanks for the responses :-) Now I'm surprised that we have three
lemmas that all work! (still welcoming more of them).

Now my questions is, which lemma is the weakest, say we hope to find a
lemma that tells us nothing more than proving the theorem?


(* James *)
Lemma even_y :
forall x y : nat,
evenb y = true -> evenb (double x y) = true.


(* Rebecca *)
Lemma double_s :
forall x y : nat,
double (S x) y = S (S (double x y)).


(* Yin *)
Lemma even_ss :
forall x y : nat,
evenb (double x y) = evenb (double x (S (S y))).



-- Yin


On Sat, Apr 28, 2012 at 3:38 PM, Yin **** <> wrote:
> That's a very nice lemma! How did you thought of it?
>
>
> -- Yin
>
>
> On Sat, Apr 28, 2012 at 3:24 PM, Rebecca Swords <> wrote:
>> Hi Yin,
>>
>> How about this lemma?
>>
>> Lemma double_s : forall x y:nat, double (S x) y = S (S (double x y)).
>>
>> The proof for this one is just by induction on x, and then for the main
>> theorem, you basically have induction on x, with one rewrite. Both proofs
>> are short and straightforward. Perhaps this is what you were looking
>> for? Here are my proofs:
>>
>> Lemma double_s : forall x y:nat, double (S x) y = S (S (double x y)).
>> Proof.
>>   intros x.
>>   induction x.
>>   reflexivity.
>>
>>   intros y.
>>   simpl.
>>   apply IHx.
>> Qed.
>>
>> Theorem even_double : forall x:nat, evenb (double x 0) = true.
>> Proof.
>>   induction x.
>>   reflexivity.
>>
>>   rewrite double_s.
>>   simpl.
>>   apply IHx.
>> Qed.
>>
>>
>> -Rebecca
>>
>>
>> On Sat, Apr 28, 2012 at 1:45 PM, Yin **** <> wrote:
>>>
>>> I had been trying not to use anything fancy (like auto), but I would
>>> try ';'. I guess I can think of it as a join point for branches? Thank
>>> you.
>>>
>>>
>>> -- Yin
>>>
>>>
>>> On Sat, Apr 28, 2012 at 1:35 PM, James T. Perconti <>
>>> wrote:
>>> > I just proved it with
>>> >   induction x; intros; simpl; auto.
>>> > Perhaps you have not learned about ; yet?  It applies a tactic to all
>>> > subgoals generated by its left-hand side.
>>> >  --Jamie
>>> >
>>> > ----- Original Message -----
>>> > From: "Yin ****" <>
>>> > To: "IUCS Programming Languages"
>>> > Sent: Saturday, April 28, 2012 1:24:44 PM GMT -05:00 US/Canada Eastern
>>> > Subject: Re: [pl-wonks] soliciting proofs for a trivial theorem
>>> >
>>> > Thank you James. The lemma works.
>>> >
>>> > I'm not sure if I got the optimal sequence of tactics though. I had to
>>> > induct on x first, then to 'intros' twice at two branches. Otherwise
>>> > the induction hypothesis will not be universally quantified. I would
>>> > appreciate a neater way to deal with this.
>>> >
>>> > Here is my little ugly proof of the lemma:
>>> >
>>> > Lemma even_y : forall x y : nat,
>>> >  evenb y = true -> evenb (double x y) = true.
>>> >
>>> > Proof.
>>> >  induction x.
>>> >  intros.
>>> >  simpl.
>>> >  apply H.
>>> >  intros.
>>> >  simpl.
>>> >  apply IHx.
>>> >  simpl.
>>> >  apply H.
>>> > Qed.
>>> >
>>> > The theorem is trivially proved using this lemma:
>>> >
>>> > Theorem even_double : forall x:nat,
>>> >  evenb (double x 0) = true.
>>> > Proof.
>>> >  intros.
>>> >  apply even_y.
>>> >  reflexivity.
>>> > Qed.
>>> >
>>> >
>>> > I also found another lemma that works:
>>> >
>>> > Lemma even_ss : forall x y : nat,
>>> >  evenb (double x y) = evenb (double x (S (S y))).
>>> >
>>> > It makes the proof of the theorem a little longer though:
>>> >
>>> > Theorem even_double : forall x:nat,
>>> >  evenb (double x 0) = true.
>>> > Proof.
>>> >  Restart.
>>> >  intros.
>>> >  induction x.
>>> >  reflexivity.
>>> >  simpl.
>>> >  rewrite <- even_ss.
>>> >  apply IHx.
>>> > Qed.
>>> >
>>> >
>>> > I'll appreciate any other tricks. Thank you.
>>> >
>>> >
>>> > -- Yin
>>> >
>>> >
>>> > On Sat, Apr 28, 2012 at 12:25 PM, James T. Perconti
>>> > <> wrote:
>>> >> Yin,
>>> >>  The lemma you want is the generalization of your theorem over the
>>> >> value of the accumulator:
>>> >>
>>> >> Lemma even_double : forall x n,
>>> >>  evenb n = true -> evenb (double x n) = true.
>>> >>
>>> >> Proving this is now a simple induction on x, and specializing n to 0
>>> >> afterward is of course trivial.
>>> >>  I'm not sure what other lemma(s) one might choose instead of this;
>>> >> maybe that double x n = (double x 0) + n and then that the sum of even nats
>>> >> is even?  But the first thing is much simpler.
>>> >>  --Jamie
>>> >>
>>> >> ----- Original Message -----
>>> >> From: "Yin ****" <>
>>> >> To: "IUCS Programming Languages"
>>> >> Sent: Saturday, April 28, 2012 12:07:47 PM GMT -05:00 US/Canada Eastern
>>> >> Subject: [pl-wonks] soliciting proofs for a trivial theorem
>>> >>
>>> >> Hello,
>>> >>
>>> >> I'm wondering what's the best way to prove this seemingly trivial
>>> >> theorem (in Coq):
>>> >>
>>> >> Theorem even_double : forall x:nat,
>>> >>  evenb (double x 0) = true.
>>> >>
>>> >> The other definitions are:
>>> >>
>>> >> Fixpoint evenb (n:nat) : bool :=
>>> >>  match n with
>>> >>    | O => true
>>> >>    | S O => false
>>> >>    | S (S n') => evenb n'
>>> >>  end.
>>> >>
>>> >> Fixpoint double (x y : nat) : nat :=
>>> >>  match x with
>>> >>    | O => y
>>> >>    | S x' => double x' (S (S y))
>>> >>  end.
>>> >>
>>> >> Everything seems to be straightforward. The only twist is that double
>>> >> has an accumulator. This is the first theorem in my learning process
>>> >> where I found that I definitely needed a lemma. The question is, which
>>> >> lemma is the best one to use?
>>> >>
>>> >>
>>> >> -- Yin
>>> >> _______________________________________________
>>> >> PL-wonks mailing list
>>> >> PL-
>>> >> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>>> >> _______________________________________________
>>> >> PL-wonks mailing list
>>> >> PL-
>>> >> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>>> >
>>> > _______________________________________________
>>> > PL-wonks mailing list
>>> > PL-
>>> > http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>>> >
>>> > _______________________________________________
>>> > PL-wonks mailing list
>>> > PL-
>>> > http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>>>
>>> _______________________________________________
>>> PL-wonks mailing list
>>> PL-
>>> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>>
>>
>>
>> _______________________________________________
>> PL-wonks mailing list
>> PL-
>> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>>

_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

Hello,

I'm wondering what's the best way to prove this seemingly trivial
theorem (in Coq):

Theorem even_double : forall x:nat,
evenb (double x 0) = true.

The other definitions are:

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

Fixpoint double (x y : nat) : nat :=
match x with
| O => y
| S x' => double x' (S (S y))
end.

Everything seems to be straightforward. The only twist is that double
has an accumulator. This is the first theorem in my learning process
where I found that I definitely needed a lemma. The question is, which
lemma is the best one to use?


-- Yin
_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
)
Yin,
The lemma you want is the generalization of your theorem over the value of the accumulator:

Lemma even_double : forall x n,
evenb n = true -> evenb (double x n) = true.

Proving this is now a simple induction on x, and specializing n to 0 afterward is of course trivial.
I'm not sure what other lemma(s) one might choose instead of this; maybe that double x n = (double x 0) + n and then that the sum of even nats is even? But the first thing is much simpler.
--Jamie

----- Original Message -----
From: "Yin ****" <>
To: "IUCS Programming Languages"
Sent: Saturday, April 28, 2012 12:07:47 PM GMT -05:00 US/Canada Eastern
Subject: [pl-wonks] soliciting proofs for a trivial theorem

Hello,

I'm wondering what's the best way to prove this seemingly trivial
theorem (in Coq):

Theorem even_double : forall x:nat,
evenb (double x 0) = true.

The other definitions are:

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

Fixpoint double (x y : nat) : nat :=
match x with
| O => y
| S x' => double x' (S (S y))
end.

Everything seems to be straightforward. The only twist is that double
has an accumulator. This is the first theorem in my learning process
where I found that I definitely needed a lemma. The question is, which
lemma is the best one to use?


-- Yin
_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
)
Thank you James. The lemma works.

I'm not sure if I got the optimal sequence of tactics though. I had to
induct on x first, then to 'intros' twice at two branches. Otherwise
the induction hypothesis will not be universally quantified. I would
appreciate a neater way to deal with this.

Here is my little ugly proof of the lemma:

Lemma even_y : forall x y : nat,
evenb y = true -> evenb (double x y) = true.

Proof.
induction x.
intros.
simpl.
apply H.
intros.
simpl.
apply IHx.
simpl.
apply H.
Qed.

The theorem is trivially proved using this lemma:

Theorem even_double : forall x:nat,
evenb (double x 0) = true.
Proof.
intros.
apply even_y.
reflexivity.
Qed.


I also found another lemma that works:

Lemma even_ss : forall x y : nat,
evenb (double x y) = evenb (double x (S (S y))).

It makes the proof of the theorem a little longer though:

Theorem even_double : forall x:nat,
evenb (double x 0) = true.
Proof.
Restart.
intros.
induction x.
reflexivity.
simpl.
rewrite <- even_ss.
apply IHx.
Qed.


I'll appreciate any other tricks. Thank you.


-- Yin


On Sat, Apr 28, 2012 at 12:25 PM, James T. Perconti
<> wrote:
> Yin,
>  The lemma you want is the generalization of your theorem over the value of the accumulator:
>
> Lemma even_double : forall x n,
>  evenb n = true -> evenb (double x n) = true.
>
> Proving this is now a simple induction on x, and specializing n to 0 afterward is of course trivial.
>  I'm not sure what other lemma(s) one might choose instead of this; maybe that double x n = (double x 0) + n and then that the sum of even nats is even?  But the first thing is much simpler.
>  --Jamie
>
> ----- Original Message -----
> From: "Yin ****" <>
> To: "IUCS Programming Languages"
> Sent: Saturday, April 28, 2012 12:07:47 PM GMT -05:00 US/Canada Eastern
> Subject: [pl-wonks] soliciting proofs for a trivial theorem
>
> Hello,
>
> I'm wondering what's the best way to prove this seemingly trivial
> theorem (in Coq):
>
> Theorem even_double : forall x:nat,
>  evenb (double x 0) = true.
>
> The other definitions are:
>
> Fixpoint evenb (n:nat) : bool :=
>  match n with
>    | O => true
>    | S O => false
>    | S (S n') => evenb n'
>  end.
>
> Fixpoint double (x y : nat) : nat :=
>  match x with
>    | O => y
>    | S x' => double x' (S (S y))
>  end.
>
> Everything seems to be straightforward. The only twist is that double
> has an accumulator. This is the first theorem in my learning process
> where I found that I definitely needed a lemma. The question is, which
> lemma is the best one to use?
>
>
> -- Yin
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

I just proved it with
induction x; intros; simpl; auto.
Perhaps you have not learned about ; yet? It applies a tactic to all subgoals generated by its left-hand side.
--Jamie

----- Original Message -----
From: "Yin ****" <>
To: "IUCS Programming Languages"
Sent: Saturday, April 28, 2012 1:24:44 PM GMT -05:00 US/Canada Eastern
Subject: Re: [pl-wonks] soliciting proofs for a trivial theorem

Thank you James. The lemma works.

I'm not sure if I got the optimal sequence of tactics though. I had to
induct on x first, then to 'intros' twice at two branches. Otherwise
the induction hypothesis will not be universally quantified. I would
appreciate a neater way to deal with this.

Here is my little ugly proof of the lemma:

Lemma even_y : forall x y : nat,
evenb y = true -> evenb (double x y) = true.

Proof.
induction x.
intros.
simpl.
apply H.
intros.
simpl.
apply IHx.
simpl.
apply H.
Qed.

The theorem is trivially proved using this lemma:

Theorem even_double : forall x:nat,
evenb (double x 0) = true.
Proof.
intros.
apply even_y.
reflexivity.
Qed.


I also found another lemma that works:

Lemma even_ss : forall x y : nat,
evenb (double x y) = evenb (double x (S (S y))).

It makes the proof of the theorem a little longer though:

Theorem even_double : forall x:nat,
evenb (double x 0) = true.
Proof.
Restart.
intros.
induction x.
reflexivity.
simpl.
rewrite <- even_ss.
apply IHx.
Qed.


I'll appreciate any other tricks. Thank you.


-- Yin


On Sat, Apr 28, 2012 at 12:25 PM, James T. Perconti
<> wrote:
> Yin,
>  The lemma you want is the generalization of your theorem over the value of the accumulator:
>
> Lemma even_double : forall x n,
>  evenb n = true -> evenb (double x n) = true.
>
> Proving this is now a simple induction on x, and specializing n to 0 afterward is of course trivial.
>  I'm not sure what other lemma(s) one might choose instead of this; maybe that double x n = (double x 0) + n and then that the sum of even nats is even?  But the first thing is much simpler.
>  --Jamie
>
> ----- Original Message -----
> From: "Yin ****" <>
> To: "IUCS Programming Languages"
> Sent: Saturday, April 28, 2012 12:07:47 PM GMT -05:00 US/Canada Eastern
> Subject: [pl-wonks] soliciting proofs for a trivial theorem
>
> Hello,
>
> I'm wondering what's the best way to prove this seemingly trivial
> theorem (in Coq):
>
> Theorem even_double : forall x:nat,
>  evenb (double x 0) = true.
>
> The other definitions are:
>
> Fixpoint evenb (n:nat) : bool :=
>  match n with
>    | O => true
>    | S O => false
>    | S (S n') => evenb n'
>  end.
>
> Fixpoint double (x y : nat) : nat :=
>  match x with
>    | O => y
>    | S x' => double x' (S (S y))
>  end.
>
> Everything seems to be straightforward. The only twist is that double
> has an accumulator. This is the first theorem in my learning process
> where I found that I definitely needed a lemma. The question is, which
> lemma is the best one to use?
>
>
> -- Yin
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

I had been trying not to use anything fancy (like auto), but I would
try ';'. I guess I can think of it as a join point for branches? Thank
you.


-- Yin


On Sat, Apr 28, 2012 at 1:35 PM, James T. Perconti <> wrote:
> I just proved it with
>   induction x; intros; simpl; auto.
> Perhaps you have not learned about ; yet?  It applies a tactic to all subgoals generated by its left-hand side.
>  --Jamie
>
> ----- Original Message -----
> From: "Yin ****" <>
> To: "IUCS Programming Languages"
> Sent: Saturday, April 28, 2012 1:24:44 PM GMT -05:00 US/Canada Eastern
> Subject: Re: [pl-wonks] soliciting proofs for a trivial theorem
>
> Thank you James. The lemma works.
>
> I'm not sure if I got the optimal sequence of tactics though. I had to
> induct on x first, then to 'intros' twice at two branches. Otherwise
> the induction hypothesis will not be universally quantified. I would
> appreciate a neater way to deal with this.
>
> Here is my little ugly proof of the lemma:
>
> Lemma even_y : forall x y : nat,
>  evenb y = true -> evenb (double x y) = true.
>
> Proof.
>  induction x.
>  intros.
>  simpl.
>  apply H.
>  intros.
>  simpl.
>  apply IHx.
>  simpl.
>  apply H.
> Qed.
>
> The theorem is trivially proved using this lemma:
>
> Theorem even_double : forall x:nat,
>  evenb (double x 0) = true.
> Proof.
>  intros.
>  apply even_y.
>  reflexivity.
> Qed.
>
>
> I also found another lemma that works:
>
> Lemma even_ss : forall x y : nat,
>  evenb (double x y) = evenb (double x (S (S y))).
>
> It makes the proof of the theorem a little longer though:
>
> Theorem even_double : forall x:nat,
>  evenb (double x 0) = true.
> Proof.
>  Restart.
>  intros.
>  induction x.
>  reflexivity.
>  simpl.
>  rewrite <- even_ss.
>  apply IHx.
> Qed.
>
>
> I'll appreciate any other tricks. Thank you.
>
>
> -- Yin
>
>
> On Sat, Apr 28, 2012 at 12:25 PM, James T. Perconti
> <> wrote:
>> Yin,
>>  The lemma you want is the generalization of your theorem over the value of the accumulator:
>>
>> Lemma even_double : forall x n,
>>  evenb n = true -> evenb (double x n) = true.
>>
>> Proving this is now a simple induction on x, and specializing n to 0 afterward is of course trivial.
>>  I'm not sure what other lemma(s) one might choose instead of this; maybe that double x n = (double x 0) + n and then that the sum of even nats is even?  But the first thing is much simpler.
>>  --Jamie
>>
>> ----- Original Message -----
>> From: "Yin ****" <>
>> To: "IUCS Programming Languages"
>> Sent: Saturday, April 28, 2012 12:07:47 PM GMT -05:00 US/Canada Eastern
>> Subject: [pl-wonks] soliciting proofs for a trivial theorem
>>
>> Hello,
>>
>> I'm wondering what's the best way to prove this seemingly trivial
>> theorem (in Coq):
>>
>> Theorem even_double : forall x:nat,
>>  evenb (double x 0) = true.
>>
>> The other definitions are:
>>
>> Fixpoint evenb (n:nat) : bool :=
>>  match n with
>>    | O => true
>>    | S O => false
>>    | S (S n') => evenb n'
>>  end.
>>
>> Fixpoint double (x y : nat) : nat :=
>>  match x with
>>    | O => y
>>    | S x' => double x' (S (S y))
>>  end.
>>
>> Everything seems to be straightforward. The only twist is that double
>> has an accumulator. This is the first theorem in my learning process
>> where I found that I definitely needed a lemma. The question is, which
>> lemma is the best one to use?
>>
>>
>> -- Yin
>> _______________________________________________
>> PL-wonks mailing list
>> PL-
>> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>> _______________________________________________
>> PL-wonks mailing list
>> PL-
>> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

Hi Yin,

How about this lemma?

Lemma double_s : forall x y:nat, double (S x) y = S (S (double x y)).

The proof for this one is just by induction on x, and then for the main
theorem, you basically have induction on x, with one rewrite. Both proofs
are short and straightforward. Perhaps this is what you were looking
for? Here are my proofs:

Lemma double_s : forall x y:nat, double (S x) y = S (S (double x y)).
Proof.
intros x.
induction x.
reflexivity.

intros y.
simpl.
apply IHx.
Qed.

Theorem even_double : forall x:nat, evenb (double x 0) = true.
Proof.
induction x.
reflexivity.

rewrite double_s.
simpl.
apply IHx.
Qed.


-Rebecca


On Sat, Apr 28, 2012 at 1:45 PM, Yin **** <> wrote:

> I had been trying not to use anything fancy (like auto), but I would
> try ';'. I guess I can think of it as a join point for branches? Thank
> you.
>
>
> -- Yin
>
>
> On Sat, Apr 28, 2012 at 1:35 PM, James T. Perconti <>
> wrote:
> > I just proved it with
> > induction x; intros; simpl; auto.
> > Perhaps you have not learned about ; yet? It applies a tactic to all
> subgoals generated by its left-hand side.
> > --Jamie
> >
> > ----- Original Message -----
> > From: "Yin ****" <>
> > To: "IUCS Programming Languages"
> > Sent: Saturday, April 28, 2012 1:24:44 PM GMT -05:00 US/Canada Eastern
> > Subject: Re: [pl-wonks] soliciting proofs for a trivial theorem
> >
> > Thank you James. The lemma works.
> >
> > I'm not sure if I got the optimal sequence of tactics though. I had to
> > induct on x first, then to 'intros' twice at two branches. Otherwise
> > the induction hypothesis will not be universally quantified. I would
> > appreciate a neater way to deal with this.
> >
> > Here is my little ugly proof of the lemma:
> >
> > Lemma even_y : forall x y : nat,
> > evenb y = true -> evenb (double x y) = true.
> >
> > Proof.
> > induction x.
> > intros.
> > simpl.
> > apply H.
> > intros.
> > simpl.
> > apply IHx.
> > simpl.
> > apply H.
> > Qed.
> >
> > The theorem is trivially proved using this lemma:
> >
> > Theorem even_double : forall x:nat,
> > evenb (double x 0) = true.
> > Proof.
> > intros.
> > apply even_y.
> > reflexivity.
> > Qed.
> >
> >
> > I also found another lemma that works:
> >
> > Lemma even_ss : forall x y : nat,
> > evenb (double x y) = evenb (double x (S (S y))).
> >
> > It makes the proof of the theorem a little longer though:
> >
> > Theorem even_double : forall x:nat,
> > evenb (double x 0) = true.
> > Proof.
> > Restart.
> > intros.
> > induction x.
> > reflexivity.
> > simpl.
> > rewrite <- even_ss.
> > apply IHx.
> > Qed.
> >
> >
> > I'll appreciate any other tricks. Thank you.
> >
> >
> > -- Yin
> >
> >
> > On Sat, Apr 28, 2012 at 12:25 PM, James T. Perconti
> > <> wrote:
> >> Yin,
> >> The lemma you want is the generalization of your theorem over the
> value of the accumulator:
> >>
> >> Lemma even_double : forall x n,
> >> evenb n = true -> evenb (double x n) = true.
> >>
> >> Proving this is now a simple induction on x, and specializing n to 0
> afterward is of course trivial.
> >> I'm not sure what other lemma(s) one might choose instead of this;
> maybe that double x n = (double x 0) + n and then that the sum of even nats
> is even? But the first thing is much simpler.
> >> --Jamie
> >>
> >> ----- Original Message -----
> >> From: "Yin ****" <>
> >> To: "IUCS Programming Languages"
> >> Sent: Saturday, April 28, 2012 12:07:47 PM GMT -05:00 US/Canada Eastern
> >> Subject: [pl-wonks] soliciting proofs for a trivial theorem
> >>
> >> Hello,
> >>
> >> I'm wondering what's the best way to prove this seemingly trivial
> >> theorem (in Coq):
> >>
> >> Theorem even_double : forall x:nat,
> >> evenb (double x 0) = true.
> >>
> >> The other definitions are:
> >>
> >> Fixpoint evenb (n:nat) : bool :=
> >> match n with
> >> | O => true
> >> | S O => false
> >> | S (S n') => evenb n'
> >> end.
> >>
> >> Fixpoint double (x y : nat) : nat :=
> >> match x with
> >> | O => y
> >> | S x' => double x' (S (S y))
> >> end.
> >>
> >> Everything seems to be straightforward. The only twist is that double
> >> has an accumulator. This is the first theorem in my learning process
> >> where I found that I definitely needed a lemma. The question is, which
> >> lemma is the best one to use?
> >>
> >>
> >> -- Yin
> >> _______________________________________________
> >> PL-wonks mailing list
> >> PL-
> >> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
> >> _______________________________________________
> >> PL-wonks mailing list
> >> PL-
> >> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
> >
> > _______________________________________________
> > PL-wonks mailing list
> > PL-
> > http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
> >
> > _______________________________________________
> > PL-wonks mailing list
> > PL-
> > http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>


That's a very nice lemma! How did you thought of it?


-- Yin


On Sat, Apr 28, 2012 at 3:24 PM, Rebecca Swords <> wrote:
> Hi Yin,
>
> How about this lemma?
>
> Lemma double_s : forall x y:nat, double (S x) y = S (S (double x y)).
>
> The proof for this one is just by induction on x, and then for the main
> theorem, you basically have induction on x, with one rewrite. Both proofs
> are short and straightforward. Perhaps this is what you were looking
> for? Here are my proofs:
>
> Lemma double_s : forall x y:nat, double (S x) y = S (S (double x y)).
> Proof.
>   intros x.
>   induction x.
>   reflexivity.
>
>   intros y.
>   simpl.
>   apply IHx.
> Qed.
>
> Theorem even_double : forall x:nat, evenb (double x 0) = true.
> Proof.
>   induction x.
>   reflexivity.
>
>   rewrite double_s.
>   simpl.
>   apply IHx.
> Qed.
>
>
> -Rebecca
>
>
> On Sat, Apr 28, 2012 at 1:45 PM, Yin **** <> wrote:
>>
>> I had been trying not to use anything fancy (like auto), but I would
>> try ';'. I guess I can think of it as a join point for branches? Thank
>> you.
>>
>>
>> -- Yin
>>
>>
>> On Sat, Apr 28, 2012 at 1:35 PM, James T. Perconti <>
>> wrote:
>> > I just proved it with
>> >   induction x; intros; simpl; auto.
>> > Perhaps you have not learned about ; yet?  It applies a tactic to all
>> > subgoals generated by its left-hand side.
>> >  --Jamie
>> >
>> > ----- Original Message -----
>> > From: "Yin ****" <>
>> > To: "IUCS Programming Languages"
>> > Sent: Saturday, April 28, 2012 1:24:44 PM GMT -05:00 US/Canada Eastern
>> > Subject: Re: [pl-wonks] soliciting proofs for a trivial theorem
>> >
>> > Thank you James. The lemma works.
>> >
>> > I'm not sure if I got the optimal sequence of tactics though. I had to
>> > induct on x first, then to 'intros' twice at two branches. Otherwise
>> > the induction hypothesis will not be universally quantified. I would
>> > appreciate a neater way to deal with this.
>> >
>> > Here is my little ugly proof of the lemma:
>> >
>> > Lemma even_y : forall x y : nat,
>> >  evenb y = true -> evenb (double x y) = true.
>> >
>> > Proof.
>> >  induction x.
>> >  intros.
>> >  simpl.
>> >  apply H.
>> >  intros.
>> >  simpl.
>> >  apply IHx.
>> >  simpl.
>> >  apply H.
>> > Qed.
>> >
>> > The theorem is trivially proved using this lemma:
>> >
>> > Theorem even_double : forall x:nat,
>> >  evenb (double x 0) = true.
>> > Proof.
>> >  intros.
>> >  apply even_y.
>> >  reflexivity.
>> > Qed.
>> >
>> >
>> > I also found another lemma that works:
>> >
>> > Lemma even_ss : forall x y : nat,
>> >  evenb (double x y) = evenb (double x (S (S y))).
>> >
>> > It makes the proof of the theorem a little longer though:
>> >
>> > Theorem even_double : forall x:nat,
>> >  evenb (double x 0) = true.
>> > Proof.
>> >  Restart.
>> >  intros.
>> >  induction x.
>> >  reflexivity.
>> >  simpl.
>> >  rewrite <- even_ss.
>> >  apply IHx.
>> > Qed.
>> >
>> >
>> > I'll appreciate any other tricks. Thank you.
>> >
>> >
>> > -- Yin
>> >
>> >
>> > On Sat, Apr 28, 2012 at 12:25 PM, James T. Perconti
>> > <> wrote:
>> >> Yin,
>> >>  The lemma you want is the generalization of your theorem over the
>> >> value of the accumulator:
>> >>
>> >> Lemma even_double : forall x n,
>> >>  evenb n = true -> evenb (double x n) = true.
>> >>
>> >> Proving this is now a simple induction on x, and specializing n to 0
>> >> afterward is of course trivial.
>> >>  I'm not sure what other lemma(s) one might choose instead of this;
>> >> maybe that double x n = (double x 0) + n and then that the sum of even nats
>> >> is even?  But the first thing is much simpler.
>> >>  --Jamie
>> >>
>> >> ----- Original Message -----
>> >> From: "Yin ****" <>
>> >> To: "IUCS Programming Languages"
>> >> Sent: Saturday, April 28, 2012 12:07:47 PM GMT -05:00 US/Canada Eastern
>> >> Subject: [pl-wonks] soliciting proofs for a trivial theorem
>> >>
>> >> Hello,
>> >>
>> >> I'm wondering what's the best way to prove this seemingly trivial
>> >> theorem (in Coq):
>> >>
>> >> Theorem even_double : forall x:nat,
>> >>  evenb (double x 0) = true.
>> >>
>> >> The other definitions are:
>> >>
>> >> Fixpoint evenb (n:nat) : bool :=
>> >>  match n with
>> >>    | O => true
>> >>    | S O => false
>> >>    | S (S n') => evenb n'
>> >>  end.
>> >>
>> >> Fixpoint double (x y : nat) : nat :=
>> >>  match x with
>> >>    | O => y
>> >>    | S x' => double x' (S (S y))
>> >>  end.
>> >>
>> >> Everything seems to be straightforward. The only twist is that double
>> >> has an accumulator. This is the first theorem in my learning process
>> >> where I found that I definitely needed a lemma. The question is, which
>> >> lemma is the best one to use?
>> >>
>> >>
>> >> -- Yin
>> >> _______________________________________________
>> >> PL-wonks mailing list
>> >> PL-
>> >> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>> >> _______________________________________________
>> >> PL-wonks mailing list
>> >> PL-
>> >> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>> >
>> > _______________________________________________
>> > PL-wonks mailing list
>> > PL-
>> > http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>> >
>> > _______________________________________________
>> > PL-wonks mailing list
>> > PL-
>> > http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>>
>> _______________________________________________
>> PL-wonks mailing list
>> PL-
>> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>
>
>
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>

_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

Thanks for the responses :-) Now I'm surprised that we have three
lemmas that all work! (still welcoming more of them).

Now my questions is, which lemma is the weakest, say we hope to find a
lemma that tells us nothing more than proving the theorem?


(* James *)
Lemma even_y :
forall x y : nat,
evenb y = true -> evenb (double x y) = true.


(* Rebecca *)
Lemma double_s :
forall x y : nat,
double (S x) y = S (S (double x y)).


(* Yin *)
Lemma even_ss :
forall x y : nat,
evenb (double x y) = evenb (double x (S (S y))).



-- Yin


On Sat, Apr 28, 2012 at 3:38 PM, Yin **** <> wrote:
> That's a very nice lemma! How did you thought of it?
>
>
> -- Yin
>
>
> On Sat, Apr 28, 2012 at 3:24 PM, Rebecca Swords <> wrote:
>> Hi Yin,
>>
>> How about this lemma?
>>
>> Lemma double_s : forall x y:nat, double (S x) y = S (S (double x y)).
>>
>> The proof for this one is just by induction on x, and then for the main
>> theorem, you basically have induction on x, with one rewrite. Both proofs
>> are short and straightforward. Perhaps this is what you were looking
>> for? Here are my proofs:
>>
>> Lemma double_s : forall x y:nat, double (S x) y = S (S (double x y)).
>> Proof.
>>   intros x.
>>   induction x.
>>   reflexivity.
>>
>>   intros y.
>>   simpl.
>>   apply IHx.
>> Qed.
>>
>> Theorem even_double : forall x:nat, evenb (double x 0) = true.
>> Proof.
>>   induction x.
>>   reflexivity.
>>
>>   rewrite double_s.
>>   simpl.
>>   apply IHx.
>> Qed.
>>
>>
>> -Rebecca
>>
>>
>> On Sat, Apr 28, 2012 at 1:45 PM, Yin **** <> wrote:
>>>
>>> I had been trying not to use anything fancy (like auto), but I would
>>> try ';'. I guess I can think of it as a join point for branches? Thank
>>> you.
>>>
>>>
>>> -- Yin
>>>
>>>
>>> On Sat, Apr 28, 2012 at 1:35 PM, James T. Perconti <>
>>> wrote:
>>> > I just proved it with
>>> >   induction x; intros; simpl; auto.
>>> > Perhaps you have not learned about ; yet?  It applies a tactic to all
>>> > subgoals generated by its left-hand side.
>>> >  --Jamie
>>> >
>>> > ----- Original Message -----
>>> > From: "Yin ****" <>
>>> > To: "IUCS Programming Languages"
>>> > Sent: Saturday, April 28, 2012 1:24:44 PM GMT -05:00 US/Canada Eastern
>>> > Subject: Re: [pl-wonks] soliciting proofs for a trivial theorem
>>> >
>>> > Thank you James. The lemma works.
>>> >
>>> > I'm not sure if I got the optimal sequence of tactics though. I had to
>>> > induct on x first, then to 'intros' twice at two branches. Otherwise
>>> > the induction hypothesis will not be universally quantified. I would
>>> > appreciate a neater way to deal with this.
>>> >
>>> > Here is my little ugly proof of the lemma:
>>> >
>>> > Lemma even_y : forall x y : nat,
>>> >  evenb y = true -> evenb (double x y) = true.
>>> >
>>> > Proof.
>>> >  induction x.
>>> >  intros.
>>> >  simpl.
>>> >  apply H.
>>> >  intros.
>>> >  simpl.
>>> >  apply IHx.
>>> >  simpl.
>>> >  apply H.
>>> > Qed.
>>> >
>>> > The theorem is trivially proved using this lemma:
>>> >
>>> > Theorem even_double : forall x:nat,
>>> >  evenb (double x 0) = true.
>>> > Proof.
>>> >  intros.
>>> >  apply even_y.
>>> >  reflexivity.
>>> > Qed.
>>> >
>>> >
>>> > I also found another lemma that works:
>>> >
>>> > Lemma even_ss : forall x y : nat,
>>> >  evenb (double x y) = evenb (double x (S (S y))).
>>> >
>>> > It makes the proof of the theorem a little longer though:
>>> >
>>> > Theorem even_double : forall x:nat,
>>> >  evenb (double x 0) = true.
>>> > Proof.
>>> >  Restart.
>>> >  intros.
>>> >  induction x.
>>> >  reflexivity.
>>> >  simpl.
>>> >  rewrite <- even_ss.
>>> >  apply IHx.
>>> > Qed.
>>> >
>>> >
>>> > I'll appreciate any other tricks. Thank you.
>>> >
>>> >
>>> > -- Yin
>>> >
>>> >
>>> > On Sat, Apr 28, 2012 at 12:25 PM, James T. Perconti
>>> > <> wrote:
>>> >> Yin,
>>> >>  The lemma you want is the generalization of your theorem over the
>>> >> value of the accumulator:
>>> >>
>>> >> Lemma even_double : forall x n,
>>> >>  evenb n = true -> evenb (double x n) = true.
>>> >>
>>> >> Proving this is now a simple induction on x, and specializing n to 0
>>> >> afterward is of course trivial.
>>> >>  I'm not sure what other lemma(s) one might choose instead of this;
>>> >> maybe that double x n = (double x 0) + n and then that the sum of even nats
>>> >> is even?  But the first thing is much simpler.
>>> >>  --Jamie
>>> >>
>>> >> ----- Original Message -----
>>> >> From: "Yin ****" <>
>>> >> To: "IUCS Programming Languages"
>>> >> Sent: Saturday, April 28, 2012 12:07:47 PM GMT -05:00 US/Canada Eastern
>>> >> Subject: [pl-wonks] soliciting proofs for a trivial theorem
>>> >>
>>> >> Hello,
>>> >>
>>> >> I'm wondering what's the best way to prove this seemingly trivial
>>> >> theorem (in Coq):
>>> >>
>>> >> Theorem even_double : forall x:nat,
>>> >>  evenb (double x 0) = true.
>>> >>
>>> >> The other definitions are:
>>> >>
>>> >> Fixpoint evenb (n:nat) : bool :=
>>> >>  match n with
>>> >>    | O => true
>>> >>    | S O => false
>>> >>    | S (S n') => evenb n'
>>> >>  end.
>>> >>
>>> >> Fixpoint double (x y : nat) : nat :=
>>> >>  match x with
>>> >>    | O => y
>>> >>    | S x' => double x' (S (S y))
>>> >>  end.
>>> >>
>>> >> Everything seems to be straightforward. The only twist is that double
>>> >> has an accumulator. This is the first theorem in my learning process
>>> >> where I found that I definitely needed a lemma. The question is, which
>>> >> lemma is the best one to use?
>>> >>
>>> >>
>>> >> -- Yin
>>> >> _______________________________________________
>>> >> PL-wonks mailing list
>>> >> PL-
>>> >> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>>> >> _______________________________________________
>>> >> PL-wonks mailing list
>>> >> PL-
>>> >> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>>> >
>>> > _______________________________________________
>>> > PL-wonks mailing list
>>> > PL-
>>> > http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>>> >
>>> > _______________________________________________
>>> > PL-wonks mailing list
>>> > PL-
>>> > http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>>>
>>> _______________________________________________
>>> PL-wonks mailing list
>>> PL-
>>> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>>
>>
>>
>> _______________________________________________
>> PL-wonks mailing list
>> PL-
>> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>>

_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

Hi Yin,

Here are some of the things I was thinking about when I came up with the
lemma. I was looking for a way to take advantage of the structure of even
numbers in the definition of evenb. To do that, I had to have to have S (S
something). I also thought it would be better to say something about how
the final result of double changes, rather than how y changes.

And in the inductive proof of even_double, the proof goal was to show that
(double (S x) 0) is even, so this lemma gives you a statement about
doubling the successor of a number.

For your question about comparing these lemmas, I'm not sure how to decide
whether one is stronger or weaker than another, but I think Jamie's is most
closely fitted to the original theorem. His lemma is only applicable when y
is even (which is the only case that matters for even_double), and it makes
almost the same statement as the original theorem.

With transitivity, yours is a statement about both even and odd values for
y. It says that for a given x, (double x y) for even values of y is either
always even or always odd, and similarly for odd values of y. Since yours
applies to both even and odd y values, I think it's probably more widely
applicable than Jamie's.

Mine doesn't say anything about evenness, oddness, or y; it's a statement
relating the results of applying double to different values of x for a
given y. I think it's probably the most general of the three lemmas. (You
can easily use it to prove the stronger theorem that double is semantically
correct, i.e., (double x 0) = x * 2.)

My question is, why do you want the weakest lemma? It seems like once you
start proving things, you might have several theorems to prove about
different aspects of your system and how its components are related. If you
use more general lemmas, it seems like they would be more likely to be
reusable in different places.

-Rebecca

On Sat, Apr 28, 2012 at 4:02 PM, Yin **** <> wrote:

> Thanks for the responses :-) Now I'm surprised that we have three
> lemmas that all work! (still welcoming more of them).
>
> Now my questions is, which lemma is the weakest, say we hope to find a
> lemma that tells us nothing more than proving the theorem?
>
>
> (* James *)
> Lemma even_y :
> forall x y : nat,
> evenb y = true -> evenb (double x y) = true.
>
>
> (* Rebecca *)
> Lemma double_s :
> forall x y : nat,
> double (S x) y = S (S (double x y)).
>
>
> (* Yin *)
> Lemma even_ss :
> forall x y : nat,
> evenb (double x y) = evenb (double x (S (S y))).
>
>
>
> -- Yin
>
>
> On Sat, Apr 28, 2012 at 3:38 PM, Yin **** <> wrote:
> > That's a very nice lemma! How did you thought of it?
> >
> >
> > -- Yin
> >
> >
> > On Sat, Apr 28, 2012 at 3:24 PM, Rebecca Swords <>
> wrote:
> >> Hi Yin,
> >>
> >> How about this lemma?
> >>
> >> Lemma double_s : forall x y:nat, double (S x) y = S (S (double x y)).
> >>
> >> The proof for this one is just by induction on x, and then for the main
> >> theorem, you basically have induction on x, with one rewrite. Both
> proofs
> >> are short and straightforward. Perhaps this is what you were looking
> >> for? Here are my proofs:
> >>
> >> Lemma double_s : forall x y:nat, double (S x) y = S (S (double x y)).
> >> Proof.
> >> intros x.
> >> induction x.
> >> reflexivity.
> >>
> >> intros y.
> >> simpl.
> >> apply IHx.
> >> Qed.
> >>
> >> Theorem even_double : forall x:nat, evenb (double x 0) = true.
> >> Proof.
> >> induction x.
> >> reflexivity.
> >>
> >> rewrite double_s.
> >> simpl.
> >> apply IHx.
> >> Qed.
> >>
> >>
> >> -Rebecca
> >>
> >>
> >> On Sat, Apr 28, 2012 at 1:45 PM, Yin **** <> wrote:
> >>>
> >>> I had been trying not to use anything fancy (like auto), but I would
> >>> try ';'. I guess I can think of it as a join point for branches? Thank
> >>> you.
> >>>
> >>>
> >>> -- Yin
> >>>
> >>>
> >>> On Sat, Apr 28, 2012 at 1:35 PM, James T. Perconti <
> >
> >>> wrote:
> >>> > I just proved it with
> >>> > induction x; intros; simpl; auto.
> >>> > Perhaps you have not learned about ; yet? It applies a tactic to all
> >>> > subgoals generated by its left-hand side.
> >>> > --Jamie
> >>> >
> >>> > ----- Original Message -----
> >>> > From: "Yin ****" <>
> >>> > To: "IUCS Programming Languages"
> >>> > Sent: Saturday, April 28, 2012 1:24:44 PM GMT -05:00 US/Canada
> Eastern
> >>> > Subject: Re: [pl-wonks] soliciting proofs for a trivial theorem
> >>> >
> >>> > Thank you James. The lemma works.
> >>> >
> >>> > I'm not sure if I got the optimal sequence of tactics though. I had
> to
> >>> > induct on x first, then to 'intros' twice at two branches. Otherwise
> >>> > the induction hypothesis will not be universally quantified. I would
> >>> > appreciate a neater way to deal with this.
> >>> >
> >>> > Here is my little ugly proof of the lemma:
> >>> >
> >>> > Lemma even_y : forall x y : nat,
> >>> > evenb y = true -> evenb (double x y) = true.
> >>> >
> >>> > Proof.
> >>> > induction x.
> >>> > intros.
> >>> > simpl.
> >>> > apply H.
> >>> > intros.
> >>> > simpl.
> >>> > apply IHx.
> >>> > simpl.
> >>> > apply H.
> >>> > Qed.
> >>> >
> >>> > The theorem is trivially proved using this lemma:
> >>> >
> >>> > Theorem even_double : forall x:nat,
> >>> > evenb (double x 0) = true.
> >>> > Proof.
> >>> > intros.
> >>> > apply even_y.
> >>> > reflexivity.
> >>> > Qed.
> >>> >
> >>> >
> >>> > I also found another lemma that works:
> >>> >
> >>> > Lemma even_ss : forall x y : nat,
> >>> > evenb (double x y) = evenb (double x (S (S y))).
> >>> >
> >>> > It makes the proof of the theorem a little longer though:
> >>> >
> >>> > Theorem even_double : forall x:nat,
> >>> > evenb (double x 0) = true.
> >>> > Proof.
> >>> > Restart.
> >>> > intros.
> >>> > induction x.
> >>> > reflexivity.
> >>> > simpl.
> >>> > rewrite <- even_ss.
> >>> > apply IHx.
> >>> > Qed.
> >>> >
> >>> >
> >>> > I'll appreciate any other tricks. Thank you.
> >>> >
> >>> >
> >>> > -- Yin
> >>> >
> >>> >
> >>> > On Sat, Apr 28, 2012 at 12:25 PM, James T. Perconti
> >>> > <> wrote:
> >>> >> Yin,
> >>> >> The lemma you want is the generalization of your theorem over the
> >>> >> value of the accumulator:
> >>> >>
> >>> >> Lemma even_double : forall x n,
> >>> >> evenb n = true -> evenb (double x n) = true.
> >>> >>
> >>> >> Proving this is now a simple induction on x, and specializing n to 0
> >>> >> afterward is of course trivial.
> >>> >> I'm not sure what other lemma(s) one might choose instead of this;
> >>> >> maybe that double x n = (double x 0) + n and then that the sum of
> even nats
> >>> >> is even? But the first thing is much simpler.
> >>> >> --Jamie
> >>> >>
> >>> >> ----- Original Message -----
> >>> >> From: "Yin ****" <>
> >>> >> To: "IUCS Programming Languages"
> >>> >> Sent: Saturday, April 28, 2012 12:07:47 PM GMT -05:00 US/Canada
> Eastern
> >>> >> Subject: [pl-wonks] soliciting proofs for a trivial theorem
> >>> >>
> >>> >> Hello,
> >>> >>
> >>> >> I'm wondering what's the best way to prove this seemingly trivial
> >>> >> theorem (in Coq):
> >>> >>
> >>> >> Theorem even_double : forall x:nat,
> >>> >> evenb (double x 0) = true.
> >>> >>
> >>> >> The other definitions are:
> >>> >>
> >>> >> Fixpoint evenb (n:nat) : bool :=
> >>> >> match n with
> >>> >> | O => true
> >>> >> | S O => false
> >>> >> | S (S n') => evenb n'
> >>> >> end.
> >>> >>
> >>> >> Fixpoint double (x y : nat) : nat :=
> >>> >> match x with
> >>> >> | O => y
> >>> >> | S x' => double x' (S (S y))
> >>> >> end.
> >>> >>
> >>> >> Everything seems to be straightforward. The only twist is that
> double
> >>> >> has an accumulator. This is the first theorem in my learning process
> >>> >> where I found that I definitely needed a lemma. The question is,
> which
> >>> >> lemma is the best one to use?
> >>> >>
> >>> >>
> >>> >> -- Yin
> >>> >> _______________________________________________
> >>> >> PL-wonks mailing list
> >>> >> PL-
> >>> >> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
> >>> >> _______________________________________________
> >>> >> PL-wonks mailing list
> >>> >> PL-
> >>> >> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
> >>> >
> >>> > _______________________________________________
> >>> > PL-wonks mailing list
> >>> > PL-
> >>> > http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
> >>> >
> >>> > _______________________________________________
> >>> > PL-wonks mailing list
> >>> > PL-
> >>> > http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
> >>>
> >>> _______________________________________________
> >>> PL-wonks mailing list
> >>> PL-
> >>> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
> >>
> >>
> >>
> >> _______________________________________________
> >> PL-wonks mailing list
> >> PL-
> >> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
> >>
>
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>

Hello,

I'm wondering what's the best way to prove this seemingly trivial
theorem (in Coq):

Theorem even_double : forall x:nat,
evenb (double x 0) = true.

The other definitions are:

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

Fixpoint double (x y : nat) : nat :=
match x with
| O => y
| S x' => double x' (S (S y))
end.

Everything seems to be straightforward. The only twist is that double
has an accumulator. This is the first theorem in my learning process
where I found that I definitely needed a lemma. The question is, which
lemma is the best one to use?


-- Yin
_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
)
Yin,
The lemma you want is the generalization of your theorem over the value of the accumulator:

Lemma even_double : forall x n,
evenb n = true -> evenb (double x n) = true.

Proving this is now a simple induction on x, and specializing n to 0 afterward is of course trivial.
I'm not sure what other lemma(s) one might choose instead of this; maybe that double x n = (double x 0) + n and then that the sum of even nats is even? But the first thing is much simpler.
--Jamie

----- Original Message -----
From: "Yin ****" <>
To: "IUCS Programming Languages"
Sent: Saturday, April 28, 2012 12:07:47 PM GMT -05:00 US/Canada Eastern
Subject: [pl-wonks] soliciting proofs for a trivial theorem

Hello,

I'm wondering what's the best way to prove this seemingly trivial
theorem (in Coq):

Theorem even_double : forall x:nat,
evenb (double x 0) = true.

The other definitions are:

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

Fixpoint double (x y : nat) : nat :=
match x with
| O => y
| S x' => double x' (S (S y))
end.

Everything seems to be straightforward. The only twist is that double
has an accumulator. This is the first theorem in my learning process
where I found that I definitely needed a lemma. The question is, which
lemma is the best one to use?


-- Yin
_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
)
Thank you James. The lemma works.

I'm not sure if I got the optimal sequence of tactics though. I had to
induct on x first, then to 'intros' twice at two branches. Otherwise
the induction hypothesis will not be universally quantified. I would
appreciate a neater way to deal with this.

Here is my little ugly proof of the lemma:

Lemma even_y : forall x y : nat,
evenb y = true -> evenb (double x y) = true.

Proof.
induction x.
intros.
simpl.
apply H.
intros.
simpl.
apply IHx.
simpl.
apply H.
Qed.

The theorem is trivially proved using this lemma:

Theorem even_double : forall x:nat,
evenb (double x 0) = true.
Proof.
intros.
apply even_y.
reflexivity.
Qed.


I also found another lemma that works:

Lemma even_ss : forall x y : nat,
evenb (double x y) = evenb (double x (S (S y))).

It makes the proof of the theorem a little longer though:

Theorem even_double : forall x:nat,
evenb (double x 0) = true.
Proof.
Restart.
intros.
induction x.
reflexivity.
simpl.
rewrite <- even_ss.
apply IHx.
Qed.


I'll appreciate any other tricks. Thank you.


-- Yin


On Sat, Apr 28, 2012 at 12:25 PM, James T. Perconti
<> wrote:
> Yin,
>  The lemma you want is the generalization of your theorem over the value of the accumulator:
>
> Lemma even_double : forall x n,
>  evenb n = true -> evenb (double x n) = true.
>
> Proving this is now a simple induction on x, and specializing n to 0 afterward is of course trivial.
>  I'm not sure what other lemma(s) one might choose instead of this; maybe that double x n = (double x 0) + n and then that the sum of even nats is even?  But the first thing is much simpler.
>  --Jamie
>
> ----- Original Message -----
> From: "Yin ****" <>
> To: "IUCS Programming Languages"
> Sent: Saturday, April 28, 2012 12:07:47 PM GMT -05:00 US/Canada Eastern
> Subject: [pl-wonks] soliciting proofs for a trivial theorem
>
> Hello,
>
> I'm wondering what's the best way to prove this seemingly trivial
> theorem (in Coq):
>
> Theorem even_double : forall x:nat,
>  evenb (double x 0) = true.
>
> The other definitions are:
>
> Fixpoint evenb (n:nat) : bool :=
>  match n with
>    | O => true
>    | S O => false
>    | S (S n') => evenb n'
>  end.
>
> Fixpoint double (x y : nat) : nat :=
>  match x with
>    | O => y
>    | S x' => double x' (S (S y))
>  end.
>
> Everything seems to be straightforward. The only twist is that double
> has an accumulator. This is the first theorem in my learning process
> where I found that I definitely needed a lemma. The question is, which
> lemma is the best one to use?
>
>
> -- Yin
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

I just proved it with
induction x; intros; simpl; auto.
Perhaps you have not learned about ; yet? It applies a tactic to all subgoals generated by its left-hand side.
--Jamie

----- Original Message -----
From: "Yin ****" <>
To: "IUCS Programming Languages"
Sent: Saturday, April 28, 2012 1:24:44 PM GMT -05:00 US/Canada Eastern
Subject: Re: [pl-wonks] soliciting proofs for a trivial theorem

Thank you James. The lemma works.

I'm not sure if I got the optimal sequence of tactics though. I had to
induct on x first, then to 'intros' twice at two branches. Otherwise
the induction hypothesis will not be universally quantified. I would
appreciate a neater way to deal with this.

Here is my little ugly proof of the lemma:

Lemma even_y : forall x y : nat,
evenb y = true -> evenb (double x y) = true.

Proof.
induction x.
intros.
simpl.
apply H.
intros.
simpl.
apply IHx.
simpl.
apply H.
Qed.

The theorem is trivially proved using this lemma:

Theorem even_double : forall x:nat,
evenb (double x 0) = true.
Proof.
intros.
apply even_y.
reflexivity.
Qed.


I also found another lemma that works:

Lemma even_ss : forall x y : nat,
evenb (double x y) = evenb (double x (S (S y))).

It makes the proof of the theorem a little longer though:

Theorem even_double : forall x:nat,
evenb (double x 0) = true.
Proof.
Restart.
intros.
induction x.
reflexivity.
simpl.
rewrite <- even_ss.
apply IHx.
Qed.


I'll appreciate any other tricks. Thank you.


-- Yin


On Sat, Apr 28, 2012 at 12:25 PM, James T. Perconti
<> wrote:
> Yin,
>  The lemma you want is the generalization of your theorem over the value of the accumulator:
>
> Lemma even_double : forall x n,
>  evenb n = true -> evenb (double x n) = true.
>
> Proving this is now a simple induction on x, and specializing n to 0 afterward is of course trivial.
>  I'm not sure what other lemma(s) one might choose instead of this; maybe that double x n = (double x 0) + n and then that the sum of even nats is even?  But the first thing is much simpler.
>  --Jamie
>
> ----- Original Message -----
> From: "Yin ****" <>
> To: "IUCS Programming Languages"
> Sent: Saturday, April 28, 2012 12:07:47 PM GMT -05:00 US/Canada Eastern
> Subject: [pl-wonks] soliciting proofs for a trivial theorem
>
> Hello,
>
> I'm wondering what's the best way to prove this seemingly trivial
> theorem (in Coq):
>
> Theorem even_double : forall x:nat,
>  evenb (double x 0) = true.
>
> The other definitions are:
>
> Fixpoint evenb (n:nat) : bool :=
>  match n with
>    | O => true
>    | S O => false
>    | S (S n') => evenb n'
>  end.
>
> Fixpoint double (x y : nat) : nat :=
>  match x with
>    | O => y
>    | S x' => double x' (S (S y))
>  end.
>
> Everything seems to be straightforward. The only twist is that double
> has an accumulator. This is the first theorem in my learning process
> where I found that I definitely needed a lemma. The question is, which
> lemma is the best one to use?
>
>
> -- Yin
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

I had been trying not to use anything fancy (like auto), but I would
try ';'. I guess I can think of it as a join point for branches? Thank
you.


-- Yin


On Sat, Apr 28, 2012 at 1:35 PM, James T. Perconti <> wrote:
> I just proved it with
>   induction x; intros; simpl; auto.
> Perhaps you have not learned about ; yet?  It applies a tactic to all subgoals generated by its left-hand side.
>  --Jamie
>
> ----- Original Message -----
> From: "Yin ****" <>
> To: "IUCS Programming Languages"
> Sent: Saturday, April 28, 2012 1:24:44 PM GMT -05:00 US/Canada Eastern
> Subject: Re: [pl-wonks] soliciting proofs for a trivial theorem
>
> Thank you James. The lemma works.
>
> I'm not sure if I got the optimal sequence of tactics though. I had to
> induct on x first, then to 'intros' twice at two branches. Otherwise
> the induction hypothesis will not be universally quantified. I would
> appreciate a neater way to deal with this.
>
> Here is my little ugly proof of the lemma:
>
> Lemma even_y : forall x y : nat,
>  evenb y = true -> evenb (double x y) = true.
>
> Proof.
>  induction x.
>  intros.
>  simpl.
>  apply H.
>  intros.
>  simpl.
>  apply IHx.
>  simpl.
>  apply H.
> Qed.
>
> The theorem is trivially proved using this lemma:
>
> Theorem even_double : forall x:nat,
>  evenb (double x 0) = true.
> Proof.
>  intros.
>  apply even_y.
>  reflexivity.
> Qed.
>
>
> I also found another lemma that works:
>
> Lemma even_ss : forall x y : nat,
>  evenb (double x y) = evenb (double x (S (S y))).
>
> It makes the proof of the theorem a little longer though:
>
> Theorem even_double : forall x:nat,
>  evenb (double x 0) = true.
> Proof.
>  Restart.
>  intros.
>  induction x.
>  reflexivity.
>  simpl.
>  rewrite <- even_ss.
>  apply IHx.
> Qed.
>
>
> I'll appreciate any other tricks. Thank you.
>
>
> -- Yin
>
>
> On Sat, Apr 28, 2012 at 12:25 PM, James T. Perconti
> <> wrote:
>> Yin,
>>  The lemma you want is the generalization of your theorem over the value of the accumulator:
>>
>> Lemma even_double : forall x n,
>>  evenb n = true -> evenb (double x n) = true.
>>
>> Proving this is now a simple induction on x, and specializing n to 0 afterward is of course trivial.
>>  I'm not sure what other lemma(s) one might choose instead of this; maybe that double x n = (double x 0) + n and then that the sum of even nats is even?  But the first thing is much simpler.
>>  --Jamie
>>
>> ----- Original Message -----
>> From: "Yin ****" <>
>> To: "IUCS Programming Languages"
>> Sent: Saturday, April 28, 2012 12:07:47 PM GMT -05:00 US/Canada Eastern
>> Subject: [pl-wonks] soliciting proofs for a trivial theorem
>>
>> Hello,
>>
>> I'm wondering what's the best way to prove this seemingly trivial
>> theorem (in Coq):
>>
>> Theorem even_double : forall x:nat,
>>  evenb (double x 0) = true.
>>
>> The other definitions are:
>>
>> Fixpoint evenb (n:nat) : bool :=
>>  match n with
>>    | O => true
>>    | S O => false
>>    | S (S n') => evenb n'
>>  end.
>>
>> Fixpoint double (x y : nat) : nat :=
>>  match x with
>>    | O => y
>>    | S x' => double x' (S (S y))
>>  end.
>>
>> Everything seems to be straightforward. The only twist is that double
>> has an accumulator. This is the first theorem in my learning process
>> where I found that I definitely needed a lemma. The question is, which
>> lemma is the best one to use?
>>
>>
>> -- Yin
>> _______________________________________________
>> PL-wonks mailing list
>> PL-
>> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>> _______________________________________________
>> PL-wonks mailing list
>> PL-
>> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

Hi Yin,

How about this lemma?

Lemma double_s : forall x y:nat, double (S x) y = S (S (double x y)).

The proof for this one is just by induction on x, and then for the main
theorem, you basically have induction on x, with one rewrite. Both proofs
are short and straightforward. Perhaps this is what you were looking
for? Here are my proofs:

Lemma double_s : forall x y:nat, double (S x) y = S (S (double x y)).
Proof.
intros x.
induction x.
reflexivity.

intros y.
simpl.
apply IHx.
Qed.

Theorem even_double : forall x:nat, evenb (double x 0) = true.
Proof.
induction x.
reflexivity.

rewrite double_s.
simpl.
apply IHx.
Qed.


-Rebecca


On Sat, Apr 28, 2012 at 1:45 PM, Yin **** <> wrote:

> I had been trying not to use anything fancy (like auto), but I would
> try ';'. I guess I can think of it as a join point for branches? Thank
> you.
>
>
> -- Yin
>
>
> On Sat, Apr 28, 2012 at 1:35 PM, James T. Perconti <>
> wrote:
> > I just proved it with
> > induction x; intros; simpl; auto.
> > Perhaps you have not learned about ; yet? It applies a tactic to all
> subgoals generated by its left-hand side.
> > --Jamie
> >
> > ----- Original Message -----
> > From: "Yin ****" <>
> > To: "IUCS Programming Languages"
> > Sent: Saturday, April 28, 2012 1:24:44 PM GMT -05:00 US/Canada Eastern
> > Subject: Re: [pl-wonks] soliciting proofs for a trivial theorem
> >
> > Thank you James. The lemma works.
> >
> > I'm not sure if I got the optimal sequence of tactics though. I had to
> > induct on x first, then to 'intros' twice at two branches. Otherwise
> > the induction hypothesis will not be universally quantified. I would
> > appreciate a neater way to deal with this.
> >
> > Here is my little ugly proof of the lemma:
> >
> > Lemma even_y : forall x y : nat,
> > evenb y = true -> evenb (double x y) = true.
> >
> > Proof.
> > induction x.
> > intros.
> > simpl.
> > apply H.
> > intros.
> > simpl.
> > apply IHx.
> > simpl.
> > apply H.
> > Qed.
> >
> > The theorem is trivially proved using this lemma:
> >
> > Theorem even_double : forall x:nat,
> > evenb (double x 0) = true.
> > Proof.
> > intros.
> > apply even_y.
> > reflexivity.
> > Qed.
> >
> >
> > I also found another lemma that works:
> >
> > Lemma even_ss : forall x y : nat,
> > evenb (double x y) = evenb (double x (S (S y))).
> >
> > It makes the proof of the theorem a little longer though:
> >
> > Theorem even_double : forall x:nat,
> > evenb (double x 0) = true.
> > Proof.
> > Restart.
> > intros.
> > induction x.
> > reflexivity.
> > simpl.
> > rewrite <- even_ss.
> > apply IHx.
> > Qed.
> >
> >
> > I'll appreciate any other tricks. Thank you.
> >
> >
> > -- Yin
> >
> >
> > On Sat, Apr 28, 2012 at 12:25 PM, James T. Perconti
> > <> wrote:
> >> Yin,
> >> The lemma you want is the generalization of your theorem over the
> value of the accumulator:
> >>
> >> Lemma even_double : forall x n,
> >> evenb n = true -> evenb (double x n) = true.
> >>
> >> Proving this is now a simple induction on x, and specializing n to 0
> afterward is of course trivial.
> >> I'm not sure what other lemma(s) one might choose instead of this;
> maybe that double x n = (double x 0) + n and then that the sum of even nats
> is even? But the first thing is much simpler.
> >> --Jamie
> >>
> >> ----- Original Message -----
> >> From: "Yin ****" <>
> >> To: "IUCS Programming Languages"
> >> Sent: Saturday, April 28, 2012 12:07:47 PM GMT -05:00 US/Canada Eastern
> >> Subject: [pl-wonks] soliciting proofs for a trivial theorem
> >>
> >> Hello,
> >>
> >> I'm wondering what's the best way to prove this seemingly trivial
> >> theorem (in Coq):
> >>
> >> Theorem even_double : forall x:nat,
> >> evenb (double x 0) = true.
> >>
> >> The other definitions are:
> >>
> >> Fixpoint evenb (n:nat) : bool :=
> >> match n with
> >> | O => true
> >> | S O => false
> >> | S (S n') => evenb n'
> >> end.
> >>
> >> Fixpoint double (x y : nat) : nat :=
> >> match x with
> >> | O => y
> >> | S x' => double x' (S (S y))
> >> end.
> >>
> >> Everything seems to be straightforward. The only twist is that double
> >> has an accumulator. This is the first theorem in my learning process
> >> where I found that I definitely needed a lemma. The question is, which
> >> lemma is the best one to use?
> >>
> >>
> >> -- Yin
> >> _______________________________________________
> >> PL-wonks mailing list
> >> PL-
> >> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
> >> _______________________________________________
> >> PL-wonks mailing list
> >> PL-
> >> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
> >
> > _______________________________________________
> > PL-wonks mailing list
> > PL-
> > http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
> >
> > _______________________________________________
> > PL-wonks mailing list
> > PL-
> > http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>


That's a very nice lemma! How did you thought of it?


-- Yin


On Sat, Apr 28, 2012 at 3:24 PM, Rebecca Swords <> wrote:
> Hi Yin,
>
> How about this lemma?
>
> Lemma double_s : forall x y:nat, double (S x) y = S (S (double x y)).
>
> The proof for this one is just by induction on x, and then for the main
> theorem, you basically have induction on x, with one rewrite. Both proofs
> are short and straightforward. Perhaps this is what you were looking
> for? Here are my proofs:
>
> Lemma double_s : forall x y:nat, double (S x) y = S (S (double x y)).
> Proof.
>   intros x.
>   induction x.
>   reflexivity.
>
>   intros y.
>   simpl.
>   apply IHx.
> Qed.
>
> Theorem even_double : forall x:nat, evenb (double x 0) = true.
> Proof.
>   induction x.
>   reflexivity.
>
>   rewrite double_s.
>   simpl.
>   apply IHx.
> Qed.
>
>
> -Rebecca
>
>
> On Sat, Apr 28, 2012 at 1:45 PM, Yin **** <> wrote:
>>
>> I had been trying not to use anything fancy (like auto), but I would
>> try ';'. I guess I can think of it as a join point for branches? Thank
>> you.
>>
>>
>> -- Yin
>>
>>
>> On Sat, Apr 28, 2012 at 1:35 PM, James T. Perconti <>
>> wrote:
>> > I just proved it with
>> >   induction x; intros; simpl; auto.
>> > Perhaps you have not learned about ; yet?  It applies a tactic to all
>> > subgoals generated by its left-hand side.
>> >  --Jamie
>> >
>> > ----- Original Message -----
>> > From: "Yin ****" <>
>> > To: "IUCS Programming Languages"
>> > Sent: Saturday, April 28, 2012 1:24:44 PM GMT -05:00 US/Canada Eastern
>> > Subject: Re: [pl-wonks] soliciting proofs for a trivial theorem
>> >
>> > Thank you James. The lemma works.
>> >
>> > I'm not sure if I got the optimal sequence of tactics though. I had to
>> > induct on x first, then to 'intros' twice at two branches. Otherwise
>> > the induction hypothesis will not be universally quantified. I would
>> > appreciate a neater way to deal with this.
>> >
>> > Here is my little ugly proof of the lemma:
>> >
>> > Lemma even_y : forall x y : nat,
>> >  evenb y = true -> evenb (double x y) = true.
>> >
>> > Proof.
>> >  induction x.
>> >  intros.
>> >  simpl.
>> >  apply H.
>> >  intros.
>> >  simpl.
>> >  apply IHx.
>> >  simpl.
>> >  apply H.
>> > Qed.
>> >
>> > The theorem is trivially proved using this lemma:
>> >
>> > Theorem even_double : forall x:nat,
>> >  evenb (double x 0) = true.
>> > Proof.
>> >  intros.
>> >  apply even_y.
>> >  reflexivity.
>> > Qed.
>> >
>> >
>> > I also found another lemma that works:
>> >
>> > Lemma even_ss : forall x y : nat,
>> >  evenb (double x y) = evenb (double x (S (S y))).
>> >
>> > It makes the proof of the theorem a little longer though:
>> >
>> > Theorem even_double : forall x:nat,
>> >  evenb (double x 0) = true.
>> > Proof.
>> >  Restart.
>> >  intros.
>> >  induction x.
>> >  reflexivity.
>> >  simpl.
>> >  rewrite <- even_ss.
>> >  apply IHx.
>> > Qed.
>> >
>> >
>> > I'll appreciate any other tricks. Thank you.
>> >
>> >
>> > -- Yin
>> >
>> >
>> > On Sat, Apr 28, 2012 at 12:25 PM, James T. Perconti
>> > <> wrote:
>> >> Yin,
>> >>  The lemma you want is the generalization of your theorem over the
>> >> value of the accumulator:
>> >>
>> >> Lemma even_double : forall x n,
>> >>  evenb n = true -> evenb (double x n) = true.
>> >>
>> >> Proving this is now a simple induction on x, and specializing n to 0
>> >> afterward is of course trivial.
>> >>  I'm not sure what other lemma(s) one might choose instead of this;
>> >> maybe that double x n = (double x 0) + n and then that the sum of even nats
>> >> is even?  But the first thing is much simpler.
>> >>  --Jamie
>> >>
>> >> ----- Original Message -----
>> >> From: "Yin ****" <>
>> >> To: "IUCS Programming Languages"
>> >> Sent: Saturday, April 28, 2012 12:07:47 PM GMT -05:00 US/Canada Eastern
>> >> Subject: [pl-wonks] soliciting proofs for a trivial theorem
>> >>
>> >> Hello,
>> >>
>> >> I'm wondering what's the best way to prove this seemingly trivial
>> >> theorem (in Coq):
>> >>
>> >> Theorem even_double : forall x:nat,
>> >>  evenb (double x 0) = true.
>> >>
>> >> The other definitions are:
>> >>
>> >> Fixpoint evenb (n:nat) : bool :=
>> >>  match n with
>> >>    | O => true
>> >>    | S O => false
>> >>    | S (S n') => evenb n'
>> >>  end.
>> >>
>> >> Fixpoint double (x y : nat) : nat :=
>> >>  match x with
>> >>    | O => y
>> >>    | S x' => double x' (S (S y))
>> >>  end.
>> >>
>> >> Everything seems to be straightforward. The only twist is that double
>> >> has an accumulator. This is the first theorem in my learning process
>> >> where I found that I definitely needed a lemma. The question is, which
>> >> lemma is the best one to use?
>> >>
>> >>
>> >> -- Yin
>> >> _______________________________________________
>> >> PL-wonks mailing list
>> >> PL-
>> >> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>> >> _______________________________________________
>> >> PL-wonks mailing list
>> >> PL-
>> >> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>> >
>> > _______________________________________________
>> > PL-wonks mailing list
>> > PL-
>> > http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>> >
>> > _______________________________________________
>> > PL-wonks mailing list
>> > PL-
>> > http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>>
>> _______________________________________________
>> PL-wonks mailing list
>> PL-
>> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>
>
>
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>

_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

Thanks for the responses :-) Now I'm surprised that we have three
lemmas that all work! (still welcoming more of them).

Now my questions is, which lemma is the weakest, say we hope to find a
lemma that tells us nothing more than proving the theorem?


(* James *)
Lemma even_y :
forall x y : nat,
evenb y = true -> evenb (double x y) = true.


(* Rebecca *)
Lemma double_s :
forall x y : nat,
double (S x) y = S (S (double x y)).


(* Yin *)
Lemma even_ss :
forall x y : nat,
evenb (double x y) = evenb (double x (S (S y))).



-- Yin


On Sat, Apr 28, 2012 at 3:38 PM, Yin **** <> wrote:
> That's a very nice lemma! How did you thought of it?
>
>
> -- Yin
>
>
> On Sat, Apr 28, 2012 at 3:24 PM, Rebecca Swords <> wrote:
>> Hi Yin,
>>
>> How about this lemma?
>>
>> Lemma double_s : forall x y:nat, double (S x) y = S (S (double x y)).
>>
>> The proof for this one is just by induction on x, and then for the main
>> theorem, you basically have induction on x, with one rewrite. Both proofs
>> are short and straightforward. Perhaps this is what you were looking
>> for? Here are my proofs:
>>
>> Lemma double_s : forall x y:nat, double (S x) y = S (S (double x y)).
>> Proof.
>>   intros x.
>>   induction x.
>>   reflexivity.
>>
>>   intros y.
>>   simpl.
>>   apply IHx.
>> Qed.
>>
>> Theorem even_double : forall x:nat, evenb (double x 0) = true.
>> Proof.
>>   induction x.
>>   reflexivity.
>>
>>   rewrite double_s.
>>   simpl.
>>   apply IHx.
>> Qed.
>>
>>
>> -Rebecca
>>
>>
>> On Sat, Apr 28, 2012 at 1:45 PM, Yin **** <> wrote:
>>>
>>> I had been trying not to use anything fancy (like auto), but I would
>>> try ';'. I guess I can think of it as a join point for branches? Thank
>>> you.
>>>
>>>
>>> -- Yin
>>>
>>>
>>> On Sat, Apr 28, 2012 at 1:35 PM, James T. Perconti <>
>>> wrote:
>>> > I just proved it with
>>> >   induction x; intros; simpl; auto.
>>> > Perhaps you have not learned about ; yet?  It applies a tactic to all
>>> > subgoals generated by its left-hand side.
>>> >  --Jamie
>>> >
>>> > ----- Original Message -----
>>> > From: "Yin ****" <>
>>> > To: "IUCS Programming Languages"
>>> > Sent: Saturday, April 28, 2012 1:24:44 PM GMT -05:00 US/Canada Eastern
>>> > Subject: Re: [pl-wonks] soliciting proofs for a trivial theorem
>>> >
>>> > Thank you James. The lemma works.
>>> >
>>> > I'm not sure if I got the optimal sequence of tactics though. I had to
>>> > induct on x first, then to 'intros' twice at two branches. Otherwise
>>> > the induction hypothesis will not be universally quantified. I would
>>> > appreciate a neater way to deal with this.
>>> >
>>> > Here is my little ugly proof of the lemma:
>>> >
>>> > Lemma even_y : forall x y : nat,
>>> >  evenb y = true -> evenb (double x y) = true.
>>> >
>>> > Proof.
>>> >  induction x.
>>> >  intros.
>>> >  simpl.
>>> >  apply H.
>>> >  intros.
>>> >  simpl.
>>> >  apply IHx.
>>> >  simpl.
>>> >  apply H.
>>> > Qed.
>>> >
>>> > The theorem is trivially proved using this lemma:
>>> >
>>> > Theorem even_double : forall x:nat,
>>> >  evenb (double x 0) = true.
>>> > Proof.
>>> >  intros.
>>> >  apply even_y.
>>> >  reflexivity.
>>> > Qed.
>>> >
>>> >
>>> > I also found another lemma that works:
>>> >
>>> > Lemma even_ss : forall x y : nat,
>>> >  evenb (double x y) = evenb (double x (S (S y))).
>>> >
>>> > It makes the proof of the theorem a little longer though:
>>> >
>>> > Theorem even_double : forall x:nat,
>>> >  evenb (double x 0) = true.
>>> > Proof.
>>> >  Restart.
>>> >  intros.
>>> >  induction x.
>>> >  reflexivity.
>>> >  simpl.
>>> >  rewrite <- even_ss.
>>> >  apply IHx.
>>> > Qed.
>>> >
>>> >
>>> > I'll appreciate any other tricks. Thank you.
>>> >
>>> >
>>> > -- Yin
>>> >
>>> >
>>> > On Sat, Apr 28, 2012 at 12:25 PM, James T. Perconti
>>> > <> wrote:
>>> >> Yin,
>>> >>  The lemma you want is the generalization of your theorem over the
>>> >> value of the accumulator:
>>> >>
>>> >> Lemma even_double : forall x n,
>>> >>  evenb n = true -> evenb (double x n) = true.
>>> >>
>>> >> Proving this is now a simple induction on x, and specializing n to 0
>>> >> afterward is of course trivial.
>>> >>  I'm not sure what other lemma(s) one might choose instead of this;
>>> >> maybe that double x n = (double x 0) + n and then that the sum of even nats
>>> >> is even?  But the first thing is much simpler.
>>> >>  --Jamie
>>> >>
>>> >> ----- Original Message -----
>>> >> From: "Yin ****" <>
>>> >> To: "IUCS Programming Languages"
>>> >> Sent: Saturday, April 28, 2012 12:07:47 PM GMT -05:00 US/Canada Eastern
>>> >> Subject: [pl-wonks] soliciting proofs for a trivial theorem
>>> >>
>>> >> Hello,
>>> >>
>>> >> I'm wondering what's the best way to prove this seemingly trivial
>>> >> theorem (in Coq):
>>> >>
>>> >> Theorem even_double : forall x:nat,
>>> >>  evenb (double x 0) = true.
>>> >>
>>> >> The other definitions are:
>>> >>
>>> >> Fixpoint evenb (n:nat) : bool :=
>>> >>  match n with
>>> >>    | O => true
>>> >>    | S O => false
>>> >>    | S (S n') => evenb n'
>>> >>  end.
>>> >>
>>> >> Fixpoint double (x y : nat) : nat :=
>>> >>  match x with
>>> >>    | O => y
>>> >>    | S x' => double x' (S (S y))
>>> >>  end.
>>> >>
>>> >> Everything seems to be straightforward. The only twist is that double
>>> >> has an accumulator. This is the first theorem in my learning process
>>> >> where I found that I definitely needed a lemma. The question is, which
>>> >> lemma is the best one to use?
>>> >>
>>> >>
>>> >> -- Yin
>>> >> _______________________________________________
>>> >> PL-wonks mailing list
>>> >> PL-
>>> >> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>>> >> _______________________________________________
>>> >> PL-wonks mailing list
>>> >> PL-
>>> >> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>>> >
>>> > _______________________________________________
>>> > PL-wonks mailing list
>>> > PL-
>>> > http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>>> >
>>> > _______________________________________________
>>> > PL-wonks mailing list
>>> > PL-
>>> > http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>>>
>>> _______________________________________________
>>> PL-wonks mailing list
>>> PL-
>>> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>>
>>
>>
>> _______________________________________________
>> PL-wonks mailing list
>> PL-
>> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>>

_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

Hi Yin,

Here are some of the things I was thinking about when I came up with the
lemma. I was looking for a way to take advantage of the structure of even
numbers in the definition of evenb. To do that, I had to have to have S (S
something). I also thought it would be better to say something about how
the final result of double changes, rather than how y changes.

And in the inductive proof of even_double, the proof goal was to show that
(double (S x) 0) is even, so this lemma gives you a statement about
doubling the successor of a number.

For your question about comparing these lemmas, I'm not sure how to decide
whether one is stronger or weaker than another, but I think Jamie's is most
closely fitted to the original theorem. His lemma is only applicable when y
is even (which is the only case that matters for even_double), and it makes
almost the same statement as the original theorem.

With transitivity, yours is a statement about both even and odd values for
y. It says that for a given x, (double x y) for even values of y is either
always even or always odd, and similarly for odd values of y. Since yours
applies to both even and odd y values, I think it's probably more widely
applicable than Jamie's.

Mine doesn't say anything about evenness, oddness, or y; it's a statement
relating the results of applying double to different values of x for a
given y. I think it's probably the most general of the three lemmas. (You
can easily use it to prove the stronger theorem that double is semantically
correct, i.e., (double x 0) = x * 2.)

My question is, why do you want the weakest lemma? It seems like once you
start proving things, you might have several theorems to prove about
different aspects of your system and how its components are related. If you
use more general lemmas, it seems like they would be more likely to be
reusable in different places.

-Rebecca

On Sat, Apr 28, 2012 at 4:02 PM, Yin **** <> wrote:

> Thanks for the responses :-) Now I'm surprised that we have three
> lemmas that all work! (still welcoming more of them).
>
> Now my questions is, which lemma is the weakest, say we hope to find a
> lemma that tells us nothing more than proving the theorem?
>
>
> (* James *)
> Lemma even_y :
> forall x y : nat,
> evenb y = true -> evenb (double x y) = true.
>
>
> (* Rebecca *)
> Lemma double_s :
> forall x y : nat,
> double (S x) y = S (S (double x y)).
>
>
> (* Yin *)
> Lemma even_ss :
> forall x y : nat,
> evenb (double x y) = evenb (double x (S (S y))).
>
>
>
> -- Yin
>
>
> On Sat, Apr 28, 2012 at 3:38 PM, Yin **** <> wrote:
> > That's a very nice lemma! How did you thought of it?
> >
> >
> > -- Yin
> >
> >
> > On Sat, Apr 28, 2012 at 3:24 PM, Rebecca Swords <>
> wrote:
> >> Hi Yin,
> >>
> >> How about this lemma?
> >>
> >> Lemma double_s : forall x y:nat, double (S x) y = S (S (double x y)).
> >>
> >> The proof for this one is just by induction on x, and then for the main
> >> theorem, you basically have induction on x, with one rewrite. Both
> proofs
> >> are short and straightforward. Perhaps this is what you were looking
> >> for? Here are my proofs:
> >>
> >> Lemma double_s : forall x y:nat, double (S x) y = S (S (double x y)).
> >> Proof.
> >> intros x.
> >> induction x.
> >> reflexivity.
> >>
> >> intros y.
> >> simpl.
> >> apply IHx.
> >> Qed.
> >>
> >> Theorem even_double : forall x:nat, evenb (double x 0) = true.
> >> Proof.
> >> induction x.
> >> reflexivity.
> >>
> >> rewrite double_s.
> >> simpl.
> >> apply IHx.
> >> Qed.
> >>
> >>
> >> -Rebecca
> >>
> >>
> >> On Sat, Apr 28, 2012 at 1:45 PM, Yin **** <> wrote:
> >>>
> >>> I had been trying not to use anything fancy (like auto), but I would
> >>> try ';'. I guess I can think of it as a join point for branches? Thank
> >>> you.
> >>>
> >>>
> >>> -- Yin
> >>>
> >>>
> >>> On Sat, Apr 28, 2012 at 1:35 PM, James T. Perconti <
> >
> >>> wrote:
> >>> > I just proved it with
> >>> > induction x; intros; simpl; auto.
> >>> > Perhaps you have not learned about ; yet? It applies a tactic to all
> >>> > subgoals generated by its left-hand side.
> >>> > --Jamie
> >>> >
> >>> > ----- Original Message -----
> >>> > From: "Yin ****" <>
> >>> > To: "IUCS Programming Languages"
> >>> > Sent: Saturday, April 28, 2012 1:24:44 PM GMT -05:00 US/Canada
> Eastern
> >>> > Subject: Re: [pl-wonks] soliciting proofs for a trivial theorem
> >>> >
> >>> > Thank you James. The lemma works.
> >>> >
> >>> > I'm not sure if I got the optimal sequence of tactics though. I had
> to
> >>> > induct on x first, then to 'intros' twice at two branches. Otherwise
> >>> > the induction hypothesis will not be universally quantified. I would
> >>> > appreciate a neater way to deal with this.
> >>> >
> >>> > Here is my little ugly proof of the lemma:
> >>> >
> >>> > Lemma even_y : forall x y : nat,
> >>> > evenb y = true -> evenb (double x y) = true.
> >>> >
> >>> > Proof.
> >>> > induction x.
> >>> > intros.
> >>> > simpl.
> >>> > apply H.
> >>> > intros.
> >>> > simpl.
> >>> > apply IHx.
> >>> > simpl.
> >>> > apply H.
> >>> > Qed.
> >>> >
> >>> > The theorem is trivially proved using this lemma:
> >>> >
> >>> > Theorem even_double : forall x:nat,
> >>> > evenb (double x 0) = true.
> >>> > Proof.
> >>> > intros.
> >>> > apply even_y.
> >>> > reflexivity.
> >>> > Qed.
> >>> >
> >>> >
> >>> > I also found another lemma that works:
> >>> >
> >>> > Lemma even_ss : forall x y : nat,
> >>> > evenb (double x y) = evenb (double x (S (S y))).
> >>> >
> >>> > It makes the proof of the theorem a little longer though:
> >>> >
> >>> > Theorem even_double : forall x:nat,
> >>> > evenb (double x 0) = true.
> >>> > Proof.
> >>> > Restart.
> >>> > intros.
> >>> > induction x.
> >>> > reflexivity.
> >>> > simpl.
> >>> > rewrite <- even_ss.
> >>> > apply IHx.
> >>> > Qed.
> >>> >
> >>> >
> >>> > I'll appreciate any other tricks. Thank you.
> >>> >
> >>> >
> >>> > -- Yin
> >>> >
> >>> >
> >>> > On Sat, Apr 28, 2012 at 12:25 PM, James T. Perconti
> >>> > <> wrote:
> >>> >> Yin,
> >>> >> The lemma you want is the generalization of your theorem over the
> >>> >> value of the accumulator:
> >>> >>
> >>> >> Lemma even_double : forall x n,
> >>> >> evenb n = true -> evenb (double x n) = true.
> >>> >>
> >>> >> Proving this is now a simple induction on x, and specializing n to 0
> >>> >> afterward is of course trivial.
> >>> >> I'm not sure what other lemma(s) one might choose instead of this;
> >>> >> maybe that double x n = (double x 0) + n and then that the sum of
> even nats
> >>> >> is even? But the first thing is much simpler.
> >>> >> --Jamie
> >>> >>
> >>> >> ----- Original Message -----
> >>> >> From: "Yin ****" <>
> >>> >> To: "IUCS Programming Languages"
> >>> >> Sent: Saturday, April 28, 2012 12:07:47 PM GMT -05:00 US/Canada
> Eastern
> >>> >> Subject: [pl-wonks] soliciting proofs for a trivial theorem
> >>> >>
> >>> >> Hello,
> >>> >>
> >>> >> I'm wondering what's the best way to prove this seemingly trivial
> >>> >> theorem (in Coq):
> >>> >>
> >>> >> Theorem even_double : forall x:nat,
> >>> >> evenb (double x 0) = true.
> >>> >>
> >>> >> The other definitions are:
> >>> >>
> >>> >> Fixpoint evenb (n:nat) : bool :=
> >>> >> match n with
> >>> >> | O => true
> >>> >> | S O => false
> >>> >> | S (S n') => evenb n'
> >>> >> end.
> >>> >>
> >>> >> Fixpoint double (x y : nat) : nat :=
> >>> >> match x with
> >>> >> | O => y
> >>> >> | S x' => double x' (S (S y))
> >>> >> end.
> >>> >>
> >>> >> Everything seems to be straightforward. The only twist is that
> double
> >>> >> has an accumulator. This is the first theorem in my learning process
> >>> >> where I found that I definitely needed a lemma. The question is,
> which
> >>> >> lemma is the best one to use?
> >>> >>
> >>> >>
> >>> >> -- Yin
> >>> >> _______________________________________________
> >>> >> PL-wonks mailing list
> >>> >> PL-
> >>> >> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
> >>> >> _______________________________________________
> >>> >> PL-wonks mailing list
> >>> >> PL-
> >>> >> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
> >>> >
> >>> > _______________________________________________
> >>> > PL-wonks mailing list
> >>> > PL-
> >>> > http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
> >>> >
> >>> > _______________________________________________
> >>> > PL-wonks mailing list
> >>> > PL-
> >>> > http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
> >>>
> >>> _______________________________________________
> >>> PL-wonks mailing list
> >>> PL-
> >>> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
> >>
> >>
> >>
> >> _______________________________________________
> >> PL-wonks mailing list
> >> PL-
> >> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
> >>
>
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>


That's an amazing analysis!

Indeed they seem to be in that order Rebecca >= Yin >= Jamie, where
Rebecca > Yin seems to be strict. I'm wondering whether Yin > Jamie is
strict. Although Jamie's lemma only talks about the case when y is
even, but evenb y = true -> evenb (double x y) = true seems also
"implicitly" talks about the case when evenb y = false.

If I change my lemma to this:

Lemma even_ss_b :
forall x y : nat,
evenb (double x y) = true -> evenb (double x (S (S y))) = true.

It talks about the same thing, although now 'true' appears explicitly.


The reason I hope to find the weakest lemma and get your train of
thoughts is because I'm wondering how a computer can prove this
theorem without any help. A strong lemma like yours takes experience
and insights to find, but a computer is too naive. So stronger lemmas
will be harder for it to see. Also it could be easy for a computer to
find a "lemma" that's impossible to prove if it doesn't use the
weakest one at hand. But maybe a leap is necessary for harder
theorems.

Also it seems that you are implicitly doing a CPS transformation in
your head and have moved those two S's toward the continuation which
goes toward evenb. Maybe we can capture that kind of continuation in a
automatic prover :-)



-- Yin



On Sat, Apr 28, 2012 at 6:14 PM, Rebecca Swords <> wrote:
> Hi Yin,
>
> Here are some of the things I was thinking about when I came up with the
> lemma. I was looking for a way to take advantage of the structure of even
> numbers in the definition of evenb. To do that, I had to have to have S (S
> something). I also thought it would be better to say something about how the
> final result of double changes, rather than how y changes.
>
> And in the inductive proof of even_double, the proof goal was to show that
> (double (S x) 0) is even, so this lemma gives you a statement about doubling
> the successor of a number.
>
> For your question about comparing these lemmas, I'm not sure how to decide
> whether one is stronger or weaker than another, but I think Jamie's is most
> closely fitted to the original theorem. His lemma is only applicable when y
> is even (which is the only case that matters for even_double), and it makes
> almost the same statement as the original theorem.
>
> With transitivity, yours is a statement about both even and odd values for
> y. It says that for a given x, (double x y) for even values of y is either
> always even or always odd, and similarly for odd values of y. Since yours
> applies to both even and odd y values, I think it's probably more widely
> applicable than Jamie's.
>
> Mine doesn't say anything about evenness, oddness, or y; it's a statement
> relating the results of applying double to different values of x for a given
> y. I think it's probably the most general of the three lemmas. (You can
> easily use it to prove the stronger theorem that double is semantically
> correct, i.e., (double x 0) = x * 2.)
>
> My question is, why do you want the weakest lemma? It seems like once you
> start proving things, you might have several theorems to prove about
> different aspects of your system and how its components are related. If you
> use more general lemmas, it seems like they would be more likely to be
> reusable in different places.
>
> -Rebecca
>
> On Sat, Apr 28, 2012 at 4:02 PM, Yin **** <> wrote:
>>
>> Thanks for the responses :-) Now I'm surprised that we have three
>> lemmas that all work! (still welcoming more of them).
>>
>> Now my questions is, which lemma is the weakest, say we hope to find a
>> lemma that tells us nothing more than proving the theorem?
>>
>>
>> (* James *)
>> Lemma even_y :
>>  forall x y : nat,
>>    evenb y = true -> evenb (double x y) = true.
>>
>>
>> (* Rebecca *)
>> Lemma double_s :
>>  forall x y : nat,
>>    double (S x) y = S (S (double x y)).
>>
>>
>> (* Yin *)
>> Lemma even_ss :
>>  forall x y : nat,
>>    evenb (double x y) = evenb (double x (S (S y))).
>>
>>
>>
>> -- Yin
>>
>>
>> On Sat, Apr 28, 2012 at 3:38 PM, Yin **** <> wrote:
>> > That's a very nice lemma! How did you thought of it?
>> >
>> >
>> > -- Yin
>> >
>> >
>> > On Sat, Apr 28, 2012 at 3:24 PM, Rebecca Swords <>
>> > wrote:
>> >> Hi Yin,
>> >>
>> >> How about this lemma?
>> >>
>> >> Lemma double_s : forall x y:nat, double (S x) y = S (S (double x y)).
>> >>
>> >> The proof for this one is just by induction on x, and then for the main
>> >> theorem, you basically have induction on x, with one rewrite. Both
>> >> proofs
>> >> are short and straightforward. Perhaps this is what you were looking
>> >> for? Here are my proofs:
>> >>
>> >> Lemma double_s : forall x y:nat, double (S x) y = S (S (double x y)).
>> >> Proof.
>> >>   intros x.
>> >>   induction x.
>> >>   reflexivity.
>> >>
>> >>   intros y.
>> >>   simpl.
>> >>   apply IHx.
>> >> Qed.
>> >>
>> >> Theorem even_double : forall x:nat, evenb (double x 0) = true.
>> >> Proof.
>> >>   induction x.
>> >>   reflexivity.
>> >>
>> >>   rewrite double_s.
>> >>   simpl.
>> >>   apply IHx.
>> >> Qed.
>> >>
>> >>
>> >> -Rebecca
>> >>
>> >>
>> >> On Sat, Apr 28, 2012 at 1:45 PM, Yin **** <> wrote:
>> >>>
>> >>> I had been trying not to use anything fancy (like auto), but I would
>> >>> try ';'. I guess I can think of it as a join point for branches? Thank
>> >>> you.
>> >>>
>> >>>
>> >>> -- Yin
>> >>>
>> >>>
>> >>> On Sat, Apr 28, 2012 at 1:35 PM, James T. Perconti
>> >>> <>
>> >>> wrote:
>> >>> > I just proved it with
>> >>> >   induction x; intros; simpl; auto.
>> >>> > Perhaps you have not learned about ; yet?  It applies a tactic to
>> >>> > all
>> >>> > subgoals generated by its left-hand side.
>> >>> >  --Jamie
>> >>> >
>> >>> > ----- Original Message -----
>> >>> > From: "Yin ****" <>
>> >>> > To: "IUCS Programming Languages"
>> >>> > Sent: Saturday, April 28, 2012 1:24:44 PM GMT -05:00 US/Canada
>> >>> > Eastern
>> >>> > Subject: Re: [pl-wonks] soliciting proofs for a trivial theorem
>> >>> >
>> >>> > Thank you James. The lemma works.
>> >>> >
>> >>> > I'm not sure if I got the optimal sequence of tactics though. I had
>> >>> > to
>> >>> > induct on x first, then to 'intros' twice at two branches. Otherwise
>> >>> > the induction hypothesis will not be universally quantified. I would
>> >>> > appreciate a neater way to deal with this.
>> >>> >
>> >>> > Here is my little ugly proof of the lemma:
>> >>> >
>> >>> > Lemma even_y : forall x y : nat,
>> >>> >  evenb y = true -> evenb (double x y) = true.
>> >>> >
>> >>> > Proof.
>> >>> >  induction x.
>> >>> >  intros.
>> >>> >  simpl.
>> >>> >  apply H.
>> >>> >  intros.
>> >>> >  simpl.
>> >>> >  apply IHx.
>> >>> >  simpl.
>> >>> >  apply H.
>> >>> > Qed.
>> >>> >
>> >>> > The theorem is trivially proved using this lemma:
>> >>> >
>> >>> > Theorem even_double : forall x:nat,
>> >>> >  evenb (double x 0) = true.
>> >>> > Proof.
>> >>> >  intros.
>> >>> >  apply even_y.
>> >>> >  reflexivity.
>> >>> > Qed.
>> >>> >
>> >>> >
>> >>> > I also found another lemma that works:
>> >>> >
>> >>> > Lemma even_ss : forall x y : nat,
>> >>> >  evenb (double x y) = evenb (double x (S (S y))).
>> >>> >
>> >>> > It makes the proof of the theorem a little longer though:
>> >>> >
>> >>> > Theorem even_double : forall x:nat,
>> >>> >  evenb (double x 0) = true.
>> >>> > Proof.
>> >>> >  Restart.
>> >>> >  intros.
>> >>> >  induction x.
>> >>> >  reflexivity.
>> >>> >  simpl.
>> >>> >  rewrite <- even_ss.
>> >>> >  apply IHx.
>> >>> > Qed.
>> >>> >
>> >>> >
>> >>> > I'll appreciate any other tricks. Thank you.
>> >>> >
>> >>> >
>> >>> > -- Yin
>> >>> >
>> >>> >
>> >>> > On Sat, Apr 28, 2012 at 12:25 PM, James T. Perconti
>> >>> > <> wrote:
>> >>> >> Yin,
>> >>> >>  The lemma you want is the generalization of your theorem over the
>> >>> >> value of the accumulator:
>> >>> >>
>> >>> >> Lemma even_double : forall x n,
>> >>> >>  evenb n = true -> evenb (double x n) = true.
>> >>> >>
>> >>> >> Proving this is now a simple induction on x, and specializing n to
>> >>> >> 0
>> >>> >> afterward is of course trivial.
>> >>> >>  I'm not sure what other lemma(s) one might choose instead of this;
>> >>> >> maybe that double x n = (double x 0) + n and then that the sum of
>> >>> >> even nats
>> >>> >> is even?  But the first thing is much simpler.
>> >>> >>  --Jamie
>> >>> >>
>> >>> >> ----- Original Message -----
>> >>> >> From: "Yin ****" <>
>> >>> >> To: "IUCS Programming Languages"
>> >>> >> Sent: Saturday, April 28, 2012 12:07:47 PM GMT -05:00 US/Canada
>> >>> >> Eastern
>> >>> >> Subject: [pl-wonks] soliciting proofs for a trivial theorem
>> >>> >>
>> >>> >> Hello,
>> >>> >>
>> >>> >> I'm wondering what's the best way to prove this seemingly trivial
>> >>> >> theorem (in Coq):
>> >>> >>
>> >>> >> Theorem even_double : forall x:nat,
>> >>> >>  evenb (double x 0) = true.
>> >>> >>
>> >>> >> The other definitions are:
>> >>> >>
>> >>> >> Fixpoint evenb (n:nat) : bool :=
>> >>> >>  match n with
>> >>> >>    | O => true
>> >>> >>    | S O => false
>> >>> >>    | S (S n') => evenb n'
>> >>> >>  end.
>> >>> >>
>> >>> >> Fixpoint double (x y : nat) : nat :=
>> >>> >>  match x with
>> >>> >>    | O => y
>> >>> >>    | S x' => double x' (S (S y))
>> >>> >>  end.
>> >>> >>
>> >>> >> Everything seems to be straightforward. The only twist is that
>> >>> >> double
>> >>> >> has an accumulator. This is the first theorem in my learning
>> >>> >> process
>> >>> >> where I found that I definitely needed a lemma. The question is,
>> >>> >> which
>> >>> >> lemma is the best one to use?
>> >>> >>
>> >>> >>
>> >>> >> -- Yin
>> >>> >> _______________________________________________
>> >>> >> PL-wonks mailing list
>> >>> >> PL-
>> >>> >> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>> >>> >> _______________________________________________
>> >>> >> PL-wonks mailing list
>> >>> >> PL-
>> >>> >> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>> >>> >
>> >>> > _______________________________________________
>> >>> > PL-wonks mailing list
>> >>> > PL-
>> >>> > http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>> >>> >
>> >>> > _______________________________________________
>> >>> > PL-wonks mailing list
>> >>> > PL-
>> >>> > http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>> >>>
>> >>> _______________________________________________
>> >>> PL-wonks mailing list
>> >>> PL-
>> >>> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>> >>
>> >>
>> >>
>> >> _______________________________________________
>> >> PL-wonks mailing list
>> >> PL-
>> >> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>> >>
>>
>> _______________________________________________
>> PL-wonks mailing list
>> PL-
>> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>
>
>
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>

_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

Hello,

I'm wondering what's the best way to prove this seemingly trivial
theorem (in Coq):

Theorem even_double : forall x:nat,
evenb (double x 0) = true.

The other definitions are:

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

Fixpoint double (x y : nat) : nat :=
match x with
| O => y
| S x' => double x' (S (S y))
end.

Everything seems to be straightforward. The only twist is that double
has an accumulator. This is the first theorem in my learning process
where I found that I definitely needed a lemma. The question is, which
lemma is the best one to use?


-- Yin
_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
)
Yin,
The lemma you want is the generalization of your theorem over the value of the accumulator:

Lemma even_double : forall x n,
evenb n = true -> evenb (double x n) = true.

Proving this is now a simple induction on x, and specializing n to 0 afterward is of course trivial.
I'm not sure what other lemma(s) one might choose instead of this; maybe that double x n = (double x 0) + n and then that the sum of even nats is even? But the first thing is much simpler.
--Jamie

----- Original Message -----
From: "Yin ****" <>
To: "IUCS Programming Languages"
Sent: Saturday, April 28, 2012 12:07:47 PM GMT -05:00 US/Canada Eastern
Subject: [pl-wonks] soliciting proofs for a trivial theorem

Hello,

I'm wondering what's the best way to prove this seemingly trivial
theorem (in Coq):

Theorem even_double : forall x:nat,
evenb (double x 0) = true.

The other definitions are:

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

Fixpoint double (x y : nat) : nat :=
match x with
| O => y
| S x' => double x' (S (S y))
end.

Everything seems to be straightforward. The only twist is that double
has an accumulator. This is the first theorem in my learning process
where I found that I definitely needed a lemma. The question is, which
lemma is the best one to use?


-- Yin
_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
)
Thank you James. The lemma works.

I'm not sure if I got the optimal sequence of tactics though. I had to
induct on x first, then to 'intros' twice at two branches. Otherwise
the induction hypothesis will not be universally quantified. I would
appreciate a neater way to deal with this.

Here is my little ugly proof of the lemma:

Lemma even_y : forall x y : nat,
evenb y = true -> evenb (double x y) = true.

Proof.
induction x.
intros.
simpl.
apply H.
intros.
simpl.
apply IHx.
simpl.
apply H.
Qed.

The theorem is trivially proved using this lemma:

Theorem even_double : forall x:nat,
evenb (double x 0) = true.
Proof.
intros.
apply even_y.
reflexivity.
Qed.


I also found another lemma that works:

Lemma even_ss : forall x y : nat,
evenb (double x y) = evenb (double x (S (S y))).

It makes the proof of the theorem a little longer though:

Theorem even_double : forall x:nat,
evenb (double x 0) = true.
Proof.
Restart.
intros.
induction x.
reflexivity.
simpl.
rewrite <- even_ss.
apply IHx.
Qed.


I'll appreciate any other tricks. Thank you.


-- Yin


On Sat, Apr 28, 2012 at 12:25 PM, James T. Perconti
<> wrote:
> Yin,
>  The lemma you want is the generalization of your theorem over the value of the accumulator:
>
> Lemma even_double : forall x n,
>  evenb n = true -> evenb (double x n) = true.
>
> Proving this is now a simple induction on x, and specializing n to 0 afterward is of course trivial.
>  I'm not sure what other lemma(s) one might choose instead of this; maybe that double x n = (double x 0) + n and then that the sum of even nats is even?  But the first thing is much simpler.
>  --Jamie
>
> ----- Original Message -----
> From: "Yin ****" <>
> To: "IUCS Programming Languages"
> Sent: Saturday, April 28, 2012 12:07:47 PM GMT -05:00 US/Canada Eastern
> Subject: [pl-wonks] soliciting proofs for a trivial theorem
>
> Hello,
>
> I'm wondering what's the best way to prove this seemingly trivial
> theorem (in Coq):
>
> Theorem even_double : forall x:nat,
>  evenb (double x 0) = true.
>
> The other definitions are:
>
> Fixpoint evenb (n:nat) : bool :=
>  match n with
>    | O => true
>    | S O => false
>    | S (S n') => evenb n'
>  end.
>
> Fixpoint double (x y : nat) : nat :=
>  match x with
>    | O => y
>    | S x' => double x' (S (S y))
>  end.
>
> Everything seems to be straightforward. The only twist is that double
> has an accumulator. This is the first theorem in my learning process
> where I found that I definitely needed a lemma. The question is, which
> lemma is the best one to use?
>
>
> -- Yin
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

I just proved it with
induction x; intros; simpl; auto.
Perhaps you have not learned about ; yet? It applies a tactic to all subgoals generated by its left-hand side.
--Jamie

----- Original Message -----
From: "Yin ****" <>
To: "IUCS Programming Languages"
Sent: Saturday, April 28, 2012 1:24:44 PM GMT -05:00 US/Canada Eastern
Subject: Re: [pl-wonks] soliciting proofs for a trivial theorem

Thank you James. The lemma works.

I'm not sure if I got the optimal sequence of tactics though. I had to
induct on x first, then to 'intros' twice at two branches. Otherwise
the induction hypothesis will not be universally quantified. I would
appreciate a neater way to deal with this.

Here is my little ugly proof of the lemma:

Lemma even_y : forall x y : nat,
evenb y = true -> evenb (double x y) = true.

Proof.
induction x.
intros.
simpl.
apply H.
intros.
simpl.
apply IHx.
simpl.
apply H.
Qed.

The theorem is trivially proved using this lemma:

Theorem even_double : forall x:nat,
evenb (double x 0) = true.
Proof.
intros.
apply even_y.
reflexivity.
Qed.


I also found another lemma that works:

Lemma even_ss : forall x y : nat,
evenb (double x y) = evenb (double x (S (S y))).

It makes the proof of the theorem a little longer though:

Theorem even_double : forall x:nat,
evenb (double x 0) = true.
Proof.
Restart.
intros.
induction x.
reflexivity.
simpl.
rewrite <- even_ss.
apply IHx.
Qed.


I'll appreciate any other tricks. Thank you.


-- Yin


On Sat, Apr 28, 2012 at 12:25 PM, James T. Perconti
<> wrote:
> Yin,
>  The lemma you want is the generalization of your theorem over the value of the accumulator:
>
> Lemma even_double : forall x n,
>  evenb n = true -> evenb (double x n) = true.
>
> Proving this is now a simple induction on x, and specializing n to 0 afterward is of course trivial.
>  I'm not sure what other lemma(s) one might choose instead of this; maybe that double x n = (double x 0) + n and then that the sum of even nats is even?  But the first thing is much simpler.
>  --Jamie
>
> ----- Original Message -----
> From: "Yin ****" <>
> To: "IUCS Programming Languages"
> Sent: Saturday, April 28, 2012 12:07:47 PM GMT -05:00 US/Canada Eastern
> Subject: [pl-wonks] soliciting proofs for a trivial theorem
>
> Hello,
>
> I'm wondering what's the best way to prove this seemingly trivial
> theorem (in Coq):
>
> Theorem even_double : forall x:nat,
>  evenb (double x 0) = true.
>
> The other definitions are:
>
> Fixpoint evenb (n:nat) : bool :=
>  match n with
>    | O => true
>    | S O => false
>    | S (S n') => evenb n'
>  end.
>
> Fixpoint double (x y : nat) : nat :=
>  match x with
>    | O => y
>    | S x' => double x' (S (S y))
>  end.
>
> Everything seems to be straightforward. The only twist is that double
> has an accumulator. This is the first theorem in my learning process
> where I found that I definitely needed a lemma. The question is, which
> lemma is the best one to use?
>
>
> -- Yin
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

I had been trying not to use anything fancy (like auto), but I would
try ';'. I guess I can think of it as a join point for branches? Thank
you.


-- Yin


On Sat, Apr 28, 2012 at 1:35 PM, James T. Perconti <> wrote:
> I just proved it with
>   induction x; intros; simpl; auto.
> Perhaps you have not learned about ; yet?  It applies a tactic to all subgoals generated by its left-hand side.
>  --Jamie
>
> ----- Original Message -----
> From: "Yin ****" <>
> To: "IUCS Programming Languages"
> Sent: Saturday, April 28, 2012 1:24:44 PM GMT -05:00 US/Canada Eastern
> Subject: Re: [pl-wonks] soliciting proofs for a trivial theorem
>
> Thank you James. The lemma works.
>
> I'm not sure if I got the optimal sequence of tactics though. I had to
> induct on x first, then to 'intros' twice at two branches. Otherwise
> the induction hypothesis will not be universally quantified. I would
> appreciate a neater way to deal with this.
>
> Here is my little ugly proof of the lemma:
>
> Lemma even_y : forall x y : nat,
>  evenb y = true -> evenb (double x y) = true.
>
> Proof.
>  induction x.
>  intros.
>  simpl.
>  apply H.
>  intros.
>  simpl.
>  apply IHx.
>  simpl.
>  apply H.
> Qed.
>
> The theorem is trivially proved using this lemma:
>
> Theorem even_double : forall x:nat,
>  evenb (double x 0) = true.
> Proof.
>  intros.
>  apply even_y.
>  reflexivity.
> Qed.
>
>
> I also found another lemma that works:
>
> Lemma even_ss : forall x y : nat,
>  evenb (double x y) = evenb (double x (S (S y))).
>
> It makes the proof of the theorem a little longer though:
>
> Theorem even_double : forall x:nat,
>  evenb (double x 0) = true.
> Proof.
>  Restart.
>  intros.
>  induction x.
>  reflexivity.
>  simpl.
>  rewrite <- even_ss.
>  apply IHx.
> Qed.
>
>
> I'll appreciate any other tricks. Thank you.
>
>
> -- Yin
>
>
> On Sat, Apr 28, 2012 at 12:25 PM, James T. Perconti
> <> wrote:
>> Yin,
>>  The lemma you want is the generalization of your theorem over the value of the accumulator:
>>
>> Lemma even_double : forall x n,
>>  evenb n = true -> evenb (double x n) = true.
>>
>> Proving this is now a simple induction on x, and specializing n to 0 afterward is of course trivial.
>>  I'm not sure what other lemma(s) one might choose instead of this; maybe that double x n = (double x 0) + n and then that the sum of even nats is even?  But the first thing is much simpler.
>>  --Jamie
>>
>> ----- Original Message -----
>> From: "Yin ****" <>
>> To: "IUCS Programming Languages"
>> Sent: Saturday, April 28, 2012 12:07:47 PM GMT -05:00 US/Canada Eastern
>> Subject: [pl-wonks] soliciting proofs for a trivial theorem
>>
>> Hello,
>>
>> I'm wondering what's the best way to prove this seemingly trivial
>> theorem (in Coq):
>>
>> Theorem even_double : forall x:nat,
>>  evenb (double x 0) = true.
>>
>> The other definitions are:
>>
>> Fixpoint evenb (n:nat) : bool :=
>>  match n with
>>    | O => true
>>    | S O => false
>>    | S (S n') => evenb n'
>>  end.
>>
>> Fixpoint double (x y : nat) : nat :=
>>  match x with
>>    | O => y
>>    | S x' => double x' (S (S y))
>>  end.
>>
>> Everything seems to be straightforward. The only twist is that double
>> has an accumulator. This is the first theorem in my learning process
>> where I found that I definitely needed a lemma. The question is, which
>> lemma is the best one to use?
>>
>>
>> -- Yin
>> _______________________________________________
>> PL-wonks mailing list
>> PL-
>> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>> _______________________________________________
>> PL-wonks mailing list
>> PL-
>> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

Hi Yin,

How about this lemma?

Lemma double_s : forall x y:nat, double (S x) y = S (S (double x y)).

The proof for this one is just by induction on x, and then for the main
theorem, you basically have induction on x, with one rewrite. Both proofs
are short and straightforward. Perhaps this is what you were looking
for? Here are my proofs:

Lemma double_s : forall x y:nat, double (S x) y = S (S (double x y)).
Proof.
intros x.
induction x.
reflexivity.

intros y.
simpl.
apply IHx.
Qed.

Theorem even_double : forall x:nat, evenb (double x 0) = true.
Proof.
induction x.
reflexivity.

rewrite double_s.
simpl.
apply IHx.
Qed.


-Rebecca


On Sat, Apr 28, 2012 at 1:45 PM, Yin **** <> wrote:

> I had been trying not to use anything fancy (like auto), but I would
> try ';'. I guess I can think of it as a join point for branches? Thank
> you.
>
>
> -- Yin
>
>
> On Sat, Apr 28, 2012 at 1:35 PM, James T. Perconti <>
> wrote:
> > I just proved it with
> > induction x; intros; simpl; auto.
> > Perhaps you have not learned about ; yet? It applies a tactic to all
> subgoals generated by its left-hand side.
> > --Jamie
> >
> > ----- Original Message -----
> > From: "Yin ****" <>
> > To: "IUCS Programming Languages"
> > Sent: Saturday, April 28, 2012 1:24:44 PM GMT -05:00 US/Canada Eastern
> > Subject: Re: [pl-wonks] soliciting proofs for a trivial theorem
> >
> > Thank you James. The lemma works.
> >
> > I'm not sure if I got the optimal sequence of tactics though. I had to
> > induct on x first, then to 'intros' twice at two branches. Otherwise
> > the induction hypothesis will not be universally quantified. I would
> > appreciate a neater way to deal with this.
> >
> > Here is my little ugly proof of the lemma:
> >
> > Lemma even_y : forall x y : nat,
> > evenb y = true -> evenb (double x y) = true.
> >
> > Proof.
> > induction x.
> > intros.
> > simpl.
> > apply H.
> > intros.
> > simpl.
> > apply IHx.
> > simpl.
> > apply H.
> > Qed.
> >
> > The theorem is trivially proved using this lemma:
> >
> > Theorem even_double : forall x:nat,
> > evenb (double x 0) = true.
> > Proof.
> > intros.
> > apply even_y.
> > reflexivity.
> > Qed.
> >
> >
> > I also found another lemma that works:
> >
> > Lemma even_ss : forall x y : nat,
> > evenb (double x y) = evenb (double x (S (S y))).
> >
> > It makes the proof of the theorem a little longer though:
> >
> > Theorem even_double : forall x:nat,
> > evenb (double x 0) = true.
> > Proof.
> > Restart.
> > intros.
> > induction x.
> > reflexivity.
> > simpl.
> > rewrite <- even_ss.
> > apply IHx.
> > Qed.
> >
> >
> > I'll appreciate any other tricks. Thank you.
> >
> >
> > -- Yin
> >
> >
> > On Sat, Apr 28, 2012 at 12:25 PM, James T. Perconti
> > <> wrote:
> >> Yin,
> >> The lemma you want is the generalization of your theorem over the
> value of the accumulator:
> >>
> >> Lemma even_double : forall x n,
> >> evenb n = true -> evenb (double x n) = true.
> >>
> >> Proving this is now a simple induction on x, and specializing n to 0
> afterward is of course trivial.
> >> I'm not sure what other lemma(s) one might choose instead of this;
> maybe that double x n = (double x 0) + n and then that the sum of even nats
> is even? But the first thing is much simpler.
> >> --Jamie
> >>
> >> ----- Original Message -----
> >> From: "Yin ****" <>
> >> To: "IUCS Programming Languages"
> >> Sent: Saturday, April 28, 2012 12:07:47 PM GMT -05:00 US/Canada Eastern
> >> Subject: [pl-wonks] soliciting proofs for a trivial theorem
> >>
> >> Hello,
> >>
> >> I'm wondering what's the best way to prove this seemingly trivial
> >> theorem (in Coq):
> >>
> >> Theorem even_double : forall x:nat,
> >> evenb (double x 0) = true.
> >>
> >> The other definitions are:
> >>
> >> Fixpoint evenb (n:nat) : bool :=
> >> match n with
> >> | O => true
> >> | S O => false
> >> | S (S n') => evenb n'
> >> end.
> >>
> >> Fixpoint double (x y : nat) : nat :=
> >> match x with
> >> | O => y
> >> | S x' => double x' (S (S y))
> >> end.
> >>
> >> Everything seems to be straightforward. The only twist is that double
> >> has an accumulator. This is the first theorem in my learning process
> >> where I found that I definitely needed a lemma. The question is, which
> >> lemma is the best one to use?
> >>
> >>
> >> -- Yin
> >> _______________________________________________
> >> PL-wonks mailing list
> >> PL-
> >> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
> >> _______________________________________________
> >> PL-wonks mailing list
> >> PL-
> >> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
> >
> > _______________________________________________
> > PL-wonks mailing list
> > PL-
> > http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
> >
> > _______________________________________________
> > PL-wonks mailing list
> > PL-
> > http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>


That's a very nice lemma! How did you thought of it?


-- Yin


On Sat, Apr 28, 2012 at 3:24 PM, Rebecca Swords <> wrote:
> Hi Yin,
>
> How about this lemma?
>
> Lemma double_s : forall x y:nat, double (S x) y = S (S (double x y)).
>
> The proof for this one is just by induction on x, and then for the main
> theorem, you basically have induction on x, with one rewrite. Both proofs
> are short and straightforward. Perhaps this is what you were looking
> for? Here are my proofs:
>
> Lemma double_s : forall x y:nat, double (S x) y = S (S (double x y)).
> Proof.
>   intros x.
>   induction x.
>   reflexivity.
>
>   intros y.
>   simpl.
>   apply IHx.
> Qed.
>
> Theorem even_double : forall x:nat, evenb (double x 0) = true.
> Proof.
>   induction x.
>   reflexivity.
>
>   rewrite double_s.
>   simpl.
>   apply IHx.
> Qed.
>
>
> -Rebecca
>
>
> On Sat, Apr 28, 2012 at 1:45 PM, Yin **** <> wrote:
>>
>> I had been trying not to use anything fancy (like auto), but I would
>> try ';'. I guess I can think of it as a join point for branches? Thank
>> you.
>>
>>
>> -- Yin
>>
>>
>> On Sat, Apr 28, 2012 at 1:35 PM, James T. Perconti <>
>> wrote:
>> > I just proved it with
>> >   induction x; intros; simpl; auto.
>> > Perhaps you have not learned about ; yet?  It applies a tactic to all
>> > subgoals generated by its left-hand side.
>> >  --Jamie
>> >
>> > ----- Original Message -----
>> > From: "Yin ****" <>
>> > To: "IUCS Programming Languages"
>> > Sent: Saturday, April 28, 2012 1:24:44 PM GMT -05:00 US/Canada Eastern
>> > Subject: Re: [pl-wonks] soliciting proofs for a trivial theorem
>> >
>> > Thank you James. The lemma works.
>> >
>> > I'm not sure if I got the optimal sequence of tactics though. I had to
>> > induct on x first, then to 'intros' twice at two branches. Otherwise
>> > the induction hypothesis will not be universally quantified. I would
>> > appreciate a neater way to deal with this.
>> >
>> > Here is my little ugly proof of the lemma:
>> >
>> > Lemma even_y : forall x y : nat,
>> >  evenb y = true -> evenb (double x y) = true.
>> >
>> > Proof.
>> >  induction x.
>> >  intros.
>> >  simpl.
>> >  apply H.
>> >  intros.
>> >  simpl.
>> >  apply IHx.
>> >  simpl.
>> >  apply H.
>> > Qed.
>> >
>> > The theorem is trivially proved using this lemma:
>> >
>> > Theorem even_double : forall x:nat,
>> >  evenb (double x 0) = true.
>> > Proof.
>> >  intros.
>> >  apply even_y.
>> >  reflexivity.
>> > Qed.
>> >
>> >
>> > I also found another lemma that works:
>> >
>> > Lemma even_ss : forall x y : nat,
>> >  evenb (double x y) = evenb (double x (S (S y))).
>> >
>> > It makes the proof of the theorem a little longer though:
>> >
>> > Theorem even_double : forall x:nat,
>> >  evenb (double x 0) = true.
>> > Proof.
>> >  Restart.
>> >  intros.
>> >  induction x.
>> >  reflexivity.
>> >  simpl.
>> >  rewrite <- even_ss.
>> >  apply IHx.
>> > Qed.
>> >
>> >
>> > I'll appreciate any other tricks. Thank you.
>> >
>> >
>> > -- Yin
>> >
>> >
>> > On Sat, Apr 28, 2012 at 12:25 PM, James T. Perconti
>> > <> wrote:
>> >> Yin,
>> >>  The lemma you want is the generalization of your theorem over the
>> >> value of the accumulator:
>> >>
>> >> Lemma even_double : forall x n,
>> >>  evenb n = true -> evenb (double x n) = true.
>> >>
>> >> Proving this is now a simple induction on x, and specializing n to 0
>> >> afterward is of course trivial.
>> >>  I'm not sure what other lemma(s) one might choose instead of this;
>> >> maybe that double x n = (double x 0) + n and then that the sum of even nats
>> >> is even?  But the first thing is much simpler.
>> >>  --Jamie
>> >>
>> >> ----- Original Message -----
>> >> From: "Yin ****" <>
>> >> To: "IUCS Programming Languages"
>> >> Sent: Saturday, April 28, 2012 12:07:47 PM GMT -05:00 US/Canada Eastern
>> >> Subject: [pl-wonks] soliciting proofs for a trivial theorem
>> >>
>> >> Hello,
>> >>
>> >> I'm wondering what's the best way to prove this seemingly trivial
>> >> theorem (in Coq):
>> >>
>> >> Theorem even_double : forall x:nat,
>> >>  evenb (double x 0) = true.
>> >>
>> >> The other definitions are:
>> >>
>> >> Fixpoint evenb (n:nat) : bool :=
>> >>  match n with
>> >>    | O => true
>> >>    | S O => false
>> >>    | S (S n') => evenb n'
>> >>  end.
>> >>
>> >> Fixpoint double (x y : nat) : nat :=
>> >>  match x with
>> >>    | O => y
>> >>    | S x' => double x' (S (S y))
>> >>  end.
>> >>
>> >> Everything seems to be straightforward. The only twist is that double
>> >> has an accumulator. This is the first theorem in my learning process
>> >> where I found that I definitely needed a lemma. The question is, which
>> >> lemma is the best one to use?
>> >>
>> >>
>> >> -- Yin
>> >> _______________________________________________
>> >> PL-wonks mailing list
>> >> PL-
>> >> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>> >> _______________________________________________
>> >> PL-wonks mailing list
>> >> PL-
>> >> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>> >
>> > _______________________________________________
>> > PL-wonks mailing list
>> > PL-
>> > http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>> >
>> > _______________________________________________
>> > PL-wonks mailing list
>> > PL-
>> > http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>>
>> _______________________________________________
>> PL-wonks mailing list
>> PL-
>> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>
>
>
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>

_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

Thanks for the responses :-) Now I'm surprised that we have three
lemmas that all work! (still welcoming more of them).

Now my questions is, which lemma is the weakest, say we hope to find a
lemma that tells us nothing more than proving the theorem?


(* James *)
Lemma even_y :
forall x y : nat,
evenb y = true -> evenb (double x y) = true.


(* Rebecca *)
Lemma double_s :
forall x y : nat,
double (S x) y = S (S (double x y)).


(* Yin *)
Lemma even_ss :
forall x y : nat,
evenb (double x y) = evenb (double x (S (S y))).



-- Yin


On Sat, Apr 28, 2012 at 3:38 PM, Yin **** <> wrote:
> That's a very nice lemma! How did you thought of it?
>
>
> -- Yin
>
>
> On Sat, Apr 28, 2012 at 3:24 PM, Rebecca Swords <> wrote:
>> Hi Yin,
>>
>> How about this lemma?
>>
>> Lemma double_s : forall x y:nat, double (S x) y = S (S (double x y)).
>>
>> The proof for this one is just by induction on x, and then for the main
>> theorem, you basically have induction on x, with one rewrite. Both proofs
>> are short and straightforward. Perhaps this is what you were looking
>> for? Here are my proofs:
>>
>> Lemma double_s : forall x y:nat, double (S x) y = S (S (double x y)).
>> Proof.
>>   intros x.
>>   induction x.
>>   reflexivity.
>>
>>   intros y.
>>   simpl.
>>   apply IHx.
>> Qed.
>>
>> Theorem even_double : forall x:nat, evenb (double x 0) = true.
>> Proof.
>>   induction x.
>>   reflexivity.
>>
>>   rewrite double_s.
>>   simpl.
>>   apply IHx.
>> Qed.
>>
>>
>> -Rebecca
>>
>>
>> On Sat, Apr 28, 2012 at 1:45 PM, Yin **** <> wrote:
>>>
>>> I had been trying not to use anything fancy (like auto), but I would
>>> try ';'. I guess I can think of it as a join point for branches? Thank
>>> you.
>>>
>>>
>>> -- Yin
>>>
>>>
>>> On Sat, Apr 28, 2012 at 1:35 PM, James T. Perconti <>
>>> wrote:
>>> > I just proved it with
>>> >   induction x; intros; simpl; auto.
>>> > Perhaps you have not learned about ; yet?  It applies a tactic to all
>>> > subgoals generated by its left-hand side.
>>> >  --Jamie
>>> >
>>> > ----- Original Message -----
>>> > From: "Yin ****" <>
>>> > To: "IUCS Programming Languages"
>>> > Sent: Saturday, April 28, 2012 1:24:44 PM GMT -05:00 US/Canada Eastern
>>> > Subject: Re: [pl-wonks] soliciting proofs for a trivial theorem
>>> >
>>> > Thank you James. The lemma works.
>>> >
>>> > I'm not sure if I got the optimal sequence of tactics though. I had to
>>> > induct on x first, then to 'intros' twice at two branches. Otherwise
>>> > the induction hypothesis will not be universally quantified. I would
>>> > appreciate a neater way to deal with this.
>>> >
>>> > Here is my little ugly proof of the lemma:
>>> >
>>> > Lemma even_y : forall x y : nat,
>>> >  evenb y = true -> evenb (double x y) = true.
>>> >
>>> > Proof.
>>> >  induction x.
>>> >  intros.
>>> >  simpl.
>>> >  apply H.
>>> >  intros.
>>> >  simpl.
>>> >  apply IHx.
>>> >  simpl.
>>> >  apply H.
>>> > Qed.
>>> >
>>> > The theorem is trivially proved using this lemma:
>>> >
>>> > Theorem even_double : forall x:nat,
>>> >  evenb (double x 0) = true.
>>> > Proof.
>>> >  intros.
>>> >  apply even_y.
>>> >  reflexivity.
>>> > Qed.
>>> >
>>> >
>>> > I also found another lemma that works:
>>> >
>>> > Lemma even_ss : forall x y : nat,
>>> >  evenb (double x y) = evenb (double x (S (S y))).
>>> >
>>> > It makes the proof of the theorem a little longer though:
>>> >
>>> > Theorem even_double : forall x:nat,
>>> >  evenb (double x 0) = true.
>>> > Proof.
>>> >  Restart.
>>> >  intros.
>>> >  induction x.
>>> >  reflexivity.
>>> >  simpl.
>>> >  rewrite <- even_ss.
>>> >  apply IHx.
>>> > Qed.
>>> >
>>> >
>>> > I'll appreciate any other tricks. Thank you.
>>> >
>>> >
>>> > -- Yin
>>> >
>>> >
>>> > On Sat, Apr 28, 2012 at 12:25 PM, James T. Perconti
>>> > <> wrote:
>>> >> Yin,
>>> >>  The lemma you want is the generalization of your theorem over the
>>> >> value of the accumulator:
>>> >>
>>> >> Lemma even_double : forall x n,
>>> >>  evenb n = true -> evenb (double x n) = true.
>>> >>
>>> >> Proving this is now a simple induction on x, and specializing n to 0
>>> >> afterward is of course trivial.
>>> >>  I'm not sure what other lemma(s) one might choose instead of this;
>>> >> maybe that double x n = (double x 0) + n and then that the sum of even nats
>>> >> is even?  But the first thing is much simpler.
>>> >>  --Jamie
>>> >>
>>> >> ----- Original Message -----
>>> >> From: "Yin ****" <>
>>> >> To: "IUCS Programming Languages"
>>> >> Sent: Saturday, April 28, 2012 12:07:47 PM GMT -05:00 US/Canada Eastern
>>> >> Subject: [pl-wonks] soliciting proofs for a trivial theorem
>>> >>
>>> >> Hello,
>>> >>
>>> >> I'm wondering what's the best way to prove this seemingly trivial
>>> >> theorem (in Coq):
>>> >>
>>> >> Theorem even_double : forall x:nat,
>>> >>  evenb (double x 0) = true.
>>> >>
>>> >> The other definitions are:
>>> >>
>>> >> Fixpoint evenb (n:nat) : bool :=
>>> >>  match n with
>>> >>    | O => true
>>> >>    | S O => false
>>> >>    | S (S n') => evenb n'
>>> >>  end.
>>> >>
>>> >> Fixpoint double (x y : nat) : nat :=
>>> >>  match x with
>>> >>    | O => y
>>> >>    | S x' => double x' (S (S y))
>>> >>  end.
>>> >>
>>> >> Everything seems to be straightforward. The only twist is that double
>>> >> has an accumulator. This is the first theorem in my learning process
>>> >> where I found that I definitely needed a lemma. The question is, which
>>> >> lemma is the best one to use?
>>> >>
>>> >>
>>> >> -- Yin
>>> >> _______________________________________________
>>> >> PL-wonks mailing list
>>> >> PL-
>>> >> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>>> >> _______________________________________________
>>> >> PL-wonks mailing list
>>> >> PL-
>>> >> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>>> >
>>> > _______________________________________________
>>> > PL-wonks mailing list
>>> > PL-
>>> > http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>>> >
>>> > _______________________________________________
>>> > PL-wonks mailing list
>>> > PL-
>>> > http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>>>
>>> _______________________________________________
>>> PL-wonks mailing list
>>> PL-
>>> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>>
>>
>>
>> _______________________________________________
>> PL-wonks mailing list
>> PL-
>> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>>

_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

Hi Yin,

Here are some of the things I was thinking about when I came up with the
lemma. I was looking for a way to take advantage of the structure of even
numbers in the definition of evenb. To do that, I had to have to have S (S
something). I also thought it would be better to say something about how
the final result of double changes, rather than how y changes.

And in the inductive proof of even_double, the proof goal was to show that
(double (S x) 0) is even, so this lemma gives you a statement about
doubling the successor of a number.

For your question about comparing these lemmas, I'm not sure how to decide
whether one is stronger or weaker than another, but I think Jamie's is most
closely fitted to the original theorem. His lemma is only applicable when y
is even (which is the only case that matters for even_double), and it makes
almost the same statement as the original theorem.

With transitivity, yours is a statement about both even and odd values for
y. It says that for a given x, (double x y) for even values of y is either
always even or always odd, and similarly for odd values of y. Since yours
applies to both even and odd y values, I think it's probably more widely
applicable than Jamie's.

Mine doesn't say anything about evenness, oddness, or y; it's a statement
relating the results of applying double to different values of x for a
given y. I think it's probably the most general of the three lemmas. (You
can easily use it to prove the stronger theorem that double is semantically
correct, i.e., (double x 0) = x * 2.)

My question is, why do you want the weakest lemma? It seems like once you
start proving things, you might have several theorems to prove about
different aspects of your system and how its components are related. If you
use more general lemmas, it seems like they would be more likely to be
reusable in different places.

-Rebecca

On Sat, Apr 28, 2012 at 4:02 PM, Yin **** <> wrote:

> Thanks for the responses :-) Now I'm surprised that we have three
> lemmas that all work! (still welcoming more of them).
>
> Now my questions is, which lemma is the weakest, say we hope to find a
> lemma that tells us nothing more than proving the theorem?
>
>
> (* James *)
> Lemma even_y :
> forall x y : nat,
> evenb y = true -> evenb (double x y) = true.
>
>
> (* Rebecca *)
> Lemma double_s :
> forall x y : nat,
> double (S x) y = S (S (double x y)).
>
>
> (* Yin *)
> Lemma even_ss :
> forall x y : nat,
> evenb (double x y) = evenb (double x (S (S y))).
>
>
>
> -- Yin
>
>
> On Sat, Apr 28, 2012 at 3:38 PM, Yin **** <> wrote:
> > That's a very nice lemma! How did you thought of it?
> >
> >
> > -- Yin
> >
> >
> > On Sat, Apr 28, 2012 at 3:24 PM, Rebecca Swords <>
> wrote:
> >> Hi Yin,
> >>
> >> How about this lemma?
> >>
> >> Lemma double_s : forall x y:nat, double (S x) y = S (S (double x y)).
> >>
> >> The proof for this one is just by induction on x, and then for the main
> >> theorem, you basically have induction on x, with one rewrite. Both
> proofs
> >> are short and straightforward. Perhaps this is what you were looking
> >> for? Here are my proofs:
> >>
> >> Lemma double_s : forall x y:nat, double (S x) y = S (S (double x y)).
> >> Proof.
> >> intros x.
> >> induction x.
> >> reflexivity.
> >>
> >> intros y.
> >> simpl.
> >> apply IHx.
> >> Qed.
> >>
> >> Theorem even_double : forall x:nat, evenb (double x 0) = true.
> >> Proof.
> >> induction x.
> >> reflexivity.
> >>
> >> rewrite double_s.
> >> simpl.
> >> apply IHx.
> >> Qed.
> >>
> >>
> >> -Rebecca
> >>
> >>
> >> On Sat, Apr 28, 2012 at 1:45 PM, Yin **** <> wrote:
> >>>
> >>> I had been trying not to use anything fancy (like auto), but I would
> >>> try ';'. I guess I can think of it as a join point for branches? Thank
> >>> you.
> >>>
> >>>
> >>> -- Yin
> >>>
> >>>
> >>> On Sat, Apr 28, 2012 at 1:35 PM, James T. Perconti <
> >
> >>> wrote:
> >>> > I just proved it with
> >>> > induction x; intros; simpl; auto.
> >>> > Perhaps you have not learned about ; yet? It applies a tactic to all
> >>> > subgoals generated by its left-hand side.
> >>> > --Jamie
> >>> >
> >>> > ----- Original Message -----
> >>> > From: "Yin ****" <>
> >>> > To: "IUCS Programming Languages"
> >>> > Sent: Saturday, April 28, 2012 1:24:44 PM GMT -05:00 US/Canada
> Eastern
> >>> > Subject: Re: [pl-wonks] soliciting proofs for a trivial theorem
> >>> >
> >>> > Thank you James. The lemma works.
> >>> >
> >>> > I'm not sure if I got the optimal sequence of tactics though. I had
> to
> >>> > induct on x first, then to 'intros' twice at two branches. Otherwise
> >>> > the induction hypothesis will not be universally quantified. I would
> >>> > appreciate a neater way to deal with this.
> >>> >
> >>> > Here is my little ugly proof of the lemma:
> >>> >
> >>> > Lemma even_y : forall x y : nat,
> >>> > evenb y = true -> evenb (double x y) = true.
> >>> >
> >>> > Proof.
> >>> > induction x.
> >>> > intros.
> >>> > simpl.
> >>> > apply H.
> >>> > intros.
> >>> > simpl.
> >>> > apply IHx.
> >>> > simpl.
> >>> > apply H.
> >>> > Qed.
> >>> >
> >>> > The theorem is trivially proved using this lemma:
> >>> >
> >>> > Theorem even_double : forall x:nat,
> >>> > evenb (double x 0) = true.
> >>> > Proof.
> >>> > intros.
> >>> > apply even_y.
> >>> > reflexivity.
> >>> > Qed.
> >>> >
> >>> >
> >>> > I also found another lemma that works:
> >>> >
> >>> > Lemma even_ss : forall x y : nat,
> >>> > evenb (double x y) = evenb (double x (S (S y))).
> >>> >
> >>> > It makes the proof of the theorem a little longer though:
> >>> >
> >>> > Theorem even_double : forall x:nat,
> >>> > evenb (double x 0) = true.
> >>> > Proof.
> >>> > Restart.
> >>> > intros.
> >>> > induction x.
> >>> > reflexivity.
> >>> > simpl.
> >>> > rewrite <- even_ss.
> >>> > apply IHx.
> >>> > Qed.
> >>> >
> >>> >
> >>> > I'll appreciate any other tricks. Thank you.
> >>> >
> >>> >
> >>> > -- Yin
> >>> >
> >>> >
> >>> > On Sat, Apr 28, 2012 at 12:25 PM, James T. Perconti
> >>> > <> wrote:
> >>> >> Yin,
> >>> >> The lemma you want is the generalization of your theorem over the
> >>> >> value of the accumulator:
> >>> >>
> >>> >> Lemma even_double : forall x n,
> >>> >> evenb n = true -> evenb (double x n) = true.
> >>> >>
> >>> >> Proving this is now a simple induction on x, and specializing n to 0
> >>> >> afterward is of course trivial.
> >>> >> I'm not sure what other lemma(s) one might choose instead of this;
> >>> >> maybe that double x n = (double x 0) + n and then that the sum of
> even nats
> >>> >> is even? But the first thing is much simpler.
> >>> >> --Jamie
> >>> >>
> >>> >> ----- Original Message -----
> >>> >> From: "Yin ****" <>
> >>> >> To: "IUCS Programming Languages"
> >>> >> Sent: Saturday, April 28, 2012 12:07:47 PM GMT -05:00 US/Canada
> Eastern
> >>> >> Subject: [pl-wonks] soliciting proofs for a trivial theorem
> >>> >>
> >>> >> Hello,
> >>> >>
> >>> >> I'm wondering what's the best way to prove this seemingly trivial
> >>> >> theorem (in Coq):
> >>> >>
> >>> >> Theorem even_double : forall x:nat,
> >>> >> evenb (double x 0) = true.
> >>> >>
> >>> >> The other definitions are:
> >>> >>
> >>> >> Fixpoint evenb (n:nat) : bool :=
> >>> >> match n with
> >>> >> | O => true
> >>> >> | S O => false
> >>> >> | S (S n') => evenb n'
> >>> >> end.
> >>> >>
> >>> >> Fixpoint double (x y : nat) : nat :=
> >>> >> match x with
> >>> >> | O => y
> >>> >> | S x' => double x' (S (S y))
> >>> >> end.
> >>> >>
> >>> >> Everything seems to be straightforward. The only twist is that
> double
> >>> >> has an accumulator. This is the first theorem in my learning process
> >>> >> where I found that I definitely needed a lemma. The question is,
> which
> >>> >> lemma is the best one to use?
> >>> >>
> >>> >>
> >>> >> -- Yin
> >>> >> _______________________________________________
> >>> >> PL-wonks mailing list
> >>> >> PL-
> >>> >> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
> >>> >> _______________________________________________
> >>> >> PL-wonks mailing list
> >>> >> PL-
> >>> >> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
> >>> >
> >>> > _______________________________________________
> >>> > PL-wonks mailing list
> >>> > PL-
> >>> > http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
> >>> >
> >>> > _______________________________________________
> >>> > PL-wonks mailing list
> >>> > PL-
> >>> > http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
> >>>
> >>> _______________________________________________
> >>> PL-wonks mailing list
> >>> PL-
> >>> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
> >>
> >>
> >>
> >> _______________________________________________
> >> PL-wonks mailing list
> >> PL-
> >> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
> >>
>
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>


That's an amazing analysis!

Indeed they seem to be in that order Rebecca >= Yin >= Jamie, where
Rebecca > Yin seems to be strict. I'm wondering whether Yin > Jamie is
strict. Although Jamie's lemma only talks about the case when y is
even, but evenb y = true -> evenb (double x y) = true seems also
"implicitly" talks about the case when evenb y = false.

If I change my lemma to this:

Lemma even_ss_b :
forall x y : nat,
evenb (double x y) = true -> evenb (double x (S (S y))) = true.

It talks about the same thing, although now 'true' appears explicitly.


The reason I hope to find the weakest lemma and get your train of
thoughts is because I'm wondering how a computer can prove this
theorem without any help. A strong lemma like yours takes experience
and insights to find, but a computer is too naive. So stronger lemmas
will be harder for it to see. Also it could be easy for a computer to
find a "lemma" that's impossible to prove if it doesn't use the
weakest one at hand. But maybe a leap is necessary for harder
theorems.

Also it seems that you are implicitly doing a CPS transformation in
your head and have moved those two S's toward the continuation which
goes toward evenb. Maybe we can capture that kind of continuation in a
automatic prover :-)



-- Yin



On Sat, Apr 28, 2012 at 6:14 PM, Rebecca Swords <> wrote:
> Hi Yin,
>
> Here are some of the things I was thinking about when I came up with the
> lemma. I was looking for a way to take advantage of the structure of even
> numbers in the definition of evenb. To do that, I had to have to have S (S
> something). I also thought it would be better to say something about how the
> final result of double changes, rather than how y changes.
>
> And in the inductive proof of even_double, the proof goal was to show that
> (double (S x) 0) is even, so this lemma gives you a statement about doubling
> the successor of a number.
>
> For your question about comparing these lemmas, I'm not sure how to decide
> whether one is stronger or weaker than another, but I think Jamie's is most
> closely fitted to the original theorem. His lemma is only applicable when y
> is even (which is the only case that matters for even_double), and it makes
> almost the same statement as the original theorem.
>
> With transitivity, yours is a statement about both even and odd values for
> y. It says that for a given x, (double x y) for even values of y is either
> always even or always odd, and similarly for odd values of y. Since yours
> applies to both even and odd y values, I think it's probably more widely
> applicable than Jamie's.
>
> Mine doesn't say anything about evenness, oddness, or y; it's a statement
> relating the results of applying double to different values of x for a given
> y. I think it's probably the most general of the three lemmas. (You can
> easily use it to prove the stronger theorem that double is semantically
> correct, i.e., (double x 0) = x * 2.)
>
> My question is, why do you want the weakest lemma? It seems like once you
> start proving things, you might have several theorems to prove about
> different aspects of your system and how its components are related. If you
> use more general lemmas, it seems like they would be more likely to be
> reusable in different places.
>
> -Rebecca
>
> On Sat, Apr 28, 2012 at 4:02 PM, Yin **** <> wrote:
>>
>> Thanks for the responses :-) Now I'm surprised that we have three
>> lemmas that all work! (still welcoming more of them).
>>
>> Now my questions is, which lemma is the weakest, say we hope to find a
>> lemma that tells us nothing more than proving the theorem?
>>
>>
>> (* James *)
>> Lemma even_y :
>>  forall x y : nat,
>>    evenb y = true -> evenb (double x y) = true.
>>
>>
>> (* Rebecca *)
>> Lemma double_s :
>>  forall x y : nat,
>>    double (S x) y = S (S (double x y)).
>>
>>
>> (* Yin *)
>> Lemma even_ss :
>>  forall x y : nat,
>>    evenb (double x y) = evenb (double x (S (S y))).
>>
>>
>>
>> -- Yin
>>
>>
>> On Sat, Apr 28, 2012 at 3:38 PM, Yin **** <> wrote:
>> > That's a very nice lemma! How did you thought of it?
>> >
>> >
>> > -- Yin
>> >
>> >
>> > On Sat, Apr 28, 2012 at 3:24 PM, Rebecca Swords <>
>> > wrote:
>> >> Hi Yin,
>> >>
>> >> How about this lemma?
>> >>
>> >> Lemma double_s : forall x y:nat, double (S x) y = S (S (double x y)).
>> >>
>> >> The proof for this one is just by induction on x, and then for the main
>> >> theorem, you basically have induction on x, with one rewrite. Both
>> >> proofs
>> >> are short and straightforward. Perhaps this is what you were looking
>> >> for? Here are my proofs:
>> >>
>> >> Lemma double_s : forall x y:nat, double (S x) y = S (S (double x y)).
>> >> Proof.
>> >>   intros x.
>> >>   induction x.
>> >>   reflexivity.
>> >>
>> >>   intros y.
>> >>   simpl.
>> >>   apply IHx.
>> >> Qed.
>> >>
>> >> Theorem even_double : forall x:nat, evenb (double x 0) = true.
>> >> Proof.
>> >>   induction x.
>> >>   reflexivity.
>> >>
>> >>   rewrite double_s.
>> >>   simpl.
>> >>   apply IHx.
>> >> Qed.
>> >>
>> >>
>> >> -Rebecca
>> >>
>> >>
>> >> On Sat, Apr 28, 2012 at 1:45 PM, Yin **** <> wrote:
>> >>>
>> >>> I had been trying not to use anything fancy (like auto), but I would
>> >>> try ';'. I guess I can think of it as a join point for branches? Thank
>> >>> you.
>> >>>
>> >>>
>> >>> -- Yin
>> >>>
>> >>>
>> >>> On Sat, Apr 28, 2012 at 1:35 PM, James T. Perconti
>> >>> <>
>> >>> wrote:
>> >>> > I just proved it with
>> >>> >   induction x; intros; simpl; auto.
>> >>> > Perhaps you have not learned about ; yet?  It applies a tactic to
>> >>> > all
>> >>> > subgoals generated by its left-hand side.
>> >>> >  --Jamie
>> >>> >
>> >>> > ----- Original Message -----
>> >>> > From: "Yin ****" <>
>> >>> > To: "IUCS Programming Languages"
>> >>> > Sent: Saturday, April 28, 2012 1:24:44 PM GMT -05:00 US/Canada
>> >>> > Eastern
>> >>> > Subject: Re: [pl-wonks] soliciting proofs for a trivial theorem
>> >>> >
>> >>> > Thank you James. The lemma works.
>> >>> >
>> >>> > I'm not sure if I got the optimal sequence of tactics though. I had
>> >>> > to
>> >>> > induct on x first, then to 'intros' twice at two branches. Otherwise
>> >>> > the induction hypothesis will not be universally quantified. I would
>> >>> > appreciate a neater way to deal with this.
>> >>> >
>> >>> > Here is my little ugly proof of the lemma:
>> >>> >
>> >>> > Lemma even_y : forall x y : nat,
>> >>> >  evenb y = true -> evenb (double x y) = true.
>> >>> >
>> >>> > Proof.
>> >>> >  induction x.
>> >>> >  intros.
>> >>> >  simpl.
>> >>> >  apply H.
>> >>> >  intros.
>> >>> >  simpl.
>> >>> >  apply IHx.
>> >>> >  simpl.
>> >>> >  apply H.
>> >>> > Qed.
>> >>> >
>> >>> > The theorem is trivially proved using this lemma:
>> >>> >
>> >>> > Theorem even_double : forall x:nat,
>> >>> >  evenb (double x 0) = true.
>> >>> > Proof.
>> >>> >  intros.
>> >>> >  apply even_y.
>> >>> >  reflexivity.
>> >>> > Qed.
>> >>> >
>> >>> >
>> >>> > I also found another lemma that works:
>> >>> >
>> >>> > Lemma even_ss : forall x y : nat,
>> >>> >  evenb (double x y) = evenb (double x (S (S y))).
>> >>> >
>> >>> > It makes the proof of the theorem a little longer though:
>> >>> >
>> >>> > Theorem even_double : forall x:nat,
>> >>> >  evenb (double x 0) = true.
>> >>> > Proof.
>> >>> >  Restart.
>> >>> >  intros.
>> >>> >  induction x.
>> >>> >  reflexivity.
>> >>> >  simpl.
>> >>> >  rewrite <- even_ss.
>> >>> >  apply IHx.
>> >>> > Qed.
>> >>> >
>> >>> >
>> >>> > I'll appreciate any other tricks. Thank you.
>> >>> >
>> >>> >
>> >>> > -- Yin
>> >>> >
>> >>> >
>> >>> > On Sat, Apr 28, 2012 at 12:25 PM, James T. Perconti
>> >>> > <> wrote:
>> >>> >> Yin,
>> >>> >>  The lemma you want is the generalization of your theorem over the
>> >>> >> value of the accumulator:
>> >>> >>
>> >>> >> Lemma even_double : forall x n,
>> >>> >>  evenb n = true -> evenb (double x n) = true.
>> >>> >>
>> >>> >> Proving this is now a simple induction on x, and specializing n to
>> >>> >> 0
>> >>> >> afterward is of course trivial.
>> >>> >>  I'm not sure what other lemma(s) one might choose instead of this;
>> >>> >> maybe that double x n = (double x 0) + n and then that the sum of
>> >>> >> even nats
>> >>> >> is even?  But the first thing is much simpler.
>> >>> >>  --Jamie
>> >>> >>
>> >>> >> ----- Original Message -----
>> >>> >> From: "Yin ****" <>
>> >>> >> To: "IUCS Programming Languages"
>> >>> >> Sent: Saturday, April 28, 2012 12:07:47 PM GMT -05:00 US/Canada
>> >>> >> Eastern
>> >>> >> Subject: [pl-wonks] soliciting proofs for a trivial theorem
>> >>> >>
>> >>> >> Hello,
>> >>> >>
>> >>> >> I'm wondering what's the best way to prove this seemingly trivial
>> >>> >> theorem (in Coq):
>> >>> >>
>> >>> >> Theorem even_double : forall x:nat,
>> >>> >>  evenb (double x 0) = true.
>> >>> >>
>> >>> >> The other definitions are:
>> >>> >>
>> >>> >> Fixpoint evenb (n:nat) : bool :=
>> >>> >>  match n with
>> >>> >>    | O => true
>> >>> >>    | S O => false
>> >>> >>    | S (S n') => evenb n'
>> >>> >>  end.
>> >>> >>
>> >>> >> Fixpoint double (x y : nat) : nat :=
>> >>> >>  match x with
>> >>> >>    | O => y
>> >>> >>    | S x' => double x' (S (S y))
>> >>> >>  end.
>> >>> >>
>> >>> >> Everything seems to be straightforward. The only twist is that
>> >>> >> double
>> >>> >> has an accumulator. This is the first theorem in my learning
>> >>> >> process
>> >>> >> where I found that I definitely needed a lemma. The question is,
>> >>> >> which
>> >>> >> lemma is the best one to use?
>> >>> >>
>> >>> >>
>> >>> >> -- Yin
>> >>> >> _______________________________________________
>> >>> >> PL-wonks mailing list
>> >>> >> PL-
>> >>> >> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>> >>> >> _______________________________________________
>> >>> >> PL-wonks mailing list
>> >>> >> PL-
>> >>> >> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>> >>> >
>> >>> > _______________________________________________
>> >>> > PL-wonks mailing list
>> >>> > PL-
>> >>> > http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>> >>> >
>> >>> > _______________________________________________
>> >>> > PL-wonks mailing list
>> >>> > PL-
>> >>> > http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>> >>>
>> >>> _______________________________________________
>> >>> PL-wonks mailing list
>> >>> PL-
>> >>> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>> >>
>> >>
>> >>
>> >> _______________________________________________
>> >> PL-wonks mailing list
>> >> PL-
>> >> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>> >>
>>
>> _______________________________________________
>> PL-wonks mailing list
>> PL-
>> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>
>
>
> _______________________________________________
> PL-wonks mailing list
> PL-
> http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
>

_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks

On Sat, Apr 28, 2012 at 3:24 PM, Rebecca Swords <> wrote:
> Lemma double_s : forall x y:nat, double (S x) y = S (S (double x y)).
> Proof.
>   intros x.
>   induction x.
>   reflexivity.
>
>   intros y.
>   simpl.
>   apply IHx.
> Qed.

If you're into terse scripts, you can tighten that up a bit:

Lemma double_s : forall x y:nat, double (S x) y = S (S (double x y)).
Proof.
intro.
induction x.
reflexivity.

intro.
apply IHx.
Qed.

--
Live well,
~wren

PhD student in Cognitive Science & Computational Linguistics
Eigenmann, room 807
1900 E. 10th St.
Bloomington, IN 47406-7512

_______________________________________________
PL-wonks mailing list
PL-
http://mailman.cs.indiana.edu/mailman/listinfo/pl-wonks
)