Zulip Chat Archive

Stream: new members

Topic: Pattern matching with dependent types


view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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.)

view this post on Zulip 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. :-)

view this post on Zulip 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!)

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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