calculate nfa attempt

Author: awalterschulze

Katydid/Expr/CalculateCompiler.lean

@@ -0,0 +1,91 @@
+-- Based on: https://youtu.be/uMurx1a6Zck?t=20144
+-- We want:
+-- 1. A Compiler (comp)
+-- 2. A Virtual Machine (exec)
+-- 3. A proof that it is correct (comp, exec = eval)
+
+inductive Regex where
+  | emptyset: Regex
+  | emptystr: Regex
+  | char (c: Char): Regex
+  | or (left: Regex) (right: Regex): Regex
+  deriving BEq
+
+def derive (r: Regex) (c: Char): Regex :=
+  match r with
+  | Regex.emptyset => Regex.emptyset
+  | Regex.emptystr => Regex.emptyset
+  | Regex.char a => if a == c then Regex.emptystr else Regex.emptystr
+  | Regex.or a b => Regex.or (derive a c) (derive b c)
+
+-- `eval :: Expr -> Int`
+-- `eval :: Expr -> m Int`
+-- `eval :: Expr -> State s Int`
+-- `newtype State s v = State (s -> (s, v))`
+-- `eval :: Expr -> s -> (s, v)`
+-- `eval :: Regex -> String -> (String, Regex)`
+def eval (r: Regex) (s: List Char): (List Char × Regex) :=
+  (]
+  , List.foldl derive r s)
+
+-- The instruction set
+-- To Calculate: `data Code = ?`
+
+-- The compiler
+-- Intuition: `comp :: Expr -> Code`
+-- Practically we need a continuation in the compiler:
+--  `comp :: Expr -> Code -> Code`, where initial Code is empty code
+--  `comp :: Regex -> NFA -> NFA`, where initial NFA is an empty NFA
+def comp (r: Regex) (d: NFA): NFA :=
+  sorry
+
+-- The virtual machine
+-- `type Stack :: [Int]`
+-- `exec :: Code -> Stack -> Stack`
+-- `exec :: Code -> Stack -> m Stack`
+-- `exec :: Code -> Stack -> State s Stack`
+-- `newtype State s v = State (s -> (s, v))`
+-- `exec :: NFA -> List Regex -> String -> (String, List Regex)`
+-- Regex = the NFA state, otherwise we cannot do an equality between eval and exec
+def exec (d: NFA) (current: List Regex) (s: String): (String × List Regex) :=
+  sorry
+
+-- Intuition: `comp, exec = eval`
+-- Intuition: `exec (comp e) s = eval e : s`
+-- Practically: `exec (comp e c) s = exec c (eval e : s)`
+-- With Effects: `exec (comp e c) s = do v <- eval e; exec c (v: s)`
+-- Solve this equation with 3 unknowns: comp, exec and code
+-- This equation has more unknowns that equations
+-- We solve this via constructive induction
+-- With Regex: `exec (comp initial_regex empty_dfa) empty_regex str`
+--             `= let (dstr, dregex) := eval initial_regex str in exec empty_dfa (dregex: empty_regex) dstr`
+-- c = any_dfa or empty_dfa
+-- e = initial_regex
+-- s = any_regexes or empty_regexs or []
+-- s has to be a list of states, to keep this formula general enough
+-- if s is a list then we compile to an NFA, instead of a DFA
+-- if we are compiling an automaton then our states have to regexes to be equal to eval and eval has to return a regex.
+-- So this means that derivatives are probably going to be evaluator.
+
+-- e = Val n
+-- do v <- eval (Val n); exec c (v: s)
+-- ...
+-- = exec c' s
+-- c' = comp (Val n) c
+
+-- initial_regex = char c
+-- `let (dstr, dregex) := eval (char c) str in exec empty_dfa (dregex: empty_regex) dstr`
+-- `let (dstr, dregex) := ("", String.foldl derive (char c) str) in exec empty_dfa (dregex: empty_regex) dstr`
+-- `let dregex := String.foldl derive (char c) str in exec empty_dfa (dregex: empty_regex) ""`
+-- `exec (comp initial_regex empty_dfa) empty_regex str`
+
+
+-- comp, exec = eval
+-- exec (comp regex dfa) char = derive regex char
+-- exec (comp regex dfa) (char:str) = exec (derive regex char) str
+-- exec (comp (Char c) dfa) char = derive (Char c) char
+-- if a == c then Regex.emptystr else Regex.emptystr
+-- (comp (Char c) dfa)
+-- dfa.add[Regex.char c, c] => Regex.emptystr
+-- dfa.add[Regex.char c, !c] => Regex.emptyset
+-- = exec c' char where c' = (comp (Char c) dfa)

Katydid/Expr/Recurse.lean

@@ -0,0 +1,152 @@
+-- Haskell
+--   data RegexF r = EmptySet
+--     | EmptyString
+--     | Character Char
+--     | Concat r r
+--     | ZeroOrMore r
+--     | Or r r
+--     deriving Functor
+-- Ocaml
+--  type 'r expr_node =
+--    | Const of int
+--    | Var of Id.t
+--    | Add of 'r * 'r
+--    | ...
+-- Lean
+inductive RegexF (r: Type u) where
+  | emptyset: RegexF r
+  | emptystr: RegexF r
+  | char: Char -> RegexF r
+  | concat: r -> r -> RegexF r
+  | star: r -> RegexF r
+  | or: r -> r -> RegexF r
+
+def RegexF.map {α β : Type u} (f: α → β) (r: RegexF α): RegexF β :=
+  match r with
+  | emptyset => emptyset
+  | emptystr => emptystr
+  | char c => char c
+  | concat p q => concat (f p) (f q)
+  | star p => star (f p)
+  | or p q => or (f p) (f q)
+
+instance : Functor RegexF where
+  map := RegexF.map
+
+-- Haskell
+--   type Regex = Fix RegexF
+-- Ocaml
+--   type expr = { unfix : expr expr_node }
+-- Lean
+inductive Regex where
+  | unfix: RegexF Regex -> Regex
+
+-- Haskell
+--   newtype Fix f = Fix (f (Fix f))
+-- Ocaml
+--   let fix : expr expr_node -> expr = fun e -> { unfix = e }
+-- Lean
+def fix: RegexF Regex -> Regex :=
+  fun (e) => Regex.unfix e
+
+-- Haskell
+--   wreckit :: Fix f -> f (Fix f)
+--   wreckit (Fix x) = x
+--   wreckit :: Regex -> RegexF Regex
+-- Ocaml
+--   let unfix r = r.unfix
+-- Lean
+def unfix: Regex -> RegexF Regex :=
+  fun r =>
+    match r with
+    | Regex.unfix rf => rf
+
+def RegexF.sizeof [SizeOf a] (r: RegexF a): Nat :=
+  match r with
+  | RegexF.emptyset => 0
+  | RegexF.emptystr => 1
+  | RegexF.char _ => 2
+  | RegexF.concat p q =>  1 + sizeOf p + sizeOf q
+  | RegexF.star p => 1 + sizeOf p
+  | RegexF.or p q => 1 + sizeOf p + sizeOf q
+
+instance [SizeOf r]: SizeOf (RegexF r) where
+  sizeOf := RegexF.sizeof
+
+def Regex.sizeof (r: Regex): Nat :=
+  match r with
+  | Regex.unfix rf =>
+    match rf with
+    | RegexF.emptyset => 0
+    | RegexF.emptystr => 1
+    | RegexF.char _ => 2
+    | RegexF.concat p q =>  1 + sizeof p + sizeof q
+    | RegexF.star p => 1 + sizeof p
+    | RegexF.or p q => 1 + sizeof p + sizeof q
+
+instance : SizeOf Regex where
+  sizeOf := Regex.sizeof
+
+def emptyset: Regex :=
+  fix RegexF.emptyset
+
+def emptystr: Regex :=
+  fix RegexF.emptystr
+
+def char (c: Char): Regex :=
+  fix (RegexF.char c)
+
+def concat (p q: Regex): Regex :=
+  fix (RegexF.concat p q)
+
+def star (p: Regex): Regex :=
+  fix (RegexF.star p)
+
+def or' (p q: Regex): Regex :=
+  fix (RegexF.or p q)
+
+def nullableAlg (r: RegexF Bool): Bool :=
+  match r with
+  | RegexF.emptyset => false
+  | RegexF.emptystr => true
+  | RegexF.char _ => false
+  | RegexF.concat p q => p && q
+  | RegexF.star _ => true
+  | RegexF.or p q => p || q
+
+-- type FAlgebra f r = f r -> r
+-- type NullableFAlgebra = FAlgebra RegexF Bool
+-- cata :: NullableFAlgebra -> Regex -> Bool
+-- cata nullableAlg regex =
+--   wreckit regex
+--   |> fmap (cata nullableAlg)
+--   |> nullableAlg
+def cata (f: RegexF Bool -> Bool) (regex: Regex): Bool :=
+  let uregex := unfix regex
+  let cf := fun (rr: Regex) => cata f rr
+  f (Functor.map cf uregex)
+  termination_by regex
+  decreasing_by sorry
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+-- nullable :: Regex -> Bool
+-- nullable = cata nullableAlg
+def nullable (r: Regex): Bool :=
+  cata nullableAlg r
+
+-- def cata [Functor f] : FAlgebra f r -> Fix f -> r
+-- cata alg = alg . fmap (cata alg) . wreckit

Katydid/Std/Ltac.lean

@@ -80,15 +80,33 @@ def run (t: Lean.Elab.Tactic.TacticM (Lean.TSyntax `tactic)): Lean.Elab.Tactic.T
   let t' ← t
   Lean.Elab.Tactic.evalTactic t'
 
--- an example tactic that applies a hypothesis to the goal if it matches a pattern
-local elab "example_apply_hypothesis" : tactic => do
+-- an example tactic that applies a hypothesis to the goal if it matches a pattern using the Qq library.
+local elab "example_apply_hypothesis_prop" : tactic => do
   let hyps ← getHypothesesProp
   for (name, ty) in hyps do
     if let ~q((((($a : Prop)) → $b) : Prop)) := ty then
       run `(tactic| apply $name )
 
 example {A B: Prop} (P: A -> B) (a: A): B := by
+  example_apply_hypothesis_prop
+  assumption
+
+local elab "example_apply_hypothesis" : tactic => do
+  let hyps ← getHypotheses
+  for (name, ty) in hyps do
+    match ty with
+    | Lean.Expr.forallE _ _ _ _ =>
+      run `(tactic| apply $name )
+      return ()
+    | _ =>
+      continue
+
+example : 1 = 1 :=
+  rfl
+
+theorem example100 {C D: Prop} (Q: C -> D) (a: C): D := by
   example_apply_hypothesis
+  try apply Q
   assumption
 
 -- Returns the main goal as a Q(Prop), such that it can be used in a pattern match.