add proof of decEq x x = Yes Refl

[clayrat]

No description provided.

[david-christiansen]

Why should we have this in the prelude? Has it come up in practice for you? I imagine it's not so useful, because if I already know that something is the same as another, then I can just use Refl directly rather than calling decEq on it.

[clayrat]

I'm doing an Idris translation of "Software foundations" and this has already come up twice when trying to prove things about functions defined via decEq. Typically you get to the point where the arguments are the same and then there's an error that smth like Decidable.Equality.Nat implementation of Decidable.Equality.DecEq, method decEq n n could not be reduced to get to the goal. Doing rewrite decEqSelfIsYes {x=n} solves this.

[david-christiansen]

Thanks, that makes sense. It would be useful for this kind of context to be part of the PR message in the future.

[clayrat]

Sure, I'll try to be more informative in the future!

[melted]

There's too much stuff in the prelude that don't belong there already. There should be a high bar to get in. Why does this need to be usable in every idris file without importing?

…

9 juli 2017 kl. 22:15 skrev Alex Gryzlov ***@***.***>: @clayrat commented on this pull request. In libs/prelude/Decidable/Equality.idr: > @@ -30,6 +22,20 @@ interface DecEq t where total decEq : (x1 : t) -> (x2 : t) -> Dec (x1 = x2) -------------------------------------------------------------------------------- +-- Utility lemmas +-------------------------------------------------------------------------------- + +||| The negation of equality is symmetric (follows from symmetry of equality) +total negEqSym : {a : t} -> {b : t} -> (a = b -> Void) -> (b = a -> Void) +negEqSym p h = p (sym h) + +||| Everything is decidably equal to itself +total decEqSelfIsYes : DecEq a => {x : a} -> decEq x x = Yes Refl +decEqSelfIsYes {x} with (decEq x x) I'm doing an Idris translation of "Software foundations" and this has already come up twice when trying to prove things about functions defined via decEq. Typically you get to the point where the arguments are the same and then there's an error that smth like Decidable.Equality.Nat implementation of Decidable.Equality.DecEq, method decEq n n could not be reduced to get to the goal. Doing rewrite decEqSelfIsYes {x=n} solves this. — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub, or mute the thread.

[ahmadsalim]

I think @melted is hinting that base or contrib are more appropriate for this function.

[clayrat]

My reasoning is that since decEq is in Prelude, being able to prove things about it is sorta fundamental. It would be nice if we didn't need this lemma, but I couldn't find another way. If you think this is too much of a hack, I can close the PR; or, if you agree this is useful, I can move it to base/contrib - just tell me which is it :)

[david-christiansen]

Given that this is something that has come up in practice, I think it's OK in the Prelude along with DecEq. If it's there, then :search and :apropos can find it, while putting it in base or contrib seems likely to ensure that it's never found by anyone but the author.

But for a Prelude change, we also need a CHANGELOG entry. Then I'm happy.

[clayrat]

Done.

[david-christiansen]

I'm happy with a merge, but I don't want to do it unilaterally - it sounds like @melted has concerns about library bloat and like @ahmadsalim may as well. What do the two of you think, given that it has been useful?

[melted]

It's ok to merge for me, but if discoverability is a problem for putting things outside the prelude, that needs to be fixed.

…

12 juli 2017 kl. 15:26 skrev David Christiansen ***@***.***>: I'm happy with a merge, but I don't want to do it unilaterally - it sounds like @melted has concerns about library bloat and like @ahmadsalim may as well. What do the two of you think, given that it has been useful? — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub, or mute the thread.

[ahmadsalim]

Yeah, LGTM.

[david-christiansen]

@melted This would indeed be good to fix, and it's an interesting thing to do research on. Referring to "proofy" things by their propositional content rather than their name might be one approach. But we're not there yet.

[david-christiansen]

Thanks, @clayrat!

[ahmadsalim]

@david-christiansen I am not sure I understand, how do :search and :apropos work today, and why would they not work with base and contrib

[david-christiansen]

They only search what's imported.

[melted]

@david-christiansen don't they search what's loaded? Base is losded but not imported.

[david-christiansen]

There's an optional parameter to get them to do that, but it makes them a lot slower and doesn't get used a lot in practice.

[justjoheinz]

What is the optional parameter, David? I would love to set this as a standard in my projects. Wasting a bit of time with ":s" searches seems to be a much better solution for me than greping through the code base. Markus 2017-07-13 15:22 GMT+02:00 David Christiansen <[email protected]>:

…

There's an optional parameter to get them to do that, but it makes them a lot slower and doesn't get used a lot in practice. — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#3905 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AAX75MomJ_4uAUxYPqGj17Blnnv2JPfmks5sNhorgaJpZM4OSI5l> .

[jfdm]

@justjoheinz the syntax is:

:search (<comma sep. list of packages>) <expr>

For example:

:search (foo,bar,foobar) Int -> Int