summaryrefslogtreecommitdiff
path: root/debian/patches/remove-ssrmatching.patch
diff options
context:
space:
mode:
Diffstat (limited to 'debian/patches/remove-ssrmatching.patch')
-rw-r--r--debian/patches/remove-ssrmatching.patch3462
1 files changed, 0 insertions, 3462 deletions
diff --git a/debian/patches/remove-ssrmatching.patch b/debian/patches/remove-ssrmatching.patch
deleted file mode 100644
index 739c643e..00000000
--- a/debian/patches/remove-ssrmatching.patch
+++ /dev/null
@@ -1,3462 +0,0 @@
-From: Benjamin Barenblat <bbaren@debian.org>
-Subject: Remove ssrmatching
-Forwarded: not-needed
-Last-Update: 2019-02-02
-
-ssrmatching still has a file licensed under CeCILL-B, which I believe is a
-nonfree license. I’ve removed it from the Debian source package (see gbp.conf).
-This patch disables everything that depends on it.
---- a/Makefile.common
-+++ b/Makefile.common
-@@ -99,7 +99,7 @@
- setoid_ring extraction \
- cc funind firstorder derive \
- rtauto nsatz syntax btauto \
-- ssrmatching ltac ssr
-+ ltac
-
- SRCDIRS:=\
- $(CORESRCDIRS) \
-@@ -156,7 +156,7 @@
- $(EXTRACTIONCMO) \
- $(CCCMO) $(FOCMO) $(RTAUTOCMO) $(BTAUTOCMO) \
- $(FUNINDCMO) $(NSATZCMO) $(SYNTAXCMO) \
-- $(DERIVECMO) $(SSRMATCHINGCMO) $(SSRCMO)
-+ $(DERIVECMO)
-
- ifeq ($(HASNATDYNLINK)-$(BEST),false-opt)
- STATICPLUGINS:=$(PLUGINSCMO)
---- a/plugins/ssr/ssrbool.v
-+++ /dev/null
-@@ -1,1893 +0,0 @@
--(************************************************************************)
--(* * The Coq Proof Assistant / The Coq Development Team *)
--(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
--(* <O___,, * (see CREDITS file for the list of authors) *)
--(* \VV/ **************************************************************)
--(* // * This file is distributed under the terms of the *)
--(* * GNU Lesser General Public License Version 2.1 *)
--(* * (see LICENSE file for the text of the license) *)
--(************************************************************************)
--
--(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
--
--(** #<style> .doc { font-family: monospace; white-space: pre; } </style># **)
--
--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.
--Unset Strict Implicit.
--Unset Printing Implicit Defensive.
--Set Warnings "-projection-no-head-constant".
--
--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. (* Prop *)
--
--Lemma prop_congr : forall b b' : bool, b = b' -> b = b' :> Prop.
--Proof. by move=> b b' ->. Qed.
--
--Ltac prop_congr := apply: prop_congr.
--
--(** Lemmas for trivial. **)
--Lemma is_true_true : true. Proof. by []. Qed.
--Lemma not_false_is_true : ~ false. Proof. by []. Qed.
--Lemma is_true_locked_true : locked true. Proof. by unlock. Qed.
--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. Proof. by case: b. Qed.
--Lemma negbTE b : ~~ b -> b = false. Proof. by case: b. Qed.
--Lemma negbF b : (b : bool) -> ~~ b = false. Proof. by case: b. Qed.
--Lemma negbFE b : ~~ b = false -> b. Proof. by case: b. Qed.
--Lemma negbK : involutive negb. Proof. by case. Qed.
--Lemma negbNE b : ~~ ~~ b -> b. Proof. by case: b. Qed.
--
--Lemma negb_inj : injective negb. Proof. exact: can_inj negbK. Qed.
--Lemma negbLR b c : b = ~~ c -> ~~ b = c. Proof. exact: canLR negbK. Qed.
--Lemma negbRL b c : ~~ b = c -> b = ~~ c. Proof. exact: canRL negbK. Qed.
--
--Lemma contra (c b : bool) : (c -> b) -> ~~ b -> ~~ c.
--Proof. by case: b => //; case: c. Qed.
--Definition contraNN := contra.
--
--Lemma contraL (c b : bool) : (c -> ~~ b) -> b -> ~~ c.
--Proof. by case: b => //; case: c. Qed.
--Definition contraTN := contraL.
--
--Lemma contraR (c b : bool) : (~~ c -> b) -> ~~ b -> c.
--Proof. by case: b => //; case: c. Qed.
--Definition contraNT := contraR.
--
--Lemma contraLR (c b : bool) : (~~ c -> ~~ b) -> b -> c.
--Proof. by case: b => //; case: c. Qed.
--Definition contraTT := contraLR.
--
--Lemma contraT b : (~~ b -> false) -> b. Proof. by case: b => // ->. Qed.
--
--Lemma wlog_neg b : (~~ b -> b) -> b. Proof. by case: b => // ->. Qed.
--
--Lemma contraFT (c b : bool) : (~~ c -> b) -> b = false -> c.
--Proof. by move/contraR=> notb_c /negbT. Qed.
--
--Lemma contraFN (c b : bool) : (c -> b) -> b = false -> ~~ c.
--Proof. by move/contra=> notb_notc /negbT. Qed.
--
--Lemma contraTF (c b : bool) : (c -> ~~ b) -> b -> c = false.
--Proof. by move/contraL=> b_notc /b_notc/negbTE. Qed.
--
--Lemma contraNF (c b : bool) : (c -> b) -> ~~ b -> c = false.
--Proof. by move/contra=> notb_notc /notb_notc/negbTE. Qed.
--
--Lemma contraFF (c b : bool) : (c -> b) -> b = false -> c = false.
--Proof. by move/contraFN=> bF_notc /bF_notc/negbTE. Qed.
--
--(**
-- 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.
--
--Prenex Implicits isSome is_inl is_left is_inleft.
--
--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).
--Proof. by case def_b: b; constructor. Qed.
--
--Lemma ifPn : if_spec (~~ b) b (if b then vT else vF).
--Proof. by case def_b: b; constructor; rewrite ?def_b. Qed.
--
--Lemma ifT : b -> (if b then vT else vF) = vT. Proof. by move->. Qed.
--Lemma ifF : b = false -> (if b then vT else vF) = vF. Proof. by move->. Qed.
--Lemma ifN : ~~ b -> (if b then vT else vF) = vF. Proof. by move/negbTE->. Qed.
--
--Lemma if_same : (if b then vT else vT) = vT.
--Proof. by case b. Qed.
--
--Lemma if_neg : (if ~~ b then vT else vF) = if b then vF else vT.
--Proof. by case b. Qed.
--
--Lemma fun_if : f (if b then vT else vF) = if b then f vT else f vF.
--Proof. by case b. Qed.
--
--Lemma if_arg (fT fF : A -> B) :
-- (if b then fT else fF) x = if b then fT x else fF x.
--Proof. by case b. Qed.
--
--(** 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. Proof. by []. Qed.
--
--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.
--Proof. by case c; case Hb. Qed.
--
--Lemma introTF : (if c then P else ~ P) -> b = c.
--Proof. by case c; case Hb. Qed.
--
--Lemma elimNTF : ~~ b = c -> if c then ~ P else P.
--Proof. by move <-; case Hb. Qed.
--
--Lemma elimTF : b = c -> if c then P else ~ P.
--Proof. by move <-; case Hb. Qed.
--
--Lemma equivPif : (Q -> P) -> (P -> Q) -> if b then Q else ~ Q.
--Proof. by case Hb; auto. Qed.
--
--Lemma xorPif : Q \/ P -> ~ (Q /\ P) -> if b then ~ Q else Q.
--Proof. by case Hb => [? _ H ? | ? H _]; case: H. Qed.
--
--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.
--Proof. by move/(introNTF Hb) <-; case b. Qed.
--
--Lemma elimTFn : b = c -> if c then ~ P else P.
--Proof. by move <-; apply: (elimNTF Hb); case b. Qed.
--
--Lemma equivPifn : (Q -> P) -> (P -> Q) -> if b then ~ Q else Q.
--Proof. by rewrite -if_neg; apply: equivPif. Qed.
--
--Lemma xorPifn : Q \/ P -> ~ (Q /\ P) -> if b then Q else ~ Q.
--Proof. by rewrite -if_neg; apply: xorPif. Qed.
--
--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. Proof. exact: introTF true _. Qed.
--Lemma introF : ~ P -> b = false. Proof. exact: introTF false _. Qed.
--Lemma introN : ~ P -> ~~ b. Proof. exact: introNTF true _. Qed.
--Lemma introNf : P -> ~~ b = false. Proof. exact: introNTF false _. Qed.
--Lemma introTn : ~ P -> b'. Proof. exact: introTFn true _. Qed.
--Lemma introFn : P -> b' = false. Proof. exact: introTFn false _. Qed.
--
--Lemma elimT : b -> P. Proof. exact: elimTF true _. Qed.
--Lemma elimF : b = false -> ~ P. Proof. exact: elimTF false _. Qed.
--Lemma elimN : ~~ b -> ~P. Proof. exact: elimNTF true _. Qed.
--Lemma elimNf : ~~ b = false -> P. Proof. exact: elimNTF false _. Qed.
--Lemma elimTn : b' -> ~ P. Proof. exact: elimTFn true _. Qed.
--Lemma elimFn : b' = false -> P. Proof. exact: elimTFn false _. Qed.
--
--Lemma introP : (b -> Q) -> (~~ b -> ~ Q) -> reflect Q b.
--Proof. by case b; constructor; auto. Qed.
--
--Lemma iffP : (P -> Q) -> (Q -> P) -> reflect Q b.
--Proof. by case: Pb; constructor; auto. Qed.
--
--Lemma equivP : (P <-> Q) -> reflect Q b.
--Proof. by case; apply: iffP. Qed.
--
--Lemma sumboolP (decQ : decidable Q) : reflect Q decQ.
--Proof. by case: decQ; constructor. Qed.
--
--Lemma appP : reflect Q b -> P -> Q.
--Proof. by move=> Qb; move/introT; case: Qb. Qed.
--
--Lemma sameP : reflect P c -> b = c.
--Proof. by case; [apply: introT | apply: introF]. Qed.
--
--Lemma decPcases : if b then P else ~ P. Proof. by case Pb. Qed.
--
--Definition decP : decidable P. by case: b decPcases; [left | right]. Defined.
--
--Lemma rwP : P <-> b. Proof. by split; [apply: introT | apply: elimT]. Qed.
--
--Lemma rwP2 : reflect Q b -> (P <-> Q).
--Proof. by move=> Qb; split=> ?; [apply: appP | apply: elimT; case: Qb]. Qed.
--
--(** 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.
--Proof. by case def_b: b / Pb; constructor; rewrite ?def_b. Qed.
--
--End Reflect.
--
--Hint View for move/ elimTF|3 elimNTF|3 elimTFn|3 introT|2 introTn|2 introN|2.
--
--Hint View for apply/ introTF|3 introNTF|3 introTFn|3 elimT|2 elimTn|2 elimN|2.
--
--Hint View for apply// equivPif|3 xorPif|3 equivPifn|3 xorPifn|3.
--
--(** 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. Proof. by case. Qed.
--Lemma impliesPn (P Q : Prop) : implies P Q -> ~ Q -> ~ P.
--Proof. by case=> iP ? /iP. Qed.
--Coercion impliesP : implies >-> Funclass.
--Hint View for move/ impliesPn|2 impliesP|2.
--Hint View for apply/ impliesPn|2 impliesP|2.
--
--(** 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).
--Proof. by split=> hC G /(_ hC). Qed.
--
--Lemma unlessR C P : implies P (\unless C, P).
--Proof. by split=> hP G _ /(_ hP). Qed.
--
--Lemma unless_sym C P : implies (\unless C, P) (\unless P, C).
--Proof. by split; apply; [apply/unlessR | apply/unlessL]. Qed.
--
--Lemma unlessP (C P : Prop) : (\unless C, P) <-> C \/ P.
--Proof. by split=> [|[/unlessL | /unlessR]]; apply; [left | right]. Qed.
--
--Lemma bind_unless C P {Q} : implies (\unless C, P) (\unless (\unless C, Q), P).
--Proof. by split; apply=> [hC|hP]; [apply/unlessL/unlessL | apply/unlessR]. Qed.
--
--Lemma unless_contra b C : implies (~~ b -> C) (\unless C, b).
--Proof. by split; case: b => [_ | hC]; [apply/unlessR | apply/unlessL/hC]. Qed.
--
--(**
-- 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.
--Proof.
--split=> [cP nP | nnP [] // nP]; last by case nnP; move/nP.
--by have: P -> false; [move/nP | move/cP].
--Qed.
--
--Lemma classicW P : P -> classically P. Proof. by move=> hP _ ->. Qed.
--
--Lemma classic_bind P Q : (P -> classically Q) -> classically P -> classically Q.
--Proof. by move=> iPQ cP b /iPQ-/cP. Qed.
--
--Lemma classic_EM P : classically (decidable P).
--Proof.
--by case=> // undecP; apply/undecP; right=> notP; apply/notF/undecP; left.
--Qed.
--
--Lemma classic_pick T P : classically ({x : T | P x} + (forall x, ~ P x)).
--Proof.
--case=> // undecP; apply/undecP; right=> x Px.
--by apply/notF/undecP; left; exists x.
--Qed.
--
--Lemma classic_imply P Q : (P -> classically Q) -> classically (P -> Q).
--Proof.
--move=> iPQ []// notPQ; apply/notPQ=> /iPQ-cQ.
--by case: notF; apply: cQ => hQ; apply: notPQ.
--Qed.
--
--(**
-- 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).
--Local Notation a P := (forall x, P x).
--
--Lemma all_and2 : implies (forall x, [/\ P1 x & P2 x]) [/\ a P1 & a P2].
--Proof. by split=> haveP; split=> x; case: (haveP x). Qed.
--
--Lemma all_and3 : implies (forall x, [/\ P1 x, P2 x & P3 x])
-- [/\ a P1, a P2 & a P3].
--Proof. by split=> haveP; split=> x; case: (haveP x). Qed.
--
--Lemma all_and4 : implies (forall x, [/\ P1 x, P2 x, P3 x & P4 x])
-- [/\ a P1, a P2, a P3 & a P4].
--Proof. by split=> haveP; split=> x; case: (haveP x). Qed.
--
--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].
--Proof. by split=> haveP; split=> x; case: (haveP x). Qed.
--
--End AllAnd.
--
--Arguments all_and2 {T P1 P2}.
--Arguments all_and3 {T P1 P2 P3}.
--Arguments all_and4 {T P1 P2 P3 P4}.
--Arguments all_and5 {T P1 P2 P3 P4 P5}.
--
--Lemma pair_andP P Q : P /\ Q <-> P * Q. Proof. by split; case. Qed.
--
--Section ReflectConnectives.
--
--Variable b1 b2 b3 b4 b5 : bool.
--
--Lemma idP : reflect b1 b1.
--Proof. by case b1; constructor. Qed.
--
--Lemma boolP : alt_spec b1 b1 b1.
--Proof. exact: (altP idP). Qed.
--
--Lemma idPn : reflect (~~ b1) (~~ b1).
--Proof. by case b1; constructor. Qed.
--
--Lemma negP : reflect (~ b1) (~~ b1).
--Proof. by case b1; constructor; auto. Qed.
--
--Lemma negPn : reflect b1 (~~ ~~ b1).
--Proof. by case b1; constructor. Qed.
--
--Lemma negPf : reflect (b1 = false) (~~ b1).
--Proof. by case b1; constructor. Qed.
--
--Lemma andP : reflect (b1 /\ b2) (b1 && b2).
--Proof. by case b1; case b2; constructor=> //; case. Qed.
--
--Lemma and3P : reflect [/\ b1, b2 & b3] [&& b1, b2 & b3].
--Proof. by case b1; case b2; case b3; constructor; try by case. Qed.
--
--Lemma and4P : reflect [/\ b1, b2, b3 & b4] [&& b1, b2, b3 & b4].
--Proof. by case b1; case b2; case b3; case b4; constructor; try by case. Qed.
--
--Lemma and5P : reflect [/\ b1, b2, b3, b4 & b5] [&& b1, b2, b3, b4 & b5].
--Proof.
--by case b1; case b2; case b3; case b4; case b5; constructor; try by case.
--Qed.
--
--Lemma orP : reflect (b1 \/ b2) (b1 || b2).
--Proof. by case b1; case b2; constructor; auto; case. Qed.
--
--Lemma or3P : reflect [\/ b1, b2 | b3] [|| b1, b2 | b3].
--Proof.
--case b1; first by constructor; constructor 1.
--case b2; first by constructor; constructor 2.
--case b3; first by constructor; constructor 3.
--by constructor; case.
--Qed.
--
--Lemma or4P : reflect [\/ b1, b2, b3 | b4] [|| b1, b2, b3 | b4].
--Proof.
--case b1; first by constructor; constructor 1.
--case b2; first by constructor; constructor 2.
--case b3; first by constructor; constructor 3.
--case b4; first by constructor; constructor 4.
--by constructor; case.
--Qed.
--
--Lemma nandP : reflect (~~ b1 \/ ~~ b2) (~~ (b1 && b2)).
--Proof. by case b1; case b2; constructor; auto; case; auto. Qed.
--
--Lemma norP : reflect (~~ b1 /\ ~~ b2) (~~ (b1 || b2)).
--Proof. by case b1; case b2; constructor; auto; case; auto. Qed.
--
--Lemma implyP : reflect (b1 -> b2) (b1 ==> b2).
--Proof. by case b1; case b2; constructor; auto. Qed.
--
--End ReflectConnectives.
--
--Arguments idP [b1].
--Arguments idPn [b1].
--Arguments negP [b1].
--Arguments negPn [b1].
--Arguments negPf [b1].
--Arguments andP [b1 b2].
--Arguments and3P [b1 b2 b3].
--Arguments and4P [b1 b2 b3 b4].
--Arguments and5P [b1 b2 b3 b4 b5].
--Arguments orP [b1 b2].
--Arguments or3P [b1 b2 b3].
--Arguments or4P [b1 b2 b3 b4].
--Arguments nandP [b1 b2].
--Arguments norP [b1 b2].
--Arguments implyP [b1 b2].
--Prenex Implicits idP idPn negP negPn negPf.
--Prenex Implicits andP and3P and4P and5P orP or3P or4P nandP norP implyP.
--
--(** Shorter, more systematic names for the boolean connectives laws. **)
--
--Lemma andTb : left_id true andb. Proof. by []. Qed.
--Lemma andFb : left_zero false andb. Proof. by []. Qed.
--Lemma andbT : right_id true andb. Proof. by case. Qed.
--Lemma andbF : right_zero false andb. Proof. by case. Qed.
--Lemma andbb : idempotent andb. Proof. by case. Qed.
--Lemma andbC : commutative andb. Proof. by do 2!case. Qed.
--Lemma andbA : associative andb. Proof. by do 3!case. Qed.
--Lemma andbCA : left_commutative andb. Proof. by do 3!case. Qed.
--Lemma andbAC : right_commutative andb. Proof. by do 3!case. Qed.
--Lemma andbACA : interchange andb andb. Proof. by do 4!case. Qed.
--
--Lemma orTb : forall b, true || b. Proof. by []. Qed.
--Lemma orFb : left_id false orb. Proof. by []. Qed.
--Lemma orbT : forall b, b || true. Proof. by case. Qed.
--Lemma orbF : right_id false orb. Proof. by case. Qed.
--Lemma orbb : idempotent orb. Proof. by case. Qed.
--Lemma orbC : commutative orb. Proof. by do 2!case. Qed.
--Lemma orbA : associative orb. Proof. by do 3!case. Qed.
--Lemma orbCA : left_commutative orb. Proof. by do 3!case. Qed.
--Lemma orbAC : right_commutative orb. Proof. by do 3!case. Qed.
--Lemma orbACA : interchange orb orb. Proof. by do 4!case. Qed.
--
--Lemma andbN b : b && ~~ b = false. Proof. by case: b. Qed.
--Lemma andNb b : ~~ b && b = false. Proof. by case: b. Qed.
--Lemma orbN b : b || ~~ b = true. Proof. by case: b. Qed.
--Lemma orNb b : ~~ b || b = true. Proof. by case: b. Qed.
--
--Lemma andb_orl : left_distributive andb orb. Proof. by do 3!case. Qed.
--Lemma andb_orr : right_distributive andb orb. Proof. by do 3!case. Qed.
--Lemma orb_andl : left_distributive orb andb. Proof. by do 3!case. Qed.
--Lemma orb_andr : right_distributive orb andb. Proof. by do 3!case. Qed.
--
--Lemma andb_idl (a b : bool) : (b -> a) -> a && b = b.
--Proof. by case: a; case: b => // ->. Qed.
--Lemma andb_idr (a b : bool) : (a -> b) -> a && b = a.
--Proof. by case: a; case: b => // ->. Qed.
--Lemma andb_id2l (a b c : bool) : (a -> b = c) -> a && b = a && c.
--Proof. by case: a; case: b; case: c => // ->. Qed.
--Lemma andb_id2r (a b c : bool) : (b -> a = c) -> a && b = c && b.
--Proof. by case: a; case: b; case: c => // ->. Qed.
--
--Lemma orb_idl (a b : bool) : (a -> b) -> a || b = b.
--Proof. by case: a; case: b => // ->. Qed.
--Lemma orb_idr (a b : bool) : (b -> a) -> a || b = a.
--Proof. by case: a; case: b => // ->. Qed.
--Lemma orb_id2l (a b c : bool) : (~~ a -> b = c) -> a || b = a || c.
--Proof. by case: a; case: b; case: c => // ->. Qed.
--Lemma orb_id2r (a b c : bool) : (~~ b -> a = c) -> a || b = c || b.
--Proof. by case: a; case: b; case: c => // ->. Qed.
--
--Lemma negb_and (a b : bool) : ~~ (a && b) = ~~ a || ~~ b.
--Proof. by case: a; case: b. Qed.
--
--Lemma negb_or (a b : bool) : ~~ (a || b) = ~~ a && ~~ b.
--Proof. by case: a; case: b. Qed.
--
--(** Pseudo-cancellation -- i.e, absorbtion **)
--
--Lemma andbK a b : a && b || a = a. Proof. by case: a; case: b. Qed.
--Lemma andKb a b : a || b && a = a. Proof. by case: a; case: b. Qed.
--Lemma orbK a b : (a || b) && a = a. Proof. by case: a; case: b. Qed.
--Lemma orKb a b : a && (b || a) = a. Proof. by case: a; case: b. Qed.
--
--(** Imply **)
--
--Lemma implybT b : b ==> true. Proof. by case: b. Qed.
--Lemma implybF b : (b ==> false) = ~~ b. Proof. by case: b. Qed.
--Lemma implyFb b : false ==> b. Proof. by []. Qed.
--Lemma implyTb b : (true ==> b) = b. Proof. by []. Qed.
--Lemma implybb b : b ==> b. Proof. by case: b. Qed.
--
--Lemma negb_imply a b : ~~ (a ==> b) = a && ~~ b.
--Proof. by case: a; case: b. Qed.
--
--Lemma implybE a b : (a ==> b) = ~~ a || b.
--Proof. by case: a; case: b. Qed.
--
--Lemma implyNb a b : (~~ a ==> b) = a || b.
--Proof. by case: a; case: b. Qed.
--
--Lemma implybN a b : (a ==> ~~ b) = (b ==> ~~ a).
--Proof. by case: a; case: b. Qed.
--
--Lemma implybNN a b : (~~ a ==> ~~ b) = b ==> a.
--Proof. by case: a; case: b. Qed.
--
--Lemma implyb_idl (a b : bool) : (~~ a -> b) -> (a ==> b) = b.
--Proof. by case: a; case: b => // ->. Qed.
--Lemma implyb_idr (a b : bool) : (b -> ~~ a) -> (a ==> b) = ~~ a.
--Proof. by case: a; case: b => // ->. Qed.
--Lemma implyb_id2l (a b c : bool) : (a -> b = c) -> (a ==> b) = (a ==> c).
--Proof. by case: a; case: b; case: c => // ->. Qed.
--
--(** Addition (xor) **)
--
--Lemma addFb : left_id false addb. Proof. by []. Qed.
--Lemma addbF : right_id false addb. Proof. by case. Qed.
--Lemma addbb : self_inverse false addb. Proof. by case. Qed.
--Lemma addbC : commutative addb. Proof. by do 2!case. Qed.
--Lemma addbA : associative addb. Proof. by do 3!case. Qed.
--Lemma addbCA : left_commutative addb. Proof. by do 3!case. Qed.
--Lemma addbAC : right_commutative addb. Proof. by do 3!case. Qed.
--Lemma addbACA : interchange addb addb. Proof. by do 4!case. Qed.
--Lemma andb_addl : left_distributive andb addb. Proof. by do 3!case. Qed.
--Lemma andb_addr : right_distributive andb addb. Proof. by do 3!case. Qed.
--Lemma addKb : left_loop id addb. Proof. by do 2!case. Qed.
--Lemma addbK : right_loop id addb. Proof. by do 2!case. Qed.
--Lemma addIb : left_injective addb. Proof. by do 3!case. Qed.
--Lemma addbI : right_injective addb. Proof. by do 3!case. Qed.
--
--Lemma addTb b : true (+) b = ~~ b. Proof. by []. Qed.
--Lemma addbT b : b (+) true = ~~ b. Proof. by case: b. Qed.
--
--Lemma addbN a b : a (+) ~~ b = ~~ (a (+) b).
--Proof. by case: a; case: b. Qed.
--Lemma addNb a b : ~~ a (+) b = ~~ (a (+) b).
--Proof. by case: a; case: b. Qed.
--
--Lemma addbP a b : reflect (~~ a = b) (a (+) b).
--Proof. by case: a; case: b; constructor. Qed.
--Arguments addbP [a b].
--
--(**
-- 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).
--Proof. by move=> *; apply/orP; left. Qed.
--
--Lemma subrelUr r1 r2 : subrel r2 (relU r1 r2).
--Proof. by move=> *; apply/orP; right. Qed.
--
--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.
--
--Arguments pred0 [T].
--Arguments predT [T].
--Prenex Implicits pred0 predT predI predU predC predD preim relU.
--
--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.
--Bind Scope type_scope with predArgType.
--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.
--
--Prenex Implicits mem.
--
--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. Proof. by []. Qed.
--Arguments sub_refl {T 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). **)
--Structure manifest_applicative_pred p := ManifestApplicativePred {
-- manifest_applicative_pred_value :> pred T;
-- _ : manifest_applicative_pred_value = p
--}.
--Definition ApplicativePred p := ManifestApplicativePred (erefl p).
--Canonical applicative_pred_applicative sp :=
-- ApplicativePred (applicative_pred_of_simpl sp).
--
--Structure manifest_simpl_pred p := ManifestSimplPred {
-- manifest_simpl_pred_value :> simpl_pred T;
-- _ : manifest_simpl_pred_value = SimplPred p
--}.
--Canonical expose_simpl_pred p := ManifestSimplPred (erefl (SimplPred p)).
--
--Structure manifest_mem_pred p := ManifestMemPred {
-- manifest_mem_pred_value :> mem_pred T;
-- _ : manifest_mem_pred_value= Mem [eta p]
--}.
--Canonical expose_mem_pred p := @ManifestMemPred p _ (erefl _).
--
--Structure applicative_mem_pred p :=
-- ApplicativeMemPred {applicative_mem_pred_value :> manifest_mem_pred p}.
--Canonical check_applicative_mem_pred p (ap : manifest_applicative_pred p) mp :=
-- @ApplicativeMemPred ap mp.
--
--Lemma mem_topred (pp : pT) : mem (topred pp) = mem pp.
--Proof. by rewrite /mem; case: pT pp => T1 app1 [mem1 /= ->]. Qed.
--
--Lemma topredE x (pp : pT) : topred pp x = (x \in pp).
--Proof. by rewrite -mem_topred. Qed.
--
--Lemma app_predE x p (ap : manifest_applicative_pred p) : ap x = (x \in p).
--Proof. by case: ap => _ /= ->. Qed.
--
--Lemma in_applicative x p (amp : applicative_mem_pred p) : in_mem x amp = p x.
--Proof. by case: amp => [[_ /= ->]]. Qed.
--
--Lemma in_collective x p (msp : manifest_simpl_pred p) :
-- (x \in collective_pred_of_simpl msp) = p x.
--Proof. by case: msp => _ /= ->. Qed.
--
--Lemma in_simpl x p (msp : manifest_simpl_pred p) :
-- in_mem x (Mem [eta fun_of_simpl (msp : simpl_pred T)]) = p x.
--Proof. by case: msp => _ /= ->. Qed.
--
--(**
-- 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.
--Proof. by []. Qed.
--
--Lemma simpl_predE p : SimplPred p =1 p.
--Proof. by []. Qed.
--
--Definition inE := (in_applicative, in_simpl, simpl_predE). (* to be extended *)
--
--Lemma mem_simpl sp : mem sp = sp :> pred T.
--Proof. by []. Qed.
--
--Definition memE := mem_simpl. (* could be extended *)
--
--Lemma mem_mem (pp : pT) : (mem (mem pp) = mem pp) * (mem [mem pp] = mem pp).
--Proof. by rewrite -mem_topred. Qed.
--
--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.
--Arguments has_quality n [T].
--
--Lemma qualifE n T p x : (x \in @Qualifier n T p) = p x. Proof. by []. Qed.
--
--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. Proof. by case: k_p. Qed.
--
--(**
-- 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.
--Proof. by case: k_q => /= _ ->. Qed.
--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)}.
--Proof.
--move=> f0 fP; apply: all_tag (fun x y => C x -> U x y) _ => x.
--by case Cx: (C x); [case/fP: Cx => y; exists y | exists (f0 x)].
--Qed.
--
--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)}.
--Proof. by move=> y0; apply: all_tag_cond_dep. Qed.
--
--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)}.
--Proof. by move=> f0 /(all_tag_cond_dep f0)[f]; exists f. Qed.
--
--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)}.
--Proof. by move=> y0; apply: all_sig_cond_dep. Qed.
--
--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.
--Proof. by move=> symR x y; apply/idP/idP; apply: symR. Qed.
--
--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.
--Proof. by move=> x y Rxy z; apply/idP/idP; apply: trR; rewrite // symR. Qed.
--
--Lemma sym_right_transitive : right_transitive.
--Proof. by move=> x y /sym_left_transitive Rxy z; rewrite !(symR z) Rxy. Qed.
--
--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.
--Proof.
--split=> [eqiR | [Rxx trR] x y z]; last by split=> [|/trR->].
--by split=> [x | x y Rxy z]; [rewrite (eqiR x x x) | rewrite (eqiR x y z)].
--Qed.
--
--End RelationProperties.
--
--Lemma rev_trans T (R : rel T) : transitive R -> transitive (fun x y => R y x).
--Proof. by move=> trR x y z Ryx Rzy; apply: trR Rzy Ryx. Qed.
--
--(** Property localization **)
--
--Local Notation "{ 'all1' P }" := (forall x, P x : Prop) (at level 0).
--Local Notation "{ 'all2' P }" := (forall x y, P x y : Prop) (at level 0).
--Local Notation "{ 'all3' P }" := (forall x y z, P x y z: Prop) (at level 0).
--Local Notation ph := (phantom _).
--
--Section LocalProperties.
--
--Variables T1 T2 T3 : Type.
--
--Variables (d1 : mem_pred T1) (d2 : mem_pred T2) (d3 : mem_pred T3).
--Local Notation ph := (phantom Prop).
--
--Definition prop_for (x : T1) P & ph {all1 P} := P x.
--
--Lemma forE x P phP : @prop_for x P phP = P x. Proof. by []. Qed.
--
--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.
--
--Local Arguments onPhantom {_%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}}.
--Proof. by move=> ? ?. Qed.
--Lemma in2W : {all2 P2} -> {in D1 & D2, {all2 P2}}.
--Proof. by move=> ? ?. Qed.
--Lemma in3W : {all3 P3} -> {in D1 & D2 & D3, {all3 P3}}.
--Proof. by move=> ? ?. Qed.
--
--Lemma in1T : {in T1, {all1 P1}} -> {all1 P1}.
--Proof. by move=> ? ?; auto. Qed.
--Lemma in2T : {in T1 & T2, {all2 P2}} -> {all2 P2}.
--Proof. by move=> ? ?; auto. Qed.
--Lemma in3T : {in T1 & T2 & T3, {all3 P3}} -> {all3 P3}.
--Proof. by move=> ? ?; auto. Qed.
--
--Lemma sub_in1 (Ph : ph {all1 P1}) : prop_in1 d1' Ph -> prop_in1 d1 Ph.
--Proof. by move=> allP x /sub1; apply: allP. Qed.
--
--Lemma sub_in11 (Ph : ph {all2 P2}) : prop_in11 d1' d2' Ph -> prop_in11 d1 d2 Ph.
--Proof. by move=> allP x1 x2 /sub1 d1x1 /sub2; apply: allP. Qed.
--
--Lemma sub_in111 (Ph : ph {all3 P3}) :
-- prop_in111 d1' d2' d3' Ph -> prop_in111 d1 d2 d3 Ph.
--Proof. by move=> allP x1 x2 x3 /sub1 d1x1 /sub2 d2x2 /sub3; apply: allP. Qed.
--
--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}. Proof. by move=> ? ?. Qed.
--
--Lemma on1lW : allQ1l f h -> {on D2, allQ1l f & h}. Proof. by move=> ? ?. Qed.
--
--Lemma on2W : allQ2 f -> {on D2 &, allQ2 f}. Proof. by move=> ? ?. Qed.
--
--Lemma on1T : {on T2, allQ1 f} -> allQ1 f. Proof. by move=> ? ?; auto. Qed.
--
--Lemma on1lT : {on T2, allQ1l f & h} -> allQ1l f h.
--Proof. by move=> ? ?; auto. Qed.
--
--Lemma on2T : {on T2 &, allQ2 f} -> allQ2 f.
--Proof. by move=> ? ?; auto. Qed.
--
--Lemma subon1 (Phf : ph (allQ1 f)) (Ph : ph (allQ1 f)) :
-- prop_on1 d2' Phf Ph -> prop_on1 d2 Phf Ph.
--Proof. by move=> allQ x /sub2; apply: allQ. Qed.
--
--Lemma subon1l (Phf : ph (allQ1l f)) (Ph : ph (allQ1l f h)) :
-- prop_on1 d2' Phf Ph -> prop_on1 d2 Phf Ph.
--Proof. by move=> allQ x /sub2; apply: allQ. Qed.
--
--Lemma subon2 (Phf : ph (allQ2 f)) (Ph : ph (allQ2 f)) :
-- prop_on2 d2' Phf Ph -> prop_on2 d2 Phf Ph.
--Proof. by move=> allQ x y /sub2=> d2fx /sub2; apply: allQ. Qed.
--
--Lemma can_in_inj : {in D1, cancel f g} -> {in D1 &, injective f}.
--Proof. by move=> fK x y /fK{2}<- /fK{2}<- ->. Qed.
--
--Lemma canLR_in x y : {in D1, cancel f g} -> y \in D1 -> x = f y -> g x = y.
--Proof. by move=> fK D1y ->; rewrite fK. Qed.
--
--Lemma canRL_in x y : {in D1, cancel f g} -> x \in D1 -> f x = y -> x = g y.
--Proof. by move=> fK D1x <-; rewrite fK. Qed.
--
--Lemma on_can_inj : {on D2, cancel f & g} -> {on D2 &, injective f}.
--Proof. by move=> fK x y /fK{2}<- /fK{2}<- ->. Qed.
--
--Lemma canLR_on x y : {on D2, cancel f & g} -> f y \in D2 -> x = f y -> g x = y.
--Proof. by move=> fK D2fy ->; rewrite fK. Qed.
--
--Lemma canRL_on x y : {on D2, cancel f & g} -> f x \in D2 -> f x = y -> x = g y.
--Proof. by move=> fK D2fx <-; rewrite fK. Qed.
--
--Lemma inW_bij : bijective f -> {in D1, bijective f}.
--Proof. by case=> g' fK g'K; exists g' => * ? *; auto. Qed.
--
--Lemma onW_bij : bijective f -> {on D2, bijective f}.
--Proof. by case=> g' fK g'K; exists g' => * ? *; auto. Qed.
--
--Lemma inT_bij : {in T1, bijective f} -> bijective f.
--Proof. by case=> g' fK g'K; exists g' => * ? *; auto. Qed.
--
--Lemma onT_bij : {on T2, bijective f} -> bijective f.
--Proof. by case=> g' fK g'K; exists g' => * ? *; auto. Qed.
--
--Lemma sub_in_bij (D1' : pred T1) :
-- {subset D1 <= D1'} -> {in D1', bijective f} -> {in D1, bijective f}.
--Proof.
--by move=> subD [g' fK g'K]; exists g' => x; move/subD; [apply: fK | apply: g'K].
--Qed.
--
--Lemma subon_bij (D2' : pred T2) :
-- {subset D2 <= D2'} -> {on D2', bijective f} -> {on D2, bijective f}.
--Proof.
--by move=> subD [g' fK g'K]; exists g' => x; move/subD; [apply: fK | apply: g'K].
--Qed.
--
--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.
--Proof. by move=> /= sub_dd'; apply: sub_in11. Qed.
--
--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.
--Proof. by move=> /= sub_dd'; apply: sub_in111. Qed.
--
--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.
--Proof. by move=> /= sub1 sub; apply: sub_in111. Qed.
--
--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.
--Proof. by move=> /= sub sub3; apply: sub_in111. Qed.
--
--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}}.
--Proof.
--split=> [eqiR | [Rxx trR] x y z *]; last by split=> [|/trR-> //]; apply: Rxx.
--by split=> [x Ax|x y Ax Ay Rxy z Az]; [rewrite (eqiR x x) | rewrite (eqiR x y)].
--Qed.
--
--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}.
--Proof. by move=> hf x ax; rewrite hf. Qed.
--
--Lemma mono2W :
-- {mono f : x y / aR x y >-> rR x y} -> {homo f : x y / aR x y >-> rR x y}.
--Proof. by move=> hf x y axy; rewrite hf. Qed.
--
--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).
--Proof. by move=> Hf x y /Hf; rewrite fgK. Qed.
--
--Lemma homoLR :
-- {homo f : x y / aR x y >-> rR x y} -> forall x y, aR x (g y) -> rR (f x) y.
--Proof. by move=> Hf x y /Hf; rewrite fgK. Qed.
--
--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}.
--Proof.
--move=> mf mg x y; case: (boolP (rR _ _))=> [/mg //|].
--by apply: contraNF=> /mf; rewrite !fgK.
--Qed.
--
--Lemma monoLR :
-- {mono f : x y / aR x y >-> rR x y} -> forall x y, rR (f x) y = aR x (g y).
--Proof. by move=> mf x y; rewrite -{1}[y]fgK mf. Qed.
--
--Lemma monoRL :
-- {mono f : x y / aR x y >-> rR x y} -> forall x y, rR x (f y) = aR (g x) y.
--Proof. by move=> mf x y; rewrite -{1}[x]fgK mf. Qed.
--
--Lemma can_mono :
-- {mono f : x y / aR x y >-> rR x y} -> {mono g : x y / rR x y >-> aR x y}.
--Proof. by move=> mf x y /=; rewrite -mf !fgK. Qed.
--
--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}}.
--Proof. by move=> hf x y hx hy axy; rewrite hf. Qed.
--
--Lemma mono2W_in :
-- {in aD, {mono f : x / aP x >-> rP x}} ->
-- {in aD, {homo f : x / aP x >-> rP x}}.
--Proof. by move=> hf x hx ax; rewrite hf. Qed.
--
--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)}.
--Proof. by move=> Hf x y hx hy /Hf; rewrite fgK_on //; apply. Qed.
--
--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}.
--Proof. by move=> Hf x y hx hy /Hf; rewrite fgK_on //; apply. Qed.
--
--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}}.
--Proof.
--move=> mf mg x y hx hy; case: (boolP (rR _ _))=> [/mg //|]; first exact.
--by apply: contraNF=> /mf; rewrite !fgK_on //; apply.
--Qed.
--
--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)}.
--Proof. by move=> mf x y hx hy; rewrite -{1}[y]fgK_on // mf. Qed.
--
--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}.
--Proof. by move=> mf x y hx hy; rewrite -{1}[x]fgK_on // mf. Qed.
--
--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}}.
--Proof. by move=> mf x y hx hy /=; rewrite -mf // !fgK_on. Qed.
--
--End MonoHomoMorphismTheory_in.
---- a/plugins/ssr/ssreflect.v
-+++ /dev/null
-@@ -1,470 +0,0 @@
--(************************************************************************)
--(* * The Coq Proof Assistant / The Coq Development Team *)
--(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
--(* <O___,, * (see CREDITS file for the list of authors) *)
--(* \VV/ **************************************************************)
--(* // * This file is distributed under the terms of the *)
--(* * GNU Lesser General Public License Version 2.1 *)
--(* * (see LICENSE file for the text of the license) *)
--(************************************************************************)
--
--(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
--
--(** #<style> .doc { font-family: monospace; white-space: pre; } </style># **)
--
--Require Import Bool. (* For bool_scope delimiter 'bool'. *)
--Require Import ssrmatching.
--Declare ML Module "ssreflect_plugin".
--
--
--(**
-- This file is the Gallina part of the ssreflect plugin implementation.
-- Files that use the ssreflect plugin should always Require ssreflect and
-- either Import ssreflect or Import ssreflect.SsrSyntax.
-- Part of the contents of this file is technical and will only interest
-- advanced developers; in addition the following are defined:
-- #[#the str of v by f#]# == the Canonical s : str such that f s = v.
-- #[#the str of v#]# == the Canonical s : str that coerces to v.
-- argumentType c == the T such that c : forall x : T, P x.
-- returnType c == the R such that c : T -> R.
-- {type of c for s} == P s where c : forall x : T, P x.
-- phantom T v == singleton type with inhabitant Phantom T v.
-- phant T == singleton type with inhabitant Phant v.
-- =^~ r == the converse of rewriting rule r (e.g., in a
-- rewrite multirule).
-- unkeyed t == t, but treated as an unkeyed matching pattern by
-- the ssreflect matching algorithm.
-- nosimpl t == t, but on the right-hand side of Definition C :=
-- nosimpl disables expansion of C by /=.
-- locked t == t, but locked t is not convertible to t.
-- locked_with k t == t, but not convertible to t or locked_with k' t
-- unless k = k' (with k : unit). Coq type-checking
-- will be much more efficient if locked_with with a
-- bespoke k is used for sealed definitions.
-- unlockable v == interface for sealed constant definitions of v.
-- Unlockable def == the unlockable that registers def : C = v.
-- #[#unlockable of C#]# == a clone for C of the canonical unlockable for the
-- definition of C (e.g., if it uses locked_with).
-- #[#unlockable fun C#]# == #[#unlockable of C#]# with the expansion forced to be
-- an explicit lambda expression.
-- -> The usage pattern for ADT operations is:
-- Definition foo_def x1 .. xn := big_foo_expression.
-- Fact foo_key : unit. Proof. by #[# #]#. Qed.
-- Definition foo := locked_with foo_key foo_def.
-- Canonical foo_unlockable := #[#unlockable fun foo#]#.
-- This minimizes the comparison overhead for foo, while still allowing
-- rewrite unlock to expose big_foo_expression.
-- More information about these definitions and their use can be found in the
-- ssreflect manual, and in specific comments below. **)
--
--
--
--Set Implicit Arguments.
--Unset Strict Implicit.
--Unset Printing Implicit Defensive.
--
--Module SsrSyntax.
--
--(**
-- Declare Ssr keywords: 'is' 'of' '//' '/=' and '//='. We also declare the
-- parsing level 8, as a workaround for a notation grammar factoring problem.
-- Arguments of application-style notations (at level 10) should be declared
-- at level 8 rather than 9 or the camlp5 grammar will not factor properly. **)
--
--Reserved Notation "(* x 'is' y 'of' z 'isn't' // /= //= *)" (at level 8).
--Reserved Notation "(* 69 *)" (at level 69).
--
--(** Non ambiguous keyword to check if the SsrSyntax module is imported **)
--Reserved Notation "(* Use to test if 'SsrSyntax_is_Imported' *)" (at level 8).
--
--Reserved Notation "<hidden n >" (at level 200).
--Reserved Notation "T (* n *)" (at level 200, format "T (* n *)").
--
--End SsrSyntax.
--
--Export SsrMatchingSyntax.
--Export SsrSyntax.
--
--(**
-- Make the general "if" into a notation, so that we can override it below.
-- The notations are "only parsing" because the Coq decompiler will not
-- recognize the expansion of the boolean if; using the default printer
-- avoids a spurrious trailing %%GEN_IF. **)
--
--Delimit Scope general_if_scope with GEN_IF.
--
--Notation "'if' c 'then' v1 'else' v2" :=
-- (if c then v1 else v2)
-- (at level 200, c, v1, v2 at level 200, only parsing) : general_if_scope.
--
--Notation "'if' c 'return' t 'then' v1 'else' v2" :=
-- (if c return t then v1 else v2)
-- (at level 200, c, t, v1, v2 at level 200, only parsing) : general_if_scope.
--
--Notation "'if' c 'as' x 'return' t 'then' v1 'else' v2" :=
-- (if c as x return t then v1 else v2)
-- (at level 200, c, t, v1, v2 at level 200, x ident, only parsing)
-- : general_if_scope.
--
--(** Force boolean interpretation of simple if expressions. **)
--
--Delimit Scope boolean_if_scope with BOOL_IF.
--
--Notation "'if' c 'return' t 'then' v1 'else' v2" :=
-- (if c%bool is true in bool return t then v1 else v2) : boolean_if_scope.
--
--Notation "'if' c 'then' v1 'else' v2" :=
-- (if c%bool is true in bool return _ then v1 else v2) : boolean_if_scope.
--
--Notation "'if' c 'as' x 'return' t 'then' v1 'else' v2" :=
-- (if c%bool is true as x in bool return t then v1 else v2) : boolean_if_scope.
--
--Open Scope boolean_if_scope.
--
--(**
-- To allow a wider variety of notations without reserving a large number of
-- of identifiers, the ssreflect library systematically uses "forms" to
-- enclose complex mixfix syntax. A "form" is simply a mixfix expression
-- enclosed in square brackets and introduced by a keyword:
-- #[#keyword ... #]#
-- Because the keyword follows a bracket it does not need to be reserved.
-- Non-ssreflect libraries that do not respect the form syntax (e.g., the Coq
-- Lists library) should be loaded before ssreflect so that their notations
-- do not mask all ssreflect forms. **)
--Delimit Scope form_scope with FORM.
--Open Scope form_scope.
--
--(**
-- Allow overloading of the cast (x : T) syntax, put whitespace around the
-- ":" symbol to avoid lexical clashes (and for consistency with the parsing
-- precedence of the notation, which binds less tightly than application),
-- and put printing boxes that print the type of a long definition on a
-- separate line rather than force-fit it at the right margin. **)
--Notation "x : T" := (x : T)
-- (at level 100, right associativity,
-- format "'[hv' x '/ ' : T ']'") : core_scope.
--
--(**
-- Allow the casual use of notations like nat * nat for explicit Type
-- declarations. Note that (nat * nat : Type) is NOT equivalent to
-- (nat * nat)%%type, whose inferred type is legacy type "Set". **)
--Notation "T : 'Type'" := (T%type : Type)
-- (at level 100, only parsing) : core_scope.
--(** Allow similarly Prop annotation for, e.g., rewrite multirules. **)
--Notation "P : 'Prop'" := (P%type : Prop)
-- (at level 100, only parsing) : core_scope.
--
--(** Constants for abstract: and #[#: name #]# intro pattern **)
--Definition abstract_lock := unit.
--Definition abstract_key := tt.
--
--Definition abstract (statement : Type) (id : nat) (lock : abstract_lock) :=
-- let: tt := lock in statement.
--
--Notation "<hidden n >" := (abstract _ n _).
--Notation "T (* n *)" := (abstract T n abstract_key).
--
--(** Constants for tactic-views **)
--Inductive external_view : Type := tactic_view of Type.
--
--(**
-- Syntax for referring to canonical structures:
-- #[#the struct_type of proj_val by proj_fun#]#
-- This form denotes the Canonical instance s of the Structure type
-- struct_type whose proj_fun projection is proj_val, i.e., such that
-- proj_fun s = proj_val.
-- Typically proj_fun will be A record field accessors of struct_type, but
-- this need not be the case; it can be, for instance, a field of a record
-- type to which struct_type coerces; proj_val will likewise be coerced to
-- the return type of proj_fun. In all but the simplest cases, proj_fun
-- should be eta-expanded to allow for the insertion of implicit arguments.
-- In the common case where proj_fun itself is a coercion, the "by" part
-- can be omitted entirely; in this case it is inferred by casting s to the
-- inferred type of proj_val. Obviously the latter can be fixed by using an
-- explicit cast on proj_val, and it is highly recommended to do so when the
-- return type intended for proj_fun is "Type", as the type inferred for
-- proj_val may vary because of sort polymorphism (it could be Set or Prop).
-- Note when using the #[#the _ of _ #]# form to generate a substructure from a
-- telescopes-style canonical hierarchy (implementing inheritance with
-- coercions), one should always project or coerce the value to the BASE
-- structure, because Coq will only find a Canonical derived structure for
-- the Canonical base structure -- not for a base structure that is specific
-- to proj_value. **)
--
--Module TheCanonical.
--
--Variant put vT sT (v1 v2 : vT) (s : sT) := Put.
--
--Definition get vT sT v s (p : @put vT sT v v s) := let: Put _ _ _ := p in s.
--
--Definition get_by vT sT of sT -> vT := @get vT sT.
--
--End TheCanonical.
--
--Import TheCanonical. (* Note: no export. *)
--
--Local Arguments get_by _%type_scope _%type_scope _ _ _ _.
--
--Notation "[ 'the' sT 'of' v 'by' f ]" :=
-- (@get_by _ sT f _ _ ((fun v' (s : sT) => Put v' (f s) s) v _))
-- (at level 0, only parsing) : form_scope.
--
--Notation "[ 'the' sT 'of' v ]" := (get ((fun s : sT => Put v (*coerce*)s s) _))
-- (at level 0, only parsing) : form_scope.
--
--(**
-- The following are "format only" versions of the above notations. Since Coq
-- doesn't provide this facility, we fake it by splitting the "the" keyword.
-- We need to do this to prevent the formatter from being be thrown off by
-- application collapsing, coercion insertion and beta reduction in the right
-- hand side of the notations above. **)
--
--Notation "[ 'th' 'e' sT 'of' v 'by' f ]" := (@get_by _ sT f v _ _)
-- (at level 0, format "[ 'th' 'e' sT 'of' v 'by' f ]") : form_scope.
--
--Notation "[ 'th' 'e' sT 'of' v ]" := (@get _ sT v _ _)
-- (at level 0, format "[ 'th' 'e' sT 'of' v ]") : form_scope.
--
--(**
-- We would like to recognize
--Notation " #[# 'th' 'e' sT 'of' v : 'Type' #]#" := (@get Type sT v _ _)
-- (at level 0, format " #[# 'th' 'e' sT 'of' v : 'Type' #]#") : form_scope.
-- **)
--
--(**
-- Helper notation for canonical structure inheritance support.
-- This is a workaround for the poor interaction between delta reduction and
-- canonical projections in Coq's unification algorithm, by which transparent
-- definitions hide canonical instances, i.e., in
-- Canonical a_type_struct := @Struct a_type ...
-- Definition my_type := a_type.
-- my_type doesn't effectively inherit the struct structure from a_type. Our
-- solution is to redeclare the instance as follows
-- Canonical my_type_struct := Eval hnf in #[#struct of my_type#]#.
-- The special notation #[#str of _ #]# must be defined for each Strucure "str"
-- with constructor "Str", typically as follows
-- Definition clone_str s :=
-- let: Str _ x y ... z := s return {type of Str for s} -> str in
-- fun k => k _ x y ... z.
-- Notation " #[# 'str' 'of' T 'for' s #]#" := (@clone_str s (@Str T))
-- (at level 0, format " #[# 'str' 'of' T 'for' s #]#") : form_scope.
-- Notation " #[# 'str' 'of' T #]#" := (repack_str (fun x => @Str T x))
-- (at level 0, format " #[# 'str' 'of' T #]#") : form_scope.
-- The notation for the match return predicate is defined below; the eta
-- expansion in the second form serves both to distinguish it from the first
-- and to avoid the delta reduction problem.
-- There are several variations on the notation and the definition of the
-- the "clone" function, for telescopes, mixin classes, and join (multiple
-- inheritance) classes. We describe a different idiom for clones in ssrfun;
-- it uses phantom types (see below) and static unification; see fintype and
-- ssralg for examples. **)
--
--Definition argumentType T P & forall x : T, P x := T.
--Definition dependentReturnType T P & forall x : T, P x := P.
--Definition returnType aT rT & aT -> rT := rT.
--
--Notation "{ 'type' 'of' c 'for' s }" := (dependentReturnType c s)
-- (at level 0, format "{ 'type' 'of' c 'for' s }") : type_scope.
--
--(**
-- A generic "phantom" type (actually, a unit type with a phantom parameter).
-- This type can be used for type definitions that require some Structure
-- on one of their parameters, to allow Coq to infer said structure so it
-- does not have to be supplied explicitly or via the " #[#the _ of _ #]#" notation
-- (the latter interacts poorly with other Notation).
-- The definition of a (co)inductive type with a parameter p : p_type, that
-- needs to use the operations of a structure
-- Structure p_str : Type := p_Str {p_repr :> p_type; p_op : p_repr -> ...}
-- should be given as
-- Inductive indt_type (p : p_str) := Indt ... .
-- Definition indt_of (p : p_str) & phantom p_type p := indt_type p.
-- Notation "{ 'indt' p }" := (indt_of (Phantom p)).
-- Definition indt p x y ... z : {indt p} := @Indt p x y ... z.
-- Notation " #[# 'indt' x y ... z #]#" := (indt x y ... z).
-- That is, the concrete type and its constructor should be shadowed by
-- definitions that use a phantom argument to infer and display the true
-- value of p (in practice, the "indt" constructor often performs additional
-- functions, like "locking" the representation -- see below).
-- We also define a simpler version ("phant" / "Phant") of phantom for the
-- common case where p_type is Type. **)
--
--Variant phantom T (p : T) := Phantom.
--Arguments phantom : clear implicits.
--Arguments Phantom : clear implicits.
--Variant phant (p : Type) := Phant.
--
--(** Internal tagging used by the implementation of the ssreflect elim. **)
--
--Definition protect_term (A : Type) (x : A) : A := x.
--
--(**
-- The ssreflect idiom for a non-keyed pattern:
-- - unkeyed t wiil match any subterm that unifies with t, regardless of
-- whether it displays the same head symbol as t.
-- - unkeyed t a b will match any application of a term f unifying with t,
-- to two arguments unifying with with a and b, repectively, regardless of
-- apparent head symbols.
-- - unkeyed x where x is a variable will match any subterm with the same
-- type as x (when x would raise the 'indeterminate pattern' error). **)
--
--Notation unkeyed x := (let flex := x in flex).
--
--(** Ssreflect converse rewrite rule rule idiom. **)
--Definition ssr_converse R (r : R) := (Logic.I, r).
--Notation "=^~ r" := (ssr_converse r) (at level 100) : form_scope.
--
--(**
-- Term tagging (user-level).
-- The ssreflect library uses four strengths of term tagging to restrict
-- convertibility during type checking:
-- nosimpl t simplifies to t EXCEPT in a definition; more precisely, given
-- Definition foo := nosimpl bar, foo (or foo t') will NOT be expanded by
-- the /= and //= switches unless it is in a forcing context (e.g., in
-- match foo t' with ... end, foo t' will be reduced if this allows the
-- match to be reduced). Note that nosimpl bar is simply notation for a
-- a term that beta-iota reduces to bar; hence rewrite /foo will replace
-- foo by bar, and rewrite -/foo will replace bar by foo.
-- CAVEAT: nosimpl should not be used inside a Section, because the end of
-- section "cooking" removes the iota redex.
-- locked t is provably equal to t, but is not convertible to t; 'locked'
-- provides support for selective rewriting, via the lock t : t = locked t
-- Lemma, and the ssreflect unlock tactic.
-- locked_with k t is equal but not convertible to t, much like locked t,
-- but supports explicit tagging with a value k : unit. This is used to
-- mitigate a flaw in the term comparison heuristic of the Coq kernel,
-- which treats all terms of the form locked t as equal and conpares their
-- arguments recursively, leading to an exponential blowup of comparison.
-- For this reason locked_with should be used rather than locked when
-- defining ADT operations. The unlock tactic does not support locked_with
-- but the unlock rewrite rule does, via the unlockable interface.
-- we also use Module Type ascription to create truly opaque constants,
-- because simple expansion of constants to reveal an unreducible term
-- doubles the time complexity of a negative comparison. Such opaque
-- constants can be expanded generically with the unlock rewrite rule.
-- See the definition of card and subset in fintype for examples of this. **)
--
--Notation nosimpl t := (let: tt := tt in t).
--
--Lemma master_key : unit. Proof. exact tt. Qed.
--Definition locked A := let: tt := master_key in fun x : A => x.
--
--Lemma lock A x : x = locked x :> A. Proof. unlock; reflexivity. Qed.
--
--(** Needed for locked predicates, in particular for eqType's. **)
--Lemma not_locked_false_eq_true : locked false <> true.
--Proof. unlock; discriminate. Qed.
--
--(** The basic closing tactic "done". **)
--Ltac done :=
-- trivial; hnf; intros; solve
-- [ do ![solve [trivial | apply: sym_equal; trivial]
-- | discriminate | contradiction | split]
-- | case not_locked_false_eq_true; assumption
-- | match goal with H : ~ _ |- _ => solve [case H; trivial] end ].
--
--(** Quicker done tactic not including split, syntax: /0/ **)
--Ltac ssrdone0 :=
-- trivial; hnf; intros; solve
-- [ do ![solve [trivial | apply: sym_equal; trivial]
-- | discriminate | contradiction ]
-- | case not_locked_false_eq_true; assumption
-- | match goal with H : ~ _ |- _ => solve [case H; trivial] end ].
--
--(** To unlock opaque constants. **)
--Structure unlockable T v := Unlockable {unlocked : T; _ : unlocked = v}.
--Lemma unlock T x C : @unlocked T x C = x. Proof. by case: C. Qed.
--
--Notation "[ 'unlockable' 'of' C ]" := (@Unlockable _ _ C (unlock _))
-- (at level 0, format "[ 'unlockable' 'of' C ]") : form_scope.
--
--Notation "[ 'unlockable' 'fun' C ]" := (@Unlockable _ (fun _ => _) C (unlock _))
-- (at level 0, format "[ 'unlockable' 'fun' C ]") : form_scope.
--
--(** Generic keyed constant locking. **)
--
--(** The argument order ensures that k is always compared before T. **)
--Definition locked_with k := let: tt := k in fun T x => x : T.
--
--(**
-- This can be used as a cheap alternative to cloning the unlockable instance
-- below, but with caution as unkeyed matching can be expensive. **)
--Lemma locked_withE T k x : unkeyed (locked_with k x) = x :> T.
--Proof. by case: k. Qed.
--
--(** Intensionaly, this instance will not apply to locked u. **)
--Canonical locked_with_unlockable T k x :=
-- @Unlockable T x (locked_with k x) (locked_withE k x).
--
--(** More accurate variant of unlock, and safer alternative to locked_withE. **)
--Lemma unlock_with T k x : unlocked (locked_with_unlockable k x) = x :> T.
--Proof. exact: unlock. Qed.
--
--(** The internal lemmas for the have tactics. **)
--
--Definition ssr_have Plemma Pgoal (step : Plemma) rest : Pgoal := rest step.
--Arguments ssr_have Plemma [Pgoal].
--
--Definition ssr_have_let Pgoal Plemma step
-- (rest : let x : Plemma := step in Pgoal) : Pgoal := rest.
--Arguments ssr_have_let [Pgoal].
--
--Definition ssr_suff Plemma Pgoal step (rest : Plemma) : Pgoal := step rest.
--Arguments ssr_suff Plemma [Pgoal].
--
--Definition ssr_wlog := ssr_suff.
--Arguments ssr_wlog Plemma [Pgoal].
--
--(** Internal N-ary congruence lemmas for the congr tactic. **)
--
--Fixpoint nary_congruence_statement (n : nat)
-- : (forall B, (B -> B -> Prop) -> Prop) -> Prop :=
-- match n with
-- | O => fun k => forall B, k B (fun x1 x2 : B => x1 = x2)
-- | S n' =>
-- let k' A B e (f1 f2 : A -> B) :=
-- forall x1 x2, x1 = x2 -> (e (f1 x1) (f2 x2) : Prop) in
-- fun k => forall A, nary_congruence_statement n' (fun B e => k _ (k' A B e))
-- end.
--
--Lemma nary_congruence n (k := fun B e => forall y : B, (e y y : Prop)) :
-- nary_congruence_statement n k.
--Proof.
--have: k _ _ := _; rewrite {1}/k.
--elim: n k => [|n IHn] k k_P /= A; first exact: k_P.
--by apply: IHn => B e He; apply: k_P => f x1 x2 <-.
--Qed.
--
--Lemma ssr_congr_arrow Plemma Pgoal : Plemma = Pgoal -> Plemma -> Pgoal.
--Proof. by move->. Qed.
--Arguments ssr_congr_arrow : clear implicits.
--
--(** View lemmas that don't use reflection. **)
--
--Section ApplyIff.
--
--Variables P Q : Prop.
--Hypothesis eqPQ : P <-> Q.
--
--Lemma iffLR : P -> Q. Proof. by case: eqPQ. Qed.
--Lemma iffRL : Q -> P. Proof. by case: eqPQ. Qed.
--
--Lemma iffLRn : ~P -> ~Q. Proof. by move=> nP tQ; case: nP; case: eqPQ tQ. Qed.
--Lemma iffRLn : ~Q -> ~P. Proof. by move=> nQ tP; case: nQ; case: eqPQ tP. Qed.
--
--End ApplyIff.
--
--Hint View for move/ iffLRn|2 iffRLn|2 iffLR|2 iffRL|2.
--Hint View for apply/ iffRLn|2 iffLRn|2 iffRL|2 iffLR|2.
--
--(**
-- To focus non-ssreflect tactics on a subterm, eg vm_compute.
-- Usage:
-- elim/abstract_context: (pattern) => G defG.
-- vm_compute; rewrite {}defG {G}.
-- Note that vm_cast are not stored in the proof term
-- for reductions occuring in the context, hence
-- set here := pattern; vm_compute in (value of here)
-- blows up at Qed time. **)
--Lemma abstract_context T (P : T -> Type) x :
-- (forall Q, Q = P -> Q x) -> P x.
--Proof. by move=> /(_ P); apply. Qed.
---- a/plugins/ssr/ssrfun.v
-+++ /dev/null
-@@ -1,805 +0,0 @@
--(************************************************************************)
--(* * The Coq Proof Assistant / The Coq Development Team *)
--(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
--(* <O___,, * (see CREDITS file for the list of authors) *)
--(* \VV/ **************************************************************)
--(* // * This file is distributed under the terms of the *)
--(* * GNU Lesser General Public License Version 2.1 *)
--(* * (see LICENSE file for the text of the license) *)
--(************************************************************************)
--
--(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
--
--(** #<style> .doc { font-family: monospace; white-space: pre; } </style># **)
--
--Require Import ssreflect.
--
--
--(**
-- This file contains the basic definitions and notations for working with
-- functions. The definitions provide for:
--
-- - Pair projections:
-- p.1 == first element of a pair
-- p.2 == second element of a pair
-- These notations also apply to p : P /\ Q, via an and >-> pair coercion.
--
-- - Simplifying functions, beta-reduced by /= and simpl:
-- #[#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 common domain type
-- #[#fun (x : T) y => E#]# \
-- #[#fun (x : xT) (y : yT) => E#]# | == binary function with (some) explicit,
-- #[#fun x (y : T) => E#]# / independent domain types for each argument
--
-- - 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.
--
-- - Sigma types:
-- tag w == the i of w : {i : I & T i}.
-- tagged w == the T i component of w : {i : I & T i}.
-- Tagged T x == the {i : I & T i} with component x : T i.
-- tag2 w == the i of w : {i : I & T i & U i}.
-- tagged2 w == the T i component of w : {i : I & T i & U i}.
-- tagged2' w == the U i component of w : {i : I & T i & U i}.
-- Tagged2 T U x y == the {i : I & T i} with components x : T i and y : U i.
-- sval u == the x of u : {x : T | P x}.
-- s2val u == the x of u : {x : T | P x & Q x}.
-- The properties of sval u, s2val u are given by lemmas svalP, s2valP, and
-- s2valP'. We provide coercions sigT2 >-> sigT and sig2 >-> sig >-> sigT.
-- A suite of lemmas (all_sig, ...) let us skolemize sig, sig2, sigT, sigT2
-- and pair, e.g.,
-- have /all_sig#[#f fP#]# (x : T): {y : U | P y} by ...
-- yields an f : T -> U such that fP : forall x, P (f x).
-- - Identity functions:
-- id == NOTATION for the explicit identity function fun x => x.
-- @id T == notation for the explicit identity at type T.
-- idfun == an expression with a head constant, convertible to id;
-- idfun x simplifies to x.
-- @idfun T == the expression above, specialized to type T.
-- 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 for all x.
-- f1 =1 f2 :> A == ... and f2 is explicitly typed.
-- f1 =2 f2 == f1 x y is equal to f2 x y for all x y.
-- f1 =2 f2 :> A == ... and f2 is explicitly typed.
--
-- - Composition for total and partial functions:
-- f^~ y == function f with second argument specialised to y,
-- i.e., fun x => f x y
-- CAVEAT: conditional (non-maximal) implicit arguments
-- of f are NOT inserted in this context
-- @^~ x == application at x, i.e., fun f => f x
-- #[#eta f#]# == the explicit eta-expansion of f, i.e., fun x => f x
-- CAVEAT: conditional (non-maximal) implicit arguments
-- of f are NOT inserted in this context.
-- fun=> v := the constant function fun _ => v.
-- f1 \o f2 == composition of f1 and f2.
-- Note: (f1 \o f2) x simplifies to f1 (f2 x).
-- f1 \; f2 == categorical composition of f1 and f2. This expands to
-- to f2 \o f1 and (f1 \; f2) x simplifies to f2 (f1 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 (e op x = x).
-- right_id e op <-> e is a right identity for op (x op e = x).
-- left_inverse e inv op <-> inv is a left inverse for op wrt identity e,
-- i.e., (inv x) op x = e.
-- right_inverse e inv op <-> inv is a right inverse for op wrt identity e
-- i.e., x op (i x) = e.
-- self_inverse e op <-> each x is its own op-inverse (x op x = e).
-- idempotent op <-> op is idempotent for op (x op x = x).
-- associative op <-> op is associative, i.e.,
-- x op (y op z) = (x op y) op z.
-- commutative op <-> op is commutative (x op y = y op x).
-- left_commutative op <-> op is left commutative, i.e.,
-- x op (y op z) = y op (x op z).
-- right_commutative op <-> op is right commutative, i.e.,
-- (x op y) op z = (x op z) op y.
-- left_zero z op <-> z is a left zero for op (z op x = z).
-- right_zero z op <-> z is a right zero for op (x op z = z).
-- left_distributive op1 op2 <-> op1 distributes over op2 to the left:
-- (x op2 y) op1 z = (x op1 z) op2 (y op1 z).
-- right_distributive op1 op2 <-> op distributes over add to the right:
-- x op1 (y op2 z) = (x op1 z) op2 (x op1 z).
-- interchange op1 op2 <-> op1 and op2 satisfy an interchange law:
-- (x op2 y) op1 (z op2 t) = (x op1 z) op2 (y op1 t).
-- Note that interchange op op is a commutativity property.
-- left_injective op <-> op is injective in its left argument:
-- x op y = z op y -> x = z.
-- right_injective op <-> op is injective in its right argument:
-- x op y = x op z -> y = z.
-- left_loop inv op <-> op, inv obey the inverse loop left axiom:
-- (inv x) op (x op 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: x op ((inv x) op y) = y, for all x, y.
-- right_loop inv op <-> op, inv obey the inverse loop right axiom:
-- (x op y) op (inv y) = x for all x, y.
-- rev_right_loop inv op <-> op, inv obey the inverse loop reverse right
-- axiom: (x op y) op (inv y) = x for all x, y.
-- Note that familiar "cancellation" identities like x + y - y = x or
-- x - y + y = x are respectively instances of right_loop and rev_right_loop
-- The corresponding lemmas will use the K and NK/VK 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); if r == R#[#x#]#,
-- this states that f a = R#[#f x#]# for all x.
-- {morph f : x / a} <-> f is a morphism with respect to the
-- function expression (fun x => a). This is
-- shorthand for {morph f : x / a >-> a}; note
-- that the two instances of a are often
-- interpreted at different types.
-- {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 the
-- function expression (fun x y => a).
-- {homo f : x / a >-> r} <-> f is a homomorphism with respect to the
-- predicates (fun x => a) and (fun x => r);
-- if r == R#[#x#]#, this states that a -> R#[#f x#]#
-- for all x.
-- {homo f : x / a} <-> f is a homomorphism with respect to the
-- predicate expression (fun x => a).
-- {homo f : x y / a >-> r} <-> f is a homomorphism with respect to the
-- relations (fun x y => a) and (fun x y => r).
-- {homo f : x y / a} <-> f is a homomorphism with respect to the
-- relation expression (fun x y => a).
-- {mono f : x / a >-> r} <-> f is monotone with respect to projectors
-- (fun x => a) and (fun x => r); if r == R#[#x#]#,
-- this states that R#[#f x#]# = a for all x.
-- {mono f : x / a} <-> f is monotone with respect to the projector
-- expression (fun x => a).
-- {mono f : x y / a >-> r} <-> f is monotone with respect to relators
-- (fun x y => a) and (fun x y => r).
-- {mono f : x y / a} <-> f is monotone with respect to the relator
-- expression (fun x y => a).
--
-- The file also contains some basic lemmas for the above concepts.
-- Lemmas relative to cancellation laws use some abbreviated suffixes:
-- K - a cancellation rule like esymK : cancel (@esym T x y) (@esym T y x).
-- LR - a lemma moving an operation from the left hand side of a relation to
-- the right hand side, like canLR: cancel g f -> x = g y -> f x = y.
-- RL - a lemma moving an operation from the right to the left, e.g., canRL.
-- Beware that the LR and RL orientations refer to an "apply" (back chaining)
-- usage; when using the same lemmas with "have" or "move" (forward chaining)
-- the directions will be reversed!. **)
--
--
--Set Implicit Arguments.
--Unset Strict Implicit.
--Unset Printing Implicit Defensive.
--
--Delimit Scope fun_scope with FUN.
--Open Scope fun_scope.
--
--(** Notations for argument transpose **)
--Notation "f ^~ y" := (fun x => f x y)
-- (at level 10, y at level 8, no associativity, format "f ^~ y") : fun_scope.
--Notation "@^~ x" := (fun f => f x)
-- (at level 10, x at level 8, no associativity, format "@^~ x") : fun_scope.
--
--Delimit Scope pair_scope with PAIR.
--Open Scope pair_scope.
--
--(** Notations for pair/conjunction projections **)
--Notation "p .1" := (fst p)
-- (at level 2, left associativity, format "p .1") : pair_scope.
--Notation "p .2" := (snd p)
-- (at level 2, left associativity, format "p .2") : pair_scope.
--
--Coercion pair_of_and P Q (PandQ : P /\ Q) := (proj1 PandQ, proj2 PandQ).
--
--Definition all_pair I T U (w : forall i : I, T i * U i) :=
-- (fun i => (w i).1, fun i => (w i).2).
--
--(**
-- Complements on the option type constructor, used below to
-- encode partial functions. **)
--
--Module Option.
--
--Definition apply aT rT (f : aT -> rT) x u := if u is Some y then f y else x.
--
--Definition default T := apply (fun x : T => x).
--
--Definition bind aT rT (f : aT -> option rT) := apply f None.
--
--Definition map aT rT (f : aT -> rT) := bind (fun x => Some (f x)).
--
--End Option.
--
--Notation oapp := Option.apply.
--Notation odflt := Option.default.
--Notation obind := Option.bind.
--Notation omap := Option.map.
--Notation some := (@Some _) (only parsing).
--
--(** Shorthand for some basic equality lemmas. **)
--
--Notation erefl := refl_equal.
--Notation ecast i T e x := (let: erefl in _ = i := e return T in x).
--Definition esym := sym_eq.
--Definition nesym := sym_not_eq.
--Definition etrans := trans_eq.
--Definition congr1 := f_equal.
--Definition congr2 := f_equal2.
--(** Force at least one implicit when used as a view. **)
--Prenex Implicits esym nesym.
--
--(** A predicate for singleton types. **)
--Definition all_equal_to T (x0 : T) := forall x, unkeyed x = x0.
--
--Lemma unitE : all_equal_to tt. Proof. by case. Qed.
--
--(** A generic wrapper type **)
--
--Structure wrapped T := Wrap {unwrap : T}.
--Canonical wrap T x := @Wrap T x.
--
--Prenex Implicits unwrap wrap Wrap.
--
--(**
-- 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. **)
--
--Reserved Notation "[ 'rec' a0 ]"
-- (at level 0, format "[ 'rec' a0 ]").
--Reserved Notation "[ 'rec' a0 , a1 ]"
-- (at level 0, format "[ 'rec' a0 , a1 ]").
--Reserved Notation "[ 'rec' a0 , a1 , a2 ]"
-- (at level 0, format "[ 'rec' a0 , a1 , a2 ]").
--Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 ]"
-- (at level 0, format "[ 'rec' a0 , a1 , a2 , a3 ]").
--Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 , a4 ]"
-- (at level 0, format "[ 'rec' a0 , a1 , a2 , a3 , a4 ]").
--Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 ]"
-- (at level 0, format "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 ]").
--Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 ]"
-- (at level 0, format "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 ]").
--Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 , a7 ]"
-- (at level 0,
-- format "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 , a7 ]").
--Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 , a7 , a8 ]"
-- (at level 0,
-- format "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 , a7 , a8 ]").
--Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 , a7 , a8 , a9 ]"
-- (at level 0,
-- format "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 , a7 , a8 , a9 ]").
--
--(**
-- Definitions and notation for explicit functions with simplification,
-- i.e., which simpl and /= beta expand (this is complementary to nosimpl). **)
--
--Section SimplFun.
--
--Variables aT rT : Type.
--
--Variant simpl_fun := SimplFun of aT -> rT.
--
--Definition fun_of_simpl f := fun x => let: SimplFun lam := f in lam x.
--
--Coercion fun_of_simpl : simpl_fun >-> Funclass.
--
--End SimplFun.
--
--Notation "[ 'fun' : T => E ]" := (SimplFun (fun _ : T => E))
-- (at level 0,
-- format "'[hv' [ 'fun' : T => '/ ' E ] ']'") : fun_scope.
--
--Notation "[ 'fun' x => E ]" := (SimplFun (fun x => E))
-- (at level 0, x ident,
-- format "'[hv' [ 'fun' x => '/ ' E ] ']'") : fun_scope.
--
--Notation "[ 'fun' x : T => E ]" := (SimplFun (fun x : T => E))
-- (at level 0, x ident, only parsing) : fun_scope.
--
--Notation "[ 'fun' x y => E ]" := (fun x => [fun y => E])
-- (at level 0, x ident, y ident,
-- format "'[hv' [ 'fun' x y => '/ ' E ] ']'") : fun_scope.
--
--Notation "[ 'fun' x y : T => E ]" := (fun x : T => [fun y : T => E])
-- (at level 0, x ident, y ident, only parsing) : fun_scope.
--
--Notation "[ 'fun' ( x : T ) y => E ]" := (fun x : T => [fun y => E])
-- (at level 0, x ident, y ident, only parsing) : fun_scope.
--
--Notation "[ 'fun' x ( y : T ) => E ]" := (fun x => [fun y : T => E])
-- (at level 0, x ident, y ident, only parsing) : fun_scope.
--
--Notation "[ 'fun' ( x : xT ) ( y : yT ) => E ]" :=
-- (fun x : xT => [fun y : yT => E])
-- (at level 0, x ident, y ident, only parsing) : fun_scope.
--
--(** For delta functions in eqtype.v. **)
--Definition SimplFunDelta aT rT (f : aT -> aT -> rT) := [fun z => f z z].
--
--(**
-- Extensional equality, for unary and binary functions, including syntactic
-- sugar. **)
--
--Section ExtensionalEquality.
--
--Variables A B C : Type.
--
--Definition eqfun (f g : B -> A) : Prop := forall x, f x = g x.
--
--Definition eqrel (r s : C -> B -> A) : Prop := forall x y, r x y = s x y.
--
--Lemma frefl f : eqfun f f. Proof. by []. Qed.
--Lemma fsym f g : eqfun f g -> eqfun g f. Proof. by move=> eq_fg x. Qed.
--
--Lemma ftrans f g h : eqfun f g -> eqfun g h -> eqfun f h.
--Proof. by move=> eq_fg eq_gh x; rewrite eq_fg. Qed.
--
--Lemma rrefl r : eqrel r r. Proof. by []. Qed.
--
--End ExtensionalEquality.
--
--Typeclasses Opaque eqfun.
--Typeclasses Opaque eqrel.
--
--Hint Resolve frefl rrefl.
--
--Notation "f1 =1 f2" := (eqfun f1 f2)
-- (at level 70, no associativity) : fun_scope.
--Notation "f1 =1 f2 :> A" := (f1 =1 (f2 : A))
-- (at level 70, f2 at next level, A at level 90) : fun_scope.
--Notation "f1 =2 f2" := (eqrel f1 f2)
-- (at level 70, no associativity) : fun_scope.
--Notation "f1 =2 f2 :> A" := (f1 =2 (f2 : A))
-- (at level 70, f2 at next level, A at level 90) : fun_scope.
--
--Section Composition.
--
--Variables A B C : Type.
--
--Definition funcomp u (f : B -> A) (g : C -> B) x := let: tt := u in f (g x).
--Definition catcomp u g f := funcomp u f g.
--Local Notation comp := (funcomp tt).
--
--Definition pcomp (f : B -> option A) (g : C -> option B) x := obind f (g x).
--
--Lemma eq_comp f f' g g' : f =1 f' -> g =1 g' -> comp f g =1 comp f' g'.
--Proof. by move=> eq_ff' eq_gg' x; rewrite /= eq_gg' eq_ff'. Qed.
--
--End Composition.
--
--Notation comp := (funcomp tt).
--Notation "@ 'comp'" := (fun A B C => @funcomp A B C tt).
--Notation "f1 \o f2" := (comp f1 f2)
-- (at level 50, format "f1 \o '/ ' f2") : fun_scope.
--Notation "f1 \; f2" := (catcomp tt f1 f2)
-- (at level 60, right associativity, format "f1 \; '/ ' f2") : fun_scope.
--
--Notation "[ 'eta' f ]" := (fun x => f x)
-- (at level 0, format "[ 'eta' f ]") : fun_scope.
--
--Notation "'fun' => E" := (fun _ => E) (at level 200, only parsing) : fun_scope.
--
--Notation id := (fun x => x).
--Notation "@ 'id' T" := (fun x : T => x)
-- (at level 10, T at level 8, only parsing) : fun_scope.
--
--Definition id_head T u x : T := let: tt := u in x.
--Definition explicit_id_key := tt.
--Notation idfun := (id_head tt).
--Notation "@ 'idfun' T " := (@id_head T explicit_id_key)
-- (at level 10, T at level 8, format "@ 'idfun' T") : fun_scope.
--
--Definition phant_id T1 T2 v1 v2 := phantom T1 v1 -> phantom T2 v2.
--
--(** Strong sigma types. **)
--
--Section Tag.
--
--Variables (I : Type) (i : I) (T_ U_ : I -> Type).
--
--Definition tag := projT1.
--Definition tagged : forall w, T_(tag w) := @projT2 I [eta T_].
--Definition Tagged x := @existT I [eta T_] i x.
--
--Definition tag2 (w : @sigT2 I T_ U_) := let: existT2 _ _ i _ _ := w in i.
--Definition tagged2 w : T_(tag2 w) := let: existT2 _ _ _ x _ := w in x.
--Definition tagged2' w : U_(tag2 w) := let: existT2 _ _ _ _ y := w in y.
--Definition Tagged2 x y := @existT2 I [eta T_] [eta U_] i x y.
--
--End Tag.
--
--Arguments Tagged [I i].
--Arguments Tagged2 [I i].
--Prenex Implicits tag tagged Tagged tag2 tagged2 tagged2' Tagged2.
--
--Coercion tag_of_tag2 I T_ U_ (w : @sigT2 I T_ U_) :=
-- Tagged (fun i => T_ i * U_ i)%type (tagged2 w, tagged2' w).
--
--Lemma all_tag I T U :
-- (forall x : I, {y : T x & U x y}) ->
-- {f : forall x, T x & forall x, U x (f x)}.
--Proof. by move=> fP; exists (fun x => tag (fP x)) => x; case: (fP x). Qed.
--
--Lemma all_tag2 I T U V :
-- (forall i : I, {y : T i & U i y & V i y}) ->
-- {f : forall i, T i & forall i, U i (f i) & forall i, V i (f i)}.
--Proof. by case/all_tag=> f /all_pair[]; exists f. Qed.
--
--(** Refinement types. **)
--
--(** Prenex Implicits and renaming. **)
--Notation sval := (@proj1_sig _ _).
--Notation "@ 'sval'" := (@proj1_sig) (at level 10, format "@ 'sval'").
--
--Section Sig.
--
--Variables (T : Type) (P Q : T -> Prop).
--
--Lemma svalP (u : sig P) : P (sval u). Proof. by case: u. Qed.
--
--Definition s2val (u : sig2 P Q) := let: exist2 _ _ x _ _ := u in x.
--
--Lemma s2valP u : P (s2val u). Proof. by case: u. Qed.
--
--Lemma s2valP' u : Q (s2val u). Proof. by case: u. Qed.
--
--End Sig.
--
--Prenex Implicits svalP s2val s2valP s2valP'.
--
--Coercion tag_of_sig I P (u : @sig I P) := Tagged P (svalP u).
--
--Coercion sig_of_sig2 I P Q (u : @sig2 I P Q) :=
-- exist (fun i => P i /\ Q i) (s2val u) (conj (s2valP u) (s2valP' u)).
--
--Lemma all_sig I T P :
-- (forall x : I, {y : T x | P x y}) ->
-- {f : forall x, T x | forall x, P x (f x)}.
--Proof. by case/all_tag=> f; exists f. Qed.
--
--Lemma all_sig2 I T P Q :
-- (forall x : I, {y : T x | P x y & Q x y}) ->
-- {f : forall x, T x | forall x, P x (f x) & forall x, Q x (f x)}.
--Proof. by case/all_sig=> f /all_pair[]; exists f. Qed.
--
--Section Morphism.
--
--Variables (aT rT sT : Type) (f : aT -> rT).
--
--(** Morphism property for unary and binary functions **)
--Definition morphism_1 aF rF := forall x, f (aF x) = rF (f x).
--Definition morphism_2 aOp rOp := forall x y, f (aOp x y) = rOp (f x) (f y).
--
--(** Homomorphism property for unary and binary relations **)
--Definition homomorphism_1 (aP rP : _ -> Prop) := forall x, aP x -> rP (f x).
--Definition homomorphism_2 (aR rR : _ -> _ -> Prop) :=
-- forall x y, aR x y -> rR (f x) (f y).
--
--(** Stability property for unary and binary relations **)
--Definition monomorphism_1 (aP rP : _ -> sT) := forall x, rP (f x) = aP x.
--Definition monomorphism_2 (aR rR : _ -> _ -> sT) :=
-- forall x y, rR (f x) (f y) = aR x y.
--
--End Morphism.
--
--Notation "{ 'morph' f : x / a >-> r }" :=
-- (morphism_1 f (fun x => a) (fun x => r))
-- (at level 0, f at level 99, x ident,
-- format "{ 'morph' f : x / a >-> r }") : type_scope.
--
--Notation "{ 'morph' f : x / a }" :=
-- (morphism_1 f (fun x => a) (fun x => a))
-- (at level 0, f at level 99, x ident,
-- format "{ 'morph' f : x / a }") : type_scope.
--
--Notation "{ 'morph' f : x y / a >-> r }" :=
-- (morphism_2 f (fun x y => a) (fun x y => r))
-- (at level 0, f at level 99, x ident, y ident,
-- format "{ 'morph' f : x y / a >-> r }") : type_scope.
--
--Notation "{ 'morph' f : x y / a }" :=
-- (morphism_2 f (fun x y => a) (fun x y => a))
-- (at level 0, f at level 99, x ident, y ident,
-- format "{ 'morph' f : x y / a }") : type_scope.
--
--Notation "{ 'homo' f : x / a >-> r }" :=
-- (homomorphism_1 f (fun x => a) (fun x => r))
-- (at level 0, f at level 99, x ident,
-- format "{ 'homo' f : x / a >-> r }") : type_scope.
--
--Notation "{ 'homo' f : x / a }" :=
-- (homomorphism_1 f (fun x => a) (fun x => a))
-- (at level 0, f at level 99, x ident,
-- format "{ 'homo' f : x / a }") : type_scope.
--
--Notation "{ 'homo' f : x y / a >-> r }" :=
-- (homomorphism_2 f (fun x y => a) (fun x y => r))
-- (at level 0, f at level 99, x ident, y ident,
-- format "{ 'homo' f : x y / a >-> r }") : type_scope.
--
--Notation "{ 'homo' f : x y / a }" :=
-- (homomorphism_2 f (fun x y => a) (fun x y => a))
-- (at level 0, f at level 99, x ident, y ident,
-- format "{ 'homo' f : x y / a }") : type_scope.
--
--Notation "{ 'homo' f : x y /~ a }" :=
-- (homomorphism_2 f (fun y x => a) (fun x y => a))
-- (at level 0, f at level 99, x ident, y ident,
-- format "{ 'homo' f : x y /~ a }") : type_scope.
--
--Notation "{ 'mono' f : x / a >-> r }" :=
-- (monomorphism_1 f (fun x => a) (fun x => r))
-- (at level 0, f at level 99, x ident,
-- format "{ 'mono' f : x / a >-> r }") : type_scope.
--
--Notation "{ 'mono' f : x / a }" :=
-- (monomorphism_1 f (fun x => a) (fun x => a))
-- (at level 0, f at level 99, x ident,
-- format "{ 'mono' f : x / a }") : type_scope.
--
--Notation "{ 'mono' f : x y / a >-> r }" :=
-- (monomorphism_2 f (fun x y => a) (fun x y => r))
-- (at level 0, f at level 99, x ident, y ident,
-- format "{ 'mono' f : x y / a >-> r }") : type_scope.
--
--Notation "{ 'mono' f : x y / a }" :=
-- (monomorphism_2 f (fun x y => a) (fun x y => a))
-- (at level 0, f at level 99, x ident, y ident,
-- format "{ 'mono' f : x y / a }") : type_scope.
--
--Notation "{ 'mono' f : x y /~ a }" :=
-- (monomorphism_2 f (fun y x => a) (fun x y => a))
-- (at level 0, f at level 99, x ident, y ident,
-- format "{ 'mono' f : x y /~ a }") : type_scope.
--
--(**
-- 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. **)
--
--Section Injections.
--
--(**
-- 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). **)
--Variables (rT aT : Type) (f : aT -> rT).
--
--Definition injective := forall x1 x2, f x1 = f x2 -> x1 = x2.
--
--Definition cancel g := forall x, g (f x) = x.
--
--Definition pcancel g := forall x, g (f x) = Some x.
--
--Definition ocancel (g : aT -> option rT) h := forall x, oapp h x (g x) = x.
--
--Lemma can_pcan g : cancel g -> pcancel (fun y => Some (g y)).
--Proof. by move=> fK x; congr (Some _). Qed.
--
--Lemma pcan_inj g : pcancel g -> injective.
--Proof. by move=> fK x y /(congr1 g); rewrite !fK => [[]]. Qed.
--
--Lemma can_inj g : cancel g -> injective.
--Proof. by move/can_pcan; apply: pcan_inj. Qed.
--
--Lemma canLR g x y : cancel g -> x = f y -> g x = y.
--Proof. by move=> fK ->. Qed.
--
--Lemma canRL g x y : cancel g -> f x = y -> x = g y.
--Proof. by move=> fK <-. Qed.
--
--End Injections.
--
--Lemma Some_inj {T} : injective (@Some T). Proof. by move=> x y []. Qed.
--
--(** Force implicits to use as a view. **)
--Prenex Implicits Some_inj.
--
--(** cancellation lemmas for dependent type casts. **)
--Lemma esymK T x y : cancel (@esym T x y) (@esym T y x).
--Proof. by case: y /. Qed.
--
--Lemma etrans_id T x y (eqxy : x = y :> T) : etrans (erefl x) eqxy = eqxy.
--Proof. by case: y / eqxy. Qed.
--
--Section InjectionsTheory.
--
--Variables (A B C : Type) (f g : B -> A) (h : C -> B).
--
--Lemma inj_id : injective (@id A).
--Proof. by []. Qed.
--
--Lemma inj_can_sym f' : cancel f f' -> injective f' -> cancel f' f.
--Proof. by move=> fK injf' x; apply: injf'. Qed.
--
--Lemma inj_comp : injective f -> injective h -> injective (f \o h).
--Proof. by move=> injf injh x y /injf; apply: injh. Qed.
--
--Lemma can_comp f' h' : cancel f f' -> cancel h h' -> cancel (f \o h) (h' \o f').
--Proof. by move=> fK hK x; rewrite /= fK hK. Qed.
--
--Lemma pcan_pcomp f' h' :
-- pcancel f f' -> pcancel h h' -> pcancel (f \o h) (pcomp h' f').
--Proof. by move=> fK hK x; rewrite /pcomp fK /= hK. Qed.
--
--Lemma eq_inj : injective f -> f =1 g -> injective g.
--Proof. by move=> injf eqfg x y; rewrite -2!eqfg; apply: injf. Qed.
--
--Lemma eq_can f' g' : cancel f f' -> f =1 g -> f' =1 g' -> cancel g g'.
--Proof. by move=> fK eqfg eqfg' x; rewrite -eqfg -eqfg'. Qed.
--
--Lemma inj_can_eq f' : cancel f f' -> injective f' -> cancel g f' -> f =1 g.
--Proof. by move=> fK injf' gK x; apply: injf'; rewrite fK. Qed.
--
--End InjectionsTheory.
--
--Section Bijections.
--
--Variables (A B : Type) (f : B -> A).
--
--Variant bijective : Prop := Bijective g of cancel f g & cancel g f.
--
--Hypothesis bijf : bijective.
--
--Lemma bij_inj : injective f.
--Proof. by case: bijf => g fK _; apply: can_inj fK. Qed.
--
--Lemma bij_can_sym f' : cancel f' f <-> cancel f f'.
--Proof.
--split=> fK; first exact: inj_can_sym fK bij_inj.
--by case: bijf => h _ hK x; rewrite -[x]hK fK.
--Qed.
--
--Lemma bij_can_eq f' f'' : cancel f f' -> cancel f f'' -> f' =1 f''.
--Proof.
--by move=> fK fK'; apply: (inj_can_eq _ bij_inj); apply/bij_can_sym.
--Qed.
--
--End Bijections.
--
--Section BijectionsTheory.
--
--Variables (A B C : Type) (f : B -> A) (h : C -> B).
--
--Lemma eq_bij : bijective f -> forall g, f =1 g -> bijective g.
--Proof. by case=> f' fK f'K g eqfg; exists f'; eapply eq_can; eauto. Qed.
--
--Lemma bij_comp : bijective f -> bijective h -> bijective (f \o h).
--Proof.
--by move=> [f' fK f'K] [h' hK h'K]; exists (h' \o f'); apply: can_comp; auto.
--Qed.
--
--Lemma bij_can_bij : bijective f -> forall f', cancel f f' -> bijective f'.
--Proof. by move=> bijf; exists f; first by apply/(bij_can_sym bijf). Qed.
--
--End BijectionsTheory.
--
--Section Involutions.
--
--Variables (A : Type) (f : A -> A).
--
--Definition involutive := cancel f f.
--
--Hypothesis Hf : involutive.
--
--Lemma inv_inj : injective f. Proof. exact: can_inj Hf. Qed.
--Lemma inv_bij : bijective f. Proof. by exists f. Qed.
--
--End Involutions.
--
--Section OperationProperties.
--
--Variables S T R : Type.
--
--Section SopTisR.
--Implicit Type op : S -> T -> R.
--Definition left_inverse e inv op := forall x, op (inv x) x = e.
--Definition right_inverse e inv op := forall x, op x (inv x) = e.
--Definition left_injective op := forall x, injective (op^~ x).
--Definition right_injective op := forall y, injective (op y).
--End SopTisR.
--
--
--Section SopTisS.
--Implicit Type op : S -> T -> S.
--Definition right_id e op := forall x, op x e = x.
--Definition left_zero z op := forall x, op z x = z.
--Definition right_commutative op := forall x y z, op (op x y) z = op (op x z) y.
--Definition left_distributive op add :=
-- forall x y z, op (add x y) z = add (op x z) (op y z).
--Definition right_loop inv op := forall y, cancel (op^~ y) (op^~ (inv y)).
--Definition rev_right_loop inv op := forall y, cancel (op^~ (inv y)) (op^~ y).
--End SopTisS.
--
--Section SopTisT.
--Implicit Type op : S -> T -> T.
--Definition left_id e op := forall x, op e x = x.
--Definition right_zero z op := forall x, op x z = z.
--Definition left_commutative op := forall x y z, op x (op y z) = op y (op x z).
--Definition right_distributive op add :=
-- forall x y z, op x (add y z) = add (op x y) (op x z).
--Definition left_loop inv op := forall x, cancel (op x) (op (inv x)).
--Definition rev_left_loop inv op := forall x, cancel (op (inv x)) (op x).
--End SopTisT.
--
--Section SopSisT.
--Implicit Type op : S -> S -> T.
--Definition self_inverse e op := forall x, op x x = e.
--Definition commutative op := forall x y, op x y = op y x.
--End SopSisT.
--
--Section SopSisS.
--Implicit Type op : S -> S -> S.
--Definition idempotent op := forall x, op x x = x.
--Definition associative op := forall x y z, op x (op y z) = op (op x y) z.
--Definition interchange op1 op2 :=
-- forall x y z t, op1 (op2 x y) (op2 z t) = op2 (op1 x z) (op1 y t).
--End SopSisS.
--
--End OperationProperties.
--
--
--
--
--
--
--
--
--
--
---- a/plugins/ssrmatching/ssrmatching.v
-+++ /dev/null
-@@ -1,36 +0,0 @@
--(************************************************************************)
--(* * The Coq Proof Assistant / The Coq Development Team *)
--(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
--(* <O___,, * (see CREDITS file for the list of authors) *)
--(* \VV/ **************************************************************)
--(* // * This file is distributed under the terms of the *)
--(* * GNU Lesser General Public License Version 2.1 *)
--(* * (see LICENSE file for the text of the license) *)
--(************************************************************************)
--
--(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *)
--
--Declare ML Module "ssrmatching_plugin".
--
--Module SsrMatchingSyntax.
--
--(* Reserve the notation for rewrite patterns so that the user is not allowed *)
--(* to declare it at a different level. *)
--Reserved Notation "( a 'in' b )" (at level 0).
--Reserved Notation "( a 'as' b )" (at level 0).
--Reserved Notation "( a 'in' b 'in' c )" (at level 0).
--Reserved Notation "( a 'as' b 'in' c )" (at level 0).
--
--(* Notation to define shortcuts for the "X in t" part of a pattern. *)
--Notation "( X 'in' t )" := (_ : fun X => t) : ssrpatternscope.
--Delimit Scope ssrpatternscope with pattern.
--
--(* Some shortcuts for recurrent "X in t" parts. *)
--Notation RHS := (X in _ = X)%pattern.
--Notation LHS := (X in X = _)%pattern.
--
--End SsrMatchingSyntax.
--
--Export SsrMatchingSyntax.
--
--Tactic Notation "ssrpattern" ssrpatternarg(p) := ssrpattern p .
---- a/test-suite/Makefile
-+++ b/test-suite/Makefile
-@@ -99,7 +99,7 @@
-
- VSUBSYSTEMS := prerequisite success failure $(BUGS) output \
- output-modulo-time $(INTERACTIVE) micromega $(COMPLEXITY) modules stm \
-- coqdoc ssr
-+ coqdoc
-
- # All subsystems
- SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile tools unit-tests
-@@ -167,7 +167,6 @@
- $(call summary_dir, "Complexity tests", complexity); \
- $(call summary_dir, "Module tests", modules); \
- $(call summary_dir, "STM tests", stm); \
-- $(call summary_dir, "SSR tests", ssr); \
- $(call summary_dir, "IDE tests", ide); \
- $(call summary_dir, "VI tests", vio); \
- $(call summary_dir, "Coqchk tests", coqchk); \
---- a/test-suite/bugs/closed/2800.v
-+++ /dev/null
-@@ -1,19 +0,0 @@
--Goal False.
--
--intuition
-- match goal with
-- | |- _ => idtac " foo"
-- end.
--
-- lazymatch goal with _ => idtac end.
-- match goal with _ => idtac end.
-- unshelve lazymatch goal with _ => idtac end.
-- unshelve match goal with _ => idtac end.
-- unshelve (let x := I in idtac).
--Abort.
--
--Require Import ssreflect.
--
--Goal True.
--match goal with _ => idtac end => //.
--Qed.
---- a/test-suite/bugs/closed/5692.v
-+++ /dev/null
-@@ -1,88 +0,0 @@
--Set Primitive Projections.
--Require Import ZArith ssreflect.
--
--Module Test1.
--
--Structure semigroup := SemiGroup {
-- sg_car :> Type;
-- sg_op : sg_car -> sg_car -> sg_car;
--}.
--
--Structure monoid := Monoid {
-- monoid_car :> Type;
-- monoid_op : monoid_car -> monoid_car -> monoid_car;
-- monoid_unit : monoid_car;
--}.
--
--Coercion monoid_sg (X : monoid) : semigroup :=
-- SemiGroup (monoid_car X) (monoid_op X).
--Canonical Structure monoid_sg.
--
--Parameter X : monoid.
--Parameter x y : X.
--
--Check (sg_op _ x y).
--
--End Test1.
--
--Module Test2.
--
--Structure semigroup := SemiGroup {
-- sg_car :> Type;
-- sg_op : sg_car -> sg_car -> sg_car;
--}.
--
--Structure monoid := Monoid {
-- monoid_car :> Type;
-- monoid_op : monoid_car -> monoid_car -> monoid_car;
-- monoid_unit : monoid_car;
-- monoid_left_id x : monoid_op monoid_unit x = x;
--}.
--
--Coercion monoid_sg (X : monoid) : semigroup :=
-- SemiGroup (monoid_car X) (monoid_op X).
--Canonical Structure monoid_sg.
--
--Canonical Structure nat_sg := SemiGroup nat plus.
--Canonical Structure nat_monoid := Monoid nat plus 0 plus_O_n.
--
--Lemma foo (x : nat) : 0 + x = x.
--Proof.
--apply monoid_left_id.
--Qed.
--
--End Test2.
--
--Module Test3.
--
--Structure semigroup := SemiGroup {
-- sg_car :> Type;
-- sg_op : sg_car -> sg_car -> sg_car;
--}.
--
--Structure group := Something {
-- group_car :> Type;
-- group_op : group_car -> group_car -> group_car;
-- group_neg : group_car -> group_car;
-- group_neg_op' x y : group_neg (group_op x y) = group_op (group_neg x) (group_neg y)
--}.
--
--Coercion group_sg (X : group) : semigroup :=
-- SemiGroup (group_car X) (group_op X).
--Canonical Structure group_sg.
--
--Axiom group_neg_op : forall (X : group) (x y : X),
-- group_neg X (sg_op (group_sg X) x y) = sg_op (group_sg X) (group_neg X x) (group_neg X y).
--
--Canonical Structure Z_sg := SemiGroup Z Z.add .
--Canonical Structure Z_group := Something Z Z.add Z.opp Z.opp_add_distr.
--
--Lemma foo (x y : Z) :
-- sg_op Z_sg (group_neg Z_group x) (group_neg Z_group y) =
-- group_neg Z_group (sg_op Z_sg x y).
--Proof.
-- rewrite -group_neg_op.
-- reflexivity.
--Qed.
--
--End Test3.
---- a/test-suite/bugs/closed/6634.v
-+++ /dev/null
-@@ -1,6 +0,0 @@
--From Coq Require Import ssreflect.
--
--Lemma normalizeP (p : tt = tt) : p = p.
--Proof.
--Fail move: {2} tt p.
--Abort.
---- a/test-suite/bugs/closed/6910.v
-+++ /dev/null
-@@ -1,5 +0,0 @@
--From Coq Require Import ssreflect ssrfun.
--
--(* We should be able to use Some_inj as a view: *)
--Lemma foo (x y : nat) : Some x = Some y -> x = y.
--Proof. by move/Some_inj. Qed.
---- a/test-suite/bugs/closed/bug_8544.v
-+++ /dev/null
-@@ -1,6 +0,0 @@
--Require Import ssreflect.
--Goal True \/ True -> False.
--Proof.
--(* the following should fail: 2 subgoals, but only one intro pattern *)
--Fail case => [a].
--Abort.
---- a/test-suite/output/ssr_clear.v
-+++ /dev/null
-@@ -1,6 +0,0 @@
--Require Import ssreflect.
--
--Example foo : True -> True.
--Proof.
--Fail move=> {NO_SUCH_NAME}.
--Abort.
---- a/test-suite/output/ssr_explain_match.v
-+++ /dev/null
-@@ -1,23 +0,0 @@
--(************************************************************************)
--(* * The Coq Proof Assistant / The Coq Development Team *)
--(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
--(* <O___,, * (see CREDITS file for the list of authors) *)
--(* \VV/ **************************************************************)
--(* // * This file is distributed under the terms of the *)
--(* * GNU Lesser General Public License Version 2.1 *)
--(* * (see LICENSE file for the text of the license) *)
--(************************************************************************)
--
--Require Import ssrmatching.
--Require Import ssreflect ssrbool TestSuite.ssr_mini_mathcomp.
--
--Definition addnAC := (addnA, addnC).
--
--Lemma test x y z : x + y + z = x + y.
--
--ssrinstancesoftpat (_ + _).
--ssrinstancesofruleL2R addnC.
--ssrinstancesofruleR2L addnA.
--ssrinstancesofruleR2L addnAC.
--Fail ssrinstancesoftpat (_ + _ in RHS). (* Not implemented *)
--Admitted.
---- a/test-suite/success/ssrpattern.v
-+++ /dev/null
-@@ -1,22 +0,0 @@
--Require Import ssrmatching.
--
--(*Set Debug SsrMatching.*)
--
--Tactic Notation "at" "[" ssrpatternarg(pat) "]" tactic(t) :=
-- let name := fresh in
-- let def_name := fresh in
-- ssrpattern pat;
-- intro name;
-- pose proof (refl_equal name) as def_name;
-- unfold name at 1 in def_name;
-- t def_name;
-- [ rewrite <- def_name | idtac.. ];
-- clear name def_name.
--
--Lemma test (H : True -> True -> 3 = 7) : 28 = 3 * 4.
--Proof.
--at [ X in X * 4 ] ltac:(fun place => rewrite -> H in place).
--- reflexivity.
--- trivial.
--- trivial.
--Qed.
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-09 19:57:12 +0000