Merge pull request #20 from leanprover-community/main

Merge updated DTr data structure so Duper can track isFromGoal information

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

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

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

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
 
+/--
+  <thf_atom_typing>
+  <tff_atom_typing>
+-/
+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 ",")

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
     /-

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"

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'

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
-* `?<name>`: Not specified, generated in function `<name>`. This is for debug purpose only.
 * `defeq <num> <name>`: The `<num>`-th definitional equality associated with definition `<name>`
 * `hw <name>`: Lemmas hard-wired into Lean-auto
 * `lctxInh`: Inhabitation fact from local context

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

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

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",

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» {