Stream: Coq users

Topic: on SProp


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (May 31 2022 at 06:37):

If you print the term you'll actually see this.

view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip Patrick Nicodemus (May 31 2022 at 06:44):

I see, nice. That's interesting.

view this post on Zulip 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: Feb 09 2023 at 00:03 UTC