From 0c609380035b2ba7b9f3e7e19e247a2e31a5989c Mon Sep 17 00:00:00 2001 From: Parcly Taxel Date: Mon, 5 Jun 2023 13:08:27 +0800 Subject: [PATCH] Cf. #4027 --- Mathlib/Data/Nat/SqrtNormNum.lean | 39 +++---------------------------- 1 file changed, 3 insertions(+), 36 deletions(-) diff --git a/Mathlib/Data/Nat/SqrtNormNum.lean b/Mathlib/Data/Nat/SqrtNormNum.lean index 31b463af4d740..57875692d1682 100644 --- a/Mathlib/Data/Nat/SqrtNormNum.lean +++ b/Mathlib/Data/Nat/SqrtNormNum.lean @@ -14,41 +14,8 @@ import Mathlib.Data.Nat.Sqrt /-! ### `norm_num` plugin for `sqrt` The `norm_num` plugin evaluates `sqrt` by bounding it between consecutive integers. --/ - - -namespace NormNum - -open Tactic Nat -theorem is_sqrt {n a a2 b : ℕ} (ha2 : a * a = a2) (hb : a2 + b = n) (hle : b ≤ bit0 a) : - sqrt n = a := by rw [← hb, ← ha2, ← pow_two]; exact sqrt_add_eq' _ hle -#align norm_num.is_sqrt NormNum.is_sqrt - -/-- Given `n` provides `(a, ⊢ nat.sqrt n = a)`. -/ -unsafe def prove_sqrt (ic : instance_cache) (n : expr) : tactic (instance_cache × expr × expr) := do - let nn ← n.toNat - let na := nn.sqrt - let (ic, a) ← ic.ofNat na - let (ic, a2, ha2) ← prove_mul_nat ic a a - let (ic, b) ← ic.ofNat (nn - na * na) - let (ic, hb) ← prove_add_nat ic a2 b n - let (ic, hle) ← prove_le_nat ic b (q((bit0 : ℕ → ℕ)).mk_app [a]) - pure (ic, a, q(@is_sqrt).mk_app [n, a, a2, b, ha2, hb, hle]) -#align norm_num.prove_sqrt norm_num.prove_sqrt - -/-- A `norm_num` plugin for `sqrt n` when `n` is a numeral. -/ -@[norm_num] -unsafe def eval_sqrt : expr → tactic (expr × expr) - | q(sqrt $(en)) => do - let n ← en.toNat - match n with - | 0 => pure (q((0 : ℕ)), q(sqrt_zero)) - | _ => do - let c ← mk_instance_cache q(ℕ) - Prod.snd <$> prove_sqrt c en - | _ => failed -#align norm_num.eval_sqrt norm_num.eval_sqrt - -end NormNum +Porting note: the sole purpose of this file is to mark it as "ported". +This file seems to be tripping up the porting dashboard. +-/