Email Gateway (Aug 22 2022 at 17:59): Email Gateway (Aug 22 2022 at 17:59):From: Makarius <makarius@sketis.net>
Great to see such work.
Note that Isabelle/HOL is just one (big and important) library in
Isabelle. Other libraries can be done at any time, without requiring
mutation of the system: it is sufficiently flexible by design.
Historically, one of the first Isabelle applications was actually
Martin-Löf Type Theory (in an early version): see Isabelle/CTT.
Makarius
Email Gateway (Aug 22 2022 at 17:59):From: Dominique Unruh <unruh@ut.ee>
Hi,
I have been wondering about how well Isabelle can be used for reasoning
using type theory.
Of course, it is possible in principle as Isabelle/CTT shows.
But looking at Isabelle/CTT, I see that typing judgments are encoded as
assumptions of axioms/lemmas
(instead of being handled by the Isabelle core as in Isabelle/HOL).
I see now way around this because the type system integrated in the
Isabelle core does not support dependent types.
I wonder how well this can be used in practice?
For example, pattern matching (e.g. in simp, or simply in rule) in HOL will
automatically check/instantiate all types.
But if type judgments are propositions, this needs to be handled using
explicit subgoals.
(For comparison: type classes are integrated into the Isabelle core even
though it would, as far as I can see, be totally fine to just use a single
sort and add preconditions of the form "bla_class TYPE('a)" to all lemmas.
But I would expect that this is much more cumbersome. Yet this is what we
essentially do in Isabelle/CTT.)
Now, I haven't used Isabelle/CTT myself, so I may be overestimating the
difficulties arising from the above.
But my feeling is that it will be difficult to get a nicely usable system
(comparable to what we can do in Isabelle/HOL).
Does anyone have experiences in this direction? I would be interested in
hearing about them (especially if I'm wrong :) ).
Best wishes,
Dominique.
Email Gateway (Aug 22 2022 at 17:59):From: Makarius <makarius@sketis.net>
On 17/08/18 15:47, Dominique Unruh wrote:
I have been wondering about how well Isabelle can be used for reasoning
using type theory.
Of course, it is possible in principle as Isabelle/CTT shows.
But looking at Isabelle/CTT, I see that typing judgments are encoded as
assumptions of axioms/lemmas
(instead of being handled by the Isabelle core as in Isabelle/HOL).
I see now way around this because the type system integrated in the
Isabelle core does not support dependent types.
Isabelle/Pure was invented to support dependent types, but they are
formally just terms. The types of Pure are just abstract syntactic
categories: it is merely accidental that HOL uses these directly as types.
I wonder how well this can be used in practice?
For example, pattern matching (e.g. in simp, or simply in rule) in HOL will
automatically check/instantiate all types.
But if type judgments are propositions, this needs to be handled using
explicit subgoals.
This touches old questions about "soft type systems" in Isabelle/Pure.
More than 10 years ago, I have added explicit programming interfaces for
that, but they are not yet used as ambitiously as the idea behind it.
Since John Harrison has recently proclaimed (again) that we should "make
set theory great again" http://aitp-conference.org/2018/slides/JH.pdf
some colleagues have started to re-open such obvious issues.
In the same line of thought, I have recently proposed to develop
something for set-theory that is analogous to TypeScript as soft
type-system over JavaScript:
https://sketis.net/2018/isabelle-vscode-and-the-language-server-protocol-at-curry-club-augsburg
See page 3 of the Slides, minute 6:20 in the Video (in German); there is
also a brief discussion concerning HoTT.
Makarius
Email Gateway (Aug 22 2022 at 17:59):From: Lawrence Paulson <lp15@cam.ac.uk>
I'm the author of Isabelle/CTT, and I see it is adhering to the spirit of Martin-Löf's original calculus. He didn't imagine any "core" to deal with types, which in any case, play the role of logical formulas and therefore cannot be dealt with automatically.
It's clear that modern type theory systems implement a lot of support for the types that behave like types, to such an extent that the idea of propositions as types is somewhat obscured. This seems to be necessary in order to cope with proofs of reasonable size. Nothing has been done with Isabelle CTT since 1986 or so, so there is a lot of catching up to do.
Larry
Email Gateway (Aug 22 2022 at 18:02):From: Joshua Chen <joshua.chen@uni-bonn.de>
I'm the author of the previously-mentioned HoTT object
logic, and though I'm still quite unfamiliar with many
aspects of both HoTT and Isabelle I thought I could share
what I've found so far.
The state of things is just about as you describe: due to
the lack of native support for dependent types we cannot
embed the HoTT types on the meta-level, hence everything
has to be on the object level.
This means that every term appearing in a statement does
indeed yield typing judgments which need to be proved
explicitly as ancillary subgoals, cluttering the goal
state.
In the current version of my HoTT logic, this issue is
alleviated slightly with somewhat rudimentary Eisbach
methods that are able to perform type inference for most
of the simpler cases, although one must still call such
methods explicitly.
But this means one can usually focus on proving the core
subgoals, leaving the ancillary typing subgoals to the end
to be taken care of automatically.
Isabelle/CTT handles such type inferences in a very
similar manner, there things are sometimes easier due to
extensionality of equality and the lack of universe types.
An interesting difficulty for HoTT that I've faced arises
in relation to proving inhabitation of a type.
If one already knows from "paper" work the form of such a
proof term, this is usually straightforward.
However arguably much of the utility of a proof assistant
arises from its aid in deriving such a proof term in the
first place, and as far as I can tell the only way to do
this is with schematic_goal.
Such derivations often require fixing specific variables
in order to apply an instantiated elimination rule, while
ensuring the variable we want to derive for stays
schematic, in order to continue derivation in a
"sub-schematic goal".
But so far I have not been able to find a way to do this;
we cannot nest schematic_goal commands, nor does
subgoal help because it converts all schematic variables
to fixed free variables.
It's certainly safe to say that using any of the type
theory object logics will at this stage not be as smooth
as using Isabelle/HOL, though I would hope at some point
to see how to write better methods to interface more
directly with the ML and make the proof process in HoTT
easier.
Still very much a work in progress! :)
Best wishes,
Josh
Last updated: Apr 27 2024 at 01:05 UTC