From 45259c0cbf9e6add428850a502ab8201bef4e581 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?George=20P=C3=AErlea?= Date: Mon, 24 Jun 2024 20:46:44 +0800 Subject: [PATCH] Bump toolchain to v4.8.0 --- Auto/Embedding/LCtx.lean | 15 ++++--- Auto/Embedding/LamBVarOp.lean | 14 +++---- Auto/Embedding/LamBase.lean | 23 +++++------ Auto/Embedding/LamBitVec.lean | 7 ++-- Auto/Embedding/LamChecker.lean | 2 +- Auto/Embedding/LamConv.lean | 4 +- Auto/Embedding/LamSystem.lean | 14 +++---- Auto/LemDB.lean | 4 +- Auto/Lib/AbstractMVars.lean | 4 +- Auto/Lib/BinTree.lean | 4 +- Auto/Lib/HList.lean | 10 ++--- Auto/Lib/Pos.lean | 5 ++- Auto/Solver/Native.lean | 2 +- Auto/Tactic.lean | 2 +- Auto/Translation/Lam2DAtomAsFVar.lean | 2 +- Auto/Translation/LamFOL2SMT.lean | 2 +- Auto/Translation/LamReif.lean | 16 ++++---- Auto/Translation/LamUtils.lean | 58 +++++++++++++-------------- lean-toolchain | 2 +- 19 files changed, 95 insertions(+), 95 deletions(-) diff --git a/Auto/Embedding/LCtx.lean b/Auto/Embedding/LCtx.lean index 39e2d3b..a4a187d 100644 --- a/Auto/Embedding/LCtx.lean +++ b/Auto/Embedding/LCtx.lean @@ -916,8 +916,10 @@ section add_nat def addAt_succ_l (lvl pos : Nat) (n : Nat) : addAt (.succ lvl) pos n = succAt pos (addAt lvl pos n) := by - dsimp [addAt, Nat.add_succ] - rw [mapAt_comp pos Nat.succ (fun x => x + lvl) n] + dsimp [addAt] + have heq: (fun x => x + (lvl + 1)) = (fun x => (x + lvl).succ) := by + apply funext; omega + rw [heq] ; apply mapAt_comp def addAt_succ_r (lvl pos : Nat) (n : Nat) : addAt (.succ lvl) pos n = addAt lvl pos (succAt pos n) := by @@ -1015,8 +1017,9 @@ section genericInst case cons x xs => simp at heq rw [← IH xs heq lctx n] - dsimp [pushLCtxs, Nat.blt, Nat.ble, Nat.add_succ] - rw [Nat.succ_sub_succ] + dsimp [pushLCtxs, Nat.blt, Nat.ble] + rw [Nat.add_succ, Nat.succ_sub_succ] + dsimp theorem contraPair.ofPushsPops (lvl : Nat) (xs : List α) (heq : xs.length = lvl) : contraPair (fun n => n + lvl) (fun lctx => List.ofFun lctx lvl = xs) (pushLCtxs xs) := by @@ -1039,8 +1042,8 @@ section genericInst case cons ty tys x xs => simp at heq apply HEq.trans _ (IH xs heq lctx n) - dsimp [Nat.blt, Nat.ble, Nat.add_succ] - rw [Nat.succ_sub_succ]; rfl) + dsimp [Nat.blt, Nat.ble] + rw [Nat.add_succ, Nat.succ_sub_succ]; rfl) theorem contraPairDep.ofPushsDepPopsDep {lctxty : α → Sort u} (lvl : Nat) {tys : List α} diff --git a/Auto/Embedding/LamBVarOp.lean b/Auto/Embedding/LamBVarOp.lean index fac3766..b9e277b 100644 --- a/Auto/Embedding/LamBVarOp.lean +++ b/Auto/Embedding/LamBVarOp.lean @@ -252,7 +252,7 @@ theorem LamTerm.bvarLifts_add : rw [Nat.add_comm]; induction lvl₁ case zero => rw [bvarLiftsIdx_zero]; rfl case succ lvl₁ IH => - rw [Nat.add_succ]; rw [bvarLiftsIdx_succ_r, bvarLiftsIdx_succ_r, IH] + rw [Nat.add_succ]; rw [bvarLiftsIdx_succ_r, bvarLiftsIdx_succ_r, IH] def LamWF.bvarLiftsIdx {lamVarTy lctx} {idx lvl : Nat} @@ -266,7 +266,7 @@ def LamWF.fromBVarLiftsIdx {xs : List LamSort} (heq : xs.length = lvl) (rterm : LamTerm) (HWF : LamWF lamVarTy ⟨pushLCtxsAt xs idx lctx, rterm.bvarLiftsIdx idx lvl, rTy⟩) : LamWF lamVarTy ⟨lctx, rterm, rTy⟩ := - LamWF.fromMapBVarAt (coPair.ofPushsPops _ _ heq) idx rterm HWF + LamWF.fromMapBVarAt (coPair.ofPushsPops _ _ heq) idx rterm HWF theorem LamWF.interp_bvarLiftsIdx (lval : LamValuation.{u}) {idx lvl : Nat} @@ -290,7 +290,7 @@ def LamWF.fromBVarLifts {xs : List LamSort} (heq : xs.length = lvl) (rterm : LamTerm) (HWF : LamWF lamVarTy ⟨pushLCtxs xs lctx, rterm.bvarLifts lvl, rTy⟩) : LamWF lamVarTy ⟨lctx, rterm, rTy⟩ := - LamWF.fromBVarLiftsIdx (idx:=0) heq rterm (Eq.mp (by rw [pushLCtxsAt_zero]) HWF) + LamWF.fromBVarLiftsIdx (idx:=0) heq rterm (Eq.mp (by rw [pushLCtxsAt_zero]) HWF) theorem LamWF.interp_bvarLifts (lval : LamValuation.{u}) {lvl : Nat} @@ -392,9 +392,9 @@ theorem LamTerm.bvarLowersIdx?_bvar_eq_some : cases h₂ : (idx + lvl).ble n <;> simp case false => have h₂' := Nat.lt_of_ble_eq_false h₂; clear h₂ - apply not_or.mpr (And.intro ?nlt ?nge) - case nlt => intro h; have h' := Nat.not_le_of_lt h.left; apply h' h₁' - case nge => intro h; have h' := Nat.not_le_of_lt h₂'; apply h' h.left + apply (And.intro ?nlt ?nge) + case nlt => intro h; have h' := Nat.not_le_of_lt h; contradiction + case nge => intro h; have h' := Nat.not_le_of_lt h₂'; contradiction case true => have h₂' := Nat.le_of_ble_eq_true h₂; clear h₂ apply Iff.intro <;> intro h @@ -535,4 +535,4 @@ def LamTerm.toString := LamTerm.toStringLCtx 0 instance : ToString LamTerm where toString := LamTerm.toString -end Auto.Embedding.Lam \ No newline at end of file +end Auto.Embedding.Lam diff --git a/Auto/Embedding/LamBase.lean b/Auto/Embedding/LamBase.lean index d4d6ffa..c64a7cc 100644 --- a/Auto/Embedding/LamBase.lean +++ b/Auto/Embedding/LamBase.lean @@ -2564,12 +2564,7 @@ theorem LamTerm.maxLooseBVarSucc.spec (m : Nat) : case mp => let IH' := Nat.pred_le_pred (IH.mp h) rw [Nat.pred_succ] at IH'; exact IH' - case mpr => - let h' := Nat.succ_le_succ h - apply IH.mpr; rw [Nat.succ_pred] at h'; exact h' - revert h; cases (maxLooseBVarSucc t) - case zero => intro h; cases h - case succ _ => intro _; simp + case mpr => apply IH.mpr; omega | .app _ t₁ t₂ => by dsimp [hasLooseBVarGe, maxLooseBVarSucc]; rw [Bool.or_eq_true]; rw [spec m t₁]; rw [spec m t₂]; @@ -2954,7 +2949,7 @@ theorem LamTerm.getLamBodyN_mkLamFN_length_eq cases l <;> cases h case refl s' l => dsimp [mkLamFN, getLamBodyN] - dsimp [Nat.add] at IH; apply IH; rfl + apply IH; rfl def LamTerm.getLamTysN (n : Nat) (t : LamTerm) : Option (List LamSort) := match n with @@ -3047,7 +3042,7 @@ theorem LamTerm.getAppArgsAux_eq : getAppArgsAux args t = getAppArgsAux [] t ++ dsimp [getAppArgsAux]; rw [IHFn (args:=(s, arg) :: args), IHFn (args:=[(s, arg)])] rw [List.append_assoc]; rfl -theorem LamTerm.maxEVarSucc_getAppArgsAux +noncomputable def LamTerm.maxEVarSucc_getAppArgsAux (hs : HList (fun (_, arg) => arg.maxEVarSucc ≤ n) args) (ht : t.maxEVarSucc ≤ n) : HList (fun (_, arg) => arg.maxEVarSucc ≤ n) (LamTerm.getAppArgsAux args t) := by induction t generalizing args <;> try exact hs @@ -3060,7 +3055,7 @@ def LamTerm.getAppArgs := getAppArgsAux [] theorem LamTerm.getAppArgs_app : getAppArgs (.app s fn arg) = getAppArgs fn ++ [(s, arg)] := by dsimp [getAppArgs, getAppArgsAux]; rw [getAppArgsAux_eq] -theorem LamTerm.maxEVarSucc_getAppArgs : +noncomputable def LamTerm.maxEVarSucc_getAppArgs : HList (fun (_, arg) => arg.maxEVarSucc ≤ t.maxEVarSucc) (LamTerm.getAppArgs t) := LamTerm.maxEVarSucc_getAppArgsAux .nil (Nat.le_refl _) @@ -3117,7 +3112,7 @@ theorem LamTerm.getAppArgsNAux_eq : getAppArgsNAux n args t = (getAppArgsNAux n cases getAppArgsNAux n [] fn <;> dsimp rw [List.append_assoc]; rfl -theorem LamTerm.maxEVarSucc_getAppArgsNAux +def LamTerm.maxEVarSucc_getAppArgsNAux (hs : HList (fun (_, arg) => arg.maxEVarSucc ≤ m) args) (ht : t.maxEVarSucc ≤ m) (heq : LamTerm.getAppArgsNAux n args t = .some args') : HList (fun (_, arg) => arg.maxEVarSucc ≤ m) args' := by @@ -3131,7 +3126,7 @@ theorem LamTerm.maxEVarSucc_getAppArgsNAux def LamTerm.getAppArgsN n := getAppArgsNAux n [] -theorem LamTerm.maxEVarSucc_getAppArgsN +def LamTerm.maxEVarSucc_getAppArgsN (heq : LamTerm.getAppArgsN n t = .some l) : HList (fun (_, arg) => arg.maxEVarSucc ≤ t.maxEVarSucc) l := LamTerm.maxEVarSucc_getAppArgsNAux .nil (Nat.le_refl _) heq @@ -3193,7 +3188,7 @@ theorem LamTerm.getAppFnN_bvarAppsRev_length_eq cases l <;> cases heq case refl s' l => rw [getAppFnN_succ']; dsimp [bvarAppsRev] - dsimp [Nat.add] at IH; rw [IH rfl]; rfl + rw [IH rfl]; rfl def LamTerm.getForallEFBody (t : LamTerm) : LamTerm := match t with @@ -3919,7 +3914,7 @@ def LamWF.ofLamCheck? {ltv : LamTyVal} : | .some (LamSort.base _), _ => intro contra; cases contra | .none, _ => intro contra; cases contra -theorem LamWF.ofNonemptyLamWF (H : Nonempty (LamWF ltv ⟨lctx, t, s⟩)) : +def LamWF.ofNonemptyLamWF (H : Nonempty (LamWF ltv ⟨lctx, t, s⟩)) : LamWF ltv ⟨lctx, t, s⟩ := by cases h₁ : LamTerm.lamCheck? ltv lctx t case none => @@ -4124,7 +4119,7 @@ theorem LamWF.interp_eqForallEFN' case nil => dsimp [mkForallEFN, interp] conv => - enter [2]; rw [IsomType.eqForall HList.nil_IsomType.{u + 1, u + 1, 0}] + enter [2]; rw [IsomType.eqForall HList.nil_IsomType.{0, u + 1, u + 1}] rw [PUnit.eqForall]; unfold HList.nil_IsomType; dsimp dsimp [pushLCtxs, pushLCtxsDep, Nat.blt, Nat.ble] apply congrArg; apply interp_substWF diff --git a/Auto/Embedding/LamBitVec.lean b/Auto/Embedding/LamBitVec.lean index 52f3871..f3ccdfe 100644 --- a/Auto/Embedding/LamBitVec.lean +++ b/Auto/Embedding/LamBitVec.lean @@ -125,12 +125,13 @@ namespace BVLems case true => rw [← Int.subNatNat_eq_coe, Int.subNatNat_of_lt (toNat_le _)] simp [BitVec.toInt, BitVec.ofInt] - have hzero : Nat.pred (2 ^ n - BitVec.toNat a) >>> i = 0 := by + have hzero : (2 ^ n - BitVec.toNat a - 1) >>> i = 0 := by 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 _)] + rw [Nat.sub_one, 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) apply eq_of_val_eq; rw [toNat_ofNatLt, hzero] - rw [toNat_neg, Int.mod_def', Int.emod]; dsimp; rw [Nat.zero_mod] + rw [toNat_neg, Int.mod_def', Int.emod]; dsimp only; rw [Nat.zero_mod] + dsimp only [Int.natAbs_ofNat, Nat.succ_eq_add_one, Nat.reduceAdd] rw [Int.subNatNat_of_sub_eq_zero ((Nat.sub_eq_zero_iff_le).mpr (Nat.two_pow_pos _))] rw [Int.toNat_ofNat, BitVec.toNat_ofNat] cases n <;> try rfl diff --git a/Auto/Embedding/LamChecker.lean b/Auto/Embedding/LamChecker.lean index 60446c6..acf6654 100644 --- a/Auto/Embedding/LamChecker.lean +++ b/Auto/Embedding/LamChecker.lean @@ -362,7 +362,7 @@ def RTable.getValidsEnsureLCtx (r : RTable) (lctx : List LamSort) (vs : List Nat | .some (.nonempty _) => .none | .none => .none -theorem RTable.getValidsEnsureLCtx_correct +noncomputable def RTable.getValidsEnsureLCtx_correct (inv : RTable.inv r cv) (heq : getValidsEnsureLCtx r lctx vs = .some ts) : HList (fun t => LamThmValid cv.toLamValuation lctx t ∧ t.maxEVarSucc ≤ r.maxEVarSucc) ts := by induction vs generalizing ts diff --git a/Auto/Embedding/LamConv.lean b/Auto/Embedding/LamConv.lean index a2a9767..a03dd6b 100644 --- a/Auto/Embedding/LamConv.lean +++ b/Auto/Embedding/LamConv.lean @@ -152,7 +152,7 @@ theorem LamTerm.maxEVarSucc_etaExpandN? (heq : etaExpandN? n s t = .some t') : dsimp [etaExpandN?] at heq; cases h : s.getArgTysN n <;> rw [h] at heq <;> cases heq case refl l => rw [maxEVarSucc_etaExpandWith] -theorem LamWF.etaExpandN? +def LamWF.etaExpandN? (heq : LamTerm.etaExpandN? n s t = .some t') (wft : LamWF ltv ⟨lctx, t, s⟩) : LamWF ltv ⟨lctx, t', s⟩ := by dsimp [LamTerm.etaExpandN?] at heq; cases h₁ : s.getArgTysN n <;> rw [h₁] at heq <;> cases heq @@ -164,7 +164,7 @@ theorem LamWF.etaExpandN? conv => arg 2; rw [seq] apply LamWF.etaExpandWith; rw [← seq]; exact wft -theorem LamWF.fromEtaExpandN? +def LamWF.fromEtaExpandN? (heq : LamTerm.etaExpandN? n s t = .some t') (wfEx : LamWF ltv ⟨lctx, t', s⟩) : LamWF ltv ⟨lctx, t, s⟩ := by dsimp [LamTerm.etaExpandN?] at heq; cases h₁ : s.getArgTysN n <;> rw [h₁] at heq <;> cases heq diff --git a/Auto/Embedding/LamSystem.lean b/Auto/Embedding/LamSystem.lean index 715369a..7cfeb13 100644 --- a/Auto/Embedding/LamSystem.lean +++ b/Auto/Embedding/LamSystem.lean @@ -266,11 +266,11 @@ theorem LamValid_substLCtxRecWF GLift.down (LamWF.interp (t:=t) (rty:=.base .prop) lval lctx' lctxTerm' ((@id (lctx' = lctx) (funext heq)) ▸ wf))) := by cases (@id (lctx' = lctx) (funext heq)); exact Iff.intro id id -theorem LamWF.ofExistsLamWF (H : ∃ (_ : LamWF ltv ⟨lctx, t, s⟩), p) : +def LamWF.ofExistsLamWF (H : ∃ (_ : LamWF ltv ⟨lctx, t, s⟩), p) : LamWF ltv ⟨lctx, t, s⟩ := by apply LamWF.ofNonemptyLamWF; cases H; apply Nonempty.intro; assumption -theorem LamThmWF.ofLamThmWFP (H : LamThmWFP lval lctx s t) : +def LamThmWF.ofLamThmWFP (H : LamThmWFP lval lctx s t) : LamThmWF lval lctx s t := by intro lctx'; apply LamWF.ofNonemptyLamWF (H lctx') @@ -298,7 +298,7 @@ theorem LamTerm.lamThmWFCheck?_spec | false => intro H; cases H | .none => intro H; cases H -theorem LamThmWF.ofLamThmWFCheck? +def LamThmWF.ofLamThmWFCheck? {lctx : List LamSort} {rty : LamSort} {t : LamTerm} (h : LamTerm.lamThmWFCheck? lval.toLamTyVal lctx t = .some rty) : LamThmWF lval lctx rty t := by revert h; dsimp [LamTerm.lamThmWFCheck?] @@ -317,7 +317,7 @@ theorem LamThmWF.ofLamThmWFCheck? | false => intro h; cases h | .none => intro h; cases h -theorem LamThmWF.ofLamThmValid (H : LamThmValid lval lctx t) : +def LamThmWF.ofLamThmValid (H : LamThmValid lval lctx t) : LamThmWF lval lctx (.base .prop) t := LamThmWF.ofLamThmWFP (fun lctx => let ⟨wf, _⟩ := H lctx; Nonempty.intro wf) @@ -359,7 +359,7 @@ theorem LamThmValid.maxLooseBVarSucc (H : LamThmValid lval lctx t) : theorem LamThmWFD.ofLamThmWF (H : LamThmWF lval lctx rty t) : LamThmWFD lval lctx rty t := by exists (H dfLCtxTy); apply LamThmWF.maxLooseBVarSucc H -theorem LamThmWF.ofLamThmWFD (H : LamThmWFD lval lctx rty t) : LamThmWF lval lctx rty t := by +def LamThmWF.ofLamThmWFD (H : LamThmWFD lval lctx rty t) : LamThmWF lval lctx rty t := by apply LamThmWF.ofLamThmWFP; have ⟨H, hSucc⟩ := H; apply LamThmWFP.ofLamThmWF intro lctx'; apply LamWF.lctxIrrelevance _ H; intros n hlt dsimp [pushLCtxs]; @@ -439,11 +439,11 @@ theorem LamThmValid.eVarIrrelevance hLamVarTy hLamILTy hTyVal hVarVal hILVal (by rw [hLCtxTy]) hirr (h lctx') -theorem LamThmWF.ofLamThmEquiv_l (teq : LamThmEquiv lval lctx rty t₁ t₂) : +def LamThmWF.ofLamThmEquiv_l (teq : LamThmEquiv lval lctx rty t₁ t₂) : LamThmWF lval lctx rty t₁ := LamThmWF.ofLamThmWFP (fun lctx' => (let ⟨wf, _⟩ := teq lctx'; ⟨wf⟩)) -theorem LamThmWF.ofLamThmEquiv_r (teq : LamThmEquiv lval lctx rty t₁ t₂) : +def LamThmWF.ofLamThmEquiv_r (teq : LamThmEquiv lval lctx rty t₁ t₂) : LamThmWF lval lctx rty t₂ := LamThmWF.ofLamThmWFP (fun lctx' => (let ⟨_, ⟨wf, _⟩⟩ := teq lctx'; ⟨wf⟩)) diff --git a/Auto/LemDB.lean b/Auto/LemDB.lean index c4bfb0b..6fb183b 100644 --- a/Auto/LemDB.lean +++ b/Auto/LemDB.lean @@ -47,8 +47,8 @@ partial def LemDB.toHashSet : LemDB → AttrM (HashSet Name) ret := ret.insertMany hset return ret -private def throwUndeclaredLemDB (dbname action : Name) : AttrM α := do - let cmdstr := "#declare_lemdb " ++ dbname +private def throwUndeclaredLemDB (dbname : Name) (action : String) : AttrM α := do + let cmdstr := "#declare_lemdb " ++ dbname.toString throwError ("Please declare lemma database using " ++ s!"command {repr cmdstr} before {action}") diff --git a/Auto/Lib/AbstractMVars.lean b/Auto/Lib/AbstractMVars.lean index 3689e6a..0e5a3e6 100644 --- a/Auto/Lib/AbstractMVars.lean +++ b/Auto/Lib/AbstractMVars.lean @@ -98,7 +98,7 @@ partial def abstractExprMVars (e : Expr) : M Expr := do let type ← abstractExprMVars decl.type let fvarId ← mkFreshFVarId let fvar := mkFVar fvarId; - let userName := if decl.userName.isAnonymous then (`x).appendIndexAfter (← get).fvars.size else decl.userName + let userName ← if decl.userName.isAnonymous then pure <| (`x).appendIndexAfter (← get).fvars.size else pure decl.userName modify fun s => { s with emap := s.emap.insert mvarId fvar, @@ -180,4 +180,4 @@ def abstractMVarsLambda (e : Expr) : MetaM AbstractMVarsResult := do setNGen s.ngen setMCtx s.mctx let e := s.lctx.mkLambda s.fvars e - pure { paramNames := s.paramNames, numMVars := s.fvars.size, expr := e } \ No newline at end of file + pure { paramNames := s.paramNames, numMVars := s.fvars.size, expr := e } diff --git a/Auto/Lib/BinTree.lean b/Auto/Lib/BinTree.lean index 8b2e887..fcf0d87 100644 --- a/Auto/Lib/BinTree.lean +++ b/Auto/Lib/BinTree.lean @@ -26,7 +26,7 @@ private theorem wfAux (n n' : Nat) : n = n' + 2 → n / 2 < n := by apply Nat.succ_le_succ; apply Nat.zero_le case hLtK => apply Nat.le_refl -theorem inductionOn.{u} +def inductionOn.{u} {motive : Nat → Sort u} (x : Nat) (ind : ∀ x, motive ((x + 2) / 2) → motive (x + 2)) (base₀ : motive 0) (base₁ : motive 1) : motive x := @@ -36,7 +36,7 @@ theorem inductionOn.{u} | x' + 2 => ind x' (inductionOn ((x' + 2) / 2) ind base₀ base₁) decreasing_by apply wfAux; rfl -theorem induction.{u} +def induction.{u} {motive : Nat → Sort u} (ind : ∀ x, motive ((x + 2) / 2) → motive (x + 2)) (base₀ : motive 0) (base₁ : motive 1) : ∀ x, motive x := diff --git a/Auto/Lib/HList.lean b/Auto/Lib/HList.lean index 5c60ce8..6c2b97d 100644 --- a/Auto/Lib/HList.lean +++ b/Auto/Lib/HList.lean @@ -7,16 +7,16 @@ inductive HList (β : α → Sort _) : List α → Sort _ | nil : HList β .nil | cons : (x : β ty) → HList β tys → HList β (ty :: tys) -theorem HList.nil_IsomType : IsomType (HList β .nil) PUnit := +def HList.nil_IsomType : IsomType (HList β .nil) PUnit := ⟨fun _ => .unit, fun _ => .nil, fun x => match x with | .nil => rfl, fun _ => rfl⟩ -theorem HList.cons_IsomType : IsomType (HList β (a :: as)) (β a × HList β as) := +def HList.cons_IsomType : IsomType (HList β (a :: as)) (β a × HList β as) := ⟨fun xs => match xs with | .cons x xs => (x, xs), fun (x, xs) => .cons x xs, fun xs => match xs with | .cons _ _ => rfl, fun (_, _) => rfl⟩ -theorem HList.singleton_IsomType : IsomType (HList β [a]) (β a) := +def HList.singleton_IsomType : IsomType (HList β [a]) (β a) := ⟨fun xs => match xs with | .cons x .nil => x, fun x => .cons x .nil, fun xs => match xs with | .cons _ .nil => rfl, @@ -129,14 +129,14 @@ theorem HList.append_get_append_eq (xs : HList β (as ++ bs)) : cases xs; case cons x xs => dsimp [append_get_left, append_get_right, append]; rw [IH] -theorem HList.append_IsomType {α : Type u} {β : α → Sort v} {xs ys : List α} : +def HList.append_IsomType {α : Type u} {β : α → Sort v} {xs ys : List α} : IsomType (HList β (xs ++ ys)) (PProd (HList β xs) (HList β ys)) := ⟨fun l => ⟨l.append_get_left, l.append_get_right⟩, fun ⟨l₁, l₂⟩ => HList.append l₁ l₂, HList.append_get_append_eq, fun ⟨l₁, l₂⟩ => by dsimp; congr; rw [append_get_left_eq]; rw [append_get_right_eq]⟩ -theorem HList.append_singleton_IsomType {α : Type u} {β : α → Sort v} {xs : List α} {x : α} : +def HList.append_singleton_IsomType {α : Type u} {β : α → Sort v} {xs : List α} {x : α} : IsomType (HList β (xs ++ [x])) (PProd (HList β xs) (β x)) := ⟨fun l => ⟨l.append_get_left, match l.append_get_right with | .cons x .nil => x⟩, fun ⟨l, e⟩ => HList.append l (.cons e .nil), diff --git a/Auto/Lib/Pos.lean b/Auto/Lib/Pos.lean index 8d18437..92e049f 100644 --- a/Auto/Lib/Pos.lean +++ b/Auto/Lib/Pos.lean @@ -49,7 +49,7 @@ def ofNat'WF (n : Nat) := | _ => .xI (ofNat'WF (n / 2)) decreasing_by rw [← h]; apply ofNat'WFAux; assumption -theorem ofNat'WF.inductionOn.{u} +def ofNat'WF.inductionOn.{u} {motive : Nat → Sort u} (x : Nat) (ind : ∀ x, motive ((x + 2) / 2) → motive (x + 2)) (base₀ : motive 0) (base₁ : motive 1) : motive x := @@ -59,7 +59,7 @@ theorem ofNat'WF.inductionOn.{u} | x' + 2 => ind x' (inductionOn ((x' + 2) / 2) ind base₀ base₁) decreasing_by apply ofNat'WFAux; rfl -theorem ofNat'WF.induction +def ofNat'WF.induction {motive : Nat → Sort u} (ind : ∀ x, motive ((x + 2) / 2) → motive (x + 2)) (base₀ : motive 0) (base₁ : motive 1) : ∀ x, motive x := @@ -100,6 +100,7 @@ theorem ofNat'WF.doubleSucc_xI (n : Nat) : have heq' : Nat.succ ((2 * n' + 3) / 2) = n' + 2 := by apply congrArg; rw [Nat.add_comm]; rw [Nat.add_mul_div_left _ _ (by simp)]; rw [Nat.add_comm] + simp only [Nat.succ_eq_add_one] at heq' rw [heq'] theorem ofNat'WF_toNat' (p : Pos) : ofNat'WF (toNat' p) = p := by diff --git a/Auto/Solver/Native.lean b/Auto/Solver/Native.lean index 2c2cfd9..7fe2c15 100644 --- a/Auto/Solver/Native.lean +++ b/Auto/Solver/Native.lean @@ -38,7 +38,7 @@ def emulateNative (lemmas : Array Lemma) : MetaM Expr := do let _ ← lemmas.mapM (fun lem => do if lem.params.size != 0 then throwError "Solver.emulateNative :: Universe levels parameters are not supported") - let descrs := lemmas.zipWithIndex.map (fun (lem, i) => (s!"lem{i}", lem.type, .default)) + let descrs := lemmas.zipWithIndex.map (fun (lem, i) => (Name.mkSimple s!"lem{i}", lem.type, .default)) let sty := Expr.mkForallFromBinderDescrs descrs (.const ``False []) let sorryExpr := Lean.mkApp2 (.const ``sorryAx [.zero]) sty (.const ``Bool.false []) return Lean.mkAppN sorryExpr (lemmas.map (fun lem => lem.proof)) diff --git a/Auto/Tactic.lean b/Auto/Tactic.lean index 9dcac6e..cf5cb70 100644 --- a/Auto/Tactic.lean +++ b/Auto/Tactic.lean @@ -133,7 +133,7 @@ def parseUOrDs (stxs : Array (TSyntax ``uord)) : TacticM (Array Prep.ConstUnfold def collectLctxLemmas (lctxhyps : Bool) (ngoalAndBinders : Array FVarId) : TacticM (Array Lemma) := Meta.withNewMCtxDepth do - let fVarIds := (if lctxhyps then (← getLCtx).getFVarIds else ngoalAndBinders) + let fVarIds ← if lctxhyps then pure <| (← getLCtx).getFVarIds else pure ngoalAndBinders let mut lemmas := #[] for fVarId in fVarIds do let decl ← FVarId.getDecl fVarId diff --git a/Auto/Translation/Lam2DAtomAsFVar.lean b/Auto/Translation/Lam2DAtomAsFVar.lean index a77c22c..9c6f9b6 100644 --- a/Auto/Translation/Lam2DAtomAsFVar.lean +++ b/Auto/Translation/Lam2DAtomAsFVar.lean @@ -128,7 +128,7 @@ def withTranslatedLamTerms (ts : Array LamTerm) : ExternM (Array Expr) := do def withHyps (hyps : Array Expr) : ExternM (Array FVarId) := do let mut ret := #[] for hyp in hyps do - let name := "_exHyp" ++ (← mkFreshId).toString + let name := Name.mkSimple $ "_exHyp" ++ (← mkFreshId).toString let newFVarId ← withLocalDecl name .default hyp .default ret := ret.push newFVarId return ret diff --git a/Auto/Translation/LamFOL2SMT.lean b/Auto/Translation/LamFOL2SMT.lean index e444913..aed845d 100644 --- a/Auto/Translation/LamFOL2SMT.lean +++ b/Auto/Translation/LamFOL2SMT.lean @@ -536,7 +536,7 @@ def withExprValuation let .some s := sni.lamEVarTy[n]? | throwError "SMT.printValuation :: Unknown etom {n}" let type ← Lam2D.interpLamSortAsUnlifted tyValMap s - return ((name : Name), .default, fun _ => pure type)) + return (Name.mkSimple name , .default, fun _ => pure type)) Meta.withLocalDecls declInfos (fun etomFVars => do let etomValMap := HashMap.ofList ((etomsWithName.zip etomFVars).map (fun ((n, _), e) => (n, e))).data printFn tyValMap varValMap etomValMap) diff --git a/Auto/Translation/LamReif.lean b/Auto/Translation/LamReif.lean index b89d179..50ebd9f 100644 --- a/Auto/Translation/LamReif.lean +++ b/Auto/Translation/LamReif.lean @@ -1581,7 +1581,7 @@ section BuildChecker -- Given a list of expression of type `ty`, construct the corresponding `BinTree` private def exprListToBinTree (l : List Expr) (lvl : Level) (ty : Expr) := - (@instToExprBinTree Expr (instExprToExprId ty) ⟨lvl, Prop⟩).toExpr (BinTree.ofListGet l) + (@instToExprBinTreeOfToLevel Expr (instExprToExprId ty) ⟨lvl, Prop⟩).toExpr (BinTree.ofListGet l) -- Given a list of expression of type `ty`, construct the corresponding `lctx` private def exprListToLCtx (l : List Expr) (lvl : Level) (ty : Expr) := @@ -1663,7 +1663,7 @@ section BuildChecker importedFactsTree := importedFactsTree.insert n vEntry let type := Lean.mkApp2 (.const ``PSigma [.succ .zero, .zero]) (.const ``ImportEntry []) (.app (.const ``importTablePSigmaβ [u]) chkValExpr) - let importTableExpr := (@instToExprBinTree Expr + let importTableExpr := (@instToExprBinTreeOfToLevel Expr (instExprToExprId type) ⟨.zero, Prop⟩).toExpr importTable let importedFacts := Lean.toExpr importedFactsTree return (importTableExpr, importedFacts) @@ -1747,23 +1747,23 @@ section BuildChecker let runResultExpr := Lean.mkApp3 (.const ``RTable.mk []) (Lean.toExpr (← getRTableTree)) (Lean.toExpr (← getMaxEVarSucc)) (Lean.toExpr (← getLamEVarTyTree)) - mkNativeAuxDecl "lam_ssrefl_rr" (Lean.mkConst ``RTable) runResultExpr + mkNativeAuxDecl `lam_ssrefl_rr (Lean.mkConst ``RTable) runResultExpr def buildFullCheckerExprFor_indirectReduce_reflection (re : REntry) : ReifM Expr := do printCheckerStats let startTime ← IO.monoMsNow let u ← getU let lvtExpr := Lean.toExpr (BinTree.ofListGet ((← getVarVal).map Prod.snd).data) - let lvtNativeName ← mkNativeAuxDecl "lam_ssrefl_lvt" (Expr.app (.const ``BinTree [.zero]) (Lean.mkConst ``LamSort)) lvtExpr + let lvtNativeName ← mkNativeAuxDecl `lam_ssrefl_lvt (Expr.app (.const ``BinTree [.zero]) (Lean.mkConst ``LamSort)) lvtExpr let litExpr := Lean.toExpr (BinTree.ofListGet (← getLamILTy).data) - let litNativeName ← mkNativeAuxDecl "lam_ssrefl_lit" (Expr.app (.const ``BinTree [.zero]) (Lean.mkConst ``LamSort)) litExpr + let litNativeName ← mkNativeAuxDecl `lam_ssrefl_lit (Expr.app (.const ``BinTree [.zero]) (Lean.mkConst ``LamSort)) litExpr let cpvExpr ← buildCPValExpr let cpvTy := Expr.const ``CPVal [u] let checker ← Meta.withLetDecl `cpval cpvTy cpvExpr fun cpvFVarExpr => do let (itExpr, ifExpr) ← buildImportTableExpr cpvFVarExpr - let ifNativeName ← mkNativeAuxDecl "lam_ssrefl_if" (Expr.app (.const ``BinTree [.zero]) (Lean.mkConst ``REntry)) ifExpr + let ifNativeName ← mkNativeAuxDecl `lam_ssrefl_if (Expr.app (.const ``BinTree [.zero]) (Lean.mkConst ``REntry)) ifExpr let csExpr ← buildChkStepsExpr - let csNativeName ← mkNativeAuxDecl "lam_ssrefl_cs" (Lean.mkConst ``ChkSteps) csExpr + let csNativeName ← mkNativeAuxDecl `lam_ssrefl_cs (Lean.mkConst ``ChkSteps) csExpr let .valid lctx t := re | throwError "buildFullCheckerExprFor :: {re} is not a `valid` entry" let vExpr := Lean.toExpr (← lookupREntryPos! re) @@ -1773,7 +1773,7 @@ section BuildChecker let heqBoolExpr := Lean.mkApp7 (.const ``Checker.getValidExport_indirectReduce_reflection_runEq []) (Lean.mkConst lvtNativeName) (Lean.mkConst litNativeName) (Lean.mkConst ifNativeName) (Lean.mkConst csNativeName) vExpr (Lean.toExpr lctx) (Lean.toExpr t) - let heqNativeName ← mkNativeAuxDecl "lam_ssrefl_hEq" (Lean.mkConst ``Bool) heqBoolExpr + let heqNativeName ← mkNativeAuxDecl `lam_ssrefl_hEq (Lean.mkConst ``Bool) heqBoolExpr let heqRflPrf ← Meta.mkEqRefl (toExpr true) let heqExpr := mkApp3 (Lean.mkConst ``Lean.ofReduceBool) (Lean.mkConst heqNativeName) (toExpr true) heqRflPrf let getEntry := Lean.mkAppN (.const ``Checker.getValidExport_indirectReduce_reflection [u]) diff --git a/Auto/Translation/LamUtils.lean b/Auto/Translation/LamUtils.lean index b3ee072..03439eb 100644 --- a/Auto/Translation/LamUtils.lean +++ b/Auto/Translation/LamUtils.lean @@ -408,13 +408,13 @@ namespace Lam2D (mkApp2 (mkConst ``instHMul [.zero]) natc (mkConst ``instMulNat))), (``Nat.div, mkApp4 (.const ``HDiv.hDiv [.zero, .zero, .zero]) natc natc natc - (mkApp2 (mkConst ``instHDiv [.zero]) natc (mkConst ``Nat.instDivNat))), + (mkApp2 (mkConst ``instHDiv [.zero]) natc (mkConst ``Nat.instDiv))), (``Nat.mod, mkApp4 (.const ``HMod.hMod [.zero, .zero, .zero]) natc natc natc - (mkApp2 (mkConst ``instHMod [.zero]) natc (mkConst ``Nat.instModNat))), + (mkApp2 (mkConst ``instHMod [.zero]) natc (mkConst ``Nat.instMod))), (``Nat.le, mkApp2 (.const ``LE.le [.zero]) natc (mkConst ``instLENat)), (``Nat.lt, mkApp2 (.const ``LT.lt [.zero]) natc (mkConst ``instLTNat)), - (``Nat.max, mkApp2 (.const ``Max.max [.zero]) natc (mkConst ``Nat.instMaxNat)), + (``Nat.max, mkApp2 (.const ``Max.max [.zero]) natc (mkConst ``Nat.instMax)), (``Nat.min, mkApp2 (.const ``Min.min [.zero]) natc (mkConst ``instMinNat)) ] @@ -427,23 +427,23 @@ namespace Lam2D (``Int.neg , mkApp2 (.const ``Neg.neg [.zero]) intc (mkConst ``Int.instNegInt)), (``Int.add , mkApp4 (.const ``HAdd.hAdd [.zero, .zero, .zero]) intc intc intc - (mkApp2 (.const ``instHAdd [.zero]) intc (mkConst ``Int.instAddInt))), + (mkApp2 (.const ``instHAdd [.zero]) intc (mkConst ``Int.instAdd))), (``Int.sub , mkApp4 (.const ``HSub.hSub [.zero, .zero, .zero]) intc intc intc - (mkApp2 (.const ``instHSub [.zero]) intc (mkConst ``Int.instSubInt))), + (mkApp2 (.const ``instHSub [.zero]) intc (mkConst ``Int.instSub))), (``Int.mul , mkApp4 (.const ``HMul.hMul [.zero, .zero, .zero]) intc intc intc - (mkApp2 (.const ``instHMul [.zero]) intc (mkConst ``Int.instMulInt))), + (mkApp2 (.const ``instHMul [.zero]) intc (mkConst ``Int.instMul))), (``Int.ediv , mkApp4 (.const ``HDiv.hDiv [.zero, .zero, .zero]) intc intc intc - (mkApp2 (.const ``instHDiv [.zero]) intc (mkConst ``Int.instDivInt))), + (mkApp2 (.const ``instHDiv [.zero]) intc (mkConst ``Int.instDiv))), (``Int.emod , mkApp4 (.const ``HMod.hMod [.zero, .zero, .zero]) intc intc intc - (mkApp2 (.const ``instHMod [.zero]) intc (mkConst ``Int.instModInt))), + (mkApp2 (.const ``instHMod [.zero]) intc (mkConst ``Int.instMod))), (``Int.le , mkApp2 (.const ``LE.le [.zero]) intc (mkConst ``Int.instLEInt)), (``Int.lt , mkApp2 (.const ``LT.lt [.zero]) intc (mkConst ``Int.instLTInt)), - (``Int.max , mkApp2 (.const ``Max.max [.zero]) intc (mkConst ``Int.instMaxInt)), - (``Int.min , mkApp2 (.const ``Min.min [.zero]) intc (mkConst ``Int.instMinInt)) + (``Int.max , mkApp2 (.const ``Max.max [.zero]) intc (mkConst ``Int.instMax)), + (``Int.min , mkApp2 (.const ``Min.min [.zero]) intc (mkConst ``Int.instMin)) ] def stringConstSimpNFList : List (Name × Expr) := @@ -452,8 +452,8 @@ namespace Lam2D [ (``String.append, mkApp4 (.const ``HAppend.hAppend [.zero, .zero, .zero]) stringc stringc stringc - (mkApp2 (.const ``instHAppend [.zero]) stringc (mkConst ``String.instAppendString))), - (``String.lt, mkApp2 (.const ``LT.lt [.zero]) stringc (mkConst ``String.instLTString)), + (mkApp2 (.const ``instHAppendOfAppend [.zero]) stringc (mkConst ``String.instAppend))), + (``String.lt, mkApp2 (.const ``LT.lt [.zero]) stringc (mkConst ``String.instLT)), ] open LamCstrD in @@ -464,57 +464,57 @@ namespace Lam2D [ (``BitVec.add , .lam `n natc (mkApp4 (.const ``HAdd.hAdd [.zero, .zero, .zero]) (.app bitVecc (.bvar 0)) (.app bitVecc (.bvar 0)) (.app bitVecc (.bvar 0)) - (mkApp2 (.const ``instHAdd [.zero]) (.app bitVecc (.bvar 0)) (.app (mkConst ``BitVec.instAddBitVec) (.bvar 0)))) .default), + (mkApp2 (.const ``instHAdd [.zero]) (.app bitVecc (.bvar 0)) (.app (mkConst ``BitVec.instAdd) (.bvar 0)))) .default), (``BitVec.sub , .lam `n natc (mkApp4 (.const ``HSub.hSub [.zero, .zero, .zero]) (.app bitVecc (.bvar 0)) (.app bitVecc (.bvar 0)) (.app bitVecc (.bvar 0)) - (mkApp2 (.const ``instHSub [.zero]) (.app bitVecc (.bvar 0)) (.app (mkConst ``BitVec.instSubBitVec) (.bvar 0)))) .default), + (mkApp2 (.const ``instHSub [.zero]) (.app bitVecc (.bvar 0)) (.app (mkConst ``BitVec.instSub) (.bvar 0)))) .default), (``BitVec.mul , .lam `n natc (mkApp4 (.const ``HMul.hMul [.zero, .zero, .zero]) (.app bitVecc (.bvar 0)) (.app bitVecc (.bvar 0)) (.app bitVecc (.bvar 0)) - (mkApp2 (.const ``instHMul [.zero]) (.app bitVecc (.bvar 0)) (.app (mkConst ``BitVec.instMulBitVec) (.bvar 0)))) .default), + (mkApp2 (.const ``instHMul [.zero]) (.app bitVecc (.bvar 0)) (.app (mkConst ``BitVec.instMul) (.bvar 0)))) .default), (``BitVec.udiv , .lam `n natc (mkApp4 (.const ``HDiv.hDiv [.zero, .zero, .zero]) (.app bitVecc (.bvar 0)) (.app bitVecc (.bvar 0)) (.app bitVecc (.bvar 0)) - (mkApp2 (.const ``instHDiv [.zero]) (.app bitVecc (.bvar 0)) (.app (mkConst ``BitVec.instDivBitVec) (.bvar 0)))) .default), + (mkApp2 (.const ``instHDiv [.zero]) (.app bitVecc (.bvar 0)) (.app (mkConst ``BitVec.instDiv) (.bvar 0)))) .default), (``BitVec.umod , .lam `n natc (mkApp4 (.const ``HMod.hMod [.zero, .zero, .zero]) (.app bitVecc (.bvar 0)) (.app bitVecc (.bvar 0)) (.app bitVecc (.bvar 0)) - (mkApp2 (.const ``instHMod [.zero]) (.app bitVecc (.bvar 0)) (.app (mkConst ``BitVec.instModBitVec) (.bvar 0)))) .default), + (mkApp2 (.const ``instHMod [.zero]) (.app bitVecc (.bvar 0)) (.app (mkConst ``BitVec.instMod) (.bvar 0)))) .default), (``BitVec.neg , .lam `n natc (mkApp2 - (.const ``Neg.neg [.zero]) (.app bitVecc (.bvar 0)) (.app (mkConst ``BitVec.instNegBitVec) (.bvar 0))) .default), + (.const ``Neg.neg [.zero]) (.app bitVecc (.bvar 0)) (.app (mkConst ``BitVec.instNeg) (.bvar 0))) .default), (``BitVec.propult , .lam `n natc (mkApp2 - (.const ``LT.lt [.zero]) (.app bitVecc (.bvar 0)) (.app (mkConst ``BitVec.instLTBitVec) (.bvar 0))) .default), + (.const ``LT.lt [.zero]) (.app bitVecc (.bvar 0)) (.app (mkConst ``BitVec.instLT) (.bvar 0))) .default), (``BitVec.propule , .lam `n natc (mkApp2 - (.const ``LE.le [.zero]) (.app bitVecc (.bvar 0)) (.app (mkConst ``BitVec.instLEBitVec) (.bvar 0))) .default), + (.const ``LE.le [.zero]) (.app bitVecc (.bvar 0)) (.app (mkConst ``BitVec.instLE) (.bvar 0))) .default), (``BitVec.and , .lam `n natc (mkApp4 (.const ``HAnd.hAnd [.zero, .zero, .zero]) (.app bitVecc (.bvar 0)) (.app bitVecc (.bvar 0)) (.app bitVecc (.bvar 0)) - (mkApp2 (.const ``instHAnd [.zero]) (.app bitVecc (.bvar 0)) (.app (mkConst ``BitVec.instAndOpBitVec) (.bvar 0)))) .default), + (mkApp2 (.const ``instHAndOfAndOp [.zero]) (.app bitVecc (.bvar 0)) (.app (mkConst ``BitVec.instAndOp) (.bvar 0)))) .default), (``BitVec.or , .lam `n natc (mkApp4 (.const ``HOr.hOr [.zero, .zero, .zero]) (.app bitVecc (.bvar 0)) (.app bitVecc (.bvar 0)) (.app bitVecc (.bvar 0)) - (mkApp2 (.const ``instHOr [.zero]) (.app bitVecc (.bvar 0)) (.app (mkConst ``BitVec.instOrOpBitVec) (.bvar 0)))) .default), + (mkApp2 (.const ``instHOrOfOrOp [.zero]) (.app bitVecc (.bvar 0)) (.app (mkConst ``BitVec.instOrOp) (.bvar 0)))) .default), (``BitVec.xor , .lam `n natc (mkApp4 (.const ``HXor.hXor [.zero, .zero, .zero]) (.app bitVecc (.bvar 0)) (.app bitVecc (.bvar 0)) (.app bitVecc (.bvar 0)) - (mkApp2 (.const ``instHXor [.zero]) (.app bitVecc (.bvar 0)) (.app (mkConst ``BitVec.instXorBitVec) (.bvar 0)))) .default), + (mkApp2 (.const ``instHXorOfXor [.zero]) (.app bitVecc (.bvar 0)) (.app (mkConst ``BitVec.instXor) (.bvar 0)))) .default), (``BitVec.not , .lam `n natc (mkApp2 (.const ``Complement.complement [.zero]) (.app bitVecc (.bvar 0)) - (.app (mkConst ``BitVec.instComplementBitVec) (.bvar 0))) .default), + (.app (mkConst ``BitVec.instComplement) (.bvar 0))) .default), (``BitVec.shiftLeft , .lam `n natc (mkApp4 (.const ``HShiftLeft.hShiftLeft [.zero, .zero, .zero]) (.app bitVecc (.bvar 0)) natc (.app bitVecc (.bvar 0)) - (.app (mkConst ``BitVec.instHShiftLeftBitVecNat) (.bvar 0))) .default), + (.app (mkConst ``BitVec.instHShiftLeftNat ) (.bvar 0))) .default), (``BitVec.ushiftRight , .lam `n natc (mkApp4 (.const ``HShiftRight.hShiftRight [.zero, .zero, .zero]) (.app bitVecc (.bvar 0)) natc (.app bitVecc (.bvar 0)) - (.app (mkConst ``BitVec.instHShiftRightBitVecNat) (.bvar 0))) .default), + (.app (mkConst ``BitVec.instHShiftRightNat) (.bvar 0))) .default), (``BitVec.smtHshiftLeft , .lam `n natc (.lam `m natc (.lam `a (.app bitVecc (.bvar 1)) (.lam `b (.app bitVecc (.bvar 1)) (mkApp6 (.const ``HShiftLeft.hShiftLeft [.zero, .zero, .zero]) (.app bitVecc (.bvar 3)) natc (.app bitVecc (.bvar 3)) - (.app (mkConst ``BitVec.instHShiftLeftBitVecNat) (.bvar 3)) (.bvar 1) (mkApp2 (mkConst ``BitVec.toNat) (.bvar 2) (.bvar 0)) + (.app (mkConst ``BitVec.instHShiftLeftNat) (.bvar 3)) (.bvar 1) (mkApp2 (mkConst ``BitVec.toNat) (.bvar 2) (.bvar 0)) ) .default ) .default) .default) .default), (``BitVec.smtHushiftRight , .lam `n natc (.lam `m natc (.lam `a (.app bitVecc (.bvar 1)) (.lam `b (.app bitVecc (.bvar 1)) (mkApp6 (.const ``HShiftRight.hShiftRight [.zero, .zero, .zero]) (.app bitVecc (.bvar 3)) natc (.app bitVecc (.bvar 3)) - (.app (mkConst ``BitVec.instHShiftRightBitVecNat) (.bvar 3)) (.bvar 1) (mkApp2 (mkConst ``BitVec.toNat) (.bvar 2) (.bvar 0)) + (.app (mkConst ``BitVec.instHShiftRightNat) (.bvar 3)) (.bvar 1) (mkApp2 (mkConst ``BitVec.toNat) (.bvar 2) (.bvar 0)) ) .default ) .default) .default) .default), (``BitVec.append , .lam `n natc (.lam `m natc (mkApp4 (.const ``HAppend.hAppend [.zero, .zero, .zero]) (.app bitVecc (.bvar 1)) (.app bitVecc (.bvar 0)) (.app bitVecc (mkApp6 (.const ``HAdd.hAdd [.zero, .zero, .zero]) natc natc natc (mkApp2 (.const ``instHAdd [.zero]) natc (mkConst ``instAddNat)) (.bvar 1) (.bvar 0))) - (mkApp2 (.const ``BitVec.instHAppendBitVecHAddNatInstHAddInstAddNat []) (.bvar 1) (.bvar 0))) .default) .default), + (mkApp2 (.const ``BitVec.instHAppendHAddNat []) (.bvar 1) (.bvar 0))) .default) .default), ] def lamBaseTermSimpNFList : List (Name × Expr) := diff --git a/lean-toolchain b/lean-toolchain index e69bc88..66aa763 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.7.0 \ No newline at end of file +leanprover/lean4:v4.8.0 \ No newline at end of file