I've been working through the second chapter of Software Foundations
(http://www.cis.upenn.edu/~bcpierce/sf/Lists.html) and I keep getting
stuck on proving this theorem:

Theorem distr_rev : forall l1 l2 : natlist,
rev (l1 ++ l2) = (rev l2) ++ (rev l1).

(In English: if you append two lists and reverse the result, it's the
same as if you had reversed them individually and then appended them
in the opposite order.)

I've tried induction on l1, induction on l2, various helper lemmas,
all to no avail. Anyone been able to solve this one yet and if so, do
you have any tips?

Lindsey
_______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe.

I've been working through the second chapter of Software Foundations
(http://www.cis.upenn.edu/~bcpierce/sf/Lists.html) and I keep getting
stuck on proving this theorem:

Theorem distr_rev : forall l1 l2 : natlist,
rev (l1 ++ l2) = (rev l2) ++ (rev l1).

(In English: if you append two lists and reverse the result, it's the
same as if you had reversed them individually and then appended them
in the opposite order.)

I've tried induction on l1, induction on l2, various helper lemmas,
all to no avail. Anyone been able to solve this one yet and if so, do
you have any tips?

Lindsey
_______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. In HOL this is proved by induction on l1 (with l2 universally
quantified), then rewriting with definition of append, definition of
reverse, the fact that append to nil is identity, and the fact that
append is associative. I'm assuming the definitions are similar in Coq
(i.e. they look like standard functional programming language
definitions of append and reverse)...

show us the subgoals if you just do an induction on l1...

On Thu, Sep 23, 2010 at 7:21 AM, Lindsey Kuper <> wrote:
> I've been working through the second chapter of Software Foundations
> (http://www.cis.upenn.edu/~bcpierce/sf/Lists.html) and I keep getting
> stuck on proving this theorem:
>
> Theorem distr_rev : forall l1 l2 : natlist,
>  rev (l1 ++ l2) = (rev l2) ++ (rev l1).
>
> (In English: if you append two lists and reverse the result, it's the
> same as if you had reversed them individually and then appended them
> in the opposite order.)
>
> I've tried induction on l1, induction on l2, various helper lemmas,
> all to no avail.  Anyone been able to solve this one yet and if so, do
> you have any tips?
>
> Lindsey
> _______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe.

I've been working through the second chapter of Software Foundations
(http://www.cis.upenn.edu/~bcpierce/sf/Lists.html) and I keep getting
stuck on proving this theorem:

Theorem distr_rev : forall l1 l2 : natlist,
rev (l1 ++ l2) = (rev l2) ++ (rev l1).

(In English: if you append two lists and reverse the result, it's the
same as if you had reversed them individually and then appended them
in the opposite order.)

I've tried induction on l1, induction on l2, various helper lemmas,
all to no avail. Anyone been able to solve this one yet and if so, do
you have any tips?

Lindsey
_______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. In HOL this is proved by induction on l1 (with l2 universally
quantified), then rewriting with definition of append, definition of
reverse, the fact that append to nil is identity, and the fact that
append is associative. I'm assuming the definitions are similar in Coq
(i.e. they look like standard functional programming language
definitions of append and reverse)...

show us the subgoals if you just do an induction on l1...

On Thu, Sep 23, 2010 at 7:21 AM, Lindsey Kuper <> wrote:
> I've been working through the second chapter of Software Foundations
> (http://www.cis.upenn.edu/~bcpierce/sf/Lists.html) and I keep getting
> stuck on proving this theorem:
>
> Theorem distr_rev : forall l1 l2 : natlist,
>  rev (l1 ++ l2) = (rev l2) ++ (rev l1).
>
> (In English: if you append two lists and reverse the result, it's the
> same as if you had reversed them individually and then appended them
> in the opposite order.)
>
> I've tried induction on l1, induction on l2, various helper lemmas,
> all to no avail.  Anyone been able to solve this one yet and if so, do
> you have any tips?
>
> Lindsey
> _______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. Finally got it. (Spoilers below if anyone's curious. The snoc_app
helper was the key.)

Ramana, it kind of seems like in Coq the "rewriting with definition
of" steps are taken care of automatically by the "simpl" tactic. I
think you would only use the rewrite tactic with a theorem or an IH,
not with a definition. I didn't end up using the fact that append is
associative, but only because reverse is defined in terms of "snoc",
not in terms of append.

Theorem app_nil_end : forall l : natlist,
l ++ [] = l.
Proof.
intros l. induction l as [ | n l'].
Case "l = nil".
reflexivity.
Case "l = cons n l'".
simpl. rewrite -> IHl'. reflexivity. Qed.

Lemma snoc_app : forall x y : natlist, forall z : nat,
snoc (x ++ y) z = x ++ snoc y z.
Proof.
intros x y z. induction x as [ | a d].
Case "x = nil".
simpl. reflexivity.
Case "x = cons a d".
simpl. rewrite <- IHd. reflexivity.
Qed.

Theorem distr_rev : forall l1 l2 : natlist,
rev (l1 ++ l2) = (rev l2) ++ (rev l1).
Proof.
intros l1 l2. induction l1 as [ | n1 l1'].
Case "l1 = nil".
simpl. rewrite -> app_nil_end. reflexivity.
Case "l1 = cons n1 l1'".
simpl.
rewrite -> IHl1'.
rewrite <- snoc_app.
reflexivity.
Qed.
_______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe.

I've been working through the second chapter of Software Foundations
(http://www.cis.upenn.edu/~bcpierce/sf/Lists.html) and I keep getting
stuck on proving this theorem:

Theorem distr_rev : forall l1 l2 : natlist,
rev (l1 ++ l2) = (rev l2) ++ (rev l1).

(In English: if you append two lists and reverse the result, it's the
same as if you had reversed them individually and then appended them
in the opposite order.)

I've tried induction on l1, induction on l2, various helper lemmas,
all to no avail. Anyone been able to solve this one yet and if so, do
you have any tips?

Lindsey
_______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. In HOL this is proved by induction on l1 (with l2 universally
quantified), then rewriting with definition of append, definition of
reverse, the fact that append to nil is identity, and the fact that
append is associative. I'm assuming the definitions are similar in Coq
(i.e. they look like standard functional programming language
definitions of append and reverse)...

show us the subgoals if you just do an induction on l1...

On Thu, Sep 23, 2010 at 7:21 AM, Lindsey Kuper <> wrote:
> I've been working through the second chapter of Software Foundations
> (http://www.cis.upenn.edu/~bcpierce/sf/Lists.html) and I keep getting
> stuck on proving this theorem:
>
> Theorem distr_rev : forall l1 l2 : natlist,
>  rev (l1 ++ l2) = (rev l2) ++ (rev l1).
>
> (In English: if you append two lists and reverse the result, it's the
> same as if you had reversed them individually and then appended them
> in the opposite order.)
>
> I've tried induction on l1, induction on l2, various helper lemmas,
> all to no avail.  Anyone been able to solve this one yet and if so, do
> you have any tips?
>
> Lindsey
> _______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. Finally got it. (Spoilers below if anyone's curious. The snoc_app
helper was the key.)

Ramana, it kind of seems like in Coq the "rewriting with definition
of" steps are taken care of automatically by the "simpl" tactic. I
think you would only use the rewrite tactic with a theorem or an IH,
not with a definition. I didn't end up using the fact that append is
associative, but only because reverse is defined in terms of "snoc",
not in terms of append.

Theorem app_nil_end : forall l : natlist,
l ++ [] = l.
Proof.
intros l. induction l as [ | n l'].
Case "l = nil".
reflexivity.
Case "l = cons n l'".
simpl. rewrite -> IHl'. reflexivity. Qed.

Lemma snoc_app : forall x y : natlist, forall z : nat,
snoc (x ++ y) z = x ++ snoc y z.
Proof.
intros x y z. induction x as [ | a d].
Case "x = nil".
simpl. reflexivity.
Case "x = cons a d".
simpl. rewrite <- IHd. reflexivity.
Qed.

Theorem distr_rev : forall l1 l2 : natlist,
rev (l1 ++ l2) = (rev l2) ++ (rev l1).
Proof.
intros l1 l2. induction l1 as [ | n1 l1'].
Case "l1 = nil".
simpl. rewrite -> app_nil_end. reflexivity.
Case "l1 = cons n1 l1'".
simpl.
rewrite -> IHl1'.
rewrite <- snoc_app.
reflexivity.
Qed.
_______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. in HOL definitions are just theorems (of the form |- foo x y z = blah
)... what makes them different in Coq?

yes snoc_app is what you need if your reverse is defined like that.
you could now prove your reverse equivalent to one defined in terms of append.

On Thu, Sep 23, 2010 at 10:06 AM, Lindsey Kuper <> wrote:
> Finally got it.  (Spoilers below if anyone's curious.  The snoc_app
> helper was the key.)
>
> Ramana, it kind of seems like in Coq the "rewriting with definition
> of" steps are taken care of automatically by the "simpl" tactic.  I
> think you would only use the rewrite tactic with a theorem or an IH,
> not with a definition.  I didn't end up using the fact that append is
> associative, but only because reverse is defined in terms of "snoc",
> not in terms of append.
>
> Theorem app_nil_end : forall l : natlist,
>  l ++ [] = l.
> Proof.
>  intros l. induction l as [ | n l'].
>  Case "l = nil".
>    reflexivity.
>  Case "l = cons n l'".
>    simpl. rewrite -> IHl'. reflexivity. Qed.
>
> Lemma snoc_app : forall x y : natlist, forall z : nat,
>  snoc (x ++ y) z = x ++ snoc y z.
> Proof.
>  intros x y z. induction x as [ | a d].
>  Case "x = nil".
>    simpl. reflexivity.
>  Case "x = cons a d".
>    simpl. rewrite <- IHd. reflexivity.
> Qed.
>
> Theorem distr_rev : forall l1 l2 : natlist,
>  rev (l1 ++ l2) = (rev l2) ++ (rev l1).
> Proof.
>  intros l1 l2. induction l1 as [ | n1 l1'].
>  Case "l1 = nil".
>    simpl. rewrite -> app_nil_end. reflexivity.
>  Case "l1 = cons n1 l1'".
>    simpl.
>    rewrite -> IHl1'.
>    rewrite <- snoc_app.
>    reflexivity.
> Qed.
> _______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe.

I've been working through the second chapter of Software Foundations
(http://www.cis.upenn.edu/~bcpierce/sf/Lists.html) and I keep getting
stuck on proving this theorem:

Theorem distr_rev : forall l1 l2 : natlist,
rev (l1 ++ l2) = (rev l2) ++ (rev l1).

(In English: if you append two lists and reverse the result, it's the
same as if you had reversed them individually and then appended them
in the opposite order.)

I've tried induction on l1, induction on l2, various helper lemmas,
all to no avail. Anyone been able to solve this one yet and if so, do
you have any tips?

Lindsey
_______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. In HOL this is proved by induction on l1 (with l2 universally
quantified), then rewriting with definition of append, definition of
reverse, the fact that append to nil is identity, and the fact that
append is associative. I'm assuming the definitions are similar in Coq
(i.e. they look like standard functional programming language
definitions of append and reverse)...

show us the subgoals if you just do an induction on l1...

On Thu, Sep 23, 2010 at 7:21 AM, Lindsey Kuper <> wrote:
> I've been working through the second chapter of Software Foundations
> (http://www.cis.upenn.edu/~bcpierce/sf/Lists.html) and I keep getting
> stuck on proving this theorem:
>
> Theorem distr_rev : forall l1 l2 : natlist,
>  rev (l1 ++ l2) = (rev l2) ++ (rev l1).
>
> (In English: if you append two lists and reverse the result, it's the
> same as if you had reversed them individually and then appended them
> in the opposite order.)
>
> I've tried induction on l1, induction on l2, various helper lemmas,
> all to no avail.  Anyone been able to solve this one yet and if so, do
> you have any tips?
>
> Lindsey
> _______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. Finally got it. (Spoilers below if anyone's curious. The snoc_app
helper was the key.)

Ramana, it kind of seems like in Coq the "rewriting with definition
of" steps are taken care of automatically by the "simpl" tactic. I
think you would only use the rewrite tactic with a theorem or an IH,
not with a definition. I didn't end up using the fact that append is
associative, but only because reverse is defined in terms of "snoc",
not in terms of append.

Theorem app_nil_end : forall l : natlist,
l ++ [] = l.
Proof.
intros l. induction l as [ | n l'].
Case "l = nil".
reflexivity.
Case "l = cons n l'".
simpl. rewrite -> IHl'. reflexivity. Qed.

Lemma snoc_app : forall x y : natlist, forall z : nat,
snoc (x ++ y) z = x ++ snoc y z.
Proof.
intros x y z. induction x as [ | a d].
Case "x = nil".
simpl. reflexivity.
Case "x = cons a d".
simpl. rewrite <- IHd. reflexivity.
Qed.

Theorem distr_rev : forall l1 l2 : natlist,
rev (l1 ++ l2) = (rev l2) ++ (rev l1).
Proof.
intros l1 l2. induction l1 as [ | n1 l1'].
Case "l1 = nil".
simpl. rewrite -> app_nil_end. reflexivity.
Case "l1 = cons n1 l1'".
simpl.
rewrite -> IHl1'.
rewrite <- snoc_app.
reflexivity.
Qed.
_______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. in HOL definitions are just theorems (of the form |- foo x y z = blah
)... what makes them different in Coq?

yes snoc_app is what you need if your reverse is defined like that.
you could now prove your reverse equivalent to one defined in terms of append.

On Thu, Sep 23, 2010 at 10:06 AM, Lindsey Kuper <> wrote:
> Finally got it.  (Spoilers below if anyone's curious.  The snoc_app
> helper was the key.)
>
> Ramana, it kind of seems like in Coq the "rewriting with definition
> of" steps are taken care of automatically by the "simpl" tactic.  I
> think you would only use the rewrite tactic with a theorem or an IH,
> not with a definition.  I didn't end up using the fact that append is
> associative, but only because reverse is defined in terms of "snoc",
> not in terms of append.
>
> Theorem app_nil_end : forall l : natlist,
>  l ++ [] = l.
> Proof.
>  intros l. induction l as [ | n l'].
>  Case "l = nil".
>    reflexivity.
>  Case "l = cons n l'".
>    simpl. rewrite -> IHl'. reflexivity. Qed.
>
> Lemma snoc_app : forall x y : natlist, forall z : nat,
>  snoc (x ++ y) z = x ++ snoc y z.
> Proof.
>  intros x y z. induction x as [ | a d].
>  Case "x = nil".
>    simpl. reflexivity.
>  Case "x = cons a d".
>    simpl. rewrite <- IHd. reflexivity.
> Qed.
>
> Theorem distr_rev : forall l1 l2 : natlist,
>  rev (l1 ++ l2) = (rev l2) ++ (rev l1).
> Proof.
>  intros l1 l2. induction l1 as [ | n1 l1'].
>  Case "l1 = nil".
>    simpl. rewrite -> app_nil_end. reflexivity.
>  Case "l1 = cons n1 l1'".
>    simpl.
>    rewrite -> IHl1'.
>    rewrite <- snoc_app.
>    reflexivity.
> Qed.
> _______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. On Wed, Sep 22, 2010 at 8:27 PM, Ramana Kumar <> wrote:
> in HOL definitions are just theorems (of the form |- foo x y z = blah
> )... what makes them different in Coq?

Well, the difference between a definition and a theorem in Coq is that
a theorem needs a proof.
_______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe.

I've been working through the second chapter of Software Foundations
(http://www.cis.upenn.edu/~bcpierce/sf/Lists.html) and I keep getting
stuck on proving this theorem:

Theorem distr_rev : forall l1 l2 : natlist,
rev (l1 ++ l2) = (rev l2) ++ (rev l1).

(In English: if you append two lists and reverse the result, it's the
same as if you had reversed them individually and then appended them
in the opposite order.)

I've tried induction on l1, induction on l2, various helper lemmas,
all to no avail. Anyone been able to solve this one yet and if so, do
you have any tips?

Lindsey
_______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. In HOL this is proved by induction on l1 (with l2 universally
quantified), then rewriting with definition of append, definition of
reverse, the fact that append to nil is identity, and the fact that
append is associative. I'm assuming the definitions are similar in Coq
(i.e. they look like standard functional programming language
definitions of append and reverse)...

show us the subgoals if you just do an induction on l1...

On Thu, Sep 23, 2010 at 7:21 AM, Lindsey Kuper <> wrote:
> I've been working through the second chapter of Software Foundations
> (http://www.cis.upenn.edu/~bcpierce/sf/Lists.html) and I keep getting
> stuck on proving this theorem:
>
> Theorem distr_rev : forall l1 l2 : natlist,
>  rev (l1 ++ l2) = (rev l2) ++ (rev l1).
>
> (In English: if you append two lists and reverse the result, it's the
> same as if you had reversed them individually and then appended them
> in the opposite order.)
>
> I've tried induction on l1, induction on l2, various helper lemmas,
> all to no avail.  Anyone been able to solve this one yet and if so, do
> you have any tips?
>
> Lindsey
> _______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. Finally got it. (Spoilers below if anyone's curious. The snoc_app
helper was the key.)

Ramana, it kind of seems like in Coq the "rewriting with definition
of" steps are taken care of automatically by the "simpl" tactic. I
think you would only use the rewrite tactic with a theorem or an IH,
not with a definition. I didn't end up using the fact that append is
associative, but only because reverse is defined in terms of "snoc",
not in terms of append.

Theorem app_nil_end : forall l : natlist,
l ++ [] = l.
Proof.
intros l. induction l as [ | n l'].
Case "l = nil".
reflexivity.
Case "l = cons n l'".
simpl. rewrite -> IHl'. reflexivity. Qed.

Lemma snoc_app : forall x y : natlist, forall z : nat,
snoc (x ++ y) z = x ++ snoc y z.
Proof.
intros x y z. induction x as [ | a d].
Case "x = nil".
simpl. reflexivity.
Case "x = cons a d".
simpl. rewrite <- IHd. reflexivity.
Qed.

Theorem distr_rev : forall l1 l2 : natlist,
rev (l1 ++ l2) = (rev l2) ++ (rev l1).
Proof.
intros l1 l2. induction l1 as [ | n1 l1'].
Case "l1 = nil".
simpl. rewrite -> app_nil_end. reflexivity.
Case "l1 = cons n1 l1'".
simpl.
rewrite -> IHl1'.
rewrite <- snoc_app.
reflexivity.
Qed.
_______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. in HOL definitions are just theorems (of the form |- foo x y z = blah
)... what makes them different in Coq?

yes snoc_app is what you need if your reverse is defined like that.
you could now prove your reverse equivalent to one defined in terms of append.

On Thu, Sep 23, 2010 at 10:06 AM, Lindsey Kuper <> wrote:
> Finally got it.  (Spoilers below if anyone's curious.  The snoc_app
> helper was the key.)
>
> Ramana, it kind of seems like in Coq the "rewriting with definition
> of" steps are taken care of automatically by the "simpl" tactic.  I
> think you would only use the rewrite tactic with a theorem or an IH,
> not with a definition.  I didn't end up using the fact that append is
> associative, but only because reverse is defined in terms of "snoc",
> not in terms of append.
>
> Theorem app_nil_end : forall l : natlist,
>  l ++ [] = l.
> Proof.
>  intros l. induction l as [ | n l'].
>  Case "l = nil".
>    reflexivity.
>  Case "l = cons n l'".
>    simpl. rewrite -> IHl'. reflexivity. Qed.
>
> Lemma snoc_app : forall x y : natlist, forall z : nat,
>  snoc (x ++ y) z = x ++ snoc y z.
> Proof.
>  intros x y z. induction x as [ | a d].
>  Case "x = nil".
>    simpl. reflexivity.
>  Case "x = cons a d".
>    simpl. rewrite <- IHd. reflexivity.
> Qed.
>
> Theorem distr_rev : forall l1 l2 : natlist,
>  rev (l1 ++ l2) = (rev l2) ++ (rev l1).
> Proof.
>  intros l1 l2. induction l1 as [ | n1 l1'].
>  Case "l1 = nil".
>    simpl. rewrite -> app_nil_end. reflexivity.
>  Case "l1 = cons n1 l1'".
>    simpl.
>    rewrite -> IHl1'.
>    rewrite <- snoc_app.
>    reflexivity.
> Qed.
> _______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. On Wed, Sep 22, 2010 at 8:27 PM, Ramana Kumar <> wrote:
> in HOL definitions are just theorems (of the form |- foo x y z = blah
> )... what makes them different in Coq?

Well, the difference between a definition and a theorem in Coq is that
a theorem needs a proof.
_______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. definitions need proofs too (type correctness, termination (think of
recursive functions)).
but that point aside, just think of "proof by definitional extension"
as a special proof procedure that lets you prove a theorem about a new
constant for free. then the "definition" you get out of that is just a
theorem like any other.

On Thu, Sep 23, 2010 at 11:50 AM, Lindsey Kuper <> wrote:
> On Wed, Sep 22, 2010 at 8:27 PM, Ramana Kumar <> wrote:
>> in HOL definitions are just theorems (of the form |- foo x y z = blah
>> )... what makes them different in Coq?
>
> Well, the difference between a definition and a theorem in Coq is that
> a theorem needs a proof.
> _______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe.

I've been working through the second chapter of Software Foundations
(http://www.cis.upenn.edu/~bcpierce/sf/Lists.html) and I keep getting
stuck on proving this theorem:

Theorem distr_rev : forall l1 l2 : natlist,
rev (l1 ++ l2) = (rev l2) ++ (rev l1).

(In English: if you append two lists and reverse the result, it's the
same as if you had reversed them individually and then appended them
in the opposite order.)

I've tried induction on l1, induction on l2, various helper lemmas,
all to no avail. Anyone been able to solve this one yet and if so, do
you have any tips?

Lindsey
_______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. In HOL this is proved by induction on l1 (with l2 universally
quantified), then rewriting with definition of append, definition of
reverse, the fact that append to nil is identity, and the fact that
append is associative. I'm assuming the definitions are similar in Coq
(i.e. they look like standard functional programming language
definitions of append and reverse)...

show us the subgoals if you just do an induction on l1...

On Thu, Sep 23, 2010 at 7:21 AM, Lindsey Kuper <> wrote:
> I've been working through the second chapter of Software Foundations
> (http://www.cis.upenn.edu/~bcpierce/sf/Lists.html) and I keep getting
> stuck on proving this theorem:
>
> Theorem distr_rev : forall l1 l2 : natlist,
>  rev (l1 ++ l2) = (rev l2) ++ (rev l1).
>
> (In English: if you append two lists and reverse the result, it's the
> same as if you had reversed them individually and then appended them
> in the opposite order.)
>
> I've tried induction on l1, induction on l2, various helper lemmas,
> all to no avail.  Anyone been able to solve this one yet and if so, do
> you have any tips?
>
> Lindsey
> _______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. Finally got it. (Spoilers below if anyone's curious. The snoc_app
helper was the key.)

Ramana, it kind of seems like in Coq the "rewriting with definition
of" steps are taken care of automatically by the "simpl" tactic. I
think you would only use the rewrite tactic with a theorem or an IH,
not with a definition. I didn't end up using the fact that append is
associative, but only because reverse is defined in terms of "snoc",
not in terms of append.

Theorem app_nil_end : forall l : natlist,
l ++ [] = l.
Proof.
intros l. induction l as [ | n l'].
Case "l = nil".
reflexivity.
Case "l = cons n l'".
simpl. rewrite -> IHl'. reflexivity. Qed.

Lemma snoc_app : forall x y : natlist, forall z : nat,
snoc (x ++ y) z = x ++ snoc y z.
Proof.
intros x y z. induction x as [ | a d].
Case "x = nil".
simpl. reflexivity.
Case "x = cons a d".
simpl. rewrite <- IHd. reflexivity.
Qed.

Theorem distr_rev : forall l1 l2 : natlist,
rev (l1 ++ l2) = (rev l2) ++ (rev l1).
Proof.
intros l1 l2. induction l1 as [ | n1 l1'].
Case "l1 = nil".
simpl. rewrite -> app_nil_end. reflexivity.
Case "l1 = cons n1 l1'".
simpl.
rewrite -> IHl1'.
rewrite <- snoc_app.
reflexivity.
Qed.
_______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. in HOL definitions are just theorems (of the form |- foo x y z = blah
)... what makes them different in Coq?

yes snoc_app is what you need if your reverse is defined like that.
you could now prove your reverse equivalent to one defined in terms of append.

On Thu, Sep 23, 2010 at 10:06 AM, Lindsey Kuper <> wrote:
> Finally got it.  (Spoilers below if anyone's curious.  The snoc_app
> helper was the key.)
>
> Ramana, it kind of seems like in Coq the "rewriting with definition
> of" steps are taken care of automatically by the "simpl" tactic.  I
> think you would only use the rewrite tactic with a theorem or an IH,
> not with a definition.  I didn't end up using the fact that append is
> associative, but only because reverse is defined in terms of "snoc",
> not in terms of append.
>
> Theorem app_nil_end : forall l : natlist,
>  l ++ [] = l.
> Proof.
>  intros l. induction l as [ | n l'].
>  Case "l = nil".
>    reflexivity.
>  Case "l = cons n l'".
>    simpl. rewrite -> IHl'. reflexivity. Qed.
>
> Lemma snoc_app : forall x y : natlist, forall z : nat,
>  snoc (x ++ y) z = x ++ snoc y z.
> Proof.
>  intros x y z. induction x as [ | a d].
>  Case "x = nil".
>    simpl. reflexivity.
>  Case "x = cons a d".
>    simpl. rewrite <- IHd. reflexivity.
> Qed.
>
> Theorem distr_rev : forall l1 l2 : natlist,
>  rev (l1 ++ l2) = (rev l2) ++ (rev l1).
> Proof.
>  intros l1 l2. induction l1 as [ | n1 l1'].
>  Case "l1 = nil".
>    simpl. rewrite -> app_nil_end. reflexivity.
>  Case "l1 = cons n1 l1'".
>    simpl.
>    rewrite -> IHl1'.
>    rewrite <- snoc_app.
>    reflexivity.
> Qed.
> _______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. On Wed, Sep 22, 2010 at 8:27 PM, Ramana Kumar <> wrote:
> in HOL definitions are just theorems (of the form |- foo x y z = blah
> )... what makes them different in Coq?

Well, the difference between a definition and a theorem in Coq is that
a theorem needs a proof.
_______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. definitions need proofs too (type correctness, termination (think of
recursive functions)).
but that point aside, just think of "proof by definitional extension"
as a special proof procedure that lets you prove a theorem about a new
constant for free. then the "definition" you get out of that is just a
theorem like any other.

On Thu, Sep 23, 2010 at 11:50 AM, Lindsey Kuper <> wrote:
> On Wed, Sep 22, 2010 at 8:27 PM, Ramana Kumar <> wrote:
>> in HOL definitions are just theorems (of the form |- foo x y z = blah
>> )... what makes them different in Coq?
>
> Well, the difference between a definition and a theorem in Coq is that
> a theorem needs a proof.
> _______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. On Wed, Sep 22, 2010 at 9:55 PM, Ramana Kumar <> wrote:
> definitions need proofs too (type correctness, termination (think of
> recursive functions)).

Yeah, any definition you write with Definition in Coq needs to type
check, and any definition you write with Fixpoint needs to type check
and also satisfy syntactic constraints on what Coq calls the
"decreasing argument" to show that it will terminate, but neither of
those are what Coq calls a Theorem, which needs to be followed with a
Proof. I'm using all those words (Definition, Theorem, Proof) in the
sense of Coq commands, so sorry for the confusion; I don't know how
those concepts map onto HOL.
_______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe.

I've been working through the second chapter of Software Foundations
(http://www.cis.upenn.edu/~bcpierce/sf/Lists.html) and I keep getting
stuck on proving this theorem:

Theorem distr_rev : forall l1 l2 : natlist,
rev (l1 ++ l2) = (rev l2) ++ (rev l1).

(In English: if you append two lists and reverse the result, it's the
same as if you had reversed them individually and then appended them
in the opposite order.)

I've tried induction on l1, induction on l2, various helper lemmas,
all to no avail. Anyone been able to solve this one yet and if so, do
you have any tips?

Lindsey
_______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. In HOL this is proved by induction on l1 (with l2 universally
quantified), then rewriting with definition of append, definition of
reverse, the fact that append to nil is identity, and the fact that
append is associative. I'm assuming the definitions are similar in Coq
(i.e. they look like standard functional programming language
definitions of append and reverse)...

show us the subgoals if you just do an induction on l1...

On Thu, Sep 23, 2010 at 7:21 AM, Lindsey Kuper <> wrote:
> I've been working through the second chapter of Software Foundations
> (http://www.cis.upenn.edu/~bcpierce/sf/Lists.html) and I keep getting
> stuck on proving this theorem:
>
> Theorem distr_rev : forall l1 l2 : natlist,
>  rev (l1 ++ l2) = (rev l2) ++ (rev l1).
>
> (In English: if you append two lists and reverse the result, it's the
> same as if you had reversed them individually and then appended them
> in the opposite order.)
>
> I've tried induction on l1, induction on l2, various helper lemmas,
> all to no avail.  Anyone been able to solve this one yet and if so, do
> you have any tips?
>
> Lindsey
> _______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. Finally got it. (Spoilers below if anyone's curious. The snoc_app
helper was the key.)

Ramana, it kind of seems like in Coq the "rewriting with definition
of" steps are taken care of automatically by the "simpl" tactic. I
think you would only use the rewrite tactic with a theorem or an IH,
not with a definition. I didn't end up using the fact that append is
associative, but only because reverse is defined in terms of "snoc",
not in terms of append.

Theorem app_nil_end : forall l : natlist,
l ++ [] = l.
Proof.
intros l. induction l as [ | n l'].
Case "l = nil".
reflexivity.
Case "l = cons n l'".
simpl. rewrite -> IHl'. reflexivity. Qed.

Lemma snoc_app : forall x y : natlist, forall z : nat,
snoc (x ++ y) z = x ++ snoc y z.
Proof.
intros x y z. induction x as [ | a d].
Case "x = nil".
simpl. reflexivity.
Case "x = cons a d".
simpl. rewrite <- IHd. reflexivity.
Qed.

Theorem distr_rev : forall l1 l2 : natlist,
rev (l1 ++ l2) = (rev l2) ++ (rev l1).
Proof.
intros l1 l2. induction l1 as [ | n1 l1'].
Case "l1 = nil".
simpl. rewrite -> app_nil_end. reflexivity.
Case "l1 = cons n1 l1'".
simpl.
rewrite -> IHl1'.
rewrite <- snoc_app.
reflexivity.
Qed.
_______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. in HOL definitions are just theorems (of the form |- foo x y z = blah
)... what makes them different in Coq?

yes snoc_app is what you need if your reverse is defined like that.
you could now prove your reverse equivalent to one defined in terms of append.

On Thu, Sep 23, 2010 at 10:06 AM, Lindsey Kuper <> wrote:
> Finally got it.  (Spoilers below if anyone's curious.  The snoc_app
> helper was the key.)
>
> Ramana, it kind of seems like in Coq the "rewriting with definition
> of" steps are taken care of automatically by the "simpl" tactic.  I
> think you would only use the rewrite tactic with a theorem or an IH,
> not with a definition.  I didn't end up using the fact that append is
> associative, but only because reverse is defined in terms of "snoc",
> not in terms of append.
>
> Theorem app_nil_end : forall l : natlist,
>  l ++ [] = l.
> Proof.
>  intros l. induction l as [ | n l'].
>  Case "l = nil".
>    reflexivity.
>  Case "l = cons n l'".
>    simpl. rewrite -> IHl'. reflexivity. Qed.
>
> Lemma snoc_app : forall x y : natlist, forall z : nat,
>  snoc (x ++ y) z = x ++ snoc y z.
> Proof.
>  intros x y z. induction x as [ | a d].
>  Case "x = nil".
>    simpl. reflexivity.
>  Case "x = cons a d".
>    simpl. rewrite <- IHd. reflexivity.
> Qed.
>
> Theorem distr_rev : forall l1 l2 : natlist,
>  rev (l1 ++ l2) = (rev l2) ++ (rev l1).
> Proof.
>  intros l1 l2. induction l1 as [ | n1 l1'].
>  Case "l1 = nil".
>    simpl. rewrite -> app_nil_end. reflexivity.
>  Case "l1 = cons n1 l1'".
>    simpl.
>    rewrite -> IHl1'.
>    rewrite <- snoc_app.
>    reflexivity.
> Qed.
> _______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. On Wed, Sep 22, 2010 at 8:27 PM, Ramana Kumar <> wrote:
> in HOL definitions are just theorems (of the form |- foo x y z = blah
> )... what makes them different in Coq?

Well, the difference between a definition and a theorem in Coq is that
a theorem needs a proof.
_______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. definitions need proofs too (type correctness, termination (think of
recursive functions)).
but that point aside, just think of "proof by definitional extension"
as a special proof procedure that lets you prove a theorem about a new
constant for free. then the "definition" you get out of that is just a
theorem like any other.

On Thu, Sep 23, 2010 at 11:50 AM, Lindsey Kuper <> wrote:
> On Wed, Sep 22, 2010 at 8:27 PM, Ramana Kumar <> wrote:
>> in HOL definitions are just theorems (of the form |- foo x y z = blah
>> )... what makes them different in Coq?
>
> Well, the difference between a definition and a theorem in Coq is that
> a theorem needs a proof.
> _______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. On Wed, Sep 22, 2010 at 9:55 PM, Ramana Kumar <> wrote:
> definitions need proofs too (type correctness, termination (think of
> recursive functions)).

Yeah, any definition you write with Definition in Coq needs to type
check, and any definition you write with Fixpoint needs to type check
and also satisfy syntactic constraints on what Coq calls the
"decreasing argument" to show that it will terminate, but neither of
those are what Coq calls a Theorem, which needs to be followed with a
Proof. I'm using all those words (Definition, Theorem, Proof) in the
sense of Coq commands, so sorry for the confusion; I don't know how
those concepts map onto HOL.
_______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. Actually, in Coq both Definition and Theorem are the same thing. They
both need a type (or by Curry-Howard a proposition) and an
implementation (or by Curry-Howard a proof).

For example:
Definition x : forall a, a -> a := fun a -> a.

This has the type "forall a, a -> a" and the implementation "fun a ->
a". Or you could read it as the theorem "forall a, a -> a" with the
proof given by the arrow elimination rule (i.e. "fun a -> body") and
then invoking body.

If on the other hand you write:
Definition x : forall a, a -> a.
Proof. intros. trivial. Qed.

Then Coq runs the "intros" and "trivial" tactics to generate a lambda
term with with "forall a, a -> a".

To see this lambda term run "Print x".

Summary: Coq is just like HOL in this regard. (Though IIRC, there are
some technical differences where using Definition vs. Theorem give some
hints to Coq about which approach you intend to use.)

On 09/22/2010 10:14 PM, Lindsey Kuper wrote:
> On Wed, Sep 22, 2010 at 9:55 PM, Ramana Kumar<> wrote:
>> definitions need proofs too (type correctness, termination (think of
>> recursive functions)).
>
> Yeah, any definition you write with Definition in Coq needs to type
> check, and any definition you write with Fixpoint needs to type check
> and also satisfy syntactic constraints on what Coq calls the
> "decreasing argument" to show that it will terminate, but neither of
> those are what Coq calls a Theorem, which needs to be followed with a
> Proof. I'm using all those words (Definition, Theorem, Proof) in the
> sense of Coq commands, so sorry for the confusion; I don't know how
> those concepts map onto HOL.
> _______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe.

I've been working through the second chapter of Software Foundations
(http://www.cis.upenn.edu/~bcpierce/sf/Lists.html) and I keep getting
stuck on proving this theorem:

Theorem distr_rev : forall l1 l2 : natlist,
rev (l1 ++ l2) = (rev l2) ++ (rev l1).

(In English: if you append two lists and reverse the result, it's the
same as if you had reversed them individually and then appended them
in the opposite order.)

I've tried induction on l1, induction on l2, various helper lemmas,
all to no avail. Anyone been able to solve this one yet and if so, do
you have any tips?

Lindsey
_______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. In HOL this is proved by induction on l1 (with l2 universally
quantified), then rewriting with definition of append, definition of
reverse, the fact that append to nil is identity, and the fact that
append is associative. I'm assuming the definitions are similar in Coq
(i.e. they look like standard functional programming language
definitions of append and reverse)...

show us the subgoals if you just do an induction on l1...

On Thu, Sep 23, 2010 at 7:21 AM, Lindsey Kuper <> wrote:
> I've been working through the second chapter of Software Foundations
> (http://www.cis.upenn.edu/~bcpierce/sf/Lists.html) and I keep getting
> stuck on proving this theorem:
>
> Theorem distr_rev : forall l1 l2 : natlist,
>  rev (l1 ++ l2) = (rev l2) ++ (rev l1).
>
> (In English: if you append two lists and reverse the result, it's the
> same as if you had reversed them individually and then appended them
> in the opposite order.)
>
> I've tried induction on l1, induction on l2, various helper lemmas,
> all to no avail.  Anyone been able to solve this one yet and if so, do
> you have any tips?
>
> Lindsey
> _______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. Finally got it. (Spoilers below if anyone's curious. The snoc_app
helper was the key.)

Ramana, it kind of seems like in Coq the "rewriting with definition
of" steps are taken care of automatically by the "simpl" tactic. I
think you would only use the rewrite tactic with a theorem or an IH,
not with a definition. I didn't end up using the fact that append is
associative, but only because reverse is defined in terms of "snoc",
not in terms of append.

Theorem app_nil_end : forall l : natlist,
l ++ [] = l.
Proof.
intros l. induction l as [ | n l'].
Case "l = nil".
reflexivity.
Case "l = cons n l'".
simpl. rewrite -> IHl'. reflexivity. Qed.

Lemma snoc_app : forall x y : natlist, forall z : nat,
snoc (x ++ y) z = x ++ snoc y z.
Proof.
intros x y z. induction x as [ | a d].
Case "x = nil".
simpl. reflexivity.
Case "x = cons a d".
simpl. rewrite <- IHd. reflexivity.
Qed.

Theorem distr_rev : forall l1 l2 : natlist,
rev (l1 ++ l2) = (rev l2) ++ (rev l1).
Proof.
intros l1 l2. induction l1 as [ | n1 l1'].
Case "l1 = nil".
simpl. rewrite -> app_nil_end. reflexivity.
Case "l1 = cons n1 l1'".
simpl.
rewrite -> IHl1'.
rewrite <- snoc_app.
reflexivity.
Qed.
_______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. in HOL definitions are just theorems (of the form |- foo x y z = blah
)... what makes them different in Coq?

yes snoc_app is what you need if your reverse is defined like that.
you could now prove your reverse equivalent to one defined in terms of append.

On Thu, Sep 23, 2010 at 10:06 AM, Lindsey Kuper <> wrote:
> Finally got it.  (Spoilers below if anyone's curious.  The snoc_app
> helper was the key.)
>
> Ramana, it kind of seems like in Coq the "rewriting with definition
> of" steps are taken care of automatically by the "simpl" tactic.  I
> think you would only use the rewrite tactic with a theorem or an IH,
> not with a definition.  I didn't end up using the fact that append is
> associative, but only because reverse is defined in terms of "snoc",
> not in terms of append.
>
> Theorem app_nil_end : forall l : natlist,
>  l ++ [] = l.
> Proof.
>  intros l. induction l as [ | n l'].
>  Case "l = nil".
>    reflexivity.
>  Case "l = cons n l'".
>    simpl. rewrite -> IHl'. reflexivity. Qed.
>
> Lemma snoc_app : forall x y : natlist, forall z : nat,
>  snoc (x ++ y) z = x ++ snoc y z.
> Proof.
>  intros x y z. induction x as [ | a d].
>  Case "x = nil".
>    simpl. reflexivity.
>  Case "x = cons a d".
>    simpl. rewrite <- IHd. reflexivity.
> Qed.
>
> Theorem distr_rev : forall l1 l2 : natlist,
>  rev (l1 ++ l2) = (rev l2) ++ (rev l1).
> Proof.
>  intros l1 l2. induction l1 as [ | n1 l1'].
>  Case "l1 = nil".
>    simpl. rewrite -> app_nil_end. reflexivity.
>  Case "l1 = cons n1 l1'".
>    simpl.
>    rewrite -> IHl1'.
>    rewrite <- snoc_app.
>    reflexivity.
> Qed.
> _______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. On Wed, Sep 22, 2010 at 8:27 PM, Ramana Kumar <> wrote:
> in HOL definitions are just theorems (of the form |- foo x y z = blah
> )... what makes them different in Coq?

Well, the difference between a definition and a theorem in Coq is that
a theorem needs a proof.
_______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. definitions need proofs too (type correctness, termination (think of
recursive functions)).
but that point aside, just think of "proof by definitional extension"
as a special proof procedure that lets you prove a theorem about a new
constant for free. then the "definition" you get out of that is just a
theorem like any other.

On Thu, Sep 23, 2010 at 11:50 AM, Lindsey Kuper <> wrote:
> On Wed, Sep 22, 2010 at 8:27 PM, Ramana Kumar <> wrote:
>> in HOL definitions are just theorems (of the form |- foo x y z = blah
>> )... what makes them different in Coq?
>
> Well, the difference between a definition and a theorem in Coq is that
> a theorem needs a proof.
> _______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. On Wed, Sep 22, 2010 at 9:55 PM, Ramana Kumar <> wrote:
> definitions need proofs too (type correctness, termination (think of
> recursive functions)).

Yeah, any definition you write with Definition in Coq needs to type
check, and any definition you write with Fixpoint needs to type check
and also satisfy syntactic constraints on what Coq calls the
"decreasing argument" to show that it will terminate, but neither of
those are what Coq calls a Theorem, which needs to be followed with a
Proof. I'm using all those words (Definition, Theorem, Proof) in the
sense of Coq commands, so sorry for the confusion; I don't know how
those concepts map onto HOL.
_______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. Actually, in Coq both Definition and Theorem are the same thing. They
both need a type (or by Curry-Howard a proposition) and an
implementation (or by Curry-Howard a proof).

For example:
Definition x : forall a, a -> a := fun a -> a.

This has the type "forall a, a -> a" and the implementation "fun a ->
a". Or you could read it as the theorem "forall a, a -> a" with the
proof given by the arrow elimination rule (i.e. "fun a -> body") and
then invoking body.

If on the other hand you write:
Definition x : forall a, a -> a.
Proof. intros. trivial. Qed.

Then Coq runs the "intros" and "trivial" tactics to generate a lambda
term with with "forall a, a -> a".

To see this lambda term run "Print x".

Summary: Coq is just like HOL in this regard. (Though IIRC, there are
some technical differences where using Definition vs. Theorem give some
hints to Coq about which approach you intend to use.)

On 09/22/2010 10:14 PM, Lindsey Kuper wrote:
> On Wed, Sep 22, 2010 at 9:55 PM, Ramana Kumar<> wrote:
>> definitions need proofs too (type correctness, termination (think of
>> recursive functions)).
>
> Yeah, any definition you write with Definition in Coq needs to type
> check, and any definition you write with Fixpoint needs to type check
> and also satisfy syntactic constraints on what Coq calls the
> "decreasing argument" to show that it will terminate, but neither of
> those are what Coq calls a Theorem, which needs to be followed with a
> Proof. I'm using all those words (Definition, Theorem, Proof) in the
> sense of Coq commands, so sorry for the confusion; I don't know how
> those concepts map onto HOL.
> _______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. Steve Johnson wrote:
>
> Or if you are in a hurry, this example is worked out in Section 7.7 of
> my book.
>
It's protected, at least when I try from home. Any workaround?

thnx much - daniel

I've been working through the second chapter of Software Foundations
(http://www.cis.upenn.edu/~bcpierce/sf/Lists.html) and I keep getting
stuck on proving this theorem:

Theorem distr_rev : forall l1 l2 : natlist,
rev (l1 ++ l2) = (rev l2) ++ (rev l1).

(In English: if you append two lists and reverse the result, it's the
same as if you had reversed them individually and then appended them
in the opposite order.)

I've tried induction on l1, induction on l2, various helper lemmas,
all to no avail. Anyone been able to solve this one yet and if so, do
you have any tips?

Lindsey
_______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. In HOL this is proved by induction on l1 (with l2 universally
quantified), then rewriting with definition of append, definition of
reverse, the fact that append to nil is identity, and the fact that
append is associative. I'm assuming the definitions are similar in Coq
(i.e. they look like standard functional programming language
definitions of append and reverse)...

show us the subgoals if you just do an induction on l1...

On Thu, Sep 23, 2010 at 7:21 AM, Lindsey Kuper <> wrote:
> I've been working through the second chapter of Software Foundations
> (http://www.cis.upenn.edu/~bcpierce/sf/Lists.html) and I keep getting
> stuck on proving this theorem:
>
> Theorem distr_rev : forall l1 l2 : natlist,
>  rev (l1 ++ l2) = (rev l2) ++ (rev l1).
>
> (In English: if you append two lists and reverse the result, it's the
> same as if you had reversed them individually and then appended them
> in the opposite order.)
>
> I've tried induction on l1, induction on l2, various helper lemmas,
> all to no avail.  Anyone been able to solve this one yet and if so, do
> you have any tips?
>
> Lindsey
> _______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. Finally got it. (Spoilers below if anyone's curious. The snoc_app
helper was the key.)

Ramana, it kind of seems like in Coq the "rewriting with definition
of" steps are taken care of automatically by the "simpl" tactic. I
think you would only use the rewrite tactic with a theorem or an IH,
not with a definition. I didn't end up using the fact that append is
associative, but only because reverse is defined in terms of "snoc",
not in terms of append.

Theorem app_nil_end : forall l : natlist,
l ++ [] = l.
Proof.
intros l. induction l as [ | n l'].
Case "l = nil".
reflexivity.
Case "l = cons n l'".
simpl. rewrite -> IHl'. reflexivity. Qed.

Lemma snoc_app : forall x y : natlist, forall z : nat,
snoc (x ++ y) z = x ++ snoc y z.
Proof.
intros x y z. induction x as [ | a d].
Case "x = nil".
simpl. reflexivity.
Case "x = cons a d".
simpl. rewrite <- IHd. reflexivity.
Qed.

Theorem distr_rev : forall l1 l2 : natlist,
rev (l1 ++ l2) = (rev l2) ++ (rev l1).
Proof.
intros l1 l2. induction l1 as [ | n1 l1'].
Case "l1 = nil".
simpl. rewrite -> app_nil_end. reflexivity.
Case "l1 = cons n1 l1'".
simpl.
rewrite -> IHl1'.
rewrite <- snoc_app.
reflexivity.
Qed.
_______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. in HOL definitions are just theorems (of the form |- foo x y z = blah
)... what makes them different in Coq?

yes snoc_app is what you need if your reverse is defined like that.
you could now prove your reverse equivalent to one defined in terms of append.

On Thu, Sep 23, 2010 at 10:06 AM, Lindsey Kuper <> wrote:
> Finally got it.  (Spoilers below if anyone's curious.  The snoc_app
> helper was the key.)
>
> Ramana, it kind of seems like in Coq the "rewriting with definition
> of" steps are taken care of automatically by the "simpl" tactic.  I
> think you would only use the rewrite tactic with a theorem or an IH,
> not with a definition.  I didn't end up using the fact that append is
> associative, but only because reverse is defined in terms of "snoc",
> not in terms of append.
>
> Theorem app_nil_end : forall l : natlist,
>  l ++ [] = l.
> Proof.
>  intros l. induction l as [ | n l'].
>  Case "l = nil".
>    reflexivity.
>  Case "l = cons n l'".
>    simpl. rewrite -> IHl'. reflexivity. Qed.
>
> Lemma snoc_app : forall x y : natlist, forall z : nat,
>  snoc (x ++ y) z = x ++ snoc y z.
> Proof.
>  intros x y z. induction x as [ | a d].
>  Case "x = nil".
>    simpl. reflexivity.
>  Case "x = cons a d".
>    simpl. rewrite <- IHd. reflexivity.
> Qed.
>
> Theorem distr_rev : forall l1 l2 : natlist,
>  rev (l1 ++ l2) = (rev l2) ++ (rev l1).
> Proof.
>  intros l1 l2. induction l1 as [ | n1 l1'].
>  Case "l1 = nil".
>    simpl. rewrite -> app_nil_end. reflexivity.
>  Case "l1 = cons n1 l1'".
>    simpl.
>    rewrite -> IHl1'.
>    rewrite <- snoc_app.
>    reflexivity.
> Qed.
> _______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. On Wed, Sep 22, 2010 at 8:27 PM, Ramana Kumar <> wrote:
> in HOL definitions are just theorems (of the form |- foo x y z = blah
> )... what makes them different in Coq?

Well, the difference between a definition and a theorem in Coq is that
a theorem needs a proof.
_______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. definitions need proofs too (type correctness, termination (think of
recursive functions)).
but that point aside, just think of "proof by definitional extension"
as a special proof procedure that lets you prove a theorem about a new
constant for free. then the "definition" you get out of that is just a
theorem like any other.

On Thu, Sep 23, 2010 at 11:50 AM, Lindsey Kuper <> wrote:
> On Wed, Sep 22, 2010 at 8:27 PM, Ramana Kumar <> wrote:
>> in HOL definitions are just theorems (of the form |- foo x y z = blah
>> )... what makes them different in Coq?
>
> Well, the difference between a definition and a theorem in Coq is that
> a theorem needs a proof.
> _______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. On Wed, Sep 22, 2010 at 9:55 PM, Ramana Kumar <> wrote:
> definitions need proofs too (type correctness, termination (think of
> recursive functions)).

Yeah, any definition you write with Definition in Coq needs to type
check, and any definition you write with Fixpoint needs to type check
and also satisfy syntactic constraints on what Coq calls the
"decreasing argument" to show that it will terminate, but neither of
those are what Coq calls a Theorem, which needs to be followed with a
Proof. I'm using all those words (Definition, Theorem, Proof) in the
sense of Coq commands, so sorry for the confusion; I don't know how
those concepts map onto HOL.
_______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. Actually, in Coq both Definition and Theorem are the same thing. They
both need a type (or by Curry-Howard a proposition) and an
implementation (or by Curry-Howard a proof).

For example:
Definition x : forall a, a -> a := fun a -> a.

This has the type "forall a, a -> a" and the implementation "fun a ->
a". Or you could read it as the theorem "forall a, a -> a" with the
proof given by the arrow elimination rule (i.e. "fun a -> body") and
then invoking body.

If on the other hand you write:
Definition x : forall a, a -> a.
Proof. intros. trivial. Qed.

Then Coq runs the "intros" and "trivial" tactics to generate a lambda
term with with "forall a, a -> a".

To see this lambda term run "Print x".

Summary: Coq is just like HOL in this regard. (Though IIRC, there are
some technical differences where using Definition vs. Theorem give some
hints to Coq about which approach you intend to use.)

On 09/22/2010 10:14 PM, Lindsey Kuper wrote:
> On Wed, Sep 22, 2010 at 9:55 PM, Ramana Kumar<> wrote:
>> definitions need proofs too (type correctness, termination (think of
>> recursive functions)).
>
> Yeah, any definition you write with Definition in Coq needs to type
> check, and any definition you write with Fixpoint needs to type check
> and also satisfy syntactic constraints on what Coq calls the
> "decreasing argument" to show that it will terminate, but neither of
> those are what Coq calls a Theorem, which needs to be followed with a
> Proof. I'm using all those words (Definition, Theorem, Proof) in the
> sense of Coq commands, so sorry for the confusion; I don't know how
> those concepts map onto HOL.
> _______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. Steve Johnson wrote:
>
> Or if you are in a hurry, this example is worked out in Section 7.7 of
> my book.
>
It's protected, at least when I try from home. Any workaround?

thnx much - daniel On Wed, Sep 22, 2010 at 8:06 PM, Lindsey Kuper <> wrote:
> Ramana, it kind of seems like in Coq the "rewriting with definition
> of" steps are taken care of automatically by the "simpl" tactic.  I
> think you would only use the rewrite tactic with a theorem or an IH,

Yes, "rewrite" is only used for applying proofs of equality to rewrite
things. Whereas "simpl" and related tactics are for doing evaluation,
which includes replacing a variable by its definition.

As Michael mentions "definitions" and "theorems" are the same thing,
modulo Coq's messed up way of trying to do irrelevance via forbidding
the reduction of things. Srsly, the only difference between Coq's ten
billion names for defining things is whether the resulting definition
is opaque or translucent re evaluation. If there were a Coquette, it
would only have keywords for giving definitions of variables and for
giving definitions of (co)inductive types. If you really wanted to
keep the opaqueness around for some reason, you could push that into
the terms just like fix, cofix, fun,...

--
Live well,
~wren

_______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe.

I've been working through the second chapter of Software Foundations
(http://www.cis.upenn.edu/~bcpierce/sf/Lists.html) and I keep getting
stuck on proving this theorem:

Theorem distr_rev : forall l1 l2 : natlist,
rev (l1 ++ l2) = (rev l2) ++ (rev l1).

(In English: if you append two lists and reverse the result, it's the
same as if you had reversed them individually and then appended them
in the opposite order.)

I've tried induction on l1, induction on l2, various helper lemmas,
all to no avail. Anyone been able to solve this one yet and if so, do
you have any tips?

Lindsey
_______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. In HOL this is proved by induction on l1 (with l2 universally
quantified), then rewriting with definition of append, definition of
reverse, the fact that append to nil is identity, and the fact that
append is associative. I'm assuming the definitions are similar in Coq
(i.e. they look like standard functional programming language
definitions of append and reverse)...

show us the subgoals if you just do an induction on l1...

On Thu, Sep 23, 2010 at 7:21 AM, Lindsey Kuper <> wrote:
> I've been working through the second chapter of Software Foundations
> (http://www.cis.upenn.edu/~bcpierce/sf/Lists.html) and I keep getting
> stuck on proving this theorem:
>
> Theorem distr_rev : forall l1 l2 : natlist,
>  rev (l1 ++ l2) = (rev l2) ++ (rev l1).
>
> (In English: if you append two lists and reverse the result, it's the
> same as if you had reversed them individually and then appended them
> in the opposite order.)
>
> I've tried induction on l1, induction on l2, various helper lemmas,
> all to no avail.  Anyone been able to solve this one yet and if so, do
> you have any tips?
>
> Lindsey
> _______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. Finally got it. (Spoilers below if anyone's curious. The snoc_app
helper was the key.)

Ramana, it kind of seems like in Coq the "rewriting with definition
of" steps are taken care of automatically by the "simpl" tactic. I
think you would only use the rewrite tactic with a theorem or an IH,
not with a definition. I didn't end up using the fact that append is
associative, but only because reverse is defined in terms of "snoc",
not in terms of append.

Theorem app_nil_end : forall l : natlist,
l ++ [] = l.
Proof.
intros l. induction l as [ | n l'].
Case "l = nil".
reflexivity.
Case "l = cons n l'".
simpl. rewrite -> IHl'. reflexivity. Qed.

Lemma snoc_app : forall x y : natlist, forall z : nat,
snoc (x ++ y) z = x ++ snoc y z.
Proof.
intros x y z. induction x as [ | a d].
Case "x = nil".
simpl. reflexivity.
Case "x = cons a d".
simpl. rewrite <- IHd. reflexivity.
Qed.

Theorem distr_rev : forall l1 l2 : natlist,
rev (l1 ++ l2) = (rev l2) ++ (rev l1).
Proof.
intros l1 l2. induction l1 as [ | n1 l1'].
Case "l1 = nil".
simpl. rewrite -> app_nil_end. reflexivity.
Case "l1 = cons n1 l1'".
simpl.
rewrite -> IHl1'.
rewrite <- snoc_app.
reflexivity.
Qed.
_______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. in HOL definitions are just theorems (of the form |- foo x y z = blah
)... what makes them different in Coq?

yes snoc_app is what you need if your reverse is defined like that.
you could now prove your reverse equivalent to one defined in terms of append.

On Thu, Sep 23, 2010 at 10:06 AM, Lindsey Kuper <> wrote:
> Finally got it.  (Spoilers below if anyone's curious.  The snoc_app
> helper was the key.)
>
> Ramana, it kind of seems like in Coq the "rewriting with definition
> of" steps are taken care of automatically by the "simpl" tactic.  I
> think you would only use the rewrite tactic with a theorem or an IH,
> not with a definition.  I didn't end up using the fact that append is
> associative, but only because reverse is defined in terms of "snoc",
> not in terms of append.
>
> Theorem app_nil_end : forall l : natlist,
>  l ++ [] = l.
> Proof.
>  intros l. induction l as [ | n l'].
>  Case "l = nil".
>    reflexivity.
>  Case "l = cons n l'".
>    simpl. rewrite -> IHl'. reflexivity. Qed.
>
> Lemma snoc_app : forall x y : natlist, forall z : nat,
>  snoc (x ++ y) z = x ++ snoc y z.
> Proof.
>  intros x y z. induction x as [ | a d].
>  Case "x = nil".
>    simpl. reflexivity.
>  Case "x = cons a d".
>    simpl. rewrite <- IHd. reflexivity.
> Qed.
>
> Theorem distr_rev : forall l1 l2 : natlist,
>  rev (l1 ++ l2) = (rev l2) ++ (rev l1).
> Proof.
>  intros l1 l2. induction l1 as [ | n1 l1'].
>  Case "l1 = nil".
>    simpl. rewrite -> app_nil_end. reflexivity.
>  Case "l1 = cons n1 l1'".
>    simpl.
>    rewrite -> IHl1'.
>    rewrite <- snoc_app.
>    reflexivity.
> Qed.
> _______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. On Wed, Sep 22, 2010 at 8:27 PM, Ramana Kumar <> wrote:
> in HOL definitions are just theorems (of the form |- foo x y z = blah
> )... what makes them different in Coq?

Well, the difference between a definition and a theorem in Coq is that
a theorem needs a proof.
_______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. definitions need proofs too (type correctness, termination (think of
recursive functions)).
but that point aside, just think of "proof by definitional extension"
as a special proof procedure that lets you prove a theorem about a new
constant for free. then the "definition" you get out of that is just a
theorem like any other.

On Thu, Sep 23, 2010 at 11:50 AM, Lindsey Kuper <> wrote:
> On Wed, Sep 22, 2010 at 8:27 PM, Ramana Kumar <> wrote:
>> in HOL definitions are just theorems (of the form |- foo x y z = blah
>> )... what makes them different in Coq?
>
> Well, the difference between a definition and a theorem in Coq is that
> a theorem needs a proof.
> _______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. On Wed, Sep 22, 2010 at 9:55 PM, Ramana Kumar <> wrote:
> definitions need proofs too (type correctness, termination (think of
> recursive functions)).

Yeah, any definition you write with Definition in Coq needs to type
check, and any definition you write with Fixpoint needs to type check
and also satisfy syntactic constraints on what Coq calls the
"decreasing argument" to show that it will terminate, but neither of
those are what Coq calls a Theorem, which needs to be followed with a
Proof. I'm using all those words (Definition, Theorem, Proof) in the
sense of Coq commands, so sorry for the confusion; I don't know how
those concepts map onto HOL.
_______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. Actually, in Coq both Definition and Theorem are the same thing. They
both need a type (or by Curry-Howard a proposition) and an
implementation (or by Curry-Howard a proof).

For example:
Definition x : forall a, a -> a := fun a -> a.

This has the type "forall a, a -> a" and the implementation "fun a ->
a". Or you could read it as the theorem "forall a, a -> a" with the
proof given by the arrow elimination rule (i.e. "fun a -> body") and
then invoking body.

If on the other hand you write:
Definition x : forall a, a -> a.
Proof. intros. trivial. Qed.

Then Coq runs the "intros" and "trivial" tactics to generate a lambda
term with with "forall a, a -> a".

To see this lambda term run "Print x".

Summary: Coq is just like HOL in this regard. (Though IIRC, there are
some technical differences where using Definition vs. Theorem give some
hints to Coq about which approach you intend to use.)

On 09/22/2010 10:14 PM, Lindsey Kuper wrote:
> On Wed, Sep 22, 2010 at 9:55 PM, Ramana Kumar<> wrote:
>> definitions need proofs too (type correctness, termination (think of
>> recursive functions)).
>
> Yeah, any definition you write with Definition in Coq needs to type
> check, and any definition you write with Fixpoint needs to type check
> and also satisfy syntactic constraints on what Coq calls the
> "decreasing argument" to show that it will terminate, but neither of
> those are what Coq calls a Theorem, which needs to be followed with a
> Proof. I'm using all those words (Definition, Theorem, Proof) in the
> sense of Coq commands, so sorry for the confusion; I don't know how
> those concepts map onto HOL.
> _______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. Steve Johnson wrote:
>
> Or if you are in a hurry, this example is worked out in Section 7.7 of
> my book.
>
It's protected, at least when I try from home. Any workaround?

thnx much - daniel On Wed, Sep 22, 2010 at 8:06 PM, Lindsey Kuper <> wrote:
> Ramana, it kind of seems like in Coq the "rewriting with definition
> of" steps are taken care of automatically by the "simpl" tactic.  I
> think you would only use the rewrite tactic with a theorem or an IH,

Yes, "rewrite" is only used for applying proofs of equality to rewrite
things. Whereas "simpl" and related tactics are for doing evaluation,
which includes replacing a variable by its definition.

As Michael mentions "definitions" and "theorems" are the same thing,
modulo Coq's messed up way of trying to do irrelevance via forbidding
the reduction of things. Srsly, the only difference between Coq's ten
billion names for defining things is whether the resulting definition
is opaque or translucent re evaluation. If there were a Coquette, it
would only have keywords for giving definitions of variables and for
giving definitions of (co)inductive types. If you really wanted to
keep the opaqueness around for some reason, you could push that into
the terms just like fix, cofix, fun,...

--
Live well,
~wren

_______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. HOL has a constant Abbrev, defined by "Abbrev x = x" but intended for
use when x is of the form "var = term", which the simplifier (i.e.
rewriter) doesn't expand underneath. This gives you a general form of
opaqueness, where you set up a temporary binding from var to term.
(You rewrite with the definition of Abbrev in a particular place
(which you can specify with a pattern) to make the var transparent, or
just make it disappear really.) I think this is somewhat like your
idea of using fix, cofix, etc.

Then there is also the notion of a parse-level abbreviation, which the
parser and pretty printer print one way, which might look like a
constant, but the real term underneath is something else. This will
always be completely transparent, since there isn't anything at the
term level to be opaque.

Finally, constants are by default opaque unless you include some
theorem about them in your call to the simplifier (or such a theorem
is in the automatic extendible set of rewrites). (Such a theorem could
be a "definition".)

On Thu, Sep 23, 2010 at 6:33 PM, wren ng thornton <> wrote:
> On Wed, Sep 22, 2010 at 8:06 PM, Lindsey Kuper <> wrote:
>> Ramana, it kind of seems like in Coq the "rewriting with definition
>> of" steps are taken care of automatically by the "simpl" tactic.  I
>> think you would only use the rewrite tactic with a theorem or an IH,
>
> Yes, "rewrite" is only used for applying proofs of equality to rewrite
> things. Whereas "simpl" and related tactics are for doing evaluation,
> which includes replacing a variable by its definition.
>
> As Michael mentions "definitions" and "theorems" are the same thing,
> modulo Coq's messed up way of trying to do irrelevance via forbidding
> the reduction of things. Srsly, the only difference between Coq's ten
> billion names for defining things is whether the resulting definition
> is opaque or translucent re evaluation. If there were a Coquette, it
> would only have keywords for giving definitions of variables and for
> giving definitions of (co)inductive types. If you really wanted to
> keep the opaqueness around for some reason, you could push that into
> the terms just like fix, cofix, fun,...
>
> --
> Live well,
> ~wren
>
> _______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe.

I've been working through the second chapter of Software Foundations
(http://www.cis.upenn.edu/~bcpierce/sf/Lists.html) and I keep getting
stuck on proving this theorem:

Theorem distr_rev : forall l1 l2 : natlist,
rev (l1 ++ l2) = (rev l2) ++ (rev l1).

(In English: if you append two lists and reverse the result, it's the
same as if you had reversed them individually and then appended them
in the opposite order.)

I've tried induction on l1, induction on l2, various helper lemmas,
all to no avail. Anyone been able to solve this one yet and if so, do
you have any tips?

Lindsey
_______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. In HOL this is proved by induction on l1 (with l2 universally
quantified), then rewriting with definition of append, definition of
reverse, the fact that append to nil is identity, and the fact that
append is associative. I'm assuming the definitions are similar in Coq
(i.e. they look like standard functional programming language
definitions of append and reverse)...

show us the subgoals if you just do an induction on l1...

On Thu, Sep 23, 2010 at 7:21 AM, Lindsey Kuper <> wrote:
> I've been working through the second chapter of Software Foundations
> (http://www.cis.upenn.edu/~bcpierce/sf/Lists.html) and I keep getting
> stuck on proving this theorem:
>
> Theorem distr_rev : forall l1 l2 : natlist,
>  rev (l1 ++ l2) = (rev l2) ++ (rev l1).
>
> (In English: if you append two lists and reverse the result, it's the
> same as if you had reversed them individually and then appended them
> in the opposite order.)
>
> I've tried induction on l1, induction on l2, various helper lemmas,
> all to no avail.  Anyone been able to solve this one yet and if so, do
> you have any tips?
>
> Lindsey
> _______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. Finally got it. (Spoilers below if anyone's curious. The snoc_app
helper was the key.)

Ramana, it kind of seems like in Coq the "rewriting with definition
of" steps are taken care of automatically by the "simpl" tactic. I
think you would only use the rewrite tactic with a theorem or an IH,
not with a definition. I didn't end up using the fact that append is
associative, but only because reverse is defined in terms of "snoc",
not in terms of append.

Theorem app_nil_end : forall l : natlist,
l ++ [] = l.
Proof.
intros l. induction l as [ | n l'].
Case "l = nil".
reflexivity.
Case "l = cons n l'".
simpl. rewrite -> IHl'. reflexivity. Qed.

Lemma snoc_app : forall x y : natlist, forall z : nat,
snoc (x ++ y) z = x ++ snoc y z.
Proof.
intros x y z. induction x as [ | a d].
Case "x = nil".
simpl. reflexivity.
Case "x = cons a d".
simpl. rewrite <- IHd. reflexivity.
Qed.

Theorem distr_rev : forall l1 l2 : natlist,
rev (l1 ++ l2) = (rev l2) ++ (rev l1).
Proof.
intros l1 l2. induction l1 as [ | n1 l1'].
Case "l1 = nil".
simpl. rewrite -> app_nil_end. reflexivity.
Case "l1 = cons n1 l1'".
simpl.
rewrite -> IHl1'.
rewrite <- snoc_app.
reflexivity.
Qed.
_______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. in HOL definitions are just theorems (of the form |- foo x y z = blah
)... what makes them different in Coq?

yes snoc_app is what you need if your reverse is defined like that.
you could now prove your reverse equivalent to one defined in terms of append.

On Thu, Sep 23, 2010 at 10:06 AM, Lindsey Kuper <> wrote:
> Finally got it.  (Spoilers below if anyone's curious.  The snoc_app
> helper was the key.)
>
> Ramana, it kind of seems like in Coq the "rewriting with definition
> of" steps are taken care of automatically by the "simpl" tactic.  I
> think you would only use the rewrite tactic with a theorem or an IH,
> not with a definition.  I didn't end up using the fact that append is
> associative, but only because reverse is defined in terms of "snoc",
> not in terms of append.
>
> Theorem app_nil_end : forall l : natlist,
>  l ++ [] = l.
> Proof.
>  intros l. induction l as [ | n l'].
>  Case "l = nil".
>    reflexivity.
>  Case "l = cons n l'".
>    simpl. rewrite -> IHl'. reflexivity. Qed.
>
> Lemma snoc_app : forall x y : natlist, forall z : nat,
>  snoc (x ++ y) z = x ++ snoc y z.
> Proof.
>  intros x y z. induction x as [ | a d].
>  Case "x = nil".
>    simpl. reflexivity.
>  Case "x = cons a d".
>    simpl. rewrite <- IHd. reflexivity.
> Qed.
>
> Theorem distr_rev : forall l1 l2 : natlist,
>  rev (l1 ++ l2) = (rev l2) ++ (rev l1).
> Proof.
>  intros l1 l2. induction l1 as [ | n1 l1'].
>  Case "l1 = nil".
>    simpl. rewrite -> app_nil_end. reflexivity.
>  Case "l1 = cons n1 l1'".
>    simpl.
>    rewrite -> IHl1'.
>    rewrite <- snoc_app.
>    reflexivity.
> Qed.
> _______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. On Wed, Sep 22, 2010 at 8:27 PM, Ramana Kumar <> wrote:
> in HOL definitions are just theorems (of the form |- foo x y z = blah
> )... what makes them different in Coq?

Well, the difference between a definition and a theorem in Coq is that
a theorem needs a proof.
_______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. definitions need proofs too (type correctness, termination (think of
recursive functions)).
but that point aside, just think of "proof by definitional extension"
as a special proof procedure that lets you prove a theorem about a new
constant for free. then the "definition" you get out of that is just a
theorem like any other.

On Thu, Sep 23, 2010 at 11:50 AM, Lindsey Kuper <> wrote:
> On Wed, Sep 22, 2010 at 8:27 PM, Ramana Kumar <> wrote:
>> in HOL definitions are just theorems (of the form |- foo x y z = blah
>> )... what makes them different in Coq?
>
> Well, the difference between a definition and a theorem in Coq is that
> a theorem needs a proof.
> _______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. On Wed, Sep 22, 2010 at 9:55 PM, Ramana Kumar <> wrote:
> definitions need proofs too (type correctness, termination (think of
> recursive functions)).

Yeah, any definition you write with Definition in Coq needs to type
check, and any definition you write with Fixpoint needs to type check
and also satisfy syntactic constraints on what Coq calls the
"decreasing argument" to show that it will terminate, but neither of
those are what Coq calls a Theorem, which needs to be followed with a
Proof. I'm using all those words (Definition, Theorem, Proof) in the
sense of Coq commands, so sorry for the confusion; I don't know how
those concepts map onto HOL.
_______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. Actually, in Coq both Definition and Theorem are the same thing. They
both need a type (or by Curry-Howard a proposition) and an
implementation (or by Curry-Howard a proof).

For example:
Definition x : forall a, a -> a := fun a -> a.

This has the type "forall a, a -> a" and the implementation "fun a ->
a". Or you could read it as the theorem "forall a, a -> a" with the
proof given by the arrow elimination rule (i.e. "fun a -> body") and
then invoking body.

If on the other hand you write:
Definition x : forall a, a -> a.
Proof. intros. trivial. Qed.

Then Coq runs the "intros" and "trivial" tactics to generate a lambda
term with with "forall a, a -> a".

To see this lambda term run "Print x".

Summary: Coq is just like HOL in this regard. (Though IIRC, there are
some technical differences where using Definition vs. Theorem give some
hints to Coq about which approach you intend to use.)

On 09/22/2010 10:14 PM, Lindsey Kuper wrote:
> On Wed, Sep 22, 2010 at 9:55 PM, Ramana Kumar<> wrote:
>> definitions need proofs too (type correctness, termination (think of
>> recursive functions)).
>
> Yeah, any definition you write with Definition in Coq needs to type
> check, and any definition you write with Fixpoint needs to type check
> and also satisfy syntactic constraints on what Coq calls the
> "decreasing argument" to show that it will terminate, but neither of
> those are what Coq calls a Theorem, which needs to be followed with a
> Proof. I'm using all those words (Definition, Theorem, Proof) in the
> sense of Coq commands, so sorry for the confusion; I don't know how
> those concepts map onto HOL.
> _______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. Steve Johnson wrote:
>
> Or if you are in a hurry, this example is worked out in Section 7.7 of
> my book.
>
It's protected, at least when I try from home. Any workaround?

thnx much - daniel On Wed, Sep 22, 2010 at 8:06 PM, Lindsey Kuper <> wrote:
> Ramana, it kind of seems like in Coq the "rewriting with definition
> of" steps are taken care of automatically by the "simpl" tactic.  I
> think you would only use the rewrite tactic with a theorem or an IH,

Yes, "rewrite" is only used for applying proofs of equality to rewrite
things. Whereas "simpl" and related tactics are for doing evaluation,
which includes replacing a variable by its definition.

As Michael mentions "definitions" and "theorems" are the same thing,
modulo Coq's messed up way of trying to do irrelevance via forbidding
the reduction of things. Srsly, the only difference between Coq's ten
billion names for defining things is whether the resulting definition
is opaque or translucent re evaluation. If there were a Coquette, it
would only have keywords for giving definitions of variables and for
giving definitions of (co)inductive types. If you really wanted to
keep the opaqueness around for some reason, you could push that into
the terms just like fix, cofix, fun,...

--
Live well,
~wren

_______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. HOL has a constant Abbrev, defined by "Abbrev x = x" but intended for
use when x is of the form "var = term", which the simplifier (i.e.
rewriter) doesn't expand underneath. This gives you a general form of
opaqueness, where you set up a temporary binding from var to term.
(You rewrite with the definition of Abbrev in a particular place
(which you can specify with a pattern) to make the var transparent, or
just make it disappear really.) I think this is somewhat like your
idea of using fix, cofix, etc.

Then there is also the notion of a parse-level abbreviation, which the
parser and pretty printer print one way, which might look like a
constant, but the real term underneath is something else. This will
always be completely transparent, since there isn't anything at the
term level to be opaque.

Finally, constants are by default opaque unless you include some
theorem about them in your call to the simplifier (or such a theorem
is in the automatic extendible set of rewrites). (Such a theorem could
be a "definition".)

On Thu, Sep 23, 2010 at 6:33 PM, wren ng thornton <> wrote:
> On Wed, Sep 22, 2010 at 8:06 PM, Lindsey Kuper <> wrote:
>> Ramana, it kind of seems like in Coq the "rewriting with definition
>> of" steps are taken care of automatically by the "simpl" tactic.  I
>> think you would only use the rewrite tactic with a theorem or an IH,
>
> Yes, "rewrite" is only used for applying proofs of equality to rewrite
> things. Whereas "simpl" and related tactics are for doing evaluation,
> which includes replacing a variable by its definition.
>
> As Michael mentions "definitions" and "theorems" are the same thing,
> modulo Coq's messed up way of trying to do irrelevance via forbidding
> the reduction of things. Srsly, the only difference between Coq's ten
> billion names for defining things is whether the resulting definition
> is opaque or translucent re evaluation. If there were a Coquette, it
> would only have keywords for giving definitions of variables and for
> giving definitions of (co)inductive types. If you really wanted to
> keep the opaqueness around for some reason, you could push that into
> the terms just like fix, cofix, fun,...
>
> --
> Live well,
> ~wren
>
> _______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. On Fri, Sep 24, 2010 at 12:17 AM, Steve Johnson <> wrote:
> I wonder if you could do it the other way around?  That is Reverse_snoc =
> Reverse_append.
> and then prove the distributive lemma based on associativity?

sounds plausible, although I haven't tried it... would you want a snoc
induction principle? (do you have one?)

>
> Ramana Kumar wrote:
>
> in HOL definitions are just theorems (of the form |- foo x y z = blah
> )... what makes them different in Coq?
>
> yes snoc_app is what you need if your reverse is defined like that.
> you could now prove your reverse equivalent to one defined in terms of
> append.
>
>
>
>
> _______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe.

I've been working through the second chapter of Software Foundations
(http://www.cis.upenn.edu/~bcpierce/sf/Lists.html) and I keep getting
stuck on proving this theorem:

Theorem distr_rev : forall l1 l2 : natlist,
rev (l1 ++ l2) = (rev l2) ++ (rev l1).

(In English: if you append two lists and reverse the result, it's the
same as if you had reversed them individually and then appended them
in the opposite order.)

I've tried induction on l1, induction on l2, various helper lemmas,
all to no avail. Anyone been able to solve this one yet and if so, do
you have any tips?

Lindsey
_______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. In HOL this is proved by induction on l1 (with l2 universally
quantified), then rewriting with definition of append, definition of
reverse, the fact that append to nil is identity, and the fact that
append is associative. I'm assuming the definitions are similar in Coq
(i.e. they look like standard functional programming language
definitions of append and reverse)...

show us the subgoals if you just do an induction on l1...

On Thu, Sep 23, 2010 at 7:21 AM, Lindsey Kuper <> wrote:
> I've been working through the second chapter of Software Foundations
> (http://www.cis.upenn.edu/~bcpierce/sf/Lists.html) and I keep getting
> stuck on proving this theorem:
>
> Theorem distr_rev : forall l1 l2 : natlist,
>  rev (l1 ++ l2) = (rev l2) ++ (rev l1).
>
> (In English: if you append two lists and reverse the result, it's the
> same as if you had reversed them individually and then appended them
> in the opposite order.)
>
> I've tried induction on l1, induction on l2, various helper lemmas,
> all to no avail.  Anyone been able to solve this one yet and if so, do
> you have any tips?
>
> Lindsey
> _______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. Finally got it. (Spoilers below if anyone's curious. The snoc_app
helper was the key.)

Ramana, it kind of seems like in Coq the "rewriting with definition
of" steps are taken care of automatically by the "simpl" tactic. I
think you would only use the rewrite tactic with a theorem or an IH,
not with a definition. I didn't end up using the fact that append is
associative, but only because reverse is defined in terms of "snoc",
not in terms of append.

Theorem app_nil_end : forall l : natlist,
l ++ [] = l.
Proof.
intros l. induction l as [ | n l'].
Case "l = nil".
reflexivity.
Case "l = cons n l'".
simpl. rewrite -> IHl'. reflexivity. Qed.

Lemma snoc_app : forall x y : natlist, forall z : nat,
snoc (x ++ y) z = x ++ snoc y z.
Proof.
intros x y z. induction x as [ | a d].
Case "x = nil".
simpl. reflexivity.
Case "x = cons a d".
simpl. rewrite <- IHd. reflexivity.
Qed.

Theorem distr_rev : forall l1 l2 : natlist,
rev (l1 ++ l2) = (rev l2) ++ (rev l1).
Proof.
intros l1 l2. induction l1 as [ | n1 l1'].
Case "l1 = nil".
simpl. rewrite -> app_nil_end. reflexivity.
Case "l1 = cons n1 l1'".
simpl.
rewrite -> IHl1'.
rewrite <- snoc_app.
reflexivity.
Qed.
_______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. in HOL definitions are just theorems (of the form |- foo x y z = blah
)... what makes them different in Coq?

yes snoc_app is what you need if your reverse is defined like that.
you could now prove your reverse equivalent to one defined in terms of append.

On Thu, Sep 23, 2010 at 10:06 AM, Lindsey Kuper <> wrote:
> Finally got it.  (Spoilers below if anyone's curious.  The snoc_app
> helper was the key.)
>
> Ramana, it kind of seems like in Coq the "rewriting with definition
> of" steps are taken care of automatically by the "simpl" tactic.  I
> think you would only use the rewrite tactic with a theorem or an IH,
> not with a definition.  I didn't end up using the fact that append is
> associative, but only because reverse is defined in terms of "snoc",
> not in terms of append.
>
> Theorem app_nil_end : forall l : natlist,
>  l ++ [] = l.
> Proof.
>  intros l. induction l as [ | n l'].
>  Case "l = nil".
>    reflexivity.
>  Case "l = cons n l'".
>    simpl. rewrite -> IHl'. reflexivity. Qed.
>
> Lemma snoc_app : forall x y : natlist, forall z : nat,
>  snoc (x ++ y) z = x ++ snoc y z.
> Proof.
>  intros x y z. induction x as [ | a d].
>  Case "x = nil".
>    simpl. reflexivity.
>  Case "x = cons a d".
>    simpl. rewrite <- IHd. reflexivity.
> Qed.
>
> Theorem distr_rev : forall l1 l2 : natlist,
>  rev (l1 ++ l2) = (rev l2) ++ (rev l1).
> Proof.
>  intros l1 l2. induction l1 as [ | n1 l1'].
>  Case "l1 = nil".
>    simpl. rewrite -> app_nil_end. reflexivity.
>  Case "l1 = cons n1 l1'".
>    simpl.
>    rewrite -> IHl1'.
>    rewrite <- snoc_app.
>    reflexivity.
> Qed.
> _______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. On Wed, Sep 22, 2010 at 8:27 PM, Ramana Kumar <> wrote:
> in HOL definitions are just theorems (of the form |- foo x y z = blah
> )... what makes them different in Coq?

Well, the difference between a definition and a theorem in Coq is that
a theorem needs a proof.
_______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. definitions need proofs too (type correctness, termination (think of
recursive functions)).
but that point aside, just think of "proof by definitional extension"
as a special proof procedure that lets you prove a theorem about a new
constant for free. then the "definition" you get out of that is just a
theorem like any other.

On Thu, Sep 23, 2010 at 11:50 AM, Lindsey Kuper <> wrote:
> On Wed, Sep 22, 2010 at 8:27 PM, Ramana Kumar <> wrote:
>> in HOL definitions are just theorems (of the form |- foo x y z = blah
>> )... what makes them different in Coq?
>
> Well, the difference between a definition and a theorem in Coq is that
> a theorem needs a proof.
> _______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. On Wed, Sep 22, 2010 at 9:55 PM, Ramana Kumar <> wrote:
> definitions need proofs too (type correctness, termination (think of
> recursive functions)).

Yeah, any definition you write with Definition in Coq needs to type
check, and any definition you write with Fixpoint needs to type check
and also satisfy syntactic constraints on what Coq calls the
"decreasing argument" to show that it will terminate, but neither of
those are what Coq calls a Theorem, which needs to be followed with a
Proof. I'm using all those words (Definition, Theorem, Proof) in the
sense of Coq commands, so sorry for the confusion; I don't know how
those concepts map onto HOL.
_______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. Actually, in Coq both Definition and Theorem are the same thing. They
both need a type (or by Curry-Howard a proposition) and an
implementation (or by Curry-Howard a proof).

For example:
Definition x : forall a, a -> a := fun a -> a.

This has the type "forall a, a -> a" and the implementation "fun a ->
a". Or you could read it as the theorem "forall a, a -> a" with the
proof given by the arrow elimination rule (i.e. "fun a -> body") and
then invoking body.

If on the other hand you write:
Definition x : forall a, a -> a.
Proof. intros. trivial. Qed.

Then Coq runs the "intros" and "trivial" tactics to generate a lambda
term with with "forall a, a -> a".

To see this lambda term run "Print x".

Summary: Coq is just like HOL in this regard. (Though IIRC, there are
some technical differences where using Definition vs. Theorem give some
hints to Coq about which approach you intend to use.)

On 09/22/2010 10:14 PM, Lindsey Kuper wrote:
> On Wed, Sep 22, 2010 at 9:55 PM, Ramana Kumar<> wrote:
>> definitions need proofs too (type correctness, termination (think of
>> recursive functions)).
>
> Yeah, any definition you write with Definition in Coq needs to type
> check, and any definition you write with Fixpoint needs to type check
> and also satisfy syntactic constraints on what Coq calls the
> "decreasing argument" to show that it will terminate, but neither of
> those are what Coq calls a Theorem, which needs to be followed with a
> Proof. I'm using all those words (Definition, Theorem, Proof) in the
> sense of Coq commands, so sorry for the confusion; I don't know how
> those concepts map onto HOL.
> _______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. Steve Johnson wrote:
>
> Or if you are in a hurry, this example is worked out in Section 7.7 of
> my book.
>
It's protected, at least when I try from home. Any workaround?

thnx much - daniel On Wed, Sep 22, 2010 at 8:06 PM, Lindsey Kuper <> wrote:
> Ramana, it kind of seems like in Coq the "rewriting with definition
> of" steps are taken care of automatically by the "simpl" tactic.  I
> think you would only use the rewrite tactic with a theorem or an IH,

Yes, "rewrite" is only used for applying proofs of equality to rewrite
things. Whereas "simpl" and related tactics are for doing evaluation,
which includes replacing a variable by its definition.

As Michael mentions "definitions" and "theorems" are the same thing,
modulo Coq's messed up way of trying to do irrelevance via forbidding
the reduction of things. Srsly, the only difference between Coq's ten
billion names for defining things is whether the resulting definition
is opaque or translucent re evaluation. If there were a Coquette, it
would only have keywords for giving definitions of variables and for
giving definitions of (co)inductive types. If you really wanted to
keep the opaqueness around for some reason, you could push that into
the terms just like fix, cofix, fun,...

--
Live well,
~wren

_______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. HOL has a constant Abbrev, defined by "Abbrev x = x" but intended for
use when x is of the form "var = term", which the simplifier (i.e.
rewriter) doesn't expand underneath. This gives you a general form of
opaqueness, where you set up a temporary binding from var to term.
(You rewrite with the definition of Abbrev in a particular place
(which you can specify with a pattern) to make the var transparent, or
just make it disappear really.) I think this is somewhat like your
idea of using fix, cofix, etc.

Then there is also the notion of a parse-level abbreviation, which the
parser and pretty printer print one way, which might look like a
constant, but the real term underneath is something else. This will
always be completely transparent, since there isn't anything at the
term level to be opaque.

Finally, constants are by default opaque unless you include some
theorem about them in your call to the simplifier (or such a theorem
is in the automatic extendible set of rewrites). (Such a theorem could
be a "definition".)

On Thu, Sep 23, 2010 at 6:33 PM, wren ng thornton <> wrote:
> On Wed, Sep 22, 2010 at 8:06 PM, Lindsey Kuper <> wrote:
>> Ramana, it kind of seems like in Coq the "rewriting with definition
>> of" steps are taken care of automatically by the "simpl" tactic.  I
>> think you would only use the rewrite tactic with a theorem or an IH,
>
> Yes, "rewrite" is only used for applying proofs of equality to rewrite
> things. Whereas "simpl" and related tactics are for doing evaluation,
> which includes replacing a variable by its definition.
>
> As Michael mentions "definitions" and "theorems" are the same thing,
> modulo Coq's messed up way of trying to do irrelevance via forbidding
> the reduction of things. Srsly, the only difference between Coq's ten
> billion names for defining things is whether the resulting definition
> is opaque or translucent re evaluation. If there were a Coquette, it
> would only have keywords for giving definitions of variables and for
> giving definitions of (co)inductive types. If you really wanted to
> keep the opaqueness around for some reason, you could push that into
> the terms just like fix, cofix, fun,...
>
> --
> Live well,
> ~wren
>
> _______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. On Fri, Sep 24, 2010 at 12:17 AM, Steve Johnson <> wrote:
> I wonder if you could do it the other way around?  That is Reverse_snoc =
> Reverse_append.
> and then prove the distributive lemma based on associativity?

sounds plausible, although I haven't tried it... would you want a snoc
induction principle? (do you have one?)

>
> Ramana Kumar wrote:
>
> in HOL definitions are just theorems (of the form |- foo x y z = blah
> )... what makes them different in Coq?
>
> yes snoc_app is what you need if your reverse is defined like that.
> you could now prove your reverse equivalent to one defined in terms of
> append.
>
>
>
>
> _______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe. On Thu, Sep 23, 2010 at 7:23 PM, Ramana Kumar <> wrote:
> On Fri, Sep 24, 2010 at 12:17 AM, Steve Johnson <> wrote:
>> I wonder if you could do it the other way around?  That is Reverse_snoc =
>> Reverse_append.
>> and then prove the distributive lemma based on associativity?
>
> sounds plausible, although I haven't tried it... would you want a snoc
> induction principle? (do you have one?)

Writing a snoc induction principle is actually a lot of fun (depending
on your definition of fun). In particular, there's an easy definition
which is horribly inefficient computationally, and then there's the
efficient version you'd write in a non-dependent language but it's
much harder to prove things about. (At least for the Vec version of
snoc induction; the List version might not be as interesting.)

--
Live well,
~wren

_______________________________________________
___________________________________________________

Posted on the PL-wonks mailing list. Go to http://www.cs.indiana.edu/mailman/listinfo/pl-wonks to subscribe.