How to use Set.image and have prop that says elem is of Set

Stream: new members

[An Qi Zhang]

Hello! When using Set.image to map from a Set "x" to another Set "y" with a function "f", I was wondering if there's a way to get a prop that says the element f works on is of x?

Here's a MWE to illustrate:

import Mathlib

namespace MWE

inductive Nats
| order : Nat → Nat → Nats
| one : Nat → Nats

abbrev SetNats := Set Nats

def Nats.before : Nats → Nat → Prop
| ns, n =>
  match ns with
  | order _ n₂ => n = n₂
  | one _ => false

def SetNats.before (x : SetNats) (n : Nat) : SetNats := {nats ∈ x | nats.before n}

lemma SetNats.mem_before (x : SetNats) (n : Nat) : ∀ m ∈ x.before n, m ∈ x ∧ m.before n := by
  simp [SetNats.before]

def Nats.pred (nats : Nats) (n : Nat) : (nats_is_order : nats.before n) → Nat
| nats_is_order =>
  match nats with
  | .order n₁ n₂ =>
    if h : n₂ = n then n₁
    /- Is this a good approach? Or is there a better approach, that will let lean eliminate
    the other branch (else) automatically? -/
    else absurd nats_is_order (by simp_all [Nats.before])

def SetNats.predecessor (x : SetNats) (n : Nat) : Set Nat :=
  let ordered := x.before n
  /- Need to state variable `nats` is in `ordered` somehow?
  Or is there a better approach? -/
  ordered.image (λ nats => nats.pred n ((ordered.mem_before n) nats))

[Kenny Lau]

import Mathlib

namespace MWE

inductive Nats
| order : Nat → Nat → Nats
| one : Nat → Nats

abbrev SetNats := Set Nats

def Nats.before : Nats → Nat → Prop
| ns, n =>
  match ns with
  | order _ n₂ => n = n₂
  | one _ => false

def SetNats.before (x : SetNats) (n : Nat) : SetNats := {nats ∈ x | nats.before n}

lemma SetNats.mem_before (x : SetNats) (n : Nat) : ∀ m ∈ x.before n, m ∈ x ∧ m.before n := by
  simp [SetNats.before]

/-
def Nats.pred : Π (nats : Nats) (n : Nat) (nats_is_order : nats.before n), Nat
| (order n₁ _), _, rfl => n₁
-/

def Nats.pred : Π (nats : Nats) (n : Nat), Nat
| (order n₁ n₂), n₃ => n₁
| (one n₁), n₃ => n₁

def SetNats.predecessor (x : SetNats) (n : Nat) : Set Nat :=
  let ordered := x.before n
  /- Need to state variable `nats` is in `ordered` somehow?
  Or is there a better approach? -/
  ordered.image (λ nats => nats.pred n)

@An Qi Zhang just for the first question, the answer is to include the variables to the right of the colon, i.e. I changed (nats : Nats) (n : Nat) : (nats_is_order : nats.before n) → Nat to Π (nats : Nats) (n : Nat) (nats_is_order : nats.before n), Nat.

But you'll notice that I commented that solution out, because for your next question, the philosophy is that it's always better to define a full function with junk values than to define a partial function, because then you wouldn't have to supply proofs. This is why in Lean, 1 / 0 = 0:

import Mathlib

example : (1 / 0 : ℚ) = 0 := by rw [Rat.div_def, Rat.inv_zero, one_mul]

[Kenny Lau]

"full function with junk values" means a function that does not take in any proofs as the input

[Kenny Lau]

and returns incorrect result outside the "domain" specified