declarative/natural proofs via mixfix syntax  Michael Shulman  3/18/14 4:51 PM  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 poorman'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 informaltoformal translation described in section 1.11 of the book. Has anyone experimented with this sort of idea before? Mike 
Re: [HoTT] declarative/natural proofs via mixfix syntax  Andrea Vezzosi  3/19/14 3:26 AM  Hi, For transitivity chains there's a quite popular syntax:https://github.com/agda/agdastdlib/blob/master/src/Relation/Binary/EqReasoning.agda#L9 http://en.wikipedia.org/wiki/Isabelle_%28proof_assistant%29#Example_proof

Re: [HoTT] declarative/natural proofs via mixfix syntax  Michael Shulman  3/19/14 7:14 AM  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. 
Re: [HoTT] declarative/natural proofs via mixfix syntax  Andrea Vezzosi  3/19/14 7:34 AM  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. 
Re: [HoTT] declarative/natural proofs via mixfix syntax  Andreas Abel  3/19/14 7:38 AM  Looks neat.
I think such a language would be a nice complement to the equalityreasoning 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 "Noops" 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/ 
Re: [HoTT] declarative/natural proofs via mixfix syntax  Bas Spitters  3/20/14 3:10 AM  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 pseudonatural 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 regeneration of declarative scripts.  On Wed, Mar 19, 2014 at 12:51 AM, Michael Shulman <shu...@sandiego.edu> wrote:  