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?

You should probably `Set Printing Coercions`

or `Set Printing All`

if you don't understand what's going on.

Thanks.

`Set Printing Coercions`

and `rewrite /Rnat /fun_hrel`

made it clear.

Last updated: Jul 15 2024 at 20:02 UTC