new quotient theory with explicit canonical map

Author: oskgo

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.
 

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,21 +21,28 @@ 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.
 
 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.
 

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.
 

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,68 +96,39 @@ 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.
 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.