From 54b3b3d9d50cfac0fe206ee7a19d6abcc2ee702a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Maxime=20D=C3=A9n=C3=A8s?= Date: Mon, 18 Feb 2019 11:28:00 +0000 Subject: [PATCH 1/2] Stdlib2: get started MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Maxime Dénès Co-authored-by: Vincent Laporte --- src/.gitignore | 6 + src/_CoqProject | 19 + src/abstract.v | 37 + src/bool.v | 2010 +++++++++++++++++++++++++++++++++++++++++ src/bootstrap | 3 + src/congr.v | 28 + src/datatypes.v | 132 +++ src/decimal.v | 177 ++++ src/equality.v | 91 ++ src/functions.v | 744 +++++++++++++++ src/lock.v | 79 ++ src/matching.v | 30 + src/nat.v | 50 + src/prelude.v | 44 + src/prelude_plugins.v | 6 + src/prop.v | 121 +++ src/ssreflect.v | 320 +++++++ 17 files changed, 3897 insertions(+) create mode 100644 src/.gitignore create mode 100644 src/_CoqProject create mode 100644 src/abstract.v create mode 100644 src/bool.v create mode 100755 src/bootstrap create mode 100644 src/congr.v create mode 100644 src/datatypes.v create mode 100644 src/decimal.v create mode 100644 src/equality.v create mode 100644 src/functions.v create mode 100644 src/lock.v create mode 100644 src/matching.v create mode 100644 src/nat.v create mode 100644 src/prelude.v create mode 100644 src/prelude_plugins.v create mode 100644 src/prop.v create mode 100644 src/ssreflect.v diff --git a/src/.gitignore b/src/.gitignore new file mode 100644 index 0000000..d8b9383 --- /dev/null +++ b/src/.gitignore @@ -0,0 +1,6 @@ +Makefile +Makefile.conf +.coqdeps.d +*.vo +*.glob +.*.aux diff --git a/src/_CoqProject b/src/_CoqProject new file mode 100644 index 0000000..3889766 --- /dev/null +++ b/src/_CoqProject @@ -0,0 +1,19 @@ +-arg -noinit +-arg -w +-arg +non-primitive-record +-R . Stdlib + +abstract.v +bool.v +congr.v +datatypes.v +decimal.v +equality.v +functions.v +lock.v +nat.v +prelude.v +prelude_plugins.v +prop.v +ssreflect.v +matching.v diff --git a/src/abstract.v b/src/abstract.v new file mode 100644 index 0000000..51de114 --- /dev/null +++ b/src/abstract.v @@ -0,0 +1,37 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* " := (abstract _ n _). +Notation "T (* n *)" := (abstract T n abstract_key). + +Register abstract_lock as plugins.ssreflect.abstract_lock. +Register abstract_key as plugins.ssreflect.abstract_key. +Register abstract as plugins.ssreflect.abstract. + +(* 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. diff --git a/src/bool.v b/src/bool.v new file mode 100644 index 0000000..9204d43 --- /dev/null +++ b/src/bool.v @@ -0,0 +1,2010 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* .doc { font-family: monospace; white-space: pre; } # **) + +Require Import functions. +Require Import lock. +Import prelude ssreflect prop equality datatypes nat. + +(********************************************************************) +(** * The boolean datatype *) + +(** [bool] is the datatype of the boolean values [true] and [false] *) + +Variant bool := +| true : bool +| false : bool. + +Add Printing If bool. + +Declare Scope bool_scope. +Delimit Scope bool_scope with bool. +Bind Scope bool_scope with bool. + +Register bool as core.bool.type. +Register true as core.bool.true. +Register false as core.bool.false. + + +(** Basic boolean operators *) + +Definition andb (b1 b2:bool) : bool := if b1 then b2 else false. + +Definition orb (b1 b2:bool) : bool := if b1 then true else b2. + +Definition implb (b1 b2:bool) : bool := if b1 then b2 else true. + +Definition xorb (b1 b2:bool) : bool := + match b1, b2 with + | true, true => false + | true, false => true + | false, true => true + | false, false => false + end. + +Definition negb (b:bool) := if b then false else true. + +Infix "||" := orb (at level 50, left associativity) : bool_scope. +Infix "&&" := andb (at level 40, left associativity) : bool_scope. + +Register andb as core.bool.andb. +Register orb as core.bool.orb. +Register xorb as core.bool.xorb. +Register negb as core.bool.negb. + +(** + 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 Warnings "-projection-no-head-constant". + +(* 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. *) + +Declare Scope general_if_scope. +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. *) + +Declare Scope boolean_if_scope. +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. + +(*****************************************) +(** * Reflect: a specialized inductive type for + relating propositions and booleans, + as popularized by the Ssreflect library. *) +(*****************************************) + +Variant reflect (P : Prop) : bool -> Type := + | ReflectT : P -> reflect P true + | ReflectF : ~ P -> reflect P false. +Hint Constructors reflect : bool. + +(** Interest: a case on a reflect lemma or hyp performs clever + unification, and leave the goal in a convenient shape + (a bit like case_eq). *) + +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 **) +Local 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. + +(** Interpretation of booleans as propositions **) +Definition is_true b := b = true. +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 : core. + +(* 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: eq_sym; trivial] + | discriminate | contradiction | split] + | case not_locked_false_eq_true; assumption + | match goal with H : ~ _ |- _ => solve [case H; trivial] end ]. + +(** 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 isLeft A B (u : A + B) := if u is Left _ then true else false. + +Prenex Implicits isSome isLeft. + +Definition decidable (P: Prop) : Type := 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: T -> Prop) : 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. **) + +Variant and3 (P1 P2 P3 : Prop) : Prop := And3 of P1 & P2 & P3. + +Variant and4 (P1 P2 P3 P4 : Prop) : Prop := And4 of P1 & P2 & P3 & P4. + +Variant and5 (P1 P2 P3 P4 P5 : Prop) : Prop := + And5 of P1 & P2 & P3 & P4 & P5. + +Variant or3 (P1 P2 P3 : Prop) : Prop := Or31 of P1 | Or32 of P2 | Or33 of P3. + +Variant 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. + case b1; first by do 2 left. + case b2; first by left; right. + by right; 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. + case: b1; last by do 2 left. + case: b2; last by left; right. + by right; case. +Qed. + +Lemma norP : reflect (~~ b1 /\ ~~ b2) (~~ (b1 || b2)). +Proof. + case: b1; first by right; case. + case: b2; first by right; case. + by left. +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]). + +(* Set Warnings "-non-primitive-record". *) +Unset Primitive Projections. +Structure predType := PredType { + pred_sort :> Type; + topred : pred_sort -> pred T; + _predType_2: {mem | isMem topred mem} +}. +Set Primitive Projections. + +Definition mkPredType pT toP := PredType (exist (@isMem pT toP) _ eq_refl). + +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 \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_2 : manifest_applicative_pred_value = p +}. +Definition ApplicativePred p := ManifestApplicativePred (eq_refl 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_2 : manifest_simpl_pred_value = SimplPred p +}. +Canonical expose_simpl_pred p := ManifestSimplPred (eq_refl (SimplPred p)). + +Structure manifest_mem_pred p := ManifestMemPred { + manifest_mem_pred_value :> mem_pred T; + _manifest_mem_pred_2 : manifest_mem_pred_value= Mem [eta p] +}. +Canonical expose_mem_pred p := @ManifestMemPred p _ eq_refl. + +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. + +Local Open Scope nat_scope. + +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; _keyed_pred_1 : 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; _keyed_qualifier_1 : unkey_qualifier = q}. +Definition KeyedQualifier k := PackKeyedQualifier k (eq_refl 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. diff --git a/src/bootstrap b/src/bootstrap new file mode 100755 index 0000000..9d71478 --- /dev/null +++ b/src/bootstrap @@ -0,0 +1,3 @@ +#!/bin/sh + +coq_makefile -f _CoqProject -o Makefile diff --git a/src/congr.v b/src/congr.v new file mode 100644 index 0000000..9fbd482 --- /dev/null +++ b/src/congr.v @@ -0,0 +1,28 @@ +Require Import prelude ssreflect equality nat abstract. + +(* 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. + +Register nary_congruence as plugins.ssreflect.nary_congruence. +Register ssr_congr_arrow as plugins.ssreflect.ssr_congr_arrow. diff --git a/src/datatypes.v b/src/datatypes.v new file mode 100644 index 0000000..6364249 --- /dev/null +++ b/src/datatypes.v @@ -0,0 +1,132 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* 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). + +(** Inversion principles *) +Definition optionI A (oa oa': option A) (e: oa = oa') : + if oa is Some a then if oa' is Some a' then a = a' else False else if oa' is Some _ then False else True + := + let: eq_refl := e in + if oa is Some a then eq_refl else I. + +(** [prod A B], written [A * B], is the product of [A] and [B]; + the pair [pair A B a b] of [a] and [b] is abbreviated [(a,b)] *) + +#[universes(template)] +Record prod (A B : Type) : Type := + pair { fst : A; snd : B }. + +Arguments pair {A B} _ _. + +Declare Scope pair_scope. +Delimit Scope pair_scope with PAIR. +Open Scope pair_scope. + +Reserved Notation "x * y" (at level 40, left associativity). +Notation "x * y" := (prod x y) : type_scope. + +Reserved Notation "( x , y , .. , z )" (at level 0). +Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : pair_scope. + +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) := (and_proj1 PandQ, and_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). + +Definition prod_rect (A B: Type) (T: prod A B -> Type) (h: forall (a: A) (b: B), T (a, b)) p : T p := + let: (a, b) := p in h a b. + +Register prod as core.prod.type. +Register pair as core.prod.intro. +Register prod_rect as core.prod.rect. + +Register fst as core.prod.proj1. +Register snd as core.prod.proj2. + +(** [(sig A P)], or more suggestively [{x:A | P x}], denotes the subset + of elements of the type [A] which satisfy the predicate [P]. + Similarly [(sig2 A P Q)], or [{x:A | P x & Q x}], denotes the subset + of elements of the type [A] which satisfy both [P] and [Q]. *) + +Record sig (A : Type) (P : A -> Type) : Type := + exist { sig_proj1 : A; sig_proj2 : P sig_proj1 }. + +Arguments exist {A} _. + +Record sig2 (A : Type) (P Q : A -> Type) : Type := + exist2 { sig2_proj1 : A; sig2_proj2 : P sig2_proj1; sig2_proj3 : Q sig2_proj1 }. + +Arguments exist2 {A} _ _. + +Reserved Notation "{ x | P }" (at level 0, x at level 99). +Reserved Notation "{ x | P & Q }" (at level 0, x at level 99). + +Reserved Notation "{ x : A | P }" (at level 0, x at level 99). +Reserved Notation "{ x : A | P & Q }" (at level 0, x at level 99). + +Notation "{ x | P }" := (sig (fun x => P)) : type_scope. +Notation "{ x | P & Q }" := (sig2 (fun x => P) (fun x => Q)) : type_scope. +Notation "{ x : A | P }" := (sig (A:=A) (fun x => P)) : type_scope. +Notation "{ x : A | P & Q }" := (sig2 (A:=A) (fun x => P) (fun x => Q)) : + type_scope. + +(** [sum A B], also noted [A + B] is the disjoint sum of datatypes [A] and [B]. *) +Variant sum A B : Type := +| Left of A +| Right of B. + +Infix "+" := sum (at level 50, left associativity) : type_scope. + +Arguments Left {A B} _. +Arguments Right {A B} _. diff --git a/src/decimal.v b/src/decimal.v new file mode 100644 index 0000000..6729f3e --- /dev/null +++ b/src/decimal.v @@ -0,0 +1,177 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* nzhead d + | _ => d + end. + +(** [unorm] : normalization of unsigned integers *) + +Definition unorm d := + match nzhead d with + | Nil => zero + | d => d + end. + +(** [norm] : normalization of signed integers *) + +Definition norm d := + match d with + | Pos d => Pos (unorm d) + | Neg d => + match nzhead d with + | Nil => Pos zero + | d => Neg d + end + end. + +(** A few easy operations. For more advanced computations, use the conversions + with other Coq numeral datatypes (e.g. Z) and the operations on them. *) + +Definition opp (d:int) := + match d with + | Pos d => Neg d + | Neg d => Pos d + end. + +(** For conversions with binary numbers, it is easier to operate + on little-endian numbers. *) + +Fixpoint revapp (d d' : uint) := + match d with + | Nil => d' + | D0 d => revapp d (D0 d') + | D1 d => revapp d (D1 d') + | D2 d => revapp d (D2 d') + | D3 d => revapp d (D3 d') + | D4 d => revapp d (D4 d') + | D5 d => revapp d (D5 d') + | D6 d => revapp d (D6 d') + | D7 d => revapp d (D7 d') + | D8 d => revapp d (D8 d') + | D9 d => revapp d (D9 d') + end. + +Definition rev d := revapp d Nil. + +Module Little. + +(** Successor of little-endian numbers *) + +Fixpoint succ d := + match d with + | Nil => D1 Nil + | D0 d => D1 d + | D1 d => D2 d + | D2 d => D3 d + | D3 d => D4 d + | D4 d => D5 d + | D5 d => D6 d + | D6 d => D7 d + | D7 d => D8 d + | D8 d => D9 d + | D9 d => D0 (succ d) + end. + +(** Doubling little-endian numbers *) + +Fixpoint double d := + match d with + | Nil => Nil + | D0 d => D0 (double d) + | D1 d => D2 (double d) + | D2 d => D4 (double d) + | D3 d => D6 (double d) + | D4 d => D8 (double d) + | D5 d => D0 (succ_double d) + | D6 d => D2 (succ_double d) + | D7 d => D4 (succ_double d) + | D8 d => D6 (succ_double d) + | D9 d => D8 (succ_double d) + end + +with succ_double d := + match d with + | Nil => D1 Nil + | D0 d => D1 (double d) + | D1 d => D3 (double d) + | D2 d => D5 (double d) + | D3 d => D7 (double d) + | D4 d => D9 (double d) + | D5 d => D1 (succ_double d) + | D6 d => D3 (succ_double d) + | D7 d => D5 (succ_double d) + | D8 d => D7 (succ_double d) + | D9 d => D9 (succ_double d) + end. + +End Little. + +(** Pseudo-conversion functions used when declaring + Numeral Notations on [uint] and [int]. *) + +Definition uint_of_uint (i:uint) := i. +Definition int_of_int (i:int) := i. diff --git a/src/equality.v b/src/equality.v new file mode 100644 index 0000000..ecfa186 --- /dev/null +++ b/src/equality.v @@ -0,0 +1,91 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* A]. This is Leibniz equality + as it expresses that [x] and [y] are equal iff every property on + [A] which is true of [x] is also true of [y] *) + +Reserved Notation "x = y :> T" +(at level 70, y at next level, no associativity). +Reserved Notation "x = y" (at level 70, no associativity). +Reserved Notation "x = y = z" +(at level 70, no associativity, y at next level). + +Inductive eq (A : Type) (x : A) : A -> Prop := + eq_refl : x = x :> A + +where "x = y :> A" := (@eq A x y) : type_scope. + +Register eq as core.eq.type. +Register eq_refl as core.eq.refl. +Register eq_ind as core.eq.ind. +Register eq_rect as core.eq.rect. + +Reserved Notation "x <> y :> T" +(at level 70, y at next level, no associativity). +Reserved Notation "x <> y" (at level 70, no associativity). + +Notation "x = y" := (x = y :>_) : type_scope. +Notation "x <> y :> T" := (~ x = y :> T) : type_scope. +Notation "x <> y" := (x <> y :>_) : type_scope. + +Arguments eq {A} x _. +Prenex Implicits eq_refl. +Arguments eq_refl {A x}, {A} x. + +Arguments eq_ind [A] x P _ y _. +Arguments eq_rec [A] x P _ y _. +Arguments eq_rect [A] x P _ y _. + +Definition eq_rect_dep A (x: A) (P: forall y, x = y -> Type) (ih: P x (eq_refl x)) y (e: x = y) : P y e := + let: eq_refl := e in ih. + +Section equality. + +Context {A B : Type} (f : A -> B) {x y z : A}. + +Definition eq_sym : x = y -> y = x := + fun e => let: eq_refl := e in eq_refl. + +Definition eq_trans : x = y -> y = z -> x = z := + fun e => let: eq_refl := e in fun f => f. + +Definition eq_congr1 : x = y -> f x = f y := + fun e => let: eq_refl := e in eq_refl. + +End equality. + +Register eq_sym as core.eq.sym. +Register eq_trans as core.eq.trans. +Register eq_congr1 as core.eq.congr. + +Definition eq_rect_r A (x: A) (P: A -> Type) (ih: P x) y (e: y = x) : P y := + eq_rect x P ih y (eq_sym e). + +Definition eq_ind_r := eq_rect_r. + +Lemma neq_sym A (x y : A) : x <> y -> y <> x. +Proof. by move=> neq_xy /eq_sym. Qed. + +(* A predicate for singleton types. *) +Definition all_equal_to T (x0 : T) := forall x, unkeyed x = x0. + +Ltac done := + trivial; hnf; intros; solve + [ do ![solve [trivial | apply: eq_sym; trivial] + | discriminate | contradiction | split] + | match goal with H : ~ _ |- _ => solve [case H; trivial] end ]. diff --git a/src/functions.v b/src/functions.v new file mode 100644 index 0000000..2510104 --- /dev/null +++ b/src/functions.v @@ -0,0 +1,744 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* .doc { font-family: monospace; white-space: pre; } # **) + +Require Import prelude ssreflect prop datatypes equality congr. + + +(** + 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!. **) + + +Declare Scope fun_scope. +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. + +(** Shorthand for some basic equality lemmas. **) + +Notation ecast i T e x := (let: eq_refl in _ = i := e return T in x). + +(** 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 : core. + +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, left associativity, format "f1 \o '/ ' f2") : fun_scope. +Infix "∘" := comp (at level 50, left associativity) : 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 := sig_proj1. +Definition tagged : forall w, T_(tag w) := @sig_proj2 I [eta T_]. +Definition Tagged x := @exist I [eta T_] i x. + +Definition tag2 (w : @sig2 I T_ U_) := sig2_proj1 w. +Definition tagged2 w : T_(tag2 w) := sig2_proj2 w. +Definition tagged2' w : U_(tag2 w) := sig2_proj3 w. +Definition Tagged2 x y := @exist2 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 : @sig2 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 := (@sig_proj1 _ _). +Notation "@ 'sval'" := (@sig_proj1) (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) := sig2_proj1 u. + +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: I -> Prop) (u : @sig I P) := Tagged P (svalP u). + +Coercion sig_of_sig2 I (P Q: I -> Prop) (u : @sig2 I P Q) := + exist (fun i => P i /\ Q i) (s2val u) (and_intro (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 /(eq_congr1 g) /optionI; 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 /optionI. Qed. + +(** Force implicits to use as a view. **) +Prenex Implicits Some_inj. + +(** cancellation lemmas for dependent type casts. **) +Lemma eq_symK T x y : cancel (@eq_sym T x y) (@eq_sym T y x). +Proof. by case: y /. Qed. + +Lemma eq_trans_id T x y (eqxy : x = y :> T) : eq_trans (eq_refl 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. diff --git a/src/lock.v b/src/lock.v new file mode 100644 index 0000000..182cd63 --- /dev/null +++ b/src/lock.v @@ -0,0 +1,79 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* x. + +Register master_key as plugins.ssreflect.master_key. +Register locked as plugins.ssreflect.locked. + +Lemma lock A x : x = locked x :> A. Proof. unlock; reflexivity. Qed. + +(* To unlock opaque constants. *) +Structure unlockable T v := Unlockable { unlocked : T; unlocked_prop : 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. + diff --git a/src/matching.v b/src/matching.v new file mode 100644 index 0000000..a751f00 --- /dev/null +++ b/src/matching.v @@ -0,0 +1,30 @@ +(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) +(* Distributed under the terms of CeCILL-B. *) + +Require Import ssreflect equality. +Local Open Scope type_scope. + +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). + +Declare Scope ssrpatternscope. +Delimit Scope ssrpatternscope with pattern. + +(* Notation to define shortcuts for the "X in t" part of a pattern. *) +Notation "( X 'in' t )" := (_ : fun X => t) : ssrpatternscope. + +(* 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 . diff --git a/src/nat.v b/src/nat.v new file mode 100644 index 0000000..28ff8d4 --- /dev/null +++ b/src/nat.v @@ -0,0 +1,50 @@ +Require Import prelude ssreflect datatypes decimal. + +Inductive nat := +| O +| S of nat. + +Register nat as num.nat.type. +Register O as num.nat.O. +Register S as num.nat.S. + +Declare Scope nat_scope. + +Arguments S _%nat_scope. + +Fixpoint tail_add (m n: nat) : nat := + if m is S m' then tail_add m' (S n) else n. + +Fixpoint tail_addmul (r m n: nat) : nat := + if m is S m' then tail_addmul (tail_add n r) m' n else r. + +Definition tail_mul n m := tail_addmul O n m. + +(** ** Conversion with a decimal representation for printing/parsing *) + +Local Notation ten := (S (S (S (S (S (S (S (S (S (S O)))))))))). + +Fixpoint of_uint_acc (d: uint) (acc: nat) := + match d with + | Nil => acc + | D0 d => of_uint_acc d (tail_mul ten acc) + | D1 d => of_uint_acc d (S (tail_mul ten acc)) + | D2 d => of_uint_acc d (S (S (tail_mul ten acc))) + | D3 d => of_uint_acc d (S (S (S (tail_mul ten acc)))) + | D4 d => of_uint_acc d (S (S (S (S (tail_mul ten acc))))) + | D5 d => of_uint_acc d (S (S (S (S (S (tail_mul ten acc)))))) + | D6 d => of_uint_acc d (S (S (S (S (S (S (tail_mul ten acc))))))) + | D7 d => of_uint_acc d (S (S (S (S (S (S (S (tail_mul ten acc)))))))) + | D8 d => of_uint_acc d (S (S (S (S (S (S (S (S (tail_mul ten acc))))))))) + | D9 d => of_uint_acc d (S (S (S (S (S (S (S (S (S (tail_mul ten acc)))))))))) + end. + +Definition of_uint (d: uint) := of_uint_acc d O. + +Definition to_little_uint (n: nat) (acc: uint) : uint := + nat_rect acc (λ _, Little.succ) n. + +Definition to_uint (n: nat) : uint := + decimal.rev (to_little_uint n decimal.zero). + +Numeral Notation nat of_uint to_uint : nat_scope. diff --git a/src/prelude.v b/src/prelude.v new file mode 100644 index 0000000..9c3ac54 --- /dev/null +++ b/src/prelude.v @@ -0,0 +1,44 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* y" (at level 99, right associativity, y at level 200). +Notation "A -> B" := (forall (_ : A), B) : type_scope. +Notation "'λ' x .. y , t" := (fun x => .. (fun y => t) ..) + (at level 200, x binder, y binder, right associativity, + format "'[ ' '[ ' 'λ' x .. y ']' , '/' t ']'"). diff --git a/src/prelude_plugins.v b/src/prelude_plugins.v new file mode 100644 index 0000000..d2d9955 --- /dev/null +++ b/src/prelude_plugins.v @@ -0,0 +1,6 @@ +Require Import prelude. + +(** Plugins loaded initially *) +Declare ML Module "ssrmatching_plugin". +Declare ML Module "ssreflect_plugin". +Declare ML Module "numeral_notation_plugin". diff --git a/src/prop.v b/src/prop.v new file mode 100644 index 0000000..923d50d --- /dev/null +++ b/src/prop.v @@ -0,0 +1,121 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* y" (at level 95, no associativity). +Reserved Notation "x \/ y" (at level 85, right associativity). +Reserved Notation "x ∨ y" (at level 85, right associativity). +Reserved Notation "x /\ y" (at level 80, right associativity). +Reserved Notation "x ∧ y" (at level 80, right associativity). +Reserved Notation "~ x" (at level 75, right associativity). +Reserved Notation "¬ x" (at level 75, right associativity). + +(** [True] is the always true proposition *) + +Variant True : Prop := + I : True. + +Register True as core.True.type. +Register I as core.True.I. + +(** [False] is the always false proposition *) + +Inductive False : Prop :=. + +Register False as core.False.type. + +(** [not A], written [~A], is the negation of [A] *) +Definition not (A : Prop) := A -> False. + +Notation "~ x" := (not x) : type_scope. +Notation "¬ x" := (not x) : type_scope. + +Register not as core.not.type. + +(** Create the “core” hint database, and set its transparent state for + variables and constants explicitely. *) +Create HintDb core. +Hint Variables Opaque : core. +Hint Constants Opaque : core. + +Hint Unfold not: core. + +(* The basic closing tactic "done". *) +Ltac done := + trivial; hnf; intros; solve + [ do ![solve trivial + | discriminate | contradiction | split] + | match goal with H : ~ _ |- _ => solve [case H; trivial] end ]. + +(** [and A B], written [A /\ B], is the conjunction of [A] and [B] + + [and_intro p q] is a proof of [A /\ B] as soon as + [p] is a proof of [A] and [q] a proof of [B] + + [and_fst] and [and_snd] are first and second projections of a conjunction *) + +Record and (A B : Prop) : Prop := + and_intro { and_proj1 : A; and_proj2 : B }. + +Notation "A /\ B" := (and A B) : type_scope. +Infix "∧" := and : type_scope. + +Variant or (A B: Prop) : Prop := +| OrL of A +| OrR of B. + +Infix "\/" := or : type_scope. +Infix "∨" := or : type_scope. + +Register or as core.or.type. + +Record iff (A B : Prop) : Prop := + iff_intro { iff_proj1 : A -> B; iff_proj2 : B -> A }. +Notation "A <-> B" := (iff A B) : type_scope. + +(* 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. + +(** Existential quantification *) +Variant ex A (P: A -> Type) : Prop := +| Ex a of P a. + +Notation "'exists' x .. y , p" := (ex (fun x => .. (ex (fun y => p)) ..)) + (at level 200, x binder, right associativity, + format "'[' 'exists' '/ ' x .. y , '/ ' p ']'") +: type_scope. + +Register ex as core.ex.type. + +Variant ex2 A (P Q: A -> Type) : Prop := +| Ex2 a of P a & Q a. + +Notation "'exists2' x , p & q" := (ex2 (fun x => p) (fun x => q)) + (at level 200, x ident, p at level 200, right associativity) : type_scope. diff --git a/src/ssreflect.v b/src/ssreflect.v new file mode 100644 index 0000000..ab179f0 --- /dev/null +++ b/src/ssreflect.v @@ -0,0 +1,320 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* .doc { font-family: monospace; white-space: pre; } # **) + +Require Export prelude_plugins. +Import prelude. + +(** + 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. **) + +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 "" (at level 200). +Reserved Notation "T (* n *)" (at level 200, format "T (* n *)"). + +End SsrSyntax. + +Export SsrSyntax. + +(** + To define notations for tactic in intro patterns. + When "=> /t" is parsed, "t:%ssripat" is actually interpreted. **) +Declare Scope ssripat_scope. +Delimit Scope ssripat_scope with ssripat. + +(** + 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. **) +Declare Scope form_scope. +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. + +(** + 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. + +Register protect_term as plugins.ssreflect.protect_term. + +(** + 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). + +(** + 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. **) + + +(** The basic closing tactic "done". **) +Ltac done := + trivial; hnf; intros; solve + [ do ![solve trivial + | discriminate | contradiction | split] + ]. + +(** 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]. + +Register ssr_have as plugins.ssreflect.ssr_have. +Register ssr_have_let as plugins.ssreflect.ssr_have_let. + +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]. + +Register ssr_suff as plugins.ssreflect.ssr_suff. +Register ssr_wlog as plugins.ssreflect.ssr_wlog. From 43bd423e48f83f5673ac2e4be10bafdadbca2a21 Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Wed, 20 Feb 2019 16:36:36 +0000 Subject: [PATCH 2/2] Update README, adds CONTRIBUTING --- CONTRIBUTING.md | 81 +++++++++++++++++++++++++++++++++++++++++++++++++ README.md | 27 +++++++++++------ 2 files changed, 99 insertions(+), 9 deletions(-) create mode 100644 CONTRIBUTING.md diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md new file mode 100644 index 0000000..ea7fe50 --- /dev/null +++ b/CONTRIBUTING.md @@ -0,0 +1,81 @@ +# Contribution Guide + +This guide describes the styling conventions that are applicable to the +development of this library. + +This file is not comprehensive yet, it contains mistakes and unclear +indications, and some topics may have been overlooked: please consider improving +it. + +## Layout of the file system + +### Naming of files + +## Statements of lemmas, theorems and definitions. + +- Universal quantifications with dependent variable should appear on the left hand side of the colon, until we reach the first non dependent variables. e.g. + `Lemma example x y : x < y -> x >= y = false` + +### Naming of variables + +- Hypothesis should not be named `H`, `H'`,... but have meaningful names. For + example, an hypothesis `n > 0` should be named `n_gt0`. + +### Naming conventions + +To be defined… + +## Proof style + +### General guidelines + +- **A line should have no more than 80 characters**. What a +character is is subject to interpretation. If a line is longer than that, +it should be cut semantically. If there is no way to make a semantic +cut (e.g. the user provides an explicit term that is too long to fit on +one line), then just cut it over several lines to make it readable. + +### White space + +- Operators are surrounded by space, for example `n*m` should be written `n * m`. + +We write +- `move=>` and `move:` (no space between `move` and `=>` or `:`) +- `apply/` and `apply:` (no space between `apply` and `/` or `:`) +- `rewrite /definition` (there is a space between `rewrite` and an unfold) + +### Indentation in proof scripts + +- Lines end with a point `.` and only have `;` inside them. +- Lines that close a goal must start with a terminator (`by` or + `exact`). +- When two subgoals are created, the first subgoal is indented by 2 + spaces, the second is not. Use `last first` to bring the + smallest/less meaningful goal first, and keep the main flow of the + proof unindented. +- When more than two subgoals are created, bullets are used `-` for + the first level, `+` for the second and `*` for the third as in: + ``` + tactic. + - tactic. + + tactic. + * tactic. + * tactic. + * tactic. + + tactic. + + tactic. + - tactic + - tactic + ``` + + If all the subgoals have the same importance, use bullets for all of + them, however, if one goal is more important than the others + (i.e. is main flow of the proof). Then you might remove the bullet + for this last one and unindent it as in: + ``` + tactic. + - tactic. (* secondary subgoal 1 *) + - tactic. (* secondary subgoal 2 *) + tactic. (* third subgoal is the main one *) + ``` + diff --git a/README.md b/README.md index b6dc785..b170f6f 100644 --- a/README.md +++ b/README.md @@ -2,18 +2,27 @@ The purpose of this project is to design and implement a new standard library for Coq. It will follow a clean slate approach, not aiming at compatibility with the current library, which will be maintained separately. +## Organization + This project is coordinated by @maximedenes and can be discussed and followed at: https://github.com/coq/coq/issues/7711 and https://github.com/orgs/coq/projects/1 We foresee several stages: -- Preliminary clean-up and infrastructure work -- Implementation of prelude and basic tactics -- Experimentation on existing libraries (for example, to compare canonical - structures and type classes) -- Implementation of the first components of the library -- Extensions of the library + 1. Preliminary clean-up and infrastructure work + 1. Implementation of prelude and basic tactics + 1. Enhancement of the core of the library. + 1. First release. + 1. Implementation of the first components of the library + 1. Extensions of the library + +## Current status + +The project is currently (February 2019) in its second phase (starting the +actual implementation). + +Questions and discussions are welcome at this stage. In particular, the wiki and +issues (as opposed to code reviews) can be used to share and discuss opinions. -The project is currently in its first phase. Questions and discussions are -welcome at this stage. External code contribution will be integrated during the -last two phases. +External code contribution will be integrated during the last two phases. See +[CONTRIBUTING.md](contributing guide)