From c463d5b0052c3543f09e39d2a158bb6caaf8daa9 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Tue, 29 Nov 2016 14:43:12 +0100 Subject: [PATCH] Generalize seqmx.v to not require a ringType structure everywhere. This can be useful for example, to manipulate matrices of floating-point values, as floating-point arithmetic does not have a ring structure (addition is not even associative). Actually, the ring structure on the coefficients is definitely overkill for all non arithmetic operations over matrices. --- refinements/seqmx.v | 865 ++++++++++++++++++++++---------------------- 1 file changed, 439 insertions(+), 426 deletions(-) diff --git a/refinements/seqmx.v b/refinements/seqmx.v index fa30c37..51574e1 100644 --- a/refinements/seqmx.v +++ b/refinements/seqmx.v @@ -267,15 +267,13 @@ Parametricity copid_seqmx. Section seqmx_more_op. -Variable R : ringType. +Variable R : Type. +Context `{zero_of R}. Context (C : Type). -Context `{zero_of C, eq_of C, spec_of C R}. +Context `{spec_of C R}. Global Instance spec_seqmx m n : spec_of (@seqmx C) 'M[R]_(m, n) := - fun s => - if (s == seqmx0 m n)%C then 0 else - matrix_of_fun matrix_key (fun (i : 'I_m) (j : 'I_n) => - (nth 0 (nth [::] (map_seqmx spec s) i) j)). + fun s => \matrix_(i, j) nth 0%C (nth [::] (map_seqmx spec s) i) j. End seqmx_more_op. @@ -285,14 +283,9 @@ Section seqmx_theory. Section seqmx. -Variable R : ringType. +Variable R : Type. +Context `{zero_of R, one_of R, opp_of R, add_of R, mul_of R, eq_of R}. -Local Instance zeroR : zero_of R := 0%R. -Local Instance oneR : one_of R := 1%R. -Local Instance oppR : opp_of R := -%R. -Local Instance addR : add_of R := +%R. -Local Instance mulR : mul_of R := *%R. -Local Instance eqR : eq_of R := eqtype.eq_op. Local Instance specR : spec_of R R := spec_id. Local Instance implem_ord : forall n, (implem_of 'I_n 'I_n) := @@ -305,7 +298,7 @@ CoInductive Rseqmx {m1 m2} (rm : nat_R m1 m2) {n1 n2} (rn : nat_R n1 n2) : Rseqmx_spec (A : 'M[R]_(m1, n1)) M of size M = m2 & forall i, i < m2 -> size (nth [::] M i) = n2 - & (forall i j, (A i j = nth 0 (nth [::] M i) j)) : Rseqmx rm rn A M. + & (forall i j, (A i j = nth 0%C (nth [::] M i) j)) : Rseqmx rm rn A M. (* Definition Rord n (i : 'I_n) j := i = j :> nat. *) @@ -358,215 +351,13 @@ Proof. Qed. Instance Rseqmx_0 m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) : - refines (Rseqmx rm rn) 0 (seqmx0 m2 n2). + refines (Rseqmx rm rn) (const_mx 0%C) (seqmx0 m2 n2). Proof. rewrite refinesE; constructor=>[|i|i j]; first by rewrite size_nseq. by rewrite nth_nseq => ->; rewrite size_nseq. by rewrite mxE nth_nseq -(nat_R_eq rm) ltn_ord nth_nseq -(nat_R_eq rn) ltn_ord. Qed. -Instance Rseqmx_diag_seqmx m1 m2 (rm : nat_R m1 m2) : - refines (Rseqmx (nat_R_S_R nat_R_O_R) rm ==> Rseqmx rm rm) - diag_mx (diag_seqmx (A:=R)). -Proof. - rewrite refinesE=> _ _ [M sM h1 h2 h3]. - constructor=> [|i ltim|i j]. - by rewrite size_map ord_enum_eqE size_enum_ord h2. - by rewrite /diag_seqmx /mkseqmx_ord ord_enum_eqE h2 // - (nth_map (Ordinal ltim)) ?size_enum_ord // - size_map size_enum_ord. - rewrite mxE h3 /diag_seqmx /mkseqmx_ord ord_enum_eqE h2 // -(nat_R_eq rm) - (nth_map i) ?size_enum_ord // (nth_map j) ?size_enum_ord // - !nth_ord_enum. - by case: (i == j). -Qed. - -Instance Rseqmx_scalar_seqmx m1 m2 (rm : nat_R m1 m2) : - refines (eq ==> Rseqmx rm rm) scalar_mx (scalar_seqmx m2). -Proof. - rewrite refinesE=> x y rxy. - rewrite /scalar_seqmx -diag_const_mx. - exact: refinesP. -Qed. - -Instance Rseqmx_1 m1 m2 (rm : nat_R m1 m2) : - refines (Rseqmx rm rm) 1%:M (seqmx1 m2). -Proof. - rewrite /seqmx1. - eapply refines_apply; first exact: Rseqmx_scalar_seqmx. - by rewrite refinesE. -Qed. - -Instance Rseqmx_opp m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) : - refines (Rseqmx rm rn ==> Rseqmx rm rn) -%R -%C. -Proof. -rewrite refinesE=> ? ? [A M h1 h2 h3]. -constructor=> [|i ltim|i j]; first by rewrite size_map h1. - rewrite (nth_map [::]); last by rewrite h1. - by rewrite size_map h2. -rewrite mxE (nth_map [::]); last by rewrite h1 -(nat_R_eq rm) ltn_ord. -rewrite (nth_map 0); first by rewrite h3. -by rewrite h2 -?(nat_R_eq rm) -?(nat_R_eq rn) ltn_ord. -Qed. - - -Instance Rseqmx_add m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) : - refines (Rseqmx rm rn ==> Rseqmx rm rn ==> Rseqmx rm rn) +%R +%C. -Proof. - rewrite refinesE=> _ _ [M sM h1 h2 h3] _ _ [N sN h'1 h'2 h'3]. - constructor=> [|i ltim|i j]; rewrite [(_ + _)%C]zipwithE. - by rewrite size_map size1_zip h1 ?h'1. - by rewrite (nth_map ([::], [::])) ?nth_zip ?zipwithE ?size_map ?size1_zip /= - ?h1 ?h'1 ?h2 ?h'2 ?ltim. - by rewrite (nth_map ([::], [::])) ?nth_zip /= ?size1_zip ?h1 ?h'1 - -?(nat_R_eq rm) ?ltn_ord // mxE h3 h'3 zipwithE - -[[seq _ | _ <- _]](mkseq_nth 0%C) nth_mkseq /= - ?(nth_map (0%C, 0%C)) ?nth_zip ?size_map /= ?size1_zip ?h2 ?h'2 - -?(nat_R_eq rm) -?(nat_R_eq rn) ?ltn_ord. -Qed. - -Instance Rseqmx_sub m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) : - refines (Rseqmx rm rn ==> Rseqmx rm rn ==> Rseqmx rm rn) - (fun M N => M - N) sub_op. -Proof. - rewrite refinesE=> _ _ [M sM h1 h2 h3] _ _ [N sN h'1 h'2 h'3]. - constructor=> [|i ltim|i j]; rewrite [(_ - _)%C]zipwithE. - by rewrite size_map size1_zip ?size_map h1 ?h'1. - by rewrite (nth_map ([::], [::])) ?nth_zip ?zipwithE ?size_map ?size1_zip /= - ?(nth_map [::]) ?size_map ?h1 ?h'1 ?h2 ?h'2 ?ltim. - by rewrite !mxE h3 h'3 (nth_map ([::], [::])) ?zipwithE ?(nth_map (0%C, 0%C)) - ?nth_zip /= ?(nth_map [::]) ?size1_zip ?size_map ?(nth_map 0%C) - ?h1 ?h'1 ?h2 ?h'2 -?(nat_R_eq rm) -?(nat_R_eq rn) ?ltn_ord. -Qed. - -Lemma minSS (p q : nat) : minn p.+1 q.+1 = (minn p q).+1. -Proof. by rewrite /minn ltnS; case:ifP. Qed. - -Lemma size_fold (s : seq (seq R)) k - (hs : forall i : nat, i < size s -> size (nth [::] s i) = k) : - size (foldr (zipwith cons) (nseq k [::]) s) = k. -Proof. - elim: s hs=> [_|a s ihs hs] /=; first by rewrite size_nseq. - rewrite zipwithE size_map size1_zip ?ihs; have /= ha := hs 0%N; - rewrite ?ha //. - by move=> q hq; rewrite -(hs q.+1). -Qed. - -Lemma size_nth_fold (s : seq (seq R)) j k (ltkj : k < j) - (hs : forall l : nat, l < size s -> size (nth [::] s l) = j) : - size (nth [::] (foldr (zipwith cons) (nseq j [::]) s) k) = size s. -Proof. - elim: s hs=> [_|a s ihs hs] /=. - by rewrite nth_nseq if_same. - rewrite zipwithE (nth_map (0, [::])) ?nth_zip /= ?ihs // ?size1_zip - ?size_fold; have /= ha := hs 0%N; rewrite ?ha //; - by move=> l hl; rewrite -(hs l.+1). -Qed. - -Lemma nth_fold (s : seq (seq R)) j k l (ltks : k < size s) (ltlj : l < j) - (hs : forall l : nat, l < size s -> size (nth [::] s l) = j) : - (nth [::] (foldr (zipwith cons) (nseq j [::]) s) l)`_k = (nth [::] s k)`_l. -Proof. - elim: s k ltks hs=> [_ _ _|a s ihs k ltks hs] //=. - rewrite zipwithE (nth_map (0, [::])) ?nth_zip /= ?size1_zip ?size_fold; - have /= ha := hs 0%N; rewrite ?ha //; - first (case: k ltks=> [|k' ltk's] //=; rewrite ?ihs //); - by move=> q hq; rewrite -(hs q.+1). -Qed. - -Instance Rseqmx_trseqmx m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) : - refines (Rseqmx rm rn ==> Rseqmx rn rm) trmx (@trseqmx R m2 n2). -Proof. - rewrite /trseqmx. - case: rm=> [|k1 k2 rk] /=; - rewrite refinesE=> _ _ [M sM h1 h2 h3]; - constructor=> [|i ltim|i j]. - by rewrite size_nseq. - by rewrite nth_nseq ltim. - by rewrite -(nat_R_eq rn) nth_nseq ltn_ord mxE h3 (size0nil h1) - !nth_nil. - by rewrite size_fold ?h1. - by rewrite size_nth_fold ?h1. - by rewrite mxE h3 nth_fold ?h1 // -?(nat_R_eq rn) -?(nat_R_eq rk). -Qed. - -Instance Rseqmx_mul m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) - p1 p2 (rp : nat_R p1 p2) : - refines (Rseqmx rm rn ==> Rseqmx rn rp ==> Rseqmx rm rp) - mulmx (@hmul_op _ _ _ m2 n2 p2). -Proof. - case: rn=> [|k1 k2 rk]; - rewrite refinesE=> _ _ [M sM h1 h2 h3] _ _ [N sN h'1 h'2 h'3]. - constructor=> [|i ltim|i j]; rewrite /hmul_op /mul_seqmx /seqmx0. - by rewrite size_nseq. - by rewrite nth_nseq h1 ltim size_nseq. - by rewrite nth_nseq h1 -(nat_R_eq rm) ltn_ord nth_nseq -(nat_R_eq rp) - ltn_ord mxE big_ord0. - constructor=> [|i ltim|i j]; rewrite /hmul_op /mul_seqmx. - by rewrite size_map. - by rewrite (nth_map [::]) ?h1 // size_map /trseqmx /= size_fold ?h'1. - rewrite (nth_map [::]) ?h1 -?(nat_R_eq rm) // (nth_map [::]) /trseqmx - ?size_fold ?h'1 ?h'2 // -?(nat_R_eq rp) //. - set F := (fun z x y => _). - have ->: forall s1 s2 (t : R), (foldl2 F t s1 s2) = - (t + \sum_(0 <= k < minn (size s1) (size s2)) s1`_k * s2`_k). - elim=>[s2 t|t1 s1 IHs s2 t]. - by rewrite min0n big_mkord big_ord0 GRing.addr0. - case:s2=>[|t2 s2]; first by rewrite minn0 big_mkord big_ord0 GRing.addr0. - by rewrite /= IHs minSS big_nat_recl // /F [(_ + t)%C]addrC addrA. - rewrite add0r big_mkord size_nth_fold ?h'1 ?h2 -?(nat_R_eq rm) // - ?(nat_R_eq rp) // /minn if_same mxE -(nat_R_eq rk). - apply: eq_bigr=> k _. - by rewrite h3 h'3 nth_fold ?h'1 ?(nat_R_eq rp) // -(nat_R_eq rk). -Qed. - -Instance Rseqmx_scale m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) : - refines (eq ==> Rseqmx rm rn ==> Rseqmx rm rn) *:%R *:%C. -Proof. - rewrite refinesE=> _ x -> _ _ [M sM h1 h2 h3]. - constructor=> [|i ltim|i j]; rewrite [(_ *: _)%C]/scale_seqmx. - by rewrite size_map. - by rewrite (nth_map [::]) ?size_map ?h1 ?h2. - by rewrite mxE (nth_map [::]) ?(nth_map 0%C) ?h1 ?h2 ?h3 -?(nat_R_eq rm) - -?(nat_R_eq rn). -Qed. - -Lemma eq_seqE (T : Type) (f : T -> T -> bool) s1 s2 : size s1 = size s2 -> - eq_seq f s1 s2 = all (fun xy => f xy.1 xy.2) (zip s1 s2). -Proof. -elim: s1 s2 => [|x1 s1 IHs] [] //= x2 s2 /eqP eq_sz. -by rewrite IHs //; apply/eqP. -Qed. - -Instance Rseqmx_eq m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) : - refines (Rseqmx rm rn ==> Rseqmx rm rn ==> bool_R) eqtype.eq_op eq_op. -Proof. - rewrite refinesE=> _ _ [M sM h1 h2 h3] _ _ [N sN h'1 h'2 h'3]. - suff ->: (M == N) = (eq_seq (eq_seq eqR) sM sN). - exact: bool_Rxx. - apply/eqP/idP=> [/matrixP heq|]. - rewrite eq_seqE ?h1 ?h'1 //. - apply/(all_nthP ([::], [::]))=> i. - rewrite size1_zip ?nth_zip ?h1 ?h'1 //=; move=> ltim. - rewrite eq_seqE ?h2 ?h'2 //. - apply/(all_nthP (0, 0))=> j. - rewrite size1_zip ?nth_zip ?h2 ?h'2 //= -(nat_R_eq rn); move=> ltjn. - rewrite -(nat_R_eq rm) in ltim. - have := heq (Ordinal ltim) (Ordinal ltjn); rewrite h3 h'3=> ->. - by apply/eqP. - rewrite eq_seqE ?h1 ?h'1 //. - move/(all_nthP ([::], [::])). - rewrite size1_zip ?h1 ?h'1 //; move=> heq. - apply/matrixP=> i j. - have := heq i; rewrite -(nat_R_eq rm) ltn_ord; move/implyP; rewrite implyTb. - rewrite nth_zip ?h1 ?h'1 //= eq_seqE ?h2 ?h'2 -?(nat_R_eq rm) //. - move/(all_nthP (0, 0))=> /(_ j). - rewrite nth_zip ?size1_zip ?h2 ?h'2 -?(nat_R_eq rm) //= h3 h'3 -?(nat_R_eq rn) - (ltn_ord _) /eqR. - move=> he. - by apply/eqP; rewrite he. -Qed. - Instance Rseqmx_top_left_seqmx m1 m2 (rm : nat_R m1 m2) : refines (Rseqmx (nat_R_S_R rm) (nat_R_S_R rm) ==> eq) (fun M => M ord0 ord0) top_left_op. @@ -759,90 +550,56 @@ Proof. by rewrite addnC -addnBA ?subnn ?addn0 -?addnBA ?subnn ?addn0. Qed. -Instance Rseqmx_delta_seqmx m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) - (i1 : 'I_m1) (i2 : 'I_m2) (ri : nat_R i1 i2) (j1 : 'I_n1) (j2 : 'I_n2) - (rj : nat_R j1 j2) : - refines (Rseqmx rm rn) (delta_mx i1 j1) (delta_seqmx m2 n2 i2 j2). +Lemma minSS (p q : nat) : minn p.+1 q.+1 = (minn p q).+1. +Proof. by rewrite /minn ltnS; case:ifP. Qed. + +Lemma size_fold (s : seq (seq R)) k + (hs : forall i : nat, i < size s -> size (nth [::] s i) = k) : + size (foldr (zipwith cons) (nseq k [::]) s) = k. Proof. - rewrite refinesE -(nat_R_eq ri) -(nat_R_eq rj); constructor=> [|k ltkm|k l]. - by rewrite size_map ord_enum_eqE size_enum_ord. - by rewrite (nth_map (Ordinal ltkm)) !ord_enum_eqE ?size_enum_ord // size_map - size_enum_ord. - rewrite mxE /delta_seqmx /mkseqmx_ord !ord_enum_eqE -(nat_R_eq rm) - -(nat_R_eq rn) (nth_map k) ?size_enum_ord // (nth_map l) - ?size_enum_ord // !nth_ord_enum. - by case: ifP. + elim: s hs=> [_|a s ihs hs] /=; first by rewrite size_nseq. + rewrite zipwithE size_map size1_zip ?ihs; have /= ha := hs 0%N; + rewrite ?ha //. + by move=> q hq; rewrite -(hs q.+1). Qed. -Instance Rseqmx_trace_seqmx m1 m2 (rm : nat_R m1 m2) : - refines (Rseqmx rm rm ==> eq) mxtrace (trace_seqmx (A:=R) (m:=m2)). +Lemma size_nth_fold (s : seq (seq R)) j k (ltkj : k < j) + (hs : forall l : nat, l < size s -> size (nth [::] s l) = j) : + size (nth [::] (foldr (zipwith cons) (nseq j [::]) s) k) = size s. Proof. - apply refines_abstr. - rewrite !refinesE /mxtrace. - elim: rm=> [|n1 n2 rn ih] /= M sM rM. - by rewrite big_ord0. - rewrite big_ord_recl -(ih (drsubmx (M : 'M_(1 + n1, 1 + n1)))). - have <- : M ord0 ord0 = top_left_seqmx sM. - apply refinesP; rewrite -[M _ _]/((fun (M : 'M_(_)) => M _ _) _). - eapply refines_apply. - apply Rseqmx_top_left_seqmx. - rewrite refinesE; eassumption. - apply: congr2=> //; apply eq_bigr=> i _. - by rewrite -[in LHS](@submxK R 1 n1 1 n1 M) -zmodp.rshift1 - [LHS](@block_mxEdr R 1 n1 1 n1). - apply refinesP; eapply refines_apply. - apply Rseqmx_drsubseqmx. - rewrite refinesE. - have H : nat_R_S_R rn = addn_R (nat_R_S_R nat_R_O_R) rn by []. - rewrite H in rM. - eassumption. + elim: s hs=> [_|a s ihs hs] /=. + by rewrite nth_nseq if_same. + rewrite zipwithE (nth_map (0%C, [::])) ?nth_zip /= ?ihs // ?size1_zip + ?size_fold; have /= ha := hs 0%N; rewrite ?ha //; + by move=> l hl; rewrite -(hs l.+1). Qed. -Instance Rseqmx_pid_seqmx m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) - r1 r2 (rr : nat_R r1 r2) : - refines (Rseqmx rm rn) (pid_mx r1) (pid_seqmx m2 n2 r2). +Lemma nth_fold (s : seq (seq R)) j k l (ltks : k < size s) (ltlj : l < j) + (hs : forall l : nat, l < size s -> size (nth [::] s l) = j) : + nth 0%C (nth [::] (foldr (zipwith cons) (nseq j [::]) s) l) k + = nth 0%C (nth [::] s k) l. Proof. - rewrite refinesE; constructor=> [|i ltim|i j]. - by rewrite size_map ord_enum_eqE size_enum_ord. - by rewrite (nth_map (Ordinal ltim)) !ord_enum_eqE ?size_enum_ord // size_map - size_enum_ord. - rewrite mxE /pid_seqmx /mkseqmx_ord !ord_enum_eqE -(nat_R_eq rm) - -(nat_R_eq rn) (nth_map i) ?size_enum_ord // (nth_map j) - ?size_enum_ord // !nth_ord_enum -(nat_R_eq rr). - by case: ifP. -Qed. - -Instance Rseqmx_copid_seqmx m1 m2 (rm : nat_R m1 m2) r1 r2 (rr : nat_R r1 r2) : - refines (Rseqmx rm rm) (copid_mx r1) (copid_seqmx m2 r2). -Proof. - rewrite /copid_mx /copid_seqmx /sub_op /sub_seqmx. - eapply refines_apply; tc. - eapply refines_apply; tc. - exact: Rseqmx_pid_seqmx. + elim: s k ltks hs=> [_ _ _|a s ihs k ltks hs] //=. + rewrite zipwithE (nth_map (0%C, [::])) ?nth_zip /= ?size1_zip ?size_fold; + have /= ha := hs 0%N; rewrite ?ha //; + first (case: k ltks=> [|k' ltk's] //=; rewrite ?ihs //); + by move=> q hq; rewrite -(hs q.+1). Qed. -Instance Rseqmx_spec_l m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) : - refines (Rseqmx rm rn ==> Logic.eq) spec_id spec. +Instance Rseqmx_trseqmx m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) : + refines (Rseqmx rm rn ==> Rseqmx rn rm) trmx (@trseqmx R m2 n2). Proof. - rewrite refinesE=> _ _ [M sM h1 h2 h3]. - rewrite /spec /spec_seqmx /spec_id /spec /specR /spec_id /map_seqmx map_id_in; - last first. - by move=> x; rewrite map_id. - apply/matrixP=> i j. - case: ifP; rewrite h3 mxE //. - rewrite /eq_op /eq_seqmx eq_seqE /seqmx0 /const_seqmx ?size_nseq ?h1 - ?(nat_R_eq rm) //. - move/all_nthP=> heq. - have /implyP := heq ([::], [::]) i. - rewrite size_zip h1 size_nseq -(nat_R_eq rm) minnn ltn_ord implyTb eq_seqE - nth_zip /= ?nth_nseq ?h1 ?h2 ?ltn_ord ?size_nseq -?(nat_R_eq rm) - -?(nat_R_eq rn) //. - move/all_nthP=> heq'. - have /implyP := heq' (0, 0) j. - rewrite size_zip h2 ?size_nseq -?(nat_R_eq rn) -?(nat_R_eq rm) ?minnn ltn_ord - // implyTb nth_zip /= ?nth_nseq ?h2 ?size_nseq ?ltn_ord - -?(nat_R_eq rm) ?(nat_R_eq rn) //. - by move/eqP. + rewrite /trseqmx. + case: rm=> [|k1 k2 rk] /=; + rewrite refinesE=> _ _ [M sM h1 h2 h3]; + constructor=> [|i ltim|i j]. + by rewrite size_nseq. + by rewrite nth_nseq ltim. + by rewrite -(nat_R_eq rn) nth_nseq ltn_ord mxE h3 (size0nil h1) + !nth_nil. + by rewrite size_fold ?h1. + by rewrite size_nth_fold ?h1. + by rewrite mxE h3 nth_fold ?h1 // -?(nat_R_eq rn) -?(nat_R_eq rk). Qed. Section seqmx_param. @@ -853,11 +610,11 @@ Context (I : nat -> Type) Context `{zero_of C, one_of C, opp_of C, add_of C, mul_of C, eq_of C}. Context `{spec_of C R}. Context `{forall n, implem_of 'I_n (I n)}. -Context `{!refines rAC 0%R 0%C, !refines rAC 1%R 1%C}. -Context `{!refines (rAC ==> rAC) -%R -%C}. -Context `{!refines (rAC ==> rAC ==> rAC) +%R +%C}. -Context `{!refines (rAC ==> rAC ==> rAC) *%R *%C}. -Context `{!refines (rAC ==> rAC ==> bool_R) eqtype.eq_op eq_op}. +Context `{!refines rAC 0%C 0%C, !refines rAC 1%C 1%C}. +Context `{!refines (rAC ==> rAC) -%C -%C}. +Context `{!refines (rAC ==> rAC ==> rAC) +%C +%C}. +Context `{!refines (rAC ==> rAC ==> rAC) *%C *%C}. +Context `{!refines (rAC ==> rAC ==> bool_R) eq_op eq_op}. Context `{!refines (rAC ==> Logic.eq) spec_id spec}. Context `{forall n1 n2 (rn : nat_R n1 n2), refines (ordinal_R rn ==> rI rn) implem_id implem}. @@ -934,109 +691,13 @@ Global Instance refine_const_seqmx m n : Proof. exact: RseqmxC_const_seqmx. Qed. Global Instance RseqmxC_0 m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) : - refines (RseqmxC rm rn) 0 (@hzero_op _ _ _ m2 n2). + refines (RseqmxC rm rn) (const_mx 0%C) (@hzero_op _ _ _ m2 n2). Proof. param_comp seqmx0_R. Qed. Global Instance refine_0_seqmx m n : - refines (RseqmxC (nat_Rxx m) (nat_Rxx n)) 0 (@hzero_op _ _ _ m n). + refines (RseqmxC (nat_Rxx m) (nat_Rxx n)) (const_mx 0%C) (@hzero_op _ _ _ m n). Proof. exact: RseqmxC_0. Qed. -Global Instance RseqmxC_diag_seqmx m1 m2 (rm : nat_R m1 m2) : - refines (RseqmxC (nat_R_S_R nat_R_O_R) rm ==> RseqmxC rm rm) - diag_mx (diag_seqmx (A:=C)). -Proof. param_comp diag_seqmx_R. Qed. - -Global Instance refine_diag_seqmx m : - refines (RseqmxC (nat_R_S_R nat_R_O_R) (nat_Rxx m) ==> - RseqmxC (nat_Rxx m) (nat_Rxx m)) - diag_mx (diag_seqmx (A:=C)). -Proof. exact: RseqmxC_diag_seqmx. Qed. - -Global Instance RseqmxC_scalar_seqmx m1 m2 (rm : nat_R m1 m2) : - refines (rAC ==> RseqmxC rm rm) scalar_mx (scalar_seqmx m2). -Proof. param_comp scalar_seqmx_R. Qed. - -Global Instance refine_scalar_seqmx m : - refines (rAC ==> RseqmxC (nat_Rxx m) (nat_Rxx m)) scalar_mx (scalar_seqmx m). -Proof. exact: RseqmxC_scalar_seqmx. Qed. - -Global Instance RseqmxC_1 m1 m2 (rm : nat_R m1 m2) : - refines (RseqmxC rm rm) 1%:M (seqmx1 m2). -Proof. param_comp seqmx1_R. Qed. - -Global Instance refine_1_seqmx m : - refines (RseqmxC (nat_Rxx m) (nat_Rxx m)) 1%:M (seqmx1 m). -Proof. exact: RseqmxC_1. Qed. - -Global Instance RseqmxC_opp m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) : - refines (RseqmxC rm rn ==> RseqmxC rm rn) -%R -%C. -Proof. param_comp opp_seqmx_R. Qed. - -Global Instance refine_opp_seqmx m n : - refines (RseqmxC (nat_Rxx m) (nat_Rxx n) ==> RseqmxC (nat_Rxx m) (nat_Rxx n)) - -%R -%C. -Proof. exact: RseqmxC_opp. Qed. - -Global Instance RseqmxC_add m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) : - refines (RseqmxC rm rn ==> RseqmxC rm rn ==> RseqmxC rm rn) +%R +%C. -Proof. param_comp add_seqmx_R. Qed. - -Global Instance refine_add_seqmx m n : - refines (RseqmxC (nat_Rxx m) (nat_Rxx n) ==> RseqmxC (nat_Rxx m) (nat_Rxx n) - ==> RseqmxC (nat_Rxx m) (nat_Rxx n)) +%R +%C. -Proof. exact: RseqmxC_add. Qed. - -Global Instance RseqmxC_sub m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) : - refines (RseqmxC rm rn ==> RseqmxC rm rn ==> RseqmxC rm rn) - (fun M N => M - N) sub_op. -Proof. param_comp sub_seqmx_R. Qed. - -Global Instance refine_sub_seqmx m n : - refines (RseqmxC (nat_Rxx m) (nat_Rxx n) ==> RseqmxC (nat_Rxx m) (nat_Rxx n) - ==> RseqmxC (nat_Rxx m) (nat_Rxx n)) - (fun M N => M - N) sub_op. -Proof. exact: RseqmxC_sub. Qed. - -Global Instance RseqmxC_tr m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) : - refines (RseqmxC rm rn ==> RseqmxC rn rm) trmx (@trseqmx C m2 n2). -Proof. param_comp trseqmx_R. Qed. - -Global Instance refine_trseqmx m n : - refines (RseqmxC (nat_Rxx m) (nat_Rxx n) ==> RseqmxC (nat_Rxx n) (nat_Rxx m)) - trmx (@trseqmx C m n). -Proof. exact: RseqmxC_tr. Qed. - -Global Instance RseqmxC_mul m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) - p1 p2 (rp : nat_R p1 p2) : - refines (RseqmxC rm rn ==> RseqmxC rn rp ==> RseqmxC rm rp) - mulmx (@hmul_op _ _ _ m2 n2 p2). -Proof. param_comp mul_seqmx_R. Qed. - -Global Instance refine_mul_seqmx m n p : - refines (RseqmxC (nat_Rxx m) (nat_Rxx n) ==> RseqmxC (nat_Rxx n) (nat_Rxx p) - ==> RseqmxC (nat_Rxx m) (nat_Rxx p)) - mulmx (@hmul_op _ _ _ m n p). -Proof. exact: RseqmxC_mul. Qed. - -Global Instance RseqmxC_scale m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) - : refines (rAC ==> RseqmxC rm rn ==> RseqmxC rm rn) *:%R *:%C. -Proof. param_comp scale_seqmx_R. Qed. - -Global Instance refine_scale_seqmx m n : - refines (rAC ==> RseqmxC (nat_Rxx m) (nat_Rxx n) ==> - RseqmxC (nat_Rxx m) (nat_Rxx n)) *:%R *:%C. -Proof. exact: RseqmxC_scale. Qed. - -Global Instance RseqmxC_eq m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) : - refines (RseqmxC rm rn ==> RseqmxC rm rn ==> bool_R) - eqtype.eq_op eq_op. -Proof. param_comp eq_seqmx_R. Qed. - -Global Instance refine_eq_seqmx m n : - refines (RseqmxC (nat_Rxx m) (nat_Rxx n) ==> RseqmxC (nat_Rxx m) (nat_Rxx n) - ==> bool_R) eqtype.eq_op eq_op. -Proof. exact: RseqmxC_eq. Qed. - Global Instance RseqmxC_top_left_seqmx m1 m2 (rm : nat_R m1 m2) : refines (RseqmxC (nat_R_S_R rm) (nat_R_S_R rm) ==> rAC) (fun M => M ord0 ord0) @@ -1053,7 +714,7 @@ Global Instance RseqmxC_usubseqmx m11 m12 (rm1 : nat_R m11 m12) m21 m22 (rm2 : nat_R m21 m22) n1 n2 (rn : nat_R n1 n2) : refines (RseqmxC (addn_R rm1 rm2) rn ==> RseqmxC rm1 rn) (@matrix.usubmx R m11 m21 n1) (@usubseqmx C m12 m22 n2). -Proof. param_comp usubseqmx_R. Qed. +Proof. param_comp usubseqmx_R; rewrite refinesE; apply nat_Rxx. Qed. Global Instance refine_usubseqmx m1 m2 n : refines (RseqmxC (addn_R (nat_Rxx m1) (nat_Rxx m2)) (nat_Rxx n) ==> @@ -1065,7 +726,7 @@ Global Instance RseqmxC_dsubseqmx m11 m12 (rm1 : nat_R m11 m12) m21 m22 (rm2 : nat_R m21 m22) n1 n2 (rn : nat_R n1 n2) : refines (RseqmxC (addn_R rm1 rm2) rn ==> RseqmxC rm2 rn) (@matrix.dsubmx R m11 m21 n1) (@dsubseqmx C m12 m22 n2). -Proof. param_comp dsubseqmx_R. Qed. +Proof. param_comp dsubseqmx_R; rewrite refinesE; apply nat_Rxx. Qed. Global Instance refine_dsubseqmx m1 m2 n : refines (RseqmxC (addn_R (nat_Rxx m1) (nat_Rxx m2)) (nat_Rxx n) ==> @@ -1077,7 +738,7 @@ Global Instance RseqmxC_lsubseqmx m1 m2 (rm : nat_R m1 m2) n11 n12 (rn1 : nat_R n11 n12) n21 n22 (rn2 : nat_R n21 n22) : refines (RseqmxC rm (addn_R rn1 rn2) ==> RseqmxC rm rn1) (@matrix.lsubmx R m1 n11 n21) (@lsubseqmx C m2 n12 n22). -Proof. param_comp lsubseqmx_R. Qed. +Proof. param_comp lsubseqmx_R; rewrite refinesE; apply nat_Rxx. Qed. Global Instance refine_lsubseqmx m n1 n2 : refines (RseqmxC (nat_Rxx m) (addn_R (nat_Rxx n1) (nat_Rxx n2)) ==> @@ -1089,7 +750,7 @@ Global Instance RseqmxC_rsubseqmx m1 m2 (rm : nat_R m1 m2) n11 n12 (rn1 : nat_R n11 n12) n21 n22 (rn2 : nat_R n21 n22) : refines (RseqmxC rm (addn_R rn1 rn2) ==> RseqmxC rm rn2) (@matrix.rsubmx R m1 n11 n21) (@rsubseqmx C m2 n12 n22). -Proof. param_comp rsubseqmx_R. Qed. +Proof. param_comp rsubseqmx_R; rewrite refinesE; apply nat_Rxx. Qed. Global Instance refine_rsubseqmx m n1 n2 : refines (RseqmxC (nat_Rxx m) (addn_R (nat_Rxx n1) (nat_Rxx n2)) ==> @@ -1102,7 +763,7 @@ Global Instance RseqmxC_ulsubseqmx m11 m12 (rm1 : nat_R m11 m12) m21 m22 (rn2 : nat_R n21 n22) : refines (RseqmxC (addn_R rm1 rm2) (addn_R rn1 rn2) ==> RseqmxC rm1 rn1) (@matrix.ulsubmx R m11 m21 n11 n21) (@ulsubseqmx C m12 m22 n12 n22). -Proof. param_comp ulsubseqmx_R. Qed. +Proof. param_comp ulsubseqmx_R; rewrite refinesE; apply nat_Rxx. Qed. Global Instance refine_ulsubseqmx m1 m2 n1 n2 : refines (RseqmxC (addn_R (nat_Rxx m1) (nat_Rxx m2)) @@ -1116,7 +777,7 @@ Global Instance RseqmxC_ursubseqmx m11 m12 (rm1 : nat_R m11 m12) m21 m22 (rn2 : nat_R n21 n22) : refines (RseqmxC (addn_R rm1 rm2) (addn_R rn1 rn2) ==> RseqmxC rm1 rn2) (@matrix.ursubmx R m11 m21 n11 n21) (@ursubseqmx C m12 m22 n12 n22). -Proof. param_comp ursubseqmx_R. Qed. +Proof. param_comp ursubseqmx_R; rewrite refinesE; apply nat_Rxx. Qed. Global Instance refine_ursubseqmx m1 m2 n1 n2 : refines (RseqmxC (addn_R (nat_Rxx m1) (nat_Rxx m2)) @@ -1130,7 +791,7 @@ Global Instance RseqmxC_dlsubseqmx m11 m12 (rm1 : nat_R m11 m12) m21 m22 (rn2 : nat_R n21 n22) : refines (RseqmxC (addn_R rm1 rm2) (addn_R rn1 rn2) ==> RseqmxC rm2 rn1) (@matrix.dlsubmx R m11 m21 n11 n21) (@dlsubseqmx C m12 m22 n12 n22). -Proof. param_comp dlsubseqmx_R. Qed. +Proof. param_comp dlsubseqmx_R; rewrite refinesE; apply nat_Rxx. Qed. Global Instance refine_dlsubseqmx m1 m2 n1 n2 : refines (RseqmxC (addn_R (nat_Rxx m1) (nat_Rxx m2)) @@ -1144,7 +805,7 @@ Global Instance RseqmxC_drsubseqmx m11 m12 (rm1 : nat_R m11 m12) m21 m22 (rn2 : nat_R n21 n22) : refines (RseqmxC (addn_R rm1 rm2) (addn_R rn1 rn2) ==> RseqmxC rm2 rn2) (@matrix.drsubmx R m11 m21 n11 n21) (@drsubseqmx C m12 m22 n12 n22). -Proof. param_comp drsubseqmx_R. Qed. +Proof. param_comp drsubseqmx_R; rewrite refinesE; apply nat_Rxx. Qed. Global Instance refine_drsubseqmx m1 m2 n1 n2 : refines (RseqmxC (addn_R (nat_Rxx m1) (nat_Rxx m2)) @@ -1157,7 +818,7 @@ Global Instance RseqmxC_row_seqmx m1 m2 (rm : nat_R m1 m2) n11 n12 (rn1 : nat_R n11 n12) n21 n22 (rn2 : nat_R n21 n22) : refines (RseqmxC rm rn1 ==> RseqmxC rm rn2 ==> RseqmxC rm (addn_R rn1 rn2)) (@matrix.row_mx R m1 n11 n21) (@row_seqmx C m2 n12 n22). -Proof. param_comp row_seqmx_R. Qed. +Proof. param_comp row_seqmx_R; rewrite refinesE; apply nat_Rxx. Qed. Global Instance refine_row_seqmx m n1 n2 : refines (RseqmxC (nat_Rxx m) (nat_Rxx n1) ==> RseqmxC (nat_Rxx m) (nat_Rxx n2) @@ -1169,7 +830,7 @@ Global Instance RseqmxC_col_seqmx m11 m12 (rm1 : nat_R m11 m12) m21 m22 (rm2 : nat_R m21 m22) n1 n2 (rn : nat_R n1 n2) : refines (RseqmxC rm1 rn ==> RseqmxC rm2 rn ==> RseqmxC (addn_R rm1 rm2) rn) (@matrix.col_mx R m11 m21 n1) (@col_seqmx C m12 m22 n2). -Proof. param_comp col_seqmx_R. Qed. +Proof. param_comp col_seqmx_R; rewrite refinesE; apply nat_Rxx. Qed. Global Instance refine_col_seqmx m1 m2 n : refines (RseqmxC (nat_Rxx m1) (nat_Rxx n) ==> RseqmxC (nat_Rxx m2) (nat_Rxx n) @@ -1183,7 +844,7 @@ Global Instance RseqmxC_block_seqmx m11 m12 (rm1 : nat_R m11 m12) m21 m22 refines (RseqmxC rm1 rn1 ==> RseqmxC rm1 rn2 ==> RseqmxC rm2 rn1 ==> RseqmxC rm2 rn2 ==> RseqmxC (addn_R rm1 rm2) (addn_R rn1 rn2)) (@matrix.block_mx R m11 m21 n11 n21) (@block_seqmx C m12 m22 n12 n22). -Proof. param_comp block_seqmx_R. Qed. +Proof. param_comp block_seqmx_R; rewrite refinesE; apply nat_Rxx. Qed. Global Instance refine_block_seqmx m1 m2 n1 n2 : refines (RseqmxC (nat_Rxx m1) (nat_Rxx n1) ==> @@ -1195,14 +856,374 @@ Global Instance refine_block_seqmx m1 m2 n1 n2 : (@matrix.block_mx R m1 m2 n1 n2) (@block_seqmx C m1 m2 n1 n2). Proof. exact: RseqmxC_block_seqmx. Qed. +Global Instance RseqmxC_tr m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) : + refines (RseqmxC rm rn ==> RseqmxC rn rm) trmx (@trseqmx C m2 n2). +Proof. param_comp trseqmx_R. Qed. + +Global Instance refine_trseqmx m n : + refines (RseqmxC (nat_Rxx m) (nat_Rxx n) ==> RseqmxC (nat_Rxx n) (nat_Rxx m)) + trmx (@trseqmx C m n). +Proof. exact: RseqmxC_tr. Qed. + +End seqmx_param. +End seqmx. + +Section seqmx_ring. + +Variable R : ringType. + +(* The "Global" is needed for lemma RseqmxC_char_poly_mx below. *) +Global Instance zeroR : zero_of R := 0%R. +Local Instance oneR : one_of R := 1%R. +Local Instance oppR : opp_of R := -%R. +Local Instance addR : add_of R := +%R. +Local Instance mulR : mul_of R := *%R. +Local Instance eqR : eq_of R := eqtype.eq_op. +Local Instance specR_ring : spec_of R R := spec_id. + +Local Instance implem_ord_ring : forall n, (implem_of 'I_n 'I_n) := + fun _ => implem_id. + +Local Open Scope rel_scope. + +Instance Rseqmx_diag_seqmx m1 m2 (rm : nat_R m1 m2) : + refines (Rseqmx (nat_R_S_R nat_R_O_R) rm ==> Rseqmx rm rm) + diag_mx (diag_seqmx (A:=R)). +Proof. + rewrite refinesE=> _ _ [M sM h1 h2 h3]. + constructor=> [|i ltim|i j]. + by rewrite size_map ord_enum_eqE size_enum_ord h2. + by rewrite /diag_seqmx /mkseqmx_ord ord_enum_eqE h2 // + (nth_map (Ordinal ltim)) ?size_enum_ord // + size_map size_enum_ord. + rewrite mxE h3 /diag_seqmx /mkseqmx_ord ord_enum_eqE h2 // -(nat_R_eq rm) + (nth_map i) ?size_enum_ord // (nth_map j) ?size_enum_ord // + !nth_ord_enum. + by case: (i == j). +Qed. + +Existing Instance Rseqmx_const_seqmx. + +Instance Rseqmx_scalar_seqmx m1 m2 (rm : nat_R m1 m2) : + refines (eq ==> Rseqmx rm rm) scalar_mx (scalar_seqmx (A:=R) m2). +Proof. + rewrite refinesE=> x y rxy. + rewrite /scalar_seqmx -diag_const_mx. + exact: refinesP. +Qed. + +Instance Rseqmx_1 m1 m2 (rm : nat_R m1 m2) : + refines (Rseqmx rm rm) 1%:M (seqmx1 (A:=R) m2). +Proof. + rewrite /seqmx1. + eapply refines_apply; first exact: Rseqmx_scalar_seqmx. + by rewrite refinesE. +Qed. + +Instance Rseqmx_opp m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) : + refines (Rseqmx (R:=R) rm rn ==> Rseqmx rm rn) -%R -%C. +Proof. +rewrite refinesE=> ? ? [A M h1 h2 h3]. +constructor=> [|i ltim|i j]; first by rewrite size_map h1. + rewrite (nth_map [::]); last by rewrite h1. + by rewrite size_map h2. +rewrite mxE (nth_map [::]); last by rewrite h1 -(nat_R_eq rm) ltn_ord. +rewrite (nth_map 0); first by rewrite h3. +by rewrite h2 -?(nat_R_eq rm) -?(nat_R_eq rn) ltn_ord. +Qed. + +Instance Rseqmx_add m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) : + refines (Rseqmx (R:=R) rm rn ==> Rseqmx rm rn ==> Rseqmx rm rn) +%R +%C. +Proof. + rewrite refinesE=> _ _ [M sM h1 h2 h3] _ _ [N sN h'1 h'2 h'3]. + constructor=> [|i ltim|i j]; rewrite [(_ + _)%C]zipwithE. + by rewrite size_map size1_zip h1 ?h'1. + by rewrite (nth_map ([::], [::])) ?nth_zip ?zipwithE ?size_map ?size1_zip /= + ?h1 ?h'1 ?h2 ?h'2 ?ltim. + by rewrite (nth_map ([::], [::])) ?nth_zip /= ?size1_zip ?h1 ?h'1 + -?(nat_R_eq rm) ?ltn_ord // mxE h3 h'3 zipwithE + -[[seq _ | _ <- _]](mkseq_nth 0%C) nth_mkseq /= + ?(nth_map (0%C, 0%C)) ?nth_zip ?size_map /= ?size1_zip ?h2 ?h'2 + -?(nat_R_eq rm) -?(nat_R_eq rn) ?ltn_ord. +Qed. + +Instance Rseqmx_sub m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) : + refines (Rseqmx (R:=R) rm rn ==> Rseqmx rm rn ==> Rseqmx rm rn) + (fun M N => M - N) sub_op. +Proof. + rewrite refinesE=> _ _ [M sM h1 h2 h3] _ _ [N sN h'1 h'2 h'3]. + constructor=> [|i ltim|i j]; rewrite [(_ - _)%C]zipwithE. + by rewrite size_map size1_zip ?size_map h1 ?h'1. + by rewrite (nth_map ([::], [::])) ?nth_zip ?zipwithE ?size_map ?size1_zip /= + ?(nth_map [::]) ?size_map ?h1 ?h'1 ?h2 ?h'2 ?ltim. + by rewrite !mxE h3 h'3 (nth_map ([::], [::])) ?zipwithE ?(nth_map (0%C, 0%C)) + ?nth_zip /= ?(nth_map [::]) ?size1_zip ?size_map ?(nth_map 0%C) + ?h1 ?h'1 ?h2 ?h'2 -?(nat_R_eq rm) -?(nat_R_eq rn) ?ltn_ord. +Qed. + +Instance Rseqmx_mul m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) + p1 p2 (rp : nat_R p1 p2) : + refines (Rseqmx (R:=R) rm rn ==> Rseqmx rn rp ==> Rseqmx rm rp) + mulmx (@hmul_op _ _ _ m2 n2 p2). +Proof. + case: rn=> [|k1 k2 rk]; + rewrite refinesE=> _ _ [M sM h1 h2 h3] _ _ [N sN h'1 h'2 h'3]. + constructor=> [|i ltim|i j]; rewrite /hmul_op /mul_seqmx /seqmx0. + by rewrite size_nseq. + by rewrite nth_nseq h1 ltim size_nseq. + by rewrite nth_nseq h1 -(nat_R_eq rm) ltn_ord nth_nseq -(nat_R_eq rp) + ltn_ord mxE big_ord0. + constructor=> [|i ltim|i j]; rewrite /hmul_op /mul_seqmx. + by rewrite size_map. + by rewrite (nth_map [::]) ?h1 // size_map /trseqmx /= size_fold ?h'1. + rewrite (nth_map [::]) ?h1 -?(nat_R_eq rm) // (nth_map [::]) /trseqmx + ?size_fold ?h'1 ?h'2 // -?(nat_R_eq rp) //. + set F := (fun z x y => _). + have ->: forall s1 s2 (t : R), (foldl2 F t s1 s2) = + (t + \sum_(0 <= k < minn (size s1) (size s2)) s1`_k * s2`_k). + elim=>[s2 t|t1 s1 IHs s2 t]. + by rewrite min0n big_mkord big_ord0 GRing.addr0. + case:s2=>[|t2 s2]; first by rewrite minn0 big_mkord big_ord0 GRing.addr0. + by rewrite /= IHs minSS big_nat_recl // /F [(_ + t)%C]addrC addrA. + rewrite add0r big_mkord size_nth_fold ?h'1 ?h2 -?(nat_R_eq rm) // + ?(nat_R_eq rp) // /minn if_same mxE -(nat_R_eq rk). + apply: eq_bigr=> k _. + by rewrite h3 h'3 nth_fold ?h'1 ?(nat_R_eq rp) // -(nat_R_eq rk). +Qed. + +Instance Rseqmx_scale m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) : + refines (eq ==> Rseqmx (R:=R) rm rn ==> Rseqmx rm rn) *:%R *:%C. +Proof. + rewrite refinesE=> _ x -> _ _ [M sM h1 h2 h3]. + constructor=> [|i ltim|i j]; rewrite [(_ *: _)%C]/scale_seqmx. + by rewrite size_map. + by rewrite (nth_map [::]) ?size_map ?h1 ?h2. + by rewrite mxE (nth_map [::]) ?(nth_map 0%C) ?h1 ?h2 ?h3 -?(nat_R_eq rm) + -?(nat_R_eq rn). +Qed. + +Lemma eq_seqE (T : Type) (f : T -> T -> bool) s1 s2 : size s1 = size s2 -> + eq_seq f s1 s2 = all (fun xy => f xy.1 xy.2) (zip s1 s2). +Proof. +elim: s1 s2 => [|x1 s1 IHs] [] //= x2 s2 /eqP eq_sz. +by rewrite IHs //; apply/eqP. +Qed. + +Instance Rseqmx_eq m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) : + refines (Rseqmx (R:=R) rm rn ==> Rseqmx rm rn ==> bool_R) eqtype.eq_op eq_op. +Proof. + rewrite refinesE=> _ _ [M sM h1 h2 h3] _ _ [N sN h'1 h'2 h'3]. + suff ->: (M == N) = (eq_seq (eq_seq eqR) sM sN). + exact: bool_Rxx. + apply/eqP/idP=> [/matrixP heq|]. + rewrite eq_seqE ?h1 ?h'1 //. + apply/(all_nthP ([::], [::]))=> i. + rewrite size1_zip ?nth_zip ?h1 ?h'1 //=; move=> ltim. + rewrite eq_seqE ?h2 ?h'2 //. + apply/(all_nthP (0, 0))=> j. + rewrite size1_zip ?nth_zip ?h2 ?h'2 //= -(nat_R_eq rn); move=> ltjn. + rewrite -(nat_R_eq rm) in ltim. + have := heq (Ordinal ltim) (Ordinal ltjn); rewrite h3 h'3=> ->. + by apply/eqP. + rewrite eq_seqE ?h1 ?h'1 //. + move/(all_nthP ([::], [::])). + rewrite size1_zip ?h1 ?h'1 //; move=> heq. + apply/matrixP=> i j. + have := heq i; rewrite -(nat_R_eq rm) ltn_ord; move/implyP; rewrite implyTb. + rewrite nth_zip ?h1 ?h'1 //= eq_seqE ?h2 ?h'2 -?(nat_R_eq rm) //. + move/(all_nthP (0, 0))=> /(_ j). + rewrite nth_zip ?size1_zip ?h2 ?h'2 -?(nat_R_eq rm) //= h3 h'3 -?(nat_R_eq rn) + (ltn_ord _) /eqR. + move=> he. + by apply/eqP; rewrite he. +Qed. + +Instance Rseqmx_delta_seqmx m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) + (i1 : 'I_m1) (i2 : 'I_m2) (ri : nat_R i1 i2) (j1 : 'I_n1) (j2 : 'I_n2) + (rj : nat_R j1 j2) : + refines (Rseqmx (R:=R) rm rn) (delta_mx i1 j1) (delta_seqmx m2 n2 i2 j2). +Proof. + rewrite refinesE -(nat_R_eq ri) -(nat_R_eq rj); constructor=> [|k ltkm|k l]. + by rewrite size_map ord_enum_eqE size_enum_ord. + by rewrite (nth_map (Ordinal ltkm)) !ord_enum_eqE ?size_enum_ord // size_map + size_enum_ord. + rewrite mxE /delta_seqmx /mkseqmx_ord !ord_enum_eqE -(nat_R_eq rm) + -(nat_R_eq rn) (nth_map k) ?size_enum_ord // (nth_map l) + ?size_enum_ord // !nth_ord_enum. + by case: ifP. +Qed. + +Instance Rseqmx_trace_seqmx m1 m2 (rm : nat_R m1 m2) : + refines (Rseqmx rm rm ==> eq) mxtrace (trace_seqmx (A:=R) (m:=m2)). +Proof. + apply refines_abstr. + rewrite !refinesE /mxtrace. + elim: rm=> [|n1 n2 rn ih] /= M sM rM. + by rewrite big_ord0. + rewrite big_ord_recl -(ih (drsubmx (M : 'M_(1 + n1, 1 + n1)))). + have <- : M ord0 ord0 = top_left_seqmx sM. + apply refinesP; rewrite -[M _ _]/((fun (M : 'M_(_)) => M _ _) _). + eapply refines_apply. + apply Rseqmx_top_left_seqmx. + rewrite refinesE; eassumption. + apply: congr2=> //; apply eq_bigr=> i _. + by rewrite -[in LHS](@submxK R 1 n1 1 n1 M) -zmodp.rshift1 + [LHS](@block_mxEdr R 1 n1 1 n1). + apply refinesP; eapply refines_apply. + apply Rseqmx_drsubseqmx. + rewrite refinesE. + have H : nat_R_S_R rn = addn_R (nat_R_S_R nat_R_O_R) rn by []. + rewrite H in rM. + eassumption. +Qed. + +Instance Rseqmx_pid_seqmx m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) + r1 r2 (rr : nat_R r1 r2) : + refines (Rseqmx (R:=R) rm rn) (pid_mx r1) (pid_seqmx m2 n2 r2). +Proof. + rewrite refinesE; constructor=> [|i ltim|i j]. + by rewrite size_map ord_enum_eqE size_enum_ord. + by rewrite (nth_map (Ordinal ltim)) !ord_enum_eqE ?size_enum_ord // size_map + size_enum_ord. + rewrite mxE /pid_seqmx /mkseqmx_ord !ord_enum_eqE -(nat_R_eq rm) + -(nat_R_eq rn) (nth_map i) ?size_enum_ord // (nth_map j) + ?size_enum_ord // !nth_ord_enum -(nat_R_eq rr). + by case: ifP. +Qed. + +Instance Rseqmx_copid_seqmx m1 m2 (rm : nat_R m1 m2) r1 r2 (rr : nat_R r1 r2) : + refines (Rseqmx (R:=R) rm rm) (copid_mx r1) (copid_seqmx m2 r2). +Proof. + rewrite /copid_mx /copid_seqmx /sub_op /sub_seqmx. + eapply refines_apply; tc. + eapply refines_apply; tc. + exact: Rseqmx_pid_seqmx. +Qed. + +Instance Rseqmx_spec_l m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) : + refines (Rseqmx (R:=R) rm rn ==> Logic.eq) spec_id spec. +Proof. + rewrite refinesE=> _ _ [M sM h1 h2 h3]. + rewrite /spec /spec_seqmx /spec_id /spec /specR /spec_id /map_seqmx map_id_in; + last first. + by move=> x; rewrite map_id. + by apply/matrixP=> i j; rewrite h3 mxE. +Qed. + +Section seqmx_ring_param. + +Context (C : Type) (rAC : R -> C -> Type). +Context (I : nat -> Type) + (rI : forall n1 n2, nat_R n1 n2 -> 'I_n1 -> I n2 -> Type). +Context `{zero_of C, one_of C, opp_of C, add_of C, mul_of C, eq_of C}. +Context `{spec_of C R}. +Context `{forall n, implem_of 'I_n (I n)}. +Context `{!refines rAC 0%R 0%C, !refines rAC 1%R 1%C}. +Context `{!refines (rAC ==> rAC) -%R -%C}. +Context `{!refines (rAC ==> rAC ==> rAC) +%R +%C}. +Context `{!refines (rAC ==> rAC ==> rAC) *%R *%C}. +Context `{!refines (rAC ==> rAC ==> bool_R) eqtype.eq_op eq_op}. +Context `{!refines (rAC ==> Logic.eq) spec_id spec}. +Context `{forall n1 n2 (rn : nat_R n1 n2), + refines (ordinal_R rn ==> rI rn) implem_id implem}. + +Notation RseqmxC := (RseqmxC rAC). + +Global Instance RseqmxC_diag_seqmx m1 m2 (rm : nat_R m1 m2) : + refines (RseqmxC (nat_R_S_R nat_R_O_R) rm ==> RseqmxC rm rm) + diag_mx (diag_seqmx (A:=C)). +Proof. param_comp diag_seqmx_R. Qed. + +Global Instance refine_diag_seqmx m : + refines (RseqmxC (nat_R_S_R nat_R_O_R) (nat_Rxx m) ==> + RseqmxC (nat_Rxx m) (nat_Rxx m)) + diag_mx (diag_seqmx (A:=C)). +Proof. exact: RseqmxC_diag_seqmx. Qed. + +Global Instance RseqmxC_scalar_seqmx m1 m2 (rm : nat_R m1 m2) : + refines (rAC ==> RseqmxC rm rm) scalar_mx (scalar_seqmx m2). +Proof. param_comp scalar_seqmx_R; rewrite refinesE; apply nat_Rxx. Qed. + +Global Instance refine_scalar_seqmx m : + refines (rAC ==> RseqmxC (nat_Rxx m) (nat_Rxx m)) scalar_mx (scalar_seqmx m). +Proof. exact: RseqmxC_scalar_seqmx. Qed. + +Global Instance RseqmxC_1 m1 m2 (rm : nat_R m1 m2) : + refines (RseqmxC rm rm) 1%:M (seqmx1 m2). +Proof. param_comp seqmx1_R; rewrite refinesE; apply nat_Rxx. Qed. + +Global Instance refine_1_seqmx m : + refines (RseqmxC (nat_Rxx m) (nat_Rxx m)) 1%:M (seqmx1 m). +Proof. exact: RseqmxC_1. Qed. + +Global Instance RseqmxC_opp m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) : + refines (RseqmxC rm rn ==> RseqmxC rm rn) -%R -%C. +Proof. param_comp opp_seqmx_R. Qed. + +Global Instance refine_opp_seqmx m n : + refines (RseqmxC (nat_Rxx m) (nat_Rxx n) ==> RseqmxC (nat_Rxx m) (nat_Rxx n)) + -%R -%C. +Proof. exact: RseqmxC_opp. Qed. + +Global Instance RseqmxC_add m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) : + refines (RseqmxC rm rn ==> RseqmxC rm rn ==> RseqmxC rm rn) +%R +%C. +Proof. param_comp add_seqmx_R. Qed. + +Global Instance refine_add_seqmx m n : + refines (RseqmxC (nat_Rxx m) (nat_Rxx n) ==> RseqmxC (nat_Rxx m) (nat_Rxx n) + ==> RseqmxC (nat_Rxx m) (nat_Rxx n)) +%R +%C. +Proof. exact: RseqmxC_add. Qed. + +Global Instance RseqmxC_sub m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) : + refines (RseqmxC rm rn ==> RseqmxC rm rn ==> RseqmxC rm rn) + (fun M N => M - N) sub_op. +Proof. param_comp sub_seqmx_R. Qed. + +Global Instance refine_sub_seqmx m n : + refines (RseqmxC (nat_Rxx m) (nat_Rxx n) ==> RseqmxC (nat_Rxx m) (nat_Rxx n) + ==> RseqmxC (nat_Rxx m) (nat_Rxx n)) + (fun M N => M - N) sub_op. +Proof. exact: RseqmxC_sub. Qed. + +Global Instance RseqmxC_mul m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) + p1 p2 (rp : nat_R p1 p2) : + refines (RseqmxC rm rn ==> RseqmxC rn rp ==> RseqmxC rm rp) + mulmx (@hmul_op _ _ _ m2 n2 p2). +Proof. param_comp mul_seqmx_R; rewrite refinesE; apply nat_Rxx. Qed. + +Global Instance refine_mul_seqmx m n p : + refines (RseqmxC (nat_Rxx m) (nat_Rxx n) ==> RseqmxC (nat_Rxx n) (nat_Rxx p) + ==> RseqmxC (nat_Rxx m) (nat_Rxx p)) + mulmx (@hmul_op _ _ _ m n p). +Proof. exact: RseqmxC_mul. Qed. + +Global Instance RseqmxC_scale m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) + : refines (rAC ==> RseqmxC rm rn ==> RseqmxC rm rn) *:%R *:%C. +Proof. param_comp scale_seqmx_R. Qed. + +Global Instance refine_scale_seqmx m n : + refines (rAC ==> RseqmxC (nat_Rxx m) (nat_Rxx n) ==> + RseqmxC (nat_Rxx m) (nat_Rxx n)) *:%R *:%C. +Proof. exact: RseqmxC_scale. Qed. + +Global Instance RseqmxC_eq m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) : + refines (RseqmxC rm rn ==> RseqmxC rm rn ==> bool_R) + eqtype.eq_op eq_op. +Proof. param_comp eq_seqmx_R. Qed. + +Global Instance refine_eq_seqmx m n : + refines (RseqmxC (nat_Rxx m) (nat_Rxx n) ==> RseqmxC (nat_Rxx m) (nat_Rxx n) + ==> bool_R) eqtype.eq_op eq_op. +Proof. exact: RseqmxC_eq. Qed. + Global Instance RseqmxC_delta_seqmx m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) (i1 : 'I_m1) (i2 : 'I_m2) (ri : nat_R i1 i2) (j1 : 'I_n1) (j2 : 'I_n2) (rj : nat_R j1 j2) : - refines (RseqmxC rm rn) (delta_mx i1 j1) (delta_seqmx m2 n2 i2 j2). + refines (RseqmxC rm rn) (delta_mx i1 j1) (delta_seqmx (A:=C) m2 n2 i2 j2). Proof. eapply refines_trans; tc. eapply Rseqmx_delta_seqmx; eassumption. - rewrite refinesE; eapply delta_seqmx_R; exact: refinesP. + rewrite refinesE; eapply delta_seqmx_R; try exact: refinesP; apply nat_Rxx. Qed. Global Instance refine_delta_seqmx m n i j : @@ -1212,7 +1233,7 @@ Proof. apply RseqmxC_delta_seqmx; exact: nat_Rxx. Qed. Global Instance RseqmxC_trace_seqmx m1 m2 (rm : nat_R m1 m2) : refines (RseqmxC rm rm ==> rAC) mxtrace (trace_seqmx (A:=C) (m:=m2)). -Proof. param_comp trace_seqmx_R. Qed. +Proof. param_comp trace_seqmx_R; rewrite refinesE; apply nat_Rxx. Qed. Global Instance refine_trace_seqmx m : refines (RseqmxC (nat_Rxx m) (nat_Rxx m) ==> rAC) @@ -1225,7 +1246,7 @@ Global Instance RseqmxC_pid_seqmx m1 m2 (rm : nat_R m1 m2) n1 n2 Proof. eapply refines_trans; tc. eapply Rseqmx_pid_seqmx; eassumption. - rewrite refinesE; eapply pid_seqmx_R; exact: refinesP. + rewrite refinesE; eapply pid_seqmx_R; try exact: refinesP; apply nat_Rxx. Qed. Global Instance refine_pid_seqmx m n r : @@ -1238,7 +1259,8 @@ Global Instance RseqmxC_copid_seqmx m1 m2 (rm : nat_R m1 m2) r1 r2 Proof. eapply refines_trans; tc. eapply Rseqmx_copid_seqmx; eassumption. - rewrite refinesE; eapply copid_seqmx_R=> *; exact: refinesP. + rewrite refinesE. + eapply copid_seqmx_R=> *; try exact: refinesP; apply nat_Rxx. Qed. Global Instance refine_copid_seqmx m r : @@ -1250,22 +1272,12 @@ Global Instance RseqmxC_spec m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) : Proof. eapply refines_trans; tc. rewrite refinesE /spec /spec_seqmx /spec /specR=> l l' rl. - have -> : forall m n, (l' == seqmx0 m n)%C = (l == seqmx0 m n)%C. - elim: rl=> [i j|x y rx p q rp ih i j] {l l'} /=. - by case: i. - rewrite /eq_op /eq_seqmx /=. - case: i=> [|i] //=. - rewrite [eq_seq _ q _]ih. - apply: congr2=> //=. - elim: rx j=> [j|a b ra l l' rl ihl j] /=; - case: j=> [|j] //=. - by rewrite ihl [(a == _)%C]refines_eq. have -> : map_seqmx spec l = (map_seqmx spec l' : @seqmx R). elim: rl=> [|a b ra p q rp ih] //=. rewrite ih. apply: congr2=> //. elim: ra=> [|x y rxy s t rst ihs] //=. - by rewrite ihs [specR _]refines_eq. + by rewrite ihs [specR_ring _]refines_eq. by []. Qed. @@ -1273,14 +1285,15 @@ Global Instance refine_spec_seqmx m n : refines (RseqmxC (nat_Rxx m) (nat_Rxx n) ==> Logic.eq) spec_id spec. Proof. exact: RseqmxC_spec. Qed. -End seqmx_param. -End seqmx. +End seqmx_ring_param. +End seqmx_ring. Section seqmx2. Local Open Scope rel_scope. -Variable R R' : ringType. +Variable R R' : Type. +Context `{!zero_of R, !zero_of R'}. Instance Rseqmx_map_seqmx m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) : refines (eq ==> Rseqmx (R:=R) rm rn ==> Rseqmx (R:=R') rm rn) @@ -1291,7 +1304,7 @@ Proof. by rewrite (nth_map [::]) ?h1 // size_map h2. rewrite mxE (nth_map [::]) ?h1 -?(nat_R_eq rm) ?ltn_ord //. rewrite (nth_map (M i j)) ?h2 -?(nat_R_eq rm) -?(nat_R_eq rn) ?ltn_ord //. - apply: congr1; rewrite h3 -[X in (nth (_`_ _) X _)](mkseq_nth 0) nth_mkseq //. + apply: congr1; rewrite {1}h3; apply set_nth_default. by rewrite h2 -?(nat_R_eq rm) -?(nat_R_eq rn) ltn_ord. Qed. @@ -1452,4 +1465,4 @@ apply/eqP. Time by coqeal. Abort. -End testmx. \ No newline at end of file +End testmx.