Skip to content

keeganperry7/symbolic-automatic-derivatives

BranchesTags
 
 

Repository files navigation

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).

Links

Requirements

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

Trivial differences from the Agda implementation

Equality ≡

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

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

Proofs of Contradiction

Agda seems to be better at using type inference to infer bottom, while Lean typically prefers the use of a tactic.

For example, proving the derivative of the empty string is the empty set, requires proving a few cases of bottom (⊥ in Agda and PEmpty in Lean). In Agda these proofs are completed with type inference:

δ𝟏  : δ 𝟏 a ⟷ ∅
δ𝟏 = mk↔′ (λ ()) (λ ()) (λ ()) (λ ())

In Lean we need to use the contradiction tactic or the proof becomes very long.

def derive_emptystr {α: Type u} {a: α} {w: List α}:
  (derive emptystr a) w <=> emptyset w := by
  apply TEquiv.mk <;> (intro x; cases x) <;> contradiction

For non Lean users: <;> is similar to the Monad bind operator (>>=) over proof goals. It takes a list of goals to prove and applies the following tactics to each of the goals, which each produce another list of goals, which are all joined together into one list.

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:

About

Symbolic and Automatic Differentiation of Languages in Lean

Resources

Readme

License

Apache-2.0 license
Activity

Stars

0 stars

Watchers

0 watching

Forks

0 forks
Report repository

Releases

No releases published

Packages

No packages published

Languages

  • Lean 100.0%