Library eqtype

This file defines two "base" combinatorial interfaces:                  
    eqType == the structure for types with a decidable equality          
 subType p == the structure for types isomorphic to {x : T | p x} with   
              p : pred T for some type T                                 
 The eqType interface supports the following operations:                 
          x == y <=> x compares equal to y (this is a boolean test)      
     x == y :> T <=> x == y at type T                                    
          x != y <=> x and y compare unequal                             
     x != y :> T <=>  "    "      "    "     at type T                   
         x =P y  <=> a proof of reflect (x = y) (x == y); this coerces   
                     to x == y -> x = y.                                 
             pred1 a == the singleton predicate [pred x | x == a]        
 pred2, pred3, pred4 == pair, triple, quad predicates                    
            predC1 a == [pred x | x != a]                                
      [predU1 a & A] == [pred x | (x == a) || (x \in A)]                 
      [predD1 A & a] == [pred x | (x != a) && (x \in A)]                 
  predU1 a P, predD1 P a == applicative versions of the above            
              frel f == the relation associated with f : T -> T          
                     := [rel x y | f x == y]                             
       invariant k f == elements of T whose k-class is f-invariant       
                     := [pred x | k (f x) == k x] with f : T -> T        
  [fun x : T => e0 with a1 |-> e1, .., a_n |-> e_n]                      
  [eta f with a1 |-> e1, .., a_n |-> e_n] ==                             
    the auto-expanding function that maps x = a_i to e_i, and other      
    values of x to e0 (resp. f x). In the first form the : T is optional 
    and x can occur in a_i or e_i.                                       
 Equality on an eqType is proof-irrelevant (lemma eq_irrelevance).       
   The eqType interface is implemented for most standard datatypes:      
  bool, unit, void, option, prod (denoted A * B), sum (denoted A + B),   
  sig (denoted {x | P}), sigT (denoted {i : I & T}).                     
   The fields of sig, sig2, and sigT are renamed sval, svalP, s2val,     
 s2valP, s2valP', tag, and tagged, respectively. We also define          
   Tagged T_ x == eta-friendly constructor for {i : I | T_ i}, x : T_ i  
   tagged_as u v == v cast as T_(tag u) if tag v == tag u, else u        
     thus, u == v <=> (tag u == tag v) && (tagged u == tagged_as u v)    
 The subType interface supports the following operations:                
      val == the generic injection from a subType S of T into T          
             e.g., if u : {x : T | P}, then val u : T                    
             val is injective because P is proof-irrelevant (P is in     
             bool, and the is_true coercion expands to P = true).        
     valP == the generic proof of P (val u) for u : subType P            
 Sub x Px == the generic constructor for a subType P; Px is a proof of   
             P x and P should be infered from the expected return type.  
  insub x == the generic partial projection of T into a subType S of T   
             This returns an option S; if S : subType P then             
                insub x = Some u with val u = x if P x,                  
                          None if ~~ P x                                 
             The insubP lemma encapsulates this dichotomy.               
             P should be infered from the expected return type.          
  innew x == total (non-option) variant of insub when P = predT          
 {? x | P} == option {x | P} (syntax for casting insub x)                
 insubd u0 x == the generic projection with default value u0             
             == odflt u0 (insub x)                                       
 insigd A0 x == special case of insubd for S == {x | x \in A}, where     
                A0 is a proof of x0 \in A.                               
 insub_eq x == transparent version of insub x that expands to Some/None  
               when P x can evaluate.                                    
  The subType interface is most often implemented using one of:          
   [subType for S_val by Srect]                                          
     where S_val : S -> T is a field accessor of a Record type S that is 
     isomorphic to {x : T | P} and Srect is the induction principle      
     automatically generated by the Coq Inductive or Record commands.    
   [newType for S_val by Srect]                                          
     variant of the above when S is a wrapper type for T (so P = predT)  
   [subType for S_val], [subType for S_val, S], [subType of S]           
     clone the canonical subType structure for S; if S_val is specified  
     then it replaces the inferred injection function.                   
 Subtypes inherit the eqType structure of their base types; the generic  
 structure should be explicitly instantiated using the                   
   [eqMixin of S by <:]                                                  
 construct to declare the Equality mixin; this pattern is repeated for   
 all the combinatorial interfaces (Choice, Countable, Finite).           
   More generally, the eqType structure can be transfered by (partial)   
 injections, using InjEqMixin, PcanEqMixin, or CanEqMixin.               

We use the module system to circumvent a silly limitation that  
 forbids using the same constant to coerce to different targets. 

Comparison for booleans. 

Equality-based predicates.       

Lemmas for reflected equality and functions.   

The invariant of an function f wrt a projection k is the pred of points 
 that have the same projection as their image.                           

Various EqType constructions.                                         

Prenex Implicits and renaming. 

Shorthand for the return type of insub. 

Because the standard prologue of Coq declares { x ... } with x   
 at level 99, we can't give shorthand for {x | x \in A}, however. 

A variant of injection with default that infers a collective predicate 
 from the membership proof for the default value.                       

There should be a rel definition for the subType equality op, but this 
 seems to cause the simpl tactic to diverge on expressions involving == 
 on 4+ nested subTypes in a "strict" position (e.g., after ~~).         
 Definition feq f := [rel x y | f x == f y].