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.
```/-
Copyright (c) 2022 Moritz Doll. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
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! ๐
```