Stream: Coq devs & plugin devs

Topic: SProp, pose and change


view this post on Zulip Kenji Maillard (Oct 29 2021 at 10:32):

I stumbled upon a strange interaction of pose with change on an inductive in SProp:

Inductive P : SProp := C.

Goal forall (f : P -> Type) (x : P), f x.
  intros f x.
  (* Works as expected *)
  Fail Fail change x with C.

  pose (t := C).
  (* Does not work ??? *)
  Fail change x with t.

  (* Works if we explicitly unfold *)
  let tu := eval unfold t in t in change x with tu.

I am not sure were the problem is coming from and I didn't find a corresponding issue on github, should I open one ?
cc @Gaëtan Gilbert

view this post on Zulip Gaëtan Gilbert (Oct 29 2021 at 10:34):

classic bad relevance
it may be possible to get pose to generate correct relevance so worth an issue imo

view this post on Zulip Pierre-Marie Pédrot (Oct 29 2021 at 11:11):

A way to print the relevances in debug mode would be appreciated btw.

view this post on Zulip Pierre-Marie Pédrot (Oct 29 2021 at 11:21):

See https://github.com/coq/coq/pull/15090.

view this post on Zulip Pierre-Marie Pédrot (Oct 29 2021 at 11:21):

Incidentally this fixes the issue I was mentioning last lunch with my descent into madness with prefascist CwFs

view this post on Zulip Kenji Maillard (Oct 29 2021 at 11:47):

Filed an issue to keep track of this https://github.com/coq/coq/issues/15091


Last updated: May 28 2023 at 16:30 UTC