Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
```/-
Authors: Moritz Doll, Mario Carneiro, Robert Y. Lewis
-/
import Mathlib.Tactic.Basic
import Mathlib.Tactic.NormCast
import Mathlib.Tactic.Zify.Attr
import Mathlib.Data.Int.Basic

/-!
# `zify` tactic

The `zify` tactic is used to shift propositions from `ℕ` to `ℤ`.
This is often useful since `ℤ` has well-behaved subtraction.
```
example (a b c x y z : ℕ) (h : ¬ x*y*z < 0) : c < a + 3*b := by
zify
zify at h
/-
h : ¬↑x * ↑y * ↑z < 0
⊢ ↑c < ↑a + 3 * ↑b
-/
```
-/

namespace Mathlib.Tactic.Zify

open Lean
open Lean.Meta
open Lean.Parser.Tactic
open Lean.Elab.Tactic

/--
The `zify` tactic is used to shift propositions from `ℕ` to `ℤ`.
This is often useful since `ℤ` has well-behaved subtraction.
```
example (a b c x y z : ℕ) (h : ¬ x*y*z < 0) : c < a + 3*b := by
zify
zify at h
/-
h : ¬↑x * ↑y * ↑z < 0
⊢ ↑c < ↑a + 3 * ↑b
-/
```
`zify` can be given extra lemmas to use in simplification. This is especially useful in the
presence of nat subtraction: passing `≤` arguments will allow `push_cast` to do more work.
```
example (a b c : ℕ) (h : a - b < c) (hab : b ≤ a) : false := by
zify [hab] at h
/- h : ↑a - ↑b < ↑c -/
```
`zify` makes use of the `@[zify_simps]` attribute to move propositions,
and the `push_cast` tactic to simplify the `ℤ`-valued expressions.
`zify` is in some sense dual to the `lift` tactic. `lift (z : ℤ) to ℕ` will change the type of an
integer `z` (in the supertype) to `ℕ` (the subtype), given a proof that `z ≥ 0`;
propositions concerning `z` will still be over `ℤ`. `zify` changes propositions about `ℕ` (the
subtype) to propositions about `ℤ` (the supertype), without changing the type of any variable.
-/
syntax (name := zify: ParserDescrzify) "zify" (simpArgs: ParserDescrsimpArgs)? (ppSpace: Parser.ParserppSpace location: ParserDescrlocation)? : tactic: Parser.Categorytactic

macro_rules
| `(tactic| zify \$[[\$simpArgs: ?m.95simpArgs,*]]? \$[at \$location: ?m.583location]?) =>
let args: ?m.683args := simpArgs: ?m.99 x✝¹simpArgs.map: {α : Type ?u.685} → {β : Type ?u.684} → (α → β) → Option α → Option βmap (·.getElems: {k : SyntaxNodeKinds} → {sep : String} → Syntax.TSepArray k sep → TSyntaxArray kgetElems) |>.getD: {α : Type ?u.698} → Option α → α → αgetD #[]: Array ?m.705#[]
`(tactic|
simp (config := {decide := false}) only [zify_simps, push_cast, \$args: ?m.683args,*] \$[at \$location: TSyntax [`Lean.Parser.Tactic.locationWildcard, `Lean.Parser.Tactic.locationHyp]location]?)

/-- The `Simp.Context` generated by `zify`. -/
def mkZifyContext: Option (Syntax.TSepArray `Lean.Parser.Tactic.simpStar ",") → TacticM MkSimpContextResultmkZifyContext (simpArgs: Option (Syntax.TSepArray `Lean.Parser.Tactic.simpStar ",")simpArgs : Option: Type ?u.6264 → Type ?u.6264Option (Syntax.TSepArray: SyntaxNodeKinds → String → TypeSyntax.TSepArray `Lean.Parser.Tactic.simpStar: Name`Lean.Parser.Tactic.simpStar ",": String",")) :
TacticM: Type → TypeTacticM MkSimpContextResult: TypeMkSimpContextResult := do
let args: ?m.6371args := simpArgs: Option (Syntax.TSepArray `Lean.Parser.Tactic.simpStar ",")simpArgs.map: {α : Type ?u.6373} → {β : Type ?u.6372} → (α → β) → Option α → Option βmap (·.getElems: {k : SyntaxNodeKinds} → {sep : String} → Syntax.TSepArray k sep → TSyntaxArray kgetElems) |>.getD: {α : Type ?u.6387} → Option α → α → αgetD #[]: Array ?m.6394#[]
mkSimpContext: Syntax → Bool → optParam SimpKind SimpKind.simp → optParam Bool false → TacticM MkSimpContextResultmkSimpContext
(← `(tactic| simp (config := {decide := false}) only [zify_simps, push_cast, \$args,*])): ?m.7551(← `(tactic| (← `(tactic| simp (config := {decide := false}) only [zify_simps, push_cast, \$args,*])): ?m.7551simp(← `(tactic| simp (config := {decide := false}) only [zify_simps, push_cast, \$args,*])): ?m.7551 ((← `(tactic| simp (config := {decide := false}) only [zify_simps, push_cast, \$args,*])): ?m.7551config(← `(tactic| simp (config := {decide := false}) only [zify_simps, push_cast, \$args,*])): ?m.7551 := {decide := false}) (← `(tactic| simp (config := {decide := false}) only [zify_simps, push_cast, \$args,*])): ?m.7551only(← `(tactic| simp (config := {decide := false}) only [zify_simps, push_cast, \$args,*])): ?m.7551 [zify_simps, push_cast, \$args: ?m.6371args(← `(tactic| simp (config := {decide := false}) only [zify_simps, push_cast, \$args,*])): ?m.7551,*])) false: Boolfalse

/-- A variant of `applySimpResultToProp` that cannot close the goal, but does not need a meta
variable and returns a tuple of a proof and the corresponding simplified proposition. -/
def applySimpResultToProp': Expr → Expr → Simp.Result → MetaM (Expr × Expr)applySimpResultToProp' (proof: Exprproof : Expr: TypeExpr) (prop: Exprprop : Expr: TypeExpr) (r: Simp.Resultr : Simp.Result: TypeSimp.Result) : MetaM: Type → TypeMetaM (Expr: TypeExpr × Expr: TypeExpr) :=
do
match r: Simp.Resultr.proof?: Simp.Result → Option Exprproof? with
| some: {α : Type ?u.12970} → α → Option αsome eqProof: ExpreqProof => return (← mkExpectedTypeHint: Expr → Expr → MetaM ExprmkExpectedTypeHint (← mkEqMP eqProof proof): ?m.13043(← mkEqMP: Expr → Expr → MetaM ExprmkEqMP(← mkEqMP eqProof proof): ?m.13043 eqProof: ExpreqProof(← mkEqMP eqProof proof): ?m.13043 proof: Exprproof(← mkEqMP eqProof proof): ?m.13043) r: Simp.Resultr.expr: Simp.Result → Exprexpr, r: Simp.Resultr.expr: Simp.Result → Exprexpr)
| none: {α : Type ?u.12974} → Option αnone =>
if r: Simp.Resultr.expr: Simp.Result → Exprexpr != prop: Exprprop then
return (← mkExpectedTypeHint: Expr → Expr → MetaM ExprmkExpectedTypeHint proof: Exprproof r: Simp.Resultr.expr: Simp.Result → Exprexpr, r: Simp.Resultr.expr: Simp.Result → Exprexpr)
else
return (proof: Exprproof, r: Simp.Resultr.expr: Simp.Result → Exprexpr)

/-- Translate a proof and the proposition into a zified form. -/
def zifyProof: Option (Syntax.TSepArray `Lean.Parser.Tactic.simpStar ",") → Expr → Expr → TacticM (Expr × Expr)zifyProof (simpArgs: Option (Syntax.TSepArray `Lean.Parser.Tactic.simpStar ",")simpArgs : Option: Type ?u.14452 → Type ?u.14452Option (Syntax.TSepArray: SyntaxNodeKinds → String → TypeSyntax.TSepArray `Lean.Parser.Tactic.simpStar: Name`Lean.Parser.Tactic.simpStar ",": String","))
(proof: Exprproof : Expr: TypeExpr) (prop: Exprprop : Expr: TypeExpr) : TacticM: Type → TypeTacticM (Expr: TypeExpr × Expr: TypeExpr) := do
let ctx_result: ?m.14634ctx_result ← mkZifyContext: Option (Syntax.TSepArray `Lean.Parser.Tactic.simpStar ",") → TacticM MkSimpContextResultmkZifyContext simpArgs: Option (Syntax.TSepArray `Lean.Parser.Tactic.simpStar ",")simpArgs
let (r: Simp.Resultr, _) ← simp: Expr →
Simp.Context →
optParam (Option Simp.Discharge) none → optParam Simp.UsedSimps ∅ → MetaM (Simp.Result × Simp.UsedSimps)simp prop: Exprprop ctx_result: ?m.14634ctx_result.ctx: MkSimpContextResult → Simp.Contextctx
applySimpResultToProp': Expr → Expr → Simp.Result → MetaM (Expr × Expr)applySimpResultToProp' proof: Exprproof prop: Exprprop r: Simp.Resultr

@[zify_simps] lemma nat_cast_eq: ∀ (a b : ℕ), a = b ↔ ↑a = ↑bnat_cast_eq (a: ℕa b: ℕb : ℕ: Typeℕ) : a: ℕa = b: ℕb ↔ (a: ℕa : ℤ: Typeℤ) = (b: ℕb : ℤ: Typeℤ) := Int.ofNat_inj: ∀ {m n : ℕ}, ↑m = ↑n ↔ m = nInt.ofNat_inj.symm: ∀ {a b : Prop}, (a ↔ b) → (b ↔ a)symm
@[zify_simps] lemma nat_cast_le: ∀ (a b : ℕ), a ≤ b ↔ ↑a ≤ ↑bnat_cast_le (a: ℕa b: ℕb : ℕ: Typeℕ) : a: ℕa ≤ b: ℕb ↔ (a: ℕa : ℤ: Typeℤ) ≤ (b: ℕb : ℤ: Typeℤ) := Int.ofNat_le: ∀ {m n : ℕ}, ↑m ≤ ↑n ↔ m ≤ nInt.ofNat_le.symm: ∀ {a b : Prop}, (a ↔ b) → (b ↔ a)symm
@[zify_simps] lemma nat_cast_lt: ∀ (a b : ℕ), a < b ↔ ↑a < ↑bnat_cast_lt (a: ℕa b: ℕb : ℕ: Typeℕ) : a: ℕa < b: ℕb ↔ (a: ℕa : ℤ: Typeℤ) < (b: ℕb : ℤ: Typeℤ) := Int.ofNat_lt: ∀ {n m : ℕ}, ↑n < ↑m ↔ n < mInt.ofNat_lt.symm: ∀ {a b : Prop}, (a ↔ b) → (b ↔ a)symm
@[zify_simps] lemma nat_cast_ne: ∀ (a b : ℕ), a ≠ b ↔ ↑a ≠ ↑bnat_cast_ne (a: ℕa b: ℕb : ℕ: Typeℕ) : a: ℕa ≠ b: ℕb ↔ (a: ℕa : ℤ: Typeℤ) ≠ (b: ℕb : ℤ: Typeℤ) := byGoals accomplished! 🐙
a, b: ℕa ≠ b ↔ ↑a ≠ ↑bsimp only [ne_eq: ∀ {α : Sort ?u.16996} (a b : α), (a ≠ b) = ¬a = bne_eq, Int.cast_eq_cast_iff_Nat: ∀ (m n : ℕ), ↑m = ↑n ↔ m = nInt.cast_eq_cast_iff_Nat]Goals accomplished! 🐙
```