## Stream: Coq users

### Topic: Reflecting definitional equality into bool

#### 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.

#### 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

#### Christopher Lam (Feb 10 2024 at 03:18):

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

#### 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

#### 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?

#### 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