how to use the `match` tactic in this case?

Stream: lean4

[ChenW]

In the code below, I aim to define a function called monotone_limit, which returns the limit of a sequence of sets.

import Mathlib.Data.Set.Lattice
import Mathlib.Data.Nat.Prime.Basic
open Set

-- Define monotonicity properties for sequences of sets
def non_dec {α : Type*} (A : ℕ → Set α) : Prop := ∀ (n : ℕ), A n ⊆ A (n + 1)
def non_inc {α : Type*} (A : ℕ → Set α) : Prop := ∀ (n : ℕ), A (n + 1) ⊆ A n
def is_monotone {α : Type*} (A : ℕ → Set α) : Prop := non_dec A ∨ non_inc A

-- Define the limit for non-decreasing and non-increasing sequences of sets
def monotone_limit_non_dec {α : Type*} (A : ℕ → Set α) : Set α := ⋃ n, A n
def monotone_limit_non_inc {α : Type*} (A : ℕ → Set α) : Set α := ⋂ n, A n

-- Attempt to implement `monotone_limit`
-- These implementations fail for the reasons described below.

-- Attempt 1: Using `match ... with`
/-
def monotone_limit {α : Type*} (A : ℕ → Set α) (h_mono : is_monotone A) : Set α := by
  -- tactic 'cases' failed, nested error:
  -- tactic 'induction' failed, recursor 'Or.casesOn' can only eliminate into Prop
  match h_mono with
  | Or.inl h_non_dec => monotone_limit_non_dec A
  | Or.inr h_non_inc => monotone_limit_non_inc A
-/

-- Attempt 2: Using `if ... else`
/-
def monotone_limit {α : Type*} (A : ℕ → Set α) (h_mono : is_monotone A) : Set α :=
  -- Error:
  -- failed to synthesize
  -- Decidable (non_dec A)
  if h_non_dec : non_dec A then
    monotone_limit_non_dec A
  else
    monotone_limit_non_inc A
-/

However, I failed to implement the function using either if ... else or match ... with. Could you explain why these attempts failed and provide any suggestions for resolving the issue? Any help would be greatly appreciated.

[Paige Thomas]

I think maybe the issue is that non_dec and non_inc are not decidable, because the domain of the function A is infinite? Therefore h_mono: is_monotone A is also not decidable. So I'm not sure this function can be defined. Someone should correct me if I am wrong.

[Paige Thomas]

That is, ∀ (n : ℕ), ... can't be computed.

[Kyle Miller]

Here's a possibility:

import Mathlib.Data.Set.Lattice
import Mathlib.Data.Nat.Prime.Basic
open Set

-- Define monotonicity properties for sequences of sets
def non_dec {α : Type*} (A : ℕ → Set α) : Prop := ∀ (n : ℕ), A n ⊆ A (n + 1)
def non_inc {α : Type*} (A : ℕ → Set α) : Prop := ∀ (n : ℕ), A (n + 1) ⊆ A n
def is_monotone {α : Type*} (A : ℕ → Set α) : Prop := non_dec A ∨ non_inc A

-- Define the limit for non-decreasing and non-increasing sequences of sets
def monotone_limit_non_dec {α : Type*} (A : ℕ → Set α) : Set α := ⋃ n, A n
def monotone_limit_non_inc {α : Type*} (A : ℕ → Set α) : Set α := ⋂ n, A n

def monotone_limit {α : Type*} (A : ℕ → Set α) : Set α :=
  have := Classical.dec
  if non_dec A then
    monotone_limit_non_dec A
  else if non_inc A then
    monotone_limit_non_inc A
  else
    -- Not necessary, but might be nice to have a specific "junk value"
    ∅

theorem monotone_limit_eq_of_non_dec {α : Type*} (A : ℕ → Set α) (h : non_dec A) :
    monotone_limit A = monotone_limit_non_dec A := by
  simp [monotone_limit, h]

theorem monotone_limit_eq_of_non_inc {α : Type*} (A : ℕ → Set α) (h : non_inc A) :
    monotone_limit A = monotone_limit_non_inc A := by
  by_cases h' : non_dec A
  · have : ∀ n, A (n + 1) = A n := fun n => subset_antisymm (h n) (h' n)
    have : ∀ n, A n = A 0 := by
      intro n
      induction n
      · rfl
      · simp [*]
    ext
    simp [monotone_limit, h, h', monotone_limit_non_dec, monotone_limit_non_inc, this]
  · simp [monotone_limit, h, h']

theorem monotone_limit_eq {α : Type*} (A : ℕ → Set α) (h : is_monotone A) :
    monotone_limit A = monotone_limit_non_dec A ∨ monotone_limit A = monotone_limit_non_inc A := by
  cases h <;> simp [monotone_limit_eq_of_non_dec, monotone_limit_eq_of_non_inc, *]

[Chris Wong]

I wonder why we don't need a noncomputable keyword. Is it because Set is prop anyway?

[Aaron Liu]

Set α is implemented as α → Prop, so the "conclusion" is a Sort 0, which is a type, which has no runtime representation. Since there is nothing to compile, there is no need to say noncomputable.

[ChenW]

Kyle Miller said:

Here's a possibility:

import Mathlib.Data.Set.Lattice
import Mathlib.Data.Nat.Prime.Basic
open Set

-- Define monotonicity properties for sequences of sets
def non_dec {α : Type*} (A : ℕ → Set α) : Prop := ∀ (n : ℕ), A n ⊆ A (n + 1)
def non_inc {α : Type*} (A : ℕ → Set α) : Prop := ∀ (n : ℕ), A (n + 1) ⊆ A n
def is_monotone {α : Type*} (A : ℕ → Set α) : Prop := non_dec A ∨ non_inc A

-- Define the limit for non-decreasing and non-increasing sequences of sets
def monotone_limit_non_dec {α : Type*} (A : ℕ → Set α) : Set α := ⋃ n, A n
def monotone_limit_non_inc {α : Type*} (A : ℕ → Set α) : Set α := ⋂ n, A n

def monotone_limit {α : Type*} (A : ℕ → Set α) : Set α :=
  have := Classical.dec
  if non_dec A then
    monotone_limit_non_dec A
  else if non_inc A then
    monotone_limit_non_inc A
  else
    -- Not necessary, but might be nice to have a specific "junk value"
    ∅

theorem monotone_limit_eq_of_non_dec {α : Type*} (A : ℕ → Set α) (h : non_dec A) :
    monotone_limit A = monotone_limit_non_dec A := by
  simp [monotone_limit, h]

theorem monotone_limit_eq_of_non_inc {α : Type*} (A : ℕ → Set α) (h : non_inc A) :
    monotone_limit A = monotone_limit_non_inc A := by
  by_cases h' : non_dec A
  · have : ∀ n, A (n + 1) = A n := fun n => subset_antisymm (h n) (h' n)
    have : ∀ n, A n = A 0 := by
      intro n
      induction n
      · rfl
      · simp [*]
    ext
    simp [monotone_limit, h, h', monotone_limit_non_dec, monotone_limit_non_inc, this]
  · simp [monotone_limit, h, h']

theorem monotone_limit_eq {α : Type*} (A : ℕ → Set α) (h : is_monotone A) :
    monotone_limit A = monotone_limit_non_dec A ∨ monotone_limit A = monotone_limit_non_inc A := by
  cases h <;> simp [monotone_limit_eq_of_non_dec, monotone_limit_eq_of_non_inc, *]

Thanks. This is helpful. :+1: .