Library ssrfun

This file contains the basic definitions and notations for working with   
 functions. The definitions concern:                                       


 

  Pair projections                                                         
    p.1  == first element of a pair                                        
    p.2  == second element of a pair                                       


 

  Simplifying functions, beta-reduced by simpl and /= :                    
           [fun : T => E] == constant function from type T that returns E  
             [fun x => E] == unary function                                
         [fun x : T => E] == unary function with explicit domain type      
           [fun x y => E] == binary function                               
       [fun x y : T => E] == binary function with explicit domain type     
     [fun (x : T) y => E] == binary function with explicit domain type     
     [fun x (y : T) => E] == binary function with explicit domain type     
 [fun (x : xT) (y : yT) => E]                                              
 - partial functions using option type,                                    
     oapp f d ox == if ox is Some x returns f x,        d otherwise        
      odflt d ox == if ox is Some x returns x,          d otherwise        
      obind f ox == if ox is Some x returns f x,        None otherwise     
       omap f ox == if ox is Some x returns Some (f x), None otherwise     
 - singleton types,                                                        
  all_equal_to x0 == x0 is the only value in its type, so any such value   
                     can be rewritten to x0.                               
 - a generic wrapper type,                                                 
       wrapped T == the inductive type with values Wrap x for x : T        
        unwrap w == the projection of w : wrapped T on T                   
          wrap x == the canonical injection of x : T into wrapped T; it is 
                    equivalent to Wrap x, but is declared as a (default)   
                    Canonical Structure, which lets the Coq HO unification 
                    automatically expand x into unwrap (wrap x). The delta 
                    reduction of wrap x to Wrap can be exploited to        
                    introduce controlled nondeterminism in Canonical       
                    Structure inference, as in the implementation of       
                    the mxdirect predicate in matrix.v.                    
 - identity functions                                                      
    id           == NOTATION for the explicit identity function fun x => x 
    @id T        == notation for the explicit identity at type T           
    idfun        == a constant whose definition is the identity function   
    phant_id x y == the function type phantom _ x -> phantom _ y           
In addition to their casual use in functional programming, identity

 functions are often used to trigger static unification as part of the     
 construction of dependent Records and Structures. For example, if we need 
 a structure sT over a type T, we take as arguments T, sT, and a "dummy"   
 function T -> sort sT:                                                    
   Definition foo T sT & T -> sort sT := ...                               
 We can avoid specifying sT directly by calling foo (@id T), or specify    
 the call completely while still ensuring the consistency of T and sT, by  
 calling @foo T sT idfun. The phant_id type allows us to extend this trick 
 to non-Type canonical projections. It also allows us to sidestep          
 dependent type constraints when building explicit records, e.g., given    
    Record r := R { x; y : T(x)}.                                          
 if we need to build an r from a given y0 while inferring some x0, such    
 that y0 : T(x0), we pose                                                  
    Definition mk_r .. y .. (x := ...) y' & phant_id y y' := R x y'.       
 Calling @mk_r .. y0 .. id will cause Coq to use y' := y0, while checking  
 the dependent type constraint y0 : T(x0).                                 
 - extensional equality for functions and relations (i.e. functions of two 
   arguments),                                                             
    f1 =1 f2      ==  f1 x is equal to f2 x forall x                       
    f1 =1 f2 :> A ==    ... and f2 is explicitly typed                     
    f1 =2 f2      ==  f1 x y is equal to f2 x y forall x y                 
    f1 =2 f2 :> A ==    ... and f2 is explicitly typed                     
 - composition for total and partial functions,                            
            f^~ y == function f with y as second argument y                
                     caveat: conditional (non-maximal) implicit arguments  
                     of f are NOT inserted in this context                 
        f1 \o f2  == composition of f1 and f2                              
                     note: (f1 \o f2) x simplifies to f1 (f2 x)            
      pcomp f1 f2 == composition of partial functions f1 and f2            
 - properties of functions                                                 
      injective f == f is injective                                        
       cancel f g == g is a left inverse of f / f is a right inverse of g  
      pcancel f g == g is a left inverse of f where g is partial           
      ocancel f g == g is a left inverse of f where f is partial           
      bijective f == f is bijective (has a left and right inverse)         
       involutive f == f is involutive                                     
 - properties for operations                                               
              left_id e op == e is a left identity for op                  
             right_id e op == e is a right identity for op                 
       left_inverse e i op == i is a left inverse for op with identity e   
      right_inverse e i op == i is a right inverse for op with identity e  
         self_inverse e op == each x is its own op-inverse (op x x = e)    
             idempotent op == op is idempotent for op                      
              associate op == op is associative                            
            commutative op == op is commutative                            
       left_commutative op == op is left commutative                       
      right_commutative op == op is right commutative                      
            left_zero z op == z is a right zero for op                     
           right_zero z op == z is a right zero for op                     
  left_distributive op add == op distributes over add to the left          
 right_distributive op add == op distributes over add to the right         
         left_injective op == op is injective in its left argument         
        right_injective op == op is injective in its right argument        
          left_loop inv op == op, inv obey the inverse loop left axiom:    
                              op (inv x) (op x y) = y for all x, y, i.e.,  
                              op (inv x) is always a left inverse of op x  
      rev_left_loop inv op == op, inv obey the inverse loop reverse left   
                              axiom: op x (op (inv x) y) = y, for all x, y 
         right_loop inv op == op, inv obey the inverse loop right axiom:   
                              op (op x y) (inv y) = x for all x, y         
     rev_right_loop inv op == op, inv obey the inverse loop reverse right  
                              axiom: op (op x y) (inv y) = x for all x, y  
   Note that familiar "cancellation" identities like x + y - y = x or      
 x - y + x = x are respectively instances of right_loop and rev_right_loop 
 The corresponding lemmas will use the K and KV suffixes, respectively.    
 - morphisms for functions and relations,                                  
  {morph f : x / a >-> r } == f is a morphism with respect to functions    
                                 (fun x => a) and (fun x => r)             
  {morph f : x / a } == f is a morphism with respect to (fun x => a)       
  {morph f : x y / a >-> r } == f is a morphism with respect to functions  
                                 (fun x y => a) and (fun x y => r)         
  {morph f : x y / a } == f is a morphism with respect to (fun x y => a)   


 

 The file also contains some basic lemmas for the above concepts.          

Notations for pair projections 

Reserved notations for evaluation 

Reserved notations for subscripting and superscripting 

Complements on the option type constructor, used below to  
 encode partial functions.                                  

Syntax for defining auxiliary recursive function.          
  Usage:                                                    
 Section FooDefinition.                                     
 Variables (g1 : T1) (g2 : T2).  (globals)                  
 Fixoint foo_auxiliary (a3 : T3) ... :=                     
        body, using [rec e3, ...] for recursive calls       
 where "[ 'rec' a3 , a4 , ... ]" := foo_auxiliary.          
 Definition foo x y .. := [rec e1, ...].                    
 + proofs about foo                                         
 End FooDefinition.                                         

Definitions and notation for explicit functions with simplification,     
 i.e., which simpl and /= beta expand (this is complementary to nosimpl). 

For delta functions in eqtype.v. 

Shorthand for some basic equality lemmas. 

Force at least one implicit when used as a view. 

A predicate for singleton types.                                        

A generic wrapper type 

Extensional equality, for unary and binary functions, including syntactic 
 sugar.                                                                    

In an intuitionistic setting, we have two degrees of injectivity. The     
 weaker one gives only simplification, and the strong one provides a left  
 inverse (we show in `fintype' that they coincide for finite types).       
 We also define an intermediate version where the left inverse is only a   
 partial function.                                                         

rT must come first so we can use @ to mitigate the Coq 1st order   
 unification bug (e..g., Coq can't infer rT from a "cancel" lemma). 

cancellation lemmas for dependent type casts.