# Zulip Chat Archive

## Stream: new members

### Topic: Detecting case inside pattern match

#### Oskar Berndal (Dec 29 2020 at 13:56):

Hi! I'm trying to define syntax trees and prove some properties about them. I tried to illustrate my problem with a smaller example but it is still some lines, sorry about that. My problem is in the last definition.

```
structure ops :=
(symbol: Type)
(arity: symbol → ℕ)
inductive tree (o: ops)
| var: tree
| sym (s: o.symbol)(sub: fin (o.arity s) → tree): tree
inductive exops
| mul_red: exops
| mul_blu: exops
| neg_blu: exops
open exops
def arity : exops → ℕ
| mul_red := 2
| mul_blu := 2
| neg_blu := 1
def exopstree : Type := tree (ops.mk exops arity)
def red_head (t: exopstree) : Prop :=
match t with
| tree.var := true
| tree.sym s _ :=
match s with
| mul_red := true
| mul_blu := false
| neg_blu := false
end
end
def blu_head (t: exopstree) : Prop :=
match t with
| tree.var := true
| tree.sym s _ :=
match s with
| mul_blu := true
| neg_blu := true
| mul_red := false
end
end
def is_wellformed (t: exopstree) : Prop :=
begin
induction t with s sub is_wf_H,
{ exact true },
{ exact (∀ a: fin (arity s), is_wf_H a) ∧
match s with
| mul_blu := red_head(sub 0) ∧ red_head(sub 1)
| mul_red := blu_head(sub 0) ∧ blu_head(sub 1)
| neg_blu := red_head(sub 0)
end
}
end
```

As you can see, I am trying to define what it means for a tree/expression to be well formed. I want to require, in addition that its arguments are well formed, certain things of certain arguments of the expression. For sake of illustration, I want to require that the blue symbols ought to take red arguments and vice versa. Where I run into trouble is inside the very last match expression.

Lean does not seem to realize that inside the first clause, `s`

actually is `mul_blu`

, so it doesn't seem to compute `arity s`

to 2 and it doesn't realize that `0`

is a valid argument to `sub`

, which (essentially) has type `fin (arity s) → exopstree`

.

Does anyone know how to solve this? Many thanks!

#### Shing Tak Lam (Dec 29 2020 at 14:16):

Lean is complaining because `fin 0`

is empty, and doesn't have `0`

. In this specific case, you're trying to pattern match for `0 : fin (arity s)`

, and Lean does not know that `arity s`

is not `0`

.

#### Oskar Berndal (Dec 29 2020 at 14:21):

Yes. But I am inside the clause where `s`

has matched as `mul_blu`

, therefore `arity s`

ought to compute to `2`

, in my humble opinion. Can I get Lean to recognize that `arity s`

is `arity mul_blue`

? Only inside the clause, of course.

A suggestion for another approach is also welcome.

#### Shing Tak Lam (Dec 29 2020 at 14:38):

I think this is what you want?

```
structure ops :=
(symbol: Type)
(arity: symbol → ℕ)
inductive tree (o: ops)
| var: tree
| sym (s: o.symbol)(sub: fin (o.arity s) → tree): tree
inductive exops
| mul_red: exops
| mul_blu: exops
| neg_blu: exops
open exops
@[reducible] def arity : exops → ℕ
| mul_red := 2
| mul_blu := 2
| neg_blu := 1
def exopstree : Type := tree (ops.mk exops arity)
def red_head (t: exopstree) : Prop :=
match t with
| tree.var := true
| tree.sym s _ :=
match s with
| mul_red := true
| mul_blu := false
| neg_blu := false
end
end
def blu_head (t: exopstree) : Prop :=
match t with
| tree.var := true
| tree.sym s _ :=
match s with
| mul_blu := true
| neg_blu := true
| mul_red := false
end
end
def is_wellformed : exopstree → Prop
| tree.var := true
| (tree.sym mul_blu sub) := red_head (sub 0) ∧ red_head (sub 1)
| (tree.sym mul_red sub) := blu_head (sub 0) ∧ blu_head (sub 1)
| (tree.sym neg_blu sub) := red_head (sub 0)
```

Changes - I marked `arity`

as `reducible`

and I used pattern matching and not `induction`

for the definition of `is_wellformed`

#### Yakov Pechersky (Dec 29 2020 at 14:41):

Would these non-equation compiler Prop defns also work?

```
def red_head (t : exopstree) : Prop :=
t = tree.var ∨ ∃ x, t = tree.sym exops.mul_red x
def blu_head (t : exopstree) : Prop :=
t = tree.var ∨ (∃ x, t = tree.sym exops.mul_blu x) ∨ (∃ x, t = tree.sym exops.neg_blu x)
```

#### Oskar Berndal (Dec 29 2020 at 14:45):

Shing Tak Lam said:

I think this is what you want?

`structure ops := (symbol: Type) (arity: symbol → ℕ) inductive tree (o: ops) | var: tree | sym (s: o.symbol)(sub: fin (o.arity s) → tree): tree inductive exops | mul_red: exops | mul_blu: exops | neg_blu: exops open exops @[reducible] def arity : exops → ℕ | mul_red := 2 | mul_blu := 2 | neg_blu := 1 def exopstree : Type := tree (ops.mk exops arity) def red_head (t: exopstree) : Prop := match t with | tree.var := true | tree.sym s _ := match s with | mul_red := true | mul_blu := false | neg_blu := false end end def blu_head (t: exopstree) : Prop := match t with | tree.var := true | tree.sym s _ := match s with | mul_blu := true | neg_blu := true | mul_red := false end end def is_wellformed : exopstree → Prop | tree.var := true | (tree.sym mul_blu sub) := red_head (sub 0) ∧ red_head (sub 1) | (tree.sym mul_red sub) := blu_head (sub 0) ∧ blu_head (sub 1) | (tree.sym neg_blu sub) := red_head (sub 0)`

Changes - I marked

`arity`

as`reducible`

and I used pattern matching and not`induction`

for the definition of`is_wellformed`

Oh, interesting! What does `reducible`

do? Or perhaps a better question is, where can I learn about how such glyphs work, without having to bug anyone about it?

I also want the sub expressions to be well formed. I will give it a spin and come back, thank you for the suggestion!! ^_^

#### Shing Tak Lam (Dec 29 2020 at 14:49):

Yakov Pechersky said:

Would these non-equation compiler Prop defns also work?

`def red_head (t : exopstree) : Prop := t = tree.var ∨ ∃ x, t = tree.sym exops.mul_red x def blu_head (t : exopstree) : Prop := t = tree.var ∨ (∃ x, t = tree.sym exops.mul_blu x) ∨ (∃ x, t = tree.sym exops.neg_blu x)`

I don't think that's as nice to use? Since every time you want to prove something you'll need to provide the value for the `exists`

. Although using the equation compiler some golfing is possible:

```
def red_head : exopstree → Prop
| tree.var := true
| (tree.sym mul_red _) := true
| (tree.sym _ _) := false
def blu_head : exopstree → Prop
| tree.var := true
| (tree.sym mul_red _) := false
| (tree.sym _ _) := true
```

#### Oskar Berndal (Dec 29 2020 at 16:08):

Ah bugger I wasn't able to refactor my working code so that that approach worked, it seems that I inject too many 'intermediary abstractions'. Thanks anyways.

#### Oskar Berndal (Dec 30 2020 at 20:44):

Thanks to your help @Shing Tak Lam , I was able to solve my problem, following your suggestion of just flat pattern matching. I also had to use the change tactic, approximately `change [fin (actual arity of sub) → tree] at [sub]`

. It sure would be a neat thing if I could do that inside a match expression as well but I couldn't get it to work. At least I have a path forward now!!! =)

#### Shing Tak Lam (Dec 31 2020 at 07:26):

Oskar Berndal said:

Thanks to your help Shing Tak Lam , I was able to solve my problem, following your suggestion of just flat pattern matching. I also had to use the change tactic, approximately

`change [fin (actual arity of sub) → tree] at [sub]`

. It sure would be a neat thing if I could do that inside a match expression as well but I couldn't get it to work. At least I have a path forward now!!! =)

You might be able to get rid of the `change`

by adding some casts and/or type annotations, but I'm not sure without having seen your code.

Last updated: May 09 2021 at 19:11 UTC