Open
Description
/-
rev: 47f3e6393d35a7c9579fda04fa07bc81aa18a4b9
-/
import Mathlib.Topology.Closure
universe u
/- I found this issue while trying to prove such a goal. -/
/--
error:
gcongr failed, no @[gcongr] lemma applies for the template portion closure ?m.287 and the relation
LE.le
-/
#guard_msgs in
example {α : Type u} [TopologicalSpace α] {s t u : Set α}
(hst : s ⊆ t) (htu : Disjoint (closure t) u) : Disjoint (closure s) u := by
grewrite [← hst] at htu; assumption
/- First, I confirmed that there is no major bug in the mechanism of `grewrite` itself by checking
that it succeeds when changing `Disjoint s t` to `s ∩ t ⊆ ∅`. -/
/--
info:
protected theorem Set.disjoint_iff.{u} : ∀ {α : Type u} {s t : Set α}, Disjoint s t ↔ s ∩ t ⊆ ∅
-/
#guard_msgs in
#print sig Set.disjoint_iff
example {α : Type u} [TopologicalSpace α] {s t u : Set α}
(hst : s ⊆ t) (htu : Disjoint (closure t) u) : Disjoint (closure s) u := by
rewrite [Set.disjoint_iff] at htu ⊢
grewrite [← hst] at htu; assumption
/- From the error message and the registered `gcongr` lemmas, I think the error occurs in the
following flow. -/
example {α : Type*} [TopologicalSpace α] {s t u : Set α}
(hst : s ⊆ t) (htu : Disjoint (closure t) u) : Disjoint (closure s) u := by
-- First, apply the `Disjoint.mono` of the `gcongr` lemma, and solve the rfl goal.
revert htu; apply Disjoint.mono; any_goals rfl
-- Then, the goal becomes `closure s ≤ closure t` instead of `closure s ⊆ closure t`.
guard_target = closure s ≤ closure t
-- Because of this, I can't solve the goal with `gcongr` lemma's `closure_mono`.
fail_if_success with_reducible apply closure_mono
-- If I could change `closure s ⊆ closure t` to `closure s ≤ closure t`, I could solve it.
fail_if_success gcongr
rw [Set.le_iff_subset]; gcongr
/- The first solution that comes to mind is to register the lemma
`s₁ ⊆ s₂, t₁ ⊆ t₂ ⊢ Disjoint s₂ t₂ → Disjoint s₁ t₁` as a `gcongr` lemma, but in `gcongr`, only the
first registered lemma is valid for the same goal, so it cannot be used. -/
@[gcongr]
lemma Set.disjoint_mono {α : Type u} {s₁ s₂ t₁ t₂ : Set α} (hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) :
Disjoint s₂ t₂ → Disjoint s₁ t₁ :=
Disjoint.mono hs ht
/--
error:
unsolved goals
case h
α : Type u
inst✝ : TopologicalSpace α
s t u : Set α
hst : s ⊆ t
⊢ closure s ≤ closure t
-/
#guard_msgs in
example {α : Type u} [TopologicalSpace α] {s t u : Set α}
(hst : s ⊆ t) : Disjoint (closure t) u → Disjoint (closure s) u := by
gcongr
/--
error:
gcongr failed, no @[gcongr] lemma applies for the template portion closure ?m.4578 and the relation
LE.le
-/
#guard_msgs in
example {α : Type u} [TopologicalSpace α] {s t u : Set α}
(hst : s ⊆ t) (htu : Disjoint (closure t) u) : Disjoint (closure s) u := by
grewrite [← hst] at htu; assumption
/- Next, another solution that comes to mind is to register the lemma `s ⊆ t ⊢ s ≤ t` as a `gcongr`
lemma, but it cannot be registered because both sides are free variables. -/
/--
info:
theorem HasSubset.Subset.le.{u} : ∀ {α : Type u} {s t : Set α}, s ⊆ t → s ≤ t
-/
#guard_msgs in
#print sig HasSubset.Subset.le
/--
error:
@[gcongr] attribute only applies to lemmas proving f x₁ ... xₙ ∼ f x₁' ... xₙ'.
LHS is not suitable for congruence in the conclusion of ∀ {α : Type u} {s t : Set α}, s ⊆ t → s ≤ t
-/
#guard_msgs in
attribute [gcongr] HasSubset.Subset.le
/--
error:
@[gcongr] attribute only applies to lemmas proving f x₁ ... xₙ ∼ f x₁' ... xₙ'.
LHS is not suitable for congruence in the conclusion of ∀ {α : Type u} {s t : Set α}, s ⊆ t → s ≤ t
-/
#guard_msgs in
@[gcongr]
lemma HasSubset.Subset.le₂ {α : Type u} {s t : Set α} : s ⊆ t → s ≤ t :=
HasSubset.Subset.le
/--
error:
@[gcongr] attribute only applies to lemmas proving f x₁ ... xₙ ∼ f x₁' ... xₙ'.
LHS is not suitable for congruence in the conclusion of ∀ {α : Type u} {s t : Set α}, s ⊆ t → s ≤ t
-/
#guard_msgs in
@[gcongr]
lemma HasSubset.Subset.le₃ {α : Type u} {s t : Set α} (h : s ⊆ t) : s ≤ t :=
h.le
/- Also, even if you use `gcongr_forward`, you can only prove the goal as `s ⊆ t ⊢ s ≤ t` as it is,
and you cannot prove goals like `s ⊆ t ⊢ closure s ≤ closure t`. -/
/--
error:
gcongr did not make progress
-/
#guard_msgs in
example {α : Type u} {s t : Set α} (h : s ⊆ t) : s ≤ t := by
gcongr
open Lean Meta in
@[gcongr_forward]
def Mathlib.Tactic.GCongr.leOfSubset : ForwardExt where
eval h goal := do goal.assignIfDefEq (← mkAppM ``HasSubset.Subset.le #[h])
example {α : Type u} {s t : Set α} (h : s ⊆ t) : s ≤ t := by
gcongr
/--
error:
gcongr did not make progress
-/
#guard_msgs in
example {α : Type u} [TopologicalSpace α] {s t : Set α} (h : s ⊆ t) : closure s ≤ closure t := by
gcongr
/--
error:
gcongr failed, no @[gcongr] lemma applies for the template portion closure ?m.6092 and the relation
LE.le
-/
#guard_msgs in
example {α : Type u} [TopologicalSpace α] {s t u : Set α}
(hst : s ⊆ t) (htu : Disjoint (closure t) u) : Disjoint (closure s) u := by
grewrite [← hst] at htu; assumption
/- This is considered to occur when the `gcongr` normal form `s ≤ t` becomes `s ⊆ t` when
`s` and `t` are `Set`. Therefore, my proposed solution is to register such specialized propositions
using attributes like `gcongr_specialize`.
-/
/-
```lean
/--
info:
[Meta.gcongr_specialize] type: Set _ ⊢ _ ≤ _ ⤳ _ ⊆ _
-/
#guard_msgs in
set_option trace.Meta.gcongr_specialize
attribute [gcongr_specialize] HasSubset.Subset.le
example {α : Type u} [TopologicalSpace α] {s t u : Set α}
(hst : s ⊆ t) (htu : Disjoint (closure t) u) : Disjoint (closure s) u := by
grewrite [← hst] at htu; assumption
```
-/
Metadata
Metadata
Assignees
Labels
No labels