## Stream: Coq users

### Topic: Understanding subset type

#### Julin S (Sep 25 2022 at 06:19):

Hi.

I was trying out subset types and was doing

``````Lemma lt_1_2 : 1 < 2.
Proof.
auto.
Qed.

Check exist _ 1 lt_1_2 : {n:nat | n<2}.
(*
exist (fun n : nat => n < 2) 1 lt_1_2 : {n : nat | n < 2}
: {n : nat | n < 2}
*)
``````

But it seemed to be okay even when leaving a hole in place of the
`lt_1_2` proof.

``````Check exist _ 1 _ : {n:nat | n<2}
(*
exist (fun n : nat => n < 2) 1 ?l : {n : nat | n < 2}
: {n : nat | n < 2}
where
?l : [ |- (fun n : nat => n < 2) 1]
*)
``````

At first I had thought it was coq infering a term of type 1<2.

But I guess that's not the case because it works for 10<2 as well.

``````Check exist _ 10 _ : {n:nat | n<2}.
(*
exist (fun n : nat => n < 2) 10 ?l : {n : nat | n < 2}
: {n : nat | n < 2}
where
?l : [ |- (fun n : nat => n < 2) 10]
*)
``````

What's happening here?

I was basically trying to have a type consisting of all `nat`values which are less than `2`.

#### Paolo Giarrusso (Sep 25 2022 at 06:51):

The type is right; Check is creating an hole ?l of type 10 < 2, it doesn't mean that hole can be filled later

#### Paolo Giarrusso (Sep 25 2022 at 06:53):

to explore that, it might help to step through this sequence:

``````Goal {n | n < 2}.
refine (exist _ 1 _). lia.
Restart.
refine (exist _ 10 _). Fail lia.
``````

#### walker (Sep 25 2022 at 07:10):

may I ask what is the difference between Goal and theorem, and what is `refine` ?

#### Karl Palmskog (Sep 25 2022 at 07:52):

`Goal` doesn't allow you to name the resulting Coq constant, so it's for throwaway results

#### Karl Palmskog (Sep 25 2022 at 07:53):

https://coq.inria.fr/refman/proof-engine/tactics.html#coq:tacn.refine

#### Gaëtan Gilbert (Sep 25 2022 at 09:12):

Karl Palmskog said:

`Goal` doesn't allow you to name the resulting Coq constant, so it's for throwaway results

actually you can name it with `Save` ;)

#### Mukesh Tiwari (Sep 25 2022 at 11:21):

Gaëtan Gilbert said:

actually you can name it with `Save` ;)

Everyday, I discover something new on this channel :)

Last updated: Jun 15 2024 at 05:01 UTC