hex

14.5. Rewriting other interval conventions🔗

Only Set.Ioc is accepted directly. If a goal uses a closed interval Set.Icc, separate the lower endpoint from the remaining half-open interval. For a predicate φ the exact rewrites are:

∀ x ∈ Set.Icc a b, φ x becomes (a ≤ b → φ a) ∧ ∀ x ∈ Set.Ioc a b, φ x.
∃ x ∈ Set.Icc a b, φ x becomes a ≤ b ∧ (φ a ∨ ∃ x ∈ Set.Ioc a b, φ x).

For an open interval Set.Ioo, exclude the upper endpoint from Set.Ioc:

∀ x ∈ Set.Ioo a b, φ x becomes ∀ x ∈ Set.Ioc a b, x ≠ b → φ x.
∃ x ∈ Set.Ioo a b, φ x becomes ∃ x ∈ Set.Ioc a b, φ x ∧ x ≠ b.

After the endpoint proposition has been handled separately, rcf can prove the remaining singly quantified part. This worked closed-interval example checks the lower endpoint separately and sends the Set.Ioc tail to rcf:

example : ∀ x : ℝ,
    x ∈ Set.Icc (0 : ℝ) 1 → x ^ 2 ≤ 1 := by⊢ ∀ x ∈ Set.Icc 0 1, x ^ 2 ≤ 1
  have endpoint : (0 : ℝ) ^ 2 ≤ 1 := by norm_numendpoint:0 ^ 2 ≤ 1⊢ ∀ x ∈ Set.Icc 0 1, x ^ 2 ≤ 1
  have tail : ∀ x : ℝ,
      x ∈ Set.Ioc (0 : ℝ) 1 → x ^ 2 ≤ 1 := by
    rcfendpoint:0 ^ 2 ≤ 1tail:∀ x ∈ Set.Ioc 0 1, x ^ 2 ≤ 1⊢ ∀ x ∈ Set.Icc 0 1, x ^ 2 ≤ 1
  intro x hxendpoint:0 ^ 2 ≤ 1tail:∀ x ∈ Set.Ioc 0 1, x ^ 2 ≤ 1x:ℝhx:x ∈ Set.Icc 0 1⊢ x ^ 2 ≤ 1
  rcases eq_or_lt_of_le hx.1 with h | hinlendpoint:0 ^ 2 ≤ 1tail:∀ x ∈ Set.Ioc 0 1, x ^ 2 ≤ 1x:ℝhx:x ∈ Set.Icc 0 1h:0 = x⊢ x ^ 2 ≤ 1inrendpoint:0 ^ 2 ≤ 1tail:∀ x ∈ Set.Ioc 0 1, x ^ 2 ≤ 1x:ℝhx:x ∈ Set.Icc 0 1h:0 < x⊢ x ^ 2 ≤ 1
  ·inlendpoint:0 ^ 2 ≤ 1tail:∀ x ∈ Set.Ioc 0 1, x ^ 2 ≤ 1x:ℝhx:x ∈ Set.Icc 0 1h:0 = x⊢ x ^ 2 ≤ 1 subst xinlendpoint:0 ^ 2 ≤ 1tail:∀ x ∈ Set.Ioc 0 1, x ^ 2 ≤ 1hx:0 ∈ Set.Icc 0 1⊢ 0 ^ 2 ≤ 1
    exact endpointAll goals completed! 🐙
  ·inrendpoint:0 ^ 2 ≤ 1tail:∀ x ∈ Set.Ioc 0 1, x ^ 2 ≤ 1x:ℝhx:x ∈ Set.Icc 0 1h:0 < x⊢ x ^ 2 ≤ 1 exact tail x ⟨h, hx.2⟩All goals completed! 🐙

The open-interval rewrite is likewise accepted directly:

example : ∀ x : ℝ,
    x ∈ Set.Ioc (0 : ℝ) 1 → x ≠ 1 → x < 1 := by⊢ ∀ x ∈ Set.Ioc 0 1, x ≠ 1 → x < 1
  rcfAll goals completed! 🐙

example : ∃ x : ℝ,
    x ∈ Set.Ioc (0 : ℝ) 1 ∧ x = 1 / 2 ∧ x ≠ 1 := by⊢ ∃ x ∈ Set.Ioc 0 1, x = 1 / 2 ∧ x ≠ 1
  rcfAll goals completed! 🐙

When rcf sees Set.Icc or Set.Ioo directly, its error message includes the corresponding rewrite above.