Stream: Coq users

Topic: Is this some kind of refinement types

walker (Apr 11 2022 at 14:11):

I received advice here to use this type instead of vectors:

Definition tuple A n := { xs : list A | length xs = n }.

Which I ignored until today because vectors turned out to be hard to work with. I mistook this type for a record but it is not.. I tried finding exactly what is this but I failed to do so, I am struggling with the pipe symbol. and I just don't know how construct elements of this type, so I tried seing how coq cosntructs them and I tried little trick

Theorem x: tuple nat 0.
Proof.
  unfold tuple.
  assert(H: length (@nil nat) = 0 ). {auto. }
  econstructor.
  eauto.
Qed.
Print x.

and what I got is

x =
(let H : length [] = 0 := eq_refl in [] ↾ H) : tuple nat 0
     : tuple nat 0
``` Which is even worse ... I cannot figure out what this flag symbol and I cannot figure out what that pipe symbol is in that specific context.

Ali Caglayan (Apr 11 2022 at 14:12):

This is a sigma type which goes by the name sig.

Ali Caglayan (Apr 11 2022 at 14:14):

Doing Locate sig. gives:

Inductive
sig (A : Type) (P : A -> Prop) : Type :=
    exist : forall x : A, P x -> {x : A | P x}.

Arguments sig [A]%type_scope P%type_scope
Arguments exist [A]%type_scope
  P%function_scope x _

Ali Caglayan (Apr 11 2022 at 14:14):

So the constructor is called exist

Ali Caglayan (Apr 11 2022 at 14:15):

In ltac you can even use the special exists x. tactic to fill in the first field.

Gaëtan Gilbert (Apr 11 2022 at 14:15):

Unset Printing Notations is also your friend

Ali Caglayan (Apr 11 2022 at 14:15):

That might not work in CoqIDE for example however, so you will have to go to the View options. (Which is a terrible usability feature imo)

walker (Apr 11 2022 at 14:16):

yeah that doesn't work in vscoq either :(

Ali Caglayan (Apr 11 2022 at 14:16):

In VsCoq if you do Ctrl+p

Théo Winterhalter (Apr 11 2022 at 14:16):

In vscoq or whatever you can do Locate "{" also.

Ali Caglayan (Apr 11 2022 at 14:16):

and then type >

Ali Caglayan (Apr 11 2022 at 14:17):

And then type Coq

Ali Caglayan (Apr 11 2022 at 14:17):

you should see options to display stuff

walker (Apr 11 2022 at 14:18):

wow! thanks a lot!

walker (Apr 11 2022 at 14:19):

wow I spent an hour searching for the bar thing in coq syntax manual trying to figure out what it is and now I have the general technique to deal with those issues.

Ali Caglayan (Apr 11 2022 at 14:20):

Also Locate is quite smart: Locate "{ x | P }". will give:

Notation "{ x | P }" := (sig (fun x => P))
  : type_scope (default interpretation)

Last updated: Apr 19 2024 at 09:01 UTC