From dd86e52d653d189a531a8782c3f3b1a69addaf0e Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Wed, 29 May 2019 20:15:12 +0200 Subject: [PATCH] Cyril: updating order using @pi8027 branch expriment/order of mathcomp --- .travis.yml | 4 + opam | 5 +- order.v | 3109 ++++++++++++++++++++++++++++++++------------------- set.v | 69 +- shell.nix | 2 +- 5 files changed, 2030 insertions(+), 1159 deletions(-) diff --git a/.travis.yml b/.travis.yml index d389b63..d04ec66 100644 --- a/.travis.yml +++ b/.travis.yml @@ -17,6 +17,10 @@ env: - DOCKERIMAGE="mathcomp/mathcomp:1.8.0-coq-8.7" - DOCKERIMAGE="mathcomp/mathcomp:1.8.0-coq-8.8" - DOCKERIMAGE="mathcomp/mathcomp:1.8.0-coq-8.9" + - DOCKERIMAGE="mathcomp/mathcomp:1.9.0-coq-8.7" + - DOCKERIMAGE="mathcomp/mathcomp:1.9.0-coq-8.8" + - DOCKERIMAGE="mathcomp/mathcomp:1.9.0-coq-8.9" + - DOCKERIMAGE="mathcomp/mathcomp:1.9.0-coq-8.10" # - DOCKERIMAGE="mathcomp/mathcomp:1.8.0-coq-dev" - DOCKERIMAGE="mathcomp/mathcomp-dev:coq-8.7" - DOCKERIMAGE="mathcomp/mathcomp-dev:coq-8.8" diff --git a/opam b/opam index c313d81..23718c9 100644 --- a/opam +++ b/opam @@ -12,11 +12,12 @@ build: [ make "-j" "%{jobs}%" ] install: [ make "install" ] remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/mathcomp/finmap'" ] depends: [ - "coq-mathcomp-ssreflect" { (>= "1.8.0" & < "1.9.0~") | (= "dev")} + "coq" { (>= "8.7" & < "8.11~") } + "coq-mathcomp-ssreflect" { (>= "1.8.0" & < "1.10.0~") } "coq-mathcomp-bigenough" { (>= "1.0.0" & < "1.1.0~") } ] tags: [ "keyword:finmap" "keyword:finset" "keyword:multiset" "keyword:order"] -authors: [ "Cyril Cohen " ] +authors: [ "Cyril Cohen " "Kazuhiko Sakaguchi " ] synopsis: "Finite sets, finite maps, finitely supported functions, orders" description: """ This library is an extension of mathematical component in order to diff --git a/order.v b/order.v index 87b319f..44fcdcb 100644 --- a/order.v +++ b/order.v @@ -1,77 +1,105 @@ -(*************************************************************************) -(* Copyright (C) 2012 - 2016 (Draft) *) -(* C. Cohen *) -(* Based on prior works by *) -(* D. Dreyer, G. Gonthier, A. Nanevski, P-Y Strub, B. Ziliani *) -(* *) -(* This program is free software: you can redistribute it and/or modify *) -(* it under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 3 of the License, or *) -(* (at your option) any later version. *) -(* *) -(* This program is distributed in the hope that it will be useful, *) -(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) -(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *) -(* GNU General Public License for more details. *) -(* *) -(* You should have received a copy of the GNU General Public License *) -(* along with this program. If not, see . *) -(*************************************************************************) - -From mathcomp -Require Import ssreflect ssrbool eqtype ssrfun ssrnat choice seq. -From mathcomp -Require Import fintype tuple bigop path finset. - -(*****************************************************************************) -(* This files definies a ordered and decidable relations on a *) -(* type as canonical structure. One need to import Order.Theory to get *) -(* the theory of such relations. The scope order_scope (%O) contains *) -(* fancier notation for this kind of ordeering. *) -(* *) -(* porderType == the type of partially ordered types *) -(* orderType == the type of totally ordered types *) -(* latticeType == the type of distributive lattices *) -(* blatticeType == ... with a bottom elemnt *) -(* tlatticeType == ... with a top element *) -(* tblatticeType == ... with both a top and a bottom *) -(* cblatticeType == ... with a complement to, and bottom *) -(* tcblatticeType == ... with a top, bottom, and general complement *) -(* *) -(* Each of these structure take a first argument named display, of type unit *) -(* instanciating it with tt or an unknown key will lead to a default display *) -(* Optionally, one can configure the display by setting one owns notation *) -(* on operators instanciated for their particular display *) -(* One example of this is the reverse display ^r, every notation with the *) -(* suffix ^r (e.g. x <=^r y) is about the reversal order, in order not to *) -(* confuse the normal order with its reversal. *) -(* *) -(* PorderType pord_mixin == builds an ordtype from a a partial order mixin *) -(* containing le, lt and refl, antisym, trans of le *) -(* LatticeType lat_mixin == builds a distributive lattice from a porderType *) -(* meet and join and axioms *) -(* OrderType le_total == builds an order type from a lattice *) -(* and from a proof of totality *) -(* ... *) -(* *) -(* We provide a canonical structure of orderType for natural numbers (nat) *) -(* for finType and for pairs of ordType by lexicographic orderering. *) -(* *) -(* leP ltP ltgtP are the three main lemmas for case analysis *) -(* *) -(* We also provide specialized version of some theorems from path.v. *) -(* *) -(* There are three distinct uses of the symbols <, <=, > and >=: *) -(* 0-ary, unary (prefix) and binary (infix). *) -(* 0. <%O, <=%O, >%O, >=%O stand respectively for lt, le, gt and ge. *) -(* 1. (< x), (<= x), (> x), (>= x) stand respectively for *) -(* (gt x), (ge x), (lt x), (le x). *) -(* So (< x) is a predicate characterizing elements smaller than x. *) -(* 2. (x < y), (x <= y), ... mean what they are expected to. *) -(* These convention are compatible with haskell's, *) -(* where ((< y) x) = (x < y) = ((<) x y), *) -(* except that we write <%O instead of (<). *) -(*****************************************************************************) +(* (c) Copyright 2006-2019 Microsoft Corporation and Inria. *) +(* Distributed under the terms of CeCILL-B. *) +From mathcomp Require Import ssreflect ssrbool eqtype ssrfun ssrnat choice seq. +From mathcomp Require Import fintype tuple bigop path finset. + +(******************************************************************************) +(* This files defines a ordered and decidable relations on a type as *) +(* canonical structure. One need to import some of the following modules to *) +(* get the definitions, notations, and theory of such relations. *) +(* Order.Def: definitions of basic operations. *) +(* Order.Syntax: fancy notations for ordering declared in the order_scope *) +(* (%O). *) +(* Order.LTheory: theory of partially ordered types and lattices excluding *) +(* complement and totality related theorems. *) +(* Order.CTheory: theory of complemented lattices including Order.LTheory. *) +(* Order.TTheory: theory of totally ordered types including Order.LTheory. *) +(* Order.Theory: theory of ordered types including all of the above *) +(* theory modules. *) +(* *) +(* We provide the following structures of ordered types *) +(* porderType == the type of partially ordered types *) +(* orderType == the type of totally ordered types *) +(* latticeType == the type of distributive lattices *) +(* blatticeType == ... with a bottom elemnt *) +(* tblatticeType == ... with both a top and a bottom *) +(* cblatticeType == the type of sectionally complemented lattices *) +(* (lattices with a complement to, and bottom) *) +(* ctblatticeType == the type of complemented lattices *) +(* (lattices with a top, bottom, and general complement) *) +(* finPOerderType == the type of partially ordered finite types *) +(* finLatticeType == the type of nonempty finite lattices *) +(* finClatticeType == the type of nonempty finite complemented lattices *) +(* finOrderType == the type of nonempty totally ordered finite types *) +(* *) +(* Each of these structure take a first argument named display, of type unit *) +(* instanciating it with tt or an unknown key will lead to a default display. *) +(* Optionally, one can configure the display by setting one owns notation on *) +(* operators instanciated for their particular display. *) +(* One example of this is the converse display ^c, every notation with the *) +(* suffix ^c (e.g. x <=^c y) is about the converse order, in order not to *) +(* confuse the normal order with its converse. *) +(* *) +(* PorderType pord_mixin == builds a porderType from a partial order mixin *) +(* containing le, lt and refl, antisym, trans of le *) +(* LatticeType lat_mixin == builds a distributive lattice from a porderType *) +(* meet and join and axioms *) +(* OrderType le_total == builds an order type from a latticeType and from *) +(* a proof of totality *) +(* ... *) +(* *) +(* Over these structures, we have the following operations *) +(* x <= y <-> x is less than or equal to y. *) +(* x < y <-> x is less than y (:= (y != x) && (x <= y)). *) +(* x >= y <-> x is greater than or equal to y (:= y <= x). *) +(* x > y <-> x is greater than y (:= y < x). *) +(* x <= y ?= iff C <-> x is less than y, or equal iff C is true. *) +(* x >=< y <-> x and y are comparable (:= (x <= y) || (y <= x)). *) +(* x >< y <-> x and y are incomparable. *) +(* For lattices we provide the following operations *) +(* x `&` y == the meet of x and y. *) +(* x `|` y == the join of x and y. *) +(* 0 == the bottom element. *) +(* 1 == the top element. *) +(* x `\` y == the (sectional) complement of y in [0, x]. *) +(* ~` x == the complement of x in [0, 1]. *) +(* \meet_ e == iterated meet of a lattice with a top. *) +(* \join_ e == iterated join of a lattice with a bottom. *) +(* For orderType we provide the following operations *) +(* [arg minr_(i < i0 | P) M] == a value i : T minimizing M : R, subject to *) +(* the condition P (i may appear in P and M), and *) +(* provided P holds for i0. *) +(* [arg maxr_(i > i0 | P) M] == a value i maximizing M subject to P and *) +(* provided P holds for i0. *) +(* [arg min_(i < i0 in A) M] == an i \in A minimizing M if i0 \in A. *) +(* [arg max_(i > i0 in A) M] == an i \in A maximizing M if i0 \in A. *) +(* [arg min_(i < i0) M] == an i : T minimizing M, given i0 : T. *) +(* [arg max_(i > i0) M] == an i : T maximizing M, given i0 : T. *) +(* *) +(* There are three distinct uses of the symbols *) +(* <, <=, >, >=, _ <= _ ?= iff _, >=<, and ><: *) +(* 0-ary, unary (prefix), and binary (infix). *) +(* 0. <%O, <=%O, >%O, >=%O, =<%O, and ><%O stand respectively for *) +(* lt, le, gt, ge, leif (_ <= _ ?= iff _), comparable, and incomparable. *) +(* 1. (< x), (<= x), (> x), (>= x), (>=< x), and (>< x) stand respectively *) +(* for (>%O x), (>=%O x), (<%O x), (<=%O x), (>=<%O x), and (><%O x). *) +(* So (< x) is a predicate characterizing elements smaller than x. *) +(* 2. (x < y), (x <= y), ... mean what they are expected to. *) +(* These convention are compatible with Haskell's, *) +(* where ((< y) x) = (x < y) = ((<) x y), *) +(* except that we write <%O instead of (<). *) +(* *) +(* We provide the following canonical instances of ordered types *) +(* - porderType, latticeType, orderType, blatticeType of nat *) +(* - porderType of seq (lexicographic ordering) *) +(* *) +(* leP ltP ltgtP are the three main lemmas for case analysis. *) +(* *) +(* We also provide specialized version of some theorems from path.v. *) +(* *) +(* This file is based on prior works by *) +(* D. Dreyer, G. Gonthier, A. Nanevski, P-Y Strub, B. Ziliani *) +(******************************************************************************) Set Implicit Arguments. Unset Strict Implicit. @@ -95,37 +123,37 @@ Reserved Notation "x >< y" (at level 70, no associativity). Reserved Notation ">< x" (at level 35). Reserved Notation ">< y :> T" (at level 35, y at next level). -Reserved Notation "x <=^r y" (at level 70, y at next level). -Reserved Notation "x >=^r y" (at level 70, y at next level, only parsing). -Reserved Notation "x <^r y" (at level 70, y at next level). -Reserved Notation "x >^r y" (at level 70, y at next level, only parsing). -Reserved Notation "x <=^r y :> T" (at level 70, y at next level). -Reserved Notation "x >=^r y :> T" (at level 70, y at next level, only parsing). -Reserved Notation "x <^r y :> T" (at level 70, y at next level). -Reserved Notation "x >^r y :> T" (at level 70, y at next level, only parsing). -Reserved Notation "<=^r y" (at level 35). -Reserved Notation ">=^r y" (at level 35). -Reserved Notation "<^r y" (at level 35). -Reserved Notation ">^r y" (at level 35). -Reserved Notation "<=^r y :> T" (at level 35, y at next level). -Reserved Notation ">=^r y :> T" (at level 35, y at next level). -Reserved Notation "<^r y :> T" (at level 35, y at next level). -Reserved Notation ">^r y :> T" (at level 35, y at next level). -Reserved Notation "x >=<^r y" (at level 70, no associativity). -Reserved Notation ">=<^r x" (at level 35). -Reserved Notation ">=<^r y :> T" (at level 35, y at next level). -Reserved Notation "x ><^r y" (at level 70, no associativity). -Reserved Notation "><^r x" (at level 35). -Reserved Notation "><^r y :> T" (at level 35, y at next level). - -Reserved Notation "x <=^r y <=^r z" (at level 70, y, z at next level). -Reserved Notation "x <^r y <=^r z" (at level 70, y, z at next level). -Reserved Notation "x <=^r y <^r z" (at level 70, y, z at next level). -Reserved Notation "x <^r y <^r z" (at level 70, y, z at next level). -Reserved Notation "x <=^r y ?= 'iff' c" (at level 70, y, c at next level, - format "x '[hv' <=^r y '/' ?= 'iff' c ']'"). -Reserved Notation "x <=^r y ?= 'iff' c :> T" (at level 70, y, c at next level, - format "x '[hv' <=^r y '/' ?= 'iff' c :> T ']'"). +Reserved Notation "x <=^c y" (at level 70, y at next level). +Reserved Notation "x >=^c y" (at level 70, y at next level, only parsing). +Reserved Notation "x <^c y" (at level 70, y at next level). +Reserved Notation "x >^c y" (at level 70, y at next level, only parsing). +Reserved Notation "x <=^c y :> T" (at level 70, y at next level). +Reserved Notation "x >=^c y :> T" (at level 70, y at next level, only parsing). +Reserved Notation "x <^c y :> T" (at level 70, y at next level). +Reserved Notation "x >^c y :> T" (at level 70, y at next level, only parsing). +Reserved Notation "<=^c y" (at level 35). +Reserved Notation ">=^c y" (at level 35). +Reserved Notation "<^c y" (at level 35). +Reserved Notation ">^c y" (at level 35). +Reserved Notation "<=^c y :> T" (at level 35, y at next level). +Reserved Notation ">=^c y :> T" (at level 35, y at next level). +Reserved Notation "<^c y :> T" (at level 35, y at next level). +Reserved Notation ">^c y :> T" (at level 35, y at next level). +Reserved Notation "x >=<^c y" (at level 70, no associativity). +Reserved Notation ">=<^c x" (at level 35). +Reserved Notation ">=<^c y :> T" (at level 35, y at next level). +Reserved Notation "x ><^c y" (at level 70, no associativity). +Reserved Notation "><^c x" (at level 35). +Reserved Notation "><^c y :> T" (at level 35, y at next level). + +Reserved Notation "x <=^c y <=^c z" (at level 70, y, z at next level). +Reserved Notation "x <^c y <=^c z" (at level 70, y, z at next level). +Reserved Notation "x <=^c y <^c z" (at level 70, y, z at next level). +Reserved Notation "x <^c y <^c z" (at level 70, y, z at next level). +Reserved Notation "x <=^c y ?= 'iff' c" (at level 70, y, c at next level, + format "x '[hv' <=^c y '/' ?= 'iff' c ']'"). +Reserved Notation "x <=^c y ?= 'iff' c :> T" (at level 70, y, c at next level, + format "x '[hv' <=^c y '/' ?= 'iff' c :> T ']'"). (* Reserved notation for lattice operations. *) Reserved Notation "A `&` B" (at level 48, left associativity). @@ -133,11 +161,11 @@ Reserved Notation "A `|` B" (at level 52, left associativity). Reserved Notation "A `\` B" (at level 50, left associativity). Reserved Notation "~` A" (at level 35, right associativity). -(* Reserved notation for reverse lattice operations. *) -Reserved Notation "A `&^r` B" (at level 48, left associativity). -Reserved Notation "A `|^r` B" (at level 52, left associativity). -Reserved Notation "A `\^r` B" (at level 50, left associativity). -Reserved Notation "~^r` A" (at level 35, right associativity). +(* Reserved notation for converse lattice operations. *) +Reserved Notation "A `&^c` B" (at level 48, left associativity). +Reserved Notation "A `|^c` B" (at level 52, left associativity). +Reserved Notation "A `\^c` B" (at level 50, left associativity). +Reserved Notation "~^c` A" (at level 35, right associativity). Reserved Notation "\meet_ i F" (at level 41, F at level 41, i at level 0, @@ -213,82 +241,79 @@ Reserved Notation "\join_ ( i 'in' A ) F" (at level 41, F at level 41, i, A at level 50, format "'[' \join_ ( i 'in' A ) '/ ' F ']'"). -Reserved Notation "\meet^r_ i F" +Reserved Notation "\meet^c_ i F" (at level 41, F at level 41, i at level 0, - format "'[' \meet^r_ i '/ ' F ']'"). -Reserved Notation "\meet^r_ ( i <- r | P ) F" + format "'[' \meet^c_ i '/ ' F ']'"). +Reserved Notation "\meet^c_ ( i <- r | P ) F" (at level 41, F at level 41, i, r at level 50, - format "'[' \meet^r_ ( i <- r | P ) '/ ' F ']'"). -Reserved Notation "\meet^r_ ( i <- r ) F" + format "'[' \meet^c_ ( i <- r | P ) '/ ' F ']'"). +Reserved Notation "\meet^c_ ( i <- r ) F" (at level 41, F at level 41, i, r at level 50, - format "'[' \meet^r_ ( i <- r ) '/ ' F ']'"). -Reserved Notation "\meet^r_ ( m <= i < n | P ) F" + format "'[' \meet^c_ ( i <- r ) '/ ' F ']'"). +Reserved Notation "\meet^c_ ( m <= i < n | P ) F" (at level 41, F at level 41, i, m, n at level 50, - format "'[' \meet^r_ ( m <= i < n | P ) '/ ' F ']'"). -Reserved Notation "\meet^r_ ( m <= i < n ) F" + format "'[' \meet^c_ ( m <= i < n | P ) '/ ' F ']'"). +Reserved Notation "\meet^c_ ( m <= i < n ) F" (at level 41, F at level 41, i, m, n at level 50, - format "'[' \meet^r_ ( m <= i < n ) '/ ' F ']'"). -Reserved Notation "\meet^r_ ( i | P ) F" + format "'[' \meet^c_ ( m <= i < n ) '/ ' F ']'"). +Reserved Notation "\meet^c_ ( i | P ) F" (at level 41, F at level 41, i at level 50, - format "'[' \meet^r_ ( i | P ) '/ ' F ']'"). -Reserved Notation "\meet^r_ ( i : t | P ) F" + format "'[' \meet^c_ ( i | P ) '/ ' F ']'"). +Reserved Notation "\meet^c_ ( i : t | P ) F" (at level 41, F at level 41, i at level 50, only parsing). -Reserved Notation "\meet^r_ ( i : t ) F" +Reserved Notation "\meet^c_ ( i : t ) F" (at level 41, F at level 41, i at level 50, only parsing). -Reserved Notation "\meet^r_ ( i < n | P ) F" +Reserved Notation "\meet^c_ ( i < n | P ) F" (at level 41, F at level 41, i, n at level 50, - format "'[' \meet^r_ ( i < n | P ) '/ ' F ']'"). -Reserved Notation "\meet^r_ ( i < n ) F" + format "'[' \meet^c_ ( i < n | P ) '/ ' F ']'"). +Reserved Notation "\meet^c_ ( i < n ) F" (at level 41, F at level 41, i, n at level 50, - format "'[' \meet^r_ ( i < n ) F ']'"). -Reserved Notation "\meet^r_ ( i 'in' A | P ) F" + format "'[' \meet^c_ ( i < n ) F ']'"). +Reserved Notation "\meet^c_ ( i 'in' A | P ) F" (at level 41, F at level 41, i, A at level 50, - format "'[' \meet^r_ ( i 'in' A | P ) '/ ' F ']'"). -Reserved Notation "\meet^r_ ( i 'in' A ) F" + format "'[' \meet^c_ ( i 'in' A | P ) '/ ' F ']'"). +Reserved Notation "\meet^c_ ( i 'in' A ) F" (at level 41, F at level 41, i, A at level 50, - format "'[' \meet^r_ ( i 'in' A ) '/ ' F ']'"). + format "'[' \meet^c_ ( i 'in' A ) '/ ' F ']'"). -Reserved Notation "\join^r_ i F" +Reserved Notation "\join^c_ i F" (at level 41, F at level 41, i at level 0, - format "'[' \join^r_ i '/ ' F ']'"). -Reserved Notation "\join^r_ ( i <- r | P ) F" + format "'[' \join^c_ i '/ ' F ']'"). +Reserved Notation "\join^c_ ( i <- r | P ) F" (at level 41, F at level 41, i, r at level 50, - format "'[' \join^r_ ( i <- r | P ) '/ ' F ']'"). -Reserved Notation "\join^r_ ( i <- r ) F" + format "'[' \join^c_ ( i <- r | P ) '/ ' F ']'"). +Reserved Notation "\join^c_ ( i <- r ) F" (at level 41, F at level 41, i, r at level 50, - format "'[' \join^r_ ( i <- r ) '/ ' F ']'"). -Reserved Notation "\join^r_ ( m <= i < n | P ) F" + format "'[' \join^c_ ( i <- r ) '/ ' F ']'"). +Reserved Notation "\join^c_ ( m <= i < n | P ) F" (at level 41, F at level 41, i, m, n at level 50, - format "'[' \join^r_ ( m <= i < n | P ) '/ ' F ']'"). -Reserved Notation "\join^r_ ( m <= i < n ) F" + format "'[' \join^c_ ( m <= i < n | P ) '/ ' F ']'"). +Reserved Notation "\join^c_ ( m <= i < n ) F" (at level 41, F at level 41, i, m, n at level 50, - format "'[' \join^r_ ( m <= i < n ) '/ ' F ']'"). -Reserved Notation "\join^r_ ( i | P ) F" + format "'[' \join^c_ ( m <= i < n ) '/ ' F ']'"). +Reserved Notation "\join^c_ ( i | P ) F" (at level 41, F at level 41, i at level 50, - format "'[' \join^r_ ( i | P ) '/ ' F ']'"). -Reserved Notation "\join^r_ ( i : t | P ) F" + format "'[' \join^c_ ( i | P ) '/ ' F ']'"). +Reserved Notation "\join^c_ ( i : t | P ) F" (at level 41, F at level 41, i at level 50, only parsing). -Reserved Notation "\join^r_ ( i : t ) F" +Reserved Notation "\join^c_ ( i : t ) F" (at level 41, F at level 41, i at level 50, only parsing). -Reserved Notation "\join^r_ ( i < n | P ) F" +Reserved Notation "\join^c_ ( i < n | P ) F" (at level 41, F at level 41, i, n at level 50, - format "'[' \join^r_ ( i < n | P ) '/ ' F ']'"). -Reserved Notation "\join^r_ ( i < n ) F" + format "'[' \join^c_ ( i < n | P ) '/ ' F ']'"). +Reserved Notation "\join^c_ ( i < n ) F" (at level 41, F at level 41, i, n at level 50, - format "'[' \join^r_ ( i < n ) F ']'"). -Reserved Notation "\join^r_ ( i 'in' A | P ) F" + format "'[' \join^c_ ( i < n ) F ']'"). +Reserved Notation "\join^c_ ( i 'in' A | P ) F" (at level 41, F at level 41, i, A at level 50, - format "'[' \join^r_ ( i 'in' A | P ) '/ ' F ']'"). -Reserved Notation "\join^r_ ( i 'in' A ) F" + format "'[' \join^c_ ( i 'in' A | P ) '/ ' F ']'"). +Reserved Notation "\join^c_ ( i 'in' A ) F" (at level 41, F at level 41, i, A at level 50, - format "'[' \join^r_ ( i 'in' A ) '/ ' F ']'"). - -Fact unit_irrelevance (x y : unit) : x = y. -Proof. by case: x; case: y. Qed. + format "'[' \join^c_ ( i 'in' A ) '/ ' F ']'"). Module Order. @@ -298,10 +323,10 @@ Module Order. Module POrder. Section ClassDef. -Structure mixin_of (T : eqType) := Mixin { +Record mixin_of (T : eqType) := Mixin { le : rel T; lt : rel T; - _ : forall x y, lt x y = (x != y) && (le x y); + _ : forall x y, lt x y = (y != x) && (le x y); _ : reflexive le; _ : antisymmetric le; _ : transitive le @@ -321,54 +346,53 @@ Local Coercion sort : type >-> Sortclass. Variables (T : Type) (disp : unit) (cT : type disp). Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. -Definition clone disp' c of (disp = disp') & phant_id class c := - @Pack disp' T c. +Definition clone c of phant_id class c := @Pack disp T c. +Definition clone_with disp' c of phant_id class c := @Pack disp' T c. Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). -Definition pack disp := - fun b bT & phant_id (Choice.class bT) b => +Definition pack := + fun bT b & phant_id (Choice.class bT) b => fun m => Pack disp (@Class T b m). Definition eqType := @Equality.Pack cT xclass. Definition choiceType := @Choice.Pack cT xclass. End ClassDef. -Module Import Exports. -Coercion base : class_of >-> Choice.class_of. -Coercion mixin : class_of >-> mixin_of. -Coercion sort : type >-> Sortclass. +Module Exports. +Coercion base : class_of >-> Choice.class_of. +Coercion mixin : class_of >-> mixin_of. +Coercion sort : type >-> Sortclass. Coercion eqType : type >-> Equality.type. Coercion choiceType : type >-> Choice.type. - Canonical eqType. Canonical choiceType. - Notation porderType := type. Notation porderMixin := mixin_of. Notation POrderMixin := Mixin. Notation POrderType disp T m := (@pack T disp _ _ id m). - -Notation "[ 'porderType' 'of' T 'for' cT ]" := (@clone T _ cT _ _ erefl id) +Notation "[ 'porderType' 'of' T 'for' cT ]" := (@clone T _ cT _ id) (at level 0, format "[ 'porderType' 'of' T 'for' cT ]") : form_scope. Notation "[ 'porderType' 'of' T 'for' cT 'with' disp ]" := - (@clone T _ cT disp _ (unit_irrelevance _ _) id) - (at level 0, format "[ 'porderType' 'of' T 'for' cT 'with' disp ]") : form_scope. + (@clone_with T _ cT disp _ id) + (at level 0, format "[ 'porderType' 'of' T 'for' cT 'with' disp ]") : + form_scope. Notation "[ 'porderType' 'of' T ]" := [porderType of T for _] (at level 0, format "[ 'porderType' 'of' T ]") : form_scope. -Notation "[ 'porderType' 'of' T 'with' disp ]" := [porderType of T for _ with disp] +Notation "[ 'porderType' 'of' T 'with' disp ]" := + [porderType of T for _ with disp] (at level 0, format "[ 'porderType' 'of' T 'with' disp ]") : form_scope. End Exports. -End POrder. +End POrder. Import POrder.Exports. Bind Scope cpo_sort with POrder.sort. Module Import POrderDef. Section Def. -Variable (display : unit). -Local Notation porderType := (porderType display). +Variable (disp : unit). +Local Notation porderType := (porderType disp). Variable (T : porderType). Definition le (R : porderType) : rel R := POrder.le (POrder.class R). @@ -388,15 +412,15 @@ Definition leif (x y : T) C : Prop := ((x <= y) * ((x == y) = C))%type. Definition le_of_leif x y C (le_xy : @leif x y C) := le_xy.1 : le x y. -CoInductive le_xor_gt (x y : T) : bool -> bool -> Set := +Variant le_xor_gt (x y : T) : bool -> bool -> Set := | LerNotGt of x <= y : le_xor_gt x y true false | GtrNotLe of y < x : le_xor_gt x y false true. -CoInductive lt_xor_ge (x y : T) : bool -> bool -> Set := +Variant lt_xor_ge (x y : T) : bool -> bool -> Set := | LtrNotGe of x < y : lt_xor_ge x y false true | GerNotLt of y <= x : lt_xor_ge x y true false. -CoInductive comparer (x y : T) : +Variant comparer (x y : T) : bool -> bool -> bool -> bool -> bool -> bool -> Set := | ComparerEq of x = y : comparer x y true true true true false false @@ -405,7 +429,7 @@ CoInductive comparer (x y : T) : | ComparerGt of y < x : comparer x y false false false true false true. -CoInductive incomparer (x y : T) : +Variant incomparer (x y : T) : bool -> bool -> bool -> bool -> bool -> bool -> bool -> bool -> Set := | InComparerEq of x = y : incomparer x y true true true true false false true true @@ -462,7 +486,7 @@ Notation "x <= y < z" := ((x <= y) && (y < z)) : order_scope. Notation "x < y < z" := ((x < y) && (y < z)) : order_scope. Notation "x <= y ?= 'iff' C" := (leif x y C) : order_scope. -Notation "x <= y ?= 'iff' C :> R" := ((x : R) <= (y : R) ?= iff C) +Notation "x <= y ?= 'iff' C :> T" := ((x : T) <= (y : T) ?= iff C) (only parsing) : order_scope. Notation ">=< x" := (comparable x) : order_scope. @@ -473,14 +497,16 @@ Notation ">< x" := (fun y => ~~ (comparable x y)) : order_scope. Notation ">< x :> T" := (>< (x : T)) (only parsing) : order_scope. Notation "x >< y" := (~~ (comparable x y)) : order_scope. -Coercion le_of_leif : leif >-> is_true. - End POSyntax. +Module POCoercions. +Coercion le_of_leif : leif >-> is_true. +End POCoercions. + Module Lattice. Section ClassDef. -Structure mixin_of d (T : porderType d) := Mixin { +Record mixin_of d (T : porderType d) := Mixin { meet : T -> T -> T; join : T -> T -> T; _ : commutative meet; @@ -493,72 +519,103 @@ Structure mixin_of d (T : porderType d) := Mixin { _ : left_distributive meet join; }. -Record class_of d (T : Type) := Class { +Record class_of (T : Type) := Class { base : POrder.class_of T; - mixin : mixin_of (POrder.Pack d base) + mixin_disp : unit; + mixin : mixin_of (POrder.Pack mixin_disp base) }. Local Coercion base : class_of >-> POrder.class_of. -Structure type (display : unit) := - Pack { sort; _ : class_of display sort }. +Structure type (disp : unit) := Pack { sort; _ : class_of sort }. Local Coercion sort : type >-> Sortclass. Variables (T : Type) (disp : unit) (cT : type disp). -Definition class := let: Pack _ c as cT' := cT return class_of _ cT' in c. -Definition clone disp' c of (disp = disp') & phant_id class c := - @Pack disp' T c. +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. +Definition clone c of phant_id class c := @Pack disp T c. +Definition clone_with disp' c of phant_id class c := @Pack disp' T c. Let xT := let: Pack T _ := cT in T. -Notation xclass := (class : class_of _ xT). +Notation xclass := (class : class_of xT). Definition pack b0 (m0 : mixin_of (@POrder.Pack disp T b0)) := fun bT b & phant_id (@POrder.class disp bT) b => - fun m & phant_id m0 m => Pack (@Class disp T b m). + fun disp' m & phant_id m0 m => Pack disp (@Class T b disp' m). Definition eqType := @Equality.Pack cT xclass. Definition choiceType := @Choice.Pack cT xclass. Definition porderType := @POrder.Pack disp cT xclass. End ClassDef. -Module Import Exports. -Coercion base : class_of >-> POrder.class_of. -Coercion mixin : class_of >-> mixin_of. -Coercion sort : type >-> Sortclass. -Coercion eqType : type >-> Equality.type. +Module Exports. +Coercion base : class_of >-> POrder.class_of. +Coercion mixin : class_of >-> mixin_of. +Coercion sort : type >-> Sortclass. +Coercion eqType : type >-> Equality.type. Coercion choiceType : type >-> Choice.type. Coercion porderType : type >-> POrder.type. - Canonical eqType. Canonical choiceType. Canonical porderType. - Notation latticeType := type. Notation latticeMixin := mixin_of. Notation LatticeMixin := Mixin. -Notation LatticeType T m := (@pack T _ _ m _ _ id _ id). - -Notation "[ 'latticeType' 'of' T 'for' cT ]" := (@clone T _ cT _ _ erefl id) +Notation LatticeType T m := (@pack T _ _ m _ _ id _ _ id). +Notation "[ 'latticeType' 'of' T 'for' cT ]" := (@clone T _ cT _ id) (at level 0, format "[ 'latticeType' 'of' T 'for' cT ]") : form_scope. Notation "[ 'latticeType' 'of' T 'for' cT 'with' disp ]" := - (@clone T _ cT disp _ (unit_irrelevance _ _) id) - (at level 0, format "[ 'latticeType' 'of' T 'for' cT 'with' disp ]") : form_scope. + (@clone_with T _ cT disp _ id) + (at level 0, format "[ 'latticeType' 'of' T 'for' cT 'with' disp ]") : + form_scope. Notation "[ 'latticeType' 'of' T ]" := [latticeType of T for _] (at level 0, format "[ 'latticeType' 'of' T ]") : form_scope. -Notation "[ 'latticeType' 'of' T 'with' disp ]" := [latticeType of T for _ with disp] +Notation "[ 'latticeType' 'of' T 'with' disp ]" := + [latticeType of T for _ with disp] (at level 0, format "[ 'latticeType' 'of' T 'with' disp ]") : form_scope. End Exports. -End Lattice. +End Lattice. Export Lattice.Exports. Module Import LatticeDef. Section LatticeDef. -Context {display : unit}. -Local Notation latticeType := (latticeType display). -Definition meet {T : latticeType} : T -> T -> T := Lattice.meet (Lattice.class T). -Definition join {T : latticeType} : T -> T -> T := Lattice.join (Lattice.class T). +Context {disp : unit}. +Local Notation latticeType := (latticeType disp). +Context {T : latticeType}. +Definition meet : T -> T -> T := Lattice.meet (Lattice.class T). +Definition join : T -> T -> T := Lattice.join (Lattice.class T). + +Variant le_xor_gt (x y : T) : bool -> bool -> T -> T -> T -> T -> Set := + | LerNotGt of x <= y : le_xor_gt x y true false x x y y + | GtrNotLe of y < x : le_xor_gt x y false true y y x x. + +Variant lt_xor_ge (x y : T) : bool -> bool -> T -> T -> T -> T -> Set := + | LtrNotGe of x < y : lt_xor_ge x y false true x x y y + | GerNotLt of y <= x : lt_xor_ge x y true false y y x x. + +Variant comparer (x y : T) : + bool -> bool -> bool -> bool -> bool -> bool -> T -> T -> T -> T -> Set := + | ComparerEq of x = y : comparer x y + true true true true false false x x x x + | ComparerLt of x < y : comparer x y + false false true false true false x x y y + | ComparerGt of y < x : comparer x y + false false false true false true y y x x. + +Variant incomparer (x y : T) : + bool -> bool -> bool -> bool -> bool -> bool -> bool -> bool -> + T -> T -> T -> T -> Set := + | InComparerEq of x = y : incomparer x y + true true true true false false true true x x x x + | InComparerLt of x < y : incomparer x y + false false true false true false true true x x y y + | InComparerGt of y < x : incomparer x y + false false false true false true true true y y x x + | InComparer of x >< y : incomparer x y + false false false false false false false false + (meet x y) (meet x y) (join x y) (join x y). + End LatticeDef. End LatticeDef. @@ -570,31 +627,32 @@ Notation "x `|` y" := (join x y). End LatticeSyntax. Module Total. +Definition mixin_of d (T : latticeType d) := (total (<=%O : rel T)). Section ClassDef. -Local Notation mixin_of T := (total (<=%O : rel T)). -Record class_of d (T : Type) := Class { - base : Lattice.class_of d T; - mixin : total (<=%O : rel (POrder.Pack d base)) +Record class_of (T : Type) := Class { + base : Lattice.class_of T; + mixin_disp : unit; + mixin : mixin_of (Lattice.Pack mixin_disp base) }. Local Coercion base : class_of >-> Lattice.class_of. -Structure type d := Pack { sort; _ : class_of d sort }. +Structure type (d : unit) := Pack { sort; _ : class_of sort }. Local Coercion sort : type >-> Sortclass. Variables (T : Type) (disp : unit) (cT : type disp). -Definition class := let: Pack _ c as cT' := cT return class_of _ cT' in c. -Definition clone disp' c of (disp = disp') & phant_id class c := - @Pack disp' T c. +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. +Definition clone disp' c & phant_id class c := @Pack disp' T c. +Definition clone_with disp' c & phant_id class c := @Pack disp' T c. Let xT := let: Pack T _ := cT in T. -Notation xclass := (class : class_of _ xT). +Notation xclass := (class : class_of xT). Definition pack b0 (m0 : mixin_of (@Lattice.Pack disp T b0)) := fun bT b & phant_id (@Lattice.class disp bT) b => - fun m & phant_id m0 m => Pack (@Class disp T b m). + fun disp' m & phant_id m0 m => Pack disp (@Class T b disp' m). Definition eqType := @Equality.Pack cT xclass. Definition choiceType := @Choice.Pack cT xclass. @@ -603,66 +661,140 @@ Definition latticeType := @Lattice.Pack disp cT xclass. End ClassDef. -Module Import Exports. -Coercion base : class_of >-> Lattice.class_of. -Coercion sort : type >-> Sortclass. -Coercion eqType : type >-> Equality.type. +Module Exports. +Coercion base : class_of >-> Lattice.class_of. +Coercion sort : type >-> Sortclass. +Coercion eqType : type >-> Equality.type. Coercion choiceType : type >-> Choice.type. Coercion porderType : type >-> POrder.type. Coercion latticeType : type >-> Lattice.type. - Canonical eqType. Canonical choiceType. Canonical porderType. Canonical latticeType. - Notation orderType := type. -Notation OrderType T m := (@pack T _ _ m _ _ id _ id). - -Notation "[ 'orderType' 'of' T 'for' cT ]" := (@clone T _ cT _ _ erefl id) +Notation OrderType T m := (@pack T _ _ m _ _ id _ _ id). +Notation "[ 'orderType' 'of' T 'for' cT ]" := (@clone T _ cT _ _ id) (at level 0, format "[ 'orderType' 'of' T 'for' cT ]") : form_scope. Notation "[ 'orderType' 'of' T 'for' cT 'with' disp ]" := - (@clone T _ cT disp _ (unit_irrelevance _ _) id) - (at level 0, format "[ 'orderType' 'of' T 'for' cT 'with' disp ]") : form_scope. + (@clone_with T _ cT disp _ id) + (at level 0, format "[ 'orderType' 'of' T 'for' cT 'with' disp ]") : + form_scope. Notation "[ 'orderType' 'of' T ]" := [orderType of T for _] (at level 0, format "[ 'orderType' 'of' T ]") : form_scope. -Notation "[ 'orderType' 'of' T 'with' disp ]" := [orderType of T for _ with disp] +Notation "[ 'orderType' 'of' T 'with' disp ]" := + [orderType of T for _ with disp] (at level 0, format "[ 'orderType' 'of' T 'with' disp ]") : form_scope. - End Exports. -End Total. +End Total. Import Total.Exports. +Module Import TotalDef. +Section TotalDef. +Context {disp : unit} {T : orderType disp} {I : finType}. +Definition arg_min := @extremum T I <=%O. +Definition arg_max := @extremum T I >=%O. +End TotalDef. +End TotalDef. + +Module Import TotalSyntax. + +Fact total_display : unit. Proof. exact: tt. Qed. + +Notation max := (@join total_display _). +Notation "@ 'max' R" := + (@join total_display R) (at level 10, R at level 8, only parsing). +Notation min := (@meet total_display _). +Notation "@ 'min' R" := + (@meet total_display R) (at level 10, R at level 8, only parsing). + +Notation "\max_ ( i <- r | P ) F" := + (\big[@join total_display _/0%O]_(i <- r | P%B) F%O) : order_scope. +Notation "\max_ ( i <- r ) F" := + (\big[@join total_display _/0%O]_(i <- r) F%O) : order_scope. +Notation "\max_ ( i | P ) F" := + (\big[@join total_display _/0%O]_(i | P%B) F%O) : order_scope. +Notation "\max_ i F" := + (\big[@join total_display _/0%O]_i F%O) : order_scope. +Notation "\max_ ( i : I | P ) F" := + (\big[@join total_display _/0%O]_(i : I | P%B) F%O) (only parsing) : + order_scope. +Notation "\max_ ( i : I ) F" := + (\big[@join total_display _/0%O]_(i : I) F%O) (only parsing) : order_scope. +Notation "\max_ ( m <= i < n | P ) F" := + (\big[@join total_display _/0%O]_(m <= i < n | P%B) F%O) : order_scope. +Notation "\max_ ( m <= i < n ) F" := + (\big[@join total_display _/0%O]_(m <= i < n) F%O) : order_scope. +Notation "\max_ ( i < n | P ) F" := + (\big[@join total_display _/0%O]_(i < n | P%B) F%O) : order_scope. +Notation "\max_ ( i < n ) F" := + (\big[@join total_display _/0%O]_(i < n) F%O) : order_scope. +Notation "\max_ ( i 'in' A | P ) F" := + (\big[@join total_display _/0%O]_(i in A | P%B) F%O) : order_scope. +Notation "\max_ ( i 'in' A ) F" := + (\big[@join total_display _/0%O]_(i in A) F%O) : order_scope. + +Notation "[ 'arg' 'min_' ( i < i0 | P ) F ]" := + (arg_min i0 (fun i => P%B) (fun i => F)) + (at level 0, i, i0 at level 10, + format "[ 'arg' 'min_' ( i < i0 | P ) F ]") : order_scope. + +Notation "[ 'arg' 'min_' ( i < i0 'in' A ) F ]" := + [arg min_(i < i0 | i \in A) F] + (at level 0, i, i0 at level 10, + format "[ 'arg' 'min_' ( i < i0 'in' A ) F ]") : order_scope. + +Notation "[ 'arg' 'min_' ( i < i0 ) F ]" := [arg min_(i < i0 | true) F] + (at level 0, i, i0 at level 10, + format "[ 'arg' 'min_' ( i < i0 ) F ]") : order_scope. + +Notation "[ 'arg' 'max_' ( i > i0 | P ) F ]" := + (arg_max i0 (fun i => P%B) (fun i => F)) + (at level 0, i, i0 at level 10, + format "[ 'arg' 'max_' ( i > i0 | P ) F ]") : order_scope. + +Notation "[ 'arg' 'max_' ( i > i0 'in' A ) F ]" := + [arg max_(i > i0 | i \in A) F] + (at level 0, i, i0 at level 10, + format "[ 'arg' 'max_' ( i > i0 'in' A ) F ]") : order_scope. + +Notation "[ 'arg' 'max_' ( i > i0 ) F ]" := [arg max_(i > i0 | true) F] + (at level 0, i, i0 at level 10, + format "[ 'arg' 'max_' ( i > i0 ) F ]") : order_scope. + +End TotalSyntax. + Module BLattice. Section ClassDef. -Structure mixin_of d (T : porderType d) := Mixin { +Record mixin_of d (T : porderType d) := Mixin { bottom : T; _ : forall x, bottom <= x; }. -Record class_of d (T : Type) := Class { - base : Lattice.class_of d T; - mixin : mixin_of (POrder.Pack d base) +Record class_of (T : Type) := Class { + base : Lattice.class_of T; + mixin_disp : unit; + mixin : mixin_of (POrder.Pack mixin_disp base) }. Local Coercion base : class_of >-> Lattice.class_of. -Structure type d := Pack { sort; _ : class_of d sort }. +Structure type (d : unit) := Pack { sort; _ : class_of sort}. Local Coercion sort : type >-> Sortclass. Variables (T : Type) (disp : unit) (cT : type disp). -Definition class := let: Pack _ c as cT' := cT return class_of _ cT' in c. -Definition clone disp' c of (disp = disp') & phant_id class c := - @Pack disp' T c. +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. +Definition clone c of phant_id class c := @Pack disp T c. +Definition clone_with disp' c of phant_id class c := @Pack disp' T c. Let xT := let: Pack T _ := cT in T. -Notation xclass := (class : class_of _ xT). +Notation xclass := (class : class_of xT). Definition pack b0 (m0 : mixin_of (@Lattice.Pack disp T b0)) := fun bT b & phant_id (@Lattice.class disp bT) b => - fun m & phant_id m0 m => Pack (@Class disp T b m). + fun disp' m & phant_id m0 m => Pack disp (@Class T b disp' m). Definition eqType := @Equality.Pack cT xclass. Definition choiceType := @Choice.Pack cT xclass. @@ -670,37 +802,36 @@ Definition porderType := @POrder.Pack disp cT xclass. Definition latticeType := @Lattice.Pack disp cT xclass. End ClassDef. -Module Import Exports. -Coercion base : class_of >-> Lattice.class_of. -Coercion mixin : class_of >-> mixin_of. -Coercion sort : type >-> Sortclass. -Coercion eqType : type >-> Equality.type. +Module Exports. +Coercion base : class_of >-> Lattice.class_of. +Coercion mixin : class_of >-> mixin_of. +Coercion sort : type >-> Sortclass. +Coercion eqType : type >-> Equality.type. Coercion choiceType : type >-> Choice.type. Coercion porderType : type >-> POrder.type. Coercion latticeType : type >-> Lattice.type. - Canonical eqType. Canonical choiceType. Canonical porderType. Canonical latticeType. - Notation blatticeType := type. Notation blatticeMixin := mixin_of. Notation BLatticeMixin := Mixin. -Notation BLatticeType T m := (@pack T _ _ m _ _ id _ id). - -Notation "[ 'blatticeType' 'of' T 'for' cT ]" := (@clone T _ cT _ _ erefl id) +Notation BLatticeType T m := (@pack T _ _ m _ _ id _ _ id). +Notation "[ 'blatticeType' 'of' T 'for' cT ]" := (@clone T _ cT _ id) (at level 0, format "[ 'blatticeType' 'of' T 'for' cT ]") : form_scope. Notation "[ 'blatticeType' 'of' T 'for' cT 'with' disp ]" := - (@clone T _ cT disp _ (unit_irrelevance _ _) id) - (at level 0, format "[ 'blatticeType' 'of' T 'for' cT 'with' disp ]") : form_scope. + (@clone_with T _ cT disp _ id) + (at level 0, format "[ 'blatticeType' 'of' T 'for' cT 'with' disp ]") : + form_scope. Notation "[ 'blatticeType' 'of' T ]" := [blatticeType of T for _] (at level 0, format "[ 'blatticeType' 'of' T ]") : form_scope. -Notation "[ 'blatticeType' 'of' T 'with' disp ]" := [blatticeType of T for _ with disp] +Notation "[ 'blatticeType' 'of' T 'with' disp ]" := + [blatticeType of T for _ with disp] (at level 0, format "[ 'blatticeType' 'of' T 'with' disp ]") : form_scope. End Exports. -End BLattice. +End BLattice. Export BLattice.Exports. Module Import BLatticeDef. @@ -724,49 +855,50 @@ Notation "\join_ ( i : I | P ) F" := Notation "\join_ ( i : I ) F" := (\big[@join _ _/0%O]_(i : I) F%O) (only parsing) : order_scope. Notation "\join_ ( m <= i < n | P ) F" := - (\big[@join _ _/0%O]_(m <= i < n | P%B) F%O) : order_scope. + (\big[@join _ _/0%O]_(m <= i < n | P%B) F%O) : order_scope. Notation "\join_ ( m <= i < n ) F" := - (\big[@join _ _/0%O]_(m <= i < n) F%O) : order_scope. + (\big[@join _ _/0%O]_(m <= i < n) F%O) : order_scope. Notation "\join_ ( i < n | P ) F" := - (\big[@join _ _/0%O]_(i < n | P%B) F%O) : order_scope. + (\big[@join _ _/0%O]_(i < n | P%B) F%O) : order_scope. Notation "\join_ ( i < n ) F" := - (\big[@join _ _/0%O]_(i < n) F%O) : order_scope. + (\big[@join _ _/0%O]_(i < n) F%O) : order_scope. Notation "\join_ ( i 'in' A | P ) F" := - (\big[@join _ _/0%O]_(i in A | P%B) F%O) : order_scope. + (\big[@join _ _/0%O]_(i in A | P%B) F%O) : order_scope. Notation "\join_ ( i 'in' A ) F" := - (\big[@join _ _/0%O]_(i in A) F%O) : order_scope. + (\big[@join _ _/0%O]_(i in A) F%O) : order_scope. End BLatticeSyntax. Module TBLattice. Section ClassDef. -Structure mixin_of d (T : porderType d) := Mixin { +Record mixin_of d (T : porderType d) := Mixin { top : T; _ : forall x, x <= top; }. -Record class_of d (T : Type) := Class { - base : BLattice.class_of d T; - mixin : mixin_of (POrder.Pack d base) +Record class_of (T : Type) := Class { + base : BLattice.class_of T; + mixin_disp : unit; + mixin : mixin_of (POrder.Pack mixin_disp base) }. Local Coercion base : class_of >-> BLattice.class_of. -Structure type d := Pack { sort; _ : class_of d sort }. +Structure type (d : unit) := Pack { sort; _ : class_of sort }. Local Coercion sort : type >-> Sortclass. Variables (T : Type) (disp : unit) (cT : type disp). -Definition class := let: Pack _ c as cT' := cT return class_of _ cT' in c. -Definition clone disp' c of (disp = disp') & phant_id class c := - @Pack disp' T c. +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. +Definition clone c of phant_id class c := @Pack disp T c. +Definition clone_with disp' c of phant_id class c := @Pack disp' T c. Let xT := let: Pack T _ := cT in T. -Notation xclass := (class : class_of _ xT). +Notation xclass := (class : class_of xT). Definition pack b0 (m0 : mixin_of (@BLattice.Pack disp T b0)) := fun bT b & phant_id (@BLattice.class disp bT) b => - fun m & phant_id m0 m => Pack (@Class disp T b m). + fun disp' m & phant_id m0 m => Pack disp (@Class T b disp' m). Definition eqType := @Equality.Pack cT xclass. Definition choiceType := @Choice.Pack cT xclass. @@ -775,39 +907,37 @@ Definition latticeType := @Lattice.Pack disp cT xclass. Definition blatticeType := @BLattice.Pack disp cT xclass. End ClassDef. -Module Import Exports. -Coercion base : class_of >-> BLattice.class_of. -Coercion mixin : class_of >-> mixin_of. -Coercion sort : type >-> Sortclass. -Coercion eqType : type >-> Equality.type. +Module Exports. +Coercion base : class_of >-> BLattice.class_of. +Coercion mixin : class_of >-> mixin_of. +Coercion sort : type >-> Sortclass. +Coercion eqType : type >-> Equality.type. Coercion porderType : type >-> POrder.type. Coercion latticeType : type >-> Lattice.type. Coercion blatticeType : type >-> BLattice.type. - Canonical eqType. Canonical choiceType. Canonical porderType. Canonical latticeType. Canonical blatticeType. - Notation tblatticeType := type. Notation tblatticeMixin := mixin_of. Notation TBLatticeMixin := Mixin. -Notation TBLatticeType T m := (@pack T _ _ m _ _ id _ id). - -Notation "[ 'tblatticeType' 'of' T 'for' cT ]" := (@clone T _ cT _ _ erefl id) +Notation TBLatticeType T m := (@pack T _ _ m _ _ id _ _ id). +Notation "[ 'tblatticeType' 'of' T 'for' cT ]" := (@clone T _ cT _ id) (at level 0, format "[ 'tblatticeType' 'of' T 'for' cT ]") : form_scope. Notation "[ 'tblatticeType' 'of' T 'for' cT 'with' disp ]" := - (@clone T _ cT disp _ (unit_irrelevance _ _) id) - (at level 0, format "[ 'tblatticeType' 'of' T 'for' cT 'with' disp ]") : form_scope. + (@clone_with T _ cT disp _ id) + (at level 0, format "[ 'tblatticeType' 'of' T 'for' cT 'with' disp ]") : + form_scope. Notation "[ 'tblatticeType' 'of' T ]" := [tblatticeType of T for _] (at level 0, format "[ 'tblatticeType' 'of' T ]") : form_scope. -Notation "[ 'tblatticeType' 'of' T 'with' disp ]" := [tblatticeType of T for _ with disp] +Notation "[ 'tblatticeType' 'of' T 'with' disp ]" := + [tblatticeType of T for _ with disp] (at level 0, format "[ 'tblatticeType' 'of' T 'with' disp ]") : form_scope. - End Exports. -End TBLattice. +End TBLattice. Export TBLattice.Exports. Module Import TBLatticeDef. @@ -848,34 +978,35 @@ End TBLatticeSyntax. Module CBLattice. Section ClassDef. -Structure mixin_of d (T : blatticeType d) := Mixin { +Record mixin_of d (T : blatticeType d) := Mixin { sub : T -> T -> T; _ : forall x y, y `&` sub x y = bottom; _ : forall x y, (x `&` y) `|` sub x y = x }. -Record class_of d (T : Type) := Class { - base : BLattice.class_of d T; - mixin : mixin_of (BLattice.Pack base) +Record class_of (T : Type) := Class { + base : BLattice.class_of T; + mixin_disp : unit; + mixin : mixin_of (BLattice.Pack mixin_disp base) }. Local Coercion base : class_of >-> BLattice.class_of. -Structure type d := Pack { sort; _ : class_of d sort }. +Structure type (d : unit) := Pack { sort; _ : class_of sort }. Local Coercion sort : type >-> Sortclass. Variables (T : Type) (disp : unit) (cT : type disp). -Definition class := let: Pack _ c as cT' := cT return class_of _ cT' in c. -Definition clone disp' c of (disp = disp') & phant_id class c := - @Pack disp' T c. +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. +Definition clone c of phant_id class c := @Pack disp T c. +Definition clone_with disp' c of phant_id class c := @Pack disp' T c. Let xT := let: Pack T _ := cT in T. -Notation xclass := (class : class_of _ xT). +Notation xclass := (class : class_of xT). Definition pack b0 (m0 : mixin_of (@BLattice.Pack disp T b0)) := fun bT b & phant_id (@BLattice.class disp bT) b => - fun m & phant_id m0 m => Pack (@Class disp T b m). + fun disp' m & phant_id m0 m => Pack disp (@Class T b disp' m). Definition eqType := @Equality.Pack cT xclass. Definition choiceType := @Choice.Pack cT xclass. @@ -884,40 +1015,38 @@ Definition latticeType := @Lattice.Pack disp cT xclass. Definition blatticeType := @BLattice.Pack disp cT xclass. End ClassDef. -Module Import Exports. -Coercion base : class_of >-> BLattice.class_of. -Coercion mixin : class_of >-> mixin_of. -Coercion sort : type >-> Sortclass. -Coercion eqType : type >-> Equality.type. +Module Exports. +Coercion base : class_of >-> BLattice.class_of. +Coercion mixin : class_of >-> mixin_of. +Coercion sort : type >-> Sortclass. +Coercion eqType : type >-> Equality.type. Coercion choiceType : type >-> Choice.type. Coercion porderType : type >-> POrder.type. Coercion latticeType : type >-> Lattice.type. Coercion blatticeType : type >-> BLattice.type. - Canonical eqType. Canonical choiceType. Canonical porderType. Canonical latticeType. Canonical blatticeType. - Notation cblatticeType := type. Notation cblatticeMixin := mixin_of. Notation CBLatticeMixin := Mixin. -Notation CBLatticeType T m := (@pack T _ _ m _ _ id _ id). - -Notation "[ 'cblatticeType' 'of' T 'for' cT ]" := (@clone T _ cT _ _ erefl id) +Notation CBLatticeType T m := (@pack T _ _ m _ _ id _ _ id). +Notation "[ 'cblatticeType' 'of' T 'for' cT ]" := (@clone T _ cT _ id) (at level 0, format "[ 'cblatticeType' 'of' T 'for' cT ]") : form_scope. Notation "[ 'cblatticeType' 'of' T 'for' cT 'with' disp ]" := - (@clone T _ cT disp _ (unit_irrelevance _ _) id) - (at level 0, format "[ 'cblatticeType' 'of' T 'for' cT 'with' disp ]") : form_scope. + (@clone_with T _ cT disp _ id) + (at level 0, format "[ 'cblatticeType' 'of' T 'for' cT 'with' disp ]") : + form_scope. Notation "[ 'cblatticeType' 'of' T ]" := [cblatticeType of T for _] (at level 0, format "[ 'cblatticeType' 'of' T ]") : form_scope. -Notation "[ 'cblatticeType' 'of' T 'with' disp ]" := [cblatticeType of T for _ with disp] +Notation "[ 'cblatticeType' 'of' T 'with' disp ]" := + [cblatticeType of T for _ with disp] (at level 0, format "[ 'cblatticeType' 'of' T 'with' disp ]") : form_scope. - End Exports. -End CBLattice. +End CBLattice. Export CBLattice.Exports. Module Import CBLatticeDef. @@ -936,35 +1065,35 @@ Record mixin_of d (T : tblatticeType d) (sub : T -> T -> T) := Mixin { _ : forall x, compl x = sub top x }. -Record class_of d (T : Type) := Class { - base : TBLattice.class_of d T; - mixin1 : CBLattice.mixin_of (BLattice.Pack base); - mixin2 : @mixin_of d (TBLattice.Pack base) (CBLattice.sub mixin1) +Record class_of (T : Type) := Class { + base : TBLattice.class_of T; + mixin1_disp : unit; + mixin1 : CBLattice.mixin_of (BLattice.Pack mixin1_disp base); + mixin2_disp : unit; + mixin2 : @mixin_of _ (TBLattice.Pack mixin2_disp base) (CBLattice.sub mixin1) }. Local Coercion base : class_of >-> TBLattice.class_of. -Local Coercion base2 d T (c : class_of d T) := +Local Coercion base2 T (c : class_of T) : CBLattice.class_of T := CBLattice.Class (mixin1 c). -Structure type d := Pack { sort; _ : class_of d sort }. +Structure type (d : unit) := Pack { sort; _ : class_of sort }. Local Coercion sort : type >-> Sortclass. Variables (T : Type) (disp : unit) (cT : type disp). -Definition class := let: Pack _ c as cT' := cT return class_of _ cT' in c. -Definition clone disp' c of (disp = disp') & phant_id class c := - @Pack disp' T c. +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. +Definition clone c of phant_id class c := @Pack disp T c. +Definition clone_with disp' c of phant_id class c := @Pack disp' T c. Let xT := let: Pack T _ := cT in T. -Notation xclass := (class : class_of _ xT). +Notation xclass := (class : class_of xT). Definition pack := - fun bT b & phant_id (@TBLattice.class disp bT) - (b : TBLattice.class_of disp T) => - fun m1T m1 & phant_id (@CBLattice.class disp m1T) - (@CBLattice.Class disp T b m1) => - fun (m2 : @mixin_of disp (@TBLattice.Pack disp T b) (CBLattice.sub m1)) => - Pack (@Class disp T b m1 m2). + fun bT b & phant_id (@TBLattice.class disp bT) b => + fun disp1 m1T m1 & phant_id (@CBLattice.class disp1 m1T) + (@CBLattice.Class _ _ _ m1) => + fun disp2 m2 => Pack disp (@Class T b disp1 m1 disp2 m2). Definition eqType := @Equality.Pack cT xclass. Definition choiceType := @Choice.Pack cT xclass. @@ -977,20 +1106,19 @@ Definition tbd_cblatticeType := @CBLattice.Pack disp tblatticeType xclass. End ClassDef. -Module Import Exports. -Coercion base : class_of >-> TBLattice.class_of. -Coercion base2 : class_of >-> CBLattice.class_of. -Coercion mixin1 : class_of >-> CBLattice.mixin_of. -Coercion mixin2 : class_of >-> mixin_of. -Coercion sort : type >-> Sortclass. -Coercion eqType : type >-> Equality.type. +Module Exports. +Coercion base : class_of >-> TBLattice.class_of. +Coercion base2 : class_of >-> CBLattice.class_of. +Coercion mixin1 : class_of >-> CBLattice.mixin_of. +Coercion mixin2 : class_of >-> mixin_of. +Coercion sort : type >-> Sortclass. +Coercion eqType : type >-> Equality.type. Coercion choiceType : type >-> Choice.type. Coercion porderType : type >-> POrder.type. Coercion latticeType : type >-> Lattice.type. Coercion blatticeType : type >-> BLattice.type. Coercion tblatticeType : type >-> TBLattice.type. Coercion cblatticeType : type >-> CBLattice.type. - Canonical eqType. Canonical choiceType. Canonical porderType. @@ -999,29 +1127,28 @@ Canonical blatticeType. Canonical tblatticeType. Canonical cblatticeType. Canonical tbd_cblatticeType. - Notation ctblatticeType := type. Notation ctblatticeMixin := mixin_of. Notation CTBLatticeMixin := Mixin. -Notation CTBLatticeType T m := (@pack T _ _ _ id _ _ id m). - -Notation "[ 'cblatticeType' 'of' T 'for' cT ]" := (@clone T _ cT _ _ erefl id) - (at level 0, format "[ 'cblatticeType' 'of' T 'for' cT ]") : form_scope. -Notation "[ 'cblatticeType' 'of' T 'for' cT 'with' disp ]" := - (@clone T _ cT disp _ (unit_irrelevance _ _) id) - (at level 0, format "[ 'cblatticeType' 'of' T 'for' cT 'with' disp ]") : form_scope. -Notation "[ 'cblatticeType' 'of' T ]" := [cblatticeType of T for _] - (at level 0, format "[ 'cblatticeType' 'of' T ]") : form_scope. -Notation "[ 'cblatticeType' 'of' T 'with' disp ]" := [cblatticeType of T for _ with disp] - (at level 0, format "[ 'cblatticeType' 'of' T 'with' disp ]") : form_scope. - +Notation CTBLatticeType T m := (@pack T _ _ _ id _ _ _ id _ m). +Notation "[ 'ctblatticeType' 'of' T 'for' cT ]" := (@clone T _ cT _ id) + (at level 0, format "[ 'ctblatticeType' 'of' T 'for' cT ]") : form_scope. +Notation "[ 'ctblatticeType' 'of' T 'for' cT 'with' disp ]" := + (@clone_with T _ cT disp _ id) + (at level 0, format "[ 'ctblatticeType' 'of' T 'for' cT 'with' disp ]") + : form_scope. +Notation "[ 'ctblatticeType' 'of' T ]" := [ctblatticeType of T for _] + (at level 0, format "[ 'ctblatticeType' 'of' T ]") : form_scope. +Notation "[ 'ctblatticeType' 'of' T 'with' disp ]" := + [ctblatticeType of T for _ with disp] + (at level 0, format "[ 'ctblatticeType' 'of' T 'with' disp ]") : + form_scope. Notation "[ 'default_ctblatticeType' 'of' T ]" := - (@pack T _ _ _ id _ _ id (fun=> erefl)) + (@pack T _ _ _ id _ _ id (Mixin (fun=> erefl))) (at level 0, format "[ 'default_ctblatticeType' 'of' T ]") : form_scope. - End Exports. -End CTBLattice. +End CTBLattice. Export CTBLattice.Exports. Module Import CTBLatticeDef. @@ -1041,13 +1168,13 @@ Module FinPOrder. Section ClassDef. Record class_of T := Class { - base : Finite.class_of T; - mixin : POrder.mixin_of (Equality.Pack base) + base : POrder.class_of T; + mixin : Finite.mixin_of (Equality.Pack base) }. -Local Coercion base : class_of >-> Finite.class_of. -Definition base2 T (c : class_of T) := (POrder.Class (mixin c)). -Local Coercion base2 : class_of >-> POrder.class_of. +Local Coercion base : class_of >-> POrder.class_of. +Local Coercion base2 T (c : class_of T) : Finite.class_of T := + Finite.Class (mixin c). Structure type (disp : unit) := Pack { sort; _ : class_of sort }. @@ -1060,615 +1187,437 @@ Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). Definition pack := - fun b bT & phant_id (Finite.class bT) b => - fun m mT & phant_id (POrder.mixin_of mT) m => + fun bT b & phant_id (@POrder.class disp bT) b => + fun mT m & phant_id (@Finite.class mT) (@Finite.Class _ _ m) => Pack disp (@Class T b m). Definition eqType := @Equality.Pack cT xclass. -Definition finType := @Finite.Pack cT xclass. Definition choiceType := @Choice.Pack cT xclass. +Definition countType := @Countable.Pack cT xclass. +Definition finType := @Finite.Pack cT xclass. Definition porderType := @POrder.Pack disp cT xclass. +Definition count_porderType := @POrder.Pack disp countType xclass. Definition fin_porderType := @POrder.Pack disp finType xclass. End ClassDef. -Module Import Exports. -Coercion base : class_of >-> Finite.class_of. -Coercion base2 : class_of >-> POrder.class_of. -Coercion sort : type >-> Sortclass. +Module Exports. +Coercion base : class_of >-> POrder.class_of. +Coercion base2 : class_of >-> Finite.class_of. +Coercion sort : type >-> Sortclass. Coercion eqType : type >-> Equality.type. -Coercion finType : type >-> Finite.type. Coercion choiceType : type >-> Choice.type. +Coercion countType : type >-> Countable.type. +Coercion finType : type >-> Finite.type. Coercion porderType : type >-> POrder.type. - Canonical eqType. -Canonical finType. Canonical choiceType. +Canonical countType. +Canonical finType. Canonical porderType. +Canonical count_porderType. Canonical fin_porderType. - Notation finPOrderType := type. -Notation "[ 'finPOrderType' 'of' T ]" := (@pack T _ _ erefl _ _ phant_id _ _ phant_id) +Notation "[ 'finPOrderType' 'of' T ]" := (@pack T _ _ _ id _ _ id) (at level 0, format "[ 'finPOrderType' 'of' T ]") : form_scope. - End Exports. -End FinPOrder. +End FinPOrder. Import FinPOrder.Exports. Bind Scope cpo_sort with FinPOrder.sort. Module FinLattice. Section ClassDef. -Record class_of d (T : Type) := Class { - base : FinPOrder.class_of T; - mixin : Lattice.mixin_of (POrder.Pack d base) +Record class_of (T : Type) := Class { + base : TBLattice.class_of T; + mixin : Finite.mixin_of (Equality.Pack base); }. -Local Coercion base : class_of >-> FinPOrder.class_of. -Definition base2 d T (c : class_of d T) := (Lattice.Class (mixin c)). -Local Coercion base2 : class_of >-> Lattice.class_of. +Local Coercion base : class_of >-> TBLattice.class_of. +Local Coercion base2 T (c : class_of T) : Finite.class_of T := + Finite.Class (mixin c). +Local Coercion base3 T (c : class_of T) : FinPOrder.class_of T := + @FinPOrder.Class T c c. -Structure type (display : unit) := - Pack { sort; _ : class_of display sort }. +Structure type (disp : unit) := Pack { sort; _ : class_of sort }. Local Coercion sort : type >-> Sortclass. Variables (T : Type) (disp : unit) (cT : type disp). -Definition class := let: Pack _ c as cT' := cT return class_of _ cT' in c. +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. Let xT := let: Pack T _ := cT in T. -Notation xclass := (class : class_of _ xT). +Notation xclass := (class : class_of xT). -Definition pack disp := - fun bT b & phant_id (@FinPOrder.class disp bT) b => - fun mT m & phant_id (@Lattice.mixin disp mT) m => - Pack (@Class disp T b m). +Definition pack := + fun bT b & phant_id (@TBLattice.class disp bT) b => + fun mT m & phant_id (@Finite.class mT) (@Finite.Class _ _ m) => + Pack disp (@Class T b m). Definition eqType := @Equality.Pack cT xclass. -Definition finType := @Finite.Pack cT xclass. Definition choiceType := @Choice.Pack cT xclass. +Definition countType := @Countable.Pack cT xclass. +Definition finType := @Finite.Pack cT xclass. Definition porderType := @POrder.Pack disp cT xclass. Definition finPOrderType := @FinPOrder.Pack disp cT xclass. Definition latticeType := @Lattice.Pack disp cT xclass. -Definition fin_latticeType := @Lattice.Pack disp finPOrderType xclass. +Definition blatticeType := @BLattice.Pack disp cT xclass. +Definition tblatticeType := @TBLattice.Pack disp cT xclass. +Definition count_latticeType := @Lattice.Pack disp countType xclass. +Definition count_blatticeType := @BLattice.Pack disp countType xclass. +Definition count_tblatticeType := @TBLattice.Pack disp countType xclass. +Definition fin_latticeType := @Lattice.Pack disp finType xclass. +Definition fin_blatticeType := @BLattice.Pack disp finType xclass. +Definition fin_tblatticeType := @TBLattice.Pack disp finType xclass. +Definition finPOrder_latticeType := @Lattice.Pack disp finPOrderType xclass. +Definition finPOrder_blatticeType := @BLattice.Pack disp finPOrderType xclass. +Definition finPOrder_tblatticeType := @TBLattice.Pack disp finPOrderType xclass. End ClassDef. -Module Import Exports. -Coercion base : class_of >-> FinPOrder.class_of. -Coercion base2 : class_of >-> Lattice.class_of. -Coercion sort : type >-> Sortclass. -Coercion eqType : type >-> Equality.type. -Coercion finType : type >-> Finite.type. +Module Exports. +Coercion base : class_of >-> TBLattice.class_of. +Coercion base2 : class_of >-> Finite.class_of. +Coercion base3 : class_of >-> FinPOrder.class_of. +Coercion sort : type >-> Sortclass. +Coercion eqType : type >-> Equality.type. Coercion choiceType : type >-> Choice.type. +Coercion countType : type >-> Countable.type. +Coercion finType : type >-> Finite.type. Coercion porderType : type >-> POrder.type. Coercion finPOrderType : type >-> FinPOrder.type. Coercion latticeType : type >-> Lattice.type. - +Coercion blatticeType : type >-> BLattice.type. +Coercion tblatticeType : type >-> TBLattice.type. Canonical eqType. -Canonical finType. Canonical choiceType. +Canonical countType. +Canonical finType. Canonical porderType. Canonical finPOrderType. Canonical latticeType. +Canonical blatticeType. +Canonical tblatticeType. +Canonical count_latticeType. +Canonical count_blatticeType. +Canonical count_tblatticeType. Canonical fin_latticeType. - +Canonical fin_blatticeType. +Canonical fin_tblatticeType. +Canonical finPOrder_latticeType. +Canonical finPOrder_blatticeType. +Canonical finPOrder_tblatticeType. Notation finLatticeType := type. - -Notation "[ 'finLatticeType' 'of' T ]" := (@pack T _ _ erefl _ _ phant_id _ _ phant_id) +Notation "[ 'finLatticeType' 'of' T ]" := (@pack T _ _ _ id _ _ id) (at level 0, format "[ 'finLatticeType' 'of' T ]") : form_scope. End Exports. -End FinLattice. +End FinLattice. Export FinLattice.Exports. -Module FinTotal. +Module FinCLattice. Section ClassDef. -Record class_of d (T : Type) := Class { - base : FinLattice.class_of d T; - mixin : total (<=%O : rel (POrder.Pack d base)) +Record class_of (T : Type) := Class { + base : CTBLattice.class_of T; + mixin : Finite.mixin_of (Equality.Pack base); }. -Local Coercion base : class_of >-> FinLattice.class_of. -Definition base2 d T (c : class_of d T) := - (@Total.Class _ _ (FinLattice.base2 c) (@mixin _ _ c)). -Local Coercion base2 : class_of >-> Total.class_of. +Local Coercion base : class_of >-> CTBLattice.class_of. +Local Coercion base2 T (c : class_of T) : Finite.class_of T := + Finite.Class (mixin c). +Local Coercion base3 T (c : class_of T) : FinLattice.class_of T := + @FinLattice.Class T c c. -Structure type (display : unit) := - Pack { sort; _ : class_of display sort }. +Structure type (disp : unit) := Pack { sort; _ : class_of sort }. Local Coercion sort : type >-> Sortclass. Variables (T : Type) (disp : unit) (cT : type disp). -Definition class := let: Pack _ c as cT' := cT return class_of _ cT' in c. +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. Let xT := let: Pack T _ := cT in T. -Notation xclass := (class : class_of _ xT). +Notation xclass := (class : class_of xT). -Definition pack disp := - fun bT b & phant_id (@FinPOrder.class disp bT) b => - fun mT m & phant_id (@Total.mixin disp mT) m => - Pack (@Class disp T b m). +Definition pack := + fun bT b & phant_id (@CTBLattice.class disp bT) b => + fun mT m & phant_id (@Finite.class mT) (@Finite.Class _ _ m) => + Pack disp (@Class T b m). Definition eqType := @Equality.Pack cT xclass. -Definition finType := @Finite.Pack cT xclass. Definition choiceType := @Choice.Pack cT xclass. +Definition countType := @Countable.Pack cT xclass. +Definition finType := @Finite.Pack cT xclass. Definition porderType := @POrder.Pack disp cT xclass. Definition finPOrderType := @FinPOrder.Pack disp cT xclass. Definition latticeType := @Lattice.Pack disp cT xclass. +Definition blatticeType := @BLattice.Pack disp cT xclass. +Definition tblatticeType := @TBLattice.Pack disp cT xclass. Definition finLatticeType := @FinLattice.Pack disp cT xclass. -Definition orderType := @Total.Pack disp cT xclass. -Definition fin_orderType := @Total.Pack disp finLatticeType xclass. +Definition cblatticeType := @CBLattice.Pack disp cT xclass. +Definition ctblatticeType := @CTBLattice.Pack disp cT xclass. +Definition count_cblatticeType := @CBLattice.Pack disp countType xclass. +Definition count_ctblatticeType := @CTBLattice.Pack disp countType xclass. +Definition fin_cblatticeType := @CBLattice.Pack disp finType xclass. +Definition fin_ctblatticeType := @CTBLattice.Pack disp finType xclass. +Definition finPOrder_cblatticeType := @CBLattice.Pack disp finPOrderType xclass. +Definition finPOrder_ctblatticeType := + @CTBLattice.Pack disp finPOrderType xclass. +Definition finLattice_cblatticeType := + @CBLattice.Pack disp finLatticeType xclass. +Definition finLattice_ctblatticeType := + @CTBLattice.Pack disp finLatticeType xclass. End ClassDef. -Module Import Exports. -Coercion base : class_of >-> FinLattice.class_of. -Coercion base2 : class_of >-> Total.class_of. -Coercion sort : type >-> Sortclass. -Coercion eqType : type >-> Equality.type. -Coercion finType : type >-> Finite.type. +Module Exports. +Coercion base : class_of >-> CTBLattice.class_of. +Coercion base2 : class_of >-> Finite.class_of. +Coercion base3 : class_of >-> FinLattice.class_of. +Coercion sort : type >-> Sortclass. +Coercion eqType : type >-> Equality.type. Coercion choiceType : type >-> Choice.type. +Coercion countType : type >-> Countable.type. +Coercion finType : type >-> Finite.type. Coercion porderType : type >-> POrder.type. Coercion finPOrderType : type >-> FinPOrder.type. Coercion latticeType : type >-> Lattice.type. +Coercion blatticeType : type >-> BLattice.type. +Coercion tblatticeType : type >-> TBLattice.type. Coercion finLatticeType : type >-> FinLattice.type. -Coercion orderType : type >-> Total.type. - +Coercion cblatticeType : type >-> CBLattice.type. +Coercion ctblatticeType : type >-> CTBLattice.type. Canonical eqType. -Canonical finType. Canonical choiceType. +Canonical countType. +Canonical finType. Canonical porderType. Canonical finPOrderType. Canonical latticeType. +Canonical blatticeType. +Canonical tblatticeType. Canonical finLatticeType. -Canonical orderType. -Canonical fin_orderType. - -Notation finOrderType := type. - -Notation "[ 'finOrderType' 'of' T ]" := (@pack T _ _ erefl _ _ phant_id _ _ phant_id) - (at level 0, format "[ 'finOrderType' 'of' T ]") : form_scope. +Canonical cblatticeType. +Canonical ctblatticeType. +Canonical count_cblatticeType. +Canonical count_ctblatticeType. +Canonical fin_cblatticeType. +Canonical fin_ctblatticeType. +Canonical finPOrder_cblatticeType. +Canonical finPOrder_ctblatticeType. +Canonical finLattice_cblatticeType. +Canonical finLattice_ctblatticeType. +Notation finCLatticeType := type. +Notation "[ 'finCLatticeType' 'of' T ]" := (@pack T _ _ _ id _ _ id) + (at level 0, format "[ 'finCLatticeType' 'of' T ]") : form_scope. End Exports. -End FinTotal. -Export Total.Exports. +End FinCLattice. +Export FinCLattice.Exports. -Module FinBLattice. +Module FinTotal. Section ClassDef. -Record class_of d (T : Type) := Class { - base : FinLattice.class_of d T; - mixin : BLattice.mixin_of (FinPOrder.Pack d base) +Record class_of (T : Type) := Class { + base : FinLattice.class_of T; + mixin_disp : unit; + mixin : Total.mixin_of (Lattice.Pack mixin_disp base) }. Local Coercion base : class_of >-> FinLattice.class_of. -Definition base2 d T (c : class_of d T) := - (@BLattice.Class _ _ (FinLattice.base2 c) (@mixin _ _ c)). -Local Coercion base2 : class_of >-> BLattice.class_of. +Local Coercion base2 T (c : class_of T) : Total.class_of T := + @Total.Class _ c _ (mixin (c := c)). -Structure type (display : unit) := - Pack { sort; _ : class_of display sort }. +Structure type (disp : unit) := Pack { sort; _ : class_of sort }. Local Coercion sort : type >-> Sortclass. Variables (T : Type) (disp : unit) (cT : type disp). -Definition class := let: Pack _ c as cT' := cT return class_of _ cT' in c. +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. Let xT := let: Pack T _ := cT in T. -Notation xclass := (class : class_of _ xT). +Notation xclass := (class : class_of xT). -Definition pack disp := - fun bT b & phant_id (@FinPOrder.class disp bT) b => - fun mT m & phant_id (@BLattice.mixin disp mT) m => - Pack (@Class disp T b m). +Definition pack := + fun bT b & phant_id (@FinLattice.class disp bT) b => + fun disp' mT m & phant_id (@Total.class disp mT) (@Total.Class _ _ _ m) => + Pack disp (@Class T b disp' m). Definition eqType := @Equality.Pack cT xclass. -Definition finType := @Finite.Pack cT xclass. Definition choiceType := @Choice.Pack cT xclass. +Definition countType := @Countable.Pack cT xclass. +Definition finType := @Finite.Pack cT xclass. Definition porderType := @POrder.Pack disp cT xclass. Definition finPOrderType := @FinPOrder.Pack disp cT xclass. Definition latticeType := @Lattice.Pack disp cT xclass. -Definition finLatticeType := @FinLattice.Pack disp cT xclass. Definition blatticeType := @BLattice.Pack disp cT xclass. -Definition fin_blatticeType := @BLattice.Pack disp finLatticeType xclass. +Definition tblatticeType := @TBLattice.Pack disp cT xclass. +Definition finLatticeType := @FinLattice.Pack disp cT xclass. +Definition orderType := @Total.Pack disp cT xclass. +Definition order_countType := @Countable.Pack orderType xclass. +Definition order_finType := @Finite.Pack orderType xclass. +Definition order_finPOrderType := @FinPOrder.Pack disp orderType xclass. +Definition order_blatticeType := @BLattice.Pack disp orderType xclass. +Definition order_tblatticeType := @TBLattice.Pack disp orderType xclass. +Definition order_finLatticeType := @FinLattice.Pack disp orderType xclass. End ClassDef. -Module Import Exports. -Coercion base : class_of >-> FinLattice.class_of. -Coercion base2 : class_of >-> BLattice.class_of. -Coercion sort : type >-> Sortclass. -Coercion eqType : type >-> Equality.type. -Coercion finType : type >-> Finite.type. +Module Exports. +Coercion base : class_of >-> FinLattice.class_of. +Coercion base2 : class_of >-> Total.class_of. +Coercion sort : type >-> Sortclass. +Coercion eqType : type >-> Equality.type. Coercion choiceType : type >-> Choice.type. +Coercion countType : type >-> Countable.type. +Coercion finType : type >-> Finite.type. Coercion porderType : type >-> POrder.type. Coercion finPOrderType : type >-> FinPOrder.type. Coercion latticeType : type >-> Lattice.type. -Coercion finLatticeType : type >-> FinLattice.type. Coercion blatticeType : type >-> BLattice.type. - +Coercion tblatticeType : type >-> TBLattice.type. +Coercion finLatticeType : type >-> FinLattice.type. +Coercion orderType : type >-> Total.type. Canonical eqType. -Canonical finType. Canonical choiceType. +Canonical countType. +Canonical finType. Canonical porderType. Canonical finPOrderType. Canonical latticeType. -Canonical finLatticeType. Canonical blatticeType. -Canonical fin_blatticeType. - -Notation finBLatticeType := type. - -Notation "[ 'finBLatticeType' 'of' T ]" := (@pack T _ _ erefl _ _ phant_id _ _ phant_id) - (at level 0, format "[ 'finBLatticeType' 'of' T ]") : form_scope. +Canonical tblatticeType. +Canonical finLatticeType. +Canonical orderType. +Canonical order_countType. +Canonical order_finType. +Canonical order_finPOrderType. +Canonical order_blatticeType. +Canonical order_tblatticeType. +Canonical order_finLatticeType. +Notation finOrderType := type. +Notation "[ 'finOrderType' 'of' T ]" := (@pack T _ _ _ id _ _ _ id) + (at level 0, format "[ 'finOrderType' 'of' T ]") : form_scope. End Exports. -End FinBLattice. -Export FinBLattice.Exports. - -Module FinTBLattice. -Section ClassDef. +End FinTotal. +Export Total.Exports. -Record class_of d (T : Type) := Class { - base : FinBLattice.class_of d T; - mixin : TBLattice.mixin_of (FinPOrder.Pack d base) -}. +(************) +(* CONVERSE *) +(************) -Local Coercion base : class_of >-> FinBLattice.class_of. -Definition base2 d T (c : class_of d T) := - (@TBLattice.Class _ _ c (@mixin _ _ c)). -Local Coercion base2 : class_of >-> TBLattice.class_of. +Definition converse T : Type := T. +Definition converse_display : unit -> unit. Proof. exact. Qed. +Local Notation "T ^c" := (converse T) (at level 2, format "T ^c") : type_scope. -Structure type (display : unit) := - Pack { sort; _ : class_of display sort }. +Module Import ConverseSyntax. -Local Coercion sort : type >-> Sortclass. +Notation "<=^c%O" := (@le (converse_display _) _) : order_scope. +Notation ">=^c%O" := (@ge (converse_display _) _) : order_scope. +Notation ">=^c%O" := (@ge (converse_display _) _) : order_scope. +Notation "<^c%O" := (@lt (converse_display _) _) : order_scope. +Notation ">^c%O" := (@gt (converse_display _) _) : order_scope. +Notation "=<^c%O" := (@comparable (converse_display _) _) : order_scope. +Notation "><^c%O" := (fun x y => ~~ (@comparable (converse_display _) _ x y)) : + order_scope. -Variables (T : Type) (disp : unit) (cT : type disp). +Notation "<=^c y" := (>=^c%O y) : order_scope. +Notation "<=^c y :> T" := (<=^c (y : T)) : order_scope. +Notation ">=^c y" := (<=^c%O y) : order_scope. +Notation ">=^c y :> T" := (>=^c (y : T)) : order_scope. -Definition class := let: Pack _ c as cT' := cT return class_of _ cT' in c. -Let xT := let: Pack T _ := cT in T. -Notation xclass := (class : class_of _ xT). +Notation "<^c y" := (>^c%O y) : order_scope. +Notation "<^c y :> T" := (<^c (y : T)) : order_scope. +Notation ">^c y" := (<^c%O y) : order_scope. +Notation ">^c y :> T" := (>^c (y : T)) : order_scope. -Definition pack disp := - fun bT b & phant_id (@FinBLattice.class disp bT) b => - fun mT m & phant_id (@TBLattice.mixin disp mT) m => - Pack (@Class disp T b m). +Notation ">=<^c y" := (>=<^c%O y) : order_scope. +Notation ">=<^c y :> T" := (>=<^c (y : T)) : order_scope. -Definition eqType := @Equality.Pack cT xclass. -Definition finType := @Finite.Pack cT xclass. -Definition choiceType := @Choice.Pack cT xclass. -Definition porderType := @POrder.Pack disp cT xclass. -Definition finPOrderType := @FinPOrder.Pack disp cT xclass. -Definition latticeType := @Lattice.Pack disp cT xclass. -Definition finLatticeType := @FinLattice.Pack disp cT xclass. -Definition blatticeType := @BLattice.Pack disp cT xclass. -Definition finBLatticeType := @FinBLattice.Pack disp cT xclass. -Definition tblatticeType := @TBLattice.Pack disp cT xclass. -Definition fin_blatticeType := @TBLattice.Pack disp finBLatticeType xclass. +Notation "x <=^c y" := (<=^c%O x y) : order_scope. +Notation "x <=^c y :> T" := ((x : T) <=^c (y : T)) : order_scope. +Notation "x >=^c y" := (y <=^c x) (only parsing) : order_scope. +Notation "x >=^c y :> T" := ((x : T) >=^c (y : T)) (only parsing) : order_scope. -End ClassDef. +Notation "x <^c y" := (<^c%O x y) : order_scope. +Notation "x <^c y :> T" := ((x : T) <^c (y : T)) : order_scope. +Notation "x >^c y" := (y <^c x) (only parsing) : order_scope. +Notation "x >^c y :> T" := ((x : T) >^c (y : T)) (only parsing) : order_scope. -Module Import Exports. -Coercion base : class_of >-> FinBLattice.class_of. -Coercion base2 : class_of >-> TBLattice.class_of. -Coercion sort : type >-> Sortclass. -Coercion eqType : type >-> Equality.type. -Coercion finType : type >-> Finite.type. -Coercion choiceType : type >-> Choice.type. -Coercion porderType : type >-> POrder.type. -Coercion finPOrderType : type >-> FinPOrder.type. -Coercion latticeType : type >-> Lattice.type. -Coercion finLatticeType : type >-> FinLattice.type. -Coercion blatticeType : type >-> BLattice.type. -Coercion finBLatticeType : type >-> FinBLattice.type. -Coercion tblatticeType : type >-> TBLattice.type. +Notation "x <=^c y <=^c z" := ((x <=^c y) && (y <=^c z)) : order_scope. +Notation "x <^c y <=^c z" := ((x <^c y) && (y <=^c z)) : order_scope. +Notation "x <=^c y <^c z" := ((x <=^c y) && (y <^c z)) : order_scope. +Notation "x <^c y <^c z" := ((x <^c y) && (y <^c z)) : order_scope. -Canonical eqType. -Canonical finType. -Canonical choiceType. -Canonical porderType. -Canonical finPOrderType. -Canonical latticeType. -Canonical finLatticeType. -Canonical blatticeType. -Canonical finBLatticeType. -Canonical tblatticeType. -Canonical fin_blatticeType. +Notation "x <=^c y ?= 'iff' C" := ( R" := ((x : R) <=^c (y : R) ?= iff C) + (only parsing) : order_scope. -Notation finTBLatticeType := type. +Notation ">=<^c x" := (>=<^c%O x) : order_scope. +Notation ">=<^c x :> T" := (>=<^c (x : T)) (only parsing) : order_scope. +Notation "x >=<^c y" := (>=<^c%O x y) : order_scope. -Notation "[ 'finTBLatticeType' 'of' T ]" := (@pack T _ _ erefl _ _ phant_id _ _ phant_id) - (at level 0, format "[ 'finTBLatticeType' 'of' T ]") : form_scope. -End Exports. -End FinTBLattice. +Notation "><^c x" := (fun y => ~~ (>=<^c%O x y)) : order_scope. +Notation "><^c x :> T" := (><^c (x : T)) (only parsing) : order_scope. +Notation "x ><^c y" := (~~ (><^c%O x y)) : order_scope. -Export FinTBLattice.Exports. +Notation "x `&^c` y" := (@meet (converse_display _) _ x y). +Notation "x `|^c` y" := (@join (converse_display _) _ x y). -Module FinCBLattice. -Section ClassDef. +End ConverseSyntax. -Record class_of d (T : Type) := Class { - base : FinBLattice.class_of d T; - mixin : CBLattice.mixin_of (BLattice.Pack base) -}. +(**********) +(* THEORY *) +(**********) -Local Coercion base : class_of >-> FinBLattice.class_of. -Definition base2 d T (c : class_of d T) := - (@CBLattice.Class _ _ c (@mixin _ _ c)). -Local Coercion base2 : class_of >-> CBLattice.class_of. +Module Import POrderTheory. +Section POrderTheory. +Import POrderDef. -Structure type (display : unit) := - Pack { sort; _ : class_of display sort }. - -Local Coercion sort : type >-> Sortclass. - -Variables (T : Type) (disp : unit) (cT : type disp). - -Definition class := let: Pack _ c as cT' := cT return class_of _ cT' in c. -Let xT := let: Pack T _ := cT in T. -Notation xclass := (class : class_of _ xT). - -Definition pack disp := - fun bT b & phant_id (@FinBLattice.class disp bT) b => - fun mT m & phant_id (@CBLattice.mixin disp mT) m => - Pack (@Class disp T b m). - -Definition eqType := @Equality.Pack cT xclass. -Definition finType := @Finite.Pack cT xclass. -Definition choiceType := @Choice.Pack cT xclass. -Definition porderType := @POrder.Pack disp cT xclass. -Definition finPOrderType := @FinPOrder.Pack disp cT xclass. -Definition latticeType := @Lattice.Pack disp cT xclass. -Definition finLatticeType := @FinLattice.Pack disp cT xclass. -Definition blatticeType := @BLattice.Pack disp cT xclass. -Definition finBLatticeType := @FinBLattice.Pack disp cT xclass. -Definition cblatticeType := @CBLattice.Pack disp cT xclass. -Definition fin_blatticeType := @CBLattice.Pack disp finBLatticeType xclass. - -End ClassDef. - -Module Import Exports. -Coercion base : class_of >-> FinBLattice.class_of. -Coercion base2 : class_of >-> CBLattice.class_of. -Coercion sort : type >-> Sortclass. -Coercion eqType : type >-> Equality.type. -Coercion finType : type >-> Finite.type. -Coercion choiceType : type >-> Choice.type. -Coercion porderType : type >-> POrder.type. -Coercion finPOrderType : type >-> FinPOrder.type. -Coercion latticeType : type >-> Lattice.type. -Coercion finLatticeType : type >-> FinLattice.type. -Coercion blatticeType : type >-> BLattice.type. -Coercion finBLatticeType : type >-> FinBLattice.type. -Coercion cblatticeType : type >-> CBLattice.type. - -Canonical eqType. -Canonical finType. -Canonical choiceType. -Canonical porderType. -Canonical finPOrderType. -Canonical latticeType. -Canonical finLatticeType. -Canonical blatticeType. -Canonical finBLatticeType. -Canonical cblatticeType. -Canonical fin_blatticeType. - -Notation finCBLatticeType := type. - -Notation "[ 'finCBLatticeType' 'of' T ]" := (@pack T _ _ erefl _ _ phant_id _ _ phant_id) - (at level 0, format "[ 'finCBLatticeType' 'of' T ]") : form_scope. -End Exports. -End FinCBLattice. - -Export FinCBLattice.Exports. - -Module FinCTBLattice. -Section ClassDef. - -Record class_of d (T : Type) := Class { - base : FinTBLattice.class_of d T; - mixin1 : CBLattice.mixin_of (BLattice.Pack base); - mixin2 : @CTBLattice.mixin_of d (TBLattice.Pack base) (CBLattice.sub mixin1) -}. - -Local Coercion base : class_of >-> FinTBLattice.class_of. -Definition base1 d T (c : class_of d T) := - (@FinCBLattice.Class _ _ c (@mixin1 _ _ c)). -Local Coercion base1 : class_of >-> FinCBLattice.class_of. -Definition base2 d T (c : class_of d T) := - (@CTBLattice.Class _ _ c (@mixin1 _ _ c) (@mixin2 _ _ c)). -Local Coercion base2 : class_of >-> CTBLattice.class_of. - -Structure type (display : unit) := - Pack { sort; _ : class_of display sort }. - -Local Coercion sort : type >-> Sortclass. - -Variables (T : Type) (disp : unit) (cT : type disp). - -Definition class := let: Pack _ c as cT' := cT return class_of _ cT' in c. -Let xT := let: Pack T _ := cT in T. -Notation xclass := (class : class_of _ xT). - -Definition pack disp := - fun bT b & phant_id (@FinTBLattice.class disp bT) b => - fun m1T m1 & phant_id (@CTBLattice.mixin1 disp m1T) m1 => - fun m2T m2 & phant_id (@CTBLattice.mixin2 disp m2T) m2 => - Pack (@Class disp T b m1 m2). - -Definition eqType := @Equality.Pack cT xclass. -Definition finType := @Finite.Pack cT xclass. -Definition choiceType := @Choice.Pack cT xclass. -Definition porderType := @POrder.Pack disp cT xclass. -Definition finPOrderType := @FinPOrder.Pack disp cT xclass. -Definition latticeType := @Lattice.Pack disp cT xclass. -Definition finLatticeType := @FinLattice.Pack disp cT xclass. -Definition blatticeType := @BLattice.Pack disp cT xclass. -Definition finBLatticeType := @FinBLattice.Pack disp cT xclass. -Definition cblatticeType := @CBLattice.Pack disp cT xclass. -Definition tblatticeType := @TBLattice.Pack disp cT xclass. -Definition finTBLatticeType := @FinTBLattice.Pack disp cT xclass. -Definition finCBLatticeType := @FinCBLattice.Pack disp cT xclass. -Definition ctblatticeType := @CTBLattice.Pack disp cT xclass. -Definition fintb_ctblatticeType := @CTBLattice.Pack disp finTBLatticeType xclass. -Definition fincb_ctblatticeType := @CTBLattice.Pack disp finCBLatticeType xclass. - -End ClassDef. - -Module Import Exports. -Coercion base : class_of >-> FinTBLattice.class_of. -Coercion base1 : class_of >-> FinCBLattice.class_of. -Coercion base2 : class_of >-> CTBLattice.class_of. -Coercion sort : type >-> Sortclass. - -Coercion eqType : type >-> Equality.type. -Coercion finType : type >-> Finite.type. -Coercion choiceType : type >-> Choice.type. -Coercion porderType : type >-> POrder.type. -Coercion finPOrderType : type >-> FinPOrder.type. -Coercion latticeType : type >-> Lattice.type. -Coercion finLatticeType : type >-> FinLattice.type. -Coercion blatticeType : type >-> BLattice.type. -Coercion finBLatticeType : type >-> FinBLattice.type. -Coercion cblatticeType : type >-> CBLattice.type. -Coercion tblatticeType : type >-> TBLattice.type. -Coercion finTBLatticeType : type >-> FinTBLattice.type. -Coercion finCBLatticeType : type >-> FinCBLattice.type. -Coercion ctblatticeType : type >-> CTBLattice.type. -Coercion fintb_ctblatticeType : type >-> CTBLattice.type. -Coercion fincb_ctblatticeType : type >-> CTBLattice.type. - - -Canonical eqType. -Canonical finType. -Canonical choiceType. -Canonical porderType. -Canonical finPOrderType. -Canonical latticeType. -Canonical finLatticeType. -Canonical blatticeType. -Canonical finBLatticeType. -Canonical cblatticeType. -Canonical tblatticeType. -Canonical finTBLatticeType. -Canonical finCBLatticeType. -Canonical ctblatticeType. -Canonical fintb_ctblatticeType. -Canonical fincb_ctblatticeType. - -Notation finCTBLatticeType := type. - -Notation "[ 'finCTBLatticeType' 'of' T ]" := - (@pack T _ _ erefl _ _ phant_id _ _ phant_id _ _ phant_id) - (at level 0, format "[ 'finCTBLatticeType' 'of' T ]") : form_scope. -End Exports. -End FinCTBLattice. - -Export FinCTBLattice.Exports. - -(***********) -(* REVERSE *) -(***********) - -Definition reverse T : Type := T. -Definition reverse_display : unit -> unit. Proof. exact. Qed. -Local Notation "T ^r" := (reverse T) (at level 2, format "T ^r") : type_scope. - -Module Import ReverseSyntax. - -Notation "<=^r%O" := (@le (reverse_display _) _) : order_scope. -Notation ">=^r%O" := (@ge (reverse_display _) _) : order_scope. -Notation ">=^r%O" := (@ge (reverse_display _) _) : order_scope. -Notation "<^r%O" := (@lt (reverse_display _) _) : order_scope. -Notation ">^r%O" := (@gt (reverse_display _) _) : order_scope. -Notation "=<^r%O" := (@comparable (reverse_display _) _) : order_scope. -Notation "><^r%O" := (fun x y => ~~ (@comparable (reverse_display _) _ x y)) : - order_scope. - -Notation "<=^r y" := (>=^r%O y) : order_scope. -Notation "<=^r y :> T" := (<=^r (y : T)) : order_scope. -Notation ">=^r y" := (<=^r%O y) : order_scope. -Notation ">=^r y :> T" := (>=^r (y : T)) : order_scope. - -Notation "<^r y" := (>^r%O y) : order_scope. -Notation "<^r y :> T" := (<^r (y : T)) : order_scope. -Notation ">^r y" := (<^r%O y) : order_scope. -Notation ">^r y :> T" := (>^r (y : T)) : order_scope. - -Notation ">=<^r y" := (>=<^r%O y) : order_scope. -Notation ">=<^r y :> T" := (>=<^r (y : T)) : order_scope. - -Notation "x <=^r y" := (<=^r%O x y) : order_scope. -Notation "x <=^r y :> T" := ((x : T) <=^r (y : T)) : order_scope. -Notation "x >=^r y" := (y <=^r x) (only parsing) : order_scope. -Notation "x >=^r y :> T" := ((x : T) >=^r (y : T)) (only parsing) : order_scope. - -Notation "x <^r y" := (<^r%O x y) : order_scope. -Notation "x <^r y :> T" := ((x : T) <^r (y : T)) : order_scope. -Notation "x >^r y" := (y <^r x) (only parsing) : order_scope. -Notation "x >^r y :> T" := ((x : T) >^r (y : T)) (only parsing) : order_scope. - -Notation "x <=^r y <=^r z" := ((x <=^r y) && (y <=^r z)) : order_scope. -Notation "x <^r y <=^r z" := ((x <^r y) && (y <=^r z)) : order_scope. -Notation "x <=^r y <^r z" := ((x <=^r y) && (y <^r z)) : order_scope. -Notation "x <^r y <^r z" := ((x <^r y) && (y <^r z)) : order_scope. - -Notation "x <=^r y ?= 'iff' C" := ( R" := ((x : R) <=^r (y : R) ?= iff C) - (only parsing) : order_scope. - -Notation ">=<^r x" := (>=<^r%O x) : order_scope. -Notation ">=<^r x :> T" := (>=<^r (x : T)) (only parsing) : order_scope. -Notation "x >=<^r y" := (>=<^r%O x y) : order_scope. - -Notation "><^r x" := (fun y => ~~ (>=<^r%O x y)) : order_scope. -Notation "><^r x :> T" := (><^r (x : T)) (only parsing) : order_scope. -Notation "x ><^r y" := (~~ (><^r%O x y)) : order_scope. - -Notation "x `&^r` y" := (@meet (reverse_display _) _ x y). -Notation "x `|^r` y" := (@join (reverse_display _) _ x y). - -End ReverseSyntax. - -(**********) -(* THEORY *) -(**********) - -Module Import POrderTheory. -Section POrderTheory. - -Context {display : unit}. -Local Notation porderType := (porderType display). +Context {disp : unit}. +Local Notation porderType := (porderType disp). Context {T : porderType}. Implicit Types x y : T. +Lemma geE x y : ge x y = (y <= x). Proof. by []. Qed. +Lemma gtE x y : gt x y = (y < x). Proof. by []. Qed. + Lemma lexx (x : T) : x <= x. Proof. by case: T x => ? [? []]. Qed. -Hint Resolve lexx. +Hint Resolve lexx : core. Definition le_refl : reflexive le := lexx. -Hint Resolve le_refl. +Definition ge_refl : reflexive ge := lexx. +Hint Resolve le_refl : core. Lemma le_anti: antisymmetric (<=%O : rel T). Proof. by case: T => ? [? []]. Qed. +Lemma ge_anti: antisymmetric (>=%O : rel T). +Proof. by move=> x y /le_anti. Qed. + Lemma le_trans: transitive (<=%O : rel T). Proof. by case: T => ? [? []]. Qed. -Lemma lt_neqAle x y: (x < y) = (x != y) && (x <= y). +Lemma ge_trans: transitive (>=%O : rel T). +Proof. by move=> ? ? ? ? /le_trans; apply. Qed. + +Lemma lt_def x y: (x < y) = (y != x) && (x <= y). Proof. by case: T x y => ? [? []]. Qed. +Lemma lt_neqAle x y: (x < y) = (x != y) && (x <= y). +Proof. by rewrite lt_def eq_sym. Qed. + Lemma ltxx x: x < x = false. -Proof. by rewrite lt_neqAle eqxx. Qed. +Proof. by rewrite lt_def eqxx. Qed. Definition lt_irreflexive : irreflexive lt := ltxx. -Hint Resolve lt_irreflexive. +Hint Resolve lt_irreflexive : core. + +Definition ltexx := (lexx, ltxx). Lemma le_eqVlt x y: (x <= y) = (x == y) || (x < y). Proof. by rewrite lt_neqAle; case: eqP => //= ->; rewrite lexx. Qed. @@ -1700,6 +1649,9 @@ Proof. by rewrite le_eqVlt => /orP [/eqP ->|/lt_trans t /t]. Qed. Lemma lt_nsym x y : x < y -> y < x -> False. Proof. by move=> xy /(lt_trans xy); rewrite ltxx. Qed. +Lemma lt_asym x y : x < y < x = false. +Proof. by apply/negP => /andP []; apply: lt_nsym. Qed. + Lemma le_gtF x y: x <= y -> y < x = false. Proof. by move=> le_xy; apply/negP => /lt_le_trans /(_ le_xy); rewrite ltxx. @@ -1719,11 +1671,13 @@ by rewrite lt_neqAle lexy andbT; apply: contraNneq Nleyx => ->. Qed. Lemma lt_le_asym x y : x < y <= x = false. -Proof. by rewrite lt_neqAle -andbA -eq_le eq_sym; case: (_ == _). Qed. +Proof. by rewrite lt_neqAle -andbA -eq_le eq_sym andNb. Qed. Lemma le_lt_asym x y : x <= y < x = false. Proof. by rewrite andbC lt_le_asym. Qed. +Definition lte_anti := (=^~ eq_le, lt_asym, lt_le_asym, le_lt_asym). + Lemma lt_sorted_uniq_le (s : seq T) : sorted lt s = uniq s && sorted le s. Proof. @@ -1818,58 +1772,183 @@ rewrite /leif le_eqVlt; apply: (iffP idP)=> [|[]]. by move=> /orP[/eqP->|lxy] <-; rewrite ?eqxx // lt_eqF. Qed. +Lemma leif_refl x C : reflect (x <= x ?= iff C) C. +Proof. by apply: (iffP idP) => [-> | <-] //; split; rewrite ?eqxx. Qed. + +Lemma leif_trans x1 x2 x3 C12 C23 : + x1 <= x2 ?= iff C12 -> x2 <= x3 ?= iff C23 -> x1 <= x3 ?= iff C12 && C23. +Proof. +move=> ltx12 ltx23; apply/leifP; rewrite -ltx12. +case eqx12: (x1 == x2). + by rewrite (eqP eqx12) lt_neqAle !ltx23 andbT; case C23. +by rewrite (@lt_le_trans x2) ?ltx23 // lt_neqAle eqx12 ltx12. +Qed. + +Lemma leif_le x y : x <= y -> x <= y ?= iff (x >= y). +Proof. by move=> lexy; split=> //; rewrite eq_le lexy. Qed. + +Lemma leif_eq x y : x <= y -> x <= y ?= iff (x == y). +Proof. by []. Qed. + +Lemma ge_leif x y C : x <= y ?= iff C -> (y <= x) = C. +Proof. by case=> le_xy; rewrite eq_le le_xy. Qed. + +Lemma lt_leif x y C : x <= y ?= iff C -> (x < y) = ~~ C. +Proof. by move=> le_xy; rewrite lt_neqAle !le_xy andbT. Qed. + +Lemma mono_in_leif (A : pred T) (f : T -> T) C : + {in A &, {mono f : x y / x <= y}} -> + {in A &, forall x y, (f x <= f y ?= iff C) = (x <= y ?= iff C)}. +Proof. by move=> mf x y Ax Ay; rewrite /leif !eq_le !mf. Qed. + +Lemma mono_leif (f : T -> T) C : + {mono f : x y / x <= y} -> + forall x y, (f x <= f y ?= iff C) = (x <= y ?= iff C). +Proof. by move=> mf x y; rewrite /leif !eq_le !mf. Qed. + +Lemma nmono_in_leif (A : pred T) (f : T -> T) C : + {in A &, {mono f : x y /~ x <= y}} -> + {in A &, forall x y, (f x <= f y ?= iff C) = (y <= x ?= iff C)}. +Proof. by move=> mf x y Ax Ay; rewrite /leif !eq_le !mf. Qed. + +Lemma nmono_leif (f : T -> T) C : + {mono f : x y /~ x <= y} -> + forall x y, (f x <= f y ?= iff C) = (y <= x ?= iff C). +Proof. by move=> mf x y; rewrite /leif !eq_le !mf. Qed. + End POrderTheory. +Section POrderMonotonyTheory. + +Context {disp disp' : unit}. +Context {T : porderType disp} {T' : porderType disp'}. +Implicit Types (m n p : nat) (x y z : T) (u v w : T'). +Variables (D D' : pred T) (f : T -> T'). + +Hint Resolve lexx lt_neqAle (@le_anti _ T) (@le_anti _ T') lt_def : core. + +Let ge_antiT : antisymmetric (>=%O : rel T). +Proof. by move=> ? ? /le_anti. Qed. + +Lemma ltW_homo : {homo f : x y / x < y} -> {homo f : x y / x <= y}. +Proof. exact: homoW. Qed. + +Lemma ltW_nhomo : {homo f : x y /~ x < y} -> {homo f : x y /~ x <= y}. +Proof. exact: homoW. Qed. + +Lemma inj_homo_lt : + injective f -> {homo f : x y / x <= y} -> {homo f : x y / x < y}. +Proof. exact: inj_homo. Qed. + +Lemma inj_nhomo_lt : + injective f -> {homo f : x y /~ x <= y} -> {homo f : x y /~ x < y}. +Proof. exact: inj_homo. Qed. + +Lemma inc_inj : {mono f : x y / x <= y} -> injective f. +Proof. exact: mono_inj. Qed. + +Lemma dec_inj : {mono f : x y /~ x <= y} -> injective f. +Proof. exact: mono_inj. Qed. + +Lemma leW_mono : {mono f : x y / x <= y} -> {mono f : x y / x < y}. +Proof. exact: anti_mono. Qed. + +Lemma leW_nmono : {mono f : x y /~ x <= y} -> {mono f : x y /~ x < y}. +Proof. exact: anti_mono. Qed. + +(* Monotony in D D' *) +Lemma ltW_homo_in : + {in D & D', {homo f : x y / x < y}} -> {in D & D', {homo f : x y / x <= y}}. +Proof. exact: homoW_in. Qed. + +Lemma ltW_nhomo_in : + {in D & D', {homo f : x y /~ x < y}} -> {in D & D', {homo f : x y /~ x <= y}}. +Proof. exact: homoW_in. Qed. + +Lemma inj_homo_lt_in : + {in D & D', injective f} -> {in D & D', {homo f : x y / x <= y}} -> + {in D & D', {homo f : x y / x < y}}. +Proof. exact: inj_homo_in. Qed. + +Lemma inj_nhomo_lt_in : + {in D & D', injective f} -> {in D & D', {homo f : x y /~ x <= y}} -> + {in D & D', {homo f : x y /~ x < y}}. +Proof. exact: inj_homo_in. Qed. + +Lemma inc_inj_in : {in D &, {mono f : x y / x <= y}} -> + {in D &, injective f}. +Proof. exact: mono_inj_in. Qed. + +Lemma dec_inj_in : + {in D &, {mono f : x y /~ x <= y}} -> {in D &, injective f}. +Proof. exact: mono_inj_in. Qed. + +Lemma leW_mono_in : + {in D &, {mono f : x y / x <= y}} -> {in D &, {mono f : x y / x < y}}. +Proof. exact: anti_mono_in. Qed. + +Lemma leW_nmono_in : + {in D &, {mono f : x y /~ x <= y}} -> {in D &, {mono f : x y /~ x < y}}. +Proof. exact: anti_mono_in. Qed. + +End POrderMonotonyTheory. + End POrderTheory. -Hint Resolve lexx le_refl lt_irreflexive. +Hint Resolve lexx le_refl ltxx lt_irreflexive ltW lt_eqF : core. +Arguments leifP {disp T x y C}. +Arguments leif_refl {disp T x C}. +Arguments mono_in_leif [disp T A f C]. +Arguments nmono_in_leif [disp T A f C]. +Arguments mono_leif [disp T f C]. +Arguments nmono_leif [disp T f C]. -Module Import ReversePOrder. -Section ReversePOrder. -Canonical reverse_eqType (T : eqType) := EqType T [eqMixin of T^r]. -Canonical reverse_choiceType (T : choiceType) := [choiceType of T^r]. +Module Import ConversePOrder. +Section ConversePOrder. +Canonical converse_eqType (T : eqType) := EqType T [eqMixin of T^c]. +Canonical converse_choiceType (T : choiceType) := [choiceType of T^c]. -Context {display : unit}. -Local Notation porderType := (porderType display). +Context {disp : unit}. +Local Notation porderType := (porderType disp). Variable T : porderType. -Definition reverse_le (x y : T) := (y <= x). -Definition reverse_lt (x y : T) := (y < x). +Definition converse_le (x y : T) := (y <= x). +Definition converse_lt (x y : T) := (y < x). -Lemma reverse_lt_neqAle (x y : T) : reverse_lt x y = (x != y) && (reverse_le x y). -Proof. by rewrite eq_sym; apply: lt_neqAle. Qed. +Lemma converse_lt_def (x y : T) : + converse_lt x y = (y != x) && (converse_le x y). +Proof. by apply: lt_neqAle. Qed. -Fact reverse_le_anti : antisymmetric reverse_le. +Fact converse_le_anti : antisymmetric converse_le. Proof. by move=> x y /andP [xy yx]; apply/le_anti/andP; split. Qed. -Definition reverse_porderMixin := - POrderMixin reverse_lt_neqAle (lexx : reflexive reverse_le) reverse_le_anti +Definition converse_porderMixin := + POrderMixin converse_lt_def (lexx : reflexive converse_le) converse_le_anti (fun y z x zy yx => @le_trans _ _ y x z yx zy). -Canonical reverse_porderType := - POrderType (reverse_display display) (T^r) reverse_porderMixin. +Canonical converse_porderType := + POrderType (converse_display disp) (T^c) converse_porderMixin. -End ReversePOrder. -End ReversePOrder. +End ConversePOrder. +End ConversePOrder. -Definition LePOrderMixin T le rle ale tle := - @POrderMixin T le _ (fun _ _ => erefl) rle ale tle. - -Module Import ReverseLattice. -Section ReverseLattice. -Context {display : unit}. -Local Notation latticeType := (latticeType display). +Module Import ConverseLattice. +Section ConverseLattice. +Context {disp : unit}. +Local Notation latticeType := (latticeType disp). Variable L : latticeType. Implicit Types (x y : L). -Lemma meetC : commutative (@meet _ L). Proof. by case: L => [?[?[]]]. Qed. -Lemma joinC : commutative (@join _ L). Proof. by case: L => [?[?[]]]. Qed. +Lemma meetC : commutative (@meet _ L). Proof. by case: L => [?[? ?[]]]. Qed. +Lemma joinC : commutative (@join _ L). Proof. by case: L => [?[? ?[]]]. Qed. -Lemma meetA : associative (@meet _ L). Proof. by case: L => [?[?[]]]. Qed. -Lemma joinA : associative (@join _ L). Proof. by case: L => [?[?[]]]. Qed. +Lemma meetA : associative (@meet _ L). Proof. by case: L => [?[? ?[]]]. Qed. +Lemma joinA : associative (@join _ L). Proof. by case: L => [?[? ?[]]]. Qed. -Lemma joinKI y x : x `&` (x `|` y) = x. Proof. by case: L x y => [?[?[]]]. Qed. -Lemma meetKU y x : x `|` (x `&` y) = x. Proof. by case: L x y => [?[?[]]]. Qed. +Lemma joinKI y x : x `&` (x `|` y) = x. +Proof. by case: L x y => [?[? ?[]]]. Qed. +Lemma meetKU y x : x `|` (x `&` y) = x. +Proof. by case: L x y => [?[? ?[]]]. Qed. Lemma joinKIC y x : x `&` (y `|` x) = x. Proof. by rewrite joinC joinKI. Qed. Lemma meetKUC y x : x `|` (y `&` x) = x. Proof. by rewrite meetC meetKU. Qed. @@ -1883,13 +1962,13 @@ Lemma meetUKC x y : (y `&` x) `|` y = y. Proof. by rewrite meetC meetUK. Qed. Lemma joinIKC x y : (y `|` x) `&` y = y. Proof. by rewrite joinC joinIK. Qed. Lemma leEmeet x y : (x <= y) = (x `&` y == x). -Proof. by case: L x y => [?[?[]]]. Qed. +Proof. by case: L x y => [?[? ?[]]]. Qed. Lemma leEjoin x y : (x <= y) = (x `|` y == y). Proof. by rewrite leEmeet; apply/eqP/eqP => <-; rewrite (joinKI, meetUK). Qed. Lemma meetUl : left_distributive (@meet _ L) (@join _ L). -Proof. by case: L => [?[?[]]]. Qed. +Proof. by case: L => [?[? ?[]]]. Qed. Lemma meetUr : right_distributive (@meet _ L) (@join _ L). Proof. by move=> x y z; rewrite meetC meetUl ![_ `&` x]meetC. Qed. @@ -1897,20 +1976,20 @@ Proof. by move=> x y z; rewrite meetC meetUl ![_ `&` x]meetC. Qed. Lemma joinIl : left_distributive (@join _ L) (@meet _ L). Proof. by move=> x y z; rewrite meetUr joinIK meetUl -joinA meetUKC. Qed. -Fact reverse_leEmeet (x y : L^r) : (x <= y) = (x `|` y == x). +Fact converse_leEmeet (x y : L^c) : (x <= y) = (x `|` y == x). Proof. by rewrite [LHS]leEjoin joinC. Qed. -Definition reverse_latticeMixin := - @LatticeMixin _ [porderType of L^r] _ _ joinC meetC - joinA meetA meetKU joinKI reverse_leEmeet joinIl. -Canonical reverse_latticeType := LatticeType L^r reverse_latticeMixin. -End ReverseLattice. -End ReverseLattice. +Definition converse_latticeMixin := + @LatticeMixin _ [porderType of L^c] _ _ joinC meetC + joinA meetA meetKU joinKI converse_leEmeet joinIl. +Canonical converse_latticeType := LatticeType L^c converse_latticeMixin. +End ConverseLattice. +End ConverseLattice. Module Import LatticeTheoryMeet. Section LatticeTheoryMeet. -Context {display : unit}. -Local Notation latticeType := (latticeType display). +Context {disp : unit}. +Local Notation latticeType := (latticeType disp). Context {L : latticeType}. Implicit Types (x y : L). @@ -1936,16 +2015,6 @@ Proof. by rewrite meetAC meetC meetxx. Qed. (* interaction with order *) -Lemma meet_idPl {x y} : reflect (x `&` y = x) (x <= y). -Proof. by rewrite leEmeet; apply/eqP. Qed. -Lemma meet_idPr {x y} : reflect (y `&` x = x) (x <= y). -Proof. by rewrite meetC; apply/meet_idPl. Qed. - -Lemma leIidl x y : (x <= x `&` y) = (x <= y). -Proof. by rewrite !leEmeet meetKI. Qed. -Lemma leIidr x y : (x <= y `&` x) = (x <= y). -Proof. by rewrite !leEmeet meetKIC. Qed. - Lemma lexI x y z : (x <= y `&` z) = (x <= y) && (x <= z). Proof. rewrite !leEmeet; apply/idP/idP => [/eqP<-|/andP[/eqP<- /eqP<-]]. @@ -1953,192 +2022,295 @@ rewrite !leEmeet; apply/idP/idP => [/eqP<-|/andP[/eqP<- /eqP<-]]. by rewrite -[X in X `&` _]meetA meetIK meetA. Qed. -Lemma leIx x y z : (y <= x) || (z <= x) -> y `&` z <= x. -Proof. -rewrite !leEmeet => /orP [/eqP <-|/eqP <-]. - by rewrite -meetA meetACA meetxx meetAC. -by rewrite -meetA meetIK. -Qed. +Lemma leIxl x y z : y <= x -> y `&` z <= x. +Proof. by rewrite !leEmeet meetAC => /eqP ->. Qed. + +Lemma leIxr x y z : z <= x -> y `&` z <= x. +Proof. by rewrite !leEmeet -meetA => /eqP ->. Qed. + +Lemma leIx2 x y z : (y <= x) || (z <= x) -> y `&` z <= x. +Proof. by case/orP => [/leIxl|/leIxr]. Qed. Lemma leIr x y : y `&` x <= x. -Proof. by rewrite leIx ?lexx ?orbT. Qed. +Proof. by rewrite leIx2 ?lexx ?orbT. Qed. Lemma leIl x y : x `&` y <= x. -Proof. by rewrite leIx ?lexx ?orbT. Qed. +Proof. by rewrite leIx2 ?lexx ?orbT. Qed. + +Lemma meet_idPl {x y} : reflect (x `&` y = x) (x <= y). +Proof. by rewrite leEmeet; apply/eqP. Qed. +Lemma meet_idPr {x y} : reflect (y `&` x = x) (x <= y). +Proof. by rewrite meetC; apply/meet_idPl. Qed. + +Lemma leIidl x y : (x <= x `&` y) = (x <= y). +Proof. by rewrite !leEmeet meetKI. Qed. +Lemma leIidr x y : (x <= y `&` x) = (x <= y). +Proof. by rewrite !leEmeet meetKIC. Qed. + +Lemma eq_meetl x y : (x `&` y == x) = (x <= y). +Proof. by apply/esym/leEmeet. Qed. + +Lemma eq_meetr x y : (x `&` y == y) = (y <= x). +Proof. by rewrite meetC eq_meetl. Qed. Lemma leI2 x y z t : x <= z -> y <= t -> x `&` y <= z `&` t. -Proof. by move=> xz yt; rewrite lexI !leIx ?xz ?yt ?orbT //. Qed. +Proof. by move=> xz yt; rewrite lexI !leIx2 ?xz ?yt ?orbT //. Qed. End LatticeTheoryMeet. End LatticeTheoryMeet. Module Import LatticeTheoryJoin. Section LatticeTheoryJoin. -Context {display : unit}. -Local Notation latticeType := (latticeType display). +Import LatticeDef. +Context {disp : unit}. +Local Notation latticeType := (latticeType disp). Context {L : latticeType}. Implicit Types (x y : L). (* lattice theory *) Lemma joinAC : right_commutative (@join _ L). -Proof. exact: (@meetAC _ [latticeType of L^r]). Qed. +Proof. exact: (@meetAC _ [latticeType of L^c]). Qed. Lemma joinCA : left_commutative (@join _ L). -Proof. exact: (@meetCA _ [latticeType of L^r]). Qed. +Proof. exact: (@meetCA _ [latticeType of L^c]). Qed. Lemma joinACA : interchange (@join _ L) (@join _ L). -Proof. exact: (@meetACA _ [latticeType of L^r]). Qed. +Proof. exact: (@meetACA _ [latticeType of L^c]). Qed. Lemma joinxx x : x `|` x = x. -Proof. exact: (@meetxx _ [latticeType of L^r]). Qed. +Proof. exact: (@meetxx _ [latticeType of L^c]). Qed. Lemma joinKU y x : x `|` (x `|` y) = x `|` y. -Proof. exact: (@meetKI _ [latticeType of L^r]). Qed. +Proof. exact: (@meetKI _ [latticeType of L^c]). Qed. Lemma joinUK y x : (x `|` y) `|` y = x `|` y. -Proof. exact: (@meetIK _ [latticeType of L^r]). Qed. +Proof. exact: (@meetIK _ [latticeType of L^c]). Qed. Lemma joinKUC y x : x `|` (y `|` x) = x `|` y. -Proof. exact: (@meetKIC _ [latticeType of L^r]). Qed. +Proof. exact: (@meetKIC _ [latticeType of L^c]). Qed. Lemma joinUKC y x : y `|` x `|` y = x `|` y. -Proof. exact: (@meetIKC _ [latticeType of L^r]). Qed. +Proof. exact: (@meetIKC _ [latticeType of L^c]). Qed. (* interaction with order *) +Lemma leUx x y z : (x `|` y <= z) = (x <= z) && (y <= z). +Proof. exact: (@lexI _ [latticeType of L^c]). Qed. +Lemma lexUl x y z : x <= y -> x <= y `|` z. +Proof. exact: (@leIxl _ [latticeType of L^c]). Qed. +Lemma lexUr x y z : x <= z -> x <= y `|` z. +Proof. exact: (@leIxr _ [latticeType of L^c]). Qed. +Lemma lexU2 x y z : (x <= y) || (x <= z) -> x <= y `|` z. +Proof. exact: (@leIx2 _ [latticeType of L^c]). Qed. + +Lemma leUr x y : x <= y `|` x. +Proof. exact: (@leIr _ [latticeType of L^c]). Qed. +Lemma leUl x y : x <= x `|` y. +Proof. exact: (@leIl _ [latticeType of L^c]). Qed. + Lemma join_idPl {x y} : reflect (x `|` y = y) (x <= y). -Proof. exact: (@meet_idPr _ [latticeType of L^r]). Qed. +Proof. exact: (@meet_idPr _ [latticeType of L^c]). Qed. Lemma join_idPr {x y} : reflect (y `|` x = y) (x <= y). -Proof. exact: (@meet_idPl _ [latticeType of L^r]). Qed. +Proof. exact: (@meet_idPl _ [latticeType of L^c]). Qed. Lemma leUidl x y : (x `|` y <= y) = (x <= y). -Proof. exact: (@leIidr _ [latticeType of L^r]). Qed. +Proof. exact: (@leIidr _ [latticeType of L^c]). Qed. Lemma leUidr x y : (y `|` x <= y) = (x <= y). -Proof. exact: (@leIidl _ [latticeType of L^r]). Qed. - -Lemma leUx x y z : (x `|` y <= z) = (x <= z) && (y <= z). -Proof. exact: (@lexI _ [latticeType of L^r]). Qed. - -Lemma lexU x y z : (x <= y) || (x <= z) -> x <= y `|` z. -Proof. exact: (@leIx _ [latticeType of L^r]). Qed. +Proof. exact: (@leIidl _ [latticeType of L^c]). Qed. -Lemma leUr x y : x <= y `|` x. -Proof. exact: (@leIr _ [latticeType of L^r]). Qed. - -Lemma leUl x y : x <= x `|` y. -Proof. exact: (@leIl _ [latticeType of L^r]). Qed. +Lemma eq_joinl x y : (x `|` y == x) = (y <= x). +Proof. exact: (@eq_meetl _ [latticeType of L^c]). Qed. +Lemma eq_joinr x y : (x `|` y == y) = (x <= y). +Proof. exact: (@eq_meetr _ [latticeType of L^c]). Qed. Lemma leU2 x y z t : x <= z -> y <= t -> x `|` y <= z `|` t. -Proof. exact: (@leI2 _ [latticeType of L^r]). Qed. +Proof. exact: (@leI2 _ [latticeType of L^c]). Qed. (* Distributive lattice theory *) Lemma joinIr : right_distributive (@join _ L) (@meet _ L). -Proof. exact: (@meetUr _ [latticeType of L^r]). Qed. +Proof. exact: (@meetUr _ [latticeType of L^c]). Qed. + +Lemma lcomparableP x y : incomparer x y + (y == x) (x == y) (x <= y) (y <= x) (x < y) (x > y) + (y >=< x) (x >=< y) (y `&` x) (x `&` y) (y `|` x) (x `|` y). +Proof. +by case: (comparableP x) => [-> | hxy | hxy | hxy]; do 1?have hxy' := ltW hxy; + rewrite ?(meetxx, joinxx, meetC y, joinC y) + ?(meet_idPl hxy', meet_idPr hxy', join_idPl hxy', join_idPr hxy'); + constructor. +Qed. + +Lemma lcomparable_ltgtP x y : x >=< y -> + comparer x y (y == x) (x == y) (x <= y) (y <= x) (x < y) (x > y) + (y `&` x) (x `&` y) (y `|` x) (x `|` y). +Proof. by case: (lcomparableP x) => // *; constructor. Qed. + +Lemma lcomparable_leP x y : x >=< y -> + le_xor_gt x y (x <= y) (y < x) (y `&` x) (x `&` y) (y `|` x) (x `|` y). +Proof. by move/lcomparable_ltgtP => [->|/ltW xy|xy]; constructor => //. Qed. + +Lemma lcomparable_ltP x y : x >=< y -> + lt_xor_ge x y (y <= x) (x < y) (y `&` x) (x `&` y) (y `|` x) (x `|` y). +Proof. by move=> /lcomparable_ltgtP [->|xy|/ltW xy]; constructor => //. Qed. End LatticeTheoryJoin. End LatticeTheoryJoin. -Module TotalLattice. -Section TotalLattice. -Context {display : unit}. -Local Notation porderType := (porderType display). -Context {T : porderType}. -Implicit Types (x y z : T). -Hypothesis le_total : total (<=%O : rel T). +Module Import TotalTheory. +Section TotalTheory. +Context {disp : unit}. +Local Notation orderType := (orderType disp). +Context {T : orderType}. +Implicit Types (x y z t : T). + +Lemma le_total : total (<=%O : rel T). Proof. by case: T => [? [?]]. Qed. +Hint Resolve le_total : core. -Fact comparableT x y : x >=< y. Proof. exact: le_total. Qed. -Hint Resolve comparableT. +Lemma ge_total : total (>=%O : rel T). +Proof. by move=> ? ?; apply: le_total. Qed. +Hint Resolve ge_total : core. -Fact ltgtP x y : - comparer x y (y == x) (x == y) (x <= y) (y <= x) (x < y) (x > y). -Proof. exact: comparable_ltgtP. Qed. +Lemma comparableT x y : x >=< y. Proof. exact: le_total. Qed. +Hint Resolve comparableT : core. -Fact leP x y : le_xor_gt x y (x <= y) (y < x). -Proof. exact: comparable_leP. Qed. +Lemma sort_le_sorted (s : seq T) : sorted <=%O (sort <=%O s). +Proof. exact: sort_sorted. Qed. -Fact ltP x y : lt_xor_ge x y (y <= x) (x < y). -Proof. exact: comparable_ltP. Qed. +Lemma sort_lt_sorted (s : seq T) : sorted lt (sort le s) = uniq s. +Proof. by rewrite lt_sorted_uniq_le sort_uniq sort_le_sorted andbT. Qed. -Definition meet x y := if x <= y then x else y. -Definition join x y := if y <= x then x else y. +Lemma sort_le_id (s : seq T) : sorted le s -> sort le s = s. +Proof. +by move=> ss; apply: eq_sorted_le; rewrite ?sort_le_sorted // perm_sort. +Qed. -Fact meetC : commutative meet. -Proof. by move=> x y; rewrite /meet; have [] := ltgtP. Qed. +Lemma leNgt x y : (x <= y) = ~~ (y < x). Proof. exact: comparable_leNgt. Qed. -Fact joinC : commutative join. -Proof. by move=> x y; rewrite /join; have [] := ltgtP. Qed. +Lemma ltNge x y : (x < y) = ~~ (y <= x). Proof. exact: comparable_ltNge. Qed. -Fact meetA : associative meet. +Lemma wlog_le P : + (forall x y, P y x -> P x y) -> (forall x y, x <= y -> P x y) -> + forall x y, P x y. Proof. -move=> x y z; rewrite /meet; case: (leP y z) => yz; case: (leP x y) => xy //=. -- by rewrite (le_trans xy). -- by rewrite yz. -by rewrite !lt_geF // (lt_trans yz). +move=> sP hP x y; case hxy: (x <= y); last apply/sP; apply/hP => //. +by move/negbT: hxy; rewrite -ltNge; apply/ltW. Qed. -Fact joinA : associative join. +Lemma wlog_lt P : + (forall x, P x x) -> + (forall x y, (P y x -> P x y)) -> (forall x y, x < y -> P x y) -> + forall x y, P x y. Proof. -move=> x y z; rewrite /join; case: (leP z y) => yz; case: (leP y x) => xy //=. -- by rewrite (le_trans yz). -- by rewrite yz. -by rewrite !lt_geF // (lt_trans xy). +move=> rP sP hP x y; case hxy: (x < y); first by apply/hP. +case hxy': (x == y); first by move/eqP: hxy' => <-; apply: rP. +by apply/sP/hP; rewrite lt_def leNgt hxy hxy'. Qed. -Fact joinKI y x : meet x (join x y) = x. -Proof. by rewrite /meet /join; case: (leP y x) => yx; rewrite ?lexx ?ltW. Qed. +Definition ltgtP x y := LatticeTheoryJoin.lcomparable_ltgtP (comparableT x y). +Definition leP x y := LatticeTheoryJoin.lcomparable_leP (comparableT x y). +Definition ltP x y := LatticeTheoryJoin.lcomparable_ltP (comparableT x y). -Fact meetKU y x : join x (meet x y) = x. -Proof. by rewrite /meet /join; case: (leP x y) => yx; rewrite ?lexx ?ltW. Qed. +Lemma neq_lt x y : (x != y) = (x < y) || (y < x). Proof. by case: ltgtP. Qed. -Fact leEmeet x y : (x <= y) = (meet x y == x). -Proof. by rewrite /meet; case: leP => ?; rewrite ?eqxx ?lt_eqF. Qed. +Lemma lt_total x y : x != y -> (x < y) || (y < x). Proof. by case: ltgtP. Qed. -Fact meetUl : left_distributive meet join. +Lemma eq_leLR x y z t : + (x <= y -> z <= t) -> (y < x -> t < z) -> (x <= y) = (z <= t). +Proof. by move=> *; apply/idP/idP; rewrite // !leNgt; apply: contra. Qed. + +Lemma eq_leRL x y z t : + (x <= y -> z <= t) -> (y < x -> t < z) -> (z <= t) = (x <= y). +Proof. by move=> *; symmetry; apply: eq_leLR. Qed. + +Lemma eq_ltLR x y z t : + (x < y -> z < t) -> (y <= x -> t <= z) -> (x < y) = (z < t). +Proof. by move=> *; rewrite !ltNge; congr negb; apply: eq_leLR. Qed. + +Lemma eq_ltRL x y z t : + (x < y -> z < t) -> (y <= x -> t <= z) -> (z < t) = (x < y). +Proof. by move=> *; symmetry; apply: eq_ltLR. Qed. + +(* interaction with lattice operations *) + +Lemma leIx x y z : (meet y z <= x) = (y <= x) || (z <= x). Proof. -move=> x y z; rewrite /meet /join. -case: (leP y z) => yz; case: (leP y x) => xy //=; first 1 last. -- by rewrite yz [x <= z](le_trans _ yz) ?[x <= y]ltW // lt_geF. -- by rewrite lt_geF ?lexx // (lt_le_trans yz). -- by rewrite lt_geF //; have [->|/lt_geF->|] := (ltgtP x z); rewrite ?lexx. -- by have [] := (leP x z); rewrite ?xy ?yz. +by case: (leP y z) => hyz; case: leP => ?; + rewrite ?(orbT, orbF) //=; apply/esym/negbTE; + rewrite -ltNge ?(lt_le_trans _ hyz) ?(lt_trans _ hyz). Qed. -Definition Mixin := LatticeMixin meetC joinC meetA joinA joinKI meetKU leEmeet meetUl. +Lemma lexU x y z : (x <= join y z) = (x <= y) || (x <= z). +Proof. +by case: (leP y z) => hyz; case: leP => ?; + rewrite ?(orbT, orbF) //=; apply/esym/negbTE; + rewrite -ltNge ?(le_lt_trans hyz) ?(lt_trans hyz). +Qed. -End TotalLattice. -End TotalLattice. +Lemma ltxI x y z : (x < meet y z) = (x < y) && (x < z). +Proof. by rewrite !ltNge leIx negb_or. Qed. -Module TotalTheory. -Section TotalTheory. -Context {display : unit}. -Local Notation orderType := (orderType display). -Context {T : orderType}. -Implicit Types (x y : T). +Lemma ltIx x y z : (meet y z < x) = (y < x) || (z < x). +Proof. by rewrite !ltNge lexI negb_and. Qed. -Lemma le_total : total (<=%O : rel T). Proof. by case: T => [? [?]]. Qed. -Hint Resolve le_total. +Lemma ltxU x y z : (x < join y z) = (x < y) || (x < z). +Proof. by rewrite !ltNge leUx negb_and. Qed. -Lemma comparableT x y : x >=< y. Proof. exact: le_total. Qed. -Hint Resolve comparableT. +Lemma ltUx x y z : (join y z < x) = (y < x) && (z < x). +Proof. by rewrite !ltNge lexU negb_or. Qed. -Lemma sort_le_sorted (s : seq T) : sorted <=%O (sort <=%O s). -Proof. exact: sort_sorted. Qed. +Definition ltexI := (@lexI _ T, ltxI). +Definition lteIx := (leIx, ltIx). +Definition ltexU := (lexU, ltxU). +Definition lteUx := (@leUx _ T, ltUx). -Lemma sort_lt_sorted (s : seq T) : sorted lt (sort le s) = uniq s. -Proof. by rewrite lt_sorted_uniq_le sort_uniq sort_le_sorted andbT. Qed. +Section ArgExtremum. -Lemma sort_le_id (s : seq T) : sorted le s -> sort le s = s. +Context (I : finType) (i0 : I) (P : pred I) (F : I -> T) (Pi0 : P i0). + +Lemma arg_minP: extremum_spec <=%O P F (arg_min i0 P F). +Proof. by apply: extremumP => //; apply: le_trans. Qed. + +Lemma arg_maxP: extremum_spec >=%O P F (arg_max i0 P F). +Proof. by apply: extremumP => //; [apply: ge_refl | apply: ge_trans]. Qed. + +End ArgExtremum. + +End TotalTheory. +Section TotalMonotonyTheory. + +Context {disp : unit} {disp' : unit}. +Context {T : orderType disp} {T' : porderType disp'}. +Variables (D : pred T) (f : T -> T'). +Implicit Types (x y z : T) (u v w : T'). + +Lemma le_mono : {homo f : x y / x < y} -> {mono f : x y / x <= y}. Proof. -by move=> ss; apply: eq_sorted_le; rewrite ?sort_le_sorted // perm_sort. +move=> mf x y; case: ltgtP; first (by move=> ->; apply/lexx); move/mf => fxy. +- by rewrite comparable_leNgt /comparable 1?(le_eqVlt (f y)) fxy ?orbT. +- by apply/ltW. Qed. -Lemma leNgt x y : (x <= y) = ~~ (y < x). -Proof. by rewrite comparable_leNgt. Qed. +Lemma le_nmono : {homo f : x y /~ x < y} -> {mono f : x y /~ x <= y}. +Proof. +move=> mf x y; case: ltgtP; first (by move=> ->; apply/lexx); move/mf => fxy. +- by rewrite comparable_leNgt /comparable 1?(le_eqVlt (f y)) fxy ?orbT. +- by apply/ltW. +Qed. -Lemma ltNge x y : (x < y) = ~~ (y <= x). -Proof. by rewrite comparable_ltNge. Qed. +Lemma le_mono_in : + {in D &, {homo f : x y / x < y}} -> {in D &, {mono f : x y / x <= y}}. +Proof. +move=> mf x y Dx Dy; case: ltgtP; + first (by move=> ->; apply/lexx); move/mf => fxy. +- by rewrite comparable_leNgt /comparable 1?(le_eqVlt (f y)) fxy ?orbT. +- by apply/ltW/fxy. +Qed. -Definition ltgtP := TotalLattice.ltgtP le_total. -Definition leP := TotalLattice.leP le_total. -Definition ltP := TotalLattice.ltP le_total. +Lemma le_nmono_in : + {in D &, {homo f : x y /~ x < y}} -> {in D &, {mono f : x y /~ x <= y}}. +Proof. +move=> mf x y Dx Dy; case: ltgtP; + first (by move=> ->; apply/lexx); move/mf => fxy. +- by rewrite comparable_leNgt /comparable 1?(le_eqVlt (f y)) fxy ?orbT. +- by apply/ltW/fxy. +Qed. +End TotalMonotonyTheory. End TotalTheory. -End TotalTheory. - Module Import BLatticeTheory. Section BLatticeTheory. @@ -2149,8 +2321,8 @@ Implicit Types (x y z : L). Local Notation "0" := bottom. (* Distributive lattice theory with 0 & 1*) -Lemma le0x x : 0 <= x. Proof. by case: L x => [?[?[]]]. Qed. -Hint Resolve le0x. +Lemma le0x x : 0 <= x. Proof. by case: L x => [?[? ?[]]]. Qed. +Hint Resolve le0x : core. Lemma lex0 x : (x <= 0) = (x == 0). Proof. by rewrite le_eqVlt (le_gtF (le0x _)) orbF. Qed. @@ -2183,7 +2355,7 @@ Proof. by rewrite joinC [_ `|` z]joinC => /leU2l_le H /H. Qed. Lemma lexUl z x y : x `&` z = 0 -> (x <= y `|` z) = (x <= y). Proof. -move=> xz0; apply/idP/idP=> xy; last by rewrite lexU ?xy. +move=> xz0; apply/idP/idP=> xy; last by rewrite lexU2 ?xy. by apply: (@leU2l_le x z); rewrite ?joinxx. Qed. @@ -2193,7 +2365,7 @@ Proof. by move=> xz0; rewrite joinC; rewrite lexUl. Qed. Lemma leU2E x y z t : x `&` t = 0 -> y `&` z = 0 -> (x `|` y <= z `|` t) = (x <= z) && (y <= t). Proof. -move=> dxt dyz; apply/idP/andP; last by case=> ??; exact: leU2. +move=> dxt dyz; apply/idP/andP; last by case=> ? ?; exact: leU2. by move=> lexyzt; rewrite (leU2l_le _ lexyzt) // (leU2r_le _ lexyzt). Qed. @@ -2203,7 +2375,7 @@ apply/idP/idP; last by move=> /andP [/eqP-> /eqP->]; rewrite joinx0. by move=> /eqP xUy0; rewrite -!lex0 -!xUy0 ?leUl ?leUr. Qed. -CoInductive eq0_xor_gt0 x : bool -> bool -> Set := +Variant eq0_xor_gt0 x : bool -> bool -> Set := Eq0NotPOs : x = 0 -> eq0_xor_gt0 x true false | POsNotEq0 : 0 < x -> eq0_xor_gt0 x false true. @@ -2215,7 +2387,7 @@ Canonical join_comoid := Monoid.ComLaw (@joinC _ _). Lemma join_sup (I : finType) (j : I) (P : pred I) (F : I -> L) : P j -> F j <= \join_(i | P i) F i. -Proof. by move=> Pj; rewrite (bigD1 j) //= lexU ?lexx. Qed. +Proof. by move=> Pj; rewrite (bigD1 j) //= lexU2 ?lexx. Qed. Lemma join_min (I : finType) (j : I) (l : L) (P : pred I) (F : I -> L) : P j -> l <= F j -> l <= \join_(i | P i) F i. @@ -2238,7 +2410,7 @@ move=> AsubB; rewrite -(setID B A). rewrite [X in _ <= X](eq_bigl [predU B :&: A & B :\: A]); last first. by move=> i; rewrite !inE. rewrite bigU //=; last by rewrite -setI_eq0 setDE setIACA setICr setI0. -by rewrite lexU // (setIidPr _) // lexx. +by rewrite lexU2 // (setIidPr _) // lexx. Qed. Lemma joins_setU (I : finType) (A B : {set I}) (F : I -> L) : @@ -2246,7 +2418,7 @@ Lemma joins_setU (I : finType) (A B : {set I}) (F : I -> L) : Proof. apply/eqP; rewrite eq_le leUx !le_joins ?subsetUl ?subsetUr ?andbT //. apply/joinsP => i; rewrite inE; move=> /orP. -by case=> ?; rewrite lexU //; [rewrite join_sup|rewrite orbC join_sup]. +by case=> ?; rewrite lexU2 //; [rewrite join_sup|rewrite orbC join_sup]. Qed. Lemma join_seq (I : finType) (r : seq I) (F : I -> L) : @@ -2256,7 +2428,7 @@ rewrite [RHS](eq_bigl (mem [set i | i \in r])); last by move=> i; rewrite !inE. elim: r => [|i r ihr]; first by rewrite big_nil big1 // => i; rewrite ?inE. rewrite big_cons {}ihr; apply/eqP; rewrite eq_le set_cons. rewrite leUx join_sup ?inE ?eqxx // le_joins //= ?subsetUr //. -apply/joinsP => j; rewrite !inE => /predU1P [->|jr]; rewrite ?lexU ?lexx //. +apply/joinsP => j; rewrite !inE => /predU1P [->|jr]; rewrite ?lexU2 ?lexx //. by rewrite join_sup ?orbT ?inE. Qed. @@ -2274,84 +2446,84 @@ Qed. End BLatticeTheory. End BLatticeTheory. -Module Import ReverseTBLattice. -Section ReverseTBLattice. +Module Import ConverseTBLattice. +Section ConverseTBLattice. Context {disp : unit}. Local Notation tblatticeType := (tblatticeType disp). Context {L : tblatticeType}. -Lemma lex1 (x : L) : x <= top. Proof. by case: L x => [?[?[]]]. Qed. +Lemma lex1 (x : L) : x <= top. Proof. by case: L x => [?[? ?[]]]. Qed. -Definition reverse_blatticeMixin := - @BLatticeMixin _ [latticeType of L^r] top lex1. -Canonical reverse_blatticeType := BLatticeType L^r reverse_blatticeMixin. +Definition converse_blatticeMixin := + @BLatticeMixin _ [latticeType of L^c] top lex1. +Canonical converse_blatticeType := BLatticeType L^c converse_blatticeMixin. -Definition reverse_tblatticeMixin := - @TBLatticeMixin _ [latticeType of L^r] (bottom : L) (@le0x _ L). -Canonical reverse_tblatticeType := TBLatticeType L^r reverse_tblatticeMixin. +Definition converse_tblatticeMixin := + @TBLatticeMixin _ [latticeType of L^c] (bottom : L) (@le0x _ L). +Canonical converse_tblatticeType := TBLatticeType L^c converse_tblatticeMixin. -End ReverseTBLattice. -End ReverseTBLattice. +End ConverseTBLattice. +End ConverseTBLattice. -Module Import ReverseTBLatticeSyntax. -Section ReverseTBLatticeSyntax. +Module Import ConverseTBLatticeSyntax. +Section ConverseTBLatticeSyntax. Local Notation "0" := bottom. Local Notation "1" := top. -Local Notation join := (@join (reverse_display _) _). -Local Notation meet := (@meet (reverse_display _) _). +Local Notation join := (@join (converse_display _) _). +Local Notation meet := (@meet (converse_display _) _). -Notation "\join^r_ ( i <- r | P ) F" := +Notation "\join^c_ ( i <- r | P ) F" := (\big[join/0]_(i <- r | P%B) F%O) : order_scope. -Notation "\join^r_ ( i <- r ) F" := +Notation "\join^c_ ( i <- r ) F" := (\big[join/0]_(i <- r) F%O) : order_scope. -Notation "\join^r_ ( i | P ) F" := +Notation "\join^c_ ( i | P ) F" := (\big[join/0]_(i | P%B) F%O) : order_scope. -Notation "\join^r_ i F" := +Notation "\join^c_ i F" := (\big[join/0]_i F%O) : order_scope. -Notation "\join^r_ ( i : I | P ) F" := +Notation "\join^c_ ( i : I | P ) F" := (\big[join/0]_(i : I | P%B) F%O) (only parsing) : order_scope. -Notation "\join^r_ ( i : I ) F" := +Notation "\join^c_ ( i : I ) F" := (\big[join/0]_(i : I) F%O) (only parsing) : order_scope. -Notation "\join^r_ ( m <= i < n | P ) F" := +Notation "\join^c_ ( m <= i < n | P ) F" := (\big[join/0]_(m <= i < n | P%B) F%O) : order_scope. -Notation "\join^r_ ( m <= i < n ) F" := +Notation "\join^c_ ( m <= i < n ) F" := (\big[join/0]_(m <= i < n) F%O) : order_scope. -Notation "\join^r_ ( i < n | P ) F" := +Notation "\join^c_ ( i < n | P ) F" := (\big[join/0]_(i < n | P%B) F%O) : order_scope. -Notation "\join^r_ ( i < n ) F" := +Notation "\join^c_ ( i < n ) F" := (\big[join/0]_(i < n) F%O) : order_scope. -Notation "\join^r_ ( i 'in' A | P ) F" := +Notation "\join^c_ ( i 'in' A | P ) F" := (\big[join/0]_(i in A | P%B) F%O) : order_scope. -Notation "\join^r_ ( i 'in' A ) F" := +Notation "\join^c_ ( i 'in' A ) F" := (\big[join/0]_(i in A) F%O) : order_scope. -Notation "\meet^r_ ( i <- r | P ) F" := +Notation "\meet^c_ ( i <- r | P ) F" := (\big[meet/1]_(i <- r | P%B) F%O) : order_scope. -Notation "\meet^r_ ( i <- r ) F" := +Notation "\meet^c_ ( i <- r ) F" := (\big[meet/1]_(i <- r) F%O) : order_scope. -Notation "\meet^r_ ( i | P ) F" := +Notation "\meet^c_ ( i | P ) F" := (\big[meet/1]_(i | P%B) F%O) : order_scope. -Notation "\meet^r_ i F" := +Notation "\meet^c_ i F" := (\big[meet/1]_i F%O) : order_scope. -Notation "\meet^r_ ( i : I | P ) F" := +Notation "\meet^c_ ( i : I | P ) F" := (\big[meet/1]_(i : I | P%B) F%O) (only parsing) : order_scope. -Notation "\meet^r_ ( i : I ) F" := +Notation "\meet^c_ ( i : I ) F" := (\big[meet/1]_(i : I) F%O) (only parsing) : order_scope. -Notation "\meet^r_ ( m <= i < n | P ) F" := +Notation "\meet^c_ ( m <= i < n | P ) F" := (\big[meet/1]_(m <= i < n | P%B) F%O) : order_scope. -Notation "\meet^r_ ( m <= i < n ) F" := +Notation "\meet^c_ ( m <= i < n ) F" := (\big[meet/1]_(m <= i < n) F%O) : order_scope. -Notation "\meet^r_ ( i < n | P ) F" := +Notation "\meet^c_ ( i < n | P ) F" := (\big[meet/1]_(i < n | P%B) F%O) : order_scope. -Notation "\meet^r_ ( i < n ) F" := +Notation "\meet^c_ ( i < n ) F" := (\big[meet/1]_(i < n) F%O) : order_scope. -Notation "\meet^r_ ( i 'in' A | P ) F" := +Notation "\meet^c_ ( i 'in' A | P ) F" := (\big[meet/1]_(i in A | P%B) F%O) : order_scope. -Notation "\meet^r_ ( i 'in' A ) F" := +Notation "\meet^c_ ( i 'in' A ) F" := (\big[meet/1]_(i in A) F%O) : order_scope. -End ReverseTBLatticeSyntax. -End ReverseTBLatticeSyntax. +End ConverseTBLatticeSyntax. +End ConverseTBLatticeSyntax. Module Import TBLatticeTheory. Section TBLatticeTheory. @@ -2362,43 +2534,43 @@ Implicit Types (x y : L). Local Notation "1" := top. -Hint Resolve le0x lex1. +Hint Resolve le0x lex1 : core. Lemma meetx1 : right_id 1 (@meet _ L). -Proof. exact: (@joinx0 _ [tblatticeType of L^r]). Qed. +Proof. exact: (@joinx0 _ [tblatticeType of L^c]). Qed. Lemma meet1x : left_id 1 (@meet _ L). -Proof. exact: (@join0x _ [tblatticeType of L^r]). Qed. +Proof. exact: (@join0x _ [tblatticeType of L^c]). Qed. Lemma joinx1 : right_zero 1 (@join _ L). -Proof. exact: (@meetx0 _ [tblatticeType of L^r]). Qed. +Proof. exact: (@meetx0 _ [tblatticeType of L^c]). Qed. Lemma join1x : left_zero 1 (@join _ L). -Proof. exact: (@meet0x _ [tblatticeType of L^r]). Qed. +Proof. exact: (@meet0x _ [tblatticeType of L^c]). Qed. Lemma le1x x : (1 <= x) = (x == 1). -Proof. exact: (@lex0 _ [tblatticeType of L^r]). Qed. +Proof. exact: (@lex0 _ [tblatticeType of L^c]). Qed. Lemma leI2l_le y t x z : y `|` z = 1 -> x `&` y <= z `&` t -> x <= z. -Proof. rewrite joinC; exact: (@leU2l_le _ [tblatticeType of L^r]). Qed. +Proof. rewrite joinC; exact: (@leU2l_le _ [tblatticeType of L^c]). Qed. Lemma leI2r_le y t x z : y `|` z = 1 -> y `&` x <= t `&` z -> x <= z. -Proof. rewrite joinC; exact: (@leU2r_le _ [tblatticeType of L^r]). Qed. +Proof. rewrite joinC; exact: (@leU2r_le _ [tblatticeType of L^c]). Qed. Lemma lexIl z x y : z `|` y = 1 -> (x `&` z <= y) = (x <= y). -Proof. rewrite joinC; exact: (@lexUl _ [tblatticeType of L^r]). Qed. +Proof. rewrite joinC; exact: (@lexUl _ [tblatticeType of L^c]). Qed. Lemma lexIr z x y : z `|` y = 1 -> (z `&` x <= y) = (x <= y). -Proof. rewrite joinC; exact: (@lexUr _ [tblatticeType of L^r]). Qed. +Proof. rewrite joinC; exact: (@lexUr _ [tblatticeType of L^c]). Qed. Lemma leI2E x y z t : x `|` t = 1 -> y `|` z = 1 -> (x `&` y <= z `&` t) = (x <= z) && (y <= t). Proof. -by move=> ? ?; apply: (@leU2E _ [tblatticeType of L^r]); rewrite meetC. +by move=> ? ?; apply: (@leU2E _ [tblatticeType of L^c]); rewrite meetC. Qed. Lemma meet_eq1 x y : (x `&` y == 1) = (x == 1) && (y == 1). -Proof. exact: (@join_eq0 _ [tblatticeType of L^r]). Qed. +Proof. exact: (@join_eq0 _ [tblatticeType of L^c]). Qed. Canonical meet_monoid := Monoid.Law (@meetA _ _) meet1x meetx1. Canonical meet_comoid := Monoid.ComLaw (@meetC _ _). @@ -2410,31 +2582,31 @@ Canonical meet_addoid := Monoid.AddLaw (@joinIl _ L) (@joinIr _ _). Lemma meets_inf (I : finType) (j : I) (P : pred I) (F : I -> L) : P j -> \meet_(i | P i) F i <= F j. -Proof. exact: (@join_sup _ [tblatticeType of L^r]). Qed. +Proof. exact: (@join_sup _ [tblatticeType of L^c]). Qed. Lemma meets_max (I : finType) (j : I) (u : L) (P : pred I) (F : I -> L) : P j -> F j <= u -> \meet_(i | P i) F i <= u. -Proof. exact: (@join_min _ [tblatticeType of L^r]). Qed. +Proof. exact: (@join_min _ [tblatticeType of L^c]). Qed. Lemma meetsP (I : finType) (l : L) (P : pred I) (F : I -> L) : reflect (forall i : I, P i -> l <= F i) (l <= \meet_(i | P i) F i). -Proof. exact: (@joinsP _ [tblatticeType of L^r]). Qed. +Proof. exact: (@joinsP _ [tblatticeType of L^c]). Qed. Lemma le_meets (I : finType) (A B : {set I}) (F : I -> L) : A \subset B -> \meet_(i in B) F i <= \meet_(i in A) F i. -Proof. exact: (@le_joins _ [tblatticeType of L^r]). Qed. +Proof. exact: (@le_joins _ [tblatticeType of L^c]). Qed. Lemma meets_setU (I : finType) (A B : {set I}) (F : I -> L) : \meet_(i in (A :|: B)) F i = \meet_(i in A) F i `&` \meet_(i in B) F i. -Proof. exact: (@joins_setU _ [tblatticeType of L^r]). Qed. +Proof. exact: (@joins_setU _ [tblatticeType of L^c]). Qed. Lemma meet_seq (I : finType) (r : seq I) (F : I -> L) : \meet_(i <- r) F i = \meet_(i in r) F i. -Proof. exact: (@join_seq _ [tblatticeType of L^r]). Qed. +Proof. exact: (@join_seq _ [tblatticeType of L^c]). Qed. Lemma meets_total (I : finType) (d : L) (P : pred I) (F : I -> L) : (forall i : I, P i -> d `|` F i = 1) -> d `|` \meet_(i | P i) F i = 1. -Proof. exact: (@joins_disjoint _ [tblatticeType of L^r]). Qed. +Proof. exact: (@joins_disjoint _ [tblatticeType of L^c]). Qed. End TBLatticeTheory. End TBLatticeTheory. @@ -2448,7 +2620,7 @@ Implicit Types (x y z : L). Local Notation "0" := bottom. Lemma subKI x y : y `&` (x `\` y) = 0. -Proof. by case: L x y => ? [? []]. Qed. +Proof. by case: L x y => ? [? ?[]]. Qed. Lemma subIK x y : (x `\` y) `&` y = 0. Proof. by rewrite meetC subKI. Qed. @@ -2460,7 +2632,7 @@ Lemma meetBI z x y : (x `\` y) `&` (z `&` y) = 0. Proof. by rewrite meetC meetIB. Qed. Lemma joinIB y x : (x `&` y) `|` (x `\` y) = x. -Proof. by case: L x y => ? [? []]. Qed. +Proof. by case: L x y => ? [? ?[]]. Qed. Lemma joinBI y x : (x `\` y) `|` (x `&` y) = x. Proof. by rewrite joinC joinIB. Qed. @@ -2472,8 +2644,8 @@ Lemma joinBIC y x : (x `\` y) `|` (y `&` x) = x. Proof. by rewrite meetC joinBI. Qed. Lemma leBx x y : x `\` y <= x. -Proof. by rewrite -{2}[x](joinIB y) lexU // lexx orbT. Qed. -Hint Resolve leBx. +Proof. by rewrite -{2}[x](joinIB y) lexU2 // lexx orbT. Qed. +Hint Resolve leBx : core. Lemma subxx x : x `\` x = 0. Proof. by have := subKI x x; rewrite (meet_idPr _). Qed. @@ -2522,7 +2694,7 @@ Proof. by rewrite ![_ `|` x]joinC ![_ `&` x]meetC joinxB. Qed. Lemma leBr z x y : x <= y -> z `\` y <= z `\` x. Proof. -by move=> lexy; rewrite leBLR joinxB (meet_idPr _) ?leBUK ?leUr ?lexU ?lexy. +by move=> lexy; rewrite leBLR joinxB (meet_idPr _) ?leBUK ?leUr ?lexU2 ?lexy. Qed. Lemma leB2 x y z t : x <= z -> t <= y -> x `\` y <= z `\` t. @@ -2546,7 +2718,7 @@ Proof. by rewrite eq_le leBLR leBRL andbCA andbA. Qed. Lemma subxU x y z : z `\` (x `|` y) = (z `\` x) `&` (z `\` y). Proof. apply/eqP; rewrite eq_le lexI !leBr ?leUl ?leUr //=. -rewrite leBRL leIx ?leBx //= meetUr meetAC subIK -meetA subIK. +rewrite leBRL leIx2 ?leBx //= meetUr meetAC subIK -meetA subIK. by rewrite meet0x meetx0 joinx0. Qed. @@ -2628,7 +2800,7 @@ Local Notation "0" := bottom. Local Notation "1" := top. Lemma complE x : ~` x = 1 `\` x. -Proof. by case: L x => [? [? ? []]]. Qed. +Proof. by case: L x => [?[? ? ? ?[]]]. Qed. Lemma sub1x x : 1 `\` x = ~` x. Proof. by rewrite complE. Qed. @@ -2699,96 +2871,742 @@ Proof. by elim/big_rec2: _=> [|i x y ? <-]; rewrite ?compl1 ?complI. Qed. End CTBLatticeTheory. End CTBLatticeTheory. +(*************) +(* FACTORIES *) +(*************) + +Module TotalLatticeMixin. +Section TotalLatticeMixin. +Import POrderDef. +Variable (disp : unit) (T : porderType disp). +Definition of_ := total (<=%O : rel T). +Variable (m : of_). +Implicit Types (x y z : T). + +Let comparableT x y : x >=< y := m x y. + +Fact ltgtP x y : + comparer x y (y == x) (x == y) (x <= y) (y <= x) (x < y) (x > y). +Proof. exact: comparable_ltgtP. Qed. + +Fact leP x y : le_xor_gt x y (x <= y) (y < x). +Proof. exact: comparable_leP. Qed. + +Fact ltP x y : lt_xor_ge x y (y <= x) (x < y). +Proof. exact: comparable_ltP. Qed. + +Definition meet x y := if x <= y then x else y. +Definition join x y := if y <= x then x else y. + +Fact meetC : commutative meet. +Proof. by move=> x y; rewrite /meet; have [] := ltgtP. Qed. + +Fact joinC : commutative join. +Proof. by move=> x y; rewrite /join; have [] := ltgtP. Qed. + +Fact meetA : associative meet. +Proof. +move=> x y z; rewrite /meet; case: (leP y z) => yz; case: (leP x y) => xy //=. +- by rewrite (le_trans xy). +- by rewrite yz. +by rewrite !lt_geF // (lt_trans yz). +Qed. + +Fact joinA : associative join. +Proof. +move=> x y z; rewrite /join; case: (leP z y) => yz; case: (leP y x) => xy //=. +- by rewrite (le_trans yz). +- by rewrite yz. +by rewrite !lt_geF // (lt_trans xy). +Qed. + +Fact joinKI y x : meet x (join x y) = x. +Proof. by rewrite /meet /join; case: (leP y x) => yx; rewrite ?lexx ?ltW. Qed. + +Fact meetKU y x : join x (meet x y) = x. +Proof. by rewrite /meet /join; case: (leP x y) => yx; rewrite ?lexx ?ltW. Qed. + +Fact leEmeet x y : (x <= y) = (meet x y == x). +Proof. by rewrite /meet; case: leP => ?; rewrite ?eqxx ?lt_eqF. Qed. + +Fact meetUl : left_distributive meet join. +Proof. +move=> x y z; rewrite /meet /join. +case: (leP y z) => yz; case: (leP y x) => xy //=; first 1 last. +- by rewrite yz [x <= z](le_trans _ yz) ?[x <= y]ltW // lt_geF. +- by rewrite lt_geF ?lexx // (lt_le_trans yz). +- by rewrite lt_geF //; have [->|/lt_geF->|] := (ltgtP x z); rewrite ?lexx. +- by have [] := (leP x z); rewrite ?xy ?yz. +Qed. + +Definition latticeMixin := + LatticeMixin meetC joinC meetA joinA joinKI meetKU leEmeet meetUl. + +End TotalLatticeMixin. + +Module Exports. +Notation totalLatticeMixin := of_. +Coercion latticeMixin : totalLatticeMixin >-> Order.Lattice.mixin_of. +End Exports. + +End TotalLatticeMixin. +Import TotalLatticeMixin.Exports. + +Module LePOrderMixin. +Section LePOrderMixin. +Variable (T : eqType). + +Record of_ := Build { + le : rel T; + lt : rel T; + le_refl : reflexive le; + le_anti : antisymmetric le; + le_trans : transitive le; + lt_def : forall x y, lt x y = (y != x) && le x y; +}. + +Definition porderMixin (m : of_) : porderMixin T := + POrderMixin (@lt_def m) (@le_refl m) (@le_anti m) (@le_trans m). + +End LePOrderMixin. + +Module Exports. +Notation lePOrderMixin := of_. +Notation LePOrderMixin := Build. +Coercion porderMixin : lePOrderMixin >-> POrder.mixin_of. +End Exports. + +End LePOrderMixin. +Import LePOrderMixin.Exports. + +Module LtPOrderMixin. +Section LtPOrderMixin. +Variable (T : eqType). + +Record of_ := Build { + le : rel T; + lt : rel T; + lt_irr : irreflexive lt; + lt_trans : transitive lt; + le_def : forall x y, le x y = (x == y) || lt x y; +}. + +Variable (m : of_). + +Fact lt_asym x y : (lt m x y && lt m y x) = false. +Proof. +by apply/negP => /andP [] xy /(lt_trans xy); apply/negP; rewrite (lt_irr m x). +Qed. + +Fact lt_def x y : lt m x y = (y != x) && le m x y. +Proof. by rewrite le_def eq_sym; case: eqP => //= <-; rewrite lt_irr. Qed. + +Fact le_refl : reflexive (le m). +Proof. by move=> ?; rewrite le_def eqxx. Qed. + +Fact le_anti : antisymmetric (le m). +Proof. +by move=> ? ?; rewrite !le_def eq_sym -orb_andr lt_asym orbF => /eqP. +Qed. + +Fact le_trans : transitive (le m). +Proof. +by move=> y x z; rewrite !le_def => /predU1P [-> //|ltxy] /predU1P [<-|ltyz]; + rewrite ?ltxy ?(lt_trans ltxy ltyz) // ?orbT. +Qed. + +Definition porderMixin : porderMixin T := + @POrderMixin _ (le m) (lt m) lt_def le_refl le_anti le_trans. + +End LtPOrderMixin. + +Module Exports. +Notation ltPOrderMixin := of_. +Notation LtPOrderMixin := Build. +Coercion porderMixin : ltPOrderMixin >-> POrder.mixin_of. +End Exports. + +End LtPOrderMixin. +Import LtPOrderMixin.Exports. + +Module MeetJoinMixin. +Section MeetJoinMixin. + +Variable (disp : unit) (T : choiceType). + +Record of_ (disp : unit) (T : choiceType) := Build { + le : rel T; + lt : rel T; + meet : T -> T -> T; + join : T -> T -> T; + meetC : commutative meet; + joinC : commutative join; + meetA : associative meet; + joinA : associative join; + joinKI : forall y x : T, meet x (join x y) = x; + meetKU : forall y x : T, join x (meet x y) = x; + meetUl : left_distributive meet join; + meetxx : idempotent meet; + le_def : forall x y : T, le x y = (meet x y == x); + lt_def : forall x y : T, lt x y = (y != x) && le x y; +}. + + +Variable (m : of_ disp T). + +Fact le_refl : reflexive (le m). +Proof. by move=> x; rewrite le_def meetxx. Qed. + +Fact le_anti : antisymmetric (le m). +Proof. by move=> x y; rewrite !le_def meetC => /andP [] /eqP {2}<- /eqP ->. Qed. + +Fact le_trans : transitive (le m). +Proof. +move=> y x z; rewrite !le_def => /eqP lexy /eqP leyz; apply/eqP. +by rewrite -[in LHS]lexy -meetA leyz lexy. +Qed. + +Definition porderMixin : lePOrderMixin T := + LePOrderMixin le_refl le_anti le_trans (lt_def m). + +Definition latticeMixin : latticeMixin (POrderType disp T porderMixin) := + @LatticeMixin disp (POrderType disp T porderMixin) (meet m) (join m) + (meetC m) (joinC m) (meetA m) (joinA m) + (joinKI m) (meetKU m) (le_def m) (meetUl m). + +End MeetJoinMixin. + +Module Exports. +Notation meetJoinMixin := of_. +Notation MeetJoinMixin := Build. +Coercion porderMixin : meetJoinMixin >-> lePOrderMixin. +Coercion latticeMixin : meetJoinMixin >-> Lattice.mixin_of. +End Exports. + +End MeetJoinMixin. +Import MeetJoinMixin.Exports. + +Module LeOrderMixin. +Section LeOrderMixin. + +Record of_ (disp : unit) (T : choiceType) := Build { + le : rel T; + lt : rel T; + meet : T -> T -> T; + join : T -> T -> T; + le_anti : antisymmetric le; + le_trans : transitive le; + le_total : total le; + lt_def : forall x y, lt x y = (y != x) && le x y; + meet_def : forall x y, meet x y = if le x y then x else y; + join_def : forall x y, join x y = if le y x then x else y; +}. + +Variable (disp : unit) (T : choiceType) (m : of_ disp T). + +Fact le_refl : reflexive (le m). +Proof. by move=> x; case: (le m x x) (le_total m x x). Qed. + +Definition T_porderType : porderType disp := + POrderType + disp T + (LePOrderMixin le_refl (@le_anti _ _ m) (@le_trans _ _ m) (lt_def m)). +Definition T_latticeType : latticeType disp := + LatticeType T_porderType (le_total m : totalLatticeMixin T_porderType). + +Implicit Types (x y z : T_latticeType). + +Fact meetE x y : meet m x y = x `&` y. Proof. by rewrite meet_def. Qed. +Fact joinE x y : join m x y = x `|` y. Proof. by rewrite join_def. Qed. +Fact meetC : commutative (meet m). +Proof. by move=> *; rewrite !meetE meetC. Qed. +Fact joinC : commutative (join m). +Proof. by move=> *; rewrite !joinE joinC. Qed. +Fact meetA : associative (meet m). +Proof. by move=> *; rewrite !meetE meetA. Qed. +Fact joinA : associative (join m). +Proof. by move=> *; rewrite !joinE joinA. Qed. +Fact joinKI y x : meet m x (join m x y) = x. +Proof. by rewrite meetE joinE joinKI. Qed. +Fact meetKU y x : join m x (meet m x y) = x. +Proof. by rewrite meetE joinE meetKU. Qed. +Fact meetUl : left_distributive (meet m) (join m). +Proof. by move=> *; rewrite !meetE !joinE meetUl. Qed. +Fact meetxx : idempotent (meet m). +Proof. by move=> *; rewrite meetE meetxx. Qed. +Fact le_def x y : x <= y = (meet m x y == x). +Proof. by rewrite meetE (eq_meetl x y). Qed. + +Definition latticeMixin : meetJoinMixin disp T := + @MeetJoinMixin + _ _ (le m) (lt m) (meet m) (join m) + meetC joinC meetA joinA joinKI meetKU meetUl meetxx le_def (lt_def m). + +Definition totalMixin : + Total.mixin_of (LatticeType (POrderType disp T latticeMixin) latticeMixin) + := le_total m. + +End LeOrderMixin. + +Module Exports. +Notation leOrderMixin := of_. +Notation LeOrderMixin := Build. +Coercion latticeMixin : leOrderMixin >-> meetJoinMixin. +Coercion totalMixin : leOrderMixin >-> Total.mixin_of. +End Exports. + +End LeOrderMixin. +Import LeOrderMixin.Exports. + +Module LtOrderMixin. + +Record of_ (disp : unit) (T : choiceType) := Build { + le : rel T; + lt : rel T; + meet : T -> T -> T; + join : T -> T -> T; + lt_irr : irreflexive lt; + lt_trans : transitive lt; + lt_total : forall x y, x != y -> lt x y || lt y x; + le_def : forall x y, le x y = (x == y) || lt x y; + meet_def : forall x y, meet x y = if lt x y then x else y; + join_def : forall x y, join x y = if lt y x then x else y; +}. + +Section LtOrderMixin. + +Variable (disp : unit) (T : choiceType) (m : of_ disp T). + +Fact le_total : total (le m). +Proof. +by move=> x y; rewrite !le_def (eq_sym y); case: (altP eqP); [|apply: lt_total]. +Qed. + +Definition T_porderType : porderType disp := + POrderType disp T (LtPOrderMixin (lt_irr m) (@lt_trans _ _ m) (le_def m)). +Definition T_latticeType : latticeType disp := + LatticeType T_porderType (le_total : totalLatticeMixin T_porderType). + +Implicit Types (x y z : T_latticeType). + +Fact leP x y : + le_xor_gt x y (x <= y) (y < x) (y `&` x) (x `&` y) (y `|` x) (x `|` y). +Proof. by apply/lcomparable_leP/le_total. Qed. +Fact meetE x y : meet m x y = x `&` y. +Proof. by rewrite meet_def (_ : lt m x y = (x < y)) //; case: (leP y). Qed. +Fact joinE x y : join m x y = x `|` y. +Proof. by rewrite join_def (_ : lt m y x = (y < x)) //; case: leP. Qed. +Fact meetC : commutative (meet m). +Proof. by move=> *; rewrite !meetE meetC. Qed. +Fact joinC : commutative (join m). +Proof. by move=> *; rewrite !joinE joinC. Qed. +Fact meetA : associative (meet m). +Proof. by move=> *; rewrite !meetE meetA. Qed. +Fact joinA : associative (join m). +Proof. by move=> *; rewrite !joinE joinA. Qed. +Fact joinKI y x : meet m x (join m x y) = x. +Proof. by rewrite meetE joinE joinKI. Qed. +Fact meetKU y x : join m x (meet m x y) = x. +Proof. by rewrite meetE joinE meetKU. Qed. +Fact meetUl : left_distributive (meet m) (join m). +Proof. by move=> *; rewrite !meetE !joinE meetUl. Qed. +Fact meetxx : idempotent (meet m). +Proof. by move=> *; rewrite meetE meetxx. Qed. +Fact le_def' x y : x <= y = (meet m x y == x). +Proof. by rewrite meetE (eq_meetl x y). Qed. + +Definition latticeMixin : meetJoinMixin disp T := + @MeetJoinMixin + _ _ (le m) (lt m) (meet m) (join m) + meetC joinC meetA joinA joinKI meetKU meetUl meetxx + le_def' (@lt_def _ T_latticeType). + +Definition totalMixin : + Total.mixin_of (LatticeType (POrderType disp T latticeMixin) latticeMixin) + := le_total. + +End LtOrderMixin. + +Module Exports. +Notation ltOrderMixin := of_. +Notation LtOrderMixin := Build. +Coercion latticeMixin : ltOrderMixin >-> meetJoinMixin. +Coercion totalMixin : ltOrderMixin >-> Total.mixin_of. +End Exports. + +End LtOrderMixin. +Import LtOrderMixin.Exports. + (*************) (* INSTANCES *) (*************) -Module Import NatOrder. +Module NatOrder. Section NatOrder. -Fact nat_display : unit. Proof. exact: tt. Qed. -Program Definition natPOrderMixin := @POrderMixin _ leq ltn _ leqnn anti_leq leq_trans. -Next Obligation. by rewrite ltn_neqAle. Qed. -Canonical natPOrderType := POrderType nat_display nat natPOrderMixin. +Lemma minnE x y : minn x y = if (x <= y)%N then x else y. +Proof. by case: leqP => [/minn_idPl|/ltnW /minn_idPr]. Qed. + +Lemma maxnE x y : maxn x y = if (y <= x)%N then x else y. +Proof. by case: leqP => [/maxn_idPl|/ltnW/maxn_idPr]. Qed. + +Lemma ltn_def x y : (x < y)%N = (y != x) && (x <= y)%N. +Proof. by rewrite ltn_neqAle eq_sym. Qed. -Lemma leEnat (n m : nat): (n <= m) = (n <= m)%N. +Definition orderMixin := + LeOrderMixin total_display anti_leq leq_trans leq_total ltn_def minnE maxnE. + +Canonical porderType := POrderType total_display nat orderMixin. +Canonical latticeType := LatticeType nat orderMixin. +Canonical orderType := OrderType nat orderMixin. +Canonical blatticeType := BLatticeType nat (BLatticeMixin leq0n). + +Lemma leEnat: le = leq. Proof. by []. Qed. Lemma ltEnat (n m : nat): (n < m) = (n < m)%N. Proof. by []. Qed. -Definition natLatticeMixin := TotalLattice.Mixin leq_total. -Canonical natLatticeType := LatticeType nat natLatticeMixin. -Canonical natOrderType := OrderType nat leq_total. - -Definition natBLatticeMixin := BLatticeMixin leq0n. -Canonical natBLatticeType := BLatticeType nat natBLatticeMixin. +End NatOrder. +Module Exports. +Canonical porderType. +Canonical latticeType. +Canonical orderType. +Canonical blatticeType. +Definition leEnat := leEnat. +Definition ltEnat := ltEnat. +End Exports. End NatOrder. -Notation "@max" := (@join nat_display). -Notation max := (@join nat_display _). -Notation "@min" := (@meet nat_display). -Notation min := (@meet nat_display _). +Module ProductOrder. +Section ProductOrder. +Context {disp1 disp2 disp3 : unit}. -Notation "\max_ ( i <- r | P ) F" := - (\big[@join nat_display _/0%O]_(i <- r | P%B) F%O) : order_scope. -Notation "\max_ ( i <- r ) F" := - (\big[@join nat_display _/0%O]_(i <- r) F%O) : order_scope. -Notation "\max_ ( i | P ) F" := - (\big[@join nat_display _/0%O]_(i | P%B) F%O) : order_scope. -Notation "\max_ i F" := - (\big[@join nat_display _/0%O]_i F%O) : order_scope. -Notation "\max_ ( i : I | P ) F" := - (\big[@join nat_display _/0%O]_(i : I | P%B) F%O) (only parsing) : order_scope. -Notation "\max_ ( i : I ) F" := - (\big[@join nat_display _/0%O]_(i : I) F%O) (only parsing) : order_scope. -Notation "\max_ ( m <= i < n | P ) F" := - (\big[@join nat_display _/0%O]_(m <= i < n | P%B) F%O) : order_scope. -Notation "\max_ ( m <= i < n ) F" := - (\big[@join nat_display _/0%O]_(m <= i < n) F%O) : order_scope. -Notation "\max_ ( i < n | P ) F" := - (\big[@join nat_display _/0%O]_(i < n | P%B) F%O) : order_scope. -Notation "\max_ ( i < n ) F" := - (\big[@join nat_display _/0%O]_(i < n) F%O) : order_scope. -Notation "\max_ ( i 'in' A | P ) F" := - (\big[@join nat_display _/0%O]_(i in A | P%B) F%O) : order_scope. -Notation "\max_ ( i 'in' A ) F" := - (\big[@join nat_display _/0%O]_(i in A) F%O) : order_scope. +Section POrder. +Variable (T : porderType disp1) (T' : porderType disp2). -End NatOrder. +Definition le (x y : T * T') := (x.1 <= y.1) && (x.2 <= y.2). +Fact refl : reflexive le. +Proof. by move=> ?; rewrite /le !lexx. Qed. -Module SeqLexPOrder. -Section SeqLexPOrder. -Context {display : unit}. -Local Notation porderType := (porderType display). -Variable T : porderType. +Fact anti : antisymmetric le. +Proof. +case=> [? ?] [? ?]. +by rewrite andbAC andbA andbAC -andbA => /= /andP [] /le_anti -> /le_anti ->. +Qed. + +Fact trans : transitive le. +Proof. +rewrite /le => y x z /andP [] hxy ? /andP [] /(le_trans hxy) ->. +by apply: le_trans. +Qed. + +Definition porderMixin := LePOrderMixin refl anti trans (rrefl _). +Canonical porderType := POrderType disp3 (T * T') porderMixin. + +End POrder. + +Section Lattice. +Variable (T : latticeType disp1) (T' : latticeType disp2). +Implicit Types (x y : T * T'). + +Definition meet x y := (x.1 `&` y.1, x.2 `&` y.2). +Definition join x y := (x.1 `|` y.1, x.2 `|` y.2). + +Fact meetC : commutative meet. +Proof. by move=> ? ?; congr pair; rewrite meetC. Qed. + +Fact joinC : commutative join. +Proof. by move=> ? ?; congr pair; rewrite joinC. Qed. + +Fact meetA : associative meet. +Proof. by move=> ? ? ?; congr pair; rewrite meetA. Qed. + +Fact joinA : associative join. +Proof. by move=> ? ? ?; congr pair; rewrite joinA. Qed. + +Fact joinKI y x : meet x (join x y) = x. +Proof. by case: x => ? ?; congr pair; rewrite joinKI. Qed. + +Fact meetKU y x : join x (meet x y) = x. +Proof. by case: x => ? ?; congr pair; rewrite meetKU. Qed. + +Fact leEmeet x y : (x <= y) = (meet x y == x). +Proof. by rewrite /POrderDef.le /= /le /meet eqE /= -!leEmeet. Qed. + +Fact meetUl : left_distributive meet join. +Proof. by move=> ? ? ?; congr pair; rewrite meetUl. Qed. + +Definition latticeMixin := + Lattice.Mixin meetC joinC meetA joinA joinKI meetKU leEmeet meetUl. +Canonical latticeType := LatticeType (T * T') latticeMixin. + +End Lattice. + +Section BLattice. +Variable (T : blatticeType disp1) (T' : blatticeType disp2). + +Fact le0x (x : T * T') : (0, 0) <= x. +Proof. by rewrite /POrderDef.le /= /le !le0x. Qed. + +Canonical blatticeType := BLatticeType (T * T') (BLattice.Mixin le0x). + +End BLattice. + +Section TBLattice. +Variable (T : tblatticeType disp1) (T' : tblatticeType disp2). + +Fact lex1 (x : T * T') : x <= (top, top). +Proof. by rewrite /POrderDef.le /= /le !lex1. Qed. + +Canonical tblatticeType := TBLatticeType (T * T') (TBLattice.Mixin lex1). + +End TBLattice. + +Section CBLattice. +Variable (T : cblatticeType disp1) (T' : cblatticeType disp2). +Implicit Types (x y : T * T'). + +Definition sub x y := (x.1 `\` y.1, x.2 `\` y.2). + +Lemma subKI x y : y `&` (sub x y) = 0. +Proof. by congr pair; rewrite subKI. Qed. + +Lemma joinIB x y : (x `&` y) `|` (sub x y) = x. +Proof. by case: x => ? ?; congr pair; rewrite joinIB. Qed. + +Definition cblatticeMixin := CBLattice.Mixin subKI joinIB. +Canonical cblatticeType := CBLatticeType (T * T') cblatticeMixin. + +End CBLattice. + +Section CTBLattice. +Variable (T : ctblatticeType disp1) (T' : ctblatticeType disp2). +Implicit Types (x y : T * T'). + +Definition compl x := (~` x.1, ~` x.2). + +Lemma complE x : compl x = sub 1 x. +Proof. by congr pair; rewrite complE. Qed. + +Definition ctblatticeMixin := CTBLattice.Mixin complE. +Canonical ctblatticeType := CTBLatticeType (T * T') ctblatticeMixin. +(* Let default_ctblatticeType := [default_ctblatticeType of T * T']. *) + +End CTBLattice. + +Canonical finPOrderType (T : finPOrderType disp1) (T' : finPOrderType disp2) := + [finPOrderType of T * T']. + +Canonical finLatticeType + (T : finLatticeType disp1) (T' : finLatticeType disp2) := + [finLatticeType of T * T']. + +Canonical finClatticeType + (T : finCLatticeType disp1) (T' : finCLatticeType disp2) := + [finCLatticeType of T * T']. + +End ProductOrder. + +Module Exports. +Canonical porderType. +Canonical latticeType. +Canonical blatticeType. +Canonical tblatticeType. +Canonical cblatticeType. +Canonical ctblatticeType. +Canonical finPOrderType. +Canonical finLatticeType. +Canonical finClatticeType. +End Exports. +End ProductOrder. + +Module ProdLexOrder. +Section ProdLexOrder. +Context {disp1 disp2 disp3 : unit}. + +Section POrder. +Variable (T : porderType disp1) (T' : porderType disp2). +Implicit Types (x y : T * T'). + +Definition le x y := (x.1 <= y.1) && ((x.1 >= y.1) ==> (x.2 <= y.2)). + +Fact refl : reflexive le. +Proof. by move=> ?; by rewrite /le !lexx. Qed. + +Fact anti : antisymmetric le. +Proof. +rewrite /le => -[x x'] [y y'] /=; case_eq (y <= x); case_eq (x <= y) => //. +by move=> //= hxy hyx /le_anti ->; move/andP/le_anti: (conj hxy hyx) => ->. +Qed. + +Fact trans : transitive le. +Proof. +move=> y x z /andP [hxy /implyP hxy'] /andP [hyz /implyP hyz']. +rewrite /le (le_trans hxy) //=; apply/implyP => hzx. +by apply/le_trans/hxy'/(le_trans hyz): (hyz' (le_trans hzx hxy)). +Qed. + +Definition porderMixin := LePOrderMixin refl anti trans (rrefl _). +Canonical porderType := POrderType disp3 (T * T') porderMixin. + +End POrder. + +Section Total. +Variable (T : orderType disp1) (T' : orderType disp2). +Implicit Types (x y : T * T'). + +Fact total : totalLatticeMixin [porderType of T * T']. +Proof. +move=> x y; rewrite /POrderDef.le /= /le; case: (ltgtP x.1 y.1) => _ //=. +by apply: le_total. +Qed. + +Canonical latticeType := LatticeType (T * T') total. +Canonical totalType := LatticeType (T * T') total. + +End Total. + +End ProdLexOrder. + +Module Exports. +Canonical porderType. +Canonical latticeType. +Canonical totalType. +End Exports. +End ProdLexOrder. + +Module SeqProdOrder. +Section SeqProdOrder. +Context {disp disp' : unit}. + +Section POrder. +Variable T : porderType disp. +Implicit Types s : seq T. + +Fixpoint le s1 s2 := + if s1 is x1 :: s1' then + if s2 is x2 :: s2' then (x1 <= x2) && le s1' s2' else false + else + true. + +Fact refl : reflexive le. +Proof. by elim=> //= ? ? ?; rewrite !lexx. Qed. + +Fact anti : antisymmetric le. +Proof. +elim=> [|? ? ih] [|? ?] //=. +by rewrite andbAC andbA andbAC -andbA => /andP [] /le_anti -> /ih ->. +Qed. + +Fact trans : transitive le. +Proof. +elim=> [|y ys ih] [|x xs] [|z zs] //=. +by case/andP => [] xy xys /andP [] /(le_trans xy) -> /(ih _ _ xys). +Qed. + +Definition porderMixin := LePOrderMixin refl anti trans (rrefl _). +Canonical porderType := POrderType disp' (seq T) porderMixin. + +End POrder. + +Section BLattice. +Variable T : latticeType disp. +Implicit Types s : seq T. + +Fixpoint meet s1 s2 := + match s1, s2 with + | x1 :: s1', x2 :: s2' => (x1 `&` x2) :: meet s1' s2' + | _, _ => [::] + end. + +Fixpoint join s1 s2 := + match s1, s2 with + | [::], _ => s2 + | _, [::] => s1 + | x1 :: s1', x2 :: s2' => (x1 `|` x2) :: join s1' s2' + end. + +Fact meetC : commutative meet. +Proof. by elim=> [|? ? ih] [|? ?] //=; rewrite meetC ih. Qed. + +Fact joinC : commutative join. +Proof. by elim=> [|? ? ih] [|? ?] //=; rewrite joinC ih. Qed. + +Fact meetA : associative meet. +Proof. by elim=> [|? ? ih] [|? ?] [|? ?] //=; rewrite meetA ih. Qed. + +Fact joinA : associative join. +Proof. by elim=> [|? ? ih] [|? ?] [|? ?] //=; rewrite joinA ih. Qed. + +Fact meetss s : meet s s = s. +Proof. by elim: s => [|? ? ih] //=; rewrite meetxx ih. Qed. + +Fact joinKI y x : meet x (join x y) = x. +Proof. +elim: x y => [|? ? ih] [|? ?] //=; rewrite (meetxx, joinKI) ?ih //. +by congr cons; rewrite meetss. +Qed. + +Fact meetKU y x : join x (meet x y) = x. +Proof. by elim: x y => [|? ? ih] [|? ?] //=; rewrite meetKU ih. Qed. + +Fact leEmeet x y : (x <= y) = (meet x y == x). +Proof. +rewrite /POrderDef.le /=. +by elim: x y => [|? ? ih] [|? ?] //=; rewrite /eq_op /= leEmeet ih. +Qed. + +Fact meetUl : left_distributive meet join. +Proof. by elim=> [|? ? ih] [|? ?] [|? ?] //=; rewrite meetUl ih. Qed. +Fact le0x s : [::] <= s. +Proof. by []. Qed. + +Definition latticeMixin := + Lattice.Mixin meetC joinC meetA joinA joinKI meetKU leEmeet meetUl. +Canonical latticeType := LatticeType (seq T) latticeMixin. +Canonical blatticeType := BLatticeType (seq T) (BLattice.Mixin le0x). + +End BLattice. + +End SeqProdOrder. + +Module Exports. +Canonical porderType. +Canonical latticeType. +Canonical blatticeType. +End Exports. +End SeqProdOrder. + +Module SeqLexOrder. +Section SeqLexOrder. +Context {disp : unit}. + +Section POrder. +Variable T : porderType disp. Implicit Types s : seq T. -Fixpoint lexi s1 s2 := +Fixpoint le s1 s2 := if s1 is x1 :: s1' then if s2 is x2 :: s2' then - (x1 < x2) || ((x1 == x2) && lexi s1' s2') + (x1 < x2) || (x1 == x2) && le s1' s2' else false else true. -Fact lexi_le_head x sx y sy: - lexi (x :: sx) (y :: sy) -> x <= y. -Proof. by case/orP => [/ltW|/andP [/eqP-> _]]. Qed. - -Fact lexi_refl: reflexive lexi. +Fact refl: reflexive le. Proof. by elim => [|x s ih] //=; rewrite eqxx ih orbT. Qed. -Fact lexi_anti: antisymmetric lexi. +Fact anti: antisymmetric le. Proof. move=> x y /andP []; elim: x y => [|x sx ih] [|y sy] //=. by case: comparableP => //= -> lesxsy /(ih _ lesxsy) ->. Qed. -Fact lexi_trans: transitive lexi. +Fact trans: transitive le. Proof. elim=> [|y sy ih] [|x sx] [|z sz] //=. case: (comparableP x y) => //=; case: (comparableP y z) => //=. @@ -2798,17 +3616,49 @@ case: (comparableP x y) => //=; case: (comparableP y z) => //=. - by move=> ltyz /lt_trans - /(_ _ ltyz) ->. Qed. -Definition lexi_porderMixin := LePOrderMixin lexi_refl lexi_anti lexi_trans. -Canonical lexi_porderType := POrderType display (seq T) lexi_porderMixin. +Definition porderMixin := LePOrderMixin refl anti trans (rrefl _). +Canonical porderType := POrderType disp (seq T) porderMixin. + +Fact lexi_le_head x sx y sy: x :: sx <= y :: sy -> x <= y. +Proof. by case/orP => [/ltW|/andP [/eqP-> _]]. Qed. + +End POrder. -End SeqLexPOrder. -End SeqLexPOrder. +Section Total. +Variable T : orderType disp. +Implicit Types s : seq T. -Canonical SeqLexPOrder.lexi_porderType. +Fact total : totalLatticeMixin [porderType of seq T]. +Proof. +rewrite /totalLatticeMixin /= /POrderDef.le /=. +by elim=> [|? ? ih] [|? ?] //=;case: ltgtP => //=. +Qed. + +Fact le0x s : [::] <= s. +Proof. by []. Qed. + +Canonical latticeType := LatticeType (seq T) total. +Canonical blatticeType := BLatticeType (seq T) (BLattice.Mixin le0x). +Canonical totalType := LatticeType (seq T) total. + +End Total. + +End SeqLexOrder. + +Module Exports. +Canonical porderType. +Canonical latticeType. +Canonical blatticeType. +Canonical totalType. +Definition lexi_le_head := @lexi_le_head. +Arguments lexi_le_head {disp}. +End Exports. +End SeqLexOrder. Module Def. Export POrderDef. Export LatticeDef. +Export TotalDef. Export BLatticeDef. Export TBLatticeDef. Export CBLatticeDef. @@ -2817,43 +3667,58 @@ End Def. Module Syntax. Export POSyntax. +Export TotalSyntax. Export LatticeSyntax. Export BLatticeSyntax. Export TBLatticeSyntax. Export CBLatticeSyntax. Export CTBLatticeSyntax. -Export ReverseSyntax. +Export ConverseSyntax. End Syntax. -Module Theory. -Export ReversePOrder. +Module LTheory. +Export POCoercions. +Export ConversePOrder. Export POrderTheory. -Export TotalTheory. -Export ReverseLattice. + +Export ConverseLattice. Export LatticeTheoryMeet. Export LatticeTheoryJoin. Export BLatticeTheory. -Export CBLatticeTheory. -Export ReverseTBLattice. +Export ConverseTBLattice. Export TBLatticeTheory. -Export CTBLatticeTheory. -Export NatOrder. -Export SeqLexPOrder. +End LTheory. -Export POrder.Exports. -Export Total.Exports. -Export Lattice.Exports. -Export BLattice.Exports. -Export CBLattice.Exports. -Export TBLattice.Exports. -Export CTBLattice.Exports. -Export FinPOrder.Exports. -Export FinTotal.Exports. -Export FinLattice.Exports. -Export FinBLattice.Exports. -Export FinCBLattice.Exports. -Export FinTBLattice.Exports. -Export FinCTBLattice.Exports. +Module CTheory. +Export LTheory CBLatticeTheory CTBLatticeTheory. +End CTheory. + +Module TTheory. +Export LTheory TotalTheory. +End TTheory. + +Module Theory. +Export CTheory TotalTheory. End Theory. End Order. + +Export Order.POrder.Exports. +Export Order.FinPOrder.Exports. +Export Order.Lattice.Exports. +Export Order.BLattice.Exports. +Export Order.TBLattice.Exports. +Export Order.FinLattice.Exports. +Export Order.CBLattice.Exports. +Export Order.CTBLattice.Exports. +Export Order.FinCLattice.Exports. +Export Order.Total.Exports. +Export Order.FinTotal.Exports. + +Export Order.TotalLatticeMixin.Exports. +Export Order.LePOrderMixin.Exports. +Export Order.LtPOrderMixin.Exports. +Export Order.MeetJoinMixin.Exports. +Export Order.LeOrderMixin.Exports. +Export Order.LtOrderMixin.Exports. +Export Order.NatOrder.Exports. diff --git a/set.v b/set.v index bd275a2..dcc6ea0 100644 --- a/set.v +++ b/set.v @@ -140,22 +140,24 @@ Structure mixin_of d (set : elementType -> (cblatticeType (display_set d))) := (memset (imset f A) y) }. -Record class_of d (set : elementType -> Type) := Class { - base : forall X, @Order.CBLattice.class_of (display_set d) (set X); - mixin : mixin_of (fun X => Order.CBLattice.Pack (base X)) +Record class_of (set : elementType -> Type) := Class { + base : forall X, @Order.CBLattice.class_of (set X); + mixin_disp : unit; + mixin : mixin_of (fun X => Order.CBLattice.Pack (display_set mixin_disp) (base X)) }. Local Coercion base : class_of >-> Funclass. -Structure type d := Pack { sort ; _ : class_of d sort }. +Structure type (disp : unit) := Pack { sort ; _ : class_of sort }. Local Coercion sort : type >-> Funclass. Variables (set : elementType -> Type) (disp : unit) (cT : type disp). -Definition class := let: Pack _ c as cT' := cT return class_of _ cT' in c. -Definition clone disp' c of (disp = disp') & phant_id class c := - @Pack disp' set c. +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. +Definition clone c & phant_id class c := @Pack disp set c. +Definition clone_with disp' c of phant_id class c := @Pack disp' set c. + Let xset := let: Pack set _ := cT in set. Notation xclass := (class : class_of _ xset). @@ -164,7 +166,7 @@ Definition pack b0 (fun X=> @Order.CBLattice.Pack (display_set disp) (set X) (b0 X))) := fun bT b & (forall X, phant_id (@Order.CBLattice.class (display_set disp) (bT X)) (b X)) => - fun m & phant_id m0 m => Pack (@Class disp set b m). + fun disp' m & phant_id m0 m => Pack disp (@Class set b disp' m). End ClassDef. Section CanonicalDef. @@ -179,7 +181,7 @@ Variables (disp : unit) (cT : type disp). Local Notation ddisp := (display_set disp). Let xset := let: Pack set _ := cT in set. -Notation xclass := (@class _ eqType_of_elementType _ cT : class_of eqType_of_elementType _ xset). +Notation xclass := (@class _ eqType_of_elementType _ cT : class_of eqType_of_elementType xset). Definition eqType := @Equality.Pack (cT X) (xclass X). Definition choiceType := @Choice.Pack (cT X) (xclass X). @@ -212,10 +214,10 @@ Notation semisetMixin := mixin_of. Notation SemisetMixin := Mixin. Notation SemisetType set m := (@pack _ _ set _ _ m _ _ (fun=> id) _ id). -Notation "[ 'semisetType' 'of' set 'for' cset ]" := (@clone _ _ set _ cset _ _ erefl id) +Notation "[ 'semisetType' 'of' set 'for' cset ]" := (@clone _ _ set _ cset _ id) (at level 0, format "[ 'semisetType' 'of' set 'for' cset ]") : form_scope. Notation "[ 'semisetType' 'of' set 'for' cset 'with' disp ]" := - (@clone _ _ set _ cset disp _ (unit_irrelevance _ _) id) + (@clone_with _ _ set _ cset _ disp _ id) (at level 0, format "[ 'semisetType' 'of' set 'for' cset 'with' disp ]") : form_scope. Notation "[ 'semisetType' 'of' set ]" := [semisetType of set for _] (at level 0, format "[ 'semisetType' 'of' set ]") : form_scope. @@ -321,42 +323,42 @@ Implicit Types (x y : X) (A B C : set X). Lemma notin_set0 (x : X) : x \notin (set0 : set X). Proof. rewrite /set1 /in_mem /= /memset. -case: set => [S [base [memset set1 /= H ? ? ? ? ? ? ? ? ?]]] /=. +case: set => [S [base ? [memset set1 /= H ? ? ? ? ? ? ? ? ?]]] /=. exact: H. Qed. Lemma in_set1 x y : x \in ([set y] : set X) = (x == y). Proof. rewrite /set1 /in_mem /= /memset. -case: set => [S [base [memset set1 /= ? H ? ? ? ? ? ? ? ?]]] /=. +case: set => [S [base ? [memset set1 /= ? H ? ? ? ? ? ? ? ?]]] /=. exact: H. Qed. Lemma sub1set x A : ([set x] \subset A) = (x \in A). Proof. rewrite /set1 /in_mem /= /memset. -case: set A => [S [base [memset set1 /= ? ? H ? ? ? ? ? ? ?]]] A /=. +case: set A => [S [base ? [memset set1 /= ? ? H ? ? ? ? ? ? ?]]] A /=. exact: H. Qed. Lemma set_gt0_ex A : set0 \proper A -> {x | x \in A}. Proof. rewrite /set1 /in_mem /= /memset. -case: set A => [S [base [memset set1 /= ? ? ? H ? ? ? ? ? ?]]] A /=. +case: set A => [S [base ? [memset set1 /= ? ? ? H ? ? ? ? ? ?]]] A /=. exact: H. Qed. Lemma subsetP_subproof A B : {subset A <= B} -> A \subset B. Proof. rewrite /set1 /in_mem /= /memset. -case: set A B => [S [base [memset set1 /= ? ? ? ? H ? ? ? ? ?]]] /=. +case: set A B => [S [base ? [memset set1 /= ? ? ? ? H ? ? ? ? ?]]] /=. exact: H. Qed. Lemma in_setU (x : X) A B : (x \in A :|: B) = (x \in A) || (x \in B). Proof. rewrite /set1 /in_mem /= /memset. -case: set A B => [S [base [memset set1 /= ? ? ? ? ? H ? ? ? ?]]] /=. +case: set A B => [S [base ? [memset set1 /= ? ? ? ? ? H ? ? ? ?]]] /=. exact: H. Qed. @@ -780,7 +782,7 @@ Lemma subUset A B C : (B :|: C \subset A) = (B \subset A) && (C \subset A). Proof. exact: leUx. Qed. Lemma subsetU A B C : (A \subset B) || (A \subset C) -> A \subset B :|: C. -Proof. exact: lexU. Qed. +Proof. exact: lexU2. Qed. Lemma subUsetP A B C : reflect (A \subset C /\ B \subset C) (A :|: B \subset C). Proof. by rewrite subUset; apply: andP. Qed. @@ -850,7 +852,7 @@ Lemma imsetP (f : setfun set X Y) A y : reflect (exists2 x : X, x \in A & y = f x) (y \in imset f A). Proof. move: A f; rewrite /set1 /in_mem /= /memset /imset /setfun. -case: set => [S [base [memset set1 /= ? ? ? ? ? ? ? ? ? H]]] /= A f. +case: set => [S [base ? [memset set1 /= ? ? ? ? ? ? ? ? ? H]]] /= A f. exact: H. Qed. @@ -902,34 +904,34 @@ Variable eqType_of_elementType : elementType -> eqType. Coercion eqType_of_elementType : elementType >-> eqType. Implicit Types (X Y : elementType). -Record class_of d (set : elementType -> Type) := Class { - base : forall X, Order.CTBLattice.class_of (display_set d) (set X); +Record class_of (set : elementType -> Type) := Class { + base : forall X, Order.CTBLattice.class_of (set X); + mixin_disp : unit; mixin : Semiset.mixin_of eqType_of_elementType - (fun X => Order.CBLattice.Pack (base X)) + (fun X => Order.CBLattice.Pack (display_set mixin_disp) (base X)) }. Local Coercion base : class_of >-> Funclass. -Definition base2 d (set : elementType -> Type) - (c : class_of d set) := Semiset.Class (@mixin _ set c). +Definition base2 (set : elementType -> Type) + (c : class_of set) := Semiset.Class (@mixin set c). Local Coercion base2 : class_of >-> Semiset.class_of. -Structure type d := Pack { sort ; _ : class_of d sort }. +Structure type (disp : unit) := Pack { sort ; _ : class_of sort }. Local Coercion sort : type >-> Funclass. Variables (set : elementType -> Type) (disp : unit) (cT : type disp). -Definition class := let: Pack _ c as cT' := cT return class_of _ cT' in c. -(* Definition clone c of phant_id class c := @Pack set c set. *) +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. Let xset := let: Pack set _ := cT in set. Notation xclass := (class : class_of xset). Definition pack := - fun bT (b : forall X, Order.CTBLattice.class_of _ _) + fun bT (b : forall X, Order.CTBLattice.class_of _) & (forall X, phant_id (@Order.CTBLattice.class disp (bT X)) (b X)) => - fun mT m & phant_id (@Semiset.class _ eqType_of_elementType mT) - (@Semiset.Class _ _ disp set b m) => - Pack (@Class _ set (fun x => b x) m). + fun d' mT m & phant_id (@Semiset.class _ eqType_of_elementType mT) + (@Semiset.Class _ _ set b d' m) => + Pack disp (@Class set (fun x => b x) _ m). End ClassDef. @@ -946,7 +948,7 @@ Variable (disp : unit) (cT : type disp). Local Notation ddisp := (display_set disp). Let xset := let: Pack set _ := cT in set. -Notation xclass := (@class _ eqType_of_elementType _ cT : class_of eqType_of_elementType _ xset). +Notation xclass := (@class _ eqType_of_elementType _ cT : class_of eqType_of_elementType xset). Definition eqType := @Equality.Pack (cT X) (xclass X). Definition choiceType := @Choice.Pack (cT X) (xclass X). @@ -984,8 +986,7 @@ Canonical semisetType. Notation setType := type. -Notation "[ 'setType' 'of' set ]" := - (@pack _ _ set _ _ _ (fun=> id) _ _ id) +Notation "[ 'setType' 'of' set ]" := (@pack _ _ set _ _ _ (fun=> id) _ _ _ id) (at level 0, format "[ 'setType' 'of' set ]") : form_scope. End Exports. diff --git a/shell.nix b/shell.nix index cc79bb7..bea2794 100644 --- a/shell.nix +++ b/shell.nix @@ -4,7 +4,7 @@ sha256 = "0rxjkfiq53ibz0rzggvnp341b6kgzgfr9x6q07m2my7ijlirs2da"; }), coq-version ? "8.9", -mc ? "1.9.0", +mc ? "1.8.0", print-env ? false }: let