From a5b631f7260e7d29defd8bd5c67db543742c9ecd Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 9 May 2016 17:40:04 +0200 Subject: congruence/univs: properly refresh (fix #4609) In congruence, refresh universes including the Set/Prop ones so that congruence works with cumulativity, not restricting itself to the inferred types of terms that are manipulated but allowing them to be used at more general types. This fixes bug #4609. --- pretyping/evarsolve.ml | 7 ++++++- pretyping/evarsolve.mli | 8 ++++++-- 2 files changed, 12 insertions(+), 3 deletions(-) (limited to 'pretyping') diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 29af199a1..c2d47790d 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -47,7 +47,8 @@ let refresh_level evd s = | None -> true | Some l -> not (Evd.is_flexible_level evd l) -let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) pbty env evd t = +let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(propset=false) + pbty env evd t = let evdref = ref evd in let modified = ref false in let rec refresh status dir t = @@ -62,6 +63,10 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) pbty env evd t = else set_leq_sort env !evdref s s' in modified := true; evdref := evd; mkSort s' + | Sort (Prop _ as s) when propset && not dir -> + let s' = evd_comb0 (new_sort_variable status) evdref in + let evd = set_leq_sort env !evdref s s' in + modified := true; evdref := evd; mkSort s' | Prod (na,u,v) -> mkProd (na,u,refresh status dir v) | _ -> t diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index 918ba12f0..9ee815ebc 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -34,8 +34,12 @@ type conv_fun_bool = val evar_define : conv_fun -> ?choose:bool -> env -> evar_map -> bool option -> existential -> constr -> evar_map -val refresh_universes : ?status:Evd.rigid -> - ?onlyalg:bool (* Only algebraic universes *) -> +val refresh_universes : + ?status:Evd.rigid -> + ?onlyalg:bool (* Only algebraic universes *) -> + ?propset:bool -> + (* Also refresh Prop and Set universes, so that the returned type can be any supertype + of the original type *) bool option (* direction: true for levels lower than the existing levels *) -> env -> evar_map -> types -> evar_map * types -- cgit v1.2.3 From 71d4c435e42c24c21ae43f0ddcc7a71bee1009f5 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 9 May 2016 18:31:01 +0200 Subject: congruence: Restrict refreshing to Set Because refreshing Prop is not semantics-preserving, the new universe is >= Set, so cannot be minimized to Prop afterwards. --- kernel/univ.ml | 2 +- plugins/cc/cctac.ml | 2 +- pretyping/evarsolve.ml | 4 ++-- pretyping/evarsolve.mli | 2 +- test-suite/success/cc.v | 14 ++++++++++++++ test-suite/success/congruence.v | 21 --------------------- 6 files changed, 19 insertions(+), 26 deletions(-) delete mode 100644 test-suite/success/congruence.v (limited to 'pretyping') diff --git a/kernel/univ.ml b/kernel/univ.ml index 117bc4e5f..2cc57c38c 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -754,7 +754,7 @@ let is_set_arc u = Level.is_set u.univ let is_prop_arc u = Level.is_prop u.univ exception AlreadyDeclared - + let add_universe vlev strict g = try let _arcv = UMap.find vlev g in diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index ba34d49bb..c8d857b31 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -262,7 +262,7 @@ let assert_before n c = end let refresh_type env evm ty = - Evarsolve.refresh_universes ~status:Evd.univ_flexible ~propset:true + Evarsolve.refresh_universes ~status:Evd.univ_flexible ~refreshset:true (Some false) env evm ty let refresh_universes ty k = diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index c2d47790d..0db309f94 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -47,7 +47,7 @@ let refresh_level evd s = | None -> true | Some l -> not (Evd.is_flexible_level evd l) -let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(propset=false) +let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) pbty env evd t = let evdref = ref evd in let modified = ref false in @@ -63,7 +63,7 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(propset=false) else set_leq_sort env !evdref s s' in modified := true; evdref := evd; mkSort s' - | Sort (Prop _ as s) when propset && not dir -> + | Sort (Prop Pos as s) when refreshset && not dir -> let s' = evd_comb0 (new_sort_variable status) evdref in let evd = set_leq_sort env !evdref s s' in modified := true; evdref := evd; mkSort s' diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index 9ee815ebc..f94c83b6d 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -37,7 +37,7 @@ val evar_define : conv_fun -> ?choose:bool -> env -> evar_map -> val refresh_universes : ?status:Evd.rigid -> ?onlyalg:bool (* Only algebraic universes *) -> - ?propset:bool -> + ?refreshset:bool -> (* Also refresh Prop and Set universes, so that the returned type can be any supertype of the original type *) bool option (* direction: true for levels lower than the existing levels *) -> diff --git a/test-suite/success/cc.v b/test-suite/success/cc.v index a70d91963..0b0e93eb5 100644 --- a/test-suite/success/cc.v +++ b/test-suite/success/cc.v @@ -131,3 +131,17 @@ End bug_2447. +(* Example by Jonathan Leivant, congruence up to universes *) +Section JLeivant. + Variables S1 S2 : Set. + + Definition T1 : Type := S1. + Definition T2 : Type := S2. + + Goal T1 = T1. + congruence. + Undo. + unfold T1. + congruence. + Qed. +End JLeivant. diff --git a/test-suite/success/congruence.v b/test-suite/success/congruence.v deleted file mode 100644 index 873d2f9f7..000000000 --- a/test-suite/success/congruence.v +++ /dev/null @@ -1,21 +0,0 @@ -(* Example by Jonathan Leivant, congruence and tauto up to universes *) -Variables S1 S2 : Set. - -Goal @eq Type S1 S2 -> @eq Type S1 S2. -intro H. -tauto. -Qed. - -Definition T1 : Type := S1. -Definition T2 : Type := S2. - -Goal T1 = T1. -congruence. -Undo. -tauto. -Undo. -unfold T1. -congruence. -Undo. -tauto. -Qed. -- cgit v1.2.3