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: ParserDescr
zify) "zify" (
simpArgs: ParserDescr
simpArgs)? (
ppSpace: Parser.Parser
ppSpace 
location: ParserDescr
location)? : 
tactic: Parser.Category
tactic

macro_rules
| `(tactic| zify $[[$
simpArgs: ?m.95
simpArgs,*]]? $[at $
location: ?m.583
location]?) =>
  let 
args: ?m.683
args := 
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 k
getElems) |>.
getD: {ฮฑ : Type ?u.698} โ†’ Option ฮฑ โ†’ ฮฑ โ†’ ฮฑ
getD 
#[]: Array ?m.705
#[]
  `(tactic|
    simp (config := {decide := false}) only [zify_simps, push_cast, $
args: ?m.683
args,*] $[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 MkSimpContextResult
mkZifyContext (
simpArgs: Option (Syntax.TSepArray `Lean.Parser.Tactic.simpStar ",")
simpArgs : 
Option: Type ?u.6264 โ†’ Type ?u.6264
Option (
Syntax.TSepArray: SyntaxNodeKinds โ†’ String โ†’ Type
Syntax.TSepArray 
`Lean.Parser.Tactic.simpStar: Name
`Lean.Parser.Tactic.simpStar 
",": String
",")) :
    
TacticM: Type โ†’ Type
TacticM 
MkSimpContextResult: Type
MkSimpContextResult := do
  let 
args: ?m.6371
args := 
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 k
getElems) |>.
getD: {ฮฑ : Type ?u.6387} โ†’ Option ฮฑ โ†’ ฮฑ โ†’ ฮฑ
getD 
#[]: Array ?m.6394
#[]
  
mkSimpContext: Syntax โ†’ Bool โ†’ optParam SimpKind SimpKind.simp โ†’ optParam Bool false โ†’ TacticM MkSimpContextResult
mkSimpContext
    
(โ† `(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.7551
simp
(โ† `(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.7551
config
(โ† `(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.7551
only
(โ† `(tactic| simp (config := {decide := false}) only [zify_simps, push_cast, $args,*])): ?m.7551
 [zify_simps, push_cast, $
args: ?m.6371
args
(โ† `(tactic| simp (config := {decide := false}) only [zify_simps, push_cast, $args,*])): ?m.7551
,*])) 
false: Bool
false

/-- 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: Expr
proof : 
Expr: Type
Expr) (
prop: Expr
prop : 
Expr: Type
Expr) (
r: Simp.Result
r : 
Simp.Result: Type
Simp.Result) : 
MetaM: Type โ†’ Type
MetaM (
Expr: Type
Expr ร— 
Expr: Type
Expr) :=
  do
  match 
r: Simp.Result
r.
proof?: Simp.Result โ†’ Option Expr
proof? with
  | 
some: {ฮฑ : Type ?u.12970} โ†’ ฮฑ โ†’ Option ฮฑ
some 
eqProof: Expr
eqProof => return (โ† 
mkExpectedTypeHint: Expr โ†’ Expr โ†’ MetaM Expr
mkExpectedTypeHint 
(โ† mkEqMP eqProof proof): ?m.13043
(โ† 
mkEqMP: Expr โ†’ Expr โ†’ MetaM Expr
mkEqMP
(โ† mkEqMP eqProof proof): ?m.13043
 
eqProof: Expr
eqProof
(โ† mkEqMP eqProof proof): ?m.13043
 
proof: Expr
proof
(โ† mkEqMP eqProof proof): ?m.13043
) 
r: Simp.Result
r.
expr: Simp.Result โ†’ Expr
expr, 
r: Simp.Result
r.
expr: Simp.Result โ†’ Expr
expr)
  | 
none: {ฮฑ : Type ?u.12974} โ†’ Option ฮฑ
none =>
    if 
r: Simp.Result
r.
expr: Simp.Result โ†’ Expr
expr != 
prop: Expr
prop then
      return (โ† 
mkExpectedTypeHint: Expr โ†’ Expr โ†’ MetaM Expr
mkExpectedTypeHint 
proof: Expr
proof 
r: Simp.Result
r.
expr: Simp.Result โ†’ Expr
expr, 
r: Simp.Result
r.
expr: Simp.Result โ†’ Expr
expr)
    else
      return (
proof: Expr
proof, 
r: Simp.Result
r.
expr: Simp.Result โ†’ Expr
expr)

/-- 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.14452
Option (
Syntax.TSepArray: SyntaxNodeKinds โ†’ String โ†’ Type
Syntax.TSepArray 
`Lean.Parser.Tactic.simpStar: Name
`Lean.Parser.Tactic.simpStar 
",": String
","))
  (
proof: Expr
proof : 
Expr: Type
Expr) (
prop: Expr
prop : 
Expr: Type
Expr) : 
TacticM: Type โ†’ Type
TacticM (
Expr: Type
Expr ร— 
Expr: Type
Expr) := do
  let 
ctx_result: ?m.14634
ctx_result โ† 
mkZifyContext: Option (Syntax.TSepArray `Lean.Parser.Tactic.simpStar ",") โ†’ TacticM MkSimpContextResult
mkZifyContext 
simpArgs: Option (Syntax.TSepArray `Lean.Parser.Tactic.simpStar ",")
simpArgs
  let (
r: Simp.Result
r, _) โ† 
simp: Expr โ†’
  Simp.Context โ†’
    optParam (Option Simp.Discharge) none โ†’ optParam Simp.UsedSimps โˆ… โ†’ MetaM (Simp.Result ร— Simp.UsedSimps)
simp 
prop: Expr
prop 
ctx_result: ?m.14634
ctx_result.
ctx: MkSimpContextResult โ†’ Simp.Context
ctx
  
applySimpResultToProp': Expr โ†’ Expr โ†’ Simp.Result โ†’ MetaM (Expr ร— Expr)
applySimpResultToProp' 
proof: Expr
proof 
prop: Expr
prop 
r: Simp.Result
r

@[zify_simps] lemma 
nat_cast_eq: โˆ€ (a b : โ„•), a = b โ†” โ†‘a = โ†‘b
nat_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 = n
Int.ofNat_inj.
symm: โˆ€ {a b : Prop}, (a โ†” b) โ†’ (b โ†” a)
symm
@[zify_simps] lemma 
nat_cast_le: โˆ€ (a b : โ„•), a โ‰ค b โ†” โ†‘a โ‰ค โ†‘b
nat_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 โ‰ค n
Int.ofNat_le.
symm: โˆ€ {a b : Prop}, (a โ†” b) โ†’ (b โ†” a)
symm
@[zify_simps] lemma 
nat_cast_lt: โˆ€ (a b : โ„•), a < b โ†” โ†‘a < โ†‘b
nat_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 < m
Int.ofNat_lt.
symm: โˆ€ {a b : Prop}, (a โ†” b) โ†’ (b โ†” a)
symm
@[zify_simps] lemma 
nat_cast_ne: โˆ€ (a b : โ„•), a โ‰  b โ†” โ†‘a โ‰  โ†‘b
nat_cast_ne (
a: โ„•
a 
b: โ„•
b : 
โ„•: Type
โ„•) : 
a: โ„•
a โ‰  
b: โ„•
b โ†” (
a: โ„•
a : 
โ„ค: Type
โ„ค) โ‰  (
b: โ„•
b : 
โ„ค: Type
โ„ค) := 
Goals accomplished! ๐Ÿ™
a, b: โ„•

a โ‰  b โ†” โ†‘a โ‰  โ†‘b
Goals accomplished! ๐Ÿ™