Stream: Coq users

Topic: What does any value inside `{| ... |}` mean?

kumar (Apr 08 2022 at 15:13):

for example I have a proof that I need to resolve and it has a specific function

  (fun
     _ : {|
           COMPARABLE.compare :=
             fun id1 id2 : Bond_id_repr.t =>
             let
             '(t0, y) := (id1, id2) in
              let
              'Bond_id_repr.Tx_rollup_bond_id id3 := t0 in
               let
               'Bond_id_repr.Tx_rollup_bond_id id4 := y in
                Tx_rollup_repr.compare id3 id4
         |}.(COMPARABLE.t) => True)

what do things in {| .. |} mean?

Ali Caglayan (Apr 08 2022 at 15:25):

That is a constructor of a record. So if you have:

Record A := {
  b : B ;
  c : C ;
}.

and you had x : B, y : C you could have

{| b := x ; c := y |} : A

Ali Caglayan (Apr 08 2022 at 15:26):

If you do Print or About on COMPARABLE.compare you should get more info on the record.

kumar (Apr 08 2022 at 15:46):

oh so multiline assigments in coq are just syntactic sugar over records?

I did do a Print COMPARABLE.compare and I get this

COMPARABLE.compare =
fun (t : Set) (s : COMPARABLE.signature) => s.(COMPARABLE.compare)
     : forall t : Set, COMPARABLE.signature -> t -> t -> int

so this means it returns a Prop Type COMPARABLE.signature -> t -> t -> int

kumar (Apr 08 2022 at 15:53):

but this would be the type of the function input since it's (fun _ : <...>)

Ali Caglayan (Apr 08 2022 at 16:06):

I think if you do Print COMPARABLE.signature you will see the record.

Ali Caglayan (Apr 08 2022 at 16:07):

If this is from CoqOfOcaml then this record probably has two fields COMPARABLE.t and COMPARABLE.compare

Ali Caglayan (Apr 08 2022 at 16:07):

Note that whatever you wrote first is actually a projection of a record {| ... |}.(COMPARABLE.t)

Ali Caglayan (Apr 08 2022 at 16:09):

so this means take the COMPARABLE.signature which has field COMPARABLE.compare as specified and take the COMPARABLE.t projection. Since COMPARABLE.compare takes in a COMPARABLE.t I can deduce that it must be (fun _ : Bond_id_repr.t => True) or something

Ali Caglayan (Apr 08 2022 at 16:10):

If you do unfold COMPARABLE.Build_signature or unfold COMPARABLE.t in your proof that should unfold some things and simplify the goal.

Gaëtan Gilbert (Apr 08 2022 at 16:10):

you can also Unset Printing Records

Last updated: Oct 13 2024 at 01:02 UTC