diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 4cdcb78..4c8e43d 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -1,7 +1,6 @@ name: opam on: - - pull_request - push jobs: diff --git a/src/inferer.ml b/src/inferer.ml index 19acad0..0c0c85f 100644 --- a/src/inferer.ml +++ b/src/inferer.ml @@ -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 @@ -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) -> @@ -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 @@ -241,7 +241,7 @@ 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 @@ -249,13 +249,13 @@ and infer env (ctx : context) (e : exp) : exp = (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 @@ -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 @@ -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 -> @@ -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); @@ -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' @@ -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 @@ -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)) diff --git a/src/laurent.ml b/src/laurent.ml index a1bd3ff..d32f7de 100644 --- a/src/laurent.ml +++ b/src/laurent.ml @@ -1,5 +1,4 @@ open Tactics -open Inferer open Theorems open Suite diff --git a/src/tactics.ml b/src/tactics.ml index 04ab41a..c5b4f09 100644 --- a/src/tactics.ml +++ b/src/tactics.ml @@ -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 @@ -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 = @@ -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")) @@ -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 @@ -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")) @@ -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) -> @@ -148,7 +148,7 @@ 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), @@ -156,7 +156,7 @@ let apply_tactic env state tac = 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")) @@ -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")) @@ -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 -> @@ -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 diff --git a/src/theorems.ml b/src/theorems.ml index 3cf5a3e..a26da6e 100644 --- a/src/theorems.ml +++ b/src/theorems.ml @@ -1,5 +1,4 @@ open Inferer -open Suite open Tactics (* LAURENT MATHEMATICS 💡 *)