The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

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).