From 0b1ea03dafcf36880657ba910eec28ab78ccd018 Mon Sep 17 00:00:00 2001 From: Georges Gonthier Date: Thu, 13 Dec 2018 12:55:43 +0100 Subject: Adjust implicits of cancellation lemmas Like injectivity lemmas, instances of cancellation lemmas (whose conclusion is `cancel ? ?`, `{in ?, cancel ? ?}`, `pcancel`, or `ocancel`) are passed to generic lemmas such as `canRL` or `canLR_in`. Thus such lemmas should not have trailing on-demand implicits _just before_ the `cancel` conclusion, as these would be inconvenient to insert (requiring essentially an explicit eta-expansion). We therefore use `Arguments` or `Prenex Implicits` directives to make all such arguments maximally inserted implicits. We don’t, however make other arguments implicit, so as not to spoil direct instantiation of the lemmas (in, e.g., `rewrite -[y](invmK injf)`). We have also tried to do this with lemmas whose statement matches a `cancel`, i.e., ending in `forall x, g (E[x]) = x` (where pattern unification will pick up `f = fun x => E[x]`). We also adjusted implicits of a few stray injectivity lemmas, and defined constants. We provide a shorthand for reindexing a bigop with a permutation. Finally we used the new implicit signatures to simplify proofs that use injectivity or cancellation lemmas. --- mathcomp/ssreflect/choice.v | 12 +++++-- mathcomp/ssreflect/eqtype.v | 64 +++++++++++++++++++---------------- mathcomp/ssreflect/finfun.v | 1 + mathcomp/ssreflect/finset.v | 1 + mathcomp/ssreflect/fintype.v | 32 ++++++++---------- mathcomp/ssreflect/generic_quotient.v | 10 ++++-- mathcomp/ssreflect/tuple.v | 2 +- 7 files changed, 71 insertions(+), 51 deletions(-) (limited to 'mathcomp/ssreflect') diff --git a/mathcomp/ssreflect/choice.v b/mathcomp/ssreflect/choice.v index 6f46832..57b585e 100644 --- a/mathcomp/ssreflect/choice.v +++ b/mathcomp/ssreflect/choice.v @@ -141,6 +141,9 @@ Proof. by case. Qed. End OtherEncodings. +Prenex Implicits seq_of_opt tag_of_pair pair_of_tag opair_of_sum sum_of_opair. +Prenex Implicits seq_of_optK tag_of_pairK pair_of_tagK opair_of_sumK. + (* Generic variable-arity tree type, providing an encoding target for *) (* miscellaneous user datatypes. The GenTree.tree type can be combined with *) (* a sigT type to model multi-sorted concrete datatypes. *) @@ -562,8 +565,8 @@ Export Countable.Exports. Definition unpickle T := Countable.unpickle (Countable.class T). Definition pickle T := Countable.pickle (Countable.class T). -Arguments unpickle {T}. -Prenex Implicits pickle. +Arguments unpickle {T} n. +Arguments pickle {T} x. Section CountableTheory. @@ -609,6 +612,11 @@ Notation "[ 'countMixin' 'of' T 'by' <: ]" := (sub_countMixin _ : Countable.mixin_of T) (at level 0, format "[ 'countMixin' 'of' T 'by' <: ]") : form_scope. +Arguments pickle_inv {T} n. +Arguments pickleK {T} x. +Arguments pickleK_inv {T} x. +Arguments pickle_invK {T} n : rename. + Section SubCountType. Variables (T : choiceType) (P : pred T). diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v index dc3daf0..58ef844 100644 --- a/mathcomp/ssreflect/eqtype.v +++ b/mathcomp/ssreflect/eqtype.v @@ -514,7 +514,8 @@ Structure subType : Type := SubType { _ : forall x Px, val (@Sub x Px) = x }. -Arguments Sub [s]. +(* Generic proof that the second property holds by conversion. *) +(* The vrefl_rect alias is used to flag generic proofs of the first property. *) Lemma vrefl : forall x, P x -> x = x. Proof. by []. Qed. Definition vrefl_rect := vrefl. @@ -522,18 +523,21 @@ Definition clone_subType U v := fun sT & sub_sort sT -> U => fun c Urec cK (sT' := @SubType U v c Urec cK) & phant_id sT' sT => sT'. +Section Theory. + Variable sT : subType. +Local Notation val := (@val sT). +Local Notation Sub x Px := (@Sub sT x Px). + Variant Sub_spec : sT -> Type := SubSpec x Px : Sub_spec (Sub x Px). Lemma SubP u : Sub_spec u. -Proof. by case: sT Sub_spec SubSpec u => T' _ C rec /= _. Qed. +Proof. by case: sT Sub_spec SubSpec u => /= U _ mkU rec _. Qed. -Lemma SubK x Px : @val sT (Sub x Px) = x. -Proof. by case: sT. Qed. +Lemma SubK x Px : val (Sub x Px) = x. Proof. by case: sT. Qed. -Definition insub x := - if @idP (P x) is ReflectT Px then @Some sT (Sub x Px) else None. +Definition insub x := if idP is ReflectT Px then Some (Sub x Px) else None. Definition insubd u0 x := odflt u0 (insub x). @@ -561,49 +565,55 @@ Proof. by move/negPf/insubF. Qed. Lemma isSome_insub : ([eta insub] : pred T) =1 P. Proof. by apply: fsym => x; case: insubP => // /negPf. Qed. -Lemma insubK : ocancel insub (@val _). +Lemma insubK : ocancel insub val. Proof. by move=> x; case: insubP. Qed. -Lemma valP (u : sT) : P (val u). +Lemma valP u : P (val u). Proof. by case/SubP: u => x Px; rewrite SubK. Qed. -Lemma valK : pcancel (@val _) insub. +Lemma valK : pcancel val insub. Proof. by case/SubP=> x Px; rewrite SubK; apply: insubT. Qed. -Lemma val_inj : injective (@val sT). +Lemma val_inj : injective val. Proof. exact: pcan_inj valK. Qed. -Lemma valKd u0 : cancel (@val _) (insubd u0). +Lemma valKd u0 : cancel val (insubd u0). Proof. by move=> u; rewrite /insubd valK. Qed. Lemma val_insubd u0 x : val (insubd u0 x) = if P x then x else val u0. Proof. by rewrite /insubd; case: insubP => [u -> | /negPf->]. Qed. -Lemma insubdK u0 : {in P, cancel (insubd u0) (@val _)}. +Lemma insubdK u0 : {in P, cancel (insubd u0) val}. Proof. by move=> x Px; rewrite /= val_insubd [P x]Px. Qed. -Definition insub_eq x := - let Some_sub Px := Some (Sub x Px : sT) in - let None_sub _ := None in - (if P x as Px return P x = Px -> _ then Some_sub else None_sub) (erefl _). +Let insub_eq_aux x isPx : P x = isPx -> option sT := + if isPx as b return _ = b -> _ then fun Px => Some (Sub x Px) else fun=> None. +Definition insub_eq x := insub_eq_aux (erefl (P x)). Lemma insub_eqE : insub_eq =1 insub. Proof. -rewrite /insub_eq /insub => x; case: {2 3}_ / idP (erefl _) => // Px Px'. -by congr (Some _); apply: val_inj; rewrite !SubK. +rewrite /insub_eq => x; set b := P x; rewrite [in LHS]/b in (Db := erefl b) *. +by case: b in Db *; [rewrite insubT | rewrite insubF]. Qed. +End Theory. + End SubType. -Arguments SubType [T P]. -Arguments Sub {T P s}. -Arguments vrefl {T P}. -Arguments vrefl_rect {T P}. +Arguments SubType {T P} sub_sort val Sub rec SubK. +Arguments val {T P sT} u : rename. +Arguments Sub {T P sT} x Px : rename. +Arguments vrefl {T P} x Px. +Arguments vrefl_rect {T P} x Px. Arguments clone_subType [T P] U v [sT] _ [c Urec cK]. -Arguments insub {T P sT}. +Arguments insub {T P sT} x. +Arguments insubd {T P sT} u0 x. Arguments insubT [T] P [sT x]. -Arguments val_inj {T P sT} [x1 x2]. -Prenex Implicits val insubd. +Arguments val_inj {T P sT} [u1 u2] eq_u12 : rename. +Arguments valK {T P sT} u : rename. +Arguments valKd {T P sT} u0 u : rename. +Arguments insubK {T P} sT x. +Arguments insubdK {T P sT} u0 [x] Px. Local Notation inlined_sub_rect := (fun K K_S u => let (x, Px) as u return K u := u in K_S x Px). @@ -623,10 +633,6 @@ Notation "[ 'subType' 'for' v 'by' rec ]" := (SubType _ v _ rec vrefl) Notation "[ 'subType' 'of' U 'for' v ]" := (clone_subType U v id idfun) (at level 0, format "[ 'subType' 'of' U 'for' v ]") : form_scope. -(* -Notation "[ 'subType' 'for' v ]" := (clone_subType _ v id idfun) - (at level 0, format "[ 'subType' 'for' v ]") : form_scope. -*) Notation "[ 'subType' 'of' U ]" := (clone_subType U _ id id) (at level 0, format "[ 'subType' 'of' U ]") : form_scope. diff --git a/mathcomp/ssreflect/finfun.v b/mathcomp/ssreflect/finfun.v index 9929e82..db1a8e7 100644 --- a/mathcomp/ssreflect/finfun.v +++ b/mathcomp/ssreflect/finfun.v @@ -147,6 +147,7 @@ End PlainTheory. Notation family F := (family_mem (fun_of_simpl (fmem F))). Notation ffun_on R := (ffun_on_mem _ (mem R)). +Arguments ffunK {aT rT}. Arguments familyP {aT rT pT F f}. Arguments ffun_onP {aT rT R f}. diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v index 9ca96c8..87d5da4 100644 --- a/mathcomp/ssreflect/finset.v +++ b/mathcomp/ssreflect/finset.v @@ -2206,6 +2206,7 @@ Qed. End MaxSetMinSet. +Arguments setCK {T}. Arguments minsetP {T P A}. Arguments maxsetP {T P A}. Prenex Implicits minset maxset. diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v index 441fc12..06aca24 100644 --- a/mathcomp/ssreflect/fintype.v +++ b/mathcomp/ssreflect/fintype.v @@ -1485,7 +1485,7 @@ Proof. by rewrite mem_undup mem_pmap -valK map_f ?ssvalP. Qed. Lemma val_seq_sub_enum : uniq s -> map val seq_sub_enum = s. Proof. move=> Us; rewrite /seq_sub_enum undup_id ?pmap_sub_uniq //. -rewrite (pmap_filter (@insubK _ _ _)); apply/all_filterP. +rewrite (pmap_filter (insubK _)); apply/all_filterP. by apply/allP => x; rewrite isSome_insub. Qed. @@ -1646,13 +1646,13 @@ Lemma rev_ord_proof n (i : 'I_n) : n - i.+1 < n. Proof. by case: n i => [|n] [i lt_i_n] //; rewrite ltnS subSS leq_subr. Qed. Definition rev_ord n i := Ordinal (@rev_ord_proof n i). -Lemma rev_ordK n : involutive (@rev_ord n). +Lemma rev_ordK {n} : involutive (@rev_ord n). Proof. by case: n => [|n] [i lti] //; apply: val_inj; rewrite /= !subSS subKn. Qed. Lemma rev_ord_inj {n} : injective (@rev_ord n). -Proof. exact: inv_inj (@rev_ordK n). Qed. +Proof. exact: inv_inj rev_ordK. Qed. (* bijection between any finType T and the Ordinal finType of its cardinal *) Section EnumRank. @@ -1762,7 +1762,7 @@ End EnumRank. Arguments enum_val_inj {T A} [i1 i2] : rename. Arguments enum_rank_inj {T} [x1 x2]. -Prenex Implicits enum_val enum_rank. +Prenex Implicits enum_val enum_rank enum_valK enum_rankK. Lemma enum_rank_ord n i : enum_rank i = cast_ord (esym (card_ord n)) i. Proof. @@ -1800,8 +1800,8 @@ case: (ltngtP i h) => /= [-> | ltih | ->] //; last by rewrite ltnn. by rewrite subn1 /= leqNgt !(ltn_predK ltih, ltih, add1n). Qed. -Lemma unbumpK h : {in predC1 h, cancel (unbump h) (bump h)}. -Proof. by move=> i; move/negbTE=> neq_h_i; rewrite unbumpKcond neq_h_i. Qed. +Lemma unbumpK {h} : {in predC1 h, cancel (unbump h) (bump h)}. +Proof. by move=> i /negbTE-neq_h_i; rewrite unbumpKcond neq_h_i. Qed. Lemma bump_addl h i k : bump (k + h) (k + i) = k + bump h i. Proof. by rewrite /bump leq_add2l addnCA. Qed. @@ -1882,15 +1882,11 @@ by case Dui: (unlift h i) / (unliftP h i) => [j Dh|//]; exists j. Qed. Lemma lift_inj n (h : 'I_n) : injective (lift h). -Proof. -move=> i1 i2; move/eqP; rewrite [_ == _](can_eq (@bumpK _)) => eq_i12. -exact/eqP. -Qed. +Proof. by move=> i1 i2 [/(can_inj (bumpK h))/val_inj]. Qed. +Arguments lift_inj {n h} [i1 i2] eq_i12h : rename. Lemma liftK n (h : 'I_n) : pcancel (lift h) (unlift h). -Proof. -by move=> i; case: (unlift_some (neq_lift h i)) => j; move/lift_inj->. -Qed. +Proof. by move=> i; case: (unlift_some (neq_lift h i)) => j /lift_inj->. Qed. (* Shifting and splitting indices, for cutting and pasting arrays *) @@ -1906,7 +1902,7 @@ Definition rshift m n (i : 'I_n) := Ordinal (rshift_subproof m i). Lemma split_subproof m n (i : 'I_(m + n)) : i >= m -> i - m < n. Proof. by move/subSn <-; rewrite leq_subLR. Qed. -Definition split m n (i : 'I_(m + n)) : 'I_m + 'I_n := +Definition split {m n} (i : 'I_(m + n)) : 'I_m + 'I_n := match ltnP (i) m with | LtnNotGeq lt_i_m => inl _ (Ordinal lt_i_m) | GeqNotLtn ge_i_m => inr _ (Ordinal (split_subproof ge_i_m)) @@ -1922,16 +1918,16 @@ rewrite /split {-3}/leq. by case: (@ltnP i m) => cmp_i_m //=; constructor; rewrite ?subnKC. Qed. -Definition unsplit m n (jk : 'I_m + 'I_n) := +Definition unsplit {m n} (jk : 'I_m + 'I_n) := match jk with inl j => lshift n j | inr k => rshift m k end. Lemma ltn_unsplit m n (jk : 'I_m + 'I_n) : (unsplit jk < m) = jk. Proof. by case: jk => [j|k]; rewrite /= ?ltn_ord // ltnNge leq_addr. Qed. -Lemma splitK m n : cancel (@split m n) (@unsplit m n). +Lemma splitK {m n} : cancel (@split m n) unsplit. Proof. by move=> i; apply: val_inj; case: splitP. Qed. -Lemma unsplitK m n : cancel (@unsplit m n) (@split m n). +Lemma unsplitK {m n} : cancel (@unsplit m n) split. Proof. move=> jk; have:= ltn_unsplit jk. by do [case: splitP; case: jk => //= i j] => [|/addnI] => /ord_inj->. @@ -1979,6 +1975,8 @@ Arguments ord0 {n'}. Arguments ord_max {n'}. Arguments inord {n'}. Arguments sub_ord {n'}. +Arguments sub_ordK {n'}. +Arguments inord_val {n'}. (* Product of two fintypes which is a fintype *) Section ProdFinType. diff --git a/mathcomp/ssreflect/generic_quotient.v b/mathcomp/ssreflect/generic_quotient.v index b7a8444..71fd10a 100644 --- a/mathcomp/ssreflect/generic_quotient.v +++ b/mathcomp/ssreflect/generic_quotient.v @@ -144,6 +144,8 @@ Definition QuotType_clone (Q : Type) qT cT End QuotientDef. +Arguments repr_ofK {T qT}. + (****************************) (* Protecting some symbols. *) (****************************) @@ -195,7 +197,7 @@ Notation QuotType Q m := (@QuotTypePack _ Q m). Notation "[ 'quotType' 'of' Q ]" := (@QuotType_clone _ Q _ _ id) (at level 0, format "[ 'quotType' 'of' Q ]") : form_scope. -Arguments repr {T qT}. +Arguments repr {T qT} x. (************************) (* Exporting the theory *) @@ -227,6 +229,8 @@ Proof. by move=> Py x; rewrite -[x]reprK; apply: Py; rewrite reprK. Qed. End QuotTypeTheory. +Arguments reprK {T qT} x. + (*******************) (* About morphisms *) (*******************) @@ -657,6 +661,8 @@ Canonical EquivQuot.eqType. Canonical EquivQuot.choiceType. Canonical EquivQuot.eqQuotType. +Arguments EquivQuot.ereprK {D C CD DC eD encD}. + Notation "{eq_quot e }" := (@EquivQuot.type_of _ _ _ _ _ _ (Phantom (rel _) e)) : quotient_scope. Notation "x == y %[mod_eq r ]" := (x == y %[mod {eq_quot r}]) : quotient_scope. @@ -690,7 +696,7 @@ Variables (eD : equiv_rel D) (encD : encModRel CD DC eD). Notation eC := (encoded_equiv encD). Fact eq_quot_countMixin : Countable.mixin_of {eq_quot encD}. -Proof. exact: CanCountMixin (@EquivQuot.ereprK _ _ _ _ _ _). Qed. +Proof. exact: CanCountMixin EquivQuot.ereprK. Qed. Canonical eq_quot_countType := CountType {eq_quot encD} eq_quot_countMixin. End CountEncodingModuloRel. diff --git a/mathcomp/ssreflect/tuple.v b/mathcomp/ssreflect/tuple.v index 9154eb5..8f81155 100644 --- a/mathcomp/ssreflect/tuple.v +++ b/mathcomp/ssreflect/tuple.v @@ -336,7 +336,7 @@ Definition enum : seq (n.-tuple T) := Lemma enumP : Finite.axiom enum. Proof. -case=> /= t t_n; rewrite -(count_map _ (pred1 t)) (pmap_filter (@insubK _ _ _)). +case=> /= t t_n; rewrite -(count_map _ (pred1 t)) (pmap_filter (insubK _)). rewrite count_filter -(@eq_count _ (pred1 t)) => [|s /=]; last first. by rewrite isSome_insub; case: eqP=> // ->. elim: n t t_n => [|m IHm] [|x t] //= {IHm}/IHm; move: (iter m _ _) => em IHm. -- cgit v1.2.3