# Zulip Chat Archive

## Stream: Lean Together 2019

### Topic: small scale reflection

#### Kevin Buzzard (Jan 10 2019 at 08:47):

Assia is talking about small scale reflection.

The following is reflection. Imagine we have `variable A : Type`

and `variable add : A -> A -> A`

and a hypothesis that `A`

is associative. Then given some term of type `A`

, of the form `(a + (b + c)) + d`

or whatever, one could ask for a method of moving all the parentheses to the left (with perhaps an added theorem that the original term equals the "normalised" term). But you cannot write Lean code to do this! Lean interprets `(a + (b + c)) + d`

as just some term of type `A`

.

To write code which moves brackets around, one has to make a new data structure, in this case a tree type with nodes and leaves (leaves indexed by `nat`

say), and a "put into normal form" function `norm`

which sends `node (t1 (node t2 t3))`

to `node (node t1 t2) t3`

and generally sends a tree to its "normal form" with all the brackets on the left. "Reification" is the small amount of meta code which one has to write which looks at the actual expression corresponding to a term of type `A`

and turns it into a tree. One also has an `eval`

evaluation function sending a tree plus some "association list" (saying which elements of `A`

the leaves correspond to) to `A`

. One then proves a "correctness theorem" that says that given a tree and a list of `A`

's, the evaluation of `t`

and its normalisation are equal.

"Reflection" (or "the two level approach" as Henk used to call it) is exactly this situation, where terms of type A constructed using only `+`

, and terms of this abstract tree structure, reflect each other.

#### Kevin Buzzard (Jan 10 2019 at 09:03):

A really cool reflection would be between `Prop`

and `bool`

! `bool`

is a nice easy type and we can calculate with it. There's a nice function from `bool`

to `Prop`

sending `b`

to `b = tt`

(which is an equation, which is great because it means we can rewrite). Unfortunately, writing meta code which interprets an arbitrary `Prop`

as a `bool`

is asking a bit much.

#### Simon Hudon (Jan 10 2019 at 09:15):

We actually have a conversion from Prop to bool for decidable Props

Last updated: May 08 2021 at 22:13 UTC