Stream: Coq users

Topic: what does it mean "eliminate proposition into a type"?


view this post on Zulip Andrey Klaus (Jul 13 2023 at 17:05):

I'm trying to understand some things a bit better. Among other things I'm facing phrase "eliminate proposition into a type". It is in context of singleton elimination. In example, singleton elimination does not work for indexed datatypes, as for instance it applies to the equality type of Coq.

What I think I would like to have as an answer is an example of proposition which can be eliminated to a type and the result of a such elimination.

I think we could take such example of type

Inductive elim_test : Prop := ElimTest (t : True).

As far as I can see, singleton elimination should apply here because we have one constructor with one argument of type from Prop. What is the result of elimination process?

view this post on Zulip Gaëtan Gilbert (Jul 13 2023 at 18:12):

for instance you can define fun x : elim_test => match x return nat with ElimTest _ => 0 end
(nat in return nat is the type we are eliminating into)

examples where it's useful:

view this post on Zulip Paolo Giarrusso (Jul 13 2023 at 21:06):

Your second example eliminates an equality, but the quote seems to claim singleton elimination doesn't apply — here the constructor has computational arguments

view this post on Zulip Gaëtan Gilbert (Jul 13 2023 at 21:20):

what do you mean? eq_refl has no non parameter arguments

view this post on Zulip Paolo Giarrusso (Jul 13 2023 at 21:40):

where does "non-parameter" come from?

view this post on Zulip Paolo Giarrusso (Jul 13 2023 at 21:48):

Nevermind; the manual should probably be clarified to say "non-parameter arguments", even if the current text were technically correct for some reason.

A singleton definition has only one constructor and all the arguments of this constructor have type Prop.

https://coq.inria.fr/refman/language/core/inductive.html#destructors

view this post on Zulip Andrey Klaus (Jul 17 2023 at 19:49):

@Gaëtan Gilbert thank you very much for your answer. Great examples! (Actually, I'm reading Definitional Proof Irrelevance Without K.!) I think I'm missing some details now. I'm trying to figure out what exactly. This should take a bit I think. Firstly reading a link by @Paolo Giarrusso (thank you!).


Last updated: Jun 13 2024 at 19:02 UTC