Zulip Chat Archive

Stream: new members

Topic: Detecting case inside pattern match


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

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

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

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

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

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

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

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

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

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