[Agda] Hanging out with the Lean crowd

[James Wood]

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
>