From 818252a598ee58572ec39589fd947e59d0615c6d Mon Sep 17 00:00:00 2001 From: Oleh Marakhovskyi Date: Thu, 10 Jul 2025 22:36:35 +0300 Subject: [PATCH 1/2] Trying to prove limit_add --- lib/foundations/limit.laurent | 3 ++- src/tactics.ml | 10 +++++----- src/theorems.ml | 29 +++++++++++++++++++++++++++++ 3 files changed, 36 insertions(+), 6 deletions(-) diff --git a/lib/foundations/limit.laurent b/lib/foundations/limit.laurent index 82951fc..6cbd012 100644 --- a/lib/foundations/limit.laurent +++ b/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) diff --git a/src/tactics.ml b/src/tactics.ml index c5b4f09..adf403b 100644 --- a/src/tactics.ml +++ b/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 diff --git a/src/theorems.ml b/src/theorems.ml index a26da6e..c5c82f3 100644 --- a/src/theorems.ml +++ b/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 From 5f77a2aa26f083c199816f24b8de546f5b0eb5ed Mon Sep 17 00:00:00 2001 From: Oleh Marakhovskyi Date: Thu, 10 Jul 2025 22:38:31 +0300 Subject: [PATCH 2/2] Parser developments --- dune-project | 3 ++- laurent.opam | 2 +- src/dune | 3 +++ src/laurent.ml | 12 +++++++-- src/lexer.mll | 58 ++++++++++++++++++++++++++++++++++++++++++ src/parser.mly | 68 ++++++++++++++++++++++++++++++++++++++++++++++++++ 6 files changed, 142 insertions(+), 4 deletions(-) create mode 100644 src/lexer.mll create mode 100644 src/parser.mly diff --git a/dune-project b/dune-project index cac0e88..ae5efa9 100644 --- a/dune-project +++ b/dune-project @@ -1 +1,2 @@ -(lang dune 2.0) \ No newline at end of file +(lang dune 2.0) +(using menhir 2.0) diff --git a/laurent.opam b/laurent.opam index ecc29d4..84309f7 100644 --- a/laurent.opam +++ b/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] diff --git a/src/dune b/src/dune index 1bab921..1c4d828 100644 --- a/src/dune +++ b/src/dune @@ -1,3 +1,6 @@ +(ocamllex lexer) +(menhir (modules parser)) + (executable (name laurent) (public_name laurent) diff --git a/src/laurent.ml b/src/laurent.ml index 8da59e9..ebbeee8 100644 --- a/src/laurent.ml +++ b/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 - diff --git a/src/lexer.mll b/src/lexer.mll new file mode 100644 index 0000000..70edc1c --- /dev/null +++ b/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 } diff --git a/src/parser.mly b/src/parser.mly new file mode 100644 index 0000000..f75c94d --- /dev/null +++ b/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 IDENT +%token 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 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 { [] }