From 996b8096a4b00efb008f08c65e5c03499e052304 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Tue, 5 Dec 2023 15:19:54 +0100 Subject: [PATCH 1/2] Adapt to math-comp/math-comp#1131 --- refinements/examples/irred.v | 10 +++++----- refinements/refinements.v | 1 + refinements/seqmx.v | 4 ++-- refinements/seqpoly.v | 2 +- 4 files changed, 9 insertions(+), 8 deletions(-) diff --git a/refinements/examples/irred.v b/refinements/examples/irred.v index 8adab32..72f0a5f 100644 --- a/refinements/examples/irred.v +++ b/refinements/examples/irred.v @@ -196,15 +196,15 @@ Section enumerable. Context (T : finType) (T' : Type) (RT : T -> T' -> Type). Variable (N : Type) (rN : nat -> N -> Type). Context (enumT' : seq T') - {enumR : refines (perm_eq \o (list_R RT)) (@Finite.enum T) enumT'}. + {enumR : refines (perm_eq \o list_R RT) (@Finite.enum T) enumT'}. Context `{zero_of N} `{one_of N} `{add_of N}. Context `{!refines rN 0%N 0%C}. Context `{!refines rN 1%N 1%C}. -Context `{!refines (rN ==> rN ==> rN)%rel addn add_op}. +Context `{!refines (rN ==> rN ==> rN) addn add_op}. Context (P : pred T) (P' : pred T'). #[export] Instance refines_card : - (forall x x' `{!refines RT x x'}, refines (bool_R \o (@unify _)) (P x) (P' x')) -> + (forall x x' `{!refines RT x x'}, refines (bool_R \o @unify _) (P x) (P' x')) -> refines rN #|[pred x | P x]| (card' enumT' P'). Proof. move=> RP; have := refines_comp_unify (RP _ _ _) => /refines_abstr => {}RP. @@ -274,13 +274,13 @@ Context (iter' : forall T, N -> (T -> T) -> T -> T) {iterR : forall T T' RT, refines (rN ==> (RT ==> RT) ==> RT ==> RT) (@iter T) (@iter' T')}. Context (enumC : seq C) - {enumR : refines (perm_eq \o (list_R rAC)) (@Finite.enum A) enumC}. + {enumR : refines (perm_eq \o list_R rAC) (@Finite.enum A) enumC}. Definition Rnpoly : {poly_n A} -> {poly A} -> Type := fun p q => p = q :> {poly A}. Definition RnpolyC : {poly_n A} -> seqpoly C -> Type := - (Rnpoly \o (RseqpolyC rAC))%rel. + (Rnpoly \o RseqpolyC rAC). #[export] Instance refines_enum_npoly : refines (perm_eq \o list_R RnpolyC) diff --git a/refinements/refinements.v b/refinements/refinements.v index a1debfc..d971a37 100644 --- a/refinements/refinements.v +++ b/refinements/refinements.v @@ -205,6 +205,7 @@ Qed. End refinements. +Arguments refines [A B]%type R%rel m n. Arguments refinesP {T T' R x y} _. #[export] Hint Mode refines - - - + - : typeclass_instances. diff --git a/refinements/seqmx.v b/refinements/seqmx.v index f5fdb07..4021574 100644 --- a/refinements/seqmx.v +++ b/refinements/seqmx.v @@ -666,7 +666,7 @@ Qed. (rn : nat_R n1 n2) f g `{forall x y, refines (rI rm) x y -> forall z t, refines (rI rn) z t -> - refines (rAC \o (@unify _)) (f x z) (g y t)} : + refines (rAC \o @unify _) (f x z) (g y t)} : refines (RseqmxC rm rn) (\matrix_(i, j) f i j) (seqmx_of_fun (I:=I) g). Proof. @@ -680,7 +680,7 @@ Qed. #[export] Instance refine_seqmx_of_fun m n f g `{forall x y, refines (rI (nat_Rxx m)) x y -> forall z t, refines (rI (nat_Rxx n)) z t -> - refines (rAC \o (@unify _)) (f x z) (g y t)} : + refines (rAC \o @unify _) (f x z) (g y t)} : refines (RseqmxC (nat_Rxx m) (nat_Rxx n)) (\matrix_(i, j) f i j) (seqmx_of_fun (I:=I) g). Proof. exact: RseqmxC_seqmx_of_fun. Qed. diff --git a/refinements/seqpoly.v b/refinements/seqpoly.v index f203ae0..0f7e2b9 100644 --- a/refinements/seqpoly.v +++ b/refinements/seqpoly.v @@ -460,7 +460,7 @@ Context `{!refines (rN ==> rN ==> bool_R) eqtype.eq_op eq_op}. Context `{!refines (rN ==> nat_R) spec_id spec}. Definition RseqpolyC : {poly R} -> seq C -> Type := - (Rseqpoly \o (list_R rAC)). + (Rseqpoly \o list_R rAC). #[export] Instance RseqpolyC_cons : refines (rAC ==> RseqpolyC ==> RseqpolyC) (@cons_poly R) cons. From a92948849160e7a12968719b805872a849290cda Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Tue, 5 Dec 2023 17:16:52 +0100 Subject: [PATCH 2/2] Fix --- refinements/examples/irred.v | 2 +- refinements/seqpoly.v | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/refinements/examples/irred.v b/refinements/examples/irred.v index 72f0a5f..576dd9d 100644 --- a/refinements/examples/irred.v +++ b/refinements/examples/irred.v @@ -280,7 +280,7 @@ Definition Rnpoly : {poly_n A} -> {poly A} -> Type := fun p q => p = q :> {poly A}. Definition RnpolyC : {poly_n A} -> seqpoly C -> Type := - (Rnpoly \o RseqpolyC rAC). + (Rnpoly \o RseqpolyC rAC)%rel. #[export] Instance refines_enum_npoly : refines (perm_eq \o list_R RnpolyC) diff --git a/refinements/seqpoly.v b/refinements/seqpoly.v index 0f7e2b9..aa5eb47 100644 --- a/refinements/seqpoly.v +++ b/refinements/seqpoly.v @@ -460,7 +460,7 @@ Context `{!refines (rN ==> rN ==> bool_R) eqtype.eq_op eq_op}. Context `{!refines (rN ==> nat_R) spec_id spec}. Definition RseqpolyC : {poly R} -> seq C -> Type := - (Rseqpoly \o list_R rAC). + (Rseqpoly \o list_R rAC)%rel. #[export] Instance RseqpolyC_cons : refines (rAC ==> RseqpolyC ==> RseqpolyC) (@cons_poly R) cons.