From 4c4bcdd3d52cd1d850389f45986825ac0d0c4324 Mon Sep 17 00:00:00 2001 From: PratherConid Date: Sat, 23 Nov 2024 17:57:34 -0800 Subject: [PATCH] update readme --- README.md | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index f3e69fa..89e851f 100644 --- a/README.md +++ b/README.md @@ -4,7 +4,17 @@ Lean-auto is an interface between Lean and automated theorem provers. Up to now, lean-auto is maintained and developed primarily by Yicheng Qian (GitHub: PratherConid). It is currently in active development, and pull requests/issues are welcome. For more information, feel free to reach out to Yicheng Qian on [Lean Zulip](https://leanprover.zulipchat.com). -Lean-auto is based on a monomorphization procedure from dependent type theory to higher-order logic and a deep embedding of higher-order logic into dependent type theory. It is capable of handling dependently-typed and/or universe-polymorphic input terms. Currently, proof reconstruction can be handled by [Duper](https://github.com/leanprover-community/duper), a higher-order superposition prover written in Lean. +Lean-auto is based on a monomorphization procedure from dependent type theory to higher-order logic and a deep embedding of higher-order logic into dependent type theory. It is capable of handling dependently-typed and/or universe-polymorphic input terms. Currently, proof reconstruction can be handled by [Duper](https://github.com/leanprover-community/duper), a higher-order superposition prover written in Lean. To enable Duper, please import the duper repo in your project, and set the following options: +```lean +open Lean Auto in +def Auto.duperRaw (lemmas : Array Lemma) (_ : Array Lemma) : MetaM Expr := do + let lemmas : Array (Expr × Expr × Array Name × Bool) ← lemmas.mapM + (fun ⟨⟨proof, ty, _⟩, _⟩ => do return (ty, ← Meta.mkAppM ``eq_true #[proof], #[], true)) + runDuper lemmas.data 0 + +attribute [rebind Auto.Native.solverFunc] Auto.duperRaw +set_option auto.native true +``` Although Lean-auto is still under development, it's already able to solve nontrivial problems. For example the first part of the "snake lemma" in category theory can be solved by a direct invocation to ``auto`` (and the second part can also be partly automated):