diff --git a/theories/algebra/DynMatrix.eca b/theories/algebra/DynMatrix.eca index f7fc2bce4..c9ad1e11c 100644 --- a/theories/algebra/DynMatrix.eca +++ b/theories/algebra/DynMatrix.eca @@ -42,39 +42,17 @@ type prevector = (int -> R) * int. op vclamp (pv: prevector): prevector = ((fun i => if 0 <= i < pv.`2 then pv.`1 i else zeror), max 0 pv.`2). -lemma vclamp_idemp pv: vclamp (vclamp pv) = vclamp pv. -proof. rewrite /vclamp /#. qed. - -op eqv (pv1 pv2: prevector) = - vclamp pv1 = vclamp pv2. - -lemma eqv_vclamp pv: eqv pv (vclamp pv). -proof. by rewrite /eqv vclamp_idemp. qed. - -clone import Quotient.EquivQuotient as QuotientVec with - type T <- prevector, - op eqv <- eqv - rename [type] "qT" as "vector" - proof * by smt(). - -type vector = QuotientVec.vector. - -op tofunv v = vclamp (repr v). - -op offunv pv = pi (vclamp pv). - -lemma tofunvK: cancel tofunv offunv. -proof. -rewrite /tofunv /offunv /cancel => v; rewrite vclamp_idemp. -by rewrite -{2}[v]reprK -eqv_pi /eqv vclamp_idemp. -qed. - -lemma offunvK pv: tofunv (offunv pv) = vclamp pv. -proof. by rewrite /tofunv /offunv eqv_repr vclamp_idemp. qed. - -lemma vectorW (P : vector -> bool): - (forall pv, P (offunv pv)) => forall v, P v. -proof. by move=> P_pv v; rewrite -tofunvK; apply: P_pv. qed. +clone include Quotient.CanonQuotient with +type T <- prevector, +op canon <- vclamp +rename "canon" as "vclamp" +rename "repr" as "tofunv" +rename "pi" as "offunv" +rename "qT" as "vector" +rename "quot" as "vector" +proof * by smt(). + +hint simplify vclampK, offunvK. (* Dimension of the vector *) op size v = (tofunv v).`2. @@ -86,7 +64,7 @@ lemma max0size v: max 0 (size v) = size v by smt(). hint simplify max0size. lemma offunv_max f n: offunv (f, max 0 n) = offunv (f, n). -proof. rewrite /offunv -eqv_pi /eqv /vclamp /#. qed. +proof. by rewrite /offunv /vclamp /#. qed. lemma size_offunv f n: size (offunv (f, n)) = max 0 n. proof. by rewrite /size offunvK /#. qed. @@ -100,7 +78,7 @@ abbrev "_.[_]" (v: vector) (i : int) = get v i. lemma get_offunv f n (i : int) : 0 <= i < n => (offunv (f, n)).[i] = f i. -proof. by rewrite /get /= offunvK /vclamp /= => ->. qed. +proof. by rewrite /get /= /vclamp /= => ->. qed. lemma getv0E v i: !(0 <= i < size v) => v.[i] = zeror by smt(). @@ -665,40 +643,17 @@ op mclamp (pm: prematrix): prematrix = ((fun i j => if 0 <= i < pm.`2 /\ 0 <= j < pm.`3 then pm.`1 i j else zeror), max 0 pm.`2, max 0 pm.`3). -lemma mclamp_idemp pm: mclamp (mclamp pm) = mclamp pm. -proof. by rewrite /mclamp /#. qed. - -hint simplify mclamp_idemp. - -op eqv (pm1 pm2: prematrix) = mclamp pm1 = mclamp pm2. - -clone import Quotient.EquivQuotient as QuotientMat with - type T <- prematrix, - op eqv <- eqv - rename [type] "qT" as "matrix" - proof * by smt(). - -type matrix = QuotientMat.matrix. - -op tofunm m = mclamp (repr m). - -op offunm pm = pi (mclamp pm). - -lemma tofunmK : cancel tofunm offunm. -proof. -rewrite /tofunm /offunm /cancel => m /=. -have ->: pi (mclamp (repr m)) = pi (repr m) by rewrite -eqv_pi /eqv. -apply reprK. -qed. - -lemma offunmK pm: tofunm (offunm pm) = mclamp pm. -proof. by rewrite /tofunm /offunm eqv_repr. qed. - -hint simplify offunmK. +clone include Quotient.CanonQuotient with +type T <- prematrix, +op canon <- mclamp +rename "canon" as "mclamp" +rename "repr" as "tofunm" +rename "pi" as "offunm" +rename "qT" as "matrix" +rename "quot" as "matrix" +proof * by smt(). -lemma matrixW (P : matrix -> bool) : (forall pm, P (offunm pm)) => - forall m, P m. -proof. by move=> P_pm m; rewrite -tofunmK; exact: P_pm. qed. +hint simplify mclampK, offunmK. (* Number of rows and columns of matrices *) op rows m = (tofunm m).`2. @@ -873,7 +828,7 @@ lemma cols_addm (m1 m2: matrix): cols (m1 + m2) = max (cols m1) (cols m2). proof. rewrite /(+) cols_offunm /#. qed. lemma size_addm (m1 m2: matrix): size m1 = size m2 => size (m1 + m2) = size m1. -proof. move => size_eq; rewrite rows_addm cols_addm /#. qed. +proof. move => [rows_eq cols_eq]; rewrite rows_addm cols_addm /#. qed. lemma get_addm (m1 m2 : matrix) i j: (m1 + m2).[i, j] = m1.[i, j] + m2.[i, j]. proof. @@ -1756,7 +1711,7 @@ qed. lemma scalarNm (m: matrix) (s: t): (- s) *** m = - (s *** m). proof. rewrite eq_matrixP. -split => [| i j bound]; 1: rewrite !size_scalarm /=; 1: smt(size_scalarm). +split => [| i j bound]; 1: rewrite !size_scalarm /= rows_scalarm cols_scalarm //. by rewrite /= !get_scalarm /= mulrN. qed. diff --git a/theories/algebra/Matrix.eca b/theories/algebra/Matrix.eca index 336ecd3f2..ebee218ec 100644 --- a/theories/algebra/Matrix.eca +++ b/theories/algebra/Matrix.eca @@ -1,6 +1,7 @@ (* -------------------------------------------------------------------- *) require import AllCore List Distr Perms. require (*--*) Subtype Monoid Ring Subtype Bigalg StdOrder StdBigop. +require (*--*) Quotient. import StdOrder.IntOrder StdBigop.Bigreal. @@ -20,11 +21,7 @@ op size : { int | 0 <= size } as ge0_size. hint exact : ge0_size. (* -------------------------------------------------------------------- *) -type vector. - theory Vector. -op tofunv : vector -> (int -> R). -op offunv : (int -> R) -> vector. op prevector (f : int -> R) = forall i, !(0 <= i < size) => f i = zeror. @@ -32,9 +29,20 @@ op prevector (f : int -> R) = op vclamp (v : int -> R) : int -> R = fun i => if 0 <= i < size then v i else zeror. -axiom tofunv_prevector (v : vector) : prevector (tofunv v). -axiom tofunvK : cancel tofunv offunv. -axiom offunvK : forall v, tofunv (offunv v) = vclamp v. +clone include Quotient.CanonQuotient with +type T <- int -> R, +op canon <- vclamp +rename "canon" as "vclamp" +rename "repr" as "tofunv" +rename "pi" as "offunv" +rename "qT" as "vector" +proof * by smt(). + +lemma tofunv_prevector (v : vector) : prevector (tofunv v). +proof. +rewrite /prevector /= => i i_bd. +by rewrite -isvclamp_tofunv /vclamp i_bd. +qed. op "_.[_]" (v : vector) (i : int) = tofunv v i. @@ -141,7 +149,8 @@ abbrev ( ** ) = scalev. lemma scalevE a v i : (a ** v).[i] = a * v.[i]. proof. -case: (0 <= i < size) => ?; first smt(offunvK tofunvK). +case: (0 <= i < size) => ?. +- by rewrite offunvE. by rewrite !getv_out // mulr0. qed. @@ -172,10 +181,6 @@ export Vector. (* -------------------------------------------------------------------- *) theory Matrix. -type matrix. - -op tofunm : matrix -> (int -> int -> R). -op offunm : (int -> int -> R) -> matrix. abbrev mrange (i j : int) = 0 <= i < size /\ 0 <= j < size. @@ -195,9 +200,20 @@ op prematrix (f : int -> int -> R) = op mclamp (m : int -> int -> R) : int -> int -> R = fun i j : int => if mrange i j then m i j else zeror. -axiom tofunm_prematrix (m : matrix) : prematrix (tofunm m). -axiom tofunmK : cancel tofunm offunm. -axiom offunmK : forall m, tofunm (offunm m) = mclamp m. +clone include Quotient.CanonQuotient with +type T <- int -> int -> R, +op canon <- mclamp +rename "canon" as "mclamp" +rename "repr" as "tofunm" +rename "pi" as "offunm" +rename "qT" as "matrix" +proof * by smt(). + +lemma tofunm_prematrix (m : matrix) : prematrix (tofunm m). +proof. +rewrite /prematrix /= => i j ij_bd. +by rewrite -ismclamp_tofunm /mclamp ij_bd. +qed. op "_.[_]" (m : matrix) (ij : int * int) = tofunm m ij.`1 ij.`2. diff --git a/theories/algebra/PolyReduce.ec b/theories/algebra/PolyReduce.ec index 24e064d75..57fc01497 100644 --- a/theories/algebra/PolyReduce.ec +++ b/theories/algebra/PolyReduce.ec @@ -58,7 +58,8 @@ hint exact : idI. clone include RingQuotientDflInv with op p <- I proof IdealAxioms.* - rename "qT" as "polyXnD1". + rename "qT" as "polyXnD1" + rename "piK" as "piK'". realize IdealAxioms.ideal_p by apply/idI. diff --git a/theories/structure/Quotient.ec b/theories/structure/Quotient.ec index 6626fd19a..0bb246447 100644 --- a/theories/structure/Quotient.ec +++ b/theories/structure/Quotient.ec @@ -29,10 +29,52 @@ proof. by move=> Py x; rewrite -(reprK x); apply/Py; rewrite reprK. qed. end CoreQuotient. +(* -------------------------------------------------------------------- *) +(* This theory defines the effective quotient using an idempotent map, *) +(* canon. It builds on the previous theory by using for [qT] the *) +(* elements that are stable under canon. *) +(* -------------------------------------------------------------------- *) + +abstract theory CanonQuotient. + +type T. + +op canon : T -> T. + +axiom canonK (x : T): canon (canon x) = canon x. + +op iscanon x = canon x = x. + +lemma iscanon_canon x : iscanon (canon x). +proof. by rewrite /iscanon canonK. qed. + +subtype qT as QSub = {x : T | iscanon x}. +realize inhabited by exists (canon witness); apply canonK. + +import QSub. + +(* NOTE: The `canon` in `repr` might look like it does nothing, *) +(* but it can make `iscanon_repr` trivial when `iscanon_canon` is *) +clone include CoreQuotient with + type T <- T, + type qT <- qT, + op pi = fun x => QSub.insubd (canon x), + op repr = fun x => canon (QSub.val x) + + proof *. +realize reprK by move => q; rewrite /pi /repr canonK valP valKd. + +lemma iscanon_repr v : iscanon (repr v) by rewrite iscanon_canon. + +lemma piK x : repr (pi x) = canon x. +proof. by rewrite /repr insubdK // iscanon_canon. qed. + +end CanonQuotient. + (* -------------------------------------------------------------------- *) (* This theory defines the effective quotient by an equivalence *) -(* relation. It is build on the former theory, using for [qT] the *) -(* elements of [T] that are stable by repr \o pi. *) +(* relation. It is build on the former theory, using for canon the *) +(* choice map selecting a member of the equivalence class. *) (* -------------------------------------------------------------------- *) abstract theory EquivQuotient. @@ -54,32 +96,26 @@ proof. by exists x; rewrite eqv_refl. qed. op canon (x : T) = choiceb (eqv x) x. lemma eqv_canon (x : T) : eqv x (canon x). -proof. -rewrite /canon; apply: (@choicebP (eqv x) x). -by exists x; apply: eqv_refl. -qed. +proof. apply (@choicebP (eqv x) x); by exists x; apply eqv_refl. qed. lemma eqv_canon_eq (x y : T): eqv x y => canon x = canon y. proof. -move=> eqv_xy; rewrite /canon (@eq_choice (eqv x) (eqv y)). -- move=> z; split => [eqv_xz|eqv_yz]. - - by apply/(eqv_trans x) => //; rewrite eqv_sym. - - by apply/(eqv_trans _ eqv_xy eqv_yz). -by apply: choice_dfl_irrelevant; exists y; apply: eqv_refl. +move=> eqv_xy; rewrite /canon (@eq_choice (eqv x) (eqv y)) => [z|]. +- split => [eqv_xz|eqv_yz]. + + by apply (eqv_trans x) => //; rewrite eqv_sym. + + by apply (eqv_trans _ eqv_xy eqv_yz). +by apply choice_dfl_irrelevant; exists y; apply eqv_refl. qed. -lemma canonK x : canon (canon x) = canon x. -proof. by rewrite &(eqv_canon_eq) eqv_sym eqv_canon. qed. - -op iscanon x = canon x = x. - -lemma canon_iscanon x : iscanon x => canon x = x. -proof. by move=> @/iscanon /eq_sym ->; apply: canonK. qed. +clone include CanonQuotient with + type T <- T, + op canon <- canon + proof *. +realize canonK by move => x; rewrite &(eqv_canon_eq) eqv_sym eqv_canon. -lemma iscanon_canon x : iscanon (canon x). -proof. by rewrite /iscanon canonK. qed. +import QSub. -lemma eqvP x y : (eqv x y) <=> (canon x = canon y). +lemma eqvP x y : eqv x y <=> canon x = canon y. proof. split=> [/eqv_canon_eq //|eq]. rewrite &(eqv_trans (canon y)) -1:eqv_sym -1:eqv_canon. @@ -87,35 +123,12 @@ apply/(eqv_trans (canon x)); first by apply/eqv_canon. by rewrite eq &(eqv_refl). qed. -subtype qT as QSub = { x : T | iscanon x }. - -realize inhabited. -proof. smt(canonK). qed. - -import QSub. - -clone include CoreQuotient with - type T <- T, - type qT <- qT, - op pi = fun x => QSub.insubd (canon x), - op repr = fun x => QSub.val x - - proof *. - - -realize reprK. proof. -by move=> q; rewrite /pi /repr /insubd canon_iscanon 1:valP valK. -qed. - -lemma eqv_pi : forall x y , eqv x y <=> pi x = pi y. +lemma eqv_pi x y : eqv x y <=> pi x = pi y. proof. -move=> x y @/pi; split=> [eq_xy|]; first by congr; apply: eqv_canon_eq. -by move/(congr1 val); rewrite !val_insubd !iscanon_canon /= => /eqvP. +rewrite eqvP /pi; split => [->//|]. +by move => /(congr1 val); rewrite !val_insubd !iscanon_canon. qed. -lemma eqv_repr : forall x, eqv (repr (pi x)) x. -proof. -move=> x @/pi @/repr; rewrite val_insubd. -by rewrite iscanon_canon /= eqv_sym &(eqv_canon). -qed. +lemma eqv_repr x : eqv (repr (pi x)) x. +proof. rewrite /repr val_insubd iscanon_canon eqv_sym /= canonK eqv_canon. qed. end EquivQuotient.