Stream: math-comp users

Topic: Term selection under norm


view this post on Zulip Assia Mahboubi (Nov 23 2021 at 11:15):

Hi, why does this fail?

Import GRing.Theory Num.Theory Order.Theory.
Local Open Scope ring_scope.

Lemma test (z : int) : (2 %| `| z |)%N.
set x := (X in `| X |).

view this post on Zulip Assia Mahboubi (Nov 23 2021 at 11:15):

with Error: partial term `|_| does not match any subterm of the goal

view this post on Zulip Ana de Almeida Borges (Nov 23 2021 at 11:18):

I think it's because it's missing the scope annotation. This works:

set x := (X in `| X |%N).

view this post on Zulip Assia Mahboubi (Nov 23 2021 at 11:22):

Thanks!

view this post on Zulip Assia Mahboubi (Nov 23 2021 at 11:22):

But I am still a bit confused

view this post on Zulip Assia Mahboubi (Nov 23 2021 at 11:23):

Notation `| _ | is not related to that scope.

view this post on Zulip Assia Mahboubi (Nov 23 2021 at 11:23):

In the goal, it is used to disambiguate the divisibility predicate.

view this post on Zulip Ana de Almeida Borges (Nov 23 2021 at 11:28):

It is:

From mathcomp Require Import all_ssreflect all_algebra.
Import GRing.Theory Num.Theory Order.Theory.
Local Open Scope ring_scope.

Locate "`| _ |".
(*
Notation "`| m |" := (absz m) : nat_scope
Notation "`| x |" := (Num.Def.normr x) : ring_scope (default interpretation)
*)
Unset Printing Notations.
Lemma test (z : int) : (2 %| `| z |)%N.
(*
  z : int
  ============================
  dvdn 2 (absz z)
*)

So under %N the notation changes from the default Num.Def.normr x to absz.

view this post on Zulip Pierre-Yves Strub (Nov 23 2021 at 11:29):

You can find this in ssrint.v:

Notation "`| m |" := (absz m) : nat_scope.

view this post on Zulip Assia Mahboubi (Nov 23 2021 at 11:30):

Oh thanks. Sorry for the noise.

view this post on Zulip Pierre-Yves Strub (Nov 23 2021 at 11:33):

I had the very same issue (with a rewrite rule not matching). Too much overloading kills overloading :)


Last updated: Feb 02 2023 at 15:04 UTC