Stream: Coq users

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

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?

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:

• fun x : False => match x return nat with end ie exfalso
• fun (x : a = b) (y : { z : nat | z <= a}) => match x in _ = c return { z : nat | z <= c } with eq_refl => y end ie rewriting in a dependent type (the function has type a = b -> { z : nat | z <= a } -> { z : nat | z <= b }, note that { z : nat | z <= _ } is a Set not a Prop)
• well founded recursion https://coq.inria.fr/stdlib/Coq.Init.Wf.html#Fix_F (although this implementation does not rely on singleton elimination and instead uses the guard condition recognizing Acc_inv a h as a subterm of a, it could also be defined as Fixpoint Fix_F (x:A) (a:Acc x) : P x := match a return P x with Acc_intro _ a' => F (fun (y:A) (h:R y x) => Fix_F (a' h)) end).

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

Gaëtan Gilbert (Jul 13 2023 at 21:20):

what do you mean? eq_refl has no non parameter arguments

Paolo Giarrusso (Jul 13 2023 at 21:40):

where does "non-parameter" come from?

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

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: Oct 08 2024 at 15:02 UTC