diff --git a/Auto/Embedding/LamBase.lean b/Auto/Embedding/LamBase.lean index c5ed023..1aa5ff9 100644 --- a/Auto/Embedding/LamBase.lean +++ b/Auto/Embedding/LamBase.lean @@ -2462,8 +2462,8 @@ theorem LamTerm.maxLooseBVarSucc.spec (m : Nat) : | .app _ t₁ t₂ => by dsimp [hasLooseBVarGe, maxLooseBVarSucc]; rw [Bool.or_eq_true]; rw [spec m t₁]; rw [spec m t₂]; - simp [Nat.max]; rw [Nat.gt_eq_succ_le, Nat.gt_eq_succ_le, Nat.gt_eq_succ_le]; - rw [Nat.le_max_iff] + simp [Nat.max] + omega def LamTerm.maxEVarSucc : LamTerm → Nat | .atom _ => 0 diff --git a/Auto/Embedding/LamBitVec.lean b/Auto/Embedding/LamBitVec.lean index 248e5a6..d664917 100644 --- a/Auto/Embedding/LamBitVec.lean +++ b/Auto/Embedding/LamBitVec.lean @@ -2,6 +2,7 @@ import Auto.Embedding.LamConv import Auto.Lib.NatExtra import Std.Data.Int.Lemmas import Std.Data.Fin.Lemmas +import Std.Data.BitVec.Lemmas namespace Auto.Embedding.Lam @@ -81,11 +82,8 @@ namespace BitVec theorem toNat_xor (a b : Std.BitVec n) : (a ^^^ b).toNat = a.toNat ^^^ b.toNat := rfl - theorem toNat_not_aux (a : Std.BitVec n) : (~~~a).toNat = (1 <<< n).pred ^^^ a.toNat := rfl - - theorem toNat_not (a : Std.BitVec n) : (~~~a).toNat = 2 ^ n - 1 - a.toNat := by - rw [toNat_not_aux]; rw [Nat.shiftLeft_eq, Nat.one_mul, ← Nat.sub_one, Nat.ones_xor] - rcases a with ⟨⟨_, isLt⟩⟩; exact isLt + theorem toNat_not (a : Std.BitVec n) : (~~~a).toNat = 2 ^ n - 1 - a.toNat := + Std.BitVec.toNat_not theorem shiftLeft_ge_length_eq_zero (a : Std.BitVec n) (i : Nat) : i ≥ n → a <<< i = 0#n := by intro h; apply eq_of_val_eq; rw [toNat_shiftLeft, toNat_ofNat]; apply Nat.mod_eq_zero_of_dvd @@ -94,12 +92,12 @@ namespace BitVec theorem ushiftRight_ge_length_eq_zero (a : Std.BitVec n) (i : Nat) : i ≥ n → a >>> i = 0#n := by intro h; apply eq_of_val_eq; rw [toNat_ushiftRight, toNat_ofNat] - apply (Nat.le_iff_div_eq_zero (Nat.pow_two_pos _)).mpr + apply (Nat.le_iff_div_eq_zero (Nat.two_pow_pos _)).mpr apply Nat.le_trans (toNat_le _) (Nat.pow_le_pow_of_le_right (.step .refl) h) theorem ushiftRight_ge_length_eq_zero' (a : Std.BitVec n) (i : Nat) : i ≥ n → (a.toNat >>> i)#n = 0#n := by intro h; apply congr_arg (@Std.BitVec.ofNat n) - rw [Nat.shiftRight_eq_div_pow, Nat.le_iff_div_eq_zero (Nat.pow_two_pos _)] + rw [Nat.shiftRight_eq_div_pow, Nat.le_iff_div_eq_zero (Nat.two_pow_pos _)] apply Nat.le_trans (toNat_le _) (Nat.pow_le_pow_of_le_right (.step .refl) h) theorem sshiftRight_ge_length_eq_msb (a : Std.BitVec n) (i : Nat) : i ≥ n → a.sshiftRight i = @@ -112,8 +110,8 @@ namespace BitVec rw [← Int.subNatNat_eq_coe, Int.subNatNat_of_lt (toNat_le _)] simp [Std.BitVec.toInt, Std.BitVec.ofInt] have hzero : Nat.pred (2 ^ n - Std.BitVec.toNat a) >>> i = 0 := by - rw [Nat.shiftRight_eq_div_pow]; apply (Nat.le_iff_div_eq_zero (Nat.pow_two_pos _)).mpr - rw [Nat.pred_lt_iff_le (Nat.pow_two_pos _)] + rw [Nat.shiftRight_eq_div_pow]; apply (Nat.le_iff_div_eq_zero (Nat.two_pow_pos _)).mpr + rw [Nat.pred_lt_iff_le (Nat.two_pow_pos _)] apply Nat.le_trans (Nat.sub_le _ _) (Nat.pow_le_pow_of_le_right (.step .refl) h) rw [hzero]; apply eq_of_val_eq; rw [toNat_not] rw [toNat_ofNat, toNat_neg, toNat_ofNat, Nat.zero_mod, Nat.sub_zero] @@ -130,9 +128,9 @@ namespace BitVec rw [Nat.zero_mod, Nat.shiftRight_eq_div_pow] apply Iff.intro <;> intro h case mp => - rw [← Nat.le_iff_div_eq_zero (Nat.pow_two_pos _)] + rw [← Nat.le_iff_div_eq_zero (Nat.two_pow_pos _)] exact h - case mpr => rw [(Nat.le_iff_div_eq_zero (Nat.pow_two_pos _)).mpr h] + case mpr => rw [(Nat.le_iff_div_eq_zero (Nat.two_pow_pos _)).mpr h] theorem ofNat_toNat (a : Std.BitVec n) : .ofNat m a.toNat = a.zeroExtend m := by apply eq_of_val_eq; rw [toNat_ofNat, toNat_zeroExtend] @@ -156,7 +154,7 @@ namespace BitVec rw [Nat.add_sub_cancel_left, Nat.mod_add_mod, Nat.add_assoc b c] rw [← Nat.mod_add_mod, ← Nat.add_assoc _ c, Nat.add_comm _ c, Nat.add_assoc c] rw [Nat.add_comm (b % _), Nat.sub_add_cancel, ← Nat.add_mod_mod, Nat.mod_self, Nat.add_zero] - apply Nat.le_of_lt (Nat.mod_lt _ (Nat.pow_two_pos _)) + apply Nat.le_of_lt (Nat.mod_lt _ (Nat.two_pow_pos _)) case true => have hle := of_decide_eq_true hdec rw [Bool.ite_eq_true _ _ _ hle, Nat.sub_eq_zero_of_le] @@ -786,7 +784,7 @@ theorem LamTerm.maxEVarSucc_pushBVCast : maxEVarSucc (pushBVCast ct t) = maxEVar cases bvc case bvtoNat m => dsimp [maxEVarSucc, pushBVCast] - cases hble : m.ble n <;> dsimp [maxEVarSucc] <;> rw [argeq₁, argeq₂] + cases m.ble n <;> dsimp [maxEVarSucc] <;> rw [argeq₁, argeq₂] simp [Nat.max, Nat.max_zero_left, Nat.max_zero_right, maxlem₁] all_goals apply h_none_shl all_goals apply h_none_shl @@ -813,7 +811,7 @@ theorem LamTerm.maxEVarSucc_pushBVCast : maxEVarSucc (pushBVCast ct t) = maxEVar cases bvc case bvtoNat m => dsimp [maxEVarSucc, pushBVCast] - cases hble : m.ble n <;> dsimp [maxEVarSucc] <;> rw [argeq₁, argeq₂] + cases m.ble n <;> dsimp [maxEVarSucc] <;> rw [argeq₁, argeq₂] simp [Nat.max, Nat.max_zero_left, Nat.max_zero_right, maxlem₁] all_goals apply h_none_lshr all_goals apply h_none_lshr @@ -840,7 +838,7 @@ theorem LamTerm.maxEVarSucc_pushBVCast : maxEVarSucc (pushBVCast ct t) = maxEVar cases bvc case bvtoNat m => dsimp [maxEVarSucc, pushBVCast] - cases hble : m.ble n <;> dsimp [maxEVarSucc] <;> rw [argeq₁, argeq₂] + cases m.ble n <;> dsimp [maxEVarSucc] <;> rw [argeq₁, argeq₂] simp [Nat.max, Nat.max_zero_left, Nat.max_zero_right, maxlem₂] all_goals apply h_none_ashr all_goals apply h_none_ashr diff --git a/Auto/Embedding/LamPrep.lean b/Auto/Embedding/LamPrep.lean index cb512f5..0b18da5 100644 --- a/Auto/Embedding/LamPrep.lean +++ b/Auto/Embedding/LamPrep.lean @@ -609,7 +609,7 @@ theorem LamEquiv.not_and_equiv_not_or_not? | .ofApp _ _ (.ofApp _ (.ofApp _ _ Hlhs) Hrhs) => exists (.mkNot (.mkAnd Hlhs Hrhs)), (.mkOr (.mkNot Hlhs) (.mkNot Hrhs)); intro lctxTerm apply GLift.down.inj; apply propext - apply @Decidable.not_and _ _ (Classical.propDecidable _) + apply Classical.not_and_iff_or_not_not theorem LamGenConv.not_and_equiv_not_or_not? : LamGenConv lval LamTerm.not_and_equiv_not_or_not? := by intro t₁ t₂ heq lctx rty wf @@ -739,7 +739,7 @@ theorem LamEquiv.not_imp_equiv_and_not? | .ofApp _ _ (.ofApp _ (.ofApp _ _ Hlhs) Hrhs) => exists .mkNot (.mkImp Hlhs Hrhs), (.mkAnd Hlhs (.mkNot Hrhs)); intro lctxTerm apply GLift.down.inj; apply propext - apply @Decidable.not_imp _ _ (Classical.propDecidable _) + apply Classical.not_imp_iff_and_not theorem LamGenConv.not_imp_equiv_and_not? : LamGenConv lval LamTerm.not_imp_equiv_and_not? := by intro t₁ t₂ heq lctx rty wf diff --git a/Auto/Parser/TPTP.lean b/Auto/Parser/TPTP.lean index a8a12ea..468b5e6 100644 --- a/Auto/Parser/TPTP.lean +++ b/Auto/Parser/TPTP.lean @@ -274,27 +274,28 @@ partial def addOpAndRhs (lhs : Term) (minbp : Nat) : ParserM Term := do return ← addOpAndRhs (Term.mk op [lhs, rhs]) minbp partial def parseTypeDecl : ParserM Term := do - if (← peek?) == some (.op "(") then - parseToken (.op "(") - let ident ← parseIdent - if (← peek?) == some (.op ":") then - parseToken (.op ":") - let ty ← parseTerm - parseToken (.op ")") - return Term.mk (.ident ident) [ty] - else - parseToken (.op ")") - return Term.mk (.ident ident) [] + let ident ← parseIdent + if (← peek?) == some (.op ":") then + parseToken (.op ":") + let ty ← parseTerm + return Term.mk (.ident ident) [ty] else - let ident ← parseIdent - if (← peek?) == some (.op ":") then - parseToken (.op ":") - let ty ← parseTerm - return Term.mk (.ident ident) [ty] - else - return Term.mk (.ident ident) [] + return Term.mk (.ident ident) [] end +/-- + + +-/ +partial def parseAtomTyping : ParserM Term := do + if (← peek?) == .some (.op "(") then + parseToken (.op "(") + let decl ← parseAtomTyping + parseToken (.op ")") + return decl + else + parseTypeDecl + structure Command where cmd : String args : List Term @@ -316,7 +317,7 @@ def parseCommand : ParserM Command := do let kind ← parseIdent parseToken (.op ",") let val ← match kind with - | "type" => parseTypeDecl + | "type" => parseAtomTyping | _ => parseTerm if (← peek?) == some (.op ",") then parseToken (.op ",") diff --git a/Auto/Translation/Inductive.lean b/Auto/Translation/Inductive.lean index 05eb1bc..b376a7f 100644 --- a/Auto/Translation/Inductive.lean +++ b/Auto/Translation/Inductive.lean @@ -112,7 +112,7 @@ mutual let .some (.inductInfo val) := (← getEnv).find? tyctor | return if !(← @id (CoreM _) (val.all.allM isSimpleInductive)) then - trace[auto.collectInd] ("Warning : {tyctor} or some type within the " ++ + trace[auto.collectInd] (m!"Warning : {tyctor} or some type within the " ++ "same mutual block is not a simple inductive type. Ignoring it ...") return /- diff --git a/Auto/Translation/Lam2D.lean b/Auto/Translation/Lam2D.lean index a4bd245..ba128ab 100644 --- a/Auto/Translation/Lam2D.lean +++ b/Auto/Translation/Lam2D.lean @@ -331,7 +331,7 @@ def withHyps (hyps : Array Expr) : ExternM (Array FVarId) := do return ret private def callNativeExternMAction - (nonempties : Array REntry) (valids : Array REntry) (prover : Array Lemma → MetaM Expr) : + (nonempties : Array REntry) (validsWithDTr : Array (REntry × DTr)) (prover : Array Lemma → MetaM Expr) : ExternM (Expr × LamTerm × Array Nat × Array REntry × Array REntry) := do let ss ← nonempties.mapM (fun re => do match re with @@ -341,6 +341,8 @@ private def callNativeExternMAction for inh in inhs do trace[auto.printInhs] "{inh}" let inhFVars ← withHyps inhs + let valids := validsWithDTr.map Prod.fst + let hypDTrs := validsWithDTr.map Prod.snd let ts ← valids.mapM (fun re => do match re with | .valid [] t => return t @@ -354,10 +356,8 @@ private def callNativeExternMAction trace[auto.printHyps] "{hyp}" let hyps ← runMetaM <| hyps.mapM (fun e => Core.betaReduce e) let hypFvars ← withHyps hyps - -- debug - -- **TODO: Specify origin** - let lemmas : Array Lemma := (hyps.zip hypFvars).map (fun (ty, proof) => - ⟨⟨.fvar proof, ty, .leaf "?callNativeExternMAction"⟩, #[]⟩) + let lemmas : Array Lemma := ((hyps.zip hypFvars).zip hypDTrs).map + (fun ((ty, proof), dtr) => ⟨⟨.fvar proof, ty, dtr⟩, #[]⟩) -- Note that we're not introducing bound variables into local context -- in the above action, so it's reasonable to use `runMetaM` let atomsToAbstract ← getAtomsToAbstract @@ -421,7 +421,9 @@ def callNative_checker let tyVal ← LamReif.getTyVal let varVal ← LamReif.getVarVal let lamEVarTy ← LamReif.getLamEVarTy - runAtMetaM' <| (callNativeExternMAction nonempties valids prover).run' + let validsWithDTr ← valids.mapM (fun re => + do return (re, ← collectDerivFor re)) + runAtMetaM' <| (callNativeExternMAction nonempties validsWithDTr prover).run' { tyVal := tyVal, varVal := varVal, lamEVarTy := lamEVarTy } /-- @@ -436,8 +438,10 @@ def callNative_direct let tyVal ← LamReif.getTyVal let varVal ← LamReif.getVarVal let lamEVarTy ← LamReif.getLamEVarTy + let validsWithDTr ← valids.mapM (fun re => + do return (re, ← collectDerivFor re)) let (proof, _, usedEtoms, usedInhs, usedHyps) ← runAtMetaM' <| - (callNativeExternMAction nonempties valids prover).run' + (callNativeExternMAction nonempties validsWithDTr prover).run' { tyVal := tyVal, varVal := varVal, lamEVarTy := lamEVarTy } if usedEtoms.size != 0 then throwError "callNative_direct :: etoms should not occur here" diff --git a/Auto/Translation/LamFOL2SMT.lean b/Auto/Translation/LamFOL2SMT.lean index 03e9479..382390a 100644 --- a/Auto/Translation/LamFOL2SMT.lean +++ b/Auto/Translation/LamFOL2SMT.lean @@ -297,7 +297,8 @@ def lamQuantified2STerm (forall? : Bool) (s : LamSort) (body : TransM LamAtom ST let dname ← disposableName let mut body' ← body if s == .base .nat then - body' := .qStrApp "=>" #[.qStrApp ">=" #[.bvar 0, .sConst (.num 0)], body'] + let connective := if forall? then "=>" else "and" + body' := .qStrApp connective #[.qStrApp ">=" #[.bvar 0, .sConst (.num 0)], body'] match forall? with | true => return .forallE dname s' body' | false => return .existE dname s' body' diff --git a/README.md b/README.md index b197eaf..c6083f7 100644 --- a/README.md +++ b/README.md @@ -73,7 +73,6 @@ Lean-auto is still under development, but it's already able to solve nontrivial * The checker is slow on large input. For example, it takes ```6s``` to typecheck the final example in ```BinderComplexity.lean```. However, this is probably acceptable for mathlib usages, because e.g ```Mathlib/Analysis/BoxIntegral/DivergenceTheorem.lean``` has two theorems that take ```4s``` to compile (but a large portion of the ```4s``` are spent on typeclass inference) ## Rules in Proof Tree -* `?`: Not specified, generated in function ``. This is for debug purpose only. * `defeq `: The ``-th definitional equality associated with definition `` * `hw `: Lemmas hard-wired into Lean-auto * `lctxInh`: Inhabitation fact from local context diff --git a/Test/LamEmbed.lean b/Test/LamEmbed.lean index 9053ac2..6088135 100644 --- a/Test/LamEmbed.lean +++ b/Test/LamEmbed.lean @@ -15,8 +15,9 @@ def manyArgFuncTy (n : Nat) (k : Nat) : LamSort := set_option maxRecDepth 4000 in set_option lazyReduce.logInfo false in #lazyReduce manyArgFuncTy 3000 0 + set_option maxRecDepth 2000 in -#reduce LamSort.beq_eq (manyArgFuncTy 100 40) (manyArgFuncTy 100 40) +#reduce @LamSort.eq_of_beq_eq_true (manyArgFuncTy 100 40) (manyArgFuncTy 100 40) -- λ (x₁ x₂ ... xₙ : (.atom 0)) . (.atom 0) x₁ x₂ ... xₙ -- Note that the first `.atom 0` is a type atom, while the @@ -76,6 +77,3 @@ set_option maxHeartbeats 20000000 in set_option lazyReduce.printTime true set_option maxRecDepth 50000 in #lazyReduce List.map (fun n => (List.range (1000 + n)).length) (List.range 10) - -set_option maxRecDepth 50000 in -#lazyReduce (List.range 10000).length \ No newline at end of file diff --git a/Test/SmtTranslation/BoolNatInt.lean b/Test/SmtTranslation/BoolNatInt.lean index 89f23f6..15c2e32 100644 --- a/Test/SmtTranslation/BoolNatInt.lean +++ b/Test/SmtTranslation/BoolNatInt.lean @@ -36,5 +36,3 @@ example {a b c d : Bool} (h : if (if (2 < 3) then a else b) then c else d) : (a → c) ∧ (¬ a → d) := by auto example {a : Bool} : decide a = a := by auto - -#check Lean.Elab.Command.elabStructure diff --git a/lake-manifest.json b/lake-manifest.json index 44ace39..f66cb9d 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -4,10 +4,10 @@ [{"url": "https://github.com/leanprover/std4.git", "type": "git", "subDir": null, - "rev": "276953b13323ca151939eafaaec9129bf7970306", + "rev": "f697bda1b4764a571042fed030690220c66ac4b2", "name": "std", "manifestFile": "lake-manifest.json", - "inputRev": "v4.6.0-rc1", + "inputRev": "main", "inherited": false, "configFile": "lakefile.lean"}], "name": "auto", diff --git a/lakefile.lean b/lakefile.lean index 2c25f75..2dea24a 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -7,7 +7,7 @@ package «auto» { } require std from git - "https://github.com/leanprover/std4.git"@"v4.6.0-rc1" + "https://github.com/leanprover/std4.git"@"main" @[default_target] lean_lib «Auto» {