Proposition for a almost-bitsize-independent Int31.v (joint work with J. Vouillon)

As said at the beginning of the file: 

  This file contains basic definitions of a 31-bit integer
  arithmetic. In fact it is more general than that. The only reason
  for this use of 31 is the underlying mecanism for hardware-efficient
  computations by A. Spiwack. Apart from this, a switch to, say,
  63-bit integers is now just a matter of replacing every occurences
  of 31 by 63. This is actually made possible by the use of
  dependently-typed n-ary constructions for the inductive type
  [int31], its constructor [I31] and any pattern matching on it.
  If you modify this file, please preserve this genericity. 

From the user point-of-view, almost nothing has changed: functions
like On, In, shiftr, shiftl and a few others now have a
syntactically-different definition, but thanks to Eval compute in their
definition, this leads to the exact same coq objects as before. The only
difference is "Check I31" that shows the compact n-ary version 
(nfun digits 31 int31) instead of (digits -> ... -> digits -> int31).
But even "Print int31" shows the same answer as before (the above type
of I31 is shown after expansion). 

Arnaud, could you check whether all this works fine with your
retroknowledge ?

Notice the new file NaryFunction that contain generic stuff about
n-ary dependent functions. It should end some day in another place
than theories/Numbers, but I cant figure where for now. This file is
also quite skinny yet, but it's a start.




git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10967 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 142 insertions, 0 deletions

diff --git a/theories/Numbers/NaryFunctions.v b/theories/Numbers/NaryFunctions.v
new file mode 100644
index 000000000..feb7a4916
--- /dev/null
+++ b/theories/Numbers/NaryFunctions.v
@@ -0,0 +1,142 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*          Pierre Letouzey, Jerome Vouillon, PPS, Paris 7, 2008        *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+Open Local Scope type_scope.
+
+Require Import List.
+
+(** * Generic dependently-typed operators about [n]-ary functions *)
+
+(** The type of [n]-ary function: [nfun A n B] is 
+    [A -> ... -> A -> B] with [n] occurences of [A] in this type. *)
+
+Fixpoint nfun A n B := 
+ match n with
+  | O => B 
+  | S n => A -> (nfun A n B)
+ end. 
+
+Notation " A ^^ n --> B " := (nfun A n B)
+ (at level 50, n at next level) : type_scope.
+
+(** [napply_cst _ _ a n f] iterates [n] times the application of a 
+    particular constant [a] to the [n]-ary function [f]. *)
+
+Fixpoint napply_cst (A B:Type)(a:A) n : (A^^n-->B) -> B :=
+ match n return (A^^n-->B) -> B with
+  | O => fun x => x
+  | S n => fun x => napply_cst _ _ a n (x a)
+ end.
+
+
+(** A generic transformation from an n-ary function to another one.*)
+
+Fixpoint nfun_to_nfun (A B C:Type)(f:B -> C) n : 
+ (A^^n-->B) -> (A^^n-->C) :=
+ match n return (A^^n-->B) -> (A^^n-->C) with 
+  | O => f
+  | S n => fun g a => nfun_to_nfun _ _ _ f n (g a)
+ end.
+
+(** [napply_except_last _ _ n f] expects [n] arguments of type [A], 
+    applies [n-1] of them to [f] and discard the last one. *) 
+
+Definition napply_except_last (A B:Type) := 
+ nfun_to_nfun A B (A->B) (fun b a => b).
+
+(** [napply_then_last _ _ a n f] expects [n] arguments of type [A], 
+    applies them to [f] and then apply [a] to the result. *) 
+
+Definition napply_then_last (A B:Type)(a:A) := 
+ nfun_to_nfun A (A->B) B (fun fab => fab a).
+
+(** [napply_discard _ b n] expects [n] arguments, discards then, 
+    and returns [b]. *)
+
+Fixpoint napply_discard (A B:Type)(b:B) n : A^^n-->B :=
+ match n return A^^n-->B with 
+  | O => b
+  | S n => fun _ => napply_discard _ _ b n
+ end.
+
+(** A fold function *)
+
+Fixpoint nfold A B (f:A->B->B)(b:B) n : (A^^n-->B) := 
+ match n return (A^^n-->B) with 
+  | O => b
+  | S n => fun a => (nfold _ _ f (f a b) n)
+ end.
+
+
+(** [n]-ary products : [nprod A n] is [A*...*A*unit], 
+  with [n] occurrences of [A] in this type. *)
+
+Fixpoint nprod A n : Type := match n with 
+ | O => unit
+ | S n => (A * nprod A n)%type
+end.
+
+Notation "A ^ n" := (nprod A n) : type_scope.
+
+(** [n]-ary curryfication / uncurryfication *)
+
+Fixpoint ncurry (A B:Type) n : (A^n -> B) -> (A^^n-->B) := 
+  match n return (A^n -> B) -> (A^^n-->B) with 
+  | O => fun x => x tt
+  | S n => fun f a => ncurry _ _ n (fun p => f (a,p))
+  end.
+
+Fixpoint nuncurry (A B:Type) n : (A^^n-->B) -> (A^n -> B) := 
+ match n return (A^^n-->B) -> (A^n -> B) with
+  | O => fun x _ => x
+  | S n => fun f p => let (x,p) := p in nuncurry _ _ n (f x) p
+ end.
+
+(** Earlier functions can also be defined via [ncurry/nuncurry]. 
+    For instance : *)
+
+Definition nfun_to_nfun_bis A B C (f:B->C) n :
+ (A^^n-->B) -> (A^^n-->C) := 
+ fun anb => ncurry _ _ n (fun an => f ((nuncurry _ _ n anb) an)).
+
+(** We can also us it to obtain another [fold] function, 
+    equivalent to the previous one, but with a nicer expansion
+    (see for instance Int31.iszero). *)
+
+Fixpoint nfold_bis A B (f:A->B->B)(b:B) n : (A^^n-->B) := 
+ match n return (A^^n-->B) with 
+  | O => b
+  | S n => fun a => 
+      nfun_to_nfun_bis _ _ _ (f a) n (nfold_bis _ _ f b n)
+ end.
+
+(** From [nprod] to [list] *)
+
+Fixpoint nprod_to_list (A:Type) n : A^n -> list A := 
+ match n with 
+  | O => fun _ => nil
+  | S n => fun p => let (x,p) := p in x::(nprod_to_list _ n p)
+ end.
+
+(** From [list] to [nprod] *)
+
+Fixpoint nprod_of_list (A:Type)(l:list A) : A^(length l) := 
+ match l return A^(length l) with 
+  | nil => tt
+  | x::l => (x, nprod_of_list _ l)
+ end.
+
+(** This gives an additional way to write the fold *)
+
+Definition nfold_list (A B:Type)(f:A->B->B)(b:B) n : (A^^n-->B) := 
+  ncurry _ _ n (fun p => fold_right f b (nprod_to_list _ _ p)).
+