Timeline for Less ridiculous way to prove that an Ascii character compares equal with itself in Coq
Current License: CC BY-SA 4.0
3 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| yesterday | comment | added | Julio Di Egidio | @PeterLeFanuLumsdaine Generally speaking, if I have to dig into a library's implementation details in order to use it, then the library is not good enough... Encapsulation is a name for this. | |
| Jun 28 at 9:58 | comment | added | Peter LeFanu Lumsdaine |
Inspecting the proof of that library lemma eq_bool at github.com/coq/coq/blob/master/theories/Strings/Ascii.v#L74 , one can see that it’s proven there using an ad hoc local tactic t_eqb, designed for several “easy” equality lemmas like this that are given there, which simply automatically repeatedly tries applying basic lemmas on equality of Booleans and destructing the goal.
|
|
| Jun 27 at 9:41 | history | answered | Julio Di Egidio | CC BY-SA 4.0 |