Stream: Coq users

Topic: Proof Irrelevance and Program.Equality

view this post on Zulip Thibaut Pérami (Sep 28 2023 at 15:16):

So far in my development, I've mostly used UIP, with Require Import EqDep. I also use Program.Equality for dependent destruction. However, I'm now thinking of switching to requiring proof irrelevance with Require Import ProofIrrelevance. However, it seems to me like Require Import Program.Equality will always import the plain UIP eq_rect_eq axiom, which means I will have both proof irrelevance and UIP as separate axiom without one being defined from the other. Is that a problem? Is there a way to solve this?

view this post on Zulip Li-yao (Sep 28 2023 at 17:35):

I don't know of a solution but I can't imagine how that could be a problem in practice.

view this post on Zulip Théo Winterhalter (Sep 29 2023 at 06:42):

One solution is to use Equations instead of Program because you can provide your own instance of UIP. But indeed, you probably don't have a real problem to begin with.

view this post on Zulip Karl Palmskog (Sep 29 2023 at 06:47):

in many cases, I think the Equations tactics can also avoid using eq_rect_eq for dependent elimination/destruction

Last updated: Jun 23 2024 at 04:03 UTC