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?

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`

).

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

what do you mean? `eq_refl`

has no non parameter arguments

where does "non-parameter" come from?

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

@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