[DRAFT] Syntax

dune-project

@@ -1 +1,2 @@
-(lang dune 2.0)
+(lang dune 2.0)
+(using menhir 2.0)

laurent.opam

@@ -14,7 +14,7 @@ depends: [
   "z3" {>= "4.14"}
   "num" {>= "1.5"}
   "ocaml" {>= "4.14"}
-  "menhir" {>= "20220210"}
+  "menhir" {>= "20240715"}
 ]
 build: [
   ["dune" "build" "-p" name "-j" jobs]

lib/foundations/limit.laurent

@@ -1 +1,2 @@
-module limit where
+def limit_add : (f g : Nat -> Real) (L M : Real) (x_0 : Real),
+    lim f x_0 L -> lim g x_0 M -> lim (λ (n : Nat), f n + g n) x_0 (L + M)

src/dune

@@ -1,3 +1,6 @@
+(ocamllex lexer)
+(menhir (modules parser))
+
 (executable
  (name laurent)
  (public_name laurent)

src/laurent.ml

@@ -4,7 +4,7 @@ open Suite
 
 (* LAURENT LAUNCHER 🚀 *)
 
-let usage = "laurent [ repl | banner ]"
+let usage = "laurent [ repl | banner | *file* ]"
 
 let banner =
 "https://laurent.groupoid.space/
@@ -13,6 +13,13 @@ let banner =
 
 For help type `help`."
 
+let evalFile path : unit =
+  let chan = open_in path in
+  let lexbuf = Lexing.from_channel chan in
+  let commands = Parser.main Lexer.read lexbuf in
+  close_in chan;
+  flush_all ()
+
 let () =
     let args = Array.to_list Sys.argv in
     match args with
@@ -22,5 +29,6 @@ let () =
     | [_; "banner"] -> test_foundations ();
                        test_mathematics ();
                        print_endline banner
+    | [_; file] when Sys.file_exists file ->
+                       evalFile file
     | _ ->             print_endline usage
-

src/lexer.mll

@@ -0,0 +1,58 @@
+{
+  open Parser
+  open Lexing
+
+  let nextLine lexbuf =
+    let pos = lexbuf.lex_curr_p in
+    lexbuf.lex_curr_p <- { pos with pos_bol = pos.pos_cnum; pos_lnum = pos.pos_lnum + 1 }
+}
+
+let nl = "\r\n"|"\r"|"\n"
+let inlineComment = "--" [^ '\n' '\r']* (nl|eof)
+
+let ws     = ['\t' ' ']
+let latin1 = [^ '\t' ' ' '\r' '\n' '(' ')' ':' ',' '|' '{' '}'] # '-'
+let bytes2 = ['\192'-'\223']['\128'-'\191']
+let bytes3 = ['\224'-'\239']['\128'-'\191']['\128'-'\191']
+let bytes4 = ['\240'-'\247']['\128'-'\191']['\128'-'\191']['\128'-'\191']
+let utf8   = latin1|bytes2|bytes3|bytes4
+let ident  = utf8*
+let number = ['0'-'9']+
+
+let defeq  = ":=" | "\xE2\x89\x94"
+let arrow  = "->" | "\xE2\x86\x92"
+let lam    = "\\" | "\xCE\xBB"
+let forall = "forall" | "\xE2\x88\x80"
+let exists = "exists" | "\xE2\x88\x83"
+
+rule read = parse
+| nl { nextLine lexbuf; read lexbuf }
+| inlineComment { nextLine lexbuf; read lexbuf }
+| ws+ { read lexbuf }
+| '(' { LPARENS }
+| ')' { RPARENS }
+| '{' { LBRACE }
+| '}' { RBRACE }
+| '|' { PIPE }
+| '?' { HOLE }
+| lam { LAM }
+| arrow { ARROW }
+| ':' { COLON }
+| ',' { COMMA }
+| "def" { DEF }
+| ":=" { DEFEQ }
+| forall { FORALL }
+| exists { EXISTS }
+| "Prop" { PROP }
+| "Real" | "ℝ" { REAL }
+| "Nat" | "ℕ" { NAT }
+| "Set" { SET }
+| ">" { GT }
+| "<" { LT }
+| "=" { EQ }
+| "+" { PLUS }
+| "-" { MINUS }
+| "*" { TIMES }
+| number as n { NUMBER (int_of_string n) }
+| ident as s { IDENT s }
+| eof { EOF }

src/parser.mly

@@ -0,0 +1,68 @@
+%{
+  open Inferer
+
+  let rec mk_forall params body =
+    match params with
+    | [] -> body
+    | (x, ty) :: rest -> Forall (x, ty, mk_forall rest body)
+
+  let rec mk_lam params body =
+    match params with
+    | [] -> body
+    | (x, ty) :: rest -> Lam (x, ty, mk_lam rest body)
+%}
+
+%token <string> IDENT
+%token <int> NUMBER
+%token LPARENS RPARENS LBRACE RBRACE PIPE
+%token COLON COMMA LAM ARROW DEF DEFEQ
+%token FORALL EXISTS PROP REAL NAT SET
+%token GT LT EQ PLUS MINUS TIMES
+%token EOF
+
+%right ARROW
+%left PLUS MINUS
+%left TIMES
+%left GT LT EQ
+
+%start <Inferer.exp list> main
+
+%%
+
+typ:
+  | PROP { Prop }
+  | REAL { Real }
+  | NAT { Nat }
+  | SET typ { Set $2 }
+  | typ ARROW typ { Forall ("_", $1, $3) }
+  | LPARENS typ RPARENS { $2 }
+
+param:
+  | LPARENS IDENT COLON typ RPARENS { ($2, $4) }
+
+params:
+  | param { [$1] }
+  | param params { $1 :: $2 }
+
+exp:
+  | IDENT { Var $1 }
+  | NUMBER { if $1 = 0 then Zero else if $1 = 1 then One else RealConst (float_of_int $1) }
+  | LAM params COMMA exp { mk_lam $2 $4 }
+  | FORALL params COMMA exp { mk_forall $2 $4 }
+  | exp exp %prec TIMES { App ($1, $2) }
+  | exp PLUS exp { RealOps (Plus, $1, $3) }
+  | exp MINUS exp { RealOps (Minus, $1, $3) }
+  | exp TIMES exp { RealOps (Times, $1, $3) }
+  | exp GT exp { RealIneq (Gt, $1, $3) }
+  | exp LT exp { RealIneq (Lt, $1, $3) }
+  | exp EQ exp { RealIneq (Eq, $1, $3) }
+  | LBRACE IDENT COLON typ PIPE exp RBRACE { Set (Lam ($2, $4, $6)) }
+  | LPARENS exp RPARENS { $2 }
+
+definition:
+  | DEF IDENT COLON typ DEFEQ exp { ($2, $4, $6) }
+
+main:
+  | definition main { let (name, ty, term) = $1 in term :: $2 }
+  | exp main { $1 :: $2 }
+  | EOF { [] }

src/tactics.ml

@@ -15,9 +15,9 @@ type proof_state = {
 
 let next_id state = 1 + List.fold_left (fun m g -> max m g.id) 0 state.goals
 
-let ball x delta y =
-  And (RealIneq (Gt, Var delta, Zero),
-    RealIneq (Lt, RealOps (Abs, RealOps (Minus, Var y, x), Zero), Var delta))
+let ball point eps x =
+  And (RealIneq (Gt, eps, Zero),
+    RealIneq (Lt, RealOps (Abs, RealOps (Minus, x, point), Zero), eps))
 
 type tactic =
   | Intro of string
@@ -80,7 +80,7 @@ let apply_tactic env state tac =
               let new_ctx = (v, ty) :: goal.ctx in
               let new_goal = create_goal state body new_ctx in
               (match body with
-               | Forall (_, assum, inner_body) ->
+               | Forall ("_", assum, inner_body) ->
                    let new_ctx' = ("_assum", assum) :: new_ctx in
                    { state with goals = create_goal state inner_body new_ctx' :: rest }
                | _ ->
@@ -197,7 +197,7 @@ let apply_tactic env state tac =
      | goal :: rest ->
          let new_var = var ^ "_near" in
          let delta_var = "delta_" ^ var in
-         let near_assumption = ball point delta_var new_var in
+         let near_assumption = ball point (Var delta_var) (Var new_var) in
          let new_ctx = (new_var, Real) :: (delta_var, Real) :: goal.ctx in
          let new_target =
            match goal.target with

src/theorems.ml

@@ -27,6 +27,35 @@ let state3 = initial_state
           RealOps (Abs, RealOps (Minus, Var "x", One), Zero),
           RealOps (Plus, One, One)))))
 
+let limit_proof f f_0 =
+  Forall ("eps", Real,
+    Forall("x", Real,
+      Forall ("_", (ball f_0 (Var "eps") (Var "x")),
+        RealIneq (Lt,
+          RealOps (Abs, RealOps (Minus, App (f, (Var "x")) , f_0), Zero),
+          Var "eps"))))
+
+let limit_add_state = {
+  goals = [
+    { ctx =
+        ("f", Seq (Lam("n", Nat, Real))) ::
+        ("g", Seq (Lam("n", Nat, Real))) ::
+        ("f_0", Real) ::
+        ("g_0", Real) ::
+        ("lim_f", limit_proof (Var "f") (Var "f_0")) ::
+        ("lim_g", limit_proof (Var "g") (Var "g_0")) ::
+        [];
+      target = Limit (Seq (Lam ("n", Nat,
+                                 RealOps (Plus, (App (Var "f", Var "n")),
+                                                (App (Var "g", Var "n"))))),
+                       Infinity,
+                       RealOps (Plus, Var "f_0", Var "g_0"),
+                       Var "pfg");
+      id = 1 }
+  ];
+  solved = [];
+}
+
 let test_mathematics () =
   let env = [] in