diff options
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/ssreflect/Makefile.coq-makefile | 5 | ||||
| -rw-r--r-- | mathcomp/ssreflect/bigop.v | 9 | ||||
| -rw-r--r-- | mathcomp/ssreflect/fingraph.v | 115 | ||||
| -rw-r--r-- | mathcomp/ssreflect/plugin/v8.5/ssreflect_plugin.mllib | 1 | ||||
| -rw-r--r-- | mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4 | 8 | ||||
| -rw-r--r-- | mathcomp/ssreflect/plugin/v8.5/ssrmatching.v | 7 | ||||
| -rw-r--r-- | mathcomp/ssreflect/plugin/v8.5/ssrmatching_plugin.mllib | 1 | ||||
| -rw-r--r-- | mathcomp/ssreflect/seq.v | 13 |
8 files changed, 116 insertions, 43 deletions
diff --git a/mathcomp/ssreflect/Makefile.coq-makefile b/mathcomp/ssreflect/Makefile.coq-makefile index 68bfbc2..bf8115e 100644 --- a/mathcomp/ssreflect/Makefile.coq-makefile +++ b/mathcomp/ssreflect/Makefile.coq-makefile @@ -4,7 +4,8 @@ define coqmakefile MLLIB=;\ EXTRA=;\ case $(V) in\ - v8.5*|v8.4*)\ + v8.5*|v8.4*)\ + $$LN $(1)/plugin/$(V)/ssrmatching_plugin.mllib .;\ $$LN $(1)/plugin/$(V)/ssrmatching.mli .;\ $$LN $(1)/plugin/$(V)/ssrmatching.ml4 .;\ $$LN $(1)/plugin/$(V)/ssrmatching.v .;\ @@ -13,7 +14,7 @@ define coqmakefile $$LN $(1)/plugin/$(V)/ssrbool.v $(1)/;\ $$LN $(1)/plugin/$(V)/ssrfun.v $(1)/;\ $$LN $(1)/plugin/$(V)/ssreflect.v $(1)/;\ - MLLIB=ssreflect_plugin.mllib;\ + MLLIB="ssrmatching_plugin.mllib ssreflect_plugin.mllib";\ EXTRA="ssrmatching.mli ssrmatching.ml4 ssrmatching.v ssreflect.ml4";\ ;;\ v8.6*)\ diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v index a517c8a..67454ac 100644 --- a/mathcomp/ssreflect/bigop.v +++ b/mathcomp/ssreflect/bigop.v @@ -1159,6 +1159,14 @@ rewrite !(big_mkcond _ P) unlock. by elim: r1 => /= [|i r1 ->]; rewrite (mul1m, mulmA). Qed. +Lemma big_allpairs I1 I2 (r1 : seq I1) (r2 : seq I2) F : + \big[*%M/1]_(i <- [seq (i1, i2) | i1 <- r1, i2 <- r2]) F i = + \big[*%M/1]_(i1 <- r1) \big[op/idx]_(i2 <- r2) F (i1, i2). +Proof. +elim: r1 => [|i1 r1 IHr1]; first by rewrite !big_nil. +by rewrite big_cat IHr1 big_cons big_map. +Qed. + Lemma big_pred1_eq (I : finType) (i : I) F : \big[*%M/1]_(j | j == i) F j = F i. Proof. by rewrite -big_filter filter_index_enum enum1 big_seq1. Qed. @@ -1504,6 +1512,7 @@ Implicit Arguments reindex [R op idx I J P F]. Implicit Arguments reindex_inj [R op idx I h P F]. Implicit Arguments pair_big_dep [R op idx I J]. Implicit Arguments pair_big [R op idx I J]. +Implicit Arguments big_allpairs [R op idx I1 I2 r1 r2 F]. Implicit Arguments exchange_big_dep [R op idx I J rI rJ P Q F]. Implicit Arguments exchange_big_dep_nat [R op idx m1 n1 m2 n2 P Q F]. Implicit Arguments big_ord_recl [R op idx]. diff --git a/mathcomp/ssreflect/fingraph.v b/mathcomp/ssreflect/fingraph.v index 5a87c6c..dfba3c7 100644 --- a/mathcomp/ssreflect/fingraph.v +++ b/mathcomp/ssreflect/fingraph.v @@ -464,58 +464,110 @@ Qed. End Loop. -Hypothesis injf : injective f. +Section orbit_in. + +Variable S : pred_sort (predPredType T). + +Hypothesis f_in : {in S, forall x, f x \in S}. +Hypothesis injf : {in S &, injective f}. + +Lemma iter_in : {in S, forall x i, iter i f x \in S}. +Proof. by move=> x xS; elim=> [|i /f_in]. Qed. + +Lemma finv_in : {in S, forall x, finv x \in S}. +Proof. by move=> ??; rewrite iter_in. Qed. -Lemma f_finv : cancel finv f. +Lemma f_finv_in : {in S, cancel finv f}. Proof. -move=> x; move: (looping_order x) (orbit_uniq x). +move=> x xS; move: (looping_order x) (orbit_uniq x). rewrite /looping /orbit -orderSpred looping_uniq /= /looping; set n := _.-1. -case/predU1P=> // /trajectP[i lt_i_n]; rewrite -iterSr => /= /injf ->. -by case/trajectP; exists i. +case/predU1P=> // /trajectP[i lt_i_n]; rewrite -iterSr. +by move=> /injf ->; rewrite ?iter_in //; case/trajectP; exists i. +Qed. + +Lemma finv_f_in : {in S, cancel f finv}. +Proof. by move=> x xS; apply/injf; rewrite ?iter_in ?f_finv_in ?f_in. Qed. + +Lemma finv_inj_in : {in S &, injective finv}. +Proof. by move=> x y xS yS q; rewrite -(f_finv_in xS) q f_finv_in. Qed. + +Lemma fconnect_sym_in : {in S &, forall x y, fconnect f x y = fconnect f y x}. +Proof. +suff Sf : {in S &, forall x y, fconnect f x y -> fconnect f y x}. + by move=> *; apply/idP/idP=> /Sf->. +move=> x _ xS _ /connectP [p f_p ->]; elim: p => //= y p IHp in x xS f_p *. +move: f_p; rewrite -{2}(finv_f_in xS) => /andP[/eqP <- /(IHp _ (f_in xS))]. +by move=> /connect_trans -> //; apply: fconnect_finv. +Qed. + +Lemma iter_order_in : {in S, forall x, iter (order x) f x = x}. +Proof. by move=> x xS; rewrite -orderSpred iterS; apply: f_finv_in. Qed. + +Lemma iter_finv_in n : + {in S, forall x, n <= order x -> iter n finv x = iter (order x - n) f x}. +Proof. +move=> x xS; rewrite -{2}[x]iter_order_in => // /subnKC {1}<-; move: (_ - n). +move=> m; rewrite iter_add; elim: n => // n {2}<-. +by rewrite iterSr /= finv_f_in // -iter_add iter_in. +Qed. + +Lemma cycle_orbit_in : {in S, forall x, (fcycle f) (orbit x)}. +Proof. +move=> x xS; rewrite /orbit -orderSpred (cycle_path x) /= last_traject. +by rewrite -/(finv x) fpath_traject f_finv_in ?eqxx. +Qed. + +Lemma fpath_finv_in p x : (x \in S) && (fpath finv x p) = + (last x p \in S) && (fpath f (last x p) (rev (belast x p))). +Proof. +elim: p x => //= y p IHp x; rewrite rev_cons rcons_path. +transitivity [&& y \in S, f y == x & fpath finv y p]. + apply/and3P/and3P => -[xS /eqP<- fxp]; split; + by rewrite ?f_finv_in ?finv_f_in ?finv_in ?f_in. +rewrite andbCA {}IHp !andbA [RHS]andbC -andbA; congr [&& _, _ & _]. +by case: p => //= z p; rewrite rev_cons last_rcons. Qed. -Lemma finv_f : cancel f finv. -Proof. exact (inj_can_sym f_finv injf). Qed. +Lemma fpath_finv_f_in p : {in S, forall x, + fpath finv x p -> fpath f (last x p) (rev (belast x p))}. +Proof. by move=> x xS /(conj xS)/andP; rewrite fpath_finv_in => /andP[]. Qed. + +Lemma fpath_f_finv_in p x : last x p \in S -> + fpath f (last x p) (rev (belast x p)) -> fpath finv x p. +Proof. by move=> lS /(conj lS)/andP; rewrite -fpath_finv_in => /andP[]. Qed. + +End orbit_in. + +Hypothesis injf : injective f. + +Lemma f_finv : cancel finv f. Proof. exact: (in1T (f_finv_in _ (in2W _))). Qed. + +Lemma finv_f : cancel f finv. Proof. exact: (in1T (finv_f_in _ (in2W _))). Qed. Lemma fin_inj_bij : bijective f. -Proof. by exists finv; [apply finv_f | apply f_finv]. Qed. +Proof. by exists finv; [apply: finv_f|apply: f_finv]. Qed. Lemma finv_bij : bijective finv. -Proof. by exists f; [apply f_finv | apply finv_f]. Qed. +Proof. by exists f; [apply: f_finv|apply: finv_f]. Qed. -Lemma finv_inj : injective finv. -Proof. exact (can_inj f_finv). Qed. +Lemma finv_inj : injective finv. Proof. exact: (can_inj f_finv). Qed. Lemma fconnect_sym x y : fconnect f x y = fconnect f y x. -Proof. -suff{x y} Sf x y: fconnect f x y -> fconnect f y x by apply/idP/idP; auto. -case/connectP=> p f_p -> {y}; elim: p x f_p => //= y p IHp x. -rewrite -{2}(finv_f x) => /andP[/eqP-> /IHp/connect_trans-> //]. -exact: fconnect_finv. -Qed. +Proof. exact: (in2T (fconnect_sym_in _ (in2W _))). Qed. + Let symf := fconnect_sym. Lemma iter_order x : iter (order x) f x = x. -Proof. by rewrite -orderSpred iterS; apply (f_finv x). Qed. +Proof. exact: (in1T (iter_order_in _ (in2W _))). Qed. Lemma iter_finv n x : n <= order x -> iter n finv x = iter (order x - n) f x. -Proof. -rewrite -{2}[x]iter_order => /subnKC {1}<-; move: (_ - n) => m. -by rewrite iter_add; elim: n => // n {2}<-; rewrite iterSr /= finv_f. -Qed. +Proof. exact: (in1T (@iter_finv_in _ _ (in2W _) _)). Qed. Lemma cycle_orbit x : fcycle f (orbit x). -Proof. -rewrite /orbit -orderSpred (cycle_path x) /= last_traject -/(finv x). -by rewrite fpath_traject f_finv andbT /=. -Qed. +Proof. exact: (in1T (cycle_orbit_in _ (in2W _))). Qed. Lemma fpath_finv x p : fpath finv x p = fpath f (last x p) (rev (belast x p)). -Proof. -elim: p x => //= y p IHp x; rewrite rev_cons rcons_path -{}IHp andbC /=. -rewrite (canF_eq finv_f) eq_sym; congr (_ && (_ == _)). -by case: p => //= z p; rewrite rev_cons last_rcons. -Qed. +Proof. exact: (@fpath_finv_in T _ (in2W _)). Qed. Lemma same_fconnect_finv : fconnect finv =2 fconnect f. Proof. @@ -722,4 +774,3 @@ Implicit Arguments intro_adjunction [T T' h e e' a]. Implicit Arguments adjunction_n_comp [T T' e e' a]. Unset Implicit Arguments. - diff --git a/mathcomp/ssreflect/plugin/v8.5/ssreflect_plugin.mllib b/mathcomp/ssreflect/plugin/v8.5/ssreflect_plugin.mllib index 006b70f..dee851c 100644 --- a/mathcomp/ssreflect/plugin/v8.5/ssreflect_plugin.mllib +++ b/mathcomp/ssreflect/plugin/v8.5/ssreflect_plugin.mllib @@ -1,2 +1 @@ -Ssrmatching Ssreflect diff --git a/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4 b/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4 index 658966b..ebc4de9 100644 --- a/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4 +++ b/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4 @@ -49,11 +49,11 @@ open Notation_ops open Locus open Locusops -DECLARE PLUGIN "ssreflect" +DECLARE PLUGIN "ssrmatching_plugin" type loc = Loc.t let dummy_loc = Loc.ghost -let errorstrm = Errors.errorlabstrm "ssreflect" +let errorstrm = Errors.errorlabstrm "ssrmatching" let loc_error loc msg = Errors.user_err_loc (loc, msg, str msg) (* 0 cost pp function. Active only if env variable SSRDEBUG is set *) @@ -1334,14 +1334,14 @@ let () = Genarg.out_gen (topwit wit_ssrpatternarg) (Id.Map.find (Names.Id.of_string "ssrpatternarg") ist.lfun) in Proofview.V82.tactic (ssrpatterntac ist arg) in - let name = { mltac_plugin = "ssreflect"; mltac_tactic = "ssrpattern"; } in + let name = { mltac_plugin = "ssrmatching_plugin"; mltac_tactic = "ssrpattern"; } in let () = Tacenv.register_ml_tactic name mltac in let tac = TacFun ([Some (Id.of_string "ssrpatternarg")], TacML (Loc.ghost, name, [])) in let obj () = Tacenv.register_ltac true false (Id.of_string "ssrpattern") tac in - Mltop.declare_cache_obj obj "ssreflect" + Mltop.declare_cache_obj obj "ssrmatching_plugin" let ssrinstancesof ist arg gl = let ok rhs lhs ise = true in diff --git a/mathcomp/ssreflect/plugin/v8.5/ssrmatching.v b/mathcomp/ssreflect/plugin/v8.5/ssrmatching.v index 369ffaf..c20c846 100644 --- a/mathcomp/ssreflect/plugin/v8.5/ssrmatching.v +++ b/mathcomp/ssreflect/plugin/v8.5/ssrmatching.v @@ -1,9 +1,6 @@ (* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) - -Set Implicit Arguments. -Unset Strict Implicit. -Unset Printing Implicit Defensive. +Declare ML Module "ssrmatching_plugin". Module SsrMatchingSyntax. @@ -25,3 +22,5 @@ Notation LHS := (X in X = _)%pattern. End SsrMatchingSyntax. Export SsrMatchingSyntax. + +Tactic Notation "ssrpattern" ssrpatternarg(p) := ssrpattern p . diff --git a/mathcomp/ssreflect/plugin/v8.5/ssrmatching_plugin.mllib b/mathcomp/ssreflect/plugin/v8.5/ssrmatching_plugin.mllib new file mode 100644 index 0000000..5fb1f15 --- /dev/null +++ b/mathcomp/ssreflect/plugin/v8.5/ssrmatching_plugin.mllib @@ -0,0 +1 @@ +Ssrmatching diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index fa3bf25..5574892 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -2623,6 +2623,19 @@ elim: ss => //= s ss IHss in i *; rewrite subn_eq0 nth_cat. by have [//|le_s_i] := ltnP; rewrite subnDA subSn /=. Qed. +Lemma reshape_leq sh i1 i2 + (r1 := reshape_index sh i1) (c1 := reshape_offset sh i1) + (r2 := reshape_index sh i2) (c2 := reshape_offset sh i2) : + (i1 <= i2) = ((r1 < r2) || ((r1 == r2) && (c1 <= c2))). +Proof. +rewrite {}/r1 {}/c1 {}/r2 {}/c2 /reshape_offset /reshape_index. +elim: sh => [|s0 s IHs] /= in i1 i2 *; rewrite ?subn0 ?subn_eq0 //. +have [[] i1s0 [] i2s0] := (ltnP i1 s0, ltnP i2 s0); first by rewrite !subn0. +- by apply: leq_trans i2s0; apply/ltnW. +- by apply/negP => /(leq_trans i1s0); rewrite leqNgt i2s0. +by rewrite !subSn // !eqSS !ltnS !subnDA -IHs leq_subLR subnKC. +Qed. + End Flatten. Prenex Implicits flatten shape reshape. |