Stream: Coq users

Topic: Understanding subset type


view this post on Zulip 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 natvalues which are less than 2.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip walker (Sep 25 2022 at 07:10):

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

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Sep 25 2022 at 07:53):

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

view this post on Zulip 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 ;)

view this post on Zulip 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: Feb 04 2023 at 21:02 UTC