The Coq mailing list

[Paul Tarau <paul.tarau AT gmail.com>]

In my original Haskell code hdN 0 = error and tlN 0 = error. So the Lemma
should be:

Lemma cons_hd_tl :
forall n, n>0 -> consN (hdN n) (tlN n) = n.

Paul

On Tue, Jul 13, 2010 at 5:32 AM, AUGER Cedric 
<Cedric.Auger AT lri.fr>
 wrote:
> Le Mon, 12 Jul 2010 18:07:54 -0500,
> Paul Tarau 
>Â <paul.tarau AT gmail.com>
>  a écrit :
>
>> Many thanks for your help (and also to Georges and Taral) -
>> everything works now resulting in a simple arithmetic theory of
>> cons,hd, tail:
>>
>> Require Import Bool.
>> Require Import Recdef.
>> Require Import Arith.
>>
>> Fixpoint evenN (n: nat) {struct n} : bool :=
>> match n with
>> | O => true
>> | S O => false
>> | S (S x) => evenN x
>> end.
>>
>> (* half, rounded up *)
>> Function halfUpN (n  : nat) : nat :=
>>  match n with
>>  | O => O
>>  | S O => S O
>>  | S (S x) => S (halfUpN x)
>>  end.
>> Lemma halfUpN_decrease :
>>  forall n, halfUpN n <= n.
>> Proof.
>>  intros n.
>>  functional induction (halfUpN n);
>>  auto with arith.
>> Qed.
>>
>> (* returns x such that 2^x*... = n *)
>> Function hdN (n:nat) {measure (fun n => n) n} : nat :=
>> match n with
>> | O => O
>> | S x => if evenN x then O else S (hdN (halfUpN x))
>> end.
>> Proof.
>>  intros n n' H1 H2.
>>  apply le_lt_trans with n'.
>>  apply halfUpN_decrease.
>>  auto with arith.
>> Defined.
>>
>> (* returns y, such that 2^...(2*y+1) = n *)
>> Function tlN (n:nat) {measure (fun n => n) n} : nat :=
>> match n with
>> | O => O
>> | S x => if evenN x then halfUpN x else tlN (halfUpN x)
>> end.
>> Proof.
>>  intros n n' H1 H2.
>>  apply le_lt_trans with n'.
>>  apply halfUpN_decrease.
>>  auto with arith.
>> Defined.
>>
>> Fixpoint plusN (n m : nat) {struct n} : nat :=
>> match n with
>> | O => m
>> | (S x) => S (plusN x m)
>> end.
>>
>> Definition doubleN (n:nat) : nat := plusN n n.
>>
>> Fixpoint multN (n m: nat) : nat :=
>> match n with
>> | O => O
>> | S x => plusN m (multN x m)
>> end.
>>
>> Fixpoint exp2 (n:nat) {struct n} : nat :=
>> match n with
>> | O => S O
>> | S n => doubleN (exp2 n)
>> end.
>>
>> (* reverses the effect of hdN and tlN i.e. consN (hdN n) (tlN n) is n
>> *) Definition consN (x y : nat) : nat := multN (exp2 x) (S (doubleN
>> y)).
>>
>> My next challenge is to prove "list-like" properties, for instance:
>>
>> Fixpoint eqN (n m:nat) {struct n} : Prop :=
>> match n,m with
>> | O, O => True
>> | O, S _ => False
>> | S _, O => False
>> | S x, S y => eqN x y
>> end.
>>
>> Lemma cons_hd_tl :
>> forall n, eqN n (consN (hdN n) (tlN n)).
>>
>> In this case is it a good idea to define eqN by structural
>> induction or the built-in "=" relation should be used?
>>
>> Paul
>>
>
> Some piece of advice, don't rush with such definitions:
> I suspect there is some glich in your cons_hd_tl:
> If I am right,
> . tlN 0 = 0
> . hdN 0 = 0
> . consN 0 0 = 1
> but 0 is not 1.
>
> In fact, your specification of tlN is wrong:
> there is no y such that there is x such that
>  x
> 2.(2.y+1) = 0
> and you write that y works in your definition.
>
> So you should adapt your lemma, to make it provable
> (or find inconsistency in Coq).
>