diff options
| -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 |