# Zulip Chat Archive

## Stream: new members

### Topic: Pattern matching with dependent types

#### Benedikt Ahrens (Sep 24 2020 at 23:13):

Hi,

I would like to write a small interpreter, as in

```
inductive τ : Type
| nn : τ
| bb : τ
open τ
inductive Exp : τ → Type
| Ei : nat → Exp nn
| Eb : bool → Exp bb
| Eplus : Exp nn → Exp nn → Exp nn
| Eand : Exp bb → Exp bb → Exp bb
| Eequal {a : τ} : Exp a → Exp a → Exp a
def τeval : τ → Type
| nn := nat
| bb := bool
def Eeval {α : τ} : Exp α → τeval α
| (Ei n) := n
| (Eb b) := b
| (Eplus a b) := (Eeval a) + (Eeval b)
| (Eand a b) := (Eeval a) ∧ (Eeval b)
| (Eequal a b) := eqdec (Eeval a) (Eequal b)
```

However, I do not know how to write the patterns in the function `Eeval`

: how do I handle the argument `α`

?

Also, in the last pattern I will need a boolean equality test for nat and bool. Is there a way to search the library, e.g., `#search nat -> nat -> bool`

? to find functions of that type?

#### Scott Morrison (Sep 25 2020 at 00:03):

@Benedikt Ahrens

```
inductive τ : Type
| nn : τ
| bb : τ
open τ
inductive Exp : τ → Type
| Ei : nat → Exp nn
| Eb : bool → Exp bb
| Eplus : Exp nn → Exp nn → Exp nn
| Eand : Exp bb → Exp bb → Exp bb
| Eequal {a : τ} : Exp a → Exp a → Exp bb
def τeval : τ → Type
| nn := nat
| bb := bool
instance (α : τ) : decidable_eq (τeval α) :=
by { cases α; apply_instance, }
open Exp
def Eeval : Π {α : τ}, Exp α → τeval α
| nn (Ei n) := n
| bb (Eb b) := b
| nn (Eplus a b) := ((Eeval a) + (Eeval b) : nat)
| bb (Eand a b) := band (Eeval a) (Eeval b)
| _ (Eequal a b) := ((Eeval a) = (Eeval b) : bool)
```

#### Scott Morrison (Sep 25 2020 at 00:04):

(Notice this required changing `Eequal b`

to `Eeval b`

in the last line, and `| Eequal {a : τ} : Exp a → Exp a → Exp a`

to `| Eequal {a : τ} : Exp a → Exp a → Exp bb`

.)

#### Scott Morrison (Sep 25 2020 at 00:05):

You may not like the approach I used here of using normal `Prop`

-valued equality, and then a `decidable_eq`

instance to allow casting to `bool`

, but it is the idiomatic Lean way. :-)

#### Scott Morrison (Sep 25 2020 at 00:06):

Regarding searching, there are tactics `library_search`

and `suggest`

, which try to solve the current goal using a single lemma from the library and available hypotheses. They won't help much with `nat -> nat -> bool`

. There is `#find`

, but it is unfortunately not very good. (Perhaps could become better with some love, however!)

#### Scott Morrison (Sep 25 2020 at 00:08):

Notice that in the line `| nn (Eplus a b) := ((Eeval a) + (Eeval b) : nat)`

I had to help Lean along by adding a type ascription --- typeclass resolution is done at a syntactic level, so it's not cleverer enough to "see through" `τeval nn`

and realise you are trying at add natural numbers.

#### Scott Morrison (Sep 25 2020 at 00:09):

Another approach would be to add a `has_add`

instance (or more likely, `semiring`

) for `τeval nn`

(just by unfolding the definition and then using `apply_instance`

to pick up the instance for `nat`

).

#### Benedikt Ahrens (Sep 26 2020 at 10:18):

@Scott Morrison : Thanks a lot for all the information. Yes, I had some typos in my example, thanks for spotting them. Your explanations have helped me a lot in understanding Lean. I will play around a bit with the different approaches you are suggesting.

Last updated: May 13 2021 at 18:26 UTC