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`

.

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

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.
```

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

?

`Goal`

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

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

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`

;)

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