sadol

ReProving Agda in Lean

This project translates the paper (Symbolic and Automatic Differentiation of Languages - Conal Elliott) from Agda to LeanProver.

The goals of this project are to:

Discover the differences between Agda and Lean4.
Define proofs on Type instead of Prop, since each proof represents a different parse of the language.
Avoid tactics if possible, in favour of simple trfl (our version of rfl).

Requirements

This project requires setting up lean, see the official documentation.

Trivial differences from the Agda implementation

Lean has Prop and Type and Agda has Set, which we can think of as Type in Lean. We want out proofs to be proof revelant, since each proof represents a different parse of our language. This means the theorems have to be defined on Type. For example we have equality redefined in terms of Type as TEq (using the syntax ≡) and we replace rfl with trfl, but we do not a replacement tactic for rfl.

inductive TEq.{tu} {α: Type tu} (a b: α) : Type tu where
  | mk : a = b -> TEq a b

def trfl {α : Type u} {a : α} : TEq a a := TEq.mk rfl

We needed to redefine the following types and functions to use Type instead of Prop:

Description	Prop	Type
equality	`=`	`≡` in Tipe.lean
equivalance	`Mathlib.Logic.Equiv.Defs.Equiv`	`TEquiv` or `<=>` in Function.lean
decidability	`Decidable`	`Decidability.Dec` in Decidability.lean

When write proofs, we cannot rewrite using the rw tactic, but we need to destruct equalities, to do rewrites for us:

cases H with
| refl =>

Simply renamings

Some things we renamed since they are simply called different things in Agda and Lean, while others were renamed to be closer to the Lean convention.

Description	Original Agda	Translated Lean
	`Set`	`Type`
universe levels	`ℓ`, `b`	`u`, `v`
parametric types	`A`, `B`	`α`, `β`
isomorphism	`↔`	`<=>`
extensional isomorphism	`⟷`	`∀ {w: List α}, (P w) <=> (Q w)`

Namespaces / Qualified Imports

We use namespaces as much as possible to make dependencies clear to the reader without requiring "Go to Definition" and Lean to be installed.

Description	Original Agda	Translated Lean
`List α -> Type u`	`◇.Lang`	`Language.Lang`
`List α -> β`	`◇.ν`	`Calculus.null`
`(List α -> β) -> (a: α) -> (List α -> β)`	`◇.δ`	`Calculus.derive`
	`Dec`	`Decidability.Dec`
	`Decidable`	`Decidability.DecPred`

Syntax

We dropped most of the syntax, in favour of ([a-z]|[A-Z]|'|_|\.)* names.

Description	Original Agda	Translated Lean
nullable	`ν`	`null`
derivative of a string	`𝒟`	`derives`
derivative of a character	`δ`	`derive`
	`∅`	`emptyset`
	`𝒰`	`universal`
empty string	`𝟏`	`emptystr`
character	` c	`char c`
	`∪`	`or`
	`∩`	`and`
scalar	`s · P`	`scalar s P`
	`P ⋆ Q`	`concat P Q`
zero or more	`P ☆`	`star P`
decidable bottom	`⊥?`	`Decidability.empty`
decidable top	`⊤‽`	`Decidability.unit`
decidable sum	`_⊎‽_`	`Decidability.sum`
decidable prod	`_×‽_`	`Decidability.prod`
`Dec α -> Dec (List α)`	`_✶‽`	`Decidability.list`
`(β <=> α) -> Dec α -> Dec β`	`◃`	`Decidability.apply'`
decidable equality	`_≟_`	`Decidability.decEq`
decidable denotation	`⟦_⟧‽`	`decDenote`
denotation	`⟦_⟧`	`denote`

All language operators defined in Language.lagda are referenced in other modules as ◇.∅, while in Lean they are references as qualified and non notational names Language.emptyset. The exception is Calculus.lean, where Language.lean is opened, so they are not qualified.

Explicit parameters.

We use explicit parameters and almost no module level parameters, for example Lang in Agda is defined as Lang α in Lean. In Agda the A parameter for Lang is lifted to the module level, but in this translation we make it explicit.

Reordering of definitions

In Lean definitions need to be in the order they are used. So for example, in Automatic.lean iso needs to be defined before concat, since concat uses iso, but in Automatic.lagda, this can be defined in any order.

Also each function signature and its implementatio is grouped together in Lean, while in the Agda implementation the function type signatures are grouped together and the implementations of those functions are much lower down in the file.

Non-Trivial differences from the Agda implementation

Coinduction / Termination Checking

Lean does not have coinduction, which seems to be required for defining Automatic.Lang. We attempt an inductive defintion:

inductive Lang {α: Type u} : Language.Lang α -> Type (u+1) where
  | mk
    (null: Decidability.Dec (Calculus.null R))
    (derive: (a: α) -> Lang (Calculus.derive R a))
    : Lang R

But this results in a lot of termination checking issues, when instantiating operators in Automatic.lean.

For example, when we instantiate emptyset:

-- ∅ : Lang ◇.∅
def emptyset {α: Type u}: Lang (@Language.emptyset.{u} α) := Lang.mk
  -- ν ∅ = ⊥‽
  (null := Decidability.empty)
  -- δ ∅ a = ∅
  (derive := fun _ => emptyset)

We get the following error:

fail to show termination for
  Automatic.emptyset
with errors
failed to infer structural recursion:
Not considering parameter α of Automatic.emptyset:
  it is unchanged in the recursive calls
no parameters suitable for structural recursion

well-founded recursion cannot be used, 'Automatic.emptyset' does not take any (non-fixed) arguments

This seems to be a fundamental issue in regards to how inductive types work. We can get around this issue by using unsafe:

-- ∅ : Lang ◇.∅
unsafe -- failed to infer structural recursion
def emptyset {α: Type u}: Lang (@Language.emptyset.{u} α) := Lang.mk
  -- ν ∅ = ⊥‽
  (null := Decidability.empty)
  -- δ ∅ a = ∅
  (derive := fun _ => emptyset)

This issue was probably inevitable, given that the Agda version of Lang in Automatic.lagda required coinduction, which is not a feature of Lean:

record Lang (P : ◇.Lang) : Set (suc ℓ) where
  coinductive
  field
    ν : Dec (◇.ν P)
    δ : (a : A) → Lang (◇.δ P a)

Note, the Agda representation also encountered issues with Agda's termination checker, but only when defining the derivative of the concat operator, not all operators as in Lean. Also this was fixable in Agda using a sized version of the record:

record Lang i (P : ◇.Lang) : Set (suc ℓ) where
  coinductive
  field
    ν : Dec (◇.ν P)
    δ : ∀ {j : Size< i} → (a : A) → Lang j (◇.δ P a)

We hope to find help to remove the use of unsafe in Lean or that it is possible to fix using a future coinductive feature.

Apparently there are libraries in Lean that support coinduction, but none that support indexed coinductive types, which is what we require in this case.

Also note, sized types in Agda are fundamentally flawed, so whether Agda can represent Automatic.Lang without fault, is also an open question.

Thank you

Thank you to the Conal Elliot for the idea of comparing LeanProver to Agda using the paper Symbolic and Automatic Differentiation of Languages - Conal Elliott. If you are interested in collaborating with Conal Elliott, see this Collaboration page.

Thank you to the Authors and Advisors:

And thank you to everyone on leanprover zulip chat:

Where I asked many questions about:

Reservoir