## Stream: math-comp users

### Topic: Understanding coqeal example

#### Julin Shaji (Apr 10 2024 at 09:29):

I am trying to understand the binnat.v example of CoqEAL.
https://github.com/coq-community/coqeal/blob/master/refinements/binnat.v

I was looking at this snippet of it.

``````From mathcomp Require Import all_ssreflect.
From CoqEAL Require Import hrel param refinements pos.
Require Import ZArith.

(* [nat_of_bin] is the specification function *)
Definition Rnat: nat -> N -> Type := fun_hrel nat_of_bin.

Lemma RnatE (n: nat) (x: N): refines Rnat n x -> n = x.
Proof.
rewrite refinesE.
(*
1 subgoal

n : nat
x : N

========================= (1 / 1)

Rnat n x -> n = x
*)
by [].
Qed.
``````

I couldn't figure out how `Rnat n x` is sufficient to show `n = x`.

In fact, how does `n = x` even type check?
`n: nat` and `x: N`. Is there a coercion involved?
(`Print Coercions` gave a huge list which I couldn't make sense of easily.)

A value of `Rnat n x` is just a type (`nat -> N -> Type`), right?
How did that help in showing `n=x`?

Does anyone know what's happening here?

#### Pierre Roux (Apr 10 2024 at 09:42):

You should probably `Set Printing Coercions` or `Set Printing All` if you don't understand what's going on.

#### Julin Shaji (Apr 10 2024 at 10:02):

Thanks.
`Set Printing Coercions` and `rewrite /Rnat /fun_hrel` made it clear.

Last updated: Jul 15 2024 at 20:02 UTC