Pattern matching with dependent types

Stream: new members

[Benedikt Ahrens]

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]

@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]

(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]

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]

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]

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]

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]

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