Stream: Coq users

Topic: Reflecting definitional equality into bool


view this post on Zulip Christopher Lam (Feb 09 2024 at 22:10):

Suppose I have two props, P1 and P2. Is there an easy way of reflecting into bool in such a way that if P1 and P2 are definitionally equal, I get true, and if P1 and P2 are not definitionally equal, I get false? It feels like there should be because definitional equality should be decidable, but I don't know of a way of doing it.

view this post on Zulip Gaëtan Gilbert (Feb 09 2024 at 22:57):

if they are definitionally equal, you pick true
otherwise you pick false
this is at the meta level of course

view this post on Zulip Christopher Lam (Feb 10 2024 at 03:18):

I mean is there a way of writing a function that computes this

view this post on Zulip Gaëtan Gilbert (Feb 10 2024 at 09:17):

no
suppose f : Prop -> Prop -> bool was that function
under context x, y : Prop, f x y computes to false, but when x and y are substituted with True the value changes to true
such a behaviour would be broken

view this post on Zulip Emilio Jesús Gallego Arias (Feb 11 2024 at 10:06):

Indeed what you want seems too general Chris, what are you trying to prove?

view this post on Zulip zohaze (Feb 20 2024 at 16:38):

I have non empty list(k::t) and two hypothesis. H1: k <= list_max (k::t) & H2: list_max (k::t) <=k.
From these H1 and H2 , is it possible list_max (k::t) =k?


Last updated: Jun 22 2024 at 16:02 UTC