Arend 1.8.0 released

Language updates:

• Improved performance
• Inference of unique implicit arguments
• Coercion between paths and functions
• A convenient syntax for defining HITs and pattern matching on them

Plugin updates:

• Proof Search – find declarations by their type (#319)
• Tracer – step-by-step typechecking (#168)
• Re-worked “Arend Messages” panel (#336)
  • Printing customization - control over the way of displaying expressions
• Editing:
  • Live templates – advanced completion for keywords (#252)
  • Optimize imports – detecting and removing unused imports (#11)
  • Extract expression to \let binding
  • Generate function from a goal with arguments

arend-lib:

• New and improved metas:
  • Improved Exists meta and new metas Given and Forall.
  • Improved contradiction meta. Now, it can derive contradictions from transitive closure of <, <=, and =.
  • New simplify meta.
• Locales:
  • The definition of discrete locales and the embedding of rationals into reals.
  • The definition of overt locales and open maps.
  • The construction of dense-closed and strongly dense-weakly closed factorization systems on the category of locales.
  • A proof that nuclei form a frame.
  • Limits and colimits of locales.
  • A characterization of embeddings of locales: a map of locales is a regular monomorphism if and only if the left adjoint is surjective.
  • The definition of (weakly) regular locales and a proof that the locale of reals is regular.
  • The definition of Hausdorff locales and a proof that regular locales are Hausdorff.
  • The definition of uniform locales and the construction of their completion.
• The definition of abstract reduction systems, second-order term rewriting systems, and a proof that the disjoint union of confluent left-linear systems is confluent.
• The definition of algebraic theories, the category of its models, and a proof that it has all small limits and colimits.
• The preorder of subobjects and regular subobjects.
• The construction of the structure sheaf on the spectrum of a ring.

Plugin updates

Proof Search

Nearly every proof assistant has a problem of the discoverability for proven theorems. For instance, try to recall how a lemma describing the commutativity of addition is called in your favorite proof assistant. Is it add_comm? Or +-comm?

The new “Proof Search” action helps in this situation. Invoke it and type in a signature of the declaration you are interested in – the IDE will find the declarations with such a signature:

For more information, please see the full documentation.

Tracer

The tracer is a new feature that allows you typechecking a declaration step-by-step. At each step, the IDE shows you the typechecking context for the current expression.

To use the tracer:

1. Start it via a pop-up menu on a declaration or expression.
2. Step through the expressions back and forth, jump to a specific expression via “Run to Cursor”, and stop early if needed.
3. Inspect the stack and the context in the editor view at each tracing step.

Compared to the “Show Expression Type” action, the tracer works in more contexts, shows more info, but could be slower.

Re-worked “Arend Messages” panel

The “Arend Messages” panel shows current goals and errors. We did a number of changes that are aimed to improve the UX around it:

• Goals and errors are shown in separate panels.
• Goals’ panel is not cleaned up when you remove the goal. It is only removed when a declaration, which contained a goal, has no more errors or other goals.
• Implicit goals (goals without a corresponding {?} element in the source code) are not shown by default.
• The vertical layout is supported.

Printing customization

This feature is incubating, it may be completely changed in future releases, even minor ones.

The proof terms which appear during the development of some theory may be quite large. It is often hard to read and understand them, so in order to show these terms to the user we sometimes omit certain subterms. A typical example of a kind of these subterms is implicit arguments – they often may be inferred from the context of the term, so displaying them just adds unnecessary noise. However, we also need a way to show these subterms for the purposes of debugging or better understanding the term semantics. Arend allows to configure pretty-printer options by the eye button in Arend Messages toolwindow.

This approach has a flaw: it is done in an all-or-nothing way. You are offered to display every omitted subterm of a certain kind, or not display them at all. Therefore, after changing an option of the pretty printer you become lost in the term.

Arend 1.8.0 offers a solution: we introduce printing customization right in the displayed term. You can put a cursor to a source of omittable subterms and then the appeared popup will help you to uncover what was hidden. Currently it works only for implicit arguments and types of parameters in lambda expression.

Live templates

Live templates are smart code snippets. They speed up editing by providing a completion for common code patterns. This release includes such templates for the majority of Arend keywords:

In addition, you can define your own templates in “Preferences | Editor | Live Templates | Arend”:

Optimize imports

Keeping imports clean is easier with this release. The IDE detects unused imports and highlights them in grey color. To remove such imports use the new “Code | Optimize Imports” action:

Aside from just removing, this action can optimize the imports in various ways, for example, import all declarations from a module explicitly. See “Preferences | Editor | Code Style | Arend” for the options.

Extract expression to \let binding

If you have a complex expression and want to extract some of its parts into \let bindings, the new “Create \let-binding” intention is there to automate the process:

Generate function from a goal with arguments

The “Generate function from a goal” intention is smarter now. When you invoke it on a goal with arguments, the resulting function will get parameters corresponding to those arguments:

• 2022 2
• 2021 2
• 2020 5
• 2019 3

2022

Arend 1.8.0 released

Language updates:

New IntelliJ Arend tutorial

There is a new tutorial on interactive theorem proving with IntelliJ Arend. Check it out to learn about the features of IntelliJ Arend that speed-up theorem...

Back to Top ↑

2021

Arend 1.7.0 released

Language updates:

Arend 1.6.0 released

Language updates: Built-in finite types \default implementations \coerce to function types \coerce for fields and constructors \have declaration ...

Back to Top ↑

2020

Arend 1.5.0 released

Language updates: String literals, which can be used in meta code Meta resolvers, which can be used to modify the scoping rules for meta definitions \...

Arend 1.4.0 released

Language updates: Implicit lambdas. Tests directory can be used to store files with tests, examples, and other code which is not a part of the library. ...

Tutorial Part II

The second part of our tutorial is ready.

Arend 1.3.0 released

We implemented language extensions. This can be used to implement custom operations on the abstract syntax tree which are not supported by the language. They...

The first part of our tutorial is ready

We finished the first part of our new tutorial. It covers all the basic constructions of Arend. It does not mention anything related to homotopy theory. This...

Back to Top ↑

2019

Arend 1.2.0 released

We implemented a few features related to classes and pattern matching. One of these features is pattern matching on idp : a = a, which can be used instead of...

Arend 1.1.0 released

Arend now has proof irrelevant universe of proposition and the plugin can run the typechecker automatically in background.

Arend 1.0.0 released

The first version of Arend is released!

Back to Top ↑