[Agda] Hanging out with the Lean crowd

[Henning Basold]

Hi James,

As you mentioned universal properties: reasoning about commuting
diagrams in category theory is quite neat to do in Agda, although better
heuristics to figure out implicit arguments need to be implemented. I
suppose this is because equational proofs in CT are usually not very
long and can thus be nicely presented in Agda. I have no experience in
Lean in this regard though.

Cheers,
Henning

On 21/08/2020 23:29, James Wood wrote:
> Hi Ettore,
> 
> Thanks for the question. This is maybe the part of what I wrote which I
> am least confident about, partially because “most other areas of maths”
> comprises an awful lot, and very little of it have I yet studied in
> detail. Apologies, and please point out, if I present any
> misconceptions. To make it answerable, I'll focus on a couple of core
> undergrad topics – analysis and algebra – contrasted with programming
> language metatheory. These are also going to be caricatures – in real
> life, things are not so discrete and extreme.
> 
> Analysis: We're interested in real numbers, basic operations on them,
> sequences & their limits, and continuity of ℝ → ℝ functions. Let's
> assume that we've postulated enough axioms to do classical analysis.
> Then, the reals are characterised as the unique totally ordered,
> Cauchy-complete, field satisfying the Archimedean property, and most
> arguments after establishing that never touch the particular
> implementation (Cauchy vs Dedekind vs whatever) we may use. As such, we
> never do induction on the reals (in the normal sense), so Agda's support
> for pattern-matching doesn't buy us much. We still take cases on
> ordering and do induction on natural numbers, but these features of a
> proof should be clear enough even in a Coq-style tactic script (there
> being at most 3 cases, with quite simple types). Something we really
> want is an algebraic solver for real numbers, to save us from the tedium
> of specifying algebraic manipulations in proofs. Such solvers appear to
> have been worked on more in Coq and Lean (though I'm not sure to what
> extent this is about the systems themselves).
> 
> Algebra: We're interested in some class of algebraic structures, and, of
> such structures, examples, homomorphisms, and ways to construct new
> examples from old examples. The constructions on algebraic structures
> (e.g, direct sums, direct products, tensor products, ...) are usually
> characterised by universal properties, and it is usually much easier to
> appeal to those universal properties than to any construction (similarly
> to what happened with ℝ). When these constructions are given explicitly,
> they are usually done in a seemingly random way, which we later verify
> has the right properties (i.e, we are not being directed by any types).
> And of course within a given structure, the only way to make progress is
> to use the structure's axioms along with anything else you have lying
> around, which again is unlikely to be complex inductive data types.
> 
> Programming languages: We define the syntax of a programming language
> and give it semantics – either operational or denotational. As I
> discussed earlier, the syntax of a programming language is typically
> represented as a complex indexed inductive data type, with on the order
> of 5~15 constructors. We define some similarly complex operations on the
> syntax by recursion, and prove properties of them by induction
> (“induction on the syntax of the term” is a common phrase in papers). An
> operational semantics will typically have even more constructors, while
> a denotational semantics will consist of a dependently typed function
> respecting the typing of a term. A programming language often will be
> characterised by a universal property (as the free such-and-such closed
> category with this-and-that extra bits when quotiented by the equational
> theory), but proving this theorem is typically the last result. The
> predominant style of doing PL metatheory in Agda has it that if you
> manage to define operations of the correct type, then they are almost
> certainly the ones you intended (this is type-directed programming in
> action).
> 
> It may well be that there are some areas of regular mathematics that are
> particularly well suited to the tools Agda provides. There may be yet
> others which could be presented more clearly given those tools (as we
> have seen with data structures from computer science defined to enforce
> their invariants). And sometimes you're forced into a particular proof
> assistant for other reasons – be they theoretical, social, or pedagogical.
> 
> Regards,
> James
> 
> On 21/08/2020 18:48, Ettore Aldrovandi wrote:
>> Hi James, 
>>
>> mathematician lurker here.  This is interesting:
>>
>>> On Aug 21, 2020, at 12:47, James Wood <james.wood.100 at strath.ac.uk
>>> <mailto:james.wood.100 at strath.ac.uk>> wrote:
>>>
>>> Most other areas of maths traditionally don't resemble this
>>> type-directed style of programming. There are few, small, inductive
>>> types, and a lot of reasoning is done at the level of algebraic axioms
>>> (with no inductive types in sight). These features largely nullify
>>> Agda's advantages, and instead the advantages of Lean and Coq in the
>>> field of proving shine through.
>>
>> Can you elaborate a bit?
>>
>> Thanks,
>>
>> —Ettore
>> Ettore Aldrovandi
>> Department of Mathematics, Florida State University
>> 1017 Academic Way                *   http://www.math.fsu.edu/~ealdrov
>> <https://eur02.safelinks.protection.outlook.com/?url=http:%2F%2Fwww.math.fsu.edu%2F~ealdrov&data=02%7C01%7Cjames.wood.100%40strath.ac.uk%7C6c2b818941f540e6bbff08d845fa6f51%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637336289199109081&sdata=pFvPsPeoPm38WBj55%2BzCoe14bVBK4wr3IsGE04LKYGg%3D&reserved=0>
>> Tallahassee, FL 32306-4510, USA * * aldrovandi at math dot fsu dot edu
>>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 
-------------- next part --------------
A non-text attachment was scrubbed...
Name: pEpkey.asc
Type: application/pgp-keys
Size: 3110 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200825/7fb374bd/attachment.bin>