Library ssrbool

A theory of boolean predicates and operators. A large part of this file   
 is concerned with boolean reflection. Definitions and notations:          


 

 a && b                  == boolean conjection                             
 a || b                  == boolean disjunction                            
 a ==> b                 == boolean implication                            
 ~~ a                    == boolean negation                               
 a (+) b                 == boolean xor                                    
 is_true                 == coercion bool >-> Prop                         
 reflect                 == the reflection inductive predicate             
 iffP,...                == user-oriented reflection lemmas                
 elimT                   == coercion reflect >-> Funclass, to apply        
                            reflection lemmas to boolean assertions        
 [ /\ P1 , P2 & P3 ]     == iterated logical conjonction, up to 5          
 [ \/ P1 , P2 | P3 ]     == iterated logical disjonction, up to 4          
 [&& a, b, c & d]        == iterated, right associated boolean conjunction 
                            with arbitrary arity                           
 [|| a, b, c | d]        == iterated, right associated boolean disjunction 
                            with arbitrary arity                           
 [==> a, b, c => d]      == iterated, right associated boolean             
                            implication with arbitrary arity               
 and3P,...               == specific reflection lemmas for iterated        
                            connectives                                    
 andTb, orbAC,...        == systematic names for boolean connective        
                            properties                                     
 prop_congr              == a tactic to move a boolean equality from       
                            its coerced form in Prop to the equality       
                            in bool                                        
 bool_congr              == resolution tactic for blindly weeding out      
                            like terms from boolean equalities (can fail)  


 

 This file provides a theory of boolean predicates and relations :         
   pred T                == T -> bool                                      
   simpl_pred T          == type of simplifying (see ssrfun) predicates    
   rel T                 == T -> pred T == T -> T -> bool                  
   simpl_rel T           == type of simplifying relations                  
   predType              == generic predicate interface,                   
                             implemented for lists, sets                   
 If P is a predicate the proposition "x satisfies P" can be written        
 applicatively as (P x), or using an explicit connective as (x \in P); in  
 the latter case we say that P is a "collective" predicate. We use A, B    
 rather than P, Q for collective predicates:                               
   x \in A               == x satisfies the (collective) predicate A       
   x \notin A            == x doesn't satisfy the (collective) predicate A 
 The pred T type can be used as a generic predicate type for either kind,  
 but the two kinds of predicates should not be mixed. Explicit values of   
 pred T (i.e., lamdba terms) should always be used applicatively, while    
 values of collection types implementing the predType interface, such as   
 lists or sets should always be used as collective predicates; simpl_pred  
 predicates are the only type that can be used either way (however, the    
 x \in A notation will not simplify). We provide the following conversions 
   SimplPred P           == a (simplifying) applicative equivalent of P    
   mem A                 == an applicative equivalent of A:                
                            mem A x simplifies to x \in A                  
 Alternatively one can use the syntax for explicit simplifying predicates  
 and relations:                                                            


 

 [pred x | E]            == simplifying (see ssrfun) predicate x => E      
 [pred x : T | E]        == predicate x => T, with a cast on the argument  
 [pred : T | E]          == constant predicate E on type T                 
 [pred x \in A]          == [pred x | x \in A]                             
 [pred x \in A | E]      == [pred x | (x \in A) && E]                      


 

 [predU A & B]           == union of two collective predicates             
 [predI A & B]           == intersection of collective predicates          
 [predD A & B]           == difference of collective predicates            
 [predC A]               == complement of a collective predicate           
 [preim f of A]          == preimage by f of the collective predicate A    
 predU P Q, ...          == union, etc of applicative predicates           
 pred0                   == the empty predicate                            
 predT                   == the total (always true) predicate              
                            if T : predArgType, then T coerces to predT    
 {: T}                   == T cast to predArgType (e.g., {: bool * nat})   


 

 [rel x y | E]           == simplifying relation                           
 [rel x y : T | E]       == relation, with a cast on the arguments         
 [rel x y \in A & B | E] == [rel x y | [&& x \in A, y \in B & E]]          
 [rel x y \in A & B]     == [rel x y | (x \in A) && (y \in B)]             
 [rel x y \in A | E]     == [rel x y \in A & A | E]                        
 [rel x y \in A]         == [rel x y \in A & A]                            
 relU R S                == union of relations R and S                     


 

 Some properties of predicates and relations:                              
 A =i B                  == A and B are extensionally equivalent           
 {subset A <= B}         == A is a (collective) subpredicate of B          
 subpred P Q             == P is an (applicative) subpredicate or Q        
 subrel R S              == R is a subrelation of S                        


 

 reflexive R             == R (in rel T) is reflexive                      
 irreflexive R           == R (in rel T) is irreflexive                    
 symmetric R             == R (in rel T) is symmetric (equational)         
 pre_symmetric R         == R (in rel T) is symmetric (implication)        
 antisymmetric R         == R (in rel T) is antisymmetric                  
 total R                 == R (in rel T) is total                          
 transitive R            == R (in rel T) is transitive                     
 left_transitive R       == R is a congruence on the left hand side of R   
 right_transitive R      == R is a congruence on the right hand side of R  


 

 Localization of (Prop) predicates; if P1 is convertible to forall x, Qx,  
 P2 to forall x y, Qxy and P3 to forall x y z, Qxyz :                      


 

 {for y, P1}            == Qx{y / x}                                       
 {in d, P1}             == forall x, x \in d -> Qx                         
 {in d1 & d2, P2}       == forall x y, x \in d1 -> y \in d2 -> Qxy         
 {in d &, P2}           == forall x y, x \in d -> y \in d -> Qxy           
 {in d1 & d2 &, Q3}     == forall x y z,                                   
                            x \in d1 -> y \in d2 -> z \in d2 -> Qxyz       
                            + Variants                                     
 {in d, bijective f}    == f has a right inverse in d                      
 {on cd, P1}            == forall x, (f x) \in cd -> Qx                    
                            when P1 is also convertible to Pf f            
 {on cd &, P2}          == forall x y, f x \in cd -> f y \in cd -> Qxy     
                            when P2 is also convertible to Pf f            
 {on cd, P1' & g}       == forall x, (f x) \in cd -> Qx                    
                            when P1' is convertible to Pf f and P1' g is   
                            convertible to forall x, Qx                    
 {on cd, bijective f}    == f has a right inverse on cd                    


 

 This file introduces the following suffix policy for lemma names:         
 A : associativity                                                         
 C : commutativity or set complement                                       
 D : set difference                                                        
 E : elimination                                                           
 F : boolean false                                                         
 I : set intersection                                                      
 K : cancellation                                                          
 N : boolean negation                                                      
 T : boolean truth                                                         
 U : set union                                                             
 W : weakening                                                             

We introduce a number of n-ary "list-style" notations, which share a 
 common format, namely                                                
    [op arg1, arg2, ... last_separator last_arg]                      
 This usually denotes a right-associative applications of op, e.g.,   
  [&& a, b, c & d] denotes a && (b && (c && d))                       
 The last_separator must be a non-operator token; here we use &, | or 
 => (our default is &, but we try to match the intended meaning of    
 op). The separator is a workaround for limitations of the parsing    
 engine; for similar reasons the separator cannot be omitted even     
 when last_arg can. The Notation declarations are complicated by the  
 separate treatments for fixed arities (binary for bool operators,    
 and all arities for Prop operators).                                 
   We also use the square brackets in comprehension-style notations   
 of the form                                                          
    [type var separator expr]                                         
 where "type" is the type of the comprehension (e.g., pred) and       
 separator is | or => . It is important that in other notations a      
 leading square bracket [ is always by an operator symbol or at least 
 a fixed identifier.                                                  

Shorter delimiter 

The Coq library forgets to set argument scopes on bool ops. 

An alternative to xorb that behaves somewhat better wrt simplification. 

Bool operator notation; we need to redeclare && and || so they get the 
 correct argument scopes.                                               

Coercion bool >-> Prop.                    

Lemmas for auto. 

Negation lemmas. 

Note: in the general we take NEGATION as the standard form of a 
 false condition : hypotheses should be of the form ~~ b rather  
 than b = false or ~ b, as much as possible.                     

Coercion of sum-style datatypes into bool, which makes it possible 
 to use ssr's boolean if rather than Coq's "generic" if.            

Lemmas for ifs with large conditions, which allow reasoning about the  
 condition without repeating it inside the proof (the latter IS         
 preferable when the condition is short).                               
 Usage :                                                                
   if the goal contains (if cond then ...) = ...                        
     case: ifP => Hcond.                                                
   generates two subgoal, with the assumption Hcond : cond = true/false 
     Rewrite if_same  eliminates redundant ifs                          
     Rewrite (fun_if f) moves a function f inside an if                 
     Rewrite if_arg moves an argument inside a function-valued if       

Patch for a bug in ssreflect 8.1 that corrupts patterns where a 
 wildcard appears under a match. Usage:                          
   rewrite -ifE; set x := if_expr _ _ _.                         

The reflection predicate.                                          

Core (internal) reflection lemmas, used for the three kinds of views. 

Internal negated reflection lemmas 

User-oriented reflection lemmas 

Allow the direct application of a reflection lemma to a boolean assertion.  

List notations for wider connectives; the Prop connectives have a fixed  
 width so as to avoid iterated destruction (we go up to width 5 for /\,   
 and width 4 for or. The bool connectives have arbitrary widths, but      
 denote expressions that associate to the RIGHT. This is consistent with  
 the right associativity of list expressions, and thus more convenient in 
 many proofs.                                                             

Shorter, more systematic names for the boolean connectives laws.       

Pseudo-cancellation -- i.e, absorbtion 

Imply 

addition (xor) 

Resolution tactic for blindly weeding out common terms from boolean       
 equalities. When faced with a goal of the form (andb/orb/addb b1 b2) = b3 
 they will try to locate b1 in b3 and remove it. This can fail!            

Predicates, i.e., packaged functions to bool.                  
   Indeed, pred T, the basic type for predicates over a type T, 
 is simply an alias for T -> bool.                              
   We actually distinguish two kinds of predicates, which we    
 applicative and collective, based on the syntax used to        
 specialize them to some value x in T:                          
  - For an applicative predicate P, one uses prefix syntax:     
        P x                                                     
    Also, most operations on applicative predicates us prefix   
    syntax as well (e.g., predI P Q).                           
  - For a collective predicate A, one uses infix syntax:        
        x \in A                                                 
    and all operations on collective predicates use infix       
    syntax as well (e.g., [predI A & B]).                       
 There are only two kinds of applicative predicates:            
  - pred T, the alias for T -> bool mentioned above             
  - simpl_pred T, an alias for simpl_fun T bool with a coercion 
    to pred T that auto-simplifies on application (see ssrfun). 
 On the other hand, the set of collective predicate types is    
 open-ended, via                                                
  - predType T, a Structure that can be used to put Canonical   
    collective predicate interpretation on other types, such    
    as lists, tuples, finite sets, etc.                         
 Indeed, we define such interpretations for both applicative    
 predicate types, which can therefore also be used with the     
 infix syntax, e.g. x \in predI P Q. Moreover these infix forms 
 are convertible to their prefix counterpart (e.g., predI P Q x 
 which in turn simplifies to P x && Q x).                       
   The converse is not true, however; collective predicate      
 types cannot, in general, be used applicatively, because of    
 the "uniform inheritance" restriction on implicit coercion.    
   However, we do define an explicit generic coercion           
  - mem : forall (pT : predType), pT -> mem_pred T              
    where mem_pred T is a variant of simpl_pred T that          
    preserves the infix syntax, i.e.,                           
       mem A x auto-simplifies to x \in A                       
 Indeed, the infix "collective" operators are notation for a    
 prefix operator with arguments of type mem_pred T or pred T,   
 applied to coerced collective predicates, e.g.,                
      Notation "x \in A" := (in_mem x (mem A)).                 
 This prevents the variability in the predicate type from       
 interfering with the application of generic lemmas. Moreover   
 this also makes it much easier to define generic lemmas,       
 because the simplest type -- pred T -- can be used as the type 
 of generic collective predicates, provided one takes care not  
 to use it applicatively; this avoids the burden of having to   
 declare a different predicate type for each predicate          
 parameter of each section or lemma.                            
   This trick is made possible by the fact that the constructor 
 of the mem_pred T type aligns the unification process, forcing 
 a generic "collective" predicate A : pred T to unify with the  
 actual collective B, which mem has coerced to pred T via an    
 internal, hidden implicit coercion, supplied by the predType   
 structure for B. Users should take care not to inadvertently   
 "strip" (mem B) down to the coerced B, since this will expose  
 the internal coercion: Coq will display a term B x that can't  
 be typed as such. The topredE lemma can be used to restore the 
 x \in B syntax in this case. While -topredE can conversely be  
 used to change x \in P into P x, it is safer to use the inE    
 and memE lemmas instead, as they do not run the risk of        
 exposing internal coercions. As a consequence, it is better to 
 explicitly cast a generic applicative pred T to simpl_pred,    
 using the SimplPred constructor, when it is used as a          
 collective predicate (see, e.g., Lemma eq_big in bigops.v).    
   We also sometimes "instantiate" the predType structure by    
 defining a coercion to the sort of the predPredType structure. 
 This works better for types such as set T that have subtypes   
 that coerce to them, since the same coercion will be inserted  
 by the application of mem. It also allows us to turn some      
 specific Types (namely, any aT : predArgType) into predicates, 
 specifically, the total predicate over that type, i.e.,        
 fun _ : aT => true. This allows us to write, e.g.,  #|'I_n|    
 for the cardinal of the (finite) type of integers less than n. 
   Collective predicates have a specific extensional equality,  
     - A =i B,                                                  
 while applicative predicates just use the extensional equality 
 of functions,                                                  
     - P =1 Q                                                   
 The two forms are convertible, however.                        
   We lift boolean operations to predicates, defining:          
  - predU (union), predI (intersection), predC (complement),    
    predD (difference), and preim (preimage, i.e., composition) 
 For each operation we define three forms, typically:           
   - predU : pred T -> pred T -> simpl_pred T                   
   - [predU A & B], a Notation for predU (mem A) (mem B)        
   - xpredU, a Notation for the lambda-expression inside predU, 
     which is mostly useful as an argument of =1, since it      
     exposes the head constant of the expression to the         
     ssreflect matching algorithm.                              
 The syntax for the preimage of a collective predicate A is     
   - [preim f of A]                                             
 Finally, the generic syntax for defining a simpl_pred T is     
   - [pred x : T | P(x)], [pred x | P(x)], [pred x \in A | P(x) 
 We also support boolean relations, but only the applicative    
 form, with types                                               
   - rel T, an alias for T -> pred T                            
   - simpl_rel T, an auto-simplifying version, and syntax       
     [rel x y | P(x,y)], [rel x y \in A & B | P(x,y)], etc.     
 The notation [rel of fA] can be used to coerce a function      
 returning a collective predicate to one returning pred T.      

This redundant coercion lets us "inherit" the simpl_predType canonical 
 structure by declaring a coercion to simpl_pred. This hack is the only 
 way to put a predType structure on a predArgType. We use simpl_pred    
 rather than pred to ensure that /= removes the identity coercion. Note 
 that the coercion will never be used directly for simpl_pred, since    
 the canonical structure should always resolve.                         

This lets us use some types as a synonym for their universal predicate. 
 Unfortunately, this won't work for existing types like bool, unless     
 we redefine bool, true, false and all bool ops.                         
   We don't define a coercion to Sortclass because then any coercion to  
 predArgType would always be in a conflict with a preexisting coercion   
 to Sortclass.                                                           

These must be defined outside a Section because "cooking" kills the 
 nosimpl tag.                                                        

Caveat: reflexive should not be used to state lemmas, since auto 
 and trivial will not expand the constant.                        

Property localization 

Weakening and monotonicity lemmas for localized predicates. 
 Note that using these lemmas in backward reasoning will     
 cause the expansion of the predicate definition, as Coq     
 needs to expose the quantifier to apply these lemmas. We    
 define some specialized variants to avoid this for some of  
 the ssrfun definitions.