search

frex-project / idris-frex

Other
46 stars 9 forks source link

[ refactor ] introduce Syntax.PreorderReasoning.Setoid #47

Closed gallais closed 3 years ago

gallais commented 3 years ago

Generated proofs will be hard enough to read without adding an extra layer of cruft by writing e.g. <~ x ...( (cast model).equivalence.symmetry ? ? $ prf ) when we could write ~: x ...( prf ) with a Setoid-specific syntax for reasoning.

May as well refactor the library to use this notation too.

ohad commented 3 years ago

In a different draft branch I re-did it, but I kept the ~~ syntax uniform, and changed the justification syntax ....

Any thoughts about this?

If you think this might be better, I'll wait until you finish with the certification PR and systematically change the syntax in both PRs.

ohad commented 3 years ago

Looks like the refactored refactoring introduces stuff the simplifier doesn't simplify any more?

gallais commented 3 years ago

The expected file looks extremely dodgy

ohad commented 3 years ago

Oh, right. I forgot to copy the expected tex

ohad commented 3 years ago

Looks OK now, doesn't it?

gallais commented 3 years ago

I suppose it is in the nature of commutativity that you can either apply it forward or backward and it doesn't matter. I'm guessing you flipped a direction somewhere during the refactoring hence the changes?

ohad commented 3 years ago

Ah, probably. Esp. if it used an _ to work out the terms it should commute.