diff options
| author |  Benjamin Barenblat <bbaren@debian.org> | 2019-01-17 19:58:25 -0500 |
|---|---|---|
| committer | Benjamin Barenblat <bbaren@debian.org> | 2019-01-17 19:58:25 -0500 |
| commit | 5d3dc22cc205021e517a81943952655c51777083 (patch) | |
| tree | 4cfec21ee5ea97969480ac7d932c56e1dc8fb59f | |
| parent | bac5683a8429042f04a0f60643f6f0d1983b7842 (diff) | |
Restore ssrmatching and its reverse dependencies
4181269ff800d58e60b886d0aaa2894444a9cd0d removed ssrmatching and
everything that needed it because upstream had shipped a couple of
files with bad license headers. Those files have now been fixed
(https://github.com/coq/coq/pull/9282), so grab them from master and
apply them in a patch. This restores ssrmatching to the Coq standard
library.
Once upstream cuts its next release, we should be able to delete the
patch and simply import the files from the upstream tarball.
| -rw-r--r-- | debian/changelog | 7 | ||||
| -rw-r--r-- | debian/libcoq-ocaml.install.in | 4 | ||||
| -rw-r--r-- | debian/patches/0005-remove-ssrmatching.patch | 3337 | ||||
| -rw-r--r-- | debian/patches/0005-ssrmatching-license.patch | 298 | ||||
| -rw-r--r-- | debian/patches/series | 2 |
5 files changed, 310 insertions, 3338 deletions
diff --git a/debian/changelog b/debian/changelog index 295778b0..ff8582b8 100644 --- a/debian/changelog +++ b/debian/changelog @@ -1,3 +1,10 @@ +coq (8.8.2-2) UNRELEASED; urgency=medium + + * Use freely licensed files from upstream to restore ssrmatching and reverse + dependencies. + + -- Benjamin Barenblat <bbaren@debian.org> Thu, 17 Jan 2019 17:10:25 -0500 + coq (8.8.2-1) unstable; urgency=medium * New upstream release (Closes: #910840) diff --git a/debian/libcoq-ocaml.install.in b/debian/libcoq-ocaml.install.in index c89a0e53..44d87c81 100644 --- a/debian/libcoq-ocaml.install.in +++ b/debian/libcoq-ocaml.install.in @@ -21,6 +21,8 @@ usr/lib/coq/plugins/syntax/nat_syntax_plugin.cmo usr/lib/coq/plugins/syntax/ascii_syntax_plugin.cmo usr/lib/coq/plugins/syntax/string_syntax_plugin.cmo usr/lib/coq/plugins/syntax/z_syntax_plugin.cmo +usr/lib/coq/plugins/ssr/ssreflect_plugin.cmo +usr/lib/coq/plugins/ssrmatching/ssrmatching_plugin.cmo usr/lib/coq/toploop/proofworkertop.cma usr/lib/coq/toploop/tacworkertop.cma usr/lib/coq/toploop/queryworkertop.cma @@ -49,3 +51,5 @@ DYN: usr/lib/coq/plugins/syntax/r_syntax_plugin.cmxs DYN: usr/lib/coq/plugins/syntax/int31_syntax_plugin.cmxs DYN: usr/lib/coq/plugins/syntax/ascii_syntax_plugin.cmxs DYN: usr/lib/coq/plugins/syntax/string_syntax_plugin.cmxs +DYN: usr/lib/coq/plugins/ssr/ssreflect_plugin.cmxs +DYN: usr/lib/coq/plugins/ssrmatching/ssrmatching_plugin.cmxs diff --git a/debian/patches/0005-remove-ssrmatching.patch b/debian/patches/0005-remove-ssrmatching.patch deleted file mode 100644 index a4030ec7..00000000 --- a/debian/patches/0005-remove-ssrmatching.patch +++ /dev/null @@ -1,3337 +0,0 @@ -From: Benjamin Barenblat <bbaren@debian.org> -Subject: Remove ssrmatching -Forwarded: not-needed -Last-Update: 2018-12-29 - -ssrmatching still has two files licensed under CeCILL-B, which I believe -is a nonfree license. I’ve removed them from the Debian source package -(see gbp.conf). This patch disables everything that depends on them. - -This patch is fortunately a stopgap: Upstream believes that the files -should have had the license headers changed to LGPL when importing them -and has created a pull request to change the headers now -(https://github.com/coq/coq/pull/9282). Once that is merged, this patch -should disappear and be replaced with a backport of that PR. ---- a/Makefile.common -+++ b/Makefile.common -@@ -84,7 +84,7 @@ - setoid_ring extraction fourier \ - cc funind firstorder derive \ - rtauto nsatz syntax btauto \ -- ssrmatching ltac ssr -+ ltac - - SRCDIRS:=\ - $(CORESRCDIRS) \ -@@ -149,7 +149,7 @@ - $(FOURIERCMO) $(EXTRACTIONCMO) \ - $(CCCMO) $(FOCMO) $(RTAUTOCMO) $(BTAUTOCMO) \ - $(FUNINDCMO) $(NSATZCMO) $(NATSYNTAXCMO) $(OTHERSYNTAXCMO) \ -- $(DERIVECMO) $(SSRMATCHINGCMO) $(SSRCMO) -+ $(DERIVECMO) - - ifeq ($(HASNATDYNLINK)-$(BEST),false-opt) - STATICPLUGINS:=$(PLUGINSCMO) ---- a/test-suite/success/ssrpattern.v -+++ /dev/null -@@ -1,22 +0,0 @@ --Require Import ssrmatching. -- --(*Set Debug SsrMatching.*) -- --Tactic Notation "at" "[" ssrpatternarg(pat) "]" tactic(t) := -- let name := fresh in -- let def_name := fresh in -- ssrpattern pat; -- intro name; -- pose proof (refl_equal name) as def_name; -- unfold name at 1 in def_name; -- t def_name; -- [ rewrite <- def_name | idtac.. ]; -- clear name def_name. -- --Lemma test (H : True -> True -> 3 = 7) : 28 = 3 * 4. --Proof. --at [ X in X * 4 ] ltac:(fun place => rewrite -> H in place). --- reflexivity. --- trivial. --- trivial. --Qed. ---- a/plugins/ssr/ssreflect.v -+++ /dev/null -@@ -1,453 +0,0 @@ --(************************************************************************) --(* * The Coq Proof Assistant / The Coq Development Team *) --(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) --(* <O___,, * (see CREDITS file for the list of authors) *) --(* \VV/ **************************************************************) --(* // * This file is distributed under the terms of the *) --(* * GNU Lesser General Public License Version 2.1 *) --(* * (see LICENSE file for the text of the license) *) --(************************************************************************) -- --(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -- --Require Import Bool. (* For bool_scope delimiter 'bool'. *) --Require Import ssrmatching. --Declare ML Module "ssreflect_plugin". -- --(******************************************************************************) --(* This file is the Gallina part of the ssreflect plugin implementation. *) --(* Files that use the ssreflect plugin should always Require ssreflect and *) --(* either Import ssreflect or Import ssreflect.SsrSyntax. *) --(* Part of the contents of this file is technical and will only interest *) --(* advanced developers; in addition the following are defined: *) --(* [the str of v by f] == the Canonical s : str such that f s = v. *) --(* [the str of v] == the Canonical s : str that coerces to v. *) --(* argumentType c == the T such that c : forall x : T, P x. *) --(* returnType c == the R such that c : T -> R. *) --(* {type of c for s} == P s where c : forall x : T, P x. *) --(* phantom T v == singleton type with inhabitant Phantom T v. *) --(* phant T == singleton type with inhabitant Phant v. *) --(* =^~ r == the converse of rewriting rule r (e.g., in a *) --(* rewrite multirule). *) --(* unkeyed t == t, but treated as an unkeyed matching pattern by *) --(* the ssreflect matching algorithm. *) --(* nosimpl t == t, but on the right-hand side of Definition C := *) --(* nosimpl disables expansion of C by /=. *) --(* locked t == t, but locked t is not convertible to t. *) --(* locked_with k t == t, but not convertible to t or locked_with k' t *) --(* unless k = k' (with k : unit). Coq type-checking *) --(* will be much more efficient if locked_with with a *) --(* bespoke k is used for sealed definitions. *) --(* unlockable v == interface for sealed constant definitions of v. *) --(* Unlockable def == the unlockable that registers def : C = v. *) --(* [unlockable of C] == a clone for C of the canonical unlockable for the *) --(* definition of C (e.g., if it uses locked_with). *) --(* [unlockable fun C] == [unlockable of C] with the expansion forced to be *) --(* an explicit lambda expression. *) --(* -> The usage pattern for ADT operations is: *) --(* Definition foo_def x1 .. xn := big_foo_expression. *) --(* Fact foo_key : unit. Proof. by []. Qed. *) --(* Definition foo := locked_with foo_key foo_def. *) --(* Canonical foo_unlockable := [unlockable fun foo]. *) --(* This minimizes the comparison overhead for foo, while still allowing *) --(* rewrite unlock to expose big_foo_expression. *) --(* More information about these definitions and their use can be found in the *) --(* ssreflect manual, and in specific comments below. *) --(******************************************************************************) -- -- --Set Implicit Arguments. --Unset Strict Implicit. --Unset Printing Implicit Defensive. -- --Module SsrSyntax. -- --(* Declare Ssr keywords: 'is' 'of' '//' '/=' and '//='. We also declare the *) --(* parsing level 8, as a workaround for a notation grammar factoring problem. *) --(* Arguments of application-style notations (at level 10) should be declared *) --(* at level 8 rather than 9 or the camlp5 grammar will not factor properly. *) -- --Reserved Notation "(* x 'is' y 'of' z 'isn't' // /= //= *)" (at level 8). --Reserved Notation "(* 69 *)" (at level 69). -- --(* Non ambiguous keyword to check if the SsrSyntax module is imported *) --Reserved Notation "(* Use to test if 'SsrSyntax_is_Imported' *)" (at level 8). -- --Reserved Notation "<hidden n >" (at level 200). --Reserved Notation "T (* n *)" (at level 200, format "T (* n *)"). -- --End SsrSyntax. -- --Export SsrMatchingSyntax. --Export SsrSyntax. -- --(* Make the general "if" into a notation, so that we can override it below. *) --(* The notations are "only parsing" because the Coq decompiler will not *) --(* recognize the expansion of the boolean if; using the default printer *) --(* avoids a spurrious trailing %GEN_IF. *) -- --Delimit Scope general_if_scope with GEN_IF. -- --Notation "'if' c 'then' v1 'else' v2" := -- (if c then v1 else v2) -- (at level 200, c, v1, v2 at level 200, only parsing) : general_if_scope. -- --Notation "'if' c 'return' t 'then' v1 'else' v2" := -- (if c return t then v1 else v2) -- (at level 200, c, t, v1, v2 at level 200, only parsing) : general_if_scope. -- --Notation "'if' c 'as' x 'return' t 'then' v1 'else' v2" := -- (if c as x return t then v1 else v2) -- (at level 200, c, t, v1, v2 at level 200, x ident, only parsing) -- : general_if_scope. -- --(* Force boolean interpretation of simple if expressions. *) -- --Delimit Scope boolean_if_scope with BOOL_IF. -- --Notation "'if' c 'return' t 'then' v1 'else' v2" := -- (if c%bool is true in bool return t then v1 else v2) : boolean_if_scope. -- --Notation "'if' c 'then' v1 'else' v2" := -- (if c%bool is true in bool return _ then v1 else v2) : boolean_if_scope. -- --Notation "'if' c 'as' x 'return' t 'then' v1 'else' v2" := -- (if c%bool is true as x in bool return t then v1 else v2) : boolean_if_scope. -- --Open Scope boolean_if_scope. -- --(* To allow a wider variety of notations without reserving a large number of *) --(* of identifiers, the ssreflect library systematically uses "forms" to *) --(* enclose complex mixfix syntax. A "form" is simply a mixfix expression *) --(* enclosed in square brackets and introduced by a keyword: *) --(* [keyword ... ] *) --(* Because the keyword follows a bracket it does not need to be reserved. *) --(* Non-ssreflect libraries that do not respect the form syntax (e.g., the Coq *) --(* Lists library) should be loaded before ssreflect so that their notations *) --(* do not mask all ssreflect forms. *) --Delimit Scope form_scope with FORM. --Open Scope form_scope. -- --(* Allow overloading of the cast (x : T) syntax, put whitespace around the *) --(* ":" symbol to avoid lexical clashes (and for consistency with the parsing *) --(* precedence of the notation, which binds less tightly than application), *) --(* and put printing boxes that print the type of a long definition on a *) --(* separate line rather than force-fit it at the right margin. *) --Notation "x : T" := (x : T) -- (at level 100, right associativity, -- format "'[hv' x '/ ' : T ']'") : core_scope. -- --(* Allow the casual use of notations like nat * nat for explicit Type *) --(* declarations. Note that (nat * nat : Type) is NOT equivalent to *) --(* (nat * nat)%type, whose inferred type is legacy type "Set". *) --Notation "T : 'Type'" := (T%type : Type) -- (at level 100, only parsing) : core_scope. --(* Allow similarly Prop annotation for, e.g., rewrite multirules. *) --Notation "P : 'Prop'" := (P%type : Prop) -- (at level 100, only parsing) : core_scope. -- --(* Constants for abstract: and [: name ] intro pattern *) --Definition abstract_lock := unit. --Definition abstract_key := tt. -- --Definition abstract (statement : Type) (id : nat) (lock : abstract_lock) := -- let: tt := lock in statement. -- --Notation "<hidden n >" := (abstract _ n _). --Notation "T (* n *)" := (abstract T n abstract_key). -- --(* Constants for tactic-views *) --Inductive external_view : Type := tactic_view of Type. -- --(* Syntax for referring to canonical structures: *) --(* [the struct_type of proj_val by proj_fun] *) --(* This form denotes the Canonical instance s of the Structure type *) --(* struct_type whose proj_fun projection is proj_val, i.e., such that *) --(* proj_fun s = proj_val. *) --(* Typically proj_fun will be A record field accessors of struct_type, but *) --(* this need not be the case; it can be, for instance, a field of a record *) --(* type to which struct_type coerces; proj_val will likewise be coerced to *) --(* the return type of proj_fun. In all but the simplest cases, proj_fun *) --(* should be eta-expanded to allow for the insertion of implicit arguments. *) --(* In the common case where proj_fun itself is a coercion, the "by" part *) --(* can be omitted entirely; in this case it is inferred by casting s to the *) --(* inferred type of proj_val. Obviously the latter can be fixed by using an *) --(* explicit cast on proj_val, and it is highly recommended to do so when the *) --(* return type intended for proj_fun is "Type", as the type inferred for *) --(* proj_val may vary because of sort polymorphism (it could be Set or Prop). *) --(* Note when using the [the _ of _] form to generate a substructure from a *) --(* telescopes-style canonical hierarchy (implementing inheritance with *) --(* coercions), one should always project or coerce the value to the BASE *) --(* structure, because Coq will only find a Canonical derived structure for *) --(* the Canonical base structure -- not for a base structure that is specific *) --(* to proj_value. *) -- --Module TheCanonical. -- --CoInductive put vT sT (v1 v2 : vT) (s : sT) := Put. -- --Definition get vT sT v s (p : @put vT sT v v s) := let: Put _ _ _ := p in s. -- --Definition get_by vT sT of sT -> vT := @get vT sT. -- --End TheCanonical. -- --Import TheCanonical. (* Note: no export. *) -- --Local Arguments get_by _%type_scope _%type_scope _ _ _ _. -- --Notation "[ 'the' sT 'of' v 'by' f ]" := -- (@get_by _ sT f _ _ ((fun v' (s : sT) => Put v' (f s) s) v _)) -- (at level 0, only parsing) : form_scope. -- --Notation "[ 'the' sT 'of' v ]" := (get ((fun s : sT => Put v (*coerce*)s s) _)) -- (at level 0, only parsing) : form_scope. -- --(* The following are "format only" versions of the above notations. Since Coq *) --(* doesn't provide this facility, we fake it by splitting the "the" keyword. *) --(* We need to do this to prevent the formatter from being be thrown off by *) --(* application collapsing, coercion insertion and beta reduction in the right *) --(* hand side of the notations above. *) -- --Notation "[ 'th' 'e' sT 'of' v 'by' f ]" := (@get_by _ sT f v _ _) -- (at level 0, format "[ 'th' 'e' sT 'of' v 'by' f ]") : form_scope. -- --Notation "[ 'th' 'e' sT 'of' v ]" := (@get _ sT v _ _) -- (at level 0, format "[ 'th' 'e' sT 'of' v ]") : form_scope. -- --(* We would like to recognize --Notation "[ 'th' 'e' sT 'of' v : 'Type' ]" := (@get Type sT v _ _) -- (at level 0, format "[ 'th' 'e' sT 'of' v : 'Type' ]") : form_scope. --*) -- --(* Helper notation for canonical structure inheritance support. *) --(* This is a workaround for the poor interaction between delta reduction and *) --(* canonical projections in Coq's unification algorithm, by which transparent *) --(* definitions hide canonical instances, i.e., in *) --(* Canonical a_type_struct := @Struct a_type ... *) --(* Definition my_type := a_type. *) --(* my_type doesn't effectively inherit the struct structure from a_type. Our *) --(* solution is to redeclare the instance as follows *) --(* Canonical my_type_struct := Eval hnf in [struct of my_type]. *) --(* The special notation [str of _] must be defined for each Strucure "str" *) --(* with constructor "Str", typically as follows *) --(* Definition clone_str s := *) --(* let: Str _ x y ... z := s return {type of Str for s} -> str in *) --(* fun k => k _ x y ... z. *) --(* Notation "[ 'str' 'of' T 'for' s ]" := (@clone_str s (@Str T)) *) --(* (at level 0, format "[ 'str' 'of' T 'for' s ]") : form_scope. *) --(* Notation "[ 'str' 'of' T ]" := (repack_str (fun x => @Str T x)) *) --(* (at level 0, format "[ 'str' 'of' T ]") : form_scope. *) --(* The notation for the match return predicate is defined below; the eta *) --(* expansion in the second form serves both to distinguish it from the first *) --(* and to avoid the delta reduction problem. *) --(* There are several variations on the notation and the definition of the *) --(* the "clone" function, for telescopes, mixin classes, and join (multiple *) --(* inheritance) classes. We describe a different idiom for clones in ssrfun; *) --(* it uses phantom types (see below) and static unification; see fintype and *) --(* ssralg for examples. *) -- --Definition argumentType T P & forall x : T, P x := T. --Definition dependentReturnType T P & forall x : T, P x := P. --Definition returnType aT rT & aT -> rT := rT. -- --Notation "{ 'type' 'of' c 'for' s }" := (dependentReturnType c s) -- (at level 0, format "{ 'type' 'of' c 'for' s }") : type_scope. -- --(* A generic "phantom" type (actually, a unit type with a phantom parameter). *) --(* This type can be used for type definitions that require some Structure *) --(* on one of their parameters, to allow Coq to infer said structure so it *) --(* does not have to be supplied explicitly or via the "[the _ of _]" notation *) --(* (the latter interacts poorly with other Notation). *) --(* The definition of a (co)inductive type with a parameter p : p_type, that *) --(* needs to use the operations of a structure *) --(* Structure p_str : Type := p_Str {p_repr :> p_type; p_op : p_repr -> ...} *) --(* should be given as *) --(* Inductive indt_type (p : p_str) := Indt ... . *) --(* Definition indt_of (p : p_str) & phantom p_type p := indt_type p. *) --(* Notation "{ 'indt' p }" := (indt_of (Phantom p)). *) --(* Definition indt p x y ... z : {indt p} := @Indt p x y ... z. *) --(* Notation "[ 'indt' x y ... z ]" := (indt x y ... z). *) --(* That is, the concrete type and its constructor should be shadowed by *) --(* definitions that use a phantom argument to infer and display the true *) --(* value of p (in practice, the "indt" constructor often performs additional *) --(* functions, like "locking" the representation -- see below). *) --(* We also define a simpler version ("phant" / "Phant") of phantom for the *) --(* common case where p_type is Type. *) -- --CoInductive phantom T (p : T) := Phantom. --Arguments phantom : clear implicits. --Arguments Phantom : clear implicits. --CoInductive phant (p : Type) := Phant. -- --(* Internal tagging used by the implementation of the ssreflect elim. *) -- --Definition protect_term (A : Type) (x : A) : A := x. -- --(* The ssreflect idiom for a non-keyed pattern: *) --(* - unkeyed t wiil match any subterm that unifies with t, regardless of *) --(* whether it displays the same head symbol as t. *) --(* - unkeyed t a b will match any application of a term f unifying with t, *) --(* to two arguments unifying with with a and b, repectively, regardless of *) --(* apparent head symbols. *) --(* - unkeyed x where x is a variable will match any subterm with the same *) --(* type as x (when x would raise the 'indeterminate pattern' error). *) -- --Notation unkeyed x := (let flex := x in flex). -- --(* Ssreflect converse rewrite rule rule idiom. *) --Definition ssr_converse R (r : R) := (Logic.I, r). --Notation "=^~ r" := (ssr_converse r) (at level 100) : form_scope. -- --(* Term tagging (user-level). *) --(* The ssreflect library uses four strengths of term tagging to restrict *) --(* convertibility during type checking: *) --(* nosimpl t simplifies to t EXCEPT in a definition; more precisely, given *) --(* Definition foo := nosimpl bar, foo (or foo t') will NOT be expanded by *) --(* the /= and //= switches unless it is in a forcing context (e.g., in *) --(* match foo t' with ... end, foo t' will be reduced if this allows the *) --(* match to be reduced). Note that nosimpl bar is simply notation for a *) --(* a term that beta-iota reduces to bar; hence rewrite /foo will replace *) --(* foo by bar, and rewrite -/foo will replace bar by foo. *) --(* CAVEAT: nosimpl should not be used inside a Section, because the end of *) --(* section "cooking" removes the iota redex. *) --(* locked t is provably equal to t, but is not convertible to t; 'locked' *) --(* provides support for selective rewriting, via the lock t : t = locked t *) --(* Lemma, and the ssreflect unlock tactic. *) --(* locked_with k t is equal but not convertible to t, much like locked t, *) --(* but supports explicit tagging with a value k : unit. This is used to *) --(* mitigate a flaw in the term comparison heuristic of the Coq kernel, *) --(* which treats all terms of the form locked t as equal and conpares their *) --(* arguments recursively, leading to an exponential blowup of comparison. *) --(* For this reason locked_with should be used rather than locked when *) --(* defining ADT operations. The unlock tactic does not support locked_with *) --(* but the unlock rewrite rule does, via the unlockable interface. *) --(* we also use Module Type ascription to create truly opaque constants, *) --(* because simple expansion of constants to reveal an unreducible term *) --(* doubles the time complexity of a negative comparison. Such opaque *) --(* constants can be expanded generically with the unlock rewrite rule. *) --(* See the definition of card and subset in fintype for examples of this. *) -- --Notation nosimpl t := (let: tt := tt in t). -- --Lemma master_key : unit. Proof. exact tt. Qed. --Definition locked A := let: tt := master_key in fun x : A => x. -- --Lemma lock A x : x = locked x :> A. Proof. unlock; reflexivity. Qed. -- --(* Needed for locked predicates, in particular for eqType's. *) --Lemma not_locked_false_eq_true : locked false <> true. --Proof. unlock; discriminate. Qed. -- --(* The basic closing tactic "done". *) --Ltac done := -- trivial; hnf; intros; solve -- [ do ![solve [trivial | apply: sym_equal; trivial] -- | discriminate | contradiction | split] -- | case not_locked_false_eq_true; assumption -- | match goal with H : ~ _ |- _ => solve [case H; trivial] end ]. -- --(* Quicker done tactic not including split, syntax: /0/ *) --Ltac ssrdone0 := -- trivial; hnf; intros; solve -- [ do ![solve [trivial | apply: sym_equal; trivial] -- | discriminate | contradiction ] -- | case not_locked_false_eq_true; assumption -- | match goal with H : ~ _ |- _ => solve [case H; trivial] end ]. -- --(* To unlock opaque constants. *) --Structure unlockable T v := Unlockable {unlocked : T; _ : unlocked = v}. --Lemma unlock T x C : @unlocked T x C = x. Proof. by case: C. Qed. -- --Notation "[ 'unlockable' 'of' C ]" := (@Unlockable _ _ C (unlock _)) -- (at level 0, format "[ 'unlockable' 'of' C ]") : form_scope. -- --Notation "[ 'unlockable' 'fun' C ]" := (@Unlockable _ (fun _ => _) C (unlock _)) -- (at level 0, format "[ 'unlockable' 'fun' C ]") : form_scope. -- --(* Generic keyed constant locking. *) -- --(* The argument order ensures that k is always compared before T. *) --Definition locked_with k := let: tt := k in fun T x => x : T. -- --(* This can be used as a cheap alternative to cloning the unlockable instance *) --(* below, but with caution as unkeyed matching can be expensive. *) --Lemma locked_withE T k x : unkeyed (locked_with k x) = x :> T. --Proof. by case: k. Qed. -- --(* Intensionaly, this instance will not apply to locked u. *) --Canonical locked_with_unlockable T k x := -- @Unlockable T x (locked_with k x) (locked_withE k x). -- --(* More accurate variant of unlock, and safer alternative to locked_withE. *) --Lemma unlock_with T k x : unlocked (locked_with_unlockable k x) = x :> T. --Proof. exact: unlock. Qed. -- --(* The internal lemmas for the have tactics. *) -- --Definition ssr_have Plemma Pgoal (step : Plemma) rest : Pgoal := rest step. --Arguments ssr_have Plemma [Pgoal]. -- --Definition ssr_have_let Pgoal Plemma step -- (rest : let x : Plemma := step in Pgoal) : Pgoal := rest. --Arguments ssr_have_let [Pgoal]. -- --Definition ssr_suff Plemma Pgoal step (rest : Plemma) : Pgoal := step rest. --Arguments ssr_suff Plemma [Pgoal]. -- --Definition ssr_wlog := ssr_suff. --Arguments ssr_wlog Plemma [Pgoal]. -- --(* Internal N-ary congruence lemmas for the congr tactic. *) -- --Fixpoint nary_congruence_statement (n : nat) -- : (forall B, (B -> B -> Prop) -> Prop) -> Prop := -- match n with -- | O => fun k => forall B, k B (fun x1 x2 : B => x1 = x2) -- | S n' => -- let k' A B e (f1 f2 : A -> B) := -- forall x1 x2, x1 = x2 -> (e (f1 x1) (f2 x2) : Prop) in -- fun k => forall A, nary_congruence_statement n' (fun B e => k _ (k' A B e)) -- end. -- --Lemma nary_congruence n (k := fun B e => forall y : B, (e y y : Prop)) : -- nary_congruence_statement n k. --Proof. --have: k _ _ := _; rewrite {1}/k. --elim: n k => [|n IHn] k k_P /= A; first exact: k_P. --by apply: IHn => B e He; apply: k_P => f x1 x2 <-. --Qed. -- --Lemma ssr_congr_arrow Plemma Pgoal : Plemma = Pgoal -> Plemma -> Pgoal. --Proof. by move->. Qed. --Arguments ssr_congr_arrow : clear implicits. -- --(* View lemmas that don't use reflection. *) -- --Section ApplyIff. -- --Variables P Q : Prop. --Hypothesis eqPQ : P <-> Q. -- --Lemma iffLR : P -> Q. Proof. by case: eqPQ. Qed. --Lemma iffRL : Q -> P. Proof. by case: eqPQ. Qed. -- --Lemma iffLRn : ~P -> ~Q. Proof. by move=> nP tQ; case: nP; case: eqPQ tQ. Qed. --Lemma iffRLn : ~Q -> ~P. Proof. by move=> nQ tP; case: nQ; case: eqPQ tP. Qed. -- --End ApplyIff. -- --Hint View for move/ iffLRn|2 iffRLn|2 iffLR|2 iffRL|2. --Hint View for apply/ iffRLn|2 iffLRn|2 iffRL|2 iffLR|2. -- --(* To focus non-ssreflect tactics on a subterm, eg vm_compute. *) --(* Usage: *) --(* elim/abstract_context: (pattern) => G defG. *) --(* vm_compute; rewrite {}defG {G}. *) --(* Note that vm_cast are not stored in the proof term *) --(* for reductions occuring in the context, hence *) --(* set here := pattern; vm_compute in (value of here) *) --(* blows up at Qed time. *) --Lemma abstract_context T (P : T -> Type) x : -- (forall Q, Q = P -> Q x) -> P x. --Proof. by move=> /(_ P); apply. Qed. ---- a/plugins/ssr/ssrbool.v -+++ /dev/null -@@ -1,1873 +0,0 @@ --(************************************************************************) --(* * The Coq Proof Assistant / The Coq Development Team *) --(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) --(* <O___,, * (see CREDITS file for the list of authors) *) --(* \VV/ **************************************************************) --(* // * This file is distributed under the terms of the *) --(* * GNU Lesser General Public License Version 2.1 *) --(* * (see LICENSE file for the text of the license) *) --(************************************************************************) -- --(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -- --Require Bool. --Require Import ssreflect ssrfun. -- --(******************************************************************************) --(* A theory of boolean predicates and operators. A large part of this file is *) --(* concerned with boolean reflection. *) --(* Definitions and notations: *) --(* is_true b == the coercion of b : bool to Prop (:= b = true). *) --(* This is just input and displayed as `b''. *) --(* reflect P b == the reflection inductive predicate, asserting *) --(* that the logical proposition P : prop with the *) --(* formula b : bool. Lemmas asserting reflect P b *) --(* are often referred to as "views". *) --(* iffP, appP, sameP, rwP :: lemmas for direct manipulation of reflection *) --(* views: iffP is used to prove reflection from *) --(* logical equivalence, appP to compose views, and *) --(* sameP and rwP to perform boolean and setoid *) --(* rewriting. *) --(* elimT :: coercion reflect >-> Funclass, which allows the *) --(* direct application of `reflect' views to *) --(* boolean assertions. *) --(* decidable P <-> P is effectively decidable (:= {P} + {~ P}. *) --(* contra, contraL, ... :: contraposition lemmas. *) --(* altP my_viewP :: natural alternative for reflection; given *) --(* lemma myviewP: reflect my_Prop my_formula, *) --(* have [myP | not_myP] := altP my_viewP. *) --(* generates two subgoals, in which my_formula has *) --(* been replaced by true and false, resp., with *) --(* new assumptions myP : my_Prop and *) --(* not_myP: ~~ my_formula. *) --(* Caveat: my_formula must be an APPLICATION, not *) --(* a variable, constant, let-in, etc. (due to the *) --(* poor behaviour of dependent index matching). *) --(* boolP my_formula :: boolean disjunction, equivalent to *) --(* altP (idP my_formula) but circumventing the *) --(* dependent index capture issue; destructing *) --(* boolP my_formula generates two subgoals with *) --(* assumtions my_formula and ~~ myformula. As *) --(* with altP, my_formula must be an application. *) --(* \unless C, P <-> we can assume property P when a something that *) --(* holds under condition C (such as C itself). *) --(* := forall G : Prop, (C -> G) -> (P -> G) -> G. *) --(* This is just C \/ P or rather its impredicative *) --(* encoding, whose usage better fits the above *) --(* description: given a lemma UCP whose conclusion *) --(* is \unless C, P we can assume P by writing: *) --(* wlog hP: / P by apply/UCP; (prove C -> goal). *) --(* or even apply: UCP id _ => hP if the goal is C. *) --(* classically P <-> we can assume P when proving is_true b. *) --(* := forall b : bool, (P -> b) -> b. *) --(* This is equivalent to ~ (~ P) when P : Prop. *) --(* implies P Q == wrapper coinductive type that coerces to P -> Q *) --(* and can be used as a P -> Q view unambigously. *) --(* Useful to avoid spurious insertion of <-> views *) --(* when Q is a conjunction of foralls, as in Lemma *) --(* all_and2 below; conversely, avoids confusion in *) --(* apply views for impredicative properties, such *) --(* as \unless C, P. Also supports contrapositives. *) --(* a && b == the boolean conjunction of a and b. *) --(* a || b == the boolean disjunction of a and b. *) --(* a ==> b == the boolean implication of b by a. *) --(* ~~ a == the boolean negation of a. *) --(* a (+) b == the boolean exclusive or (or sum) of a and b. *) --(* [ /\ P1 , P2 & P3 ] == multiway logical conjunction, up to 5 terms. *) --(* [ \/ P1 , P2 | P3 ] == multiway logical disjunction, up to 4 terms. *) --(* [&& a, b, c & d] == iterated, right associative boolean conjunction *) --(* with arbitrary arity. *) --(* [|| a, b, c | d] == iterated, right associative boolean disjunction *) --(* with arbitrary arity. *) --(* [==> a, b, c => d] == iterated, right associative boolean implication *) --(* with arbitrary arity. *) --(* and3P, ... == specific reflection lemmas for iterated *) --(* connectives. *) --(* andTb, orbAC, ... == systematic names for boolean connective *) --(* properties (see suffix conventions below). *) --(* prop_congr == a tactic to move a boolean equality from *) --(* its coerced form in Prop to the equality *) --(* in bool. *) --(* bool_congr == resolution tactic for blindly weeding out *) --(* like terms from boolean equalities (can fail). *) --(* This file provides a theory of boolean predicates and relations: *) --(* pred T == the type of bool predicates (:= T -> bool). *) --(* simpl_pred T == the type of simplifying bool predicates, using *) --(* the simpl_fun from ssrfun.v. *) --(* rel T == the type of bool relations. *) --(* := T -> pred T or T -> T -> bool. *) --(* simpl_rel T == type of simplifying relations. *) --(* predType == the generic predicate interface, supported for *) --(* for lists and sets. *) --(* pred_class == a coercion class for the predType projection to *) --(* pred; declaring a coercion to pred_class is an *) --(* alternative way of equipping a type with a *) --(* predType structure, which interoperates better *) --(* with coercion subtyping. This is used, e.g., *) --(* for finite sets, so that finite groups inherit *) --(* the membership operation by coercing to sets. *) --(* If P is a predicate the proposition "x satisfies P" can be written *) --(* applicatively as (P x), or using an explicit connective as (x \in P); in *) --(* the latter case we say that P is a "collective" predicate. We use A, B *) --(* rather than P, Q for collective predicates: *) --(* x \in A == x satisfies the (collective) predicate A. *) --(* x \notin A == x doesn't satisfy the (collective) predicate A. *) --(* The pred T type can be used as a generic predicate type for either kind, *) --(* but the two kinds of predicates should not be confused. When a "generic" *) --(* pred T value of one type needs to be passed as the other the following *) --(* conversions should be used explicitly: *) --(* SimplPred P == a (simplifying) applicative equivalent of P. *) --(* mem A == an applicative equivalent of A: *) --(* mem A x simplifies to x \in A. *) --(* Alternatively one can use the syntax for explicit simplifying predicates *) --(* and relations (in the following x is bound in E): *) --(* [pred x | E] == simplifying (see ssrfun) predicate x => E. *) --(* [pred x : T | E] == predicate x => E, with a cast on the argument. *) --(* [pred : T | P] == constant predicate P on type T. *) --(* [pred x | E1 & E2] == [pred x | E1 && E2]; an x : T cast is allowed. *) --(* [pred x in A] == [pred x | x in A]. *) --(* [pred x in A | E] == [pred x | x in A & E]. *) --(* [pred x in A | E1 & E2] == [pred x in A | E1 && E2]. *) --(* [predU A & B] == union of two collective predicates A and B. *) --(* [predI A & B] == intersection of collective predicates A and B. *) --(* [predD A & B] == difference of collective predicates A and B. *) --(* [predC A] == complement of the collective predicate A. *) --(* [preim f of A] == preimage under f of the collective predicate A. *) --(* predU P Q, ... == union, etc of applicative predicates. *) --(* pred0 == the empty predicate. *) --(* predT == the total (always true) predicate. *) --(* if T : predArgType, then T coerces to predT. *) --(* {: T} == T cast to predArgType (e.g., {: bool * nat}) *) --(* In the following, x and y are bound in E: *) --(* [rel x y | E] == simplifying relation x, y => E. *) --(* [rel x y : T | E] == simplifying relation with arguments cast. *) --(* [rel x y in A & B | E] == [rel x y | [&& x \in A, y \in B & E]]. *) --(* [rel x y in A & B] == [rel x y | (x \in A) && (y \in B)]. *) --(* [rel x y in A | E] == [rel x y in A & A | E]. *) --(* [rel x y in A] == [rel x y in A & A]. *) --(* relU R S == union of relations R and S. *) --(* Explicit values of type pred T (i.e., lamdba terms) should always be used *) --(* applicatively, while values of collection types implementing the predType *) --(* interface, such as sequences or sets should always be used as collective *) --(* predicates. Defined constants and functions of type pred T or simpl_pred T *) --(* as well as the explicit simpl_pred T values described below, can generally *) --(* be used either way. Note however that x \in A will not auto-simplify when *) --(* A is an explicit simpl_pred T value; the generic simplification rule inE *) --(* must be used (when A : pred T, the unfold_in rule can be used). Constants *) --(* of type pred T with an explicit simpl_pred value do not auto-simplify when *) --(* used applicatively, but can still be expanded with inE. This behavior can *) --(* be controlled as follows: *) --(* Let A : collective_pred T := [pred x | ... ]. *) --(* The collective_pred T type is just an alias for pred T, but this cast *) --(* stops rewrite inE from expanding the definition of A, thus treating A *) --(* into an abstract collection (unfold_in or in_collective can be used to *) --(* expand manually). *) --(* Let A : applicative_pred T := [pred x | ...]. *) --(* This cast causes inE to turn x \in A into the applicative A x form; *) --(* A will then have to unfolded explicitly with the /A rule. This will *) --(* also apply to any definition that reduces to A (e.g., Let B := A). *) --(* Canonical A_app_pred := ApplicativePred A. *) --(* This declaration, given after definition of A, similarly causes inE to *) --(* turn x \in A into A x, but in addition allows the app_predE rule to *) --(* turn A x back into x \in A; it can be used for any definition of type *) --(* pred T, which makes it especially useful for ambivalent predicates *) --(* as the relational transitive closure connect, that are used in both *) --(* applicative and collective styles. *) --(* Purely for aesthetics, we provide a subtype of collective predicates: *) --(* qualifier q T == a pred T pretty-printing wrapper. An A : qualifier q T *) --(* coerces to pred_class and thus behaves as a collective *) --(* predicate, but x \in A and x \notin A are displayed as: *) --(* x \is A and x \isn't A when q = 0, *) --(* x \is a A and x \isn't a A when q = 1, *) --(* x \is an A and x \isn't an A when q = 2, respectively. *) --(* [qualify x | P] := Qualifier 0 (fun x => P), constructor for the above. *) --(* [qualify x : T | P], [qualify a x | P], [qualify an X | P], etc. *) --(* variants of the above with type constraints and different *) --(* values of q. *) --(* We provide an internal interface to support attaching properties (such as *) --(* being multiplicative) to predicates: *) --(* pred_key p == phantom type that will serve as a support for properties *) --(* to be attached to p : pred_class; instances should be *) --(* created with Fact/Qed so as to be opaque. *) --(* KeyedPred k_p == an instance of the interface structure that attaches *) --(* (k_p : pred_key P) to P; the structure projection is a *) --(* coercion to pred_class. *) --(* KeyedQualifier k_q == an instance of the interface structure that attaches *) --(* (k_q : pred_key q) to (q : qualifier n T). *) --(* DefaultPredKey p == a default value for pred_key p; the vernacular command *) --(* Import DefaultKeying attaches this key to all predicates *) --(* that are not explicitly keyed. *) --(* Keys can be used to attach properties to predicates, qualifiers and *) --(* generic nouns in a way that allows them to be used transparently. The key *) --(* projection of a predicate property structure such as unsignedPred should *) --(* be a pred_key, not a pred, and corresponding lemmas will have the form *) --(* Lemma rpredN R S (oppS : @opprPred R S) (kS : keyed_pred oppS) : *) --(* {mono -%R: x / x \in kS}. *) --(* Because x \in kS will be displayed as x \in S (or x \is S, etc), the *) --(* canonical instance of opprPred will not normally be exposed (it will also *) --(* be erased by /= simplification). In addition each predicate structure *) --(* should have a DefaultPredKey Canonical instance that simply issues the *) --(* property as a proof obligation (which can be caught by the Prop-irrelevant *) --(* feature of the ssreflect plugin). *) --(* Some properties of predicates and relations: *) --(* A =i B <-> A and B are extensionally equivalent. *) --(* {subset A <= B} <-> A is a (collective) subpredicate of B. *) --(* subpred P Q <-> P is an (applicative) subpredicate or Q. *) --(* subrel R S <-> R is a subrelation of S. *) --(* In the following R is in rel T: *) --(* reflexive R <-> R is reflexive. *) --(* irreflexive R <-> R is irreflexive. *) --(* symmetric R <-> R (in rel T) is symmetric (equation). *) --(* pre_symmetric R <-> R is symmetric (implication). *) --(* antisymmetric R <-> R is antisymmetric. *) --(* total R <-> R is total. *) --(* transitive R <-> R is transitive. *) --(* left_transitive R <-> R is a congruence on its left hand side. *) --(* right_transitive R <-> R is a congruence on its right hand side. *) --(* equivalence_rel R <-> R is an equivalence relation. *) --(* Localization of (Prop) predicates; if P1 is convertible to forall x, Qx, *) --(* P2 to forall x y, Qxy and P3 to forall x y z, Qxyz : *) --(* {for y, P1} <-> Qx{y / x}. *) --(* {in A, P1} <-> forall x, x \in A -> Qx. *) --(* {in A1 & A2, P2} <-> forall x y, x \in A1 -> y \in A2 -> Qxy. *) --(* {in A &, P2} <-> forall x y, x \in A -> y \in A -> Qxy. *) --(* {in A1 & A2 & A3, Q3} <-> forall x y z, *) --(* x \in A1 -> y \in A2 -> z \in A3 -> Qxyz. *) --(* {in A1 & A2 &, Q3} == {in A1 & A2 & A2, Q3}. *) --(* {in A1 && A3, Q3} == {in A1 & A1 & A3, Q3}. *) --(* {in A &&, Q3} == {in A & A & A, Q3}. *) --(* {in A, bijective f} == f has a right inverse in A. *) --(* {on C, P1} == forall x, (f x) \in C -> Qx *) --(* when P1 is also convertible to Pf f. *) --(* {on C &, P2} == forall x y, f x \in C -> f y \in C -> Qxy *) --(* when P2 is also convertible to Pf f. *) --(* {on C, P1' & g} == forall x, (f x) \in cd -> Qx *) --(* when P1' is convertible to Pf f *) --(* and P1' g is convertible to forall x, Qx. *) --(* {on C, bijective f} == f has a right inverse on C. *) --(* This file extends the lemma name suffix conventions of ssrfun as follows: *) --(* A -- associativity, as in andbA : associative andb. *) --(* AC -- right commutativity. *) --(* ACA -- self-interchange (inner commutativity), e.g., *) --(* orbACA : (a || b) || (c || d) = (a || c) || (b || d). *) --(* b -- a boolean argument, as in andbb : idempotent andb. *) --(* C -- commutativity, as in andbC : commutative andb, *) --(* or predicate complement, as in predC. *) --(* CA -- left commutativity. *) --(* D -- predicate difference, as in predD. *) --(* E -- elimination, as in negbFE : ~~ b = false -> b. *) --(* F or f -- boolean false, as in andbF : b && false = false. *) --(* I -- left/right injectivity, as in addbI : right_injective addb, *) --(* or predicate intersection, as in predI. *) --(* l -- a left-hand operation, as andb_orl : left_distributive andb orb. *) --(* N or n -- boolean negation, as in andbN : a && (~~ a) = false. *) --(* P -- a characteristic property, often a reflection lemma, as in *) --(* andP : reflect (a /\ b) (a && b). *) --(* r -- a right-hand operation, as orb_andr : rightt_distributive orb andb. *) --(* T or t -- boolean truth, as in andbT: right_id true andb. *) --(* U -- predicate union, as in predU. *) --(* W -- weakening, as in in1W : {in D, forall x, P} -> forall x, P. *) --(******************************************************************************) -- --Set Implicit Arguments. --Unset Strict Implicit. --Unset Printing Implicit Defensive. --Set Warnings "-projection-no-head-constant". -- --Notation reflect := Bool.reflect. --Notation ReflectT := Bool.ReflectT. --Notation ReflectF := Bool.ReflectF. -- --Reserved Notation "~~ b" (at level 35, right associativity). --Reserved Notation "b ==> c" (at level 55, right associativity). --Reserved Notation "b1 (+) b2" (at level 50, left associativity). --Reserved Notation "x \in A" -- (at level 70, format "'[hv' x '/ ' \in A ']'", no associativity). --Reserved Notation "x \notin A" -- (at level 70, format "'[hv' x '/ ' \notin A ']'", no associativity). --Reserved Notation "p1 =i p2" -- (at level 70, format "'[hv' p1 '/ ' =i p2 ']'", no associativity). -- --(* We introduce a number of n-ary "list-style" notations that share a common *) --(* format, namely *) --(* [op arg1, arg2, ... last_separator last_arg] *) --(* This usually denotes a right-associative applications of op, e.g., *) --(* [&& a, b, c & d] denotes a && (b && (c && d)) *) --(* The last_separator must be a non-operator token. Here we use &, | or =>; *) --(* our default is &, but we try to match the intended meaning of op. The *) --(* separator is a workaround for limitations of the parsing engine; the same *) --(* limitations mean the separator cannot be omitted even when last_arg can. *) --(* The Notation declarations are complicated by the separate treatment for *) --(* some fixed arities (binary for bool operators, and all arities for Prop *) --(* operators). *) --(* We also use the square brackets in comprehension-style notations *) --(* [type var separator expr] *) --(* where "type" is the type of the comprehension (e.g., pred) and "separator" *) --(* is | or => . It is important that in other notations a leading square *) --(* bracket [ is always followed by an operator symbol or a fixed identifier. *) -- --Reserved Notation "[ /\ P1 & P2 ]" (at level 0, only parsing). --Reserved Notation "[ /\ P1 , P2 & P3 ]" (at level 0, format -- "'[hv' [ /\ '[' P1 , '/' P2 ']' '/ ' & P3 ] ']'"). --Reserved Notation "[ /\ P1 , P2 , P3 & P4 ]" (at level 0, format -- "'[hv' [ /\ '[' P1 , '/' P2 , '/' P3 ']' '/ ' & P4 ] ']'"). --Reserved Notation "[ /\ P1 , P2 , P3 , P4 & P5 ]" (at level 0, format -- "'[hv' [ /\ '[' P1 , '/' P2 , '/' P3 , '/' P4 ']' '/ ' & P5 ] ']'"). -- --Reserved Notation "[ \/ P1 | P2 ]" (at level 0, only parsing). --Reserved Notation "[ \/ P1 , P2 | P3 ]" (at level 0, format -- "'[hv' [ \/ '[' P1 , '/' P2 ']' '/ ' | P3 ] ']'"). --Reserved Notation "[ \/ P1 , P2 , P3 | P4 ]" (at level 0, format -- "'[hv' [ \/ '[' P1 , '/' P2 , '/' P3 ']' '/ ' | P4 ] ']'"). -- --Reserved Notation "[ && b1 & c ]" (at level 0, only parsing). --Reserved Notation "[ && b1 , b2 , .. , bn & c ]" (at level 0, format -- "'[hv' [ && '[' b1 , '/' b2 , '/' .. , '/' bn ']' '/ ' & c ] ']'"). -- --Reserved Notation "[ || b1 | c ]" (at level 0, only parsing). --Reserved Notation "[ || b1 , b2 , .. , bn | c ]" (at level 0, format -- "'[hv' [ || '[' b1 , '/' b2 , '/' .. , '/' bn ']' '/ ' | c ] ']'"). -- --Reserved Notation "[ ==> b1 => c ]" (at level 0, only parsing). --Reserved Notation "[ ==> b1 , b2 , .. , bn => c ]" (at level 0, format -- "'[hv' [ ==> '[' b1 , '/' b2 , '/' .. , '/' bn ']' '/' => c ] ']'"). -- --Reserved Notation "[ 'pred' : T => E ]" (at level 0, format -- "'[hv' [ 'pred' : T => '/ ' E ] ']'"). --Reserved Notation "[ 'pred' x => E ]" (at level 0, x at level 8, format -- "'[hv' [ 'pred' x => '/ ' E ] ']'"). --Reserved Notation "[ 'pred' x : T => E ]" (at level 0, x at level 8, format -- "'[hv' [ 'pred' x : T => '/ ' E ] ']'"). -- --Reserved Notation "[ 'rel' x y => E ]" (at level 0, x, y at level 8, format -- "'[hv' [ 'rel' x y => '/ ' E ] ']'"). --Reserved Notation "[ 'rel' x y : T => E ]" (at level 0, x, y at level 8, format -- "'[hv' [ 'rel' x y : T => '/ ' E ] ']'"). -- --(* Shorter delimiter *) --Delimit Scope bool_scope with B. --Open Scope bool_scope. -- --(* An alternative to xorb that behaves somewhat better wrt simplification. *) --Definition addb b := if b then negb else id. -- --(* Notation for && and || is declared in Init.Datatypes. *) --Notation "~~ b" := (negb b) : bool_scope. --Notation "b ==> c" := (implb b c) : bool_scope. --Notation "b1 (+) b2" := (addb b1 b2) : bool_scope. -- --(* Constant is_true b := b = true is defined in Init.Datatypes. *) --Coercion is_true : bool >-> Sortclass. (* Prop *) -- --Lemma prop_congr : forall b b' : bool, b = b' -> b = b' :> Prop. --Proof. by move=> b b' ->. Qed. -- --Ltac prop_congr := apply: prop_congr. -- --(* Lemmas for trivial. *) --Lemma is_true_true : true. Proof. by []. Qed. --Lemma not_false_is_true : ~ false. Proof. by []. Qed. --Lemma is_true_locked_true : locked true. Proof. by unlock. Qed. --Hint Resolve is_true_true not_false_is_true is_true_locked_true. -- --(* Shorter names. *) --Definition isT := is_true_true. --Definition notF := not_false_is_true. -- --(* Negation lemmas. *) -- --(* We generally take NEGATION as the standard form of a false condition: *) --(* negative boolean hypotheses should be of the form ~~ b, rather than ~ b or *) --(* b = false, as much as possible. *) -- --Lemma negbT b : b = false -> ~~ b. Proof. by case: b. Qed. --Lemma negbTE b : ~~ b -> b = false. Proof. by case: b. Qed. --Lemma negbF b : (b : bool) -> ~~ b = false. Proof. by case: b. Qed. --Lemma negbFE b : ~~ b = false -> b. Proof. by case: b. Qed. --Lemma negbK : involutive negb. Proof. by case. Qed. --Lemma negbNE b : ~~ ~~ b -> b. Proof. by case: b. Qed. -- --Lemma negb_inj : injective negb. Proof. exact: can_inj negbK. Qed. --Lemma negbLR b c : b = ~~ c -> ~~ b = c. Proof. exact: canLR negbK. Qed. --Lemma negbRL b c : ~~ b = c -> b = ~~ c. Proof. exact: canRL negbK. Qed. -- --Lemma contra (c b : bool) : (c -> b) -> ~~ b -> ~~ c. --Proof. by case: b => //; case: c. Qed. --Definition contraNN := contra. -- --Lemma contraL (c b : bool) : (c -> ~~ b) -> b -> ~~ c. --Proof. by case: b => //; case: c. Qed. --Definition contraTN := contraL. -- --Lemma contraR (c b : bool) : (~~ c -> b) -> ~~ b -> c. --Proof. by case: b => //; case: c. Qed. --Definition contraNT := contraR. -- --Lemma contraLR (c b : bool) : (~~ c -> ~~ b) -> b -> c. --Proof. by case: b => //; case: c. Qed. --Definition contraTT := contraLR. -- --Lemma contraT b : (~~ b -> false) -> b. Proof. by case: b => // ->. Qed. -- --Lemma wlog_neg b : (~~ b -> b) -> b. Proof. by case: b => // ->. Qed. -- --Lemma contraFT (c b : bool) : (~~ c -> b) -> b = false -> c. --Proof. by move/contraR=> notb_c /negbT. Qed. -- --Lemma contraFN (c b : bool) : (c -> b) -> b = false -> ~~ c. --Proof. by move/contra=> notb_notc /negbT. Qed. -- --Lemma contraTF (c b : bool) : (c -> ~~ b) -> b -> c = false. --Proof. by move/contraL=> b_notc /b_notc/negbTE. Qed. -- --Lemma contraNF (c b : bool) : (c -> b) -> ~~ b -> c = false. --Proof. by move/contra=> notb_notc /notb_notc/negbTE. Qed. -- --Lemma contraFF (c b : bool) : (c -> b) -> b = false -> c = false. --Proof. by move/contraFN=> bF_notc /bF_notc/negbTE. Qed. -- --(* Coercion of sum-style datatypes into bool, which makes it possible *) --(* to use ssr's boolean if rather than Coq's "generic" if. *) -- --Coercion isSome T (u : option T) := if u is Some _ then true else false. -- --Coercion is_inl A B (u : A + B) := if u is inl _ then true else false. -- --Coercion is_left A B (u : {A} + {B}) := if u is left _ then true else false. -- --Coercion is_inleft A B (u : A + {B}) := if u is inleft _ then true else false. -- --Prenex Implicits isSome is_inl is_left is_inleft. -- --Definition decidable P := {P} + {~ P}. -- --(* Lemmas for ifs with large conditions, which allow reasoning about the *) --(* condition without repeating it inside the proof (the latter IS *) --(* preferable when the condition is short). *) --(* Usage : *) --(* if the goal contains (if cond then ...) = ... *) --(* case: ifP => Hcond. *) --(* generates two subgoal, with the assumption Hcond : cond = true/false *) --(* Rewrite if_same eliminates redundant ifs *) --(* Rewrite (fun_if f) moves a function f inside an if *) --(* Rewrite if_arg moves an argument inside a function-valued if *) -- --Section BoolIf. -- --Variables (A B : Type) (x : A) (f : A -> B) (b : bool) (vT vF : A). -- --CoInductive if_spec (not_b : Prop) : bool -> A -> Set := -- | IfSpecTrue of b : if_spec not_b true vT -- | IfSpecFalse of not_b : if_spec not_b false vF. -- --Lemma ifP : if_spec (b = false) b (if b then vT else vF). --Proof. by case def_b: b; constructor. Qed. -- --Lemma ifPn : if_spec (~~ b) b (if b then vT else vF). --Proof. by case def_b: b; constructor; rewrite ?def_b. Qed. -- --Lemma ifT : b -> (if b then vT else vF) = vT. Proof. by move->. Qed. --Lemma ifF : b = false -> (if b then vT else vF) = vF. Proof. by move->. Qed. --Lemma ifN : ~~ b -> (if b then vT else vF) = vF. Proof. by move/negbTE->. Qed. -- --Lemma if_same : (if b then vT else vT) = vT. --Proof. by case b. Qed. -- --Lemma if_neg : (if ~~ b then vT else vF) = if b then vF else vT. --Proof. by case b. Qed. -- --Lemma fun_if : f (if b then vT else vF) = if b then f vT else f vF. --Proof. by case b. Qed. -- --Lemma if_arg (fT fF : A -> B) : -- (if b then fT else fF) x = if b then fT x else fF x. --Proof. by case b. Qed. -- --(* Turning a boolean "if" form into an application. *) --Definition if_expr := if b then vT else vF. --Lemma ifE : (if b then vT else vF) = if_expr. Proof. by []. Qed. -- --End BoolIf. -- --(* Core (internal) reflection lemmas, used for the three kinds of views. *) -- --Section ReflectCore. -- --Variables (P Q : Prop) (b c : bool). -- --Hypothesis Hb : reflect P b. -- --Lemma introNTF : (if c then ~ P else P) -> ~~ b = c. --Proof. by case c; case Hb. Qed. -- --Lemma introTF : (if c then P else ~ P) -> b = c. --Proof. by case c; case Hb. Qed. -- --Lemma elimNTF : ~~ b = c -> if c then ~ P else P. --Proof. by move <-; case Hb. Qed. -- --Lemma elimTF : b = c -> if c then P else ~ P. --Proof. by move <-; case Hb. Qed. -- --Lemma equivPif : (Q -> P) -> (P -> Q) -> if b then Q else ~ Q. --Proof. by case Hb; auto. Qed. -- --Lemma xorPif : Q \/ P -> ~ (Q /\ P) -> if b then ~ Q else Q. --Proof. by case Hb => [? _ H ? | ? H _]; case: H. Qed. -- --End ReflectCore. -- --(* Internal negated reflection lemmas *) --Section ReflectNegCore. -- --Variables (P Q : Prop) (b c : bool). --Hypothesis Hb : reflect P (~~ b). -- --Lemma introTFn : (if c then ~ P else P) -> b = c. --Proof. by move/(introNTF Hb) <-; case b. Qed. -- --Lemma elimTFn : b = c -> if c then ~ P else P. --Proof. by move <-; apply: (elimNTF Hb); case b. Qed. -- --Lemma equivPifn : (Q -> P) -> (P -> Q) -> if b then ~ Q else Q. --Proof. by rewrite -if_neg; apply: equivPif. Qed. -- --Lemma xorPifn : Q \/ P -> ~ (Q /\ P) -> if b then Q else ~ Q. --Proof. by rewrite -if_neg; apply: xorPif. Qed. -- --End ReflectNegCore. -- --(* User-oriented reflection lemmas *) --Section Reflect. -- --Variables (P Q : Prop) (b b' c : bool). --Hypotheses (Pb : reflect P b) (Pb' : reflect P (~~ b')). -- --Lemma introT : P -> b. Proof. exact: introTF true _. Qed. --Lemma introF : ~ P -> b = false. Proof. exact: introTF false _. Qed. --Lemma introN : ~ P -> ~~ b. Proof. exact: introNTF true _. Qed. --Lemma introNf : P -> ~~ b = false. Proof. exact: introNTF false _. Qed. --Lemma introTn : ~ P -> b'. Proof. exact: introTFn true _. Qed. --Lemma introFn : P -> b' = false. Proof. exact: introTFn false _. Qed. -- --Lemma elimT : b -> P. Proof. exact: elimTF true _. Qed. --Lemma elimF : b = false -> ~ P. Proof. exact: elimTF false _. Qed. --Lemma elimN : ~~ b -> ~P. Proof. exact: elimNTF true _. Qed. --Lemma elimNf : ~~ b = false -> P. Proof. exact: elimNTF false _. Qed. --Lemma elimTn : b' -> ~ P. Proof. exact: elimTFn true _. Qed. --Lemma elimFn : b' = false -> P. Proof. exact: elimTFn false _. Qed. -- --Lemma introP : (b -> Q) -> (~~ b -> ~ Q) -> reflect Q b. --Proof. by case b; constructor; auto. Qed. -- --Lemma iffP : (P -> Q) -> (Q -> P) -> reflect Q b. --Proof. by case: Pb; constructor; auto. Qed. -- --Lemma equivP : (P <-> Q) -> reflect Q b. --Proof. by case; apply: iffP. Qed. -- --Lemma sumboolP (decQ : decidable Q) : reflect Q decQ. --Proof. by case: decQ; constructor. Qed. -- --Lemma appP : reflect Q b -> P -> Q. --Proof. by move=> Qb; move/introT; case: Qb. Qed. -- --Lemma sameP : reflect P c -> b = c. --Proof. by case; [apply: introT | apply: introF]. Qed. -- --Lemma decPcases : if b then P else ~ P. Proof. by case Pb. Qed. -- --Definition decP : decidable P. by case: b decPcases; [left | right]. Defined. -- --Lemma rwP : P <-> b. Proof. by split; [apply: introT | apply: elimT]. Qed. -- --Lemma rwP2 : reflect Q b -> (P <-> Q). --Proof. by move=> Qb; split=> ?; [apply: appP | apply: elimT; case: Qb]. Qed. -- --(* Predicate family to reflect excluded middle in bool. *) --CoInductive alt_spec : bool -> Type := -- | AltTrue of P : alt_spec true -- | AltFalse of ~~ b : alt_spec false. -- --Lemma altP : alt_spec b. --Proof. by case def_b: b / Pb; constructor; rewrite ?def_b. Qed. -- --End Reflect. -- --Hint View for move/ elimTF|3 elimNTF|3 elimTFn|3 introT|2 introTn|2 introN|2. -- --Hint View for apply/ introTF|3 introNTF|3 introTFn|3 elimT|2 elimTn|2 elimN|2. -- --Hint View for apply// equivPif|3 xorPif|3 equivPifn|3 xorPifn|3. -- --(* Allow the direct application of a reflection lemma to a boolean assertion. *) --Coercion elimT : reflect >-> Funclass. -- --CoInductive implies P Q := Implies of P -> Q. --Lemma impliesP P Q : implies P Q -> P -> Q. Proof. by case. Qed. --Lemma impliesPn (P Q : Prop) : implies P Q -> ~ Q -> ~ P. --Proof. by case=> iP ? /iP. Qed. --Coercion impliesP : implies >-> Funclass. --Hint View for move/ impliesPn|2 impliesP|2. --Hint View for apply/ impliesPn|2 impliesP|2. -- --(* Impredicative or, which can emulate a classical not-implies. *) --Definition unless condition property : Prop := -- forall goal : Prop, (condition -> goal) -> (property -> goal) -> goal. -- --Notation "\unless C , P" := (unless C P) -- (at level 200, C at level 100, -- format "'[' \unless C , '/ ' P ']'") : type_scope. -- --Lemma unlessL C P : implies C (\unless C, P). --Proof. by split=> hC G /(_ hC). Qed. -- --Lemma unlessR C P : implies P (\unless C, P). --Proof. by split=> hP G _ /(_ hP). Qed. -- --Lemma unless_sym C P : implies (\unless C, P) (\unless P, C). --Proof. by split; apply; [apply/unlessR | apply/unlessL]. Qed. -- --Lemma unlessP (C P : Prop) : (\unless C, P) <-> C \/ P. --Proof. by split=> [|[/unlessL | /unlessR]]; apply; [left | right]. Qed. -- --Lemma bind_unless C P {Q} : implies (\unless C, P) (\unless (\unless C, Q), P). --Proof. by split; apply=> [hC|hP]; [apply/unlessL/unlessL | apply/unlessR]. Qed. -- --Lemma unless_contra b C : implies (~~ b -> C) (\unless C, b). --Proof. by split; case: b => [_ | hC]; [apply/unlessR | apply/unlessL/hC]. Qed. -- --(* Classical reasoning becomes directly accessible for any bool subgoal. *) --(* Note that we cannot use "unless" here for lack of universe polymorphism. *) --Definition classically P : Prop := forall b : bool, (P -> b) -> b. -- --Lemma classicP (P : Prop) : classically P <-> ~ ~ P. --Proof. --split=> [cP nP | nnP [] // nP]; last by case nnP; move/nP. --by have: P -> false; [move/nP | move/cP]. --Qed. -- --Lemma classicW P : P -> classically P. Proof. by move=> hP _ ->. Qed. -- --Lemma classic_bind P Q : (P -> classically Q) -> classically P -> classically Q. --Proof. by move=> iPQ cP b /iPQ-/cP. Qed. -- --Lemma classic_EM P : classically (decidable P). --Proof. --by case=> // undecP; apply/undecP; right=> notP; apply/notF/undecP; left. --Qed. -- --Lemma classic_pick T P : classically ({x : T | P x} + (forall x, ~ P x)). --Proof. --case=> // undecP; apply/undecP; right=> x Px. --by apply/notF/undecP; left; exists x. --Qed. -- --Lemma classic_imply P Q : (P -> classically Q) -> classically (P -> Q). --Proof. --move=> iPQ []// notPQ; apply/notPQ=> /iPQ-cQ. --by case: notF; apply: cQ => hQ; apply: notPQ. --Qed. -- --(* List notations for wider connectives; the Prop connectives have a fixed *) --(* width so as to avoid iterated destruction (we go up to width 5 for /\, and *) --(* width 4 for or). The bool connectives have arbitrary widths, but denote *) --(* expressions that associate to the RIGHT. This is consistent with the right *) --(* associativity of list expressions and thus more convenient in most proofs. *) -- --Inductive and3 (P1 P2 P3 : Prop) : Prop := And3 of P1 & P2 & P3. -- --Inductive and4 (P1 P2 P3 P4 : Prop) : Prop := And4 of P1 & P2 & P3 & P4. -- --Inductive and5 (P1 P2 P3 P4 P5 : Prop) : Prop := -- And5 of P1 & P2 & P3 & P4 & P5. -- --Inductive or3 (P1 P2 P3 : Prop) : Prop := Or31 of P1 | Or32 of P2 | Or33 of P3. -- --Inductive or4 (P1 P2 P3 P4 : Prop) : Prop := -- Or41 of P1 | Or42 of P2 | Or43 of P3 | Or44 of P4. -- --Notation "[ /\ P1 & P2 ]" := (and P1 P2) (only parsing) : type_scope. --Notation "[ /\ P1 , P2 & P3 ]" := (and3 P1 P2 P3) : type_scope. --Notation "[ /\ P1 , P2 , P3 & P4 ]" := (and4 P1 P2 P3 P4) : type_scope. --Notation "[ /\ P1 , P2 , P3 , P4 & P5 ]" := (and5 P1 P2 P3 P4 P5) : type_scope. -- --Notation "[ \/ P1 | P2 ]" := (or P1 P2) (only parsing) : type_scope. --Notation "[ \/ P1 , P2 | P3 ]" := (or3 P1 P2 P3) : type_scope. --Notation "[ \/ P1 , P2 , P3 | P4 ]" := (or4 P1 P2 P3 P4) : type_scope. -- --Notation "[ && b1 & c ]" := (b1 && c) (only parsing) : bool_scope. --Notation "[ && b1 , b2 , .. , bn & c ]" := (b1 && (b2 && .. (bn && c) .. )) -- : bool_scope. -- --Notation "[ || b1 | c ]" := (b1 || c) (only parsing) : bool_scope. --Notation "[ || b1 , b2 , .. , bn | c ]" := (b1 || (b2 || .. (bn || c) .. )) -- : bool_scope. -- --Notation "[ ==> b1 , b2 , .. , bn => c ]" := -- (b1 ==> (b2 ==> .. (bn ==> c) .. )) : bool_scope. --Notation "[ ==> b1 => c ]" := (b1 ==> c) (only parsing) : bool_scope. -- --Section AllAnd. -- --Variables (T : Type) (P1 P2 P3 P4 P5 : T -> Prop). --Local Notation a P := (forall x, P x). -- --Lemma all_and2 : implies (forall x, [/\ P1 x & P2 x]) [/\ a P1 & a P2]. --Proof. by split=> haveP; split=> x; case: (haveP x). Qed. -- --Lemma all_and3 : implies (forall x, [/\ P1 x, P2 x & P3 x]) -- [/\ a P1, a P2 & a P3]. --Proof. by split=> haveP; split=> x; case: (haveP x). Qed. -- --Lemma all_and4 : implies (forall x, [/\ P1 x, P2 x, P3 x & P4 x]) -- [/\ a P1, a P2, a P3 & a P4]. --Proof. by split=> haveP; split=> x; case: (haveP x). Qed. -- --Lemma all_and5 : implies (forall x, [/\ P1 x, P2 x, P3 x, P4 x & P5 x]) -- [/\ a P1, a P2, a P3, a P4 & a P5]. --Proof. by split=> haveP; split=> x; case: (haveP x). Qed. -- --End AllAnd. -- --Arguments all_and2 {T P1 P2}. --Arguments all_and3 {T P1 P2 P3}. --Arguments all_and4 {T P1 P2 P3 P4}. --Arguments all_and5 {T P1 P2 P3 P4 P5}. -- --Lemma pair_andP P Q : P /\ Q <-> P * Q. Proof. by split; case. Qed. -- --Section ReflectConnectives. -- --Variable b1 b2 b3 b4 b5 : bool. -- --Lemma idP : reflect b1 b1. --Proof. by case b1; constructor. Qed. -- --Lemma boolP : alt_spec b1 b1 b1. --Proof. exact: (altP idP). Qed. -- --Lemma idPn : reflect (~~ b1) (~~ b1). --Proof. by case b1; constructor. Qed. -- --Lemma negP : reflect (~ b1) (~~ b1). --Proof. by case b1; constructor; auto. Qed. -- --Lemma negPn : reflect b1 (~~ ~~ b1). --Proof. by case b1; constructor. Qed. -- --Lemma negPf : reflect (b1 = false) (~~ b1). --Proof. by case b1; constructor. Qed. -- --Lemma andP : reflect (b1 /\ b2) (b1 && b2). --Proof. by case b1; case b2; constructor=> //; case. Qed. -- --Lemma and3P : reflect [/\ b1, b2 & b3] [&& b1, b2 & b3]. --Proof. by case b1; case b2; case b3; constructor; try by case. Qed. -- --Lemma and4P : reflect [/\ b1, b2, b3 & b4] [&& b1, b2, b3 & b4]. --Proof. by case b1; case b2; case b3; case b4; constructor; try by case. Qed. -- --Lemma and5P : reflect [/\ b1, b2, b3, b4 & b5] [&& b1, b2, b3, b4 & b5]. --Proof. --by case b1; case b2; case b3; case b4; case b5; constructor; try by case. --Qed. -- --Lemma orP : reflect (b1 \/ b2) (b1 || b2). --Proof. by case b1; case b2; constructor; auto; case. Qed. -- --Lemma or3P : reflect [\/ b1, b2 | b3] [|| b1, b2 | b3]. --Proof. --case b1; first by constructor; constructor 1. --case b2; first by constructor; constructor 2. --case b3; first by constructor; constructor 3. --by constructor; case. --Qed. -- --Lemma or4P : reflect [\/ b1, b2, b3 | b4] [|| b1, b2, b3 | b4]. --Proof. --case b1; first by constructor; constructor 1. --case b2; first by constructor; constructor 2. --case b3; first by constructor; constructor 3. --case b4; first by constructor; constructor 4. --by constructor; case. --Qed. -- --Lemma nandP : reflect (~~ b1 \/ ~~ b2) (~~ (b1 && b2)). --Proof. by case b1; case b2; constructor; auto; case; auto. Qed. -- --Lemma norP : reflect (~~ b1 /\ ~~ b2) (~~ (b1 || b2)). --Proof. by case b1; case b2; constructor; auto; case; auto. Qed. -- --Lemma implyP : reflect (b1 -> b2) (b1 ==> b2). --Proof. by case b1; case b2; constructor; auto. Qed. -- --End ReflectConnectives. -- --Arguments idP [b1]. --Arguments idPn [b1]. --Arguments negP [b1]. --Arguments negPn [b1]. --Arguments negPf [b1]. --Arguments andP [b1 b2]. --Arguments and3P [b1 b2 b3]. --Arguments and4P [b1 b2 b3 b4]. --Arguments and5P [b1 b2 b3 b4 b5]. --Arguments orP [b1 b2]. --Arguments or3P [b1 b2 b3]. --Arguments or4P [b1 b2 b3 b4]. --Arguments nandP [b1 b2]. --Arguments norP [b1 b2]. --Arguments implyP [b1 b2]. --Prenex Implicits idP idPn negP negPn negPf. --Prenex Implicits andP and3P and4P and5P orP or3P or4P nandP norP implyP. -- --(* Shorter, more systematic names for the boolean connectives laws. *) -- --Lemma andTb : left_id true andb. Proof. by []. Qed. --Lemma andFb : left_zero false andb. Proof. by []. Qed. --Lemma andbT : right_id true andb. Proof. by case. Qed. --Lemma andbF : right_zero false andb. Proof. by case. Qed. --Lemma andbb : idempotent andb. Proof. by case. Qed. --Lemma andbC : commutative andb. Proof. by do 2!case. Qed. --Lemma andbA : associative andb. Proof. by do 3!case. Qed. --Lemma andbCA : left_commutative andb. Proof. by do 3!case. Qed. --Lemma andbAC : right_commutative andb. Proof. by do 3!case. Qed. --Lemma andbACA : interchange andb andb. Proof. by do 4!case. Qed. -- --Lemma orTb : forall b, true || b. Proof. by []. Qed. --Lemma orFb : left_id false orb. Proof. by []. Qed. --Lemma orbT : forall b, b || true. Proof. by case. Qed. --Lemma orbF : right_id false orb. Proof. by case. Qed. --Lemma orbb : idempotent orb. Proof. by case. Qed. --Lemma orbC : commutative orb. Proof. by do 2!case. Qed. --Lemma orbA : associative orb. Proof. by do 3!case. Qed. --Lemma orbCA : left_commutative orb. Proof. by do 3!case. Qed. --Lemma orbAC : right_commutative orb. Proof. by do 3!case. Qed. --Lemma orbACA : interchange orb orb. Proof. by do 4!case. Qed. -- --Lemma andbN b : b && ~~ b = false. Proof. by case: b. Qed. --Lemma andNb b : ~~ b && b = false. Proof. by case: b. Qed. --Lemma orbN b : b || ~~ b = true. Proof. by case: b. Qed. --Lemma orNb b : ~~ b || b = true. Proof. by case: b. Qed. -- --Lemma andb_orl : left_distributive andb orb. Proof. by do 3!case. Qed. --Lemma andb_orr : right_distributive andb orb. Proof. by do 3!case. Qed. --Lemma orb_andl : left_distributive orb andb. Proof. by do 3!case. Qed. --Lemma orb_andr : right_distributive orb andb. Proof. by do 3!case. Qed. -- --Lemma andb_idl (a b : bool) : (b -> a) -> a && b = b. --Proof. by case: a; case: b => // ->. Qed. --Lemma andb_idr (a b : bool) : (a -> b) -> a && b = a. --Proof. by case: a; case: b => // ->. Qed. --Lemma andb_id2l (a b c : bool) : (a -> b = c) -> a && b = a && c. --Proof. by case: a; case: b; case: c => // ->. Qed. --Lemma andb_id2r (a b c : bool) : (b -> a = c) -> a && b = c && b. --Proof. by case: a; case: b; case: c => // ->. Qed. -- --Lemma orb_idl (a b : bool) : (a -> b) -> a || b = b. --Proof. by case: a; case: b => // ->. Qed. --Lemma orb_idr (a b : bool) : (b -> a) -> a || b = a. --Proof. by case: a; case: b => // ->. Qed. --Lemma orb_id2l (a b c : bool) : (~~ a -> b = c) -> a || b = a || c. --Proof. by case: a; case: b; case: c => // ->. Qed. --Lemma orb_id2r (a b c : bool) : (~~ b -> a = c) -> a || b = c || b. --Proof. by case: a; case: b; case: c => // ->. Qed. -- --Lemma negb_and (a b : bool) : ~~ (a && b) = ~~ a || ~~ b. --Proof. by case: a; case: b. Qed. -- --Lemma negb_or (a b : bool) : ~~ (a || b) = ~~ a && ~~ b. --Proof. by case: a; case: b. Qed. -- --(* Pseudo-cancellation -- i.e, absorbtion *) -- --Lemma andbK a b : a && b || a = a. Proof. by case: a; case: b. Qed. --Lemma andKb a b : a || b && a = a. Proof. by case: a; case: b. Qed. --Lemma orbK a b : (a || b) && a = a. Proof. by case: a; case: b. Qed. --Lemma orKb a b : a && (b || a) = a. Proof. by case: a; case: b. Qed. -- --(* Imply *) -- --Lemma implybT b : b ==> true. Proof. by case: b. Qed. --Lemma implybF b : (b ==> false) = ~~ b. Proof. by case: b. Qed. --Lemma implyFb b : false ==> b. Proof. by []. Qed. --Lemma implyTb b : (true ==> b) = b. Proof. by []. Qed. --Lemma implybb b : b ==> b. Proof. by case: b. Qed. -- --Lemma negb_imply a b : ~~ (a ==> b) = a && ~~ b. --Proof. by case: a; case: b. Qed. -- --Lemma implybE a b : (a ==> b) = ~~ a || b. --Proof. by case: a; case: b. Qed. -- --Lemma implyNb a b : (~~ a ==> b) = a || b. --Proof. by case: a; case: b. Qed. -- --Lemma implybN a b : (a ==> ~~ b) = (b ==> ~~ a). --Proof. by case: a; case: b. Qed. -- --Lemma implybNN a b : (~~ a ==> ~~ b) = b ==> a. --Proof. by case: a; case: b. Qed. -- --Lemma implyb_idl (a b : bool) : (~~ a -> b) -> (a ==> b) = b. --Proof. by case: a; case: b => // ->. Qed. --Lemma implyb_idr (a b : bool) : (b -> ~~ a) -> (a ==> b) = ~~ a. --Proof. by case: a; case: b => // ->. Qed. --Lemma implyb_id2l (a b c : bool) : (a -> b = c) -> (a ==> b) = (a ==> c). --Proof. by case: a; case: b; case: c => // ->. Qed. -- --(* Addition (xor) *) -- --Lemma addFb : left_id false addb. Proof. by []. Qed. --Lemma addbF : right_id false addb. Proof. by case. Qed. --Lemma addbb : self_inverse false addb. Proof. by case. Qed. --Lemma addbC : commutative addb. Proof. by do 2!case. Qed. --Lemma addbA : associative addb. Proof. by do 3!case. Qed. --Lemma addbCA : left_commutative addb. Proof. by do 3!case. Qed. --Lemma addbAC : right_commutative addb. Proof. by do 3!case. Qed. --Lemma addbACA : interchange addb addb. Proof. by do 4!case. Qed. --Lemma andb_addl : left_distributive andb addb. Proof. by do 3!case. Qed. --Lemma andb_addr : right_distributive andb addb. Proof. by do 3!case. Qed. --Lemma addKb : left_loop id addb. Proof. by do 2!case. Qed. --Lemma addbK : right_loop id addb. Proof. by do 2!case. Qed. --Lemma addIb : left_injective addb. Proof. by do 3!case. Qed. --Lemma addbI : right_injective addb. Proof. by do 3!case. Qed. -- --Lemma addTb b : true (+) b = ~~ b. Proof. by []. Qed. --Lemma addbT b : b (+) true = ~~ b. Proof. by case: b. Qed. -- --Lemma addbN a b : a (+) ~~ b = ~~ (a (+) b). --Proof. by case: a; case: b. Qed. --Lemma addNb a b : ~~ a (+) b = ~~ (a (+) b). --Proof. by case: a; case: b. Qed. -- --Lemma addbP a b : reflect (~~ a = b) (a (+) b). --Proof. by case: a; case: b; constructor. Qed. --Arguments addbP [a b]. -- --(* Resolution tactic for blindly weeding out common terms from boolean *) --(* equalities. When faced with a goal of the form (andb/orb/addb b1 b2) = b3 *) --(* they will try to locate b1 in b3 and remove it. This can fail! *) -- --Ltac bool_congr := -- match goal with -- | |- (?X1 && ?X2 = ?X3) => first -- [ symmetry; rewrite -1?(andbC X1) -?(andbCA X1); congr 1 (andb X1); symmetry -- | case: (X1); [ rewrite ?andTb ?andbT // | by rewrite ?andbF /= ] ] -- | |- (?X1 || ?X2 = ?X3) => first -- [ symmetry; rewrite -1?(orbC X1) -?(orbCA X1); congr 1 (orb X1); symmetry -- | case: (X1); [ by rewrite ?orbT //= | rewrite ?orFb ?orbF ] ] -- | |- (?X1 (+) ?X2 = ?X3) => -- symmetry; rewrite -1?(addbC X1) -?(addbCA X1); congr 1 (addb X1); symmetry -- | |- (~~ ?X1 = ?X2) => congr 1 negb -- end. -- --(******************************************************************************) --(* Predicates, i.e., packaged functions to bool. *) --(* - pred T, the basic type for predicates over a type T, is simply an alias *) --(* for T -> bool. *) --(* We actually distinguish two kinds of predicates, which we call applicative *) --(* and collective, based on the syntax used to test them at some x in T: *) --(* - For an applicative predicate P, one uses prefix syntax: *) --(* P x *) --(* Also, most operations on applicative predicates use prefix syntax as *) --(* well (e.g., predI P Q). *) --(* - For a collective predicate A, one uses infix syntax: *) --(* x \in A *) --(* and all operations on collective predicates use infix syntax as well *) --(* (e.g., [predI A & B]). *) --(* There are only two kinds of applicative predicates: *) --(* - pred T, the alias for T -> bool mentioned above *) --(* - simpl_pred T, an alias for simpl_fun T bool with a coercion to pred T *) --(* that auto-simplifies on application (see ssrfun). *) --(* On the other hand, the set of collective predicate types is open-ended via *) --(* - predType T, a Structure that can be used to put Canonical collective *) --(* predicate interpretation on other types, such as lists, tuples, *) --(* finite sets, etc. *) --(* Indeed, we define such interpretations for applicative predicate types, *) --(* which can therefore also be used with the infix syntax, e.g., *) --(* x \in predI P Q *) --(* Moreover these infix forms are convertible to their prefix counterpart *) --(* (e.g., predI P Q x which in turn simplifies to P x && Q x). The converse *) --(* is not true, however; collective predicate types cannot, in general, be *) --(* general, be used applicatively, because of the "uniform inheritance" *) --(* restriction on implicit coercions. *) --(* However, we do define an explicit generic coercion *) --(* - mem : forall (pT : predType), pT -> mem_pred T *) --(* where mem_pred T is a variant of simpl_pred T that preserves the infix *) --(* syntax, i.e., mem A x auto-simplifies to x \in A. *) --(* Indeed, the infix "collective" operators are notation for a prefix *) --(* operator with arguments of type mem_pred T or pred T, applied to coerced *) --(* collective predicates, e.g., *) --(* Notation "x \in A" := (in_mem x (mem A)). *) --(* This prevents the variability in the predicate type from interfering with *) --(* the application of generic lemmas. Moreover this also makes it much easier *) --(* to define generic lemmas, because the simplest type -- pred T -- can be *) --(* used as the type of generic collective predicates, provided one takes care *) --(* not to use it applicatively; this avoids the burden of having to declare a *) --(* different predicate type for each predicate parameter of each section or *) --(* lemma. *) --(* This trick is made possible by the fact that the constructor of the *) --(* mem_pred T type aligns the unification process, forcing a generic *) --(* "collective" predicate A : pred T to unify with the actual collective B, *) --(* which mem has coerced to pred T via an internal, hidden implicit coercion, *) --(* supplied by the predType structure for B. Users should take care not to *) --(* inadvertently "strip" (mem B) down to the coerced B, since this will *) --(* expose the internal coercion: Coq will display a term B x that cannot be *) --(* typed as such. The topredE lemma can be used to restore the x \in B *) --(* syntax in this case. While -topredE can conversely be used to change *) --(* x \in P into P x, it is safer to use the inE and memE lemmas instead, as *) --(* they do not run the risk of exposing internal coercions. As a consequence *) --(* it is better to explicitly cast a generic applicative pred T to simpl_pred *) --(* using the SimplPred constructor, when it is used as a collective predicate *) --(* (see, e.g., Lemma eq_big in bigop). *) --(* We also sometimes "instantiate" the predType structure by defining a *) --(* coercion to the sort of the predPredType structure. This works better for *) --(* types such as {set T} that have subtypes that coerce to them, since the *) --(* same coercion will be inserted by the application of mem. It also lets us *) --(* turn any Type aT : predArgType into the total predicate over that type, *) --(* i.e., fun _: aT => true. This allows us to write, e.g., #|'I_n| for the *) --(* cardinal of the (finite) type of integers less than n. *) --(* Collective predicates have a specific extensional equality, *) --(* - A =i B, *) --(* while applicative predicates use the extensional equality of functions, *) --(* - P =1 Q *) --(* The two forms are convertible, however. *) --(* We lift boolean operations to predicates, defining: *) --(* - predU (union), predI (intersection), predC (complement), *) --(* predD (difference), and preim (preimage, i.e., composition) *) --(* For each operation we define three forms, typically: *) --(* - predU : pred T -> pred T -> simpl_pred T *) --(* - [predU A & B], a Notation for predU (mem A) (mem B) *) --(* - xpredU, a Notation for the lambda-expression inside predU, *) --(* which is mostly useful as an argument of =1, since it exposes the head *) --(* head constant of the expression to the ssreflect matching algorithm. *) --(* The syntax for the preimage of a collective predicate A is *) --(* - [preim f of A] *) --(* Finally, the generic syntax for defining a simpl_pred T is *) --(* - [pred x : T | P(x)], [pred x | P(x)], [pred x in A | P(x)], etc. *) --(* We also support boolean relations, but only the applicative form, with *) --(* types *) --(* - rel T, an alias for T -> pred T *) --(* - simpl_rel T, an auto-simplifying version, and syntax *) --(* [rel x y | P(x,y)], [rel x y in A & B | P(x,y)], etc. *) --(* The notation [rel of fA] can be used to coerce a function returning a *) --(* collective predicate to one returning pred T. *) --(* Finally, note that there is specific support for ambivalent predicates *) --(* that can work in either style, as per this file's head descriptor. *) --(******************************************************************************) -- --Definition pred T := T -> bool. -- --Identity Coercion fun_of_pred : pred >-> Funclass. -- --Definition rel T := T -> pred T. -- --Identity Coercion fun_of_rel : rel >-> Funclass. -- --Notation xpred0 := (fun _ => false). --Notation xpredT := (fun _ => true). --Notation xpredI := (fun (p1 p2 : pred _) x => p1 x && p2 x). --Notation xpredU := (fun (p1 p2 : pred _) x => p1 x || p2 x). --Notation xpredC := (fun (p : pred _) x => ~~ p x). --Notation xpredD := (fun (p1 p2 : pred _) x => ~~ p2 x && p1 x). --Notation xpreim := (fun f (p : pred _) x => p (f x)). --Notation xrelU := (fun (r1 r2 : rel _) x y => r1 x y || r2 x y). -- --Section Predicates. -- --Variables T : Type. -- --Definition subpred (p1 p2 : pred T) := forall x, p1 x -> p2 x. -- --Definition subrel (r1 r2 : rel T) := forall x y, r1 x y -> r2 x y. -- --Definition simpl_pred := simpl_fun T bool. --Definition applicative_pred := pred T. --Definition collective_pred := pred T. -- --Definition SimplPred (p : pred T) : simpl_pred := SimplFun p. -- --Coercion pred_of_simpl (p : simpl_pred) : pred T := fun_of_simpl p. --Coercion applicative_pred_of_simpl (p : simpl_pred) : applicative_pred := -- fun_of_simpl p. --Coercion collective_pred_of_simpl (p : simpl_pred) : collective_pred := -- fun x => (let: SimplFun f := p in fun _ => f x) x. --(* Note: applicative_of_simpl is convertible to pred_of_simpl, while *) --(* collective_of_simpl is not. *) -- --Definition pred0 := SimplPred xpred0. --Definition predT := SimplPred xpredT. --Definition predI p1 p2 := SimplPred (xpredI p1 p2). --Definition predU p1 p2 := SimplPred (xpredU p1 p2). --Definition predC p := SimplPred (xpredC p). --Definition predD p1 p2 := SimplPred (xpredD p1 p2). --Definition preim rT f (d : pred rT) := SimplPred (xpreim f d). -- --Definition simpl_rel := simpl_fun T (pred T). -- --Definition SimplRel (r : rel T) : simpl_rel := [fun x => r x]. -- --Coercion rel_of_simpl_rel (r : simpl_rel) : rel T := fun x y => r x y. -- --Definition relU r1 r2 := SimplRel (xrelU r1 r2). -- --Lemma subrelUl r1 r2 : subrel r1 (relU r1 r2). --Proof. by move=> *; apply/orP; left. Qed. -- --Lemma subrelUr r1 r2 : subrel r2 (relU r1 r2). --Proof. by move=> *; apply/orP; right. Qed. -- --CoInductive mem_pred := Mem of pred T. -- --Definition isMem pT topred mem := mem = (fun p : pT => Mem [eta topred p]). -- --Structure predType := PredType { -- pred_sort :> Type; -- topred : pred_sort -> pred T; -- _ : {mem | isMem topred mem} --}. -- --Definition mkPredType pT toP := PredType (exist (@isMem pT toP) _ (erefl _)). -- --Canonical predPredType := Eval hnf in @mkPredType (pred T) id. --Canonical simplPredType := Eval hnf in mkPredType pred_of_simpl. --Canonical boolfunPredType := Eval hnf in @mkPredType (T -> bool) id. -- --Coercion pred_of_mem mp : pred_sort predPredType := let: Mem p := mp in [eta p]. --Canonical memPredType := Eval hnf in mkPredType pred_of_mem. -- --Definition clone_pred U := -- fun pT & pred_sort pT -> U => -- fun a mP (pT' := @PredType U a mP) & phant_id pT' pT => pT'. -- --End Predicates. -- --Arguments pred0 [T]. --Arguments predT [T]. --Prenex Implicits pred0 predT predI predU predC predD preim relU. -- --Notation "[ 'pred' : T | E ]" := (SimplPred (fun _ : T => E%B)) -- (at level 0, format "[ 'pred' : T | E ]") : fun_scope. --Notation "[ 'pred' x | E ]" := (SimplPred (fun x => E%B)) -- (at level 0, x ident, format "[ 'pred' x | E ]") : fun_scope. --Notation "[ 'pred' x | E1 & E2 ]" := [pred x | E1 && E2 ] -- (at level 0, x ident, format "[ 'pred' x | E1 & E2 ]") : fun_scope. --Notation "[ 'pred' x : T | E ]" := (SimplPred (fun x : T => E%B)) -- (at level 0, x ident, only parsing) : fun_scope. --Notation "[ 'pred' x : T | E1 & E2 ]" := [pred x : T | E1 && E2 ] -- (at level 0, x ident, only parsing) : fun_scope. --Notation "[ 'rel' x y | E ]" := (SimplRel (fun x y => E%B)) -- (at level 0, x ident, y ident, format "[ 'rel' x y | E ]") : fun_scope. --Notation "[ 'rel' x y : T | E ]" := (SimplRel (fun x y : T => E%B)) -- (at level 0, x ident, y ident, only parsing) : fun_scope. -- --Notation "[ 'predType' 'of' T ]" := (@clone_pred _ T _ id _ _ id) -- (at level 0, format "[ 'predType' 'of' T ]") : form_scope. -- --(* This redundant coercion lets us "inherit" the simpl_predType canonical *) --(* instance by declaring a coercion to simpl_pred. This hack is the only way *) --(* to put a predType structure on a predArgType. We use simpl_pred rather *) --(* than pred to ensure that /= removes the identity coercion. Note that the *) --(* coercion will never be used directly for simpl_pred, since the canonical *) --(* instance should always be resolved. *) -- --Notation pred_class := (pred_sort (predPredType _)). --Coercion sort_of_simpl_pred T (p : simpl_pred T) : pred_class := p : pred T. -- --(* This lets us use some types as a synonym for their universal predicate. *) --(* Unfortunately, this won't work for existing types like bool, unless we *) --(* redefine bool, true, false and all bool ops. *) --Definition predArgType := Type. --Bind Scope type_scope with predArgType. --Identity Coercion sort_of_predArgType : predArgType >-> Sortclass. --Coercion pred_of_argType (T : predArgType) : simpl_pred T := predT. -- --Notation "{ : T }" := (T%type : predArgType) -- (at level 0, format "{ : T }") : type_scope. -- --(* These must be defined outside a Section because "cooking" kills the *) --(* nosimpl tag. *) -- --Definition mem T (pT : predType T) : pT -> mem_pred T := -- nosimpl (let: @PredType _ _ _ (exist _ mem _) := pT return pT -> _ in mem). --Definition in_mem T x mp := nosimpl pred_of_mem T mp x. -- --Prenex Implicits mem. -- --Coercion pred_of_mem_pred T mp := [pred x : T | in_mem x mp]. -- --Definition eq_mem T p1 p2 := forall x : T, in_mem x p1 = in_mem x p2. --Definition sub_mem T p1 p2 := forall x : T, in_mem x p1 -> in_mem x p2. -- --Typeclasses Opaque eq_mem. -- --Lemma sub_refl T (p : mem_pred T) : sub_mem p p. Proof. by []. Qed. --Arguments sub_refl {T p}. -- --Notation "x \in A" := (in_mem x (mem A)) : bool_scope. --Notation "x \in A" := (in_mem x (mem A)) : bool_scope. --Notation "x \notin A" := (~~ (x \in A)) : bool_scope. --Notation "A =i B" := (eq_mem (mem A) (mem B)) : type_scope. --Notation "{ 'subset' A <= B }" := (sub_mem (mem A) (mem B)) -- (at level 0, A, B at level 69, -- format "{ '[hv' 'subset' A '/ ' <= B ']' }") : type_scope. --Notation "[ 'mem' A ]" := (pred_of_simpl (pred_of_mem_pred (mem A))) -- (at level 0, only parsing) : fun_scope. --Notation "[ 'rel' 'of' fA ]" := (fun x => [mem (fA x)]) -- (at level 0, format "[ 'rel' 'of' fA ]") : fun_scope. --Notation "[ 'predI' A & B ]" := (predI [mem A] [mem B]) -- (at level 0, format "[ 'predI' A & B ]") : fun_scope. --Notation "[ 'predU' A & B ]" := (predU [mem A] [mem B]) -- (at level 0, format "[ 'predU' A & B ]") : fun_scope. --Notation "[ 'predD' A & B ]" := (predD [mem A] [mem B]) -- (at level 0, format "[ 'predD' A & B ]") : fun_scope. --Notation "[ 'predC' A ]" := (predC [mem A]) -- (at level 0, format "[ 'predC' A ]") : fun_scope. --Notation "[ 'preim' f 'of' A ]" := (preim f [mem A]) -- (at level 0, format "[ 'preim' f 'of' A ]") : fun_scope. -- --Notation "[ 'pred' x 'in' A ]" := [pred x | x \in A] -- (at level 0, x ident, format "[ 'pred' x 'in' A ]") : fun_scope. --Notation "[ 'pred' x 'in' A | E ]" := [pred x | x \in A & E] -- (at level 0, x ident, format "[ 'pred' x 'in' A | E ]") : fun_scope. --Notation "[ 'pred' x 'in' A | E1 & E2 ]" := [pred x | x \in A & E1 && E2 ] -- (at level 0, x ident, -- format "[ 'pred' x 'in' A | E1 & E2 ]") : fun_scope. --Notation "[ 'rel' x y 'in' A & B | E ]" := -- [rel x y | (x \in A) && (y \in B) && E] -- (at level 0, x ident, y ident, -- format "[ 'rel' x y 'in' A & B | E ]") : fun_scope. --Notation "[ 'rel' x y 'in' A & B ]" := [rel x y | (x \in A) && (y \in B)] -- (at level 0, x ident, y ident, -- format "[ 'rel' x y 'in' A & B ]") : fun_scope. --Notation "[ 'rel' x y 'in' A | E ]" := [rel x y in A & A | E] -- (at level 0, x ident, y ident, -- format "[ 'rel' x y 'in' A | E ]") : fun_scope. --Notation "[ 'rel' x y 'in' A ]" := [rel x y in A & A] -- (at level 0, x ident, y ident, -- format "[ 'rel' x y 'in' A ]") : fun_scope. -- --Section simpl_mem. -- --Variables (T : Type) (pT : predType T). --Implicit Types (x : T) (p : pred T) (sp : simpl_pred T) (pp : pT). -- --(* Bespoke structures that provide fine-grained control over matching the *) --(* various forms of the \in predicate; note in particular the different forms *) --(* of hoisting that are used. We had to work around several bugs in the *) --(* implementation of unification, notably improper expansion of telescope *) --(* projections and overwriting of a variable assignment by a later *) --(* unification (probably due to conversion cache cross-talk). *) --Structure manifest_applicative_pred p := ManifestApplicativePred { -- manifest_applicative_pred_value :> pred T; -- _ : manifest_applicative_pred_value = p --}. --Definition ApplicativePred p := ManifestApplicativePred (erefl p). --Canonical applicative_pred_applicative sp := -- ApplicativePred (applicative_pred_of_simpl sp). -- --Structure manifest_simpl_pred p := ManifestSimplPred { -- manifest_simpl_pred_value :> simpl_pred T; -- _ : manifest_simpl_pred_value = SimplPred p --}. --Canonical expose_simpl_pred p := ManifestSimplPred (erefl (SimplPred p)). -- --Structure manifest_mem_pred p := ManifestMemPred { -- manifest_mem_pred_value :> mem_pred T; -- _ : manifest_mem_pred_value= Mem [eta p] --}. --Canonical expose_mem_pred p := @ManifestMemPred p _ (erefl _). -- --Structure applicative_mem_pred p := -- ApplicativeMemPred {applicative_mem_pred_value :> manifest_mem_pred p}. --Canonical check_applicative_mem_pred p (ap : manifest_applicative_pred p) mp := -- @ApplicativeMemPred ap mp. -- --Lemma mem_topred (pp : pT) : mem (topred pp) = mem pp. --Proof. by rewrite /mem; case: pT pp => T1 app1 [mem1 /= ->]. Qed. -- --Lemma topredE x (pp : pT) : topred pp x = (x \in pp). --Proof. by rewrite -mem_topred. Qed. -- --Lemma app_predE x p (ap : manifest_applicative_pred p) : ap x = (x \in p). --Proof. by case: ap => _ /= ->. Qed. -- --Lemma in_applicative x p (amp : applicative_mem_pred p) : in_mem x amp = p x. --Proof. by case: amp => [[_ /= ->]]. Qed. -- --Lemma in_collective x p (msp : manifest_simpl_pred p) : -- (x \in collective_pred_of_simpl msp) = p x. --Proof. by case: msp => _ /= ->. Qed. -- --Lemma in_simpl x p (msp : manifest_simpl_pred p) : -- in_mem x (Mem [eta fun_of_simpl (msp : simpl_pred T)]) = p x. --Proof. by case: msp => _ /= ->. Qed. -- --(* Because of the explicit eta expansion in the left-hand side, this lemma *) --(* should only be used in a right-to-left direction. The 8.3 hack allowing *) --(* partial right-to-left use does not work with the improved expansion *) --(* heuristics in 8.4. *) --Lemma unfold_in x p : (x \in ([eta p] : pred T)) = p x. --Proof. by []. Qed. -- --Lemma simpl_predE p : SimplPred p =1 p. --Proof. by []. Qed. -- --Definition inE := (in_applicative, in_simpl, simpl_predE). (* to be extended *) -- --Lemma mem_simpl sp : mem sp = sp :> pred T. --Proof. by []. Qed. -- --Definition memE := mem_simpl. (* could be extended *) -- --Lemma mem_mem (pp : pT) : (mem (mem pp) = mem pp) * (mem [mem pp] = mem pp). --Proof. by rewrite -mem_topred. Qed. -- --End simpl_mem. -- --(* Qualifiers and keyed predicates. *) -- --CoInductive qualifier (q : nat) T := Qualifier of predPredType T. -- --Coercion has_quality n T (q : qualifier n T) : pred_class := -- fun x => let: Qualifier _ p := q in p x. --Arguments has_quality n [T]. -- --Lemma qualifE n T p x : (x \in @Qualifier n T p) = p x. Proof. by []. Qed. -- --Notation "x \is A" := (x \in has_quality 0 A) -- (at level 70, no associativity, -- format "'[hv' x '/ ' \is A ']'") : bool_scope. --Notation "x \is 'a' A" := (x \in has_quality 1 A) -- (at level 70, no associativity, -- format "'[hv' x '/ ' \is 'a' A ']'") : bool_scope. --Notation "x \is 'an' A" := (x \in has_quality 2 A) -- (at level 70, no associativity, -- format "'[hv' x '/ ' \is 'an' A ']'") : bool_scope. --Notation "x \isn't A" := (x \notin has_quality 0 A) -- (at level 70, no associativity, -- format "'[hv' x '/ ' \isn't A ']'") : bool_scope. --Notation "x \isn't 'a' A" := (x \notin has_quality 1 A) -- (at level 70, no associativity, -- format "'[hv' x '/ ' \isn't 'a' A ']'") : bool_scope. --Notation "x \isn't 'an' A" := (x \notin has_quality 2 A) -- (at level 70, no associativity, -- format "'[hv' x '/ ' \isn't 'an' A ']'") : bool_scope. --Notation "[ 'qualify' x | P ]" := (Qualifier 0 (fun x => P%B)) -- (at level 0, x at level 99, -- format "'[hv' [ 'qualify' x | '/ ' P ] ']'") : form_scope. --Notation "[ 'qualify' x : T | P ]" := (Qualifier 0 (fun x : T => P%B)) -- (at level 0, x at level 99, only parsing) : form_scope. --Notation "[ 'qualify' 'a' x | P ]" := (Qualifier 1 (fun x => P%B)) -- (at level 0, x at level 99, -- format "'[hv' [ 'qualify' 'a' x | '/ ' P ] ']'") : form_scope. --Notation "[ 'qualify' 'a' x : T | P ]" := (Qualifier 1 (fun x : T => P%B)) -- (at level 0, x at level 99, only parsing) : form_scope. --Notation "[ 'qualify' 'an' x | P ]" := (Qualifier 2 (fun x => P%B)) -- (at level 0, x at level 99, -- format "'[hv' [ 'qualify' 'an' x | '/ ' P ] ']'") : form_scope. --Notation "[ 'qualify' 'an' x : T | P ]" := (Qualifier 2 (fun x : T => P%B)) -- (at level 0, x at level 99, only parsing) : form_scope. -- --(* Keyed predicates: support for property-bearing predicate interfaces. *) -- --Section KeyPred. -- --Variable T : Type. --CoInductive pred_key (p : predPredType T) := DefaultPredKey. -- --Variable p : predPredType T. --Structure keyed_pred (k : pred_key p) := -- PackKeyedPred {unkey_pred :> pred_class; _ : unkey_pred =i p}. -- --Variable k : pred_key p. --Definition KeyedPred := @PackKeyedPred k p (frefl _). -- --Variable k_p : keyed_pred k. --Lemma keyed_predE : k_p =i p. Proof. by case: k_p. Qed. -- --(* Instances that strip the mem cast; the first one has "pred_of_mem" as its *) --(* projection head value, while the second has "pred_of_simpl". The latter *) --(* has the side benefit of preempting accidental misdeclarations. *) --(* Note: pred_of_mem is the registered mem >-> pred_class coercion, while *) --(* simpl_of_mem; pred_of_simpl is the mem >-> pred >=> Funclass coercion. We *) --(* must write down the coercions explicitly as the Canonical head constant *) --(* computation does not strip casts !! *) --Canonical keyed_mem := -- @PackKeyedPred k (pred_of_mem (mem k_p)) keyed_predE. --Canonical keyed_mem_simpl := -- @PackKeyedPred k (pred_of_simpl (mem k_p)) keyed_predE. -- --End KeyPred. -- --Notation "x \i 'n' S" := (x \in @unkey_pred _ S _ _) -- (at level 70, format "'[hv' x '/ ' \i 'n' S ']'") : bool_scope. -- --Section KeyedQualifier. -- --Variables (T : Type) (n : nat) (q : qualifier n T). -- --Structure keyed_qualifier (k : pred_key q) := -- PackKeyedQualifier {unkey_qualifier; _ : unkey_qualifier = q}. --Definition KeyedQualifier k := PackKeyedQualifier k (erefl q). --Variables (k : pred_key q) (k_q : keyed_qualifier k). --Fact keyed_qualifier_suproof : unkey_qualifier k_q =i q. --Proof. by case: k_q => /= _ ->. Qed. --Canonical keyed_qualifier_keyed := PackKeyedPred k keyed_qualifier_suproof. -- --End KeyedQualifier. -- --Notation "x \i 's' A" := (x \i n has_quality 0 A) -- (at level 70, format "'[hv' x '/ ' \i 's' A ']'") : bool_scope. --Notation "x \i 's' 'a' A" := (x \i n has_quality 1 A) -- (at level 70, format "'[hv' x '/ ' \i 's' 'a' A ']'") : bool_scope. --Notation "x \i 's' 'an' A" := (x \i n has_quality 2 A) -- (at level 70, format "'[hv' x '/ ' \i 's' 'an' A ']'") : bool_scope. -- --Module DefaultKeying. -- --Canonical default_keyed_pred T p := KeyedPred (@DefaultPredKey T p). --Canonical default_keyed_qualifier T n (q : qualifier n T) := -- KeyedQualifier (DefaultPredKey q). -- --End DefaultKeying. -- --(* Skolemizing with conditions. *) -- --Lemma all_tag_cond_dep I T (C : pred I) U : -- (forall x, T x) -> (forall x, C x -> {y : T x & U x y}) -> -- {f : forall x, T x & forall x, C x -> U x (f x)}. --Proof. --move=> f0 fP; apply: all_tag (fun x y => C x -> U x y) _ => x. --by case Cx: (C x); [case/fP: Cx => y; exists y | exists (f0 x)]. --Qed. -- --Lemma all_tag_cond I T (C : pred I) U : -- T -> (forall x, C x -> {y : T & U x y}) -> -- {f : I -> T & forall x, C x -> U x (f x)}. --Proof. by move=> y0; apply: all_tag_cond_dep. Qed. -- --Lemma all_sig_cond_dep I T (C : pred I) P : -- (forall x, T x) -> (forall x, C x -> {y : T x | P x y}) -> -- {f : forall x, T x | forall x, C x -> P x (f x)}. --Proof. by move=> f0 /(all_tag_cond_dep f0)[f]; exists f. Qed. -- --Lemma all_sig_cond I T (C : pred I) P : -- T -> (forall x, C x -> {y : T | P x y}) -> -- {f : I -> T | forall x, C x -> P x (f x)}. --Proof. by move=> y0; apply: all_sig_cond_dep. Qed. -- --Section RelationProperties. -- --(* Caveat: reflexive should not be used to state lemmas, as auto and trivial *) --(* will not expand the constant. *) -- --Variable T : Type. -- --Variable R : rel T. -- --Definition total := forall x y, R x y || R y x. --Definition transitive := forall y x z, R x y -> R y z -> R x z. -- --Definition symmetric := forall x y, R x y = R y x. --Definition antisymmetric := forall x y, R x y && R y x -> x = y. --Definition pre_symmetric := forall x y, R x y -> R y x. -- --Lemma symmetric_from_pre : pre_symmetric -> symmetric. --Proof. by move=> symR x y; apply/idP/idP; apply: symR. Qed. -- --Definition reflexive := forall x, R x x. --Definition irreflexive := forall x, R x x = false. -- --Definition left_transitive := forall x y, R x y -> R x =1 R y. --Definition right_transitive := forall x y, R x y -> R^~ x =1 R^~ y. -- --Section PER. -- --Hypotheses (symR : symmetric) (trR : transitive). -- --Lemma sym_left_transitive : left_transitive. --Proof. by move=> x y Rxy z; apply/idP/idP; apply: trR; rewrite // symR. Qed. -- --Lemma sym_right_transitive : right_transitive. --Proof. by move=> x y /sym_left_transitive Rxy z; rewrite !(symR z) Rxy. Qed. -- --End PER. -- --(* We define the equivalence property with prenex quantification so that it *) --(* can be localized using the {in ..., ..} form defined below. *) -- --Definition equivalence_rel := forall x y z, R z z * (R x y -> R x z = R y z). -- --Lemma equivalence_relP : equivalence_rel <-> reflexive /\ left_transitive. --Proof. --split=> [eqiR | [Rxx trR] x y z]; last by split=> [|/trR->]. --by split=> [x | x y Rxy z]; [rewrite (eqiR x x x) | rewrite (eqiR x y z)]. --Qed. -- --End RelationProperties. -- --Lemma rev_trans T (R : rel T) : transitive R -> transitive (fun x y => R y x). --Proof. by move=> trR x y z Ryx Rzy; apply: trR Rzy Ryx. Qed. -- --(* Property localization *) -- --Local Notation "{ 'all1' P }" := (forall x, P x : Prop) (at level 0). --Local Notation "{ 'all2' P }" := (forall x y, P x y : Prop) (at level 0). --Local Notation "{ 'all3' P }" := (forall x y z, P x y z: Prop) (at level 0). --Local Notation ph := (phantom _). -- --Section LocalProperties. -- --Variables T1 T2 T3 : Type. -- --Variables (d1 : mem_pred T1) (d2 : mem_pred T2) (d3 : mem_pred T3). --Local Notation ph := (phantom Prop). -- --Definition prop_for (x : T1) P & ph {all1 P} := P x. -- --Lemma forE x P phP : @prop_for x P phP = P x. Proof. by []. Qed. -- --Definition prop_in1 P & ph {all1 P} := -- forall x, in_mem x d1 -> P x. -- --Definition prop_in11 P & ph {all2 P} := -- forall x y, in_mem x d1 -> in_mem y d2 -> P x y. -- --Definition prop_in2 P & ph {all2 P} := -- forall x y, in_mem x d1 -> in_mem y d1 -> P x y. -- --Definition prop_in111 P & ph {all3 P} := -- forall x y z, in_mem x d1 -> in_mem y d2 -> in_mem z d3 -> P x y z. -- --Definition prop_in12 P & ph {all3 P} := -- forall x y z, in_mem x d1 -> in_mem y d2 -> in_mem z d2 -> P x y z. -- --Definition prop_in21 P & ph {all3 P} := -- forall x y z, in_mem x d1 -> in_mem y d1 -> in_mem z d2 -> P x y z. -- --Definition prop_in3 P & ph {all3 P} := -- forall x y z, in_mem x d1 -> in_mem y d1 -> in_mem z d1 -> P x y z. -- --Variable f : T1 -> T2. -- --Definition prop_on1 Pf P & phantom T3 (Pf f) & ph {all1 P} := -- forall x, in_mem (f x) d2 -> P x. -- --Definition prop_on2 Pf P & phantom T3 (Pf f) & ph {all2 P} := -- forall x y, in_mem (f x) d2 -> in_mem (f y) d2 -> P x y. -- --End LocalProperties. -- --Definition inPhantom := Phantom Prop. --Definition onPhantom T P (x : T) := Phantom Prop (P x). -- --Definition bijective_in aT rT (d : mem_pred aT) (f : aT -> rT) := -- exists2 g, prop_in1 d (inPhantom (cancel f g)) -- & prop_on1 d (Phantom _ (cancel g)) (onPhantom (cancel g) f). -- --Definition bijective_on aT rT (cd : mem_pred rT) (f : aT -> rT) := -- exists2 g, prop_on1 cd (Phantom _ (cancel f)) (onPhantom (cancel f) g) -- & prop_in1 cd (inPhantom (cancel g f)). -- --Notation "{ 'for' x , P }" := -- (prop_for x (inPhantom P)) -- (at level 0, format "{ 'for' x , P }") : type_scope. -- --Notation "{ 'in' d , P }" := -- (prop_in1 (mem d) (inPhantom P)) -- (at level 0, format "{ 'in' d , P }") : type_scope. -- --Notation "{ 'in' d1 & d2 , P }" := -- (prop_in11 (mem d1) (mem d2) (inPhantom P)) -- (at level 0, format "{ 'in' d1 & d2 , P }") : type_scope. -- --Notation "{ 'in' d & , P }" := -- (prop_in2 (mem d) (inPhantom P)) -- (at level 0, format "{ 'in' d & , P }") : type_scope. -- --Notation "{ 'in' d1 & d2 & d3 , P }" := -- (prop_in111 (mem d1) (mem d2) (mem d3) (inPhantom P)) -- (at level 0, format "{ 'in' d1 & d2 & d3 , P }") : type_scope. -- --Notation "{ 'in' d1 & & d3 , P }" := -- (prop_in21 (mem d1) (mem d3) (inPhantom P)) -- (at level 0, format "{ 'in' d1 & & d3 , P }") : type_scope. -- --Notation "{ 'in' d1 & d2 & , P }" := -- (prop_in12 (mem d1) (mem d2) (inPhantom P)) -- (at level 0, format "{ 'in' d1 & d2 & , P }") : type_scope. -- --Notation "{ 'in' d & & , P }" := -- (prop_in3 (mem d) (inPhantom P)) -- (at level 0, format "{ 'in' d & & , P }") : type_scope. -- --Notation "{ 'on' cd , P }" := -- (prop_on1 (mem cd) (inPhantom P) (inPhantom P)) -- (at level 0, format "{ 'on' cd , P }") : type_scope. -- --Notation "{ 'on' cd & , P }" := -- (prop_on2 (mem cd) (inPhantom P) (inPhantom P)) -- (at level 0, format "{ 'on' cd & , P }") : type_scope. -- --Local Arguments onPhantom {_%type_scope} _ _. -- --Notation "{ 'on' cd , P & g }" := -- (prop_on1 (mem cd) (Phantom (_ -> Prop) P) (onPhantom P g)) -- (at level 0, format "{ 'on' cd , P & g }") : type_scope. -- --Notation "{ 'in' d , 'bijective' f }" := (bijective_in (mem d) f) -- (at level 0, f at level 8, -- format "{ 'in' d , 'bijective' f }") : type_scope. -- --Notation "{ 'on' cd , 'bijective' f }" := (bijective_on (mem cd) f) -- (at level 0, f at level 8, -- format "{ 'on' cd , 'bijective' f }") : type_scope. -- --(* Weakening and monotonicity lemmas for localized predicates. *) --(* Note that using these lemmas in backward reasoning will force expansion of *) --(* the predicate definition, as Coq needs to expose the quantifier to apply *) --(* these lemmas. We define a few specialized variants to avoid this for some *) --(* of the ssrfun predicates. *) -- --Section LocalGlobal. -- --Variables T1 T2 T3 : predArgType. --Variables (D1 : pred T1) (D2 : pred T2) (D3 : pred T3). --Variables (d1 d1' : mem_pred T1) (d2 d2' : mem_pred T2) (d3 d3' : mem_pred T3). --Variables (f f' : T1 -> T2) (g : T2 -> T1) (h : T3). --Variables (P1 : T1 -> Prop) (P2 : T1 -> T2 -> Prop). --Variable P3 : T1 -> T2 -> T3 -> Prop. --Variable Q1 : (T1 -> T2) -> T1 -> Prop. --Variable Q1l : (T1 -> T2) -> T3 -> T1 -> Prop. --Variable Q2 : (T1 -> T2) -> T1 -> T1 -> Prop. -- --Hypothesis sub1 : sub_mem d1 d1'. --Hypothesis sub2 : sub_mem d2 d2'. --Hypothesis sub3 : sub_mem d3 d3'. -- --Lemma in1W : {all1 P1} -> {in D1, {all1 P1}}. --Proof. by move=> ? ?. Qed. --Lemma in2W : {all2 P2} -> {in D1 & D2, {all2 P2}}. --Proof. by move=> ? ?. Qed. --Lemma in3W : {all3 P3} -> {in D1 & D2 & D3, {all3 P3}}. --Proof. by move=> ? ?. Qed. -- --Lemma in1T : {in T1, {all1 P1}} -> {all1 P1}. --Proof. by move=> ? ?; auto. Qed. --Lemma in2T : {in T1 & T2, {all2 P2}} -> {all2 P2}. --Proof. by move=> ? ?; auto. Qed. --Lemma in3T : {in T1 & T2 & T3, {all3 P3}} -> {all3 P3}. --Proof. by move=> ? ?; auto. Qed. -- --Lemma sub_in1 (Ph : ph {all1 P1}) : prop_in1 d1' Ph -> prop_in1 d1 Ph. --Proof. by move=> allP x /sub1; apply: allP. Qed. -- --Lemma sub_in11 (Ph : ph {all2 P2}) : prop_in11 d1' d2' Ph -> prop_in11 d1 d2 Ph. --Proof. by move=> allP x1 x2 /sub1 d1x1 /sub2; apply: allP. Qed. -- --Lemma sub_in111 (Ph : ph {all3 P3}) : -- prop_in111 d1' d2' d3' Ph -> prop_in111 d1 d2 d3 Ph. --Proof. by move=> allP x1 x2 x3 /sub1 d1x1 /sub2 d2x2 /sub3; apply: allP. Qed. -- --Let allQ1 f'' := {all1 Q1 f''}. --Let allQ1l f'' h' := {all1 Q1l f'' h'}. --Let allQ2 f'' := {all2 Q2 f''}. -- --Lemma on1W : allQ1 f -> {on D2, allQ1 f}. Proof. by move=> ? ?. Qed. -- --Lemma on1lW : allQ1l f h -> {on D2, allQ1l f & h}. Proof. by move=> ? ?. Qed. -- --Lemma on2W : allQ2 f -> {on D2 &, allQ2 f}. Proof. by move=> ? ?. Qed. -- --Lemma on1T : {on T2, allQ1 f} -> allQ1 f. Proof. by move=> ? ?; auto. Qed. -- --Lemma on1lT : {on T2, allQ1l f & h} -> allQ1l f h. --Proof. by move=> ? ?; auto. Qed. -- --Lemma on2T : {on T2 &, allQ2 f} -> allQ2 f. --Proof. by move=> ? ?; auto. Qed. -- --Lemma subon1 (Phf : ph (allQ1 f)) (Ph : ph (allQ1 f)) : -- prop_on1 d2' Phf Ph -> prop_on1 d2 Phf Ph. --Proof. by move=> allQ x /sub2; apply: allQ. Qed. -- --Lemma subon1l (Phf : ph (allQ1l f)) (Ph : ph (allQ1l f h)) : -- prop_on1 d2' Phf Ph -> prop_on1 d2 Phf Ph. --Proof. by move=> allQ x /sub2; apply: allQ. Qed. -- --Lemma subon2 (Phf : ph (allQ2 f)) (Ph : ph (allQ2 f)) : -- prop_on2 d2' Phf Ph -> prop_on2 d2 Phf Ph. --Proof. by move=> allQ x y /sub2=> d2fx /sub2; apply: allQ. Qed. -- --Lemma can_in_inj : {in D1, cancel f g} -> {in D1 &, injective f}. --Proof. by move=> fK x y /fK{2}<- /fK{2}<- ->. Qed. -- --Lemma canLR_in x y : {in D1, cancel f g} -> y \in D1 -> x = f y -> g x = y. --Proof. by move=> fK D1y ->; rewrite fK. Qed. -- --Lemma canRL_in x y : {in D1, cancel f g} -> x \in D1 -> f x = y -> x = g y. --Proof. by move=> fK D1x <-; rewrite fK. Qed. -- --Lemma on_can_inj : {on D2, cancel f & g} -> {on D2 &, injective f}. --Proof. by move=> fK x y /fK{2}<- /fK{2}<- ->. Qed. -- --Lemma canLR_on x y : {on D2, cancel f & g} -> f y \in D2 -> x = f y -> g x = y. --Proof. by move=> fK D2fy ->; rewrite fK. Qed. -- --Lemma canRL_on x y : {on D2, cancel f & g} -> f x \in D2 -> f x = y -> x = g y. --Proof. by move=> fK D2fx <-; rewrite fK. Qed. -- --Lemma inW_bij : bijective f -> {in D1, bijective f}. --Proof. by case=> g' fK g'K; exists g' => * ? *; auto. Qed. -- --Lemma onW_bij : bijective f -> {on D2, bijective f}. --Proof. by case=> g' fK g'K; exists g' => * ? *; auto. Qed. -- --Lemma inT_bij : {in T1, bijective f} -> bijective f. --Proof. by case=> g' fK g'K; exists g' => * ? *; auto. Qed. -- --Lemma onT_bij : {on T2, bijective f} -> bijective f. --Proof. by case=> g' fK g'K; exists g' => * ? *; auto. Qed. -- --Lemma sub_in_bij (D1' : pred T1) : -- {subset D1 <= D1'} -> {in D1', bijective f} -> {in D1, bijective f}. --Proof. --by move=> subD [g' fK g'K]; exists g' => x; move/subD; [apply: fK | apply: g'K]. --Qed. -- --Lemma subon_bij (D2' : pred T2) : -- {subset D2 <= D2'} -> {on D2', bijective f} -> {on D2, bijective f}. --Proof. --by move=> subD [g' fK g'K]; exists g' => x; move/subD; [apply: fK | apply: g'K]. --Qed. -- --End LocalGlobal. -- --Lemma sub_in2 T d d' (P : T -> T -> Prop) : -- sub_mem d d' -> forall Ph : ph {all2 P}, prop_in2 d' Ph -> prop_in2 d Ph. --Proof. by move=> /= sub_dd'; apply: sub_in11. Qed. -- --Lemma sub_in3 T d d' (P : T -> T -> T -> Prop) : -- sub_mem d d' -> forall Ph : ph {all3 P}, prop_in3 d' Ph -> prop_in3 d Ph. --Proof. by move=> /= sub_dd'; apply: sub_in111. Qed. -- --Lemma sub_in12 T1 T d1 d1' d d' (P : T1 -> T -> T -> Prop) : -- sub_mem d1 d1' -> sub_mem d d' -> -- forall Ph : ph {all3 P}, prop_in12 d1' d' Ph -> prop_in12 d1 d Ph. --Proof. by move=> /= sub1 sub; apply: sub_in111. Qed. -- --Lemma sub_in21 T T3 d d' d3 d3' (P : T -> T -> T3 -> Prop) : -- sub_mem d d' -> sub_mem d3 d3' -> -- forall Ph : ph {all3 P}, prop_in21 d' d3' Ph -> prop_in21 d d3 Ph. --Proof. by move=> /= sub sub3; apply: sub_in111. Qed. -- --Lemma equivalence_relP_in T (R : rel T) (A : pred T) : -- {in A & &, equivalence_rel R} -- <-> {in A, reflexive R} /\ {in A &, forall x y, R x y -> {in A, R x =1 R y}}. --Proof. --split=> [eqiR | [Rxx trR] x y z *]; last by split=> [|/trR-> //]; apply: Rxx. --by split=> [x Ax|x y Ax Ay Rxy z Az]; [rewrite (eqiR x x) | rewrite (eqiR x y)]. --Qed. -- --Section MonoHomoMorphismTheory. -- --Variables (aT rT sT : Type) (f : aT -> rT) (g : rT -> aT). --Variables (aP : pred aT) (rP : pred rT) (aR : rel aT) (rR : rel rT). -- --Lemma monoW : {mono f : x / aP x >-> rP x} -> {homo f : x / aP x >-> rP x}. --Proof. by move=> hf x ax; rewrite hf. Qed. -- --Lemma mono2W : -- {mono f : x y / aR x y >-> rR x y} -> {homo f : x y / aR x y >-> rR x y}. --Proof. by move=> hf x y axy; rewrite hf. Qed. -- --Hypothesis fgK : cancel g f. -- --Lemma homoRL : -- {homo f : x y / aR x y >-> rR x y} -> forall x y, aR (g x) y -> rR x (f y). --Proof. by move=> Hf x y /Hf; rewrite fgK. Qed. -- --Lemma homoLR : -- {homo f : x y / aR x y >-> rR x y} -> forall x y, aR x (g y) -> rR (f x) y. --Proof. by move=> Hf x y /Hf; rewrite fgK. Qed. -- --Lemma homo_mono : -- {homo f : x y / aR x y >-> rR x y} -> {homo g : x y / rR x y >-> aR x y} -> -- {mono g : x y / rR x y >-> aR x y}. --Proof. --move=> mf mg x y; case: (boolP (rR _ _))=> [/mg //|]. --by apply: contraNF=> /mf; rewrite !fgK. --Qed. -- --Lemma monoLR : -- {mono f : x y / aR x y >-> rR x y} -> forall x y, rR (f x) y = aR x (g y). --Proof. by move=> mf x y; rewrite -{1}[y]fgK mf. Qed. -- --Lemma monoRL : -- {mono f : x y / aR x y >-> rR x y} -> forall x y, rR x (f y) = aR (g x) y. --Proof. by move=> mf x y; rewrite -{1}[x]fgK mf. Qed. -- --Lemma can_mono : -- {mono f : x y / aR x y >-> rR x y} -> {mono g : x y / rR x y >-> aR x y}. --Proof. by move=> mf x y /=; rewrite -mf !fgK. Qed. -- --End MonoHomoMorphismTheory. -- --Section MonoHomoMorphismTheory_in. -- --Variables (aT rT sT : predArgType) (f : aT -> rT) (g : rT -> aT). --Variable (aD : pred aT). --Variable (aP : pred aT) (rP : pred rT) (aR : rel aT) (rR : rel rT). -- --Notation rD := [pred x | g x \in aD]. -- --Lemma monoW_in : -- {in aD &, {mono f : x y / aR x y >-> rR x y}} -> -- {in aD &, {homo f : x y / aR x y >-> rR x y}}. --Proof. by move=> hf x y hx hy axy; rewrite hf. Qed. -- --Lemma mono2W_in : -- {in aD, {mono f : x / aP x >-> rP x}} -> -- {in aD, {homo f : x / aP x >-> rP x}}. --Proof. by move=> hf x hx ax; rewrite hf. Qed. -- --Hypothesis fgK_on : {on aD, cancel g & f}. -- --Lemma homoRL_in : -- {in aD &, {homo f : x y / aR x y >-> rR x y}} -> -- {in rD & aD, forall x y, aR (g x) y -> rR x (f y)}. --Proof. by move=> Hf x y hx hy /Hf; rewrite fgK_on //; apply. Qed. -- --Lemma homoLR_in : -- {in aD &, {homo f : x y / aR x y >-> rR x y}} -> -- {in aD & rD, forall x y, aR x (g y) -> rR (f x) y}. --Proof. by move=> Hf x y hx hy /Hf; rewrite fgK_on //; apply. Qed. -- --Lemma homo_mono_in : -- {in aD &, {homo f : x y / aR x y >-> rR x y}} -> -- {in rD &, {homo g : x y / rR x y >-> aR x y}} -> -- {in rD &, {mono g : x y / rR x y >-> aR x y}}. --Proof. --move=> mf mg x y hx hy; case: (boolP (rR _ _))=> [/mg //|]; first exact. --by apply: contraNF=> /mf; rewrite !fgK_on //; apply. --Qed. -- --Lemma monoLR_in : -- {in aD &, {mono f : x y / aR x y >-> rR x y}} -> -- {in aD & rD, forall x y, rR (f x) y = aR x (g y)}. --Proof. by move=> mf x y hx hy; rewrite -{1}[y]fgK_on // mf. Qed. -- --Lemma monoRL_in : -- {in aD &, {mono f : x y / aR x y >-> rR x y}} -> -- {in rD & aD, forall x y, rR x (f y) = aR (g x) y}. --Proof. by move=> mf x y hx hy; rewrite -{1}[x]fgK_on // mf. Qed. -- --Lemma can_mono_in : -- {in aD &, {mono f : x y / aR x y >-> rR x y}} -> -- {in rD &, {mono g : x y / rR x y >-> aR x y}}. --Proof. by move=> mf x y hx hy /=; rewrite -mf // !fgK_on. Qed. -- --End MonoHomoMorphismTheory_in. ---- a/plugins/ssr/ssrfun.v -+++ /dev/null -@@ -1,796 +0,0 @@ --(************************************************************************) --(* * The Coq Proof Assistant / The Coq Development Team *) --(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) --(* <O___,, * (see CREDITS file for the list of authors) *) --(* \VV/ **************************************************************) --(* // * This file is distributed under the terms of the *) --(* * GNU Lesser General Public License Version 2.1 *) --(* * (see LICENSE file for the text of the license) *) --(************************************************************************) -- --(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -- --Require Import ssreflect. -- --(******************************************************************************) --(* This file contains the basic definitions and notations for working with *) --(* functions. The definitions provide for: *) --(* *) --(* - Pair projections: *) --(* p.1 == first element of a pair *) --(* p.2 == second element of a pair *) --(* These notations also apply to p : P /\ Q, via an and >-> pair coercion. *) --(* *) --(* - Simplifying functions, beta-reduced by /= and simpl: *) --(* [fun : T => E] == constant function from type T that returns E *) --(* [fun x => E] == unary function *) --(* [fun x : T => E] == unary function with explicit domain type *) --(* [fun x y => E] == binary function *) --(* [fun x y : T => E] == binary function with common domain type *) --(* [fun (x : T) y => E] \ *) --(* [fun (x : xT) (y : yT) => E] | == binary function with (some) explicit, *) --(* [fun x (y : T) => E] / independent domain types for each argument *) --(* *) --(* - Partial functions using option type: *) --(* oapp f d ox == if ox is Some x returns f x, d otherwise *) --(* odflt d ox == if ox is Some x returns x, d otherwise *) --(* obind f ox == if ox is Some x returns f x, None otherwise *) --(* omap f ox == if ox is Some x returns Some (f x), None otherwise *) --(* *) --(* - Singleton types: *) --(* all_equal_to x0 == x0 is the only value in its type, so any such value *) --(* can be rewritten to x0. *) --(* *) --(* - A generic wrapper type: *) --(* wrapped T == the inductive type with values Wrap x for x : T. *) --(* unwrap w == the projection of w : wrapped T on T. *) --(* wrap x == the canonical injection of x : T into wrapped T; it is *) --(* equivalent to Wrap x, but is declared as a (default) *) --(* Canonical Structure, which lets the Coq HO unification *) --(* automatically expand x into unwrap (wrap x). The delta *) --(* reduction of wrap x to Wrap can be exploited to *) --(* introduce controlled nondeterminism in Canonical *) --(* Structure inference, as in the implementation of *) --(* the mxdirect predicate in matrix.v. *) --(* *) --(* - Sigma types: *) --(* tag w == the i of w : {i : I & T i}. *) --(* tagged w == the T i component of w : {i : I & T i}. *) --(* Tagged T x == the {i : I & T i} with component x : T i. *) --(* tag2 w == the i of w : {i : I & T i & U i}. *) --(* tagged2 w == the T i component of w : {i : I & T i & U i}. *) --(* tagged2' w == the U i component of w : {i : I & T i & U i}. *) --(* Tagged2 T U x y == the {i : I & T i} with components x : T i and y : U i. *) --(* sval u == the x of u : {x : T | P x}. *) --(* s2val u == the x of u : {x : T | P x & Q x}. *) --(* The properties of sval u, s2val u are given by lemmas svalP, s2valP, and *) --(* s2valP'. We provide coercions sigT2 >-> sigT and sig2 >-> sig >-> sigT. *) --(* A suite of lemmas (all_sig, ...) let us skolemize sig, sig2, sigT, sigT2 *) --(* and pair, e.g., *) --(* have /all_sig[f fP] (x : T): {y : U | P y} by ... *) --(* yields an f : T -> U such that fP : forall x, P (f x). *) --(* - Identity functions: *) --(* id == NOTATION for the explicit identity function fun x => x. *) --(* @id T == notation for the explicit identity at type T. *) --(* idfun == an expression with a head constant, convertible to id; *) --(* idfun x simplifies to x. *) --(* @idfun T == the expression above, specialized to type T. *) --(* phant_id x y == the function type phantom _ x -> phantom _ y. *) --(* *** In addition to their casual use in functional programming, identity *) --(* functions are often used to trigger static unification as part of the *) --(* construction of dependent Records and Structures. For example, if we need *) --(* a structure sT over a type T, we take as arguments T, sT, and a "dummy" *) --(* function T -> sort sT: *) --(* Definition foo T sT & T -> sort sT := ... *) --(* We can avoid specifying sT directly by calling foo (@id T), or specify *) --(* the call completely while still ensuring the consistency of T and sT, by *) --(* calling @foo T sT idfun. The phant_id type allows us to extend this trick *) --(* to non-Type canonical projections. It also allows us to sidestep *) --(* dependent type constraints when building explicit records, e.g., given *) --(* Record r := R {x; y : T(x)}. *) --(* if we need to build an r from a given y0 while inferring some x0, such *) --(* that y0 : T(x0), we pose *) --(* Definition mk_r .. y .. (x := ...) y' & phant_id y y' := R x y'. *) --(* Calling @mk_r .. y0 .. id will cause Coq to use y' := y0, while checking *) --(* the dependent type constraint y0 : T(x0). *) --(* *) --(* - Extensional equality for functions and relations (i.e. functions of two *) --(* arguments): *) --(* f1 =1 f2 == f1 x is equal to f2 x for all x. *) --(* f1 =1 f2 :> A == ... and f2 is explicitly typed. *) --(* f1 =2 f2 == f1 x y is equal to f2 x y for all x y. *) --(* f1 =2 f2 :> A == ... and f2 is explicitly typed. *) --(* *) --(* - Composition for total and partial functions: *) --(* f^~ y == function f with second argument specialised to y, *) --(* i.e., fun x => f x y *) --(* CAVEAT: conditional (non-maximal) implicit arguments *) --(* of f are NOT inserted in this context *) --(* @^~ x == application at x, i.e., fun f => f x *) --(* [eta f] == the explicit eta-expansion of f, i.e., fun x => f x *) --(* CAVEAT: conditional (non-maximal) implicit arguments *) --(* of f are NOT inserted in this context. *) --(* fun=> v := the constant function fun _ => v. *) --(* f1 \o f2 == composition of f1 and f2. *) --(* Note: (f1 \o f2) x simplifies to f1 (f2 x). *) --(* f1 \; f2 == categorical composition of f1 and f2. This expands to *) --(* to f2 \o f1 and (f1 \; f2) x simplifies to f2 (f1 x). *) --(* pcomp f1 f2 == composition of partial functions f1 and f2. *) --(* *) --(* *) --(* - Properties of functions: *) --(* injective f <-> f is injective. *) --(* cancel f g <-> g is a left inverse of f / f is a right inverse of g. *) --(* pcancel f g <-> g is a left inverse of f where g is partial. *) --(* ocancel f g <-> g is a left inverse of f where f is partial. *) --(* bijective f <-> f is bijective (has a left and right inverse). *) --(* involutive f <-> f is involutive. *) --(* *) --(* - Properties for operations. *) --(* left_id e op <-> e is a left identity for op (e op x = x). *) --(* right_id e op <-> e is a right identity for op (x op e = x). *) --(* left_inverse e inv op <-> inv is a left inverse for op wrt identity e, *) --(* i.e., (inv x) op x = e. *) --(* right_inverse e inv op <-> inv is a right inverse for op wrt identity e *) --(* i.e., x op (i x) = e. *) --(* self_inverse e op <-> each x is its own op-inverse (x op x = e). *) --(* idempotent op <-> op is idempotent for op (x op x = x). *) --(* associative op <-> op is associative, i.e., *) --(* x op (y op z) = (x op y) op z. *) --(* commutative op <-> op is commutative (x op y = y op x). *) --(* left_commutative op <-> op is left commutative, i.e., *) --(* x op (y op z) = y op (x op z). *) --(* right_commutative op <-> op is right commutative, i.e., *) --(* (x op y) op z = (x op z) op y. *) --(* left_zero z op <-> z is a left zero for op (z op x = z). *) --(* right_zero z op <-> z is a right zero for op (x op z = z). *) --(* left_distributive op1 op2 <-> op1 distributes over op2 to the left: *) --(* (x op2 y) op1 z = (x op1 z) op2 (y op1 z). *) --(* right_distributive op1 op2 <-> op distributes over add to the right: *) --(* x op1 (y op2 z) = (x op1 z) op2 (x op1 z). *) --(* interchange op1 op2 <-> op1 and op2 satisfy an interchange law: *) --(* (x op2 y) op1 (z op2 t) = (x op1 z) op2 (y op1 t). *) --(* Note that interchange op op is a commutativity property. *) --(* left_injective op <-> op is injective in its left argument: *) --(* x op y = z op y -> x = z. *) --(* right_injective op <-> op is injective in its right argument: *) --(* x op y = x op z -> y = z. *) --(* left_loop inv op <-> op, inv obey the inverse loop left axiom: *) --(* (inv x) op (x op y) = y for all x, y, i.e., *) --(* op (inv x) is always a left inverse of op x *) --(* rev_left_loop inv op <-> op, inv obey the inverse loop reverse left *) --(* axiom: x op ((inv x) op y) = y, for all x, y. *) --(* right_loop inv op <-> op, inv obey the inverse loop right axiom: *) --(* (x op y) op (inv y) = x for all x, y. *) --(* rev_right_loop inv op <-> op, inv obey the inverse loop reverse right *) --(* axiom: (x op y) op (inv y) = x for all x, y. *) --(* Note that familiar "cancellation" identities like x + y - y = x or *) --(* x - y + y = x are respectively instances of right_loop and rev_right_loop *) --(* The corresponding lemmas will use the K and NK/VK suffixes, respectively. *) --(* *) --(* - Morphisms for functions and relations: *) --(* {morph f : x / a >-> r} <-> f is a morphism with respect to functions *) --(* (fun x => a) and (fun x => r); if r == R[x], *) --(* this states that f a = R[f x] for all x. *) --(* {morph f : x / a} <-> f is a morphism with respect to the *) --(* function expression (fun x => a). This is *) --(* shorthand for {morph f : x / a >-> a}; note *) --(* that the two instances of a are often *) --(* interpreted at different types. *) --(* {morph f : x y / a >-> r} <-> f is a morphism with respect to functions *) --(* (fun x y => a) and (fun x y => r). *) --(* {morph f : x y / a} <-> f is a morphism with respect to the *) --(* function expression (fun x y => a). *) --(* {homo f : x / a >-> r} <-> f is a homomorphism with respect to the *) --(* predicates (fun x => a) and (fun x => r); *) --(* if r == R[x], this states that a -> R[f x] *) --(* for all x. *) --(* {homo f : x / a} <-> f is a homomorphism with respect to the *) --(* predicate expression (fun x => a). *) --(* {homo f : x y / a >-> r} <-> f is a homomorphism with respect to the *) --(* relations (fun x y => a) and (fun x y => r). *) --(* {homo f : x y / a} <-> f is a homomorphism with respect to the *) --(* relation expression (fun x y => a). *) --(* {mono f : x / a >-> r} <-> f is monotone with respect to projectors *) --(* (fun x => a) and (fun x => r); if r == R[x], *) --(* this states that R[f x] = a for all x. *) --(* {mono f : x / a} <-> f is monotone with respect to the projector *) --(* expression (fun x => a). *) --(* {mono f : x y / a >-> r} <-> f is monotone with respect to relators *) --(* (fun x y => a) and (fun x y => r). *) --(* {mono f : x y / a} <-> f is monotone with respect to the relator *) --(* expression (fun x y => a). *) --(* *) --(* The file also contains some basic lemmas for the above concepts. *) --(* Lemmas relative to cancellation laws use some abbreviated suffixes: *) --(* K - a cancellation rule like esymK : cancel (@esym T x y) (@esym T y x). *) --(* LR - a lemma moving an operation from the left hand side of a relation to *) --(* the right hand side, like canLR: cancel g f -> x = g y -> f x = y. *) --(* RL - a lemma moving an operation from the right to the left, e.g., canRL. *) --(* Beware that the LR and RL orientations refer to an "apply" (back chaining) *) --(* usage; when using the same lemmas with "have" or "move" (forward chaining) *) --(* the directions will be reversed!. *) --(******************************************************************************) -- --Set Implicit Arguments. --Unset Strict Implicit. --Unset Printing Implicit Defensive. -- --Delimit Scope fun_scope with FUN. --Open Scope fun_scope. -- --(* Notations for argument transpose *) --Notation "f ^~ y" := (fun x => f x y) -- (at level 10, y at level 8, no associativity, format "f ^~ y") : fun_scope. --Notation "@^~ x" := (fun f => f x) -- (at level 10, x at level 8, no associativity, format "@^~ x") : fun_scope. -- --Delimit Scope pair_scope with PAIR. --Open Scope pair_scope. -- --(* Notations for pair/conjunction projections *) --Notation "p .1" := (fst p) -- (at level 2, left associativity, format "p .1") : pair_scope. --Notation "p .2" := (snd p) -- (at level 2, left associativity, format "p .2") : pair_scope. -- --Coercion pair_of_and P Q (PandQ : P /\ Q) := (proj1 PandQ, proj2 PandQ). -- --Definition all_pair I T U (w : forall i : I, T i * U i) := -- (fun i => (w i).1, fun i => (w i).2). -- --(* Complements on the option type constructor, used below to *) --(* encode partial functions. *) -- --Module Option. -- --Definition apply aT rT (f : aT -> rT) x u := if u is Some y then f y else x. -- --Definition default T := apply (fun x : T => x). -- --Definition bind aT rT (f : aT -> option rT) := apply f None. -- --Definition map aT rT (f : aT -> rT) := bind (fun x => Some (f x)). -- --End Option. -- --Notation oapp := Option.apply. --Notation odflt := Option.default. --Notation obind := Option.bind. --Notation omap := Option.map. --Notation some := (@Some _) (only parsing). -- --(* Shorthand for some basic equality lemmas. *) -- --Notation erefl := refl_equal. --Notation ecast i T e x := (let: erefl in _ = i := e return T in x). --Definition esym := sym_eq. --Definition nesym := sym_not_eq. --Definition etrans := trans_eq. --Definition congr1 := f_equal. --Definition congr2 := f_equal2. --(* Force at least one implicit when used as a view. *) --Prenex Implicits esym nesym. -- --(* A predicate for singleton types. *) --Definition all_equal_to T (x0 : T) := forall x, unkeyed x = x0. -- --Lemma unitE : all_equal_to tt. Proof. by case. Qed. -- --(* A generic wrapper type *) -- --Structure wrapped T := Wrap {unwrap : T}. --Canonical wrap T x := @Wrap T x. -- --Prenex Implicits unwrap wrap Wrap. -- --(* Syntax for defining auxiliary recursive function. *) --(* Usage: *) --(* Section FooDefinition. *) --(* Variables (g1 : T1) (g2 : T2). (globals) *) --(* Fixoint foo_auxiliary (a3 : T3) ... := *) --(* body, using [rec e3, ...] for recursive calls *) --(* where "[ 'rec' a3 , a4 , ... ]" := foo_auxiliary. *) --(* Definition foo x y .. := [rec e1, ...]. *) --(* + proofs about foo *) --(* End FooDefinition. *) -- --Reserved Notation "[ 'rec' a0 ]" -- (at level 0, format "[ 'rec' a0 ]"). --Reserved Notation "[ 'rec' a0 , a1 ]" -- (at level 0, format "[ 'rec' a0 , a1 ]"). --Reserved Notation "[ 'rec' a0 , a1 , a2 ]" -- (at level 0, format "[ 'rec' a0 , a1 , a2 ]"). --Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 ]" -- (at level 0, format "[ 'rec' a0 , a1 , a2 , a3 ]"). --Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 , a4 ]" -- (at level 0, format "[ 'rec' a0 , a1 , a2 , a3 , a4 ]"). --Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 ]" -- (at level 0, format "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 ]"). --Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 ]" -- (at level 0, format "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 ]"). --Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 , a7 ]" -- (at level 0, -- format "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 , a7 ]"). --Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 , a7 , a8 ]" -- (at level 0, -- format "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 , a7 , a8 ]"). --Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 , a7 , a8 , a9 ]" -- (at level 0, -- format "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 , a7 , a8 , a9 ]"). -- --(* Definitions and notation for explicit functions with simplification, *) --(* i.e., which simpl and /= beta expand (this is complementary to nosimpl). *) -- --Section SimplFun. -- --Variables aT rT : Type. -- --CoInductive simpl_fun := SimplFun of aT -> rT. -- --Definition fun_of_simpl f := fun x => let: SimplFun lam := f in lam x. -- --Coercion fun_of_simpl : simpl_fun >-> Funclass. -- --End SimplFun. -- --Notation "[ 'fun' : T => E ]" := (SimplFun (fun _ : T => E)) -- (at level 0, -- format "'[hv' [ 'fun' : T => '/ ' E ] ']'") : fun_scope. -- --Notation "[ 'fun' x => E ]" := (SimplFun (fun x => E)) -- (at level 0, x ident, -- format "'[hv' [ 'fun' x => '/ ' E ] ']'") : fun_scope. -- --Notation "[ 'fun' x : T => E ]" := (SimplFun (fun x : T => E)) -- (at level 0, x ident, only parsing) : fun_scope. -- --Notation "[ 'fun' x y => E ]" := (fun x => [fun y => E]) -- (at level 0, x ident, y ident, -- format "'[hv' [ 'fun' x y => '/ ' E ] ']'") : fun_scope. -- --Notation "[ 'fun' x y : T => E ]" := (fun x : T => [fun y : T => E]) -- (at level 0, x ident, y ident, only parsing) : fun_scope. -- --Notation "[ 'fun' ( x : T ) y => E ]" := (fun x : T => [fun y => E]) -- (at level 0, x ident, y ident, only parsing) : fun_scope. -- --Notation "[ 'fun' x ( y : T ) => E ]" := (fun x => [fun y : T => E]) -- (at level 0, x ident, y ident, only parsing) : fun_scope. -- --Notation "[ 'fun' ( x : xT ) ( y : yT ) => E ]" := -- (fun x : xT => [fun y : yT => E]) -- (at level 0, x ident, y ident, only parsing) : fun_scope. -- --(* For delta functions in eqtype.v. *) --Definition SimplFunDelta aT rT (f : aT -> aT -> rT) := [fun z => f z z]. -- --(* Extensional equality, for unary and binary functions, including syntactic *) --(* sugar. *) -- --Section ExtensionalEquality. -- --Variables A B C : Type. -- --Definition eqfun (f g : B -> A) : Prop := forall x, f x = g x. -- --Definition eqrel (r s : C -> B -> A) : Prop := forall x y, r x y = s x y. -- --Lemma frefl f : eqfun f f. Proof. by []. Qed. --Lemma fsym f g : eqfun f g -> eqfun g f. Proof. by move=> eq_fg x. Qed. -- --Lemma ftrans f g h : eqfun f g -> eqfun g h -> eqfun f h. --Proof. by move=> eq_fg eq_gh x; rewrite eq_fg. Qed. -- --Lemma rrefl r : eqrel r r. Proof. by []. Qed. -- --End ExtensionalEquality. -- --Typeclasses Opaque eqfun. --Typeclasses Opaque eqrel. -- --Hint Resolve frefl rrefl. -- --Notation "f1 =1 f2" := (eqfun f1 f2) -- (at level 70, no associativity) : fun_scope. --Notation "f1 =1 f2 :> A" := (f1 =1 (f2 : A)) -- (at level 70, f2 at next level, A at level 90) : fun_scope. --Notation "f1 =2 f2" := (eqrel f1 f2) -- (at level 70, no associativity) : fun_scope. --Notation "f1 =2 f2 :> A" := (f1 =2 (f2 : A)) -- (at level 70, f2 at next level, A at level 90) : fun_scope. -- --Section Composition. -- --Variables A B C : Type. -- --Definition funcomp u (f : B -> A) (g : C -> B) x := let: tt := u in f (g x). --Definition catcomp u g f := funcomp u f g. --Local Notation comp := (funcomp tt). -- --Definition pcomp (f : B -> option A) (g : C -> option B) x := obind f (g x). -- --Lemma eq_comp f f' g g' : f =1 f' -> g =1 g' -> comp f g =1 comp f' g'. --Proof. by move=> eq_ff' eq_gg' x; rewrite /= eq_gg' eq_ff'. Qed. -- --End Composition. -- --Notation comp := (funcomp tt). --Notation "@ 'comp'" := (fun A B C => @funcomp A B C tt). --Notation "f1 \o f2" := (comp f1 f2) -- (at level 50, format "f1 \o '/ ' f2") : fun_scope. --Notation "f1 \; f2" := (catcomp tt f1 f2) -- (at level 60, right associativity, format "f1 \; '/ ' f2") : fun_scope. -- --Notation "[ 'eta' f ]" := (fun x => f x) -- (at level 0, format "[ 'eta' f ]") : fun_scope. -- --Notation "'fun' => E" := (fun _ => E) (at level 200, only parsing) : fun_scope. -- --Notation id := (fun x => x). --Notation "@ 'id' T" := (fun x : T => x) -- (at level 10, T at level 8, only parsing) : fun_scope. -- --Definition id_head T u x : T := let: tt := u in x. --Definition explicit_id_key := tt. --Notation idfun := (id_head tt). --Notation "@ 'idfun' T " := (@id_head T explicit_id_key) -- (at level 10, T at level 8, format "@ 'idfun' T") : fun_scope. -- --Definition phant_id T1 T2 v1 v2 := phantom T1 v1 -> phantom T2 v2. -- --(* Strong sigma types. *) -- --Section Tag. -- --Variables (I : Type) (i : I) (T_ U_ : I -> Type). -- --Definition tag := projT1. --Definition tagged : forall w, T_(tag w) := @projT2 I [eta T_]. --Definition Tagged x := @existT I [eta T_] i x. -- --Definition tag2 (w : @sigT2 I T_ U_) := let: existT2 _ _ i _ _ := w in i. --Definition tagged2 w : T_(tag2 w) := let: existT2 _ _ _ x _ := w in x. --Definition tagged2' w : U_(tag2 w) := let: existT2 _ _ _ _ y := w in y. --Definition Tagged2 x y := @existT2 I [eta T_] [eta U_] i x y. -- --End Tag. -- --Arguments Tagged [I i]. --Arguments Tagged2 [I i]. --Prenex Implicits tag tagged Tagged tag2 tagged2 tagged2' Tagged2. -- --Coercion tag_of_tag2 I T_ U_ (w : @sigT2 I T_ U_) := -- Tagged (fun i => T_ i * U_ i)%type (tagged2 w, tagged2' w). -- --Lemma all_tag I T U : -- (forall x : I, {y : T x & U x y}) -> -- {f : forall x, T x & forall x, U x (f x)}. --Proof. by move=> fP; exists (fun x => tag (fP x)) => x; case: (fP x). Qed. -- --Lemma all_tag2 I T U V : -- (forall i : I, {y : T i & U i y & V i y}) -> -- {f : forall i, T i & forall i, U i (f i) & forall i, V i (f i)}. --Proof. by case/all_tag=> f /all_pair[]; exists f. Qed. -- --(* Refinement types. *) -- --(* Prenex Implicits and renaming. *) --Notation sval := (@proj1_sig _ _). --Notation "@ 'sval'" := (@proj1_sig) (at level 10, format "@ 'sval'"). -- --Section Sig. -- --Variables (T : Type) (P Q : T -> Prop). -- --Lemma svalP (u : sig P) : P (sval u). Proof. by case: u. Qed. -- --Definition s2val (u : sig2 P Q) := let: exist2 _ _ x _ _ := u in x. -- --Lemma s2valP u : P (s2val u). Proof. by case: u. Qed. -- --Lemma s2valP' u : Q (s2val u). Proof. by case: u. Qed. -- --End Sig. -- --Prenex Implicits svalP s2val s2valP s2valP'. -- --Coercion tag_of_sig I P (u : @sig I P) := Tagged P (svalP u). -- --Coercion sig_of_sig2 I P Q (u : @sig2 I P Q) := -- exist (fun i => P i /\ Q i) (s2val u) (conj (s2valP u) (s2valP' u)). -- --Lemma all_sig I T P : -- (forall x : I, {y : T x | P x y}) -> -- {f : forall x, T x | forall x, P x (f x)}. --Proof. by case/all_tag=> f; exists f. Qed. -- --Lemma all_sig2 I T P Q : -- (forall x : I, {y : T x | P x y & Q x y}) -> -- {f : forall x, T x | forall x, P x (f x) & forall x, Q x (f x)}. --Proof. by case/all_sig=> f /all_pair[]; exists f. Qed. -- --Section Morphism. -- --Variables (aT rT sT : Type) (f : aT -> rT). -- --(* Morphism property for unary and binary functions *) --Definition morphism_1 aF rF := forall x, f (aF x) = rF (f x). --Definition morphism_2 aOp rOp := forall x y, f (aOp x y) = rOp (f x) (f y). -- --(* Homomorphism property for unary and binary relations *) --Definition homomorphism_1 (aP rP : _ -> Prop) := forall x, aP x -> rP (f x). --Definition homomorphism_2 (aR rR : _ -> _ -> Prop) := -- forall x y, aR x y -> rR (f x) (f y). -- --(* Stability property for unary and binary relations *) --Definition monomorphism_1 (aP rP : _ -> sT) := forall x, rP (f x) = aP x. --Definition monomorphism_2 (aR rR : _ -> _ -> sT) := -- forall x y, rR (f x) (f y) = aR x y. -- --End Morphism. -- --Notation "{ 'morph' f : x / a >-> r }" := -- (morphism_1 f (fun x => a) (fun x => r)) -- (at level 0, f at level 99, x ident, -- format "{ 'morph' f : x / a >-> r }") : type_scope. -- --Notation "{ 'morph' f : x / a }" := -- (morphism_1 f (fun x => a) (fun x => a)) -- (at level 0, f at level 99, x ident, -- format "{ 'morph' f : x / a }") : type_scope. -- --Notation "{ 'morph' f : x y / a >-> r }" := -- (morphism_2 f (fun x y => a) (fun x y => r)) -- (at level 0, f at level 99, x ident, y ident, -- format "{ 'morph' f : x y / a >-> r }") : type_scope. -- --Notation "{ 'morph' f : x y / a }" := -- (morphism_2 f (fun x y => a) (fun x y => a)) -- (at level 0, f at level 99, x ident, y ident, -- format "{ 'morph' f : x y / a }") : type_scope. -- --Notation "{ 'homo' f : x / a >-> r }" := -- (homomorphism_1 f (fun x => a) (fun x => r)) -- (at level 0, f at level 99, x ident, -- format "{ 'homo' f : x / a >-> r }") : type_scope. -- --Notation "{ 'homo' f : x / a }" := -- (homomorphism_1 f (fun x => a) (fun x => a)) -- (at level 0, f at level 99, x ident, -- format "{ 'homo' f : x / a }") : type_scope. -- --Notation "{ 'homo' f : x y / a >-> r }" := -- (homomorphism_2 f (fun x y => a) (fun x y => r)) -- (at level 0, f at level 99, x ident, y ident, -- format "{ 'homo' f : x y / a >-> r }") : type_scope. -- --Notation "{ 'homo' f : x y / a }" := -- (homomorphism_2 f (fun x y => a) (fun x y => a)) -- (at level 0, f at level 99, x ident, y ident, -- format "{ 'homo' f : x y / a }") : type_scope. -- --Notation "{ 'homo' f : x y /~ a }" := -- (homomorphism_2 f (fun y x => a) (fun x y => a)) -- (at level 0, f at level 99, x ident, y ident, -- format "{ 'homo' f : x y /~ a }") : type_scope. -- --Notation "{ 'mono' f : x / a >-> r }" := -- (monomorphism_1 f (fun x => a) (fun x => r)) -- (at level 0, f at level 99, x ident, -- format "{ 'mono' f : x / a >-> r }") : type_scope. -- --Notation "{ 'mono' f : x / a }" := -- (monomorphism_1 f (fun x => a) (fun x => a)) -- (at level 0, f at level 99, x ident, -- format "{ 'mono' f : x / a }") : type_scope. -- --Notation "{ 'mono' f : x y / a >-> r }" := -- (monomorphism_2 f (fun x y => a) (fun x y => r)) -- (at level 0, f at level 99, x ident, y ident, -- format "{ 'mono' f : x y / a >-> r }") : type_scope. -- --Notation "{ 'mono' f : x y / a }" := -- (monomorphism_2 f (fun x y => a) (fun x y => a)) -- (at level 0, f at level 99, x ident, y ident, -- format "{ 'mono' f : x y / a }") : type_scope. -- --Notation "{ 'mono' f : x y /~ a }" := -- (monomorphism_2 f (fun y x => a) (fun x y => a)) -- (at level 0, f at level 99, x ident, y ident, -- format "{ 'mono' f : x y /~ a }") : type_scope. -- --(* In an intuitionistic setting, we have two degrees of injectivity. The *) --(* weaker one gives only simplification, and the strong one provides a left *) --(* inverse (we show in `fintype' that they coincide for finite types). *) --(* We also define an intermediate version where the left inverse is only a *) --(* partial function. *) -- --Section Injections. -- --(* rT must come first so we can use @ to mitigate the Coq 1st order *) --(* unification bug (e..g., Coq can't infer rT from a "cancel" lemma). *) --Variables (rT aT : Type) (f : aT -> rT). -- --Definition injective := forall x1 x2, f x1 = f x2 -> x1 = x2. -- --Definition cancel g := forall x, g (f x) = x. -- --Definition pcancel g := forall x, g (f x) = Some x. -- --Definition ocancel (g : aT -> option rT) h := forall x, oapp h x (g x) = x. -- --Lemma can_pcan g : cancel g -> pcancel (fun y => Some (g y)). --Proof. by move=> fK x; congr (Some _). Qed. -- --Lemma pcan_inj g : pcancel g -> injective. --Proof. by move=> fK x y /(congr1 g); rewrite !fK => [[]]. Qed. -- --Lemma can_inj g : cancel g -> injective. --Proof. by move/can_pcan; apply: pcan_inj. Qed. -- --Lemma canLR g x y : cancel g -> x = f y -> g x = y. --Proof. by move=> fK ->. Qed. -- --Lemma canRL g x y : cancel g -> f x = y -> x = g y. --Proof. by move=> fK <-. Qed. -- --End Injections. -- --Lemma Some_inj {T} : injective (@Some T). Proof. by move=> x y []. Qed. -- --(* Force implicits to use as a view. *) --Prenex Implicits Some_inj. -- --(* cancellation lemmas for dependent type casts. *) --Lemma esymK T x y : cancel (@esym T x y) (@esym T y x). --Proof. by case: y /. Qed. -- --Lemma etrans_id T x y (eqxy : x = y :> T) : etrans (erefl x) eqxy = eqxy. --Proof. by case: y / eqxy. Qed. -- --Section InjectionsTheory. -- --Variables (A B C : Type) (f g : B -> A) (h : C -> B). -- --Lemma inj_id : injective (@id A). --Proof. by []. Qed. -- --Lemma inj_can_sym f' : cancel f f' -> injective f' -> cancel f' f. --Proof. by move=> fK injf' x; apply: injf'. Qed. -- --Lemma inj_comp : injective f -> injective h -> injective (f \o h). --Proof. by move=> injf injh x y /injf; apply: injh. Qed. -- --Lemma can_comp f' h' : cancel f f' -> cancel h h' -> cancel (f \o h) (h' \o f'). --Proof. by move=> fK hK x; rewrite /= fK hK. Qed. -- --Lemma pcan_pcomp f' h' : -- pcancel f f' -> pcancel h h' -> pcancel (f \o h) (pcomp h' f'). --Proof. by move=> fK hK x; rewrite /pcomp fK /= hK. Qed. -- --Lemma eq_inj : injective f -> f =1 g -> injective g. --Proof. by move=> injf eqfg x y; rewrite -2!eqfg; apply: injf. Qed. -- --Lemma eq_can f' g' : cancel f f' -> f =1 g -> f' =1 g' -> cancel g g'. --Proof. by move=> fK eqfg eqfg' x; rewrite -eqfg -eqfg'. Qed. -- --Lemma inj_can_eq f' : cancel f f' -> injective f' -> cancel g f' -> f =1 g. --Proof. by move=> fK injf' gK x; apply: injf'; rewrite fK. Qed. -- --End InjectionsTheory. -- --Section Bijections. -- --Variables (A B : Type) (f : B -> A). -- --CoInductive bijective : Prop := Bijective g of cancel f g & cancel g f. -- --Hypothesis bijf : bijective. -- --Lemma bij_inj : injective f. --Proof. by case: bijf => g fK _; apply: can_inj fK. Qed. -- --Lemma bij_can_sym f' : cancel f' f <-> cancel f f'. --Proof. --split=> fK; first exact: inj_can_sym fK bij_inj. --by case: bijf => h _ hK x; rewrite -[x]hK fK. --Qed. -- --Lemma bij_can_eq f' f'' : cancel f f' -> cancel f f'' -> f' =1 f''. --Proof. --by move=> fK fK'; apply: (inj_can_eq _ bij_inj); apply/bij_can_sym. --Qed. -- --End Bijections. -- --Section BijectionsTheory. -- --Variables (A B C : Type) (f : B -> A) (h : C -> B). -- --Lemma eq_bij : bijective f -> forall g, f =1 g -> bijective g. --Proof. by case=> f' fK f'K g eqfg; exists f'; eapply eq_can; eauto. Qed. -- --Lemma bij_comp : bijective f -> bijective h -> bijective (f \o h). --Proof. --by move=> [f' fK f'K] [h' hK h'K]; exists (h' \o f'); apply: can_comp; auto. --Qed. -- --Lemma bij_can_bij : bijective f -> forall f', cancel f f' -> bijective f'. --Proof. by move=> bijf; exists f; first by apply/(bij_can_sym bijf). Qed. -- --End BijectionsTheory. -- --Section Involutions. -- --Variables (A : Type) (f : A -> A). -- --Definition involutive := cancel f f. -- --Hypothesis Hf : involutive. -- --Lemma inv_inj : injective f. Proof. exact: can_inj Hf. Qed. --Lemma inv_bij : bijective f. Proof. by exists f. Qed. -- --End Involutions. -- --Section OperationProperties. -- --Variables S T R : Type. -- --Section SopTisR. --Implicit Type op : S -> T -> R. --Definition left_inverse e inv op := forall x, op (inv x) x = e. --Definition right_inverse e inv op := forall x, op x (inv x) = e. --Definition left_injective op := forall x, injective (op^~ x). --Definition right_injective op := forall y, injective (op y). --End SopTisR. -- -- --Section SopTisS. --Implicit Type op : S -> T -> S. --Definition right_id e op := forall x, op x e = x. --Definition left_zero z op := forall x, op z x = z. --Definition right_commutative op := forall x y z, op (op x y) z = op (op x z) y. --Definition left_distributive op add := -- forall x y z, op (add x y) z = add (op x z) (op y z). --Definition right_loop inv op := forall y, cancel (op^~ y) (op^~ (inv y)). --Definition rev_right_loop inv op := forall y, cancel (op^~ (inv y)) (op^~ y). --End SopTisS. -- --Section SopTisT. --Implicit Type op : S -> T -> T. --Definition left_id e op := forall x, op e x = x. --Definition right_zero z op := forall x, op x z = z. --Definition left_commutative op := forall x y z, op x (op y z) = op y (op x z). --Definition right_distributive op add := -- forall x y z, op x (add y z) = add (op x y) (op x z). --Definition left_loop inv op := forall x, cancel (op x) (op (inv x)). --Definition rev_left_loop inv op := forall x, cancel (op (inv x)) (op x). --End SopTisT. -- --Section SopSisT. --Implicit Type op : S -> S -> T. --Definition self_inverse e op := forall x, op x x = e. --Definition commutative op := forall x y, op x y = op y x. --End SopSisT. -- --Section SopSisS. --Implicit Type op : S -> S -> S. --Definition idempotent op := forall x, op x x = x. --Definition associative op := forall x y z, op x (op y z) = op (op x y) z. --Definition interchange op1 op2 := -- forall x y z t, op1 (op2 x y) (op2 z t) = op2 (op1 x z) (op1 y t). --End SopSisS. -- --End OperationProperties. -- -- -- -- -- -- -- -- -- -- ---- a/test-suite/bugs/closed/2800.v -+++ /dev/null -@@ -1,19 +0,0 @@ --Goal False. -- --intuition -- match goal with -- | |- _ => idtac " foo" -- end. -- -- lazymatch goal with _ => idtac end. -- match goal with _ => idtac end. -- unshelve lazymatch goal with _ => idtac end. -- unshelve match goal with _ => idtac end. -- unshelve (let x := I in idtac). --Abort. -- --Require Import ssreflect. -- --Goal True. --match goal with _ => idtac end => //. --Qed. ---- a/test-suite/bugs/closed/5692.v -+++ /dev/null -@@ -1,88 +0,0 @@ --Set Primitive Projections. --Require Import ZArith ssreflect. -- --Module Test1. -- --Structure semigroup := SemiGroup { -- sg_car :> Type; -- sg_op : sg_car -> sg_car -> sg_car; --}. -- --Structure monoid := Monoid { -- monoid_car :> Type; -- monoid_op : monoid_car -> monoid_car -> monoid_car; -- monoid_unit : monoid_car; --}. -- --Coercion monoid_sg (X : monoid) : semigroup := -- SemiGroup (monoid_car X) (monoid_op X). --Canonical Structure monoid_sg. -- --Parameter X : monoid. --Parameter x y : X. -- --Check (sg_op _ x y). -- --End Test1. -- --Module Test2. -- --Structure semigroup := SemiGroup { -- sg_car :> Type; -- sg_op : sg_car -> sg_car -> sg_car; --}. -- --Structure monoid := Monoid { -- monoid_car :> Type; -- monoid_op : monoid_car -> monoid_car -> monoid_car; -- monoid_unit : monoid_car; -- monoid_left_id x : monoid_op monoid_unit x = x; --}. -- --Coercion monoid_sg (X : monoid) : semigroup := -- SemiGroup (monoid_car X) (monoid_op X). --Canonical Structure monoid_sg. -- --Canonical Structure nat_sg := SemiGroup nat plus. --Canonical Structure nat_monoid := Monoid nat plus 0 plus_O_n. -- --Lemma foo (x : nat) : 0 + x = x. --Proof. --apply monoid_left_id. --Qed. -- --End Test2. -- --Module Test3. -- --Structure semigroup := SemiGroup { -- sg_car :> Type; -- sg_op : sg_car -> sg_car -> sg_car; --}. -- --Structure group := Something { -- group_car :> Type; -- group_op : group_car -> group_car -> group_car; -- group_neg : group_car -> group_car; -- group_neg_op' x y : group_neg (group_op x y) = group_op (group_neg x) (group_neg y) --}. -- --Coercion group_sg (X : group) : semigroup := -- SemiGroup (group_car X) (group_op X). --Canonical Structure group_sg. -- --Axiom group_neg_op : forall (X : group) (x y : X), -- group_neg X (sg_op (group_sg X) x y) = sg_op (group_sg X) (group_neg X x) (group_neg X y). -- --Canonical Structure Z_sg := SemiGroup Z Z.add . --Canonical Structure Z_group := Something Z Z.add Z.opp Z.opp_add_distr. -- --Lemma foo (x y : Z) : -- sg_op Z_sg (group_neg Z_group x) (group_neg Z_group y) = -- group_neg Z_group (sg_op Z_sg x y). --Proof. -- rewrite -group_neg_op. -- reflexivity. --Qed. -- --End Test3. ---- a/test-suite/bugs/closed/6634.v -+++ /dev/null -@@ -1,6 +0,0 @@ --From Coq Require Import ssreflect. -- --Lemma normalizeP (p : tt = tt) : p = p. --Proof. --Fail move: {2} tt p. --Abort. ---- a/test-suite/bugs/closed/6910.v -+++ /dev/null -@@ -1,5 +0,0 @@ --From Coq Require Import ssreflect ssrfun. -- --(* We should be able to use Some_inj as a view: *) --Lemma foo (x y : nat) : Some x = Some y -> x = y. --Proof. by move/Some_inj. Qed. ---- a/test-suite/output/ssr_clear.v -+++ /dev/null -@@ -1,6 +0,0 @@ --Require Import ssreflect. -- --Example foo : True -> True. --Proof. --Fail move=> {NO_SUCH_NAME}. --Abort. ---- a/test-suite/success/ssr_delayed_clear_rename.v -+++ /dev/null -@@ -1,5 +0,0 @@ --Require Import ssreflect. --Example foo (t t1 t2 : True) : True /\ True -> True -> True. --Proof. --move=>[{t1 t2 t} t1 t2] t. --Abort. diff --git a/debian/patches/0005-ssrmatching-license.patch b/debian/patches/0005-ssrmatching-license.patch new file mode 100644 index 00000000..f207cc8b --- /dev/null +++ b/debian/patches/0005-ssrmatching-license.patch @@ -0,0 +1,298 @@ +From: Benjamin Barenblat <bbaren@debian.org> +Subject: Replace deleted non-free ssrmatching files with free ones +Forwarded: not-needed +Last-Update: 2019-01-17 + +Coq 8.8.2 shipped with two files in ssrmatching that were licensed under +CeCILL-B, which I believe is a nonfree license. I've removed them from +the Debian source package (see gbp.conf). This patch replaces them with +equivalent files (from a later version) that are licensed freely. + +These files are present starting at upstream commit +f613d9f9f0c8aec814272f6c2dcdce7e70da47b6. I've modified them by where required +to get them to compile against 8.8.2. +--- /dev/null ++++ b/plugins/ssrmatching/ssrmatching.mli +@@ -0,0 +1,242 @@ ++(************************************************************************) ++(* * The Coq Proof Assistant / The Coq Development Team *) ++(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) ++(* <O___,, * (see CREDITS file for the list of authors) *) ++(* \VV/ **************************************************************) ++(* // * This file is distributed under the terms of the *) ++(* * GNU Lesser General Public License Version 2.1 *) ++(* * (see LICENSE file for the text of the license) *) ++(************************************************************************) ++ ++(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) ++ ++open Goal ++open Environ ++open Evd ++open Constr ++open Genintern ++ ++(** ******** Small Scale Reflection pattern matching facilities ************* *) ++ ++(** Pattern parsing *) ++ ++(** The type of context patterns, the patterns of the [set] tactic and ++ [:] tactical. These are patterns that identify a precise subterm. *) ++type cpattern ++val pr_cpattern : cpattern -> Pp.t ++ ++(** The type of rewrite patterns, the patterns of the [rewrite] tactic. ++ These patterns also include patterns that identify all the subterms ++ of a context (i.e. "in" prefix) *) ++type rpattern ++val pr_rpattern : rpattern -> Pp.t ++ ++(** Pattern interpretation and matching *) ++ ++exception NoMatch ++exception NoProgress ++ ++(** AST for [rpattern] (and consequently [cpattern]) *) ++type ('ident, 'term) ssrpattern = ++ | T of 'term ++ | In_T of 'term ++ | X_In_T of 'ident * 'term ++ | In_X_In_T of 'ident * 'term ++ | E_In_X_In_T of 'term * 'ident * 'term ++ | E_As_X_In_T of 'term * 'ident * 'term ++ ++type pattern = evar_map * (constr, constr) ssrpattern ++val pp_pattern : pattern -> Pp.t ++ ++(** Extracts the redex and applies to it the substitution part of the pattern. ++ @raise Anomaly if called on [In_T] or [In_X_In_T] *) ++val redex_of_pattern : ++ ?resolve_typeclasses:bool -> env -> pattern -> ++ constr Evd.in_evar_universe_context ++ ++(** [interp_rpattern ise gl rpat] "internalizes" and "interprets" [rpat] ++ in the current [Ltac] interpretation signature [ise] and tactic input [gl]*) ++val interp_rpattern : ++ goal sigma -> ++ rpattern -> ++ pattern ++ ++(** [interp_cpattern ise gl cpat ty] "internalizes" and "interprets" [cpat] ++ in the current [Ltac] interpretation signature [ise] and tactic input [gl]. ++ [ty] is an optional type for the redex of [cpat] *) ++val interp_cpattern : ++ goal sigma -> ++ cpattern -> (Tacexpr.glob_constr_and_expr * Geninterp.interp_sign) option -> ++ pattern ++ ++(** The set of occurrences to be matched. The boolean is set to true ++ * to signal the complement of this set (i.e. \{-1 3\}) *) ++type occ = (bool * int list) option ++ ++(** [subst e p t i]. [i] is the number of binders ++ traversed so far, [p] the term from the pattern, [t] the matched one *) ++type subst = env -> constr -> constr -> int -> constr ++ ++(** [eval_pattern b env sigma t pat occ subst] maps [t] calling [subst] on every ++ [occ] occurrence of [pat]. The [int] argument is the number of ++ binders traversed. If [pat] is [None] then then subst is called on [t]. ++ [t] must live in [env] and [sigma], [pat] must have been interpreted in ++ (an extension of) [sigma]. ++ @raise NoMatch if [pat] has no occurrence and [b] is [true] (default [false]) ++ @return [t] where all [occ] occurrences of [pat] have been mapped using ++ [subst] *) ++val eval_pattern : ++ ?raise_NoMatch:bool -> ++ env -> evar_map -> constr -> ++ pattern option -> occ -> subst -> ++ constr ++ ++(** [fill_occ_pattern b env sigma t pat occ h] is a simplified version of ++ [eval_pattern]. ++ It replaces all [occ] occurrences of [pat] in [t] with Rel [h]. ++ [t] must live in [env] and [sigma], [pat] must have been interpreted in ++ (an extension of) [sigma]. ++ @raise NoMatch if [pat] has no occurrence and [b] is [true] (default [false]) ++ @return the instance of the redex of [pat] that was matched and [t] ++ transformed as described above. *) ++val fill_occ_pattern : ++ ?raise_NoMatch:bool -> ++ env -> evar_map -> constr -> ++ pattern -> occ -> int -> ++ constr Evd.in_evar_universe_context * constr ++ ++(** *************************** Low level APIs ****************************** *) ++ ++(* The primitive matching facility. It matches of a term with holes, like ++ the T pattern above, and calls a continuation on its occurrences. *) ++ ++type ssrdir = L2R | R2L ++val pr_dir_side : ssrdir -> Pp.t ++ ++(** a pattern for a term with wildcards *) ++type tpattern ++ ++(** [mk_tpattern env sigma0 sigma_p ok p_origin dir t] compiles a term [t] ++ living in [env] [sigma] (an extension of [sigma0]) intro a [tpattern]. ++ The [tpattern] can hold a (proof) term [p] and a diction [dir]. The [ok] ++ callback is used to filter occurrences. ++ @return the compiled [tpattern] and its [evar_map] ++ @raise UserEerror is the pattern is a wildcard *) ++val mk_tpattern : ++ ?p_origin:ssrdir * constr -> ++ env -> evar_map -> ++ evar_map * constr -> ++ (constr -> evar_map -> bool) -> ++ ssrdir -> constr -> ++ evar_map * tpattern ++ ++(** [findP env t i k] is a stateful function that finds the next occurrence ++ of a tpattern and calls the callback [k] to map the subterm matched. ++ The [int] argument passed to [k] is the number of binders traversed so far ++ plus the initial value [i]. ++ @return [t] where the subterms identified by the selected occurrences of ++ the patter have been mapped using [k] ++ @raise NoMatch if the raise_NoMatch flag given to [mk_tpattern_matcher] is ++ [true] and if the pattern did not match ++ @raise UserEerror if the raise_NoMatch flag given to [mk_tpattern_matcher] is ++ [false] and if the pattern did not match *) ++type find_P = ++ env -> constr -> int -> k:subst -> constr ++ ++(** [conclude ()] asserts that all mentioned ocurrences have been visited. ++ @return the instance of the pattern, the evarmap after the pattern ++ instantiation, the proof term and the ssrdit stored in the tpattern ++ @raise UserEerror if too many occurrences were specified *) ++type conclude = ++ unit -> constr * ssrdir * (evar_map * UState.t * constr) ++ ++(** [mk_tpattern_matcher b o sigma0 occ sigma_tplist] creates a pair ++ a function [find_P] and [conclude] with the behaviour explained above. ++ The flag [b] (default [false]) changes the error reporting behaviour ++ of [find_P] if none of the [tpattern] matches. The argument [o] can ++ be passed to tune the [UserError] eventually raised (useful if the ++ pattern is coming from the LHS/RHS of an equation) *) ++val mk_tpattern_matcher : ++ ?all_instances:bool -> ++ ?raise_NoMatch:bool -> ++ ?upats_origin:ssrdir * constr -> ++ evar_map -> occ -> evar_map * tpattern list -> ++ find_P * conclude ++ ++(** Example of [mk_tpattern_matcher] to implement ++ [rewrite \{occ\}\[in t\]rules]. ++ It first matches "in t" (called [pat]), then in all matched subterms ++ it matches the LHS of the rules using [find_R]. ++ [concl0] is the initial goal, [concl] will be the goal where some terms ++ are replaced by a De Bruijn index. The [rw_progress] extra check ++ selects only occurrences that are not rewritten to themselves (e.g. ++ an occurrence "x + x" rewritten with the commutativity law of addition ++ is skipped) {[ ++ let find_R, conclude = match pat with ++ | Some (_, In_T _) -> ++ let aux (sigma, pats) (d, r, lhs, rhs) = ++ let sigma, pat = ++ mk_tpattern env0 sigma0 (sigma, r) (rw_progress rhs) d lhs in ++ sigma, pats @ [pat] in ++ let rpats = List.fold_left aux (r_sigma, []) rules in ++ let find_R, end_R = mk_tpattern_matcher sigma0 occ rpats in ++ find_R ~k:(fun _ _ h -> mkRel h), ++ fun cl -> let rdx, d, r = end_R () in (d,r),rdx ++ | _ -> ... in ++ let concl = eval_pattern env0 sigma0 concl0 pat occ find_R in ++ let (d, r), rdx = conclude concl in ]} *) ++ ++(* convenience shortcut: [pf_fill_occ_term gl occ (sigma,t)] returns ++ * the conclusion of [gl] where [occ] occurrences of [t] have been replaced ++ * by [Rel 1] and the instance of [t] *) ++val pf_fill_occ_term : goal sigma -> occ -> evar_map * EConstr.t -> EConstr.t * EConstr.t ++ ++(* It may be handy to inject a simple term into the first form of cpattern *) ++val cpattern_of_term : char * Tacexpr.glob_constr_and_expr -> Geninterp.interp_sign -> cpattern ++ ++(** Helpers to make stateful closures. Example: a [find_P] function may be ++ called many times, but the pattern instantiation phase is performed only the ++ first time. The corresponding [conclude] has to return the instantiated ++ pattern redex. Since it is up to [find_P] to raise [NoMatch] if the pattern ++ has no instance, [conclude] considers it an anomaly if the pattern did ++ not match *) ++ ++(** [do_once r f] calls [f] and updates the ref only once *) ++val do_once : 'a option ref -> (unit -> 'a) -> unit ++ ++(** [assert_done r] return the content of r. @raise Anomaly is r is [None] *) ++val assert_done : 'a option ref -> 'a ++ ++(** Very low level APIs. ++ these are calls to evarconv's [the_conv_x] followed by ++ [solve_unif_constraints_with_heuristics]. ++ In case of failure they raise [NoMatch] *) ++ ++val unify_HO : env -> evar_map -> EConstr.constr -> EConstr.constr -> evar_map ++val pf_unify_HO : goal sigma -> EConstr.constr -> EConstr.constr -> goal sigma ++ ++(** Some more low level functions needed to implement the full SSR language ++ on top of the former APIs *) ++val tag_of_cpattern : cpattern -> char ++val loc_of_cpattern : cpattern -> Loc.t option ++val id_of_pattern : pattern -> Names.Id.t option ++val is_wildcard : cpattern -> bool ++val cpattern_of_id : Names.Id.t -> cpattern ++val pr_constr_pat : constr -> Pp.t ++val pf_merge_uc : UState.t -> goal Evd.sigma -> goal Evd.sigma ++val pf_unsafe_merge_uc : UState.t -> goal Evd.sigma -> goal Evd.sigma ++ ++(* One can also "Set SsrMatchingDebug" from a .v *) ++val debug : bool -> unit ++ ++val ssrinstancesof : cpattern -> Tacmach.tactic ++ ++val profile : bool -> unit ++val wit_cpattern : cpattern Genarg.uniform_genarg_type ++val lcpattern : cpattern Pcoq.Gram.entry ++val wit_lcpattern : cpattern Genarg.uniform_genarg_type ++val cpattern : cpattern Pcoq.Gram.entry ++val wit_rpattern : rpattern Genarg.uniform_genarg_type ++val rpattern : rpattern Pcoq.Gram.entry ++ ++(* eof *) +--- /dev/null ++++ b/plugins/ssrmatching/ssrmatching.v +@@ -0,0 +1,37 @@ ++(************************************************************************) ++(* * The Coq Proof Assistant / The Coq Development Team *) ++(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) ++(* <O___,, * (see CREDITS file for the list of authors) *) ++(* \VV/ **************************************************************) ++(* // * This file is distributed under the terms of the *) ++(* * GNU Lesser General Public License Version 2.1 *) ++(* * (see LICENSE file for the text of the license) *) ++(************************************************************************) ++ ++(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) ++ ++Declare ML Module "ssrmatching_plugin". ++ ++Module SsrMatchingSyntax. ++ ++(* Reserve the notation for rewrite patterns so that the user is not allowed *) ++(* to declare it at a different level. *) ++Reserved Notation "( a 'in' b )" (at level 0). ++Reserved Notation "( a 'as' b )" (at level 0). ++Reserved Notation "( a 'in' b 'in' c )" (at level 0). ++Reserved Notation "( a 'as' b 'in' c )" (at level 0). ++ ++Delimit Scope ssrpatternscope with pattern. ++ ++(* Notation to define shortcuts for the "X in t" part of a pattern. *) ++Notation "( X 'in' t )" := (_ : fun X => t) : ssrpatternscope. ++ ++(* Some shortcuts for recurrent "X in t" parts. *) ++Notation RHS := (X in _ = X)%pattern. ++Notation LHS := (X in X = _)%pattern. ++ ++End SsrMatchingSyntax. ++ ++Export SsrMatchingSyntax. ++ ++Tactic Notation "ssrpattern" ssrpatternarg(p) := ssrpattern p . diff --git a/debian/patches/series b/debian/patches/series index 94ba4f69..7253c063 100644 --- a/debian/patches/series +++ b/debian/patches/series @@ -2,7 +2,7 @@ 0002-Remove-test-4429.patch 0003-Remove-3441.v-and-4811.v-due-to-timeout-on-small-pla.patch 0004-5127-fails-on-mips.patch -0005-remove-ssrmatching.patch +0005-ssrmatching-license.patch 0006-remove-tests-that-need-coqlib.patch 0007-spelling.patch 0008-avoid-usr-bin-env.patch |