From ba4c611f3b208826d600be5173c50441f9499b78 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Sat, 21 Dec 2024 13:10:05 -0800 Subject: [PATCH] delete LiftLets --- Mathlib.lean | 1 - .../CliffordAlgebra/EvenEquiv.lean | 1 - Mathlib/Tactic.lean | 1 - Mathlib/Tactic/LiftLets.lean | 134 ------------------ MathlibTest/LiftLets.lean | 108 -------------- scripts/noshake.json | 1 - 6 files changed, 246 deletions(-) delete mode 100644 Mathlib/Tactic/LiftLets.lean delete mode 100644 MathlibTest/LiftLets.lean diff --git a/Mathlib.lean b/Mathlib.lean index c7341a4fae6c3..db56e6cf9078c 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -4816,7 +4816,6 @@ import Mathlib.Tactic.IntervalCases import Mathlib.Tactic.IrreducibleDef import Mathlib.Tactic.Lemma import Mathlib.Tactic.Lift -import Mathlib.Tactic.LiftLets import Mathlib.Tactic.Linarith import Mathlib.Tactic.Linarith.Datatypes import Mathlib.Tactic.Linarith.Frontend diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/EvenEquiv.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/EvenEquiv.lean index 27682d972414a..2b099d379fd0f 100644 --- a/Mathlib/LinearAlgebra/CliffordAlgebra/EvenEquiv.lean +++ b/Mathlib/LinearAlgebra/CliffordAlgebra/EvenEquiv.lean @@ -6,7 +6,6 @@ Authors: Eric Wieser import Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation import Mathlib.LinearAlgebra.CliffordAlgebra.Even import Mathlib.LinearAlgebra.QuadraticForm.Prod -import Mathlib.Tactic.LiftLets /-! # Isomorphisms with the even subalgebra of a Clifford algebra diff --git a/Mathlib/Tactic.lean b/Mathlib/Tactic.lean index 228b76cabfb6a..43355fb469273 100644 --- a/Mathlib/Tactic.lean +++ b/Mathlib/Tactic.lean @@ -117,7 +117,6 @@ import Mathlib.Tactic.IntervalCases import Mathlib.Tactic.IrreducibleDef import Mathlib.Tactic.Lemma import Mathlib.Tactic.Lift -import Mathlib.Tactic.LiftLets import Mathlib.Tactic.Linarith import Mathlib.Tactic.Linarith.Datatypes import Mathlib.Tactic.Linarith.Frontend diff --git a/Mathlib/Tactic/LiftLets.lean b/Mathlib/Tactic/LiftLets.lean deleted file mode 100644 index c8827e34468e0..0000000000000 --- a/Mathlib/Tactic/LiftLets.lean +++ /dev/null @@ -1,134 +0,0 @@ -/- -Copyright (c) 2023 Kyle Miller. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Kyle Miller --/ -import Mathlib.Tactic.Basic - -/-! -# The `lift_lets` tactic - -This module defines a tactic `lift_lets` that can be used to pull `let` bindings as far out -of an expression as possible. --/ - -open Lean Elab Parser Meta Tactic - -/-- Configuration for `Lean.Expr.liftLets` and the `lift_lets` tactic. -/ -structure Lean.Expr.LiftLetsConfig where - /-- Whether to lift lets out of proofs. The default is not to. -/ - proofs : Bool := false - /-- Whether to merge let bindings if they have the same type and value. - This test is by syntactic equality, not definitional equality. - The default is to merge. -/ - merge : Bool := true - -/-- -Auxiliary definition for `Lean.Expr.liftLets`. Takes a list of the accumulated fvars. -This list is used during the computation to merge let bindings. --/ -private partial def Lean.Expr.liftLetsAux (config : LiftLetsConfig) (e : Expr) (fvars : Array Expr) - (f : Array Expr → Expr → MetaM Expr) : MetaM Expr := do - if (e.find? Expr.isLet).isNone then - -- If `e` contains no `let` expressions, then we can avoid recursing into it. - return ← f fvars e - if !config.proofs then - if ← Meta.isProof e then - return ← f fvars e - match e with - | .letE n t v b _ => - t.liftLetsAux config fvars fun fvars t' => - v.liftLetsAux config fvars fun fvars v' => do - if config.merge then - -- Eliminate the let binding if there is already one of the same type and value. - let fvar? ← fvars.findM? (fun fvar => do - let decl ← fvar.fvarId!.getDecl - return decl.type == t' && decl.value? == some v') - if let some fvar' := fvar? then - return ← (b.instantiate1 fvar').liftLetsAux config fvars f - withLetDecl n t' v' fun fvar => - (b.instantiate1 fvar).liftLetsAux config (fvars.push fvar) f - | .app x y => - x.liftLetsAux config fvars fun fvars x' => y.liftLetsAux config fvars fun fvars y' => - f fvars (.app x' y') - | .proj n idx s => - s.liftLetsAux config fvars fun fvars s' => f fvars (.proj n idx s') - | .lam n t b i => - t.liftLetsAux config fvars fun fvars t => do - -- Enter the binding, do liftLets, and lift out liftable lets - let e' ← withLocalDecl n i t fun fvar => do - (b.instantiate1 fvar).liftLetsAux config fvars fun fvars2 b => do - -- See which bindings can't be migrated out - let deps ← collectForwardDeps #[fvar] false - let fvars2 := fvars2[fvars.size:].toArray - let (fvars2, fvars2') := fvars2.partition deps.contains - mkLetFVars fvars2' (← mkLambdaFVars #[fvar] (← mkLetFVars fvars2 b)) - -- Re-enter the new lets; we do it this way to keep the local context clean - insideLets e' fvars fun fvars e'' => f fvars e'' - | .forallE n t b i => - t.liftLetsAux config fvars fun fvars t => do - -- Enter the binding, do liftLets, and lift out liftable lets - let e' ← withLocalDecl n i t fun fvar => do - (b.instantiate1 fvar).liftLetsAux config fvars fun fvars2 b => do - -- See which bindings can't be migrated out - let deps ← collectForwardDeps #[fvar] false - let fvars2 := fvars2[fvars.size:].toArray - let (fvars2, fvars2') := fvars2.partition deps.contains - mkLetFVars fvars2' (← mkForallFVars #[fvar] (← mkLetFVars fvars2 b)) - -- Re-enter the new lets; we do it this way to keep the local context clean - insideLets e' fvars fun fvars e'' => f fvars e'' - | .mdata _ e => e.liftLetsAux config fvars f - | _ => f fvars e -where - -- Like the whole `Lean.Expr.liftLets`, but only handles lets - insideLets {α} (e : Expr) (fvars : Array Expr) (f : Array Expr → Expr → MetaM α) : MetaM α := do - match e with - | .letE n t v b _ => - withLetDecl n t v fun fvar => insideLets (b.instantiate1 fvar) (fvars.push fvar) f - | _ => f fvars e - -/-- Take all the `let`s in an expression and move them outwards as far as possible. -All top-level `let`s are added to the local context, and then `f` is called with the list -of local bindings (each an fvar) and the new expression. - -Let bindings are merged if they have the same type and value. - -Use `e.liftLets mkLetFVars` to get a defeq expression with all `let`s lifted as far as possible. -/ -def Lean.Expr.liftLets (e : Expr) (f : Array Expr → Expr → MetaM Expr) - (config : LiftLetsConfig := {}) : MetaM Expr := - e.liftLetsAux config #[] f - -namespace Mathlib.Tactic - -declare_config_elab elabConfig Lean.Expr.LiftLetsConfig - -/-- -Lift all the `let` bindings in the type of an expression as far out as possible. - -When applied to the main goal, this gives one the ability to `intro` embedded `let` expressions. -For example, -```lean -example : (let x := 1; x) = 1 := by - lift_lets - -- ⊢ let x := 1; x = 1 - intro x - sorry -``` - -During the lifting process, let bindings are merged if they have the same type and value. --/ -syntax (name := lift_lets) "lift_lets" optConfig (ppSpace location)? : tactic - -elab_rules : tactic - | `(tactic| lift_lets $cfg:optConfig $[$loc:location]?) => do - let config ← elabConfig (mkOptionalNode cfg) - withLocation (expandOptLocation (Lean.mkOptionalNode loc)) - (atLocal := fun h ↦ liftMetaTactic1 fun mvarId ↦ do - let hTy ← instantiateMVars (← h.getType) - mvarId.changeLocalDecl h (← hTy.liftLets mkLetFVars config)) - (atTarget := liftMetaTactic1 fun mvarId ↦ do - let ty ← instantiateMVars (← mvarId.getType) - mvarId.change (← ty.liftLets mkLetFVars config)) - (failed := fun _ ↦ throwError "lift_lets tactic failed") - -end Mathlib.Tactic diff --git a/MathlibTest/LiftLets.lean b/MathlibTest/LiftLets.lean deleted file mode 100644 index de0ca7e728e32..0000000000000 --- a/MathlibTest/LiftLets.lean +++ /dev/null @@ -1,108 +0,0 @@ -import Mathlib.Tactic.LiftLets - -private axiom test_sorry : ∀ {α}, α -set_option autoImplicit true - -example : (let x := 1; x) = 1 := by - lift_lets - guard_target =ₛ let x := 1; x = 1 - intro _x - rfl - -example : (let x := 1; x) = (let y := 1; y) := by - lift_lets - guard_target =ₛ let x := 1; x = x - intro _x - rfl - -example : (let x := 1; x) = (let y := 1; y) := by - lift_lets (config := {merge := false}) - guard_target =ₛ let x := 1; let y := 1; x = y - intros _x _y - rfl - -example : (let x := (let y := 1; y + 1); x + 1) = 3 := by - lift_lets - guard_target =ₛ let y := 1; let x := y + 1; x + 1 = 3 - intros _y _x - rfl - -example : (fun x => let a := x; let y := 1; a + y) 2 = 2 + 1 := by - lift_lets - guard_target =ₛ let y := 1; (fun x ↦ let a := x; a + y) 2 = 2 + 1 - intro _y - rfl - -example : (fun (_ : let ty := Nat; ty) => Nat) (2 : Nat) := by - lift_lets - guard_target =ₛ let ty := Nat; (fun (_ : ty) ↦ Nat) (2 : Nat) - exact 0 - -example : (fun (x : let ty := Nat; ty) => Fin x) (2 : Nat) := by - lift_lets - guard_target =ₛ let ty := Nat; (fun (x : ty) ↦ Fin x) (2 : Nat) - exact 0 - - -example : (id : Nat → Nat) = (fun (x : let ty := Nat; ty) => x) := by - lift_lets - guard_target =ₛ let ty := Nat; (id: Nat → Nat) = fun (x : ty) ↦ x - rfl - -example : (x : let ty := Nat; ty) → let y := (1 : Nat); Fin (y + Nat.succ x) := by - lift_lets - guard_target =ₛ let ty := Nat; let y := 1; (x : ty) → Fin (y + Nat.succ x) - intro ty y x - rw [Nat.add_succ, Nat.succ_eq_add_one] - exact 0 - -example : (x : Nat) → (y : Nat) → let z := x + 1; let w := 3; Fin (z + w) := by - lift_lets - guard_target =ₛ let w := 3; (x : Nat) → let z := x + 1; Nat → Fin (z + w) - intro w x z _y - simp [w, z] - exact 0 - -example : (x : Nat) → let z := x + 1; (y : Nat) → let w := 3; Fin (z + w) := by - lift_lets - guard_target =ₛ let w := 3; (x : Nat) → let z := x + 1; Nat → Fin (z + w) - intro w x z _y - simp [w, z] - exact 0 - -example : (let x := 1; x) = (let x := 1; x) := by - lift_lets - guard_target =ₛ let x := 1; x = x - rfl - -example : (let x := 2; x) = (let y := 1; y + 1) := by - lift_lets - guard_target =ₛ let x := 2; let y := 1; x = y + 1 - rfl - -example (h : (let x := 1; x) = y) : True := by - lift_lets at h - guard_hyp h :ₛ let x := 1; x = y - trivial - -example (h : (let x := 1; x) = y) : True := by - revert h - lift_lets - intro x h - guard_hyp x : Nat := 1 - guard_hyp h :ₛ x = y - trivial - -example : let x := 1; ∀ n, let y := 1; x + n = y + n := by - lift_lets - guard_target =ₛ let x := 1; ∀ n, x + n = x + n - intros x n - rfl - -example (m : Nat) (h : ∃ n, n + 1 = m) (x : Fin m) (y : Fin _) : - cast (let h' := h.choose_spec.symm; congrArg Fin h') x = y := by - lift_lets (config := {proofs := true}) - intro h' - clear_value h' - guard_hyp h' : m = Exists.choose h + 1 - exact test_sorry diff --git a/scripts/noshake.json b/scripts/noshake.json index 4a0abe6e8cb0c..755db17cda67c 100644 --- a/scripts/noshake.json +++ b/scripts/noshake.json @@ -115,7 +115,6 @@ "Mathlib.Tactic.Lemma", "Mathlib.Tactic.LibrarySearch", "Mathlib.Tactic.Lift", - "Mathlib.Tactic.LiftLets", "Mathlib.Tactic.Linarith", "Mathlib.Tactic.Linarith.Frontend", "Mathlib.Tactic.Linarith.Lemmas",