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: Jun 13 2024 at 19:02 UTC