## 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

- The original paper: Symbolic and Automatic Differentiation of Languages - Conal Elliott
- If you are new to derivatives, here is an introduction to Brzozowski's derivatives
- Want to read the Agda code with the ability to "Go to Definition", but you do not want to install Agda. Then download the zip file in this gist: Generated HTML from the original Agda code.
- We streamed the development the foundations of this repo. You can find the recordings of your struggles on this Youtube Playlist.

### 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 |

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:

- Adam Topaz
- Alex Keizer
- Andrew Carter
- Andrés Goens
- Arthur Adjedj
- Daniel Weber
- Damiano Testa
- David Thrane Christiansen
- Edward van de Meent
- Eric Wieser
- Eric Rodriguez
- François G. Dorais
- Kim Morrison
- Kyle Miller
- Mario Carneiro
- Jannis Limperg
- Junyan Xu
- Sebastian Ullrich
- Shreyas Srinivas
- Siegmentation Fault
- Yuri de Wit

Where I asked many questions about: