Patrick Nicodemus (May 31 2022 at 06:31): Patrick Nicodemus (May 31 2022 at 06:31):I don't fully understand the documentation of SProp.
https://coq.inria.fr/refman/addendum/sprop.html#basic-constructs
Most inductives types defined in SProp are squashed types, i.e. they can only be eliminated to construct proofs of other strict propositions. Empty types are the only exception.
However I seem to be able to eliminate out of an inhabited type.
Inductive sUnit : SProp := stt.
Definition abc (x : sUnit) : nat :=
match x with
| _ => 0
end.
The code above works for me and the function returns zero.
Pierre-Marie Pédrot (May 31 2022 at 06:36):This is not an inductive elimination, because your pattern is a wildcard. In this case this boils down to a let-binding.
Pierre-Marie Pédrot (May 31 2022 at 06:37):If you print the term you'll actually see this.
Pierre-Marie Pédrot (May 31 2022 at 06:37):(Correcting myself: not even a let binding, it disappears altogether. A let-binding would be there if the wildcard is turned into a bound variable.)
Pierre-Marie Pédrot (May 31 2022 at 06:38):This is not specific to SProp, it's just the standard compilation of complex pattern-matching to simple ones.
Patrick Nicodemus (May 31 2022 at 06:44):I see, nice. That's interesting.
Gaëtan Gilbert (May 31 2022 at 08:27):Pierre-Marie Pédrot said:
(Correcting myself: not even a let binding, it disappears altogether. A let-binding would be there if the wildcard is turned into a bound variable.)
not even then IIRC
Last updated: Sep 09 2024 at 06:02 UTC