The Coq mailing list

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

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

On Mon, Jul 12, 2010 at 1:59 PM, julien forest 
<forest AT ensiie.fr>
 wrote:
> Hi,
>
> On Mon, 12 Jul 2010 11:56:38 -0500
> Paul Tarau 
>Â <paul.tarau AT gmail.com>
>  wrote:
>
>> An interesting thing with this functional induction version is that
>> when trying something like:
>>
>> Eval compute in buggy 360.
>>
>> Coq 8.1pl2 on a Mac returns
>>
>> =1 (incorrectly)
>
> No, this is correct.
>
> Try this command to see the unfolding of the function definition and
> evaluation:
>
> Goal buggy 360 = 1.
> rewrite buggy_equation. (* first recursion on 359 *)
> simpl.
> rewrite buggy_equation. (* second recursion on (half 359) -1 i.e. 178
> which is even *)
> simpl.
>
> Qed.
>
>>
>> while
>>
>> Coq 8.2 (February 2009) on a Mac returns
>>
>>    = let (v, _) := buggy_terminate 360 in v
>>      : nat
>>
>> which, I suppose needs to be further reduced or it just states
>> "I do not know what the value is but I know it will terminate".
>>
> My mistake, you should end the proof after the definition of buggy by
> Defined and not Qed.
>
>> Does 8.3 beta work correctly on such functional induction examples?
> yes of course. In fact, they have been defined using coq trunk.
>
>
> Best regards,
> Julien.
>