rename some variables to n and l for lengths

Author: awalterschulze

Nomenclature.md

@@ -15,12 +15,13 @@
 * ih, ih.* (inductive hypothesis)
 * iff, Iff (if and only if)
 * l, l[0-9]* (length variable name)
+* l (length of a Vector)
 * le (less than or equal)
 * lt (less than)
 * m (monad type variable)
 * n (natural numbers of finite number variable names)
+* n (natural number representing the number of non-terminals or production rules)
 * ℕ (natural number type)
-* μ (a number used in as a type parameter, for example Fin μ)
 * ν (nullable function name)
 * Φ, Ψ (generic predicate type parameter, Phi/Psi)
 * r (regular expression variable names) (TODO: need two more? s is symbol, p and q are for predicates)

Validator/Derive/Enter.lean

@@ -7,16 +7,16 @@ import Validator.Expr.Symbol
 
 namespace Enter
 
-def deriveEnter (xs: Rules μ α Pred ν): IfExprs μ α (Symbol.nums xs) :=
+def deriveEnter (xs: Rules n α Pred l): IfExprs n α (Symbol.nums xs) :=
   List.Vector.map
     (fun (pred, ref) => IfExpr.mk pred ref)
     (Symbol.Symbols.cast
       (Symbol.extracts xs List.Vector.nil).2
       (by ac_rfl)
     )
 
-class DeriveEnter (m: Type -> Type u) (μ: Nat) (α: outParam Type) where
-  deriveEnter {ν: Nat} (xs: Rules μ α Pred ν): m (IfExprs μ α (Symbol.nums xs))
+class DeriveEnter (m: Type -> Type u) (n: Nat) (α: outParam Type) where
+  deriveEnter {l: Nat} (xs: Rules n α Pred l): m (IfExprs n α (Symbol.nums xs))
 
-def deriveEnter_list (xs: List (Rule μ α Pred)): List (IfExpr μ α) :=
+def deriveEnter_list (xs: List (Rule n α Pred)): List (IfExpr n α) :=
   List.map (fun (pred, ref) => IfExpr.mk pred ref) (Symbol.extracts_list xs []).2

Validator/Derive/Leave.lean

@@ -5,7 +5,7 @@ import Validator.Derive.Enter
 
 namespace Leave
 
-def leave (x: Regex (Fin ν)) (es: Symbol.Symbols (Pred α × Ref μ) ν) (ns: List.Vector Bool ν): (Rule μ α Pred) :=
+def leave (x: Regex (Fin l)) (es: Symbol.Symbols (Pred α × Ref n) l) (ns: List.Vector Bool l): (Rule n α Pred) :=
   match x with
   | Regex.emptyset => Regex.emptyset
   | Regex.emptystr => Regex.emptyset
@@ -28,10 +28,10 @@ def leave (x: Regex (Fin ν)) (es: Symbol.Symbols (Pred α × Ref μ) ν) (ns: L
 -- The vectors of bools represent the nullability of the derived child expressions.
 -- Each bool will then replace each symbol expression with either an emptystr or emptyset.
 def deriveLeave
-  (xs: List.Vector (Regex (Fin ν)) μ1)
-  (es: Symbol.Symbols (Pred α × Ref μ) ν)
-  (ns: List.Vector Bool ν)
-  : (Rules μ α Pred μ1) :=
+  (xs: List.Vector (Regex (Fin l1)) l2)
+  (es: Symbol.Symbols (Pred α × Ref n) l1)
+  (ns: List.Vector Bool l1)
+  : (Rules n α Pred l2) :=
   match xs with
   | ⟨[], h⟩ => ⟨[], h⟩
   | ⟨x::xs, h⟩ =>
@@ -46,14 +46,14 @@ def deriveLeave
       )
 
 def deriveLeaves
-  (xs: Rules μ α Pred ν)
+  (xs: Rules n α Pred l)
   (ns: List.Vector Bool (Symbol.nums xs))
-  : (Rules μ α Pred ν) :=
+  : (Rules n α Pred l) :=
   let (regexes, symbols) := Symbol.extracts xs List.Vector.nil
   deriveLeave regexes symbols (Symbol.Symbols.cast ns (by simp only [zero_add]))
 
-def deriveLeaveM [Monad m] {μ: Nat} {ν: Nat} (xs: Rules μ α Pred ν) (ns: List.Vector Bool (Symbol.nums xs)): m (Rules μ α Pred ν) := do
+def deriveLeaveM [Monad m] {n: Nat} {l: Nat} (xs: Rules n α Pred l) (ns: List.Vector Bool (Symbol.nums xs)): m (Rules n α Pred l) := do
   return deriveLeaves xs ns
 
-class DeriveLeaveM (m: Type -> Type u) (μ: Nat) (α: outParam Type) where
-  deriveLeaveM {ν: Nat} (xs: Rules μ α Pred ν) (ns: List.Vector Bool (Symbol.nums xs)): m (Rules μ α Pred ν)
+class DeriveLeaveM (m: Type -> Type u) (n: Nat) (α: outParam Type) where
+  deriveLeaveM {l: Nat} (xs: Rules n α Pred l) (ns: List.Vector Bool (Symbol.nums xs)): m (Rules n α Pred l)

Validator/Expr/BCFG.lean

@@ -5,19 +5,19 @@ import Validator.Expr.Pred
 
 namespace BalancedContextFreeGrammar
 
-abbrev Ref μ := Fin μ
+abbrev Ref n := Fin n
 
 -- Balanced Context Free Grammars have the restriction that each non-terminal cannot represent any regular expression,
 -- but only regular expressions that are surrounded by a start and end terminal.
-structure Rule (μ: Nat) (α: Type) (Φ: (α: Type) -> Type) where
+structure Rule (n: Nat) (α: Type) (Φ: (α: Type) -> Type) where
   enter: Φ α
-  child: Regex (Ref μ)
+  child: Regex (Ref n)
   leave: Φ α
 
-abbrev RegexRule (μ: Nat) (α: Type) (Φ: (α: Type) -> Type) := Regex ((Φ α) ⊕ (Ref μ))
+abbrev RegexRule (n: Nat) (α: Type) (Φ: (α: Type) -> Type) := Regex ((Φ α) ⊕ (Ref n))
 
-def Rule.toRegex {μ: Nat} {α: Type} {Φ: (α: Type) -> Type}
-  (r: Rule μ α Φ): RegexRule μ α Φ :=
+def Rule.toRegex {n: Nat} {α: Type} {Φ: (α: Type) -> Type}
+  (r: Rule n α Φ): RegexRule n α Φ :=
   (Regex.concat
     (Regex.symbol (Sum.inl r.enter))
     (Regex.concat
@@ -26,14 +26,14 @@ def Rule.toRegex {μ: Nat} {α: Type} {Φ: (α: Type) -> Type}
     )
   )
 
-abbrev Rules (μ: Nat) (α: Type) (Φ: (α: Type) -> Type) := { xs: List (Rule μ α Φ) // xs.length > 0 }
+abbrev Rules (n: Nat) (α: Type) (Φ: (α: Type) -> Type) := { xs: List (Rule n α Φ) // xs.length > 0 }
 
-structure BCFG (μ: Nat) (α: Type) (Φ: (α: Type) -> Type) where
-  start: { s: List (Ref μ) // s.length > 0 }
-  prods: Vector (Rules μ α Φ) μ
+structure BCFG (n: Nat) (α: Type) (Φ: (α: Type) -> Type) where
+  start: { s: List (Ref n) // s.length > 0 }
+  prods: Vector (Rules n α Φ) n
 
-def union_rules {μ: Nat} {α: Type} {Φ: (α: Type) -> Type}
-  (xs: Rules μ α Φ): RegexRule μ α Φ :=
+def union_rules {n: Nat} {α: Type} {Φ: (α: Type) -> Type}
+  (xs: Rules n α Φ): RegexRule n α Φ :=
   match xs with
   | Subtype.mk xs hxs =>
   match xs with
@@ -42,8 +42,8 @@ def union_rules {μ: Nat} {α: Type} {Φ: (α: Type) -> Type}
   | (x::xs) => List.foldl Regex.or x.toRegex (List.map Rule.toRegex xs)
 
 def BCFG.getStart
-  {μ: Nat} {α: Type} {Φ: (α: Type) -> Type}
-  (g: BCFG μ α Φ): RegexRule μ α Φ :=
+  {n: Nat} {α: Type} {Φ: (α: Type) -> Type}
+  (g: BCFG n α Φ): RegexRule n α Φ :=
   match g.start with
   | Subtype.mk s hs =>
   match s with
@@ -52,15 +52,15 @@ def BCFG.getStart
     let xs' := (List.map (fun x' => Regex.symbol (Sum.inr x'))) xs
     List.foldl Regex.or (Regex.symbol (Sum.inr x)) xs'
 
-def BCFG.lookup {μ: Nat} {α: Type} {Φ: (α: Type) -> Type}
-  (g: BCFG μ α Φ) (ref: Fin μ): RegexRule μ α Φ :=
+def BCFG.lookup {n: Nat} {α: Type} {Φ: (α: Type) -> Type}
+  (g: BCFG n α Φ) (ref: Fin n): RegexRule n α Φ :=
   union_rules (Vector.get g.prods ref)
 
-def nullable {μ: Nat} {α: Type} {Φ: (α: Type) -> Type} (r: RegexRule μ α Φ): Bool :=
+def nullable {n: Nat} {α: Type} {Φ: (α: Type) -> Type} (r: RegexRule n α Φ): Bool :=
   Regex.nullable r
 
-partial def derive {μ: Nat} {α: Type} [DecidableEq α] [BEq α]
-  (g: BCFG μ α Pred) (r: RegexRule μ α Pred) (a: α): RegexRule μ α Pred :=
+partial def derive {n: Nat} {α: Type} [DecidableEq α] [BEq α]
+  (g: BCFG n α Pred) (r: RegexRule n α Pred) (a: α): RegexRule n α Pred :=
   match r with
   | Regex.emptyset => Regex.emptyset
   | Regex.emptystr => Regex.emptyset

Validator/Expr/Compress.lean

@@ -133,16 +133,16 @@ def vector_cast (h: n = m) (xs: List.Vector α n): List.Vector α m := by
   subst h
   exact xs
 
-def compress [DecidableEq α] (xs: Rules μ α Pred ν): Σ n, ((Rules μ α Pred n) × (Indices n ν)) :=
-  let xs_list: List (Rule μ α Pred) := xs.toList
-  have hn : xs_list.length = ν := by
+def compress [DecidableEq α] (xs: Rules n α Pred l1): Σ l2, ((Rules n α Pred l2) × (Indices l2 l1)) :=
+  let xs_list: List (Rule n α Pred) := xs.toList
+  have hn : xs_list.length = l1 := by
     simp_all only [List.Vector.toList_length, xs_list]
 
   -- sort to increase chance of cache hit
   -- TODO: let sxs := List.mergeSort xs
 
   -- remove duplicates
-  let xs_noreps: { ys: List (Rule μ α Pred) // ∀ x ∈ xs_list, x ∈ ys } := eraseReps_sub xs_list
+  let xs_noreps: { ys: List (Rule n α Pred) // ∀ x ∈ xs_list, x ∈ ys } := eraseReps_sub xs_list
 
   -- get indices
   let xs_idxs: List.Vector (Fin (xs_noreps.val).length) (List.length xs_list) := indices xs_noreps
@@ -152,19 +152,19 @@ def compress [DecidableEq α] (xs: Rules μ α Pred ν): Σ n, ((Rules μ α Pre
 
   -- find all indexes of the original expressions in the compressed expressions
   let indices: Indices (xs_noreps.val).length (List.length xs_list) := List.Vector.map (fun x => Index.val x) xs_idxs
-  let indices': Indices (xs_noreps.val).length ν := vector_cast hn indices
+  let indices': Indices (xs_noreps.val).length l1 := vector_cast hn indices
 
   Sigma.mk (List.length (xs_noreps.val)) (
     Subtype.mk xs_noreps rfl,
     indices'
   )
 
-def memVector (xs: List.Vector α ν) (y: α): Prop :=
+def memVector (xs: List.Vector α l) (y: α): Prop :=
   match xs with
   | ⟨[], _⟩ => False
   | ⟨x::xs, h⟩ => x = y \/ memVector ⟨xs, congrArg Nat.pred h⟩ y
 
-instance [DecidableEq α]: Membership α (List.Vector α ν) where
+instance [DecidableEq α]: Membership α (List.Vector α l) where
   mem := memVector
 
 theorem memVector_nil {n: Nat} {hxs: [].length = n}
@@ -189,7 +189,7 @@ theorem memVector_cons {n: Nat} {hxs: (x::xs).length = n}
     generalize_proofs at h
     exact h
 
-def indexOf' [DecidableEq α] (xs: List.Vector α ν) (y: α) (h: y ∈ xs): Fin (xs.length) :=
+def indexOf' [DecidableEq α] (xs: List.Vector α l) (y: α) (h: y ∈ xs): Fin (xs.length) :=
   match xs with
   | ⟨[], hxs⟩ => by
     exfalso
@@ -223,27 +223,27 @@ theorem memVector_emptyset [DecidableEq α] {y: Regex α}
     simp only [beq_iff_eq] at h2
     contradiction
 
-def indexOf [DecidableEq α] (xs: List.Vector (Regex α) ν) (y: Regex α) (h: y ∈ xs \/ y = Regex.emptyset): Index (xs.length) :=
+def indexOf [DecidableEq α] (xs: List.Vector (Regex α) l) (y: Regex α) (h: y ∈ xs \/ y = Regex.emptyset): Index (xs.length) :=
   if hy: y == Regex.emptyset
   then Index.emptyset
   else Index.val (indexOf' xs y (memVector_emptyset h hy))
 
-def ofIndex' (xs: Rules μ α Pred ν) (index: Fin ν): Rule μ α Pred :=
+def ofIndex' (xs: Rules n α Pred l) (index: Fin l): Rule n α Pred :=
   xs.get index
 
-def ofIndex (xs: Rules μ α Pred ν) (index: Index ν): Rule μ α Pred :=
+def ofIndex (xs: Rules n α Pred l) (index: Index l): Rule n α Pred :=
   match index with
   | Index.emptyset => Regex.emptyset
   | Index.val n => ofIndex' xs n
 
-def compressed [DecidableEq σ] (xs: List.Vector (Regex σ) ν): Nat :=
+def compressed [DecidableEq σ] (xs: List.Vector (Regex σ) l): Nat :=
   (List.erase (List.eraseReps xs.toList) Regex.emptyset).length
 
 -- theorem compressed_cons_emptyset [DecidableEq σ] (xs: List (Regex σ)):
 --   compressed ⟨Regex.emptyset :: xs, h⟩ = compressed ⟨xs, congrArg Nat.pred h⟩ := by
 --   sorry
 
-def numReps [DecidableEq α] (xs: List.Vector α μ) (x: Option α := Option.none): Nat :=
+def numReps [DecidableEq α] (xs: List.Vector α l) (x: Option α := Option.none): Nat :=
   match x with
   | Option.none =>
     match xs with
@@ -257,7 +257,7 @@ def numReps [DecidableEq α] (xs: List.Vector α μ) (x: Option α := Option.non
       then 1 + numReps ⟨xs, congrArg Nat.pred h⟩ (Option.some x')
       else numReps ⟨xs, congrArg Nat.pred h⟩ (Option.some x')
 
-theorem numReps_none_le_length [DecidableEq α] (xs: List.Vector α μ):
+theorem numReps_none_le_length [DecidableEq α] (xs: List.Vector α l):
   numReps xs Option.none <= xs.length := by
   induction xs with
   | nil =>
@@ -292,7 +292,7 @@ theorem numReps_none_le_length [DecidableEq α] (xs: List.Vector α μ):
         simp [List.Vector.length] at ih
         omega
 
-theorem numReps_some_le_length [DecidableEq α] (xs: List.Vector α μ):
+theorem numReps_some_le_length [DecidableEq α] (xs: List.Vector α l):
   numReps xs (Option.some y) <= xs.length := by
   induction xs generalizing y with
   | nil =>
@@ -319,15 +319,15 @@ theorem numReps_some_le_length [DecidableEq α] (xs: List.Vector α μ):
       have ih' := ih (y := x)
       omega
 
-theorem numReps_le_length [DecidableEq α] (xs: List.Vector α μ) (y: Option α):
+theorem numReps_le_length [DecidableEq α] (xs: List.Vector α l) (y: Option α):
   numReps xs y <= xs.length := by
   cases y with
   | none =>
     apply numReps_none_le_length
   | some y =>
     apply numReps_some_le_length
 
--- def eraseReps [DecidableEq α] (xs: List.Vector α μ) (x: Option α := Option.none): List.Vector α (μ - numReps xs x) :=
+-- def eraseReps [DecidableEq α] (xs: List.Vector α l) (x: Option α := Option.none): List.Vector α (l - numReps xs x) :=
 --   match x with
 --   | Option.none =>
 --     match xs with
@@ -394,7 +394,7 @@ theorem numReps_le_length [DecidableEq α] (xs: List.Vector α μ) (y: Option α
 --           rw [Nat.sub_add_comm hsome]
 --       ⟩
 
-def smallest [DecidableEq α] [LT α] [DecidableLT α] (xs: List.Vector α ν) (y: α): Option (Fin ν) :=
+def smallest [DecidableEq α] [LT α] [DecidableLT α] (xs: List.Vector α l) (y: α): Option (Fin l) :=
   match xs with
   | ⟨[], h⟩ => Option.none
   | ⟨x::xs, h⟩ =>
@@ -417,7 +417,7 @@ def smallest [DecidableEq α] [LT α] [DecidableLT α] (xs: List.Vector α ν) (
           simp
         ⟩
 
--- def comp [DecidableEq σ] [LT (Regex σ)] [DecidableLT (Regex σ)] (xs: List.Vector (Regex σ) ν) (dup: Option (Regex σ) := Option.none): (List.Vector (Regex σ) (compressed xs)) × (Indices ν (compressed xs)) :=
+-- def comp [DecidableEq σ] [LT (Regex σ)] [DecidableLT (Regex σ)] (xs: List.Vector (Regex σ) l) (dup: Option (Regex σ) := Option.none): (List.Vector (Regex σ) (compressed xs)) × (Indices l (compressed xs)) :=
 --   match xs with
 --   | ⟨[], h⟩ => (⟨[], by simp [compressed, List.eraseReps, List.eraseRepsBy]⟩, ⟨[], h⟩)
 --   | ⟨x::xs, h⟩ =>
@@ -436,12 +436,12 @@ def smallest [DecidableEq α] [LT α] [DecidableLT α] (xs: List.Vector α ν) (
 --       | Option.some dup => sorry
 --     | Option.some i => sorry
 
-def compressM [DecidableEq α] [Monad m] (xs: Rules μ α Pred ν): m (Σ n, (Rules μ α Pred n) × Indices n ν) := do
+def compressM [DecidableEq α] [Monad m] (xs: Rules n α Pred l1): m (Σ l2, (Rules n α Pred l2) × Indices l2 l1) := do
   return compress xs
 
 -- expand expands a list of expressions.
-def expand (indices: Indices ν1 ν2) (xs: Rules μ α Pred ν1): (Rules μ α Pred ν2) :=
+def expand (indices: Indices l1 l2) (xs: Rules n α Pred l1): (Rules n α Pred l2) :=
   List.Vector.map (ofIndex xs) indices
 
-def expandM [Monad m] (indices: Indices ν1 ν2) (xs: Rules μ α Pred ν1): m (Rules μ α Pred ν2) :=
+def expandM [Monad m] (indices: Indices l1 l2) (xs: Rules n α Pred l1): m (Rules n α Pred l2) :=
   return (expand indices xs)