Attribute Domains

Stream: Is there code for X?

[Paul Rowe]

I'm having trouble figuring out how to go about formalizing a concept called "attribute domains". The basic idea is that you have some inductive type α. This type has some list of constructors of various arities. We want to define a function f : α → vals into some (typically ordered) type of values. This function f should "match up" the constructors of α with some other list of operators on vals, where the value of f is recursively defined according to the inductive structure of the elements of α.

So far, there's no problem. If I know α and I have a list of operators in mind, I can just write the recursive function. But I'm looking for a general way of telling Lean how to build the recursive function based on, say, the type α and the list of operators to use for the respective cases.

Here's an example based on the specific structures I'm looking to support.

inductive attack_tree (lab : Type)
| atom : lab → attack_tree
| or : attack_tree → attack_tree → attack_tree
| and : attack_tree → attack_tree → attack_tree
| seq : attack_tree → attack_tree → attack_tree
open attack_tree

inductive place
| pl : string → place

inductive program
| pr : string → program

inductive component : Type
| c : place → program → component

inductive asp
| msp : component → component → asp
| nul : asp
| cpy : asp
| hsh : asp
| sig : asp

inductive dir
| pos : dir
| neg : dir

inductive split
| mk : dir → dir → split

inductive copland
| atom : asp → copland
| lseq : copland → copland → copland
| bseq : split → copland → copland → copland
| bpar : split → copland → copland → copland
| att : place → copland → copland
open copland

variable {lab : Type}

def AD1 (V : attack_tree lab → ℕ) : attack_tree lab → ℕ
| (atom a) := V (atom a)
| (or t1 t2) := min (AD1 t1) (AD1 t2)
| (and t1 t2) := AD1 t1 + AD1 t2
| (seq t1 t2) := max (AD1 t1) (AD1 t2)

def AD2 (V : copland → ℕ) : copland → ℕ
| (atom a) := V (atom a)
| (bpar s c1 c2) := AD2 c1 + AD2 c2
| (lseq c1 c2) := max (AD2 c1) (AD2 c2)
| (bseq s c1 c2) := max (AD2 c1) (AD2 c2)
| (att q c1) := AD2 c1

-- Input types are clearly wrong. How to package the necessary info?
def AD_general (α : Type) (vals : Type) (ops : list Type) :
 α → vals := sorry

I'd like the general construction to prove things like, "as long as attack_tree.and gets associated with the same operator as copland.bpar and attack_tree.seq gets associated with the same operator as copland.lseq and copland.bseq, then a property holds about the AD1 version iff it holds about the AD2 version".

[Matt Diamond]

I wonder if docs#W_type might be relevant here, as it represents inductively defined trees

[Paul Rowe]

Thanks. I’ll check into that lead when I get a chance. I really appreciate the suggestion!

[Paul Rowe]

While I have a feeling using W_types would be helpful, I decided to go with a more modest solution. Since I have two particular inductive types in mind, I can at least parameterize each of those with a list (vector, really) of functions. Since I know the number of constructors and their arities, I can hard code those into the lists. Just for reference in case it helps anybody, a revised version is below that shows the equality of the new approach with the one-off solutions.

import data.vector tactic

inductive attack_tree (lab : Type)
| atom : lab → attack_tree
| or : attack_tree → attack_tree → attack_tree
| and : attack_tree → attack_tree → attack_tree
| seq : attack_tree → attack_tree → attack_tree
open attack_tree

inductive place
| pl : string → place

inductive program
| pr : string → program

inductive component : Type
| c : place → program → component

inductive asp
| msp : component → component → asp
| nul : asp
| cpy : asp
| hsh : asp
| sig : asp

inductive dir
| pos : dir
| neg : dir

inductive split
| mk : dir → dir → split

inductive copland
| atom : asp → copland
| lseq : copland → copland → copland
| bseq : split → copland → copland → copland
| bpar : split → copland → copland → copland
| att : place → copland → copland
open copland

variable {lab : Type}

def AD1 (V : attack_tree lab → ℕ) : attack_tree lab → ℕ
| (atom a) := V (atom a)
| (or t1 t2) := min (AD1 t1) (AD1 t2)
| (and t1 t2) := AD1 t1 + AD1 t2
| (seq t1 t2) := max (AD1 t1) (AD1 t2)


-- An alternative that takes a list of functions as an argument.
def AD1' (V : attack_tree lab → ℕ) (l2 : vector (ℕ → ℕ → ℕ) 3): attack_tree lab → ℕ
| (atom a) := V (atom a)
| (or t1 t2) := (vector.nth l2 0) (AD1' t1) (AD1' t2)
| (and t1 t2) := (vector.nth l2 1) (AD1' t1) (AD1' t2)
| (seq t1 t2) := (vector.nth l2 2) (AD1' t1) (AD1' t2)

def ad1ops : vector (ℕ → ℕ → ℕ) 3 :=
⟨[(λ a b, min a b), (λ a b, a + b), (λ a b, max a b)], by simp⟩

lemma AD1_eq (V : attack_tree lab → ℕ) (t : attack_tree lab) :
AD1 V t = AD1' V ad1ops t :=
begin
  induction t,
  case attack_tree.atom : t
  { simp [AD1, AD1'], },
  case attack_tree.or : t1 t2 IH1 IH2
  { simp [AD1, AD1'],
    rw [IH1, IH2], refl, },
  case attack_tree.and : t1 t2 IH1 IH2
  { simp [AD1, AD1'],
    rw [IH1, IH2], refl, },
  case attack_tree.seq : t1 t2 IH1 IH2
  { simp [AD1, AD1'],
    rw [IH1, IH2], refl, }
end

def AD2 (V : copland → ℕ) : copland → ℕ
| (atom a) := V (atom a)
| (bpar s c1 c2) := AD2 c1 + AD2 c2
| (lseq c1 c2) := max (AD2 c1) (AD2 c2)
| (bseq s c1 c2) := max (AD2 c1) (AD2 c2)
| (att q c1) := AD2 c1

def AD2' (V : copland → ℕ) (l1 : ℕ → ℕ) (l2 : vector (ℕ → ℕ → ℕ) 2) : copland → ℕ
| (atom a) := V (atom a)
| (bpar s c1 c2) := (vector.nth l2 0) (AD2' c1) (AD2' c2)
| (lseq c1 c2) := (vector.nth l2 1) (AD2' c1) (AD2' c2)
| (bseq s c1 c2) := (vector.nth l2 1) (AD2' c1) (AD2' c2)
| (att q c1) := l1 (AD2' c1)

def ad2ops : vector (ℕ → ℕ → ℕ) 2 :=
⟨[λ a b, a + b, λ a b, max a b], by simp⟩

lemma AD2_eq (V : copland → ℕ) (c : copland) :
AD2 V c = AD2' V id ad2ops c :=
begin
  induction c,
  case copland.atom : c
  { simp [AD2, AD2'], },
  case copland.lseq : c1 c2 IH1 IH2
  { simp [AD2, AD2', IH1, IH2], refl, },
  case copland.bseq : s c1 c2 IH1 IH2
  { simp [AD2, AD2', IH1, IH2], refl, },
  case copland.bpar : s c1 c2 IH1 IH2
  { simp [AD2, AD2', IH1, IH2], refl, },
  case copland.att : q c1 IH
  { simp [AD2, AD2', IH], },
end