Skip to content

Minor improvements #4

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
5HT merged 3 commits into from
Jun 19, 2025
Merged

Minor improvements #4

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
b6614d0
Utilize ball function
Jealrock Jun 19, 2025
f530e9d
Clear warnings
Jealrock Jun 19, 2025
09b8706
Removed duplicated workflow run on PR creation
Jealrock Jun 19, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 0 additions & 1 deletion .github/workflows/main.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
name: opam

on:
- pull_request
- push

jobs:
Expand Down
46 changes: 23 additions & 23 deletions src/inferer.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -153,7 +153,7 @@ let rec string_of_exp = function
| Limit (f, x, l, p) -> "Limit (" ^ string_of_exp f ^ ", " ^ string_of_exp x ^ ", " ^ string_of_exp l ^ ", " ^ string_of_exp p ^ ")"
| Sup s -> "Sup (" ^ string_of_exp s ^ ")"
| Inf s -> "Inf (" ^ string_of_exp s ^ ")"
| Lebesgue (f, m, set) -> "Lebesgue (" ^ string_of_exp f ^ ", " ^ string_of_exp m ^ ")"
| Lebesgue (f, m, _) -> "Lebesgue (" ^ string_of_exp f ^ ", " ^ string_of_exp m ^ ")"

let rec subst_many m t =
match t with
Expand Down Expand Up @@ -208,8 +208,8 @@ and infer env (ctx : context) (e : exp) : exp =
| Set a ->
let a_ty = infer env ctx a in
(match a_ty with
| Forall (x, domain, body) when equal env ctx domain Real && equal env ctx body Prop -> Set Real
| Universe i -> Universe 0
| Forall (_, domain, body) when equal env ctx domain Real && equal env ctx body Prop -> Set Real
| Universe _ -> Universe 0
| Set b -> Set b
| _ -> raise (TypeError ("Set expects a predicate or type, got " ^ string_of_exp a_ty)))
| SetEq (s1, s2) ->
Expand All @@ -222,9 +222,9 @@ and infer env (ctx : context) (e : exp) : exp =
| False -> Prop
| Universe 0 -> Universe 1
| Universe 1 -> Universe 1
| Universe i -> raise (TypeError "Invalid Universe (index should be less than 2)")
| Universe _ -> raise (TypeError "Invalid Universe (index should be less than 2)")
| Var x -> (match lookup_var ctx x with | Some ty -> ty | None -> raise (TypeError ("Unbound variable: " ^ x)))
| Forall (x, Real, Pair (Lam (x1, p, q), Lam (y, q', p'))) when equal env ctx p p' && equal env ctx q q' -> Prop
| Forall (_, Real, Pair (Lam (_, p, q), Lam (_, q', p'))) when equal env ctx p p' && equal env ctx q q' -> Prop
| Forall (x, domain, body) ->
let _ = infer env ctx domain in
let ctx' = add_var ctx x domain in
Expand All @@ -241,21 +241,21 @@ and infer env (ctx : context) (e : exp) : exp =
| Forall (x, a, b) -> check env ctx arg a; subst x arg b
| Set (Set a) -> check env ctx arg (Set a); Prop
| Set Real -> check env ctx arg Real; Prop
| ty -> raise (TypeError "Application requires a Pi type"))
| _ -> raise (TypeError "Application requires a Pi type"))
| Lam (x, domain, body) ->
let ctx' = add_var ctx x domain in
let body_ty = infer env ctx' body in
let domain_ty = infer env ctx domain in
(match domain, body with
| Real, Prop -> Set Real
| _ -> (match domain_ty with
| Universe i -> Forall (x, domain, body_ty)
| Universe _ -> Forall (x, domain, body_ty)
| Real -> if equal env ctx body_ty Prop then Set Real else Forall (x, domain, body_ty)
| Prop -> Forall (x, domain, body_ty)
| _ -> raise (TypeError "Lambda domain must be a type or proposition")))
| Pair (a, b) -> let a_ty = infer env ctx a in let b_ty = infer env (add_var ctx "N" a_ty) b in Exists ("N", a_ty, b_ty)
| Fst p -> (match infer env ctx p with | Exists (x, a, b) -> a | ty -> raise (TypeError ("Fst expects a Sigma type")))
| Snd p -> (match infer env ctx p with | Exists (x, a, b) -> subst x (Fst p) b | ty -> raise (TypeError ("Snd expects a Sigma type")))
| Fst p -> (match infer env ctx p with | Exists (_, a, _) -> a | _ -> raise (TypeError ("Fst expects a Sigma type")))
| Snd p -> (match infer env ctx p with | Exists (x, _, b) -> subst x (Fst p) b | _ -> raise (TypeError ("Snd expects a Sigma type")))
| Prop -> Universe 0
| Bool -> Universe 0
| Integer -> Universe 0
Expand All @@ -276,8 +276,8 @@ and infer env (ctx : context) (e : exp) : exp =
let ct = infer env ctx cond in
let _ = check env ctx ct (Universe 0) in
let t_typ = infer env ctx f in let _ = check env ctx t t_typ in t_typ
| Vec (n, field, a, b) -> let _ = check env ctx field (Universe 0) in let _ = check env ctx a field in let _ = check env ctx b field in Universe 0
| RealIneq (op, a, b) ->
| Vec (_, field, a, b) -> let _ = check env ctx field (Universe 0) in let _ = check env ctx a field in let _ = check env ctx b field in Universe 0
| RealIneq (_, a, b) ->
let _ = infer env ctx a in
let _ = infer env ctx b in
Prop
Expand All @@ -286,7 +286,7 @@ and infer env (ctx : context) (e : exp) : exp =
(match op with
| Plus | Minus | Times | Div | Pow -> let _ = check env ctx b Real in Real
| Abs | Ln | Sin | Cos | Exp | Neg -> Real)
| ComplexOps (op, a, b) -> let _ = check env ctx a Complex in let _ = check env ctx b Complex in Complex
| ComplexOps (_, a, b) -> let _ = check env ctx a Complex in let _ = check env ctx b Complex in Complex
| Closure s -> let _ = check env ctx s (Set Real) in Set Real
| Union a -> let _ = check env ctx a (Forall ("n", Nat, Set Real)) in Set Real
| Complement a ->
Expand Down Expand Up @@ -348,7 +348,7 @@ and infer env (ctx : context) (e : exp) : exp =
and universe env ctx t =
match infer env ctx t with
| Universe i -> if i < 0 then raise (TypeError "Negative universe level"); i
| ty -> raise (TypeError (Printf.sprintf "Expected a universe"))
| _ -> raise (TypeError (Printf.sprintf "Expected a universe"))

and check env (ctx : context) (term : exp) (expected : exp) : unit =
if trace then Printf.printf "Check: %s Expected: %s\n" (string_of_exp term) (string_of_exp expected);
Expand All @@ -366,8 +366,8 @@ and equal' env ctx t1 t2 =
| Universe i, Universe j -> i <= j
| Forall (x, a, b), Forall (y, a', b') -> equal' env ctx a a' && equal' env (add_var ctx x a) b (subst y (Var x) b')
| Lam (x, d, b), Lam (y, d', b') -> equal' env ctx d d' && equal' env (add_var ctx x d) b (subst y (Var x) b')
| Lam (x, d, b), t when not (is_lam t) -> let x_var = Var x in equal' env ctx b (App (t, x_var)) && (match infer env ctx t with | Forall (y, a, b') -> equal' env ctx d a | _ -> false)
| t, Lam (x, d, b) when not (is_lam t) -> let x_var = Var x in equal' env ctx (App (t, x_var)) b && (match infer env ctx t with | Forall (y, a, b') -> equal' env ctx a d | _ -> false)
| Lam (x, d, b), t when not (is_lam t) -> let x_var = Var x in equal' env ctx b (App (t, x_var)) && (match infer env ctx t with | Forall (_, a, _) -> equal' env ctx d a | _ -> false)
| t, Lam (x, d, b) when not (is_lam t) -> let x_var = Var x in equal' env ctx (App (t, x_var)) b && (match infer env ctx t with | Forall (_, a, _) -> equal' env ctx a d | _ -> false)
| App (f, arg), App (f', arg') -> equal' env ctx f f' && equal' env ctx arg arg'
| Exists (x, a, b), Exists (y, a', b') -> equal' env ctx a a' && let ctx' = add_var ctx x a in equal' env ctx' b (subst y (Var x) b')
| Pair (a, b), Pair (a', b') -> equal' env ctx a a' && equal' env ctx b b'
Expand Down Expand Up @@ -415,25 +415,25 @@ and equal' env ctx t1 t2 =
and reduce env ctx t =
if verbose then Printf.printf "Reduce: %s\n" (string_of_exp t);
match t with
| SetEq (Set (Lam (x1, Real, p1)), Set (Lam (x2, Real, p2))) -> smt_verify_iff ctx_z3 p1 p2
| SetEq (Set (Lam (_, Real, p1)), Set (Lam (_, Real, p2))) -> smt_verify_iff ctx_z3 p1 p2
| SetEq (s, s') when equal env ctx s s' -> True
| Intersect (Set (Lam (x1, Real, p1)), Set (Lam (x2, Real, p2))) ->
Set (Lam ("x", Real, And (subst x1 (Var "x") p1, subst x2 (Var "x") p2)))
| Intersect (a, b) -> Intersect (reduce env ctx a, reduce env ctx b)
| App (Lam (x, domain, body), arg) -> subst x arg body
| Set (Lam (x, domain, body)) -> True
| App (Lam (x, _, body), arg) -> subst x arg body
| Set (Lam _) -> True
| App (f, arg) -> let f' = reduce env ctx f in let arg' = reduce env ctx arg in App (f', arg')
| Fst (Pair (a, b)) -> a
| Snd (Pair (a, b)) -> b
| Fst (Pair (a, _)) -> a
| Snd (Pair (_, b)) -> b
| Limit (f, x, l, p) -> Limit (reduce env ctx f, reduce env ctx x, reduce env ctx l, reduce env ctx p)
| RealOps (Abs, RealOps (Minus, a, b), Zero) ->
let a' = reduce env ctx a in
let b' = reduce env ctx b in
if equal env ctx a' b' then Zero else RealOps (Abs, RealOps (Minus, a', b'), Zero)
| RealIneq (Lt, e1, e2) ->
| RealIneq (Lt, e1, _) ->
let in_context = List.exists (fun (_, assum) ->
match assum with
| And (_, RealIneq (Lt, e1', Var delta)) when equal env ctx e1 e1' -> true
| And (_, RealIneq (Lt, e1', _)) when equal env ctx e1 e1' -> true
| _ -> false
) ctx in
if in_context then True else t
Expand All @@ -456,7 +456,7 @@ and z3_of_exp ctx = function
| RealConst i -> Arithmetic.Real.mk_numeral_i ctx (int_of_float i)
| Set (Lam (_, Real, body)) -> z3_of_exp ctx body
| RealOps (Plus, e1, e2) -> Arithmetic.mk_add ctx [z3_of_exp ctx e1; z3_of_exp ctx e2]
| Intersect (Set (Lam (x1, Real, p1)), Set (Lam (x2, Real, p2))) -> Boolean.mk_and ctx [z3_of_exp ctx p1; z3_of_exp ctx p2]
| Intersect (Set (Lam (_, Real, p1)), Set (Lam (_, Real, p2))) -> Boolean.mk_and ctx [z3_of_exp ctx p1; z3_of_exp ctx p2]
| App (Set (Lam (x, Real, body)), arg) -> z3_of_exp ctx (subst x arg body)
| x -> failwith ("Unsupported expression in Z3 conversion: " ^ (string_of_exp x))

Expand Down
1 change: 0 additions & 1 deletion src/laurent.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
open Tactics
open Inferer
open Theorems
open Suite

Expand Down
42 changes: 20 additions & 22 deletions src/tactics.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ 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 (Minus, Var y, Var x), Var delta))
RealIneq (Lt, RealOps (Abs, RealOps (Minus, Var y, x), Zero), Var delta))

type tactic =
| Intro of string
Expand All @@ -44,7 +44,7 @@ let print_state state =
List.iter print_goal state.goals;
Printf.printf "%d goals remaining\n" (List.length state.goals)

let update_goal state goal new_target new_ctx =
let create_goal state new_target new_ctx =
{ target = new_target; ctx = new_ctx; id = next_id state }

let parse_exp (s : string) : exp =
Expand Down Expand Up @@ -72,17 +72,17 @@ let parse_tactic (input : string) : tactic =

let apply_tactic env state tac =
match tac with
| Intro var ->
| Intro _ ->
(match state.goals with
| goal :: rest ->
(match goal.target with
| Forall (v, ty, body) ->
let new_ctx = (v, ty) :: goal.ctx in
let new_goal = update_goal state goal body new_ctx in
let new_goal = create_goal state body new_ctx in
(match body with
| Forall (_, assum, inner_body) ->
let new_ctx' = ("_assum", assum) :: new_ctx in
{ state with goals = update_goal state goal inner_body new_ctx' :: rest }
{ state with goals = create_goal state inner_body new_ctx' :: rest }
| _ ->
{ state with goals = new_goal :: rest })
| _ -> raise (TacticError "Intro expects a forall"))
Expand All @@ -91,9 +91,9 @@ let apply_tactic env state tac =
(match state.goals with
| goal :: rest ->
(match goal.target with
| Exists (var, ty, body) ->
| Exists (var, _, body) ->
let new_target = subst var e body in
let new_goal = update_goal state goal new_target goal.ctx in
let new_goal = create_goal state new_target goal.ctx in
let simplified_target = normalize env new_goal.ctx new_target in
if equal env new_goal.ctx simplified_target True ||
List.exists (fun (_, e') -> equal env new_goal.ctx e' simplified_target) new_goal.ctx
Expand All @@ -106,8 +106,8 @@ let apply_tactic env state tac =
| goal :: rest ->
(match goal.target with
| And (p, q) ->
let goal1 = update_goal state goal p goal.ctx in
let goal2 = update_goal state goal q goal.ctx in
let goal1 = create_goal state p goal.ctx in
let goal2 = create_goal state q goal.ctx in
{ state with goals = goal1 :: goal2 :: rest }
| _ -> raise (TacticError "Split expects a conjunction"))
| _ -> raise (TacticError "No goals"))
Expand All @@ -117,14 +117,14 @@ let apply_tactic env state tac =
let simplified_target = normalize env goal.ctx goal.target in
let is_trivial =
match simplified_target with
| Forall (_, _, Forall (x, Real, Forall (_, RealIneq (Lt, _, _), RealIneq (Lt, e2, Var "eps")))) ->
| Forall (_, _, Forall (_, Real, Forall (_, RealIneq (Lt, _, _), RealIneq (Lt, e2, Var "eps")))) ->
let reduced_e2 = reduce env goal.ctx e2 in
equal env goal.ctx reduced_e2 Zero &&
List.exists (fun (_, assum) ->
match assum with
| RealIneq (Gt, Var "eps", Zero) -> true
| _ -> false) goal.ctx
| Forall (n, Nat, Forall (_, RealIneq (Gt, Var n', e1), RealIneq (Lt, e2, Var "eps"))) ->
| Forall (_, Nat, Forall (_, RealIneq (Gt, Var _, _), RealIneq (Lt, e2, Var "eps"))) ->
let reduced_e2 = reduce env goal.ctx e2 in
equal env goal.ctx reduced_e2 Zero &&
List.exists (fun (_, assum) ->
Expand All @@ -148,15 +148,15 @@ let apply_tactic env state tac =
(match state.goals with
| goal :: rest ->
(match goal.target with
| Limit (Seq f, x, l, p) ->
| Limit (Seq f, _, l, _) ->
let new_target =
Forall ("eps", Real,
Forall ("_", RealIneq (Gt, Var "eps", Zero),
Exists ("N", Real,
Forall ("n", Nat,
Forall ("_", RealIneq (Gt, Var "n", Var "N"),
RealIneq (Lt, RealOps (Abs, RealOps (Minus, App (f, Var "n"), l), Zero), Var "eps")))))) in
let new_goal = update_goal state goal new_target goal.ctx in
let new_goal = create_goal state new_target goal.ctx in
{ state with goals = new_goal :: rest }
| _ -> raise (TacticError "Limit expects a limit expression"))
| _ -> raise (TacticError "No goals"))
Expand Down Expand Up @@ -188,7 +188,7 @@ let apply_tactic env state tac =
Forall ("x", Real,
Forall ("_", RealIneq (Lt, RealOps (Abs, RealOps (Minus, Var "x", a), Zero), Var "delta"),
RealIneq (Lt, RealOps (Abs, RealOps (Minus, App (f, Var "x"), App (f, a)), Zero), Var "eps"))))))) in
let new_goal = update_goal state goal new_target goal.ctx in
let new_goal = create_goal state new_target goal.ctx in
{ state with goals = new_goal :: rest }
| _ -> raise (TacticError "Continuity expects a continuous_at expression"))
| _ -> raise (TacticError "No goals"))
Expand All @@ -197,18 +197,16 @@ let apply_tactic env state tac =
| goal :: rest ->
let new_var = var ^ "_near" in
let delta_var = "delta_" ^ var in
let near_assumption =
And (RealIneq (Gt, Var delta_var, Zero),
RealIneq (Lt, RealOps (Abs, RealOps (Minus, Var new_var, point), Zero), Var delta_var)) in
let near_assumption = ball point delta_var new_var in
let new_ctx = (new_var, Real) :: (delta_var, Real) :: goal.ctx in
let new_target =
match goal.target with
| Forall (v, ty, Forall (_, App (Var "near", Var v'), body)) when v = v' ->
| Forall (v, _, Forall (_, App (Var "near", Var v'), body)) when v = v' ->
Forall ("_", near_assumption, subst v (Var new_var) body)
| _ ->
Forall ("_", near_assumption, goal.target)
in
let new_goal = update_goal state goal new_target new_ctx in
let new_goal = create_goal state new_target new_ctx in
{ state with goals = new_goal :: rest }
| _ -> raise (TacticError "No goals to apply near tactic"))
| ApplyLocally ->
Expand All @@ -218,14 +216,14 @@ let apply_tactic env state tac =
| Forall (_, assumption, consequent) ->
let rec extract_near assum ctx =
match assum with
| And (RealIneq (Gt, delta, Zero), rest_assum) ->
| And (RealIneq (Gt, _, Zero), _) ->
let new_ctx = ("assumption", assum) :: goal.ctx in
let simplified_target = normalize env new_ctx consequent in
if equal env new_ctx simplified_target True ||
List.exists (fun (_, e') -> equal env new_ctx e' simplified_target) new_ctx
then { goals = rest; solved = (goal.id, consequent) :: state.solved }
else { state with goals = update_goal state goal consequent new_ctx :: rest }
| And (left, right) -> extract_near right ctx
else { state with goals = create_goal state consequent new_ctx :: rest }
| And (_, right) -> extract_near right ctx
| _ -> raise (TacticError ("ApplyLocally expects a near-like assumption: " ^ string_of_exp goal.target))
in
extract_near assumption goal.ctx
Expand Down
1 change: 0 additions & 1 deletion src/theorems.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
open Inferer
open Suite
open Tactics

(* LAURENT MATHEMATICS 💡 *)
Expand Down