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: Oct 13 2024 at 01:02 UTC