From c0254eaba338a4d308b4e2f200841ff76e6b4b9a Mon Sep 17 00:00:00 2001 From: Georges Gonthier Date: Sun, 31 Mar 2019 03:52:29 +0200 Subject: Permutations and other extensions to seq; fintype documentation - Added `permutations` and some `perm_eq` lemmas suggested by @MrSet in #299 (except the link to the coq lib `Permutation` predicate). Use insertions to construct permutations. This definition is closer to the one proposed by @MrSet, than one using rotations (it adds one line to the definition of `permutations` but the proofs become a little simpler.) - Added support for casts on `map` comprehension general terms. - Added `allpairs_map[lr]` suggested by @pi8027 in #314, but with equational proofs; changed `allpairs_comp` to its converse `map_allpairs` for consistency. - Add three `allpairs` extensionality lemmas: for the non-localised, dependent localised and non-dependent localised cases; as per `eq_in_map`, the latter two are equivalences. - Documented the `all2` predicate added in #224, and the view combinators added in #202. - Renamed `seq2_ind` to `seq_ind2`, and weakened the induction hypothesis, adding a `size` equality assumption. - Corrected the header to use `<=>` for `bool` predicate documentation, and `<->` for `Prop` predicates, following the library’s general convention. - Replaced the `nosimpl` in `rev` with a `Arguments simpl never` directive, making it possible to merge the `Rev` section into the main `Sequences` section. - Miscellaneous improvements to proof scripts and file organisation. - Correct maximal implicits of `constant`. - Fixes omitted `Prenex Implicit` declaration. - Other implicits fixes. - Fix apparent `done` regression It appears `done` now does a weaker form of intros, and this broke the `dtuple_onP` proof. Updated the proof to eliminate the issue. (Commit log edited by @CohenCyril during the squash.) --- mathcomp/ssreflect/fintype.v | 24 +++++++++++++----------- 1 file changed, 13 insertions(+), 11 deletions(-) (limited to 'mathcomp/ssreflect/fintype.v') diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v index 93810ca..c06238c 100644 --- a/mathcomp/ssreflect/fintype.v +++ b/mathcomp/ssreflect/fintype.v @@ -92,9 +92,9 @@ Require Import ssrfun ssrbool eqtype ssrnat seq choice path. (* enum_rank x == the i : 'I_(#|T|) such that enum_val i = x. *) (* enum_rank_in Ax0 x == some i : 'I_(#|A|) such that enum_val i = x if *) (* x \in A, given Ax0 : x0 \in A. *) -(* A \subset B == all x \in A satisfy x \in B. *) -(* A \proper B == all x \in A satisfy x \in B but not the converse. *) -(* [disjoint A & B] == no x \in A satisfies x \in B. *) +(* A \subset B <=> all x \in A satisfy x \in B. *) +(* A \proper B <=> all x \in A satisfy x \in B but not the converse. *) +(* [disjoint A & B] <=> no x \in A satisfies x \in B. *) (* image f A == the sequence of f x for all x : T such that x \in A *) (* (where a is an applicative predicate), of length #|P|. *) (* The codomain of F can be any type, but image f A can *) @@ -108,13 +108,13 @@ Require Import ssrfun ssrbool eqtype ssrnat seq choice path. (* im_y : y \in image f P. *) (* invF inj_f y == the x such that f x = y, for inj_j : injective f with *) (* f : T -> T. *) -(* dinjectiveb A f == the restriction of f : T -> R to A is injective *) +(* dinjectiveb A f <=> the restriction of f : T -> R to A is injective *) (* (this is a bolean predicate, R must be an eqType). *) -(* injectiveb f == f : T -> R is injective (boolean predicate). *) -(* pred0b A == no x : T satisfies x \in A. *) -(* [forall x, P] == P (in which x can appear) is true for all values of x; *) +(* injectiveb f <=> f : T -> R is injective (boolean predicate). *) +(* pred0b A <=> no x : T satisfies x \in A. *) +(* [forall x, P] <=> P (in which x can appear) is true for all values of x *) (* x must range over a finType. *) -(* [exists x, P] == P is true for some value of x. *) +(* [exists x, P] <=> P is true for some value of x. *) (* [forall (x | C), P] := [forall x, C ==> P]. *) (* [forall x in A, P] := [forall (x | x \in A), P]. *) (* [exists (x | C), P] := [exists x, C && P]. *) @@ -123,13 +123,15 @@ Require Import ssrfun ssrbool eqtype ssrnat seq choice path. (* [exists x : T, P], [exists x : T in A, P], etc. *) (* -> The outer brackets can be omitted when nesting finitary quantifiers, *) (* e.g., [forall i in I, forall j in J, exists a, f i j == a]. *) -(* 'forall_pP == view for [forall x, p _], for pP : reflect .. (p _). *) -(* 'exists_pP == view for [exists x, p _], for pP : reflect .. (p _). *) +(* 'forall_pP <-> view for [forall x, p _], for pP : reflect .. (p _). *) +(* 'exists_pP <-> view for [exists x, p _], for pP : reflect .. (p _). *) +(* 'forall_in_pP <-> view for [forall x in .., p _], for pP as above. *) +(* 'exists_in_pP <-> view for [exists x in .., p _], for pP as above. *) (* [pick x | P] == Some x, for an x such that P holds, or None if there *) (* is no such x. *) (* [pick x : T] == Some x with x : T, provided T is nonempty, else None. *) (* [pick x in A] == Some x, with x \in A, or None if A is empty. *) -(* [pick x in A | P] == Some x, with x \in A s.t. P holds, else None. *) +(* [pick x in A | P] == Some x, with x \in A such that P holds, else None. *) (* [pick x | P & Q] := [pick x | P & Q]. *) (* [pick x in A | P & Q] := [pick x | P & Q]. *) (* and (un)typed variants [pick x : T | P], [pick x : T in A], [pick x], etc. *) -- cgit v1.2.3