Library Coq.ssr.ssrbool




Require Bool.
Require Import ssreflect ssrfun.

A theory of boolean predicates and operators. A large part of this file is concerned with boolean reflection. Definitions and notations: is_true b == the coercion of b : bool to Prop (:= b = true). This is just input and displayed as `b''. reflect P b == the reflection inductive predicate, asserting that the logical proposition P : prop with the formula b : bool. Lemmas asserting reflect P b are often referred to as "views". iffP, appP, sameP, rwP :: lemmas for direct manipulation of reflection views: iffP is used to prove reflection from logical equivalence, appP to compose views, and sameP and rwP to perform boolean and setoid rewriting. elimT :: coercion reflect >-> Funclass, which allows the direct application of `reflect' views to boolean assertions. decidable P <-> P is effectively decidable (:= {P} + {~ P}. contra, contraL, ... :: contraposition lemmas. altP my_viewP :: natural alternative for reflection; given lemma myviewP: reflect my_Prop my_formula, have [myP | not_myP] := altP my_viewP. generates two subgoals, in which my_formula has been replaced by true and false, resp., with new assumptions myP : my_Prop and not_myP: ~~ my_formula. Caveat: my_formula must be an APPLICATION, not a variable, constant, let-in, etc. (due to the poor behaviour of dependent index matching). boolP my_formula :: boolean disjunction, equivalent to altP (idP my_formula) but circumventing the dependent index capture issue; destructing boolP my_formula generates two subgoals with assumtions my_formula and ~~ myformula. As with altP, my_formula must be an application. \unless C, P <-> we can assume property P when a something that holds under condition C (such as C itself). := forall G : Prop, (C -> G) -> (P -> G) -> G. This is just C \/ P or rather its impredicative encoding, whose usage better fits the above description: given a lemma UCP whose conclusion is \unless C, P we can assume P by writing: wlog hP: / P by apply/UCP; (prove C -> goal). or even apply: UCP id _ => hP if the goal is C. classically P <-> we can assume P when proving is_true b. := forall b : bool, (P -> b) -> b. This is equivalent to ~ (~ P) when P : Prop. implies P Q == wrapper variant type that coerces to P -> Q and can be used as a P -> Q view unambigously. Useful to avoid spurious insertion of <-> views when Q is a conjunction of foralls, as in Lemma all_and2 below; conversely, avoids confusion in apply views for impredicative properties, such as \unless C, P. Also supports contrapositives. a && b == the boolean conjunction of a and b. a || b == the boolean disjunction of a and b. a ==> b == the boolean implication of b by a. ~~ a == the boolean negation of a. a (+) b == the boolean exclusive or (or sum) of a and b. [ /\ P1 , P2 & P3 ] == multiway logical conjunction, up to 5 terms. [ \/ P1 , P2 | P3 ] == multiway logical disjunction, up to 4 terms. [&& a, b, c & d] == iterated, right associative boolean conjunction with arbitrary arity. [|| a, b, c | d] == iterated, right associative boolean disjunction with arbitrary arity. [==> a, b, c => d] == iterated, right associative boolean implication with arbitrary arity. and3P, ... == specific reflection lemmas for iterated connectives. andTb, orbAC, ... == systematic names for boolean connective properties (see suffix conventions below). 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 == the type of bool predicates (:= T -> bool). simpl_pred T == the type of simplifying bool predicates, using the simpl_fun from ssrfun.v. rel T == the type of bool relations. := T -> pred T or T -> T -> bool. simpl_rel T == type of simplifying relations. predType == the generic predicate interface, supported for for lists and sets. pred_class == a coercion class for the predType projection to pred; declaring a coercion to pred_class is an alternative way of equipping a type with a predType structure, which interoperates better with coercion subtyping. This is used, e.g., for finite sets, so that finite groups inherit the membership operation by coercing to 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 confused. When a "generic" pred T value of one type needs to be passed as the other the following conversions should be used explicitly: 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 (in the following x is bound in E): [pred x | E] == simplifying (see ssrfun) predicate x => E. [pred x : T | E] == predicate x => E, with a cast on the argument. [pred : T | P] == constant predicate P on type T. [pred x | E1 & E2] == [pred x | E1 && E2]; an x : T cast is allowed. [pred x in A] == [pred x | x in A]. [pred x in A | E] == [pred x | x in A & E]. [pred x in A | E1 & E2] == [pred x in A | E1 && E2]. [predU A & B] == union of two collective predicates A and B. [predI A & B] == intersection of collective predicates A and B. [predD A & B] == difference of collective predicates A and B. [predC A] == complement of the collective predicate A. [preim f of A] == preimage under 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}) In the following, x and y are bound in E: [rel x y | E] == simplifying relation x, y => E. [rel x y : T | E] == simplifying relation with arguments cast. [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. Explicit values of type pred T (i.e., lamdba terms) should always be used applicatively, while values of collection types implementing the predType interface, such as sequences or sets should always be used as collective predicates. Defined constants and functions of type pred T or simpl_pred T as well as the explicit simpl_pred T values described below, can generally be used either way. Note however that x \in A will not auto-simplify when A is an explicit simpl_pred T value; the generic simplification rule inE must be used (when A : pred T, the unfold_in rule can be used). Constants of type pred T with an explicit simpl_pred value do not auto-simplify when used applicatively, but can still be expanded with inE. This behavior can be controlled as follows: Let A : collective_pred T := [pred x | ... ]. The collective_pred T type is just an alias for pred T, but this cast stops rewrite inE from expanding the definition of A, thus treating A into an abstract collection (unfold_in or in_collective can be used to expand manually). Let A : applicative_pred T := [pred x | ... ]. This cast causes inE to turn x \in A into the applicative A x form; A will then have to unfolded explicitly with the /A rule. This will also apply to any definition that reduces to A (e.g., Let B := A). Canonical A_app_pred := ApplicativePred A. This declaration, given after definition of A, similarly causes inE to turn x \in A into A x, but in addition allows the app_predE rule to turn A x back into x \in A; it can be used for any definition of type pred T, which makes it especially useful for ambivalent predicates as the relational transitive closure connect, that are used in both applicative and collective styles. Purely for aesthetics, we provide a subtype of collective predicates: qualifier q T == a pred T pretty-printing wrapper. An A : qualifier q T coerces to pred_class and thus behaves as a collective predicate, but x \in A and x \notin A are displayed as: x \is A and x \isn't A when q = 0, x \is a A and x \isn't a A when q = 1, x \is an A and x \isn't an A when q = 2, respectively. [qualify x | P] := Qualifier 0 (fun x => P), constructor for the above. [qualify x : T | P], [qualify a x | P], [qualify an X | P], etc. variants of the above with type constraints and different values of q. We provide an internal interface to support attaching properties (such as being multiplicative) to predicates: pred_key p == phantom type that will serve as a support for properties to be attached to p : pred_class; instances should be created with Fact/Qed so as to be opaque. KeyedPred k_p == an instance of the interface structure that attaches (k_p : pred_key P) to P; the structure projection is a coercion to pred_class. KeyedQualifier k_q == an instance of the interface structure that attaches (k_q : pred_key q) to (q : qualifier n T). DefaultPredKey p == a default value for pred_key p; the vernacular command Import DefaultKeying attaches this key to all predicates that are not explicitly keyed. Keys can be used to attach properties to predicates, qualifiers and generic nouns in a way that allows them to be used transparently. The key projection of a predicate property structure such as unsignedPred should be a pred_key, not a pred, and corresponding lemmas will have the form Lemma rpredN R S (oppS : @opprPred R S) (kS : keyed_pred oppS) : {mono -%R: x / x \in kS}. Because x \in kS will be displayed as x \in S (or x \is S, etc), the canonical instance of opprPred will not normally be exposed (it will also be erased by /= simplification). In addition each predicate structure should have a DefaultPredKey Canonical instance that simply issues the property as a proof obligation (which can be caught by the Prop-irrelevant feature of the ssreflect plugin). 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. In the following R is in rel T: reflexive R <-> R is reflexive. irreflexive R <-> R is irreflexive. symmetric R <-> R (in rel T) is symmetric (equation). pre_symmetric R <-> R is symmetric (implication). antisymmetric R <-> R is antisymmetric. total R <-> R is total. transitive R <-> R is transitive. left_transitive R <-> R is a congruence on its left hand side. right_transitive R <-> R is a congruence on its right hand side. equivalence_rel R <-> R is an equivalence relation. 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 A, P1} <-> forall x, x \in A -> Qx. {in A1 & A2, P2} <-> forall x y, x \in A1 -> y \in A2 -> Qxy. {in A &, P2} <-> forall x y, x \in A -> y \in A -> Qxy. {in A1 & A2 & A3, Q3} <-> forall x y z, x \in A1 -> y \in A2 -> z \in A3 -> Qxyz. {in A1 & A2 &, Q3} == {in A1 & A2 & A2, Q3}. {in A1 && A3, Q3} == {in A1 & A1 & A3, Q3}. {in A &&, Q3} == {in A & A & A, Q3}. {in A, bijective f} == f has a right inverse in A. {on C, P1} == forall x, (f x) \in C -> Qx when P1 is also convertible to Pf f. {on C &, P2} == forall x y, f x \in C -> f y \in C -> Qxy when P2 is also convertible to Pf f. {on C, 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 C, bijective f} == f has a right inverse on C. This file extends the lemma name suffix conventions of ssrfun as follows: A -- associativity, as in andbA : associative andb. AC -- right commutativity. ACA -- self-interchange (inner commutativity), e.g., orbACA : (a || b) || (c || d) = (a || c) || (b || d). b -- a boolean argument, as in andbb : idempotent andb. C -- commutativity, as in andbC : commutative andb, or predicate complement, as in predC. CA -- left commutativity. D -- predicate difference, as in predD. E -- elimination, as in negbFE : ~~ b = false -> b. F or f -- boolean false, as in andbF : b && false = false. I -- left/right injectivity, as in addbI : right_injective addb, or predicate intersection, as in predI. l -- a left-hand operation, as andb_orl : left_distributive andb orb. N or n -- boolean negation, as in andbN : a && (~~ a) = false. P -- a characteristic property, often a reflection lemma, as in andP : reflect (a /\ b) (a && b). r -- a right-hand operation, as orb_andr : rightt_distributive orb andb. T or t -- boolean truth, as in andbT: right_id true andb. U -- predicate union, as in predU. W -- weakening, as in in1W : {in D, forall x, P} -> forall x, P.

Set Implicit Arguments.

Notation reflect := Bool.reflect.
Notation ReflectT := Bool.ReflectT.
Notation ReflectF := Bool.ReflectF.

Reserved Notation "~~ b" (at level 35, right associativity).
Reserved Notation "b ==> c" (at level 55, right associativity).
Reserved Notation "b1 (+) b2" (at level 50, left associativity).
Reserved Notation "x \in A"
  (at level 70, format "'[hv' x '/ ' \in A ']'", no associativity).
Reserved Notation "x \notin A"
  (at level 70, format "'[hv' x '/ ' \notin A ']'", no associativity).
Reserved Notation "p1 =i p2"
  (at level 70, format "'[hv' p1 '/ ' =i p2 ']'", no associativity).

We introduce a number of n-ary "list-style" notations that 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; the same limitations mean the separator cannot be omitted even when last_arg can. The Notation declarations are complicated by the separate treatment for some fixed arities (binary for bool operators, and all arities for Prop operators). We also use the square brackets in comprehension-style notations [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 followed by an operator symbol or a fixed identifier.

Reserved Notation "[ /\ P1 & P2 ]" (at level 0, only parsing).
Reserved Notation "[ /\ P1 , P2 & P3 ]" (at level 0, format
  "'[hv' [ /\ '[' P1 , '/' P2 ']' '/ ' & P3 ] ']'").
Reserved Notation "[ /\ P1 , P2 , P3 & P4 ]" (at level 0, format
  "'[hv' [ /\ '[' P1 , '/' P2 , '/' P3 ']' '/ ' & P4 ] ']'").
Reserved Notation "[ /\ P1 , P2 , P3 , P4 & P5 ]" (at level 0, format
  "'[hv' [ /\ '[' P1 , '/' P2 , '/' P3 , '/' P4 ']' '/ ' & P5 ] ']'").

Reserved Notation "[ \/ P1 | P2 ]" (at level 0, only parsing).
Reserved Notation "[ \/ P1 , P2 | P3 ]" (at level 0, format
  "'[hv' [ \/ '[' P1 , '/' P2 ']' '/ ' | P3 ] ']'").
Reserved Notation "[ \/ P1 , P2 , P3 | P4 ]" (at level 0, format
  "'[hv' [ \/ '[' P1 , '/' P2 , '/' P3 ']' '/ ' | P4 ] ']'").

Reserved Notation "[ && b1 & c ]" (at level 0, only parsing).
Reserved Notation "[ && b1 , b2 , .. , bn & c ]" (at level 0, format
  "'[hv' [ && '[' b1 , '/' b2 , '/' .. , '/' bn ']' '/ ' & c ] ']'").

Reserved Notation "[ || b1 | c ]" (at level 0, only parsing).
Reserved Notation "[ || b1 , b2 , .. , bn | c ]" (at level 0, format
  "'[hv' [ || '[' b1 , '/' b2 , '/' .. , '/' bn ']' '/ ' | c ] ']'").

Reserved Notation "[ ==> b1 => c ]" (at level 0, only parsing).
Reserved Notation "[ ==> b1 , b2 , .. , bn => c ]" (at level 0, format
  "'[hv' [ ==> '[' b1 , '/' b2 , '/' .. , '/' bn ']' '/' => c ] ']'").

Reserved Notation "[ 'pred' : T => E ]" (at level 0, format
  "'[hv' [ 'pred' : T => '/ ' E ] ']'").
Reserved Notation "[ 'pred' x => E ]" (at level 0, x at level 8, format
  "'[hv' [ 'pred' x => '/ ' E ] ']'").
Reserved Notation "[ 'pred' x : T => E ]" (at level 0, x at level 8, format
  "'[hv' [ 'pred' x : T => '/ ' E ] ']'").

Reserved Notation "[ 'rel' x y => E ]" (at level 0, x, y at level 8, format
  "'[hv' [ 'rel' x y => '/ ' E ] ']'").
Reserved Notation "[ 'rel' x y : T => E ]" (at level 0, x, y at level 8, format
  "'[hv' [ 'rel' x y : T => '/ ' E ] ']'").

Shorter delimiter
Delimit Scope bool_scope with B.
Open Scope bool_scope.

An alternative to xorb that behaves somewhat better wrt simplification.
Definition addb b := if b then negb else id.

Notation for && and || is declared in Init.Datatypes.
Notation "~~ b" := (negb b) : bool_scope.
Notation "b ==> c" := (implb b c) : bool_scope.
Notation "b1 (+) b2" := (addb b1 b2) : bool_scope.

Constant is_true b := b = true is defined in Init.Datatypes.
Coercion is_true : bool >-> Sortclass.
Lemma prop_congr : forall b b' : bool, b = b' -> b = b' :> Prop.

Ltac prop_congr := apply: prop_congr.

Lemmas for trivial.
Lemma is_true_true : true.
Lemma not_false_is_true : ~ false.
Lemma is_true_locked_true : locked true.
Hint Resolve is_true_true not_false_is_true is_true_locked_true.

Shorter names.
Definition isT := is_true_true.
Definition notF := not_false_is_true.

Negation lemmas.
We generally take NEGATION as the standard form of a false condition: negative boolean hypotheses should be of the form ~~ b, rather than ~ b or b = false, as much as possible.

Lemma negbT b : b = false -> ~~ b.
Lemma negbTE b : ~~ b -> b = false.
Lemma negbF b : (b : bool) -> ~~ b = false.
Lemma negbFE b : ~~ b = false -> b.
Lemma negbK : involutive negb.
Lemma negbNE b : ~~ ~~ b -> b.

Lemma negb_inj : injective negb.
Lemma negbLR b c : b = ~~ c -> ~~ b = c.
Lemma negbRL b c : ~~ b = c -> b = ~~ c.

Lemma contra (c b : bool) : (c -> b) -> ~~ b -> ~~ c.
Definition contraNN := contra.

Lemma contraL (c b : bool) : (c -> ~~ b) -> b -> ~~ c.
Definition contraTN := contraL.

Lemma contraR (c b : bool) : (~~ c -> b) -> ~~ b -> c.
Definition contraNT := contraR.

Lemma contraLR (c b : bool) : (~~ c -> ~~ b) -> b -> c.
Definition contraTT := contraLR.

Lemma contraT b : (~~ b -> false) -> b.

Lemma wlog_neg b : (~~ b -> b) -> b.

Lemma contraFT (c b : bool) : (~~ c -> b) -> b = false -> c.

Lemma contraFN (c b : bool) : (c -> b) -> b = false -> ~~ c.

Lemma contraTF (c b : bool) : (c -> ~~ b) -> b -> c = false.

Lemma contraNF (c b : bool) : (c -> b) -> ~~ b -> c = false.

Lemma contraFF (c b : bool) : (c -> b) -> b = false -> c = false.

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

Coercion isSome T (u : option T) := if u is Some _ then true else false.

Coercion is_inl A B (u : A + B) := if u is inl _ then true else false.

Coercion is_left A B (u : {A} + {B}) := if u is left _ then true else false.

Coercion is_inleft A B (u : A + {B}) := if u is inleft _ then true else false.


Definition decidable P := {P} + {~ P}.

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

Section BoolIf.

Variables (A B : Type) (x : A) (f : A -> B) (b : bool) (vT vF : A).

Variant if_spec (not_b : Prop) : bool -> A -> Set :=
  | IfSpecTrue of b : if_spec not_b true vT
  | IfSpecFalse of not_b : if_spec not_b false vF.

Lemma ifP : if_spec (b = false) b (if b then vT else vF).

Lemma ifPn : if_spec (~~ b) b (if b then vT else vF).

Lemma ifT : b -> (if b then vT else vF) = vT.
Lemma ifF : b = false -> (if b then vT else vF) = vF.
Lemma ifN : ~~ b -> (if b then vT else vF) = vF.

Lemma if_same : (if b then vT else vT) = vT.

Lemma if_neg : (if ~~ b then vT else vF) = if b then vF else vT.

Lemma fun_if : f (if b then vT else vF) = if b then f vT else f vF.

Lemma if_arg (fT fF : A -> B) :
  (if b then fT else fF) x = if b then fT x else fF x.

Turning a boolean "if" form into an application.
Definition if_expr := if b then vT else vF.
Lemma ifE : (if b then vT else vF) = if_expr.

End BoolIf.

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

Section ReflectCore.

Variables (P Q : Prop) (b c : bool).

Hypothesis Hb : reflect P b.

Lemma introNTF : (if c then ~ P else P) -> ~~ b = c.

Lemma introTF : (if c then P else ~ P) -> b = c.

Lemma elimNTF : ~~ b = c -> if c then ~ P else P.

Lemma elimTF : b = c -> if c then P else ~ P.

Lemma equivPif : (Q -> P) -> (P -> Q) -> if b then Q else ~ Q.

Lemma xorPif : Q \/ P -> ~ (Q /\ P) -> if b then ~ Q else Q.

End ReflectCore.

Internal negated reflection lemmas
Section ReflectNegCore.

Variables (P Q : Prop) (b c : bool).
Hypothesis Hb : reflect P (~~ b).

Lemma introTFn : (if c then ~ P else P) -> b = c.

Lemma elimTFn : b = c -> if c then ~ P else P.

Lemma equivPifn : (Q -> P) -> (P -> Q) -> if b then ~ Q else Q.

Lemma xorPifn : Q \/ P -> ~ (Q /\ P) -> if b then Q else ~ Q.

End ReflectNegCore.

User-oriented reflection lemmas
Section Reflect.

Variables (P Q : Prop) (b b' c : bool).
Hypotheses (Pb : reflect P b) (Pb' : reflect P (~~ b')).

Lemma introT : P -> b.
Lemma introF : ~ P -> b = false.
Lemma introN : ~ P -> ~~ b.
Lemma introNf : P -> ~~ b = false.
Lemma introTn : ~ P -> b'.
Lemma introFn : P -> b' = false.

Lemma elimT : b -> P.
Lemma elimF : b = false -> ~ P.
Lemma elimN : ~~ b -> ~P.
Lemma elimNf : ~~ b = false -> P.
Lemma elimTn : b' -> ~ P.
Lemma elimFn : b' = false -> P.

Lemma introP : (b -> Q) -> (~~ b -> ~ Q) -> reflect Q b.

Lemma iffP : (P -> Q) -> (Q -> P) -> reflect Q b.

Lemma equivP : (P <-> Q) -> reflect Q b.

Lemma sumboolP (decQ : decidable Q) : reflect Q decQ.

Lemma appP : reflect Q b -> P -> Q.

Lemma sameP : reflect P c -> b = c.

Lemma decPcases : if b then P else ~ P.

Definition decP : decidable P.

Lemma rwP : P <-> b.

Lemma rwP2 : reflect Q b -> (P <-> Q).

Predicate family to reflect excluded middle in bool.
Variant alt_spec : bool -> Type :=
  | AltTrue of P : alt_spec true
  | AltFalse of ~~ b : alt_spec false.

Lemma altP : alt_spec b.

End Reflect.




Allow the direct application of a reflection lemma to a boolean assertion.
Coercion elimT : reflect >-> Funclass.

Variant implies P Q := Implies of P -> Q.
Lemma impliesP P Q : implies P Q -> P -> Q.
Lemma impliesPn (P Q : Prop) : implies P Q -> ~ Q -> ~ P.
Coercion impliesP : implies >-> Funclass.

Impredicative or, which can emulate a classical not-implies.
Definition unless condition property : Prop :=
 forall goal : Prop, (condition -> goal) -> (property -> goal) -> goal.

Notation "\unless C , P" := (unless C P)
  (at level 200, C at level 100,
   format "'[' \unless C , '/ ' P ']'") : type_scope.

Lemma unlessL C P : implies C (\unless C, P).

Lemma unlessR C P : implies P (\unless C, P).

Lemma unless_sym C P : implies (\unless C, P) (\unless P, C).

Lemma unlessP (C P : Prop) : (\unless C, P) <-> C \/ P.

Lemma bind_unless C P {Q} : implies (\unless C, P) (\unless (\unless C, Q), P).

Lemma unless_contra b C : implies (~~ b -> C) (\unless C, b).

Classical reasoning becomes directly accessible for any bool subgoal. Note that we cannot use "unless" here for lack of universe polymorphism.
Definition classically P : Prop := forall b : bool, (P -> b) -> b.

Lemma classicP (P : Prop) : classically P <-> ~ ~ P.

Lemma classicW P : P -> classically P.

Lemma classic_bind P Q : (P -> classically Q) -> classically P -> classically Q.

Lemma classic_EM P : classically (decidable P).

Lemma classic_pick T P : classically ({x : T | P x} + (forall x, ~ P x)).

Lemma classic_imply P Q : (P -> classically Q) -> classically (P -> Q).

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 most proofs.

Inductive and3 (P1 P2 P3 : Prop) : Prop := And3 of P1 & P2 & P3.

Inductive and4 (P1 P2 P3 P4 : Prop) : Prop := And4 of P1 & P2 & P3 & P4.

Inductive and5 (P1 P2 P3 P4 P5 : Prop) : Prop :=
  And5 of P1 & P2 & P3 & P4 & P5.

Inductive or3 (P1 P2 P3 : Prop) : Prop := Or31 of P1 | Or32 of P2 | Or33 of P3.

Inductive or4 (P1 P2 P3 P4 : Prop) : Prop :=
  Or41 of P1 | Or42 of P2 | Or43 of P3 | Or44 of P4.

Notation "[ /\ P1 & P2 ]" := (and P1 P2) (only parsing) : type_scope.
Notation "[ /\ P1 , P2 & P3 ]" := (and3 P1 P2 P3) : type_scope.
Notation "[ /\ P1 , P2 , P3 & P4 ]" := (and4 P1 P2 P3 P4) : type_scope.
Notation "[ /\ P1 , P2 , P3 , P4 & P5 ]" := (and5 P1 P2 P3 P4 P5) : type_scope.

Notation "[ \/ P1 | P2 ]" := (or P1 P2) (only parsing) : type_scope.
Notation "[ \/ P1 , P2 | P3 ]" := (or3 P1 P2 P3) : type_scope.
Notation "[ \/ P1 , P2 , P3 | P4 ]" := (or4 P1 P2 P3 P4) : type_scope.

Notation "[ && b1 & c ]" := (b1 && c) (only parsing) : bool_scope.
Notation "[ && b1 , b2 , .. , bn & c ]" := (b1 && (b2 && .. (bn && c) .. ))
  : bool_scope.

Notation "[ || b1 | c ]" := (b1 || c) (only parsing) : bool_scope.
Notation "[ || b1 , b2 , .. , bn | c ]" := (b1 || (b2 || .. (bn || c) .. ))
  : bool_scope.

Notation "[ ==> b1 , b2 , .. , bn => c ]" :=
   (b1 ==> (b2 ==> .. (bn ==> c) .. )) : bool_scope.
Notation "[ ==> b1 => c ]" := (b1 ==> c) (only parsing) : bool_scope.

Section AllAnd.

Variables (T : Type) (P1 P2 P3 P4 P5 : T -> Prop).

Lemma all_and2 : implies (forall x, [/\ P1 x & P2 x]) [/\ a P1 & a P2].

Lemma all_and3 : implies (forall x, [/\ P1 x, P2 x & P3 x])
                         [/\ a P1, a P2 & a P3].

Lemma all_and4 : implies (forall x, [/\ P1 x, P2 x, P3 x & P4 x])
                         [/\ a P1, a P2, a P3 & a P4].

Lemma all_and5 : implies (forall x, [/\ P1 x, P2 x, P3 x, P4 x & P5 x])
                         [/\ a P1, a P2, a P3, a P4 & a P5].

End AllAnd.


Lemma pair_andP P Q : P /\ Q <-> P * Q.

Section ReflectConnectives.

Variable b1 b2 b3 b4 b5 : bool.

Lemma idP : reflect b1 b1.

Lemma boolP : alt_spec b1 b1 b1.

Lemma idPn : reflect (~~ b1) (~~ b1).

Lemma negP : reflect (~ b1) (~~ b1).

Lemma negPn : reflect b1 (~~ ~~ b1).

Lemma negPf : reflect (b1 = false) (~~ b1).

Lemma andP : reflect (b1 /\ b2) (b1 && b2).

Lemma and3P : reflect [/\ b1, b2 & b3] [&& b1, b2 & b3].

Lemma and4P : reflect [/\ b1, b2, b3 & b4] [&& b1, b2, b3 & b4].

Lemma and5P : reflect [/\ b1, b2, b3, b4 & b5] [&& b1, b2, b3, b4 & b5].

Lemma orP : reflect (b1 \/ b2) (b1 || b2).

Lemma or3P : reflect [\/ b1, b2 | b3] [|| b1, b2 | b3].

Lemma or4P : reflect [\/ b1, b2, b3 | b4] [|| b1, b2, b3 | b4].

Lemma nandP : reflect (~~ b1 \/ ~~ b2) (~~ (b1 && b2)).

Lemma norP : reflect (~~ b1 /\ ~~ b2) (~~ (b1 || b2)).

Lemma implyP : reflect (b1 -> b2) (b1 ==> b2).

End ReflectConnectives.


Shorter, more systematic names for the boolean connectives laws.

Lemma andTb : left_id true andb.
Lemma andFb : left_zero false andb.
Lemma andbT : right_id true andb.
Lemma andbF : right_zero false andb.
Lemma andbb : idempotent andb.
Lemma andbC : commutative andb.
Lemma andbA : associative andb.
Lemma andbCA : left_commutative andb.
Lemma andbAC : right_commutative andb.
Lemma andbACA : interchange andb andb.

Lemma orTb : forall b, true || b.
Lemma orFb : left_id false orb.
Lemma orbT : forall b, b || true.
Lemma orbF : right_id false orb.
Lemma orbb : idempotent orb.
Lemma orbC : commutative orb.
Lemma orbA : associative orb.
Lemma orbCA : left_commutative orb.
Lemma orbAC : right_commutative orb.
Lemma orbACA : interchange orb orb.

Lemma andbN b : b && ~~ b = false.
Lemma andNb b : ~~ b && b = false.
Lemma orbN b : b || ~~ b = true.
Lemma orNb b : ~~ b || b = true.

Lemma andb_orl : left_distributive andb orb.
Lemma andb_orr : right_distributive andb orb.
Lemma orb_andl : left_distributive orb andb.
Lemma orb_andr : right_distributive orb andb.

Lemma andb_idl (a b : bool) : (b -> a) -> a && b = b.
Lemma andb_idr (a b : bool) : (a -> b) -> a && b = a.
Lemma andb_id2l (a b c : bool) : (a -> b = c) -> a && b = a && c.
Lemma andb_id2r (a b c : bool) : (b -> a = c) -> a && b = c && b.

Lemma orb_idl (a b : bool) : (a -> b) -> a || b = b.
Lemma orb_idr (a b : bool) : (b -> a) -> a || b = a.
Lemma orb_id2l (a b c : bool) : (~~ a -> b = c) -> a || b = a || c.
Lemma orb_id2r (a b c : bool) : (~~ b -> a = c) -> a || b = c || b.

Lemma negb_and (a b : bool) : ~~ (a && b) = ~~ a || ~~ b.

Lemma negb_or (a b : bool) : ~~ (a || b) = ~~ a && ~~ b.

Pseudo-cancellation -- i.e, absorbtion

Lemma andbK a b : a && b || a = a.
Lemma andKb a b : a || b && a = a.
Lemma orbK a b : (a || b) && a = a.
Lemma orKb a b : a && (b || a) = a.

Imply

Lemma implybT b : b ==> true.
Lemma implybF b : (b ==> false) = ~~ b.
Lemma implyFb b : false ==> b.
Lemma implyTb b : (true ==> b) = b.
Lemma implybb b : b ==> b.

Lemma negb_imply a b : ~~ (a ==> b) = a && ~~ b.

Lemma implybE a b : (a ==> b) = ~~ a || b.

Lemma implyNb a b : (~~ a ==> b) = a || b.

Lemma implybN a b : (a ==> ~~ b) = (b ==> ~~ a).

Lemma implybNN a b : (~~ a ==> ~~ b) = b ==> a.

Lemma implyb_idl (a b : bool) : (~~ a -> b) -> (a ==> b) = b.
Lemma implyb_idr (a b : bool) : (b -> ~~ a) -> (a ==> b) = ~~ a.
Lemma implyb_id2l (a b c : bool) : (a -> b = c) -> (a ==> b) = (a ==> c).

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!

Ltac bool_congr :=
  match goal with
  | |- (?X1 && ?X2 = ?X3) => first
  [ symmetry; rewrite -1?(andbC X1) -?(andbCA X1); congr 1 (andb X1); symmetry
  | case: (X1); [ rewrite ?andTb ?andbT // | by rewrite ?andbF /= ] ]
  | |- (?X1 || ?X2 = ?X3) => first
  [ symmetry; rewrite -1?(orbC X1) -?(orbCA X1); congr 1 (orb X1); symmetry
  | case: (X1); [ by rewrite ?orbT //= | rewrite ?orFb ?orbF ] ]
  | |- (?X1 (+) ?X2 = ?X3) =>
    symmetry; rewrite -1?(addbC X1) -?(addbCA X1); congr 1 (addb X1); symmetry
  | |- (~~ ?X1 = ?X2) => congr 1 negb
  end.

Predicates, i.e., packaged functions to bool.
  • 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 call applicative and collective, based on the syntax used to test them at some x in T:
  • For an applicative predicate P, one uses prefix syntax: P x Also, most operations on applicative predicates use 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 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 general, be used applicatively, because of the "uniform inheritance" restriction on implicit coercions. 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 cannot 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 bigop). 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 lets us turn any Type aT : predArgType into 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 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 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) ], etc.
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. Finally, note that there is specific support for ambivalent predicates that can work in either style, as per this file's head descriptor.

Definition pred T := T -> bool.

Identity Coercion fun_of_pred : pred >-> Funclass.

Definition rel T := T -> pred T.

Identity Coercion fun_of_rel : rel >-> Funclass.

Notation xpred0 := (fun _ => false).
Notation xpredT := (fun _ => true).
Notation xpredI := (fun (p1 p2 : pred _) x => p1 x && p2 x).
Notation xpredU := (fun (p1 p2 : pred _) x => p1 x || p2 x).
Notation xpredC := (fun (p : pred _) x => ~~ p x).
Notation xpredD := (fun (p1 p2 : pred _) x => ~~ p2 x && p1 x).
Notation xpreim := (fun f (p : pred _) x => p (f x)).
Notation xrelU := (fun (r1 r2 : rel _) x y => r1 x y || r2 x y).

Section Predicates.

Variables T : Type.

Definition subpred (p1 p2 : pred T) := forall x, p1 x -> p2 x.

Definition subrel (r1 r2 : rel T) := forall x y, r1 x y -> r2 x y.

Definition simpl_pred := simpl_fun T bool.
Definition applicative_pred := pred T.
Definition collective_pred := pred T.

Definition SimplPred (p : pred T) : simpl_pred := SimplFun p.

Coercion pred_of_simpl (p : simpl_pred) : pred T := fun_of_simpl p.
Coercion applicative_pred_of_simpl (p : simpl_pred) : applicative_pred :=
  fun_of_simpl p.
Coercion collective_pred_of_simpl (p : simpl_pred) : collective_pred :=
  fun x => (let: SimplFun f := p in fun _ => f x) x.
Note: applicative_of_simpl is convertible to pred_of_simpl, while collective_of_simpl is not.

Definition pred0 := SimplPred xpred0.
Definition predT := SimplPred xpredT.
Definition predI p1 p2 := SimplPred (xpredI p1 p2).
Definition predU p1 p2 := SimplPred (xpredU p1 p2).
Definition predC p := SimplPred (xpredC p).
Definition predD p1 p2 := SimplPred (xpredD p1 p2).
Definition preim rT f (d : pred rT) := SimplPred (xpreim f d).

Definition simpl_rel := simpl_fun T (pred T).

Definition SimplRel (r : rel T) : simpl_rel := [fun x => r x].

Coercion rel_of_simpl_rel (r : simpl_rel) : rel T := fun x y => r x y.

Definition relU r1 r2 := SimplRel (xrelU r1 r2).

Lemma subrelUl r1 r2 : subrel r1 (relU r1 r2).

Lemma subrelUr r1 r2 : subrel r2 (relU r1 r2).

Variant mem_pred := Mem of pred T.

Definition isMem pT topred mem := mem = (fun p : pT => Mem [eta topred p]).

Structure predType := PredType {
  pred_sort :> Type;
  topred : pred_sort -> pred T;
  _ : {mem | isMem topred mem}
}.

Definition mkPredType pT toP := PredType (exist (@isMem pT toP) _ (erefl _)).

Canonical predPredType := Eval hnf in @mkPredType (pred T) id.
Canonical simplPredType := Eval hnf in mkPredType pred_of_simpl.
Canonical boolfunPredType := Eval hnf in @mkPredType (T -> bool) id.

Coercion pred_of_mem mp : pred_sort predPredType := let: Mem p := mp in [eta p].
Canonical memPredType := Eval hnf in mkPredType pred_of_mem.

Definition clone_pred U :=
  fun pT & pred_sort pT -> U =>
  fun a mP (pT' := @PredType U a mP) & phant_id pT' pT => pT'.

End Predicates.


Notation "[ 'pred' : T | E ]" := (SimplPred (fun _ : T => E%B))
  (at level 0, format "[ 'pred' : T | E ]") : fun_scope.
Notation "[ 'pred' x | E ]" := (SimplPred (fun x => E%B))
  (at level 0, x ident, format "[ 'pred' x | E ]") : fun_scope.
Notation "[ 'pred' x | E1 & E2 ]" := [pred x | E1 && E2 ]
  (at level 0, x ident, format "[ 'pred' x | E1 & E2 ]") : fun_scope.
Notation "[ 'pred' x : T | E ]" := (SimplPred (fun x : T => E%B))
  (at level 0, x ident, only parsing) : fun_scope.
Notation "[ 'pred' x : T | E1 & E2 ]" := [pred x : T | E1 && E2 ]
  (at level 0, x ident, only parsing) : fun_scope.
Notation "[ 'rel' x y | E ]" := (SimplRel (fun x y => E%B))
  (at level 0, x ident, y ident, format "[ 'rel' x y | E ]") : fun_scope.
Notation "[ 'rel' x y : T | E ]" := (SimplRel (fun x y : T => E%B))
  (at level 0, x ident, y ident, only parsing) : fun_scope.

Notation "[ 'predType' 'of' T ]" := (@clone_pred _ T _ id _ _ id)
  (at level 0, format "[ 'predType' 'of' T ]") : form_scope.

This redundant coercion lets us "inherit" the simpl_predType canonical instance 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 instance should always be resolved.

Notation pred_class := (pred_sort (predPredType _)).
Coercion sort_of_simpl_pred T (p : simpl_pred T) : pred_class := p : pred T.

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.
Definition predArgType := Type.
Identity Coercion sort_of_predArgType : predArgType >-> Sortclass.
Coercion pred_of_argType (T : predArgType) : simpl_pred T := predT.

Notation "{ : T }" := (T%type : predArgType)
  (at level 0, format "{ : T }") : type_scope.

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

Definition mem T (pT : predType T) : pT -> mem_pred T :=
  nosimpl (let: @PredType _ _ _ (exist _ mem _) := pT return pT -> _ in mem).
Definition in_mem T x mp := nosimpl pred_of_mem T mp x.


Coercion pred_of_mem_pred T mp := [pred x : T | in_mem x mp].

Definition eq_mem T p1 p2 := forall x : T, in_mem x p1 = in_mem x p2.
Definition sub_mem T p1 p2 := forall x : T, in_mem x p1 -> in_mem x p2.

Typeclasses Opaque eq_mem.

Lemma sub_refl T (p : mem_pred T) : sub_mem p p.

Notation "x \in A" := (in_mem x (mem A)) : bool_scope.
Notation "x \in A" := (in_mem x (mem A)) : bool_scope.
Notation "x \notin A" := (~~ (x \in A)) : bool_scope.
Notation "A =i B" := (eq_mem (mem A) (mem B)) : type_scope.
Notation "{ 'subset' A <= B }" := (sub_mem (mem A) (mem B))
  (at level 0, A, B at level 69,
   format "{ '[hv' 'subset' A '/ ' <= B ']' }") : type_scope.
Notation "[ 'mem' A ]" := (pred_of_simpl (pred_of_mem_pred (mem A)))
  (at level 0, only parsing) : fun_scope.
Notation "[ 'rel' 'of' fA ]" := (fun x => [mem (fA x)])
  (at level 0, format "[ 'rel' 'of' fA ]") : fun_scope.
Notation "[ 'predI' A & B ]" := (predI [mem A] [mem B])
  (at level 0, format "[ 'predI' A & B ]") : fun_scope.
Notation "[ 'predU' A & B ]" := (predU [mem A] [mem B])
  (at level 0, format "[ 'predU' A & B ]") : fun_scope.
Notation "[ 'predD' A & B ]" := (predD [mem A] [mem B])
  (at level 0, format "[ 'predD' A & B ]") : fun_scope.
Notation "[ 'predC' A ]" := (predC [mem A])
  (at level 0, format "[ 'predC' A ]") : fun_scope.
Notation "[ 'preim' f 'of' A ]" := (preim f [mem A])
  (at level 0, format "[ 'preim' f 'of' A ]") : fun_scope.

Notation "[ 'pred' x 'in' A ]" := [pred x | x \in A]
  (at level 0, x ident, format "[ 'pred' x 'in' A ]") : fun_scope.
Notation "[ 'pred' x 'in' A | E ]" := [pred x | x \in A & E]
  (at level 0, x ident, format "[ 'pred' x 'in' A | E ]") : fun_scope.
Notation "[ 'pred' x 'in' A | E1 & E2 ]" := [pred x | x \in A & E1 && E2 ]
  (at level 0, x ident,
   format "[ 'pred' x 'in' A | E1 & E2 ]") : fun_scope.
Notation "[ 'rel' x y 'in' A & B | E ]" :=
  [rel x y | (x \in A) && (y \in B) && E]
  (at level 0, x ident, y ident,
   format "[ 'rel' x y 'in' A & B | E ]") : fun_scope.
Notation "[ 'rel' x y 'in' A & B ]" := [rel x y | (x \in A) && (y \in B)]
  (at level 0, x ident, y ident,
   format "[ 'rel' x y 'in' A & B ]") : fun_scope.
Notation "[ 'rel' x y 'in' A | E ]" := [rel x y in A & A | E]
  (at level 0, x ident, y ident,
   format "[ 'rel' x y 'in' A | E ]") : fun_scope.
Notation "[ 'rel' x y 'in' A ]" := [rel x y in A & A]
  (at level 0, x ident, y ident,
   format "[ 'rel' x y 'in' A ]") : fun_scope.

Section simpl_mem.

Variables (T : Type) (pT : predType T).
Implicit Types (x : T) (p : pred T) (sp : simpl_pred T) (pp : pT).

Bespoke structures that provide fine-grained control over matching the various forms of the \in predicate; note in particular the different forms of hoisting that are used. We had to work around several bugs in the implementation of unification, notably improper expansion of telescope projections and overwriting of a variable assignment by a later unification (probably due to conversion cache cross-talk).
Because of the explicit eta expansion in the left-hand side, this lemma should only be used in a right-to-left direction. The 8.3 hack allowing partial right-to-left use does not work with the improved expansion heuristics in 8.4.
Lemma unfold_in x p : (x \in ([eta p] : pred T)) = p x.

Lemma simpl_predE p : SimplPred p =1 p.

Definition inE := (in_applicative, in_simpl, simpl_predE).
Lemma mem_simpl sp : mem sp = sp :> pred T.

Definition memE := mem_simpl.
Lemma mem_mem (pp : pT) : (mem (mem pp) = mem pp) * (mem [mem pp] = mem pp).

End simpl_mem.

Qualifiers and keyed predicates.

Variant qualifier (q : nat) T := Qualifier of predPredType T.

Coercion has_quality n T (q : qualifier n T) : pred_class :=
  fun x => let: Qualifier _ p := q in p x.

Lemma qualifE n T p x : (x \in @Qualifier n T p) = p x.

Notation "x \is A" := (x \in has_quality 0 A)
  (at level 70, no associativity,
   format "'[hv' x '/ ' \is A ']'") : bool_scope.
Notation "x \is 'a' A" := (x \in has_quality 1 A)
  (at level 70, no associativity,
   format "'[hv' x '/ ' \is 'a' A ']'") : bool_scope.
Notation "x \is 'an' A" := (x \in has_quality 2 A)
  (at level 70, no associativity,
   format "'[hv' x '/ ' \is 'an' A ']'") : bool_scope.
Notation "x \isn't A" := (x \notin has_quality 0 A)
  (at level 70, no associativity,
   format "'[hv' x '/ ' \isn't A ']'") : bool_scope.
Notation "x \isn't 'a' A" := (x \notin has_quality 1 A)
  (at level 70, no associativity,
   format "'[hv' x '/ ' \isn't 'a' A ']'") : bool_scope.
Notation "x \isn't 'an' A" := (x \notin has_quality 2 A)
  (at level 70, no associativity,
   format "'[hv' x '/ ' \isn't 'an' A ']'") : bool_scope.
Notation "[ 'qualify' x | P ]" := (Qualifier 0 (fun x => P%B))
  (at level 0, x at level 99,
   format "'[hv' [ 'qualify' x | '/ ' P ] ']'") : form_scope.
Notation "[ 'qualify' x : T | P ]" := (Qualifier 0 (fun x : T => P%B))
  (at level 0, x at level 99, only parsing) : form_scope.
Notation "[ 'qualify' 'a' x | P ]" := (Qualifier 1 (fun x => P%B))
  (at level 0, x at level 99,
   format "'[hv' [ 'qualify' 'a' x | '/ ' P ] ']'") : form_scope.
Notation "[ 'qualify' 'a' x : T | P ]" := (Qualifier 1 (fun x : T => P%B))
  (at level 0, x at level 99, only parsing) : form_scope.
Notation "[ 'qualify' 'an' x | P ]" := (Qualifier 2 (fun x => P%B))
  (at level 0, x at level 99,
   format "'[hv' [ 'qualify' 'an' x | '/ ' P ] ']'") : form_scope.
Notation "[ 'qualify' 'an' x : T | P ]" := (Qualifier 2 (fun x : T => P%B))
  (at level 0, x at level 99, only parsing) : form_scope.

Keyed predicates: support for property-bearing predicate interfaces.

Section KeyPred.

Variable T : Type.
Variant pred_key (p : predPredType T) := DefaultPredKey.

Variable p : predPredType T.
Structure keyed_pred (k : pred_key p) :=
  PackKeyedPred {unkey_pred :> pred_class; _ : unkey_pred =i p}.

Variable k : pred_key p.
Definition KeyedPred := @PackKeyedPred k p (frefl _).

Variable k_p : keyed_pred k.
Lemma keyed_predE : k_p =i p.

Instances that strip the mem cast; the first one has "pred_of_mem" as its projection head value, while the second has "pred_of_simpl". The latter has the side benefit of preempting accidental misdeclarations. Note: pred_of_mem is the registered mem >-> pred_class coercion, while simpl_of_mem; pred_of_simpl is the mem >-> pred >=> Funclass coercion. We must write down the coercions explicitly as the Canonical head constant computation does not strip casts !!
Canonical keyed_mem :=
  @PackKeyedPred k (pred_of_mem (mem k_p)) keyed_predE.
Canonical keyed_mem_simpl :=
  @PackKeyedPred k (pred_of_simpl (mem k_p)) keyed_predE.

End KeyPred.

Notation "x \i 'n' S" := (x \in @unkey_pred _ S _ _)
  (at level 70, format "'[hv' x '/ ' \i 'n' S ']'") : bool_scope.

Section KeyedQualifier.

Variables (T : Type) (n : nat) (q : qualifier n T).

Structure keyed_qualifier (k : pred_key q) :=
  PackKeyedQualifier {unkey_qualifier; _ : unkey_qualifier = q}.
Definition KeyedQualifier k := PackKeyedQualifier k (erefl q).
Variables (k : pred_key q) (k_q : keyed_qualifier k).
Fact keyed_qualifier_suproof : unkey_qualifier k_q =i q.
Canonical keyed_qualifier_keyed := PackKeyedPred k keyed_qualifier_suproof.

End KeyedQualifier.

Notation "x \i 's' A" := (x \i n has_quality 0 A)
  (at level 70, format "'[hv' x '/ ' \i 's' A ']'") : bool_scope.
Notation "x \i 's' 'a' A" := (x \i n has_quality 1 A)
  (at level 70, format "'[hv' x '/ ' \i 's' 'a' A ']'") : bool_scope.
Notation "x \i 's' 'an' A" := (x \i n has_quality 2 A)
  (at level 70, format "'[hv' x '/ ' \i 's' 'an' A ']'") : bool_scope.

Module DefaultKeying.

Canonical default_keyed_pred T p := KeyedPred (@DefaultPredKey T p).
Canonical default_keyed_qualifier T n (q : qualifier n T) :=
  KeyedQualifier (DefaultPredKey q).

End DefaultKeying.

Skolemizing with conditions.

Lemma all_tag_cond_dep I T (C : pred I) U :
    (forall x, T x) -> (forall x, C x -> {y : T x & U x y}) ->
  {f : forall x, T x & forall x, C x -> U x (f x)}.

Lemma all_tag_cond I T (C : pred I) U :
    T -> (forall x, C x -> {y : T & U x y}) ->
  {f : I -> T & forall x, C x -> U x (f x)}.

Lemma all_sig_cond_dep I T (C : pred I) P :
    (forall x, T x) -> (forall x, C x -> {y : T x | P x y}) ->
  {f : forall x, T x | forall x, C x -> P x (f x)}.

Lemma all_sig_cond I T (C : pred I) P :
    T -> (forall x, C x -> {y : T | P x y}) ->
  {f : I -> T | forall x, C x -> P x (f x)}.

Section RelationProperties.

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

Variable T : Type.

Variable R : rel T.

Definition total := forall x y, R x y || R y x.
Definition transitive := forall y x z, R x y -> R y z -> R x z.

Definition symmetric := forall x y, R x y = R y x.
Definition antisymmetric := forall x y, R x y && R y x -> x = y.
Definition pre_symmetric := forall x y, R x y -> R y x.

Lemma symmetric_from_pre : pre_symmetric -> symmetric.

Definition reflexive := forall x, R x x.
Definition irreflexive := forall x, R x x = false.

Definition left_transitive := forall x y, R x y -> R x =1 R y.
Definition right_transitive := forall x y, R x y -> R^~ x =1 R^~ y.

Section PER.

Hypotheses (symR : symmetric) (trR : transitive).

Lemma sym_left_transitive : left_transitive.

Lemma sym_right_transitive : right_transitive.

End PER.

We define the equivalence property with prenex quantification so that it can be localized using the {in ..., ..} form defined below.

Definition equivalence_rel := forall x y z, R z z * (R x y -> R x z = R y z).

Lemma equivalence_relP : equivalence_rel <-> reflexive /\ left_transitive.

End RelationProperties.

Lemma rev_trans T (R : rel T) : transitive R -> transitive (fun x y => R y x).

Property localization


Section LocalProperties.

Variables T1 T2 T3 : Type.

Variables (d1 : mem_pred T1) (d2 : mem_pred T2) (d3 : mem_pred T3).

Definition prop_for (x : T1) P & ph {all1 P} := P x.

Lemma forE x P phP : @prop_for x P phP = P x.

Definition prop_in1 P & ph {all1 P} :=
  forall x, in_mem x d1 -> P x.

Definition prop_in11 P & ph {all2 P} :=
  forall x y, in_mem x d1 -> in_mem y d2 -> P x y.

Definition prop_in2 P & ph {all2 P} :=
  forall x y, in_mem x d1 -> in_mem y d1 -> P x y.

Definition prop_in111 P & ph {all3 P} :=
  forall x y z, in_mem x d1 -> in_mem y d2 -> in_mem z d3 -> P x y z.

Definition prop_in12 P & ph {all3 P} :=
  forall x y z, in_mem x d1 -> in_mem y d2 -> in_mem z d2 -> P x y z.

Definition prop_in21 P & ph {all3 P} :=
  forall x y z, in_mem x d1 -> in_mem y d1 -> in_mem z d2 -> P x y z.

Definition prop_in3 P & ph {all3 P} :=
  forall x y z, in_mem x d1 -> in_mem y d1 -> in_mem z d1 -> P x y z.

Variable f : T1 -> T2.

Definition prop_on1 Pf P & phantom T3 (Pf f) & ph {all1 P} :=
  forall x, in_mem (f x) d2 -> P x.

Definition prop_on2 Pf P & phantom T3 (Pf f) & ph {all2 P} :=
  forall x y, in_mem (f x) d2 -> in_mem (f y) d2 -> P x y.

End LocalProperties.

Definition inPhantom := Phantom Prop.
Definition onPhantom T P (x : T) := Phantom Prop (P x).

Definition bijective_in aT rT (d : mem_pred aT) (f : aT -> rT) :=
  exists2 g, prop_in1 d (inPhantom (cancel f g))
           & prop_on1 d (Phantom _ (cancel g)) (onPhantom (cancel g) f).

Definition bijective_on aT rT (cd : mem_pred rT) (f : aT -> rT) :=
  exists2 g, prop_on1 cd (Phantom _ (cancel f)) (onPhantom (cancel f) g)
           & prop_in1 cd (inPhantom (cancel g f)).

Notation "{ 'for' x , P }" :=
  (prop_for x (inPhantom P))
  (at level 0, format "{ 'for' x , P }") : type_scope.

Notation "{ 'in' d , P }" :=
  (prop_in1 (mem d) (inPhantom P))
  (at level 0, format "{ 'in' d , P }") : type_scope.

Notation "{ 'in' d1 & d2 , P }" :=
  (prop_in11 (mem d1) (mem d2) (inPhantom P))
  (at level 0, format "{ 'in' d1 & d2 , P }") : type_scope.

Notation "{ 'in' d & , P }" :=
  (prop_in2 (mem d) (inPhantom P))
  (at level 0, format "{ 'in' d & , P }") : type_scope.

Notation "{ 'in' d1 & d2 & d3 , P }" :=
  (prop_in111 (mem d1) (mem d2) (mem d3) (inPhantom P))
  (at level 0, format "{ 'in' d1 & d2 & d3 , P }") : type_scope.

Notation "{ 'in' d1 & & d3 , P }" :=
  (prop_in21 (mem d1) (mem d3) (inPhantom P))
  (at level 0, format "{ 'in' d1 & & d3 , P }") : type_scope.

Notation "{ 'in' d1 & d2 & , P }" :=
  (prop_in12 (mem d1) (mem d2) (inPhantom P))
  (at level 0, format "{ 'in' d1 & d2 & , P }") : type_scope.

Notation "{ 'in' d & & , P }" :=
  (prop_in3 (mem d) (inPhantom P))
  (at level 0, format "{ 'in' d & & , P }") : type_scope.

Notation "{ 'on' cd , P }" :=
  (prop_on1 (mem cd) (inPhantom P) (inPhantom P))
  (at level 0, format "{ 'on' cd , P }") : type_scope.

Notation "{ 'on' cd & , P }" :=
  (prop_on2 (mem cd) (inPhantom P) (inPhantom P))
  (at level 0, format "{ 'on' cd & , P }") : type_scope.


Notation "{ 'on' cd , P & g }" :=
  (prop_on1 (mem cd) (Phantom (_ -> Prop) P) (onPhantom P g))
  (at level 0, format "{ 'on' cd , P & g }") : type_scope.

Notation "{ 'in' d , 'bijective' f }" := (bijective_in (mem d) f)
  (at level 0, f at level 8,
   format "{ 'in' d , 'bijective' f }") : type_scope.

Notation "{ 'on' cd , 'bijective' f }" := (bijective_on (mem cd) f)
  (at level 0, f at level 8,
   format "{ 'on' cd , 'bijective' f }") : type_scope.

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

Section LocalGlobal.

Variables T1 T2 T3 : predArgType.
Variables (D1 : pred T1) (D2 : pred T2) (D3 : pred T3).
Variables (d1 d1' : mem_pred T1) (d2 d2' : mem_pred T2) (d3 d3' : mem_pred T3).
Variables (f f' : T1 -> T2) (g : T2 -> T1) (h : T3).
Variables (P1 : T1 -> Prop) (P2 : T1 -> T2 -> Prop).
Variable P3 : T1 -> T2 -> T3 -> Prop.
Variable Q1 : (T1 -> T2) -> T1 -> Prop.
Variable Q1l : (T1 -> T2) -> T3 -> T1 -> Prop.
Variable Q2 : (T1 -> T2) -> T1 -> T1 -> Prop.

Hypothesis sub1 : sub_mem d1 d1'.
Hypothesis sub2 : sub_mem d2 d2'.
Hypothesis sub3 : sub_mem d3 d3'.

Lemma in1W : {all1 P1} -> {in D1, {all1 P1}}.
Lemma in2W : {all2 P2} -> {in D1 & D2, {all2 P2}}.
Lemma in3W : {all3 P3} -> {in D1 & D2 & D3, {all3 P3}}.

Lemma in1T : {in T1, {all1 P1}} -> {all1 P1}.
Lemma in2T : {in T1 & T2, {all2 P2}} -> {all2 P2}.
Lemma in3T : {in T1 & T2 & T3, {all3 P3}} -> {all3 P3}.

Lemma sub_in1 (Ph : ph {all1 P1}) : prop_in1 d1' Ph -> prop_in1 d1 Ph.

Lemma sub_in11 (Ph : ph {all2 P2}) : prop_in11 d1' d2' Ph -> prop_in11 d1 d2 Ph.

Lemma sub_in111 (Ph : ph {all3 P3}) :
  prop_in111 d1' d2' d3' Ph -> prop_in111 d1 d2 d3 Ph.

Let allQ1 f'' := {all1 Q1 f''}.
Let allQ1l f'' h' := {all1 Q1l f'' h'}.
Let allQ2 f'' := {all2 Q2 f''}.

Lemma on1W : allQ1 f -> {on D2, allQ1 f}.

Lemma on1lW : allQ1l f h -> {on D2, allQ1l f & h}.

Lemma on2W : allQ2 f -> {on D2 &, allQ2 f}.

Lemma on1T : {on T2, allQ1 f} -> allQ1 f.

Lemma on1lT : {on T2, allQ1l f & h} -> allQ1l f h.

Lemma on2T : {on T2 &, allQ2 f} -> allQ2 f.

Lemma subon1 (Phf : ph (allQ1 f)) (Ph : ph (allQ1 f)) :
  prop_on1 d2' Phf Ph -> prop_on1 d2 Phf Ph.

Lemma subon1l (Phf : ph (allQ1l f)) (Ph : ph (allQ1l f h)) :
  prop_on1 d2' Phf Ph -> prop_on1 d2 Phf Ph.

Lemma subon2 (Phf : ph (allQ2 f)) (Ph : ph (allQ2 f)) :
  prop_on2 d2' Phf Ph -> prop_on2 d2 Phf Ph.

Lemma can_in_inj : {in D1, cancel f g} -> {in D1 &, injective f}.

Lemma canLR_in x y : {in D1, cancel f g} -> y \in D1 -> x = f y -> g x = y.

Lemma canRL_in x y : {in D1, cancel f g} -> x \in D1 -> f x = y -> x = g y.

Lemma on_can_inj : {on D2, cancel f & g} -> {on D2 &, injective f}.

Lemma canLR_on x y : {on D2, cancel f & g} -> f y \in D2 -> x = f y -> g x = y.

Lemma canRL_on x y : {on D2, cancel f & g} -> f x \in D2 -> f x = y -> x = g y.

Lemma inW_bij : bijective f -> {in D1, bijective f}.

Lemma onW_bij : bijective f -> {on D2, bijective f}.

Lemma inT_bij : {in T1, bijective f} -> bijective f.

Lemma onT_bij : {on T2, bijective f} -> bijective f.

Lemma sub_in_bij (D1' : pred T1) :
  {subset D1 <= D1'} -> {in D1', bijective f} -> {in D1, bijective f}.

Lemma subon_bij (D2' : pred T2) :
  {subset D2 <= D2'} -> {on D2', bijective f} -> {on D2, bijective f}.

End LocalGlobal.

Lemma sub_in2 T d d' (P : T -> T -> Prop) :
  sub_mem d d' -> forall Ph : ph {all2 P}, prop_in2 d' Ph -> prop_in2 d Ph.

Lemma sub_in3 T d d' (P : T -> T -> T -> Prop) :
  sub_mem d d' -> forall Ph : ph {all3 P}, prop_in3 d' Ph -> prop_in3 d Ph.

Lemma sub_in12 T1 T d1 d1' d d' (P : T1 -> T -> T -> Prop) :
  sub_mem d1 d1' -> sub_mem d d' ->
  forall Ph : ph {all3 P}, prop_in12 d1' d' Ph -> prop_in12 d1 d Ph.

Lemma sub_in21 T T3 d d' d3 d3' (P : T -> T -> T3 -> Prop) :
  sub_mem d d' -> sub_mem d3 d3' ->
  forall Ph : ph {all3 P}, prop_in21 d' d3' Ph -> prop_in21 d d3 Ph.

Lemma equivalence_relP_in T (R : rel T) (A : pred T) :
  {in A & &, equivalence_rel R}
   <-> {in A, reflexive R} /\ {in A &, forall x y, R x y -> {in A, R x =1 R y}}.

Section MonoHomoMorphismTheory.

Variables (aT rT sT : Type) (f : aT -> rT) (g : rT -> aT).
Variables (aP : pred aT) (rP : pred rT) (aR : rel aT) (rR : rel rT).

Lemma monoW : {mono f : x / aP x >-> rP x} -> {homo f : x / aP x >-> rP x}.

Lemma mono2W :
  {mono f : x y / aR x y >-> rR x y} -> {homo f : x y / aR x y >-> rR x y}.

Hypothesis fgK : cancel g f.

Lemma homoRL :
  {homo f : x y / aR x y >-> rR x y} -> forall x y, aR (g x) y -> rR x (f y).

Lemma homoLR :
  {homo f : x y / aR x y >-> rR x y} -> forall x y, aR x (g y) -> rR (f x) y.

Lemma homo_mono :
    {homo f : x y / aR x y >-> rR x y} -> {homo g : x y / rR x y >-> aR x y} ->
  {mono g : x y / rR x y >-> aR x y}.

Lemma monoLR :
  {mono f : x y / aR x y >-> rR x y} -> forall x y, rR (f x) y = aR x (g y).

Lemma monoRL :
  {mono f : x y / aR x y >-> rR x y} -> forall x y, rR x (f y) = aR (g x) y.

Lemma can_mono :
  {mono f : x y / aR x y >-> rR x y} -> {mono g : x y / rR x y >-> aR x y}.

End MonoHomoMorphismTheory.

Section MonoHomoMorphismTheory_in.

Variables (aT rT sT : predArgType) (f : aT -> rT) (g : rT -> aT).
Variable (aD : pred aT).
Variable (aP : pred aT) (rP : pred rT) (aR : rel aT) (rR : rel rT).

Notation rD := [pred x | g x \in aD].

Lemma monoW_in :
    {in aD &, {mono f : x y / aR x y >-> rR x y}} ->
  {in aD &, {homo f : x y / aR x y >-> rR x y}}.

Lemma mono2W_in :
    {in aD, {mono f : x / aP x >-> rP x}} ->
  {in aD, {homo f : x / aP x >-> rP x}}.

Hypothesis fgK_on : {on aD, cancel g & f}.

Lemma homoRL_in :
    {in aD &, {homo f : x y / aR x y >-> rR x y}} ->
  {in rD & aD, forall x y, aR (g x) y -> rR x (f y)}.

Lemma homoLR_in :
    {in aD &, {homo f : x y / aR x y >-> rR x y}} ->
  {in aD & rD, forall x y, aR x (g y) -> rR (f x) y}.

Lemma homo_mono_in :
    {in aD &, {homo f : x y / aR x y >-> rR x y}} ->
    {in rD &, {homo g : x y / rR x y >-> aR x y}} ->
  {in rD &, {mono g : x y / rR x y >-> aR x y}}.

Lemma monoLR_in :
    {in aD &, {mono f : x y / aR x y >-> rR x y}} ->
  {in aD & rD, forall x y, rR (f x) y = aR x (g y)}.

Lemma monoRL_in :
    {in aD &, {mono f : x y / aR x y >-> rR x y}} ->
  {in rD & aD, forall x y, rR x (f y) = aR (g x) y}.

Lemma can_mono_in :
    {in aD &, {mono f : x y / aR x y >-> rR x y}} ->
  {in rD &, {mono g : x y / rR x y >-> aR x y}}.

End MonoHomoMorphismTheory_in.