Detecting case inside pattern match

Stream: new members

[Oskar Berndal]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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.