Julin Shaji (Sep 25 2022 at 06:19): Julin Shaji (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.
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.
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:
Goaldoesn'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: Oct 03 2023 at 02:34 UTC