declarative/natural proofs via mixfix syntax

[Michael Shulman]

This is not exactly about HoTT per se, but afficionados of informal
type theory may be interested.

On a lark, it occurred to me that one can implement a poor-man's
"declarative" or "natural language" proof language inside type theory,
just by using verbose mixfix syntax; see attached (the examples start
at "Tautologies"). Of course, it has limitations relative to a fully
designed declarative proof language (notably the utter unhelpfulness
of the error messages when you get the syntax slightly wrong), but I
thought it was interesting. In a sense, one could regard it as an
"implementation" of the informal-to-formal translation described in
section 1.11 of the book. Has anyone experimented with this sort of
idea before?

Mike

[Andrea Vezzosi]

Hi,

For transitivity chains there's a quite popular syntax:

https://github.com/agda/agda-stdlib/blob/master/src/Relation/Binary/EqReasoning.agda#L9

And I've never used it but Isar looks similar to what you have:

http://en.wikipedia.org/wiki/Isabelle_%28proof_assistant%29#Example_proof

I like the idea of stressing more the types than the proof terms when you're not quite programming, but maybe more concisely would be better.

Cheers,

Andrea

--
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Michael Shulman]

Maybe I should have been more clear. I'm familiar with the fact that there are many proof assistants with declarative syntax out there; I was specifically asking if anyone has tried implementing such a syntax "at user level" using mixfix binders.

[Andrea Vezzosi]

Ah, fair enough.

The EqReasoning example is done at the user level with mixfix binders, I'm not aware of attempts that go beyond that.

[Andreas Abel]

Looks neat.

I think such a language would be a nice complement to the
equality-reasoning syntax Agda already has (which is also just a verbose
mixfix syntax for transitivity).

I sometimes wished for a more declarative proof language that allows to
read out proofs, but never gone beyond the aliases for the identity
functions you have in section "No-ops" of your file.

Cheers,
Andreas

--
Andreas Abel <>< Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andrea...@gu.se
http://www2.tcs.ifi.lmu.de/~abel/

[Bas Spitters]

Nice! I haven't seen this use of mixfix before, although Ltac has been exploited to do similar things in Coq.

In fact, mixfix was not present at the time Czar and its precursors were written.

This one may not be entirely unrelated, it's been a while since I looked at it:
http://www.cs.unibo.it/~sacerdot/PAPERS/jar_plmms.pdf
---
We present a declarative language inspired by the pseudo-natural language previously used in Matita for the explanation of proof terms. We show how to compile the language to proof terms and how to automatically generate declarative scripts from proof terms. Then we investigate the relationship between the two translations, identifying the amount of proof structure preserved by compilation and re-generation of declarative scripts.
----

On Wed, Mar 19, 2014 at 12:51 AM, Michael Shulman <shu...@sandiego.edu> wrote: