use efficiently #reduce inside of tactics mode?

Stream: new members

[Elif Sacikara (Alumni)]

Hello,
When we (with Ödül and some colleagues from the Institute) tried to prove that any function from a discrete topological space to any other topological space is continuous, as we attempted to state it in Thm discrete_left_adj_forget by the code below, we have seen the corresponding infoview in Lean, respectively.
Lean code:

 ∀ (U : set Y), (Y_top.is_open U) → (X_top.is_open (preimage f U))
def top_discrete (X : Type) : topological_space X := topological_space.mk
(λ (S : set X), true)
(trivial)
(begin
    intros H1 H2 H3 H4,
     trivial,
end)
(begin
 intros H1 H2,
trivial,
end)
theorem discrete_left_adjoint_forget {X : Type} : ∀ {Y : Type}
(Y_top : topological_space Y) (f : X → Y), continuous (top_discrete X) Y_top f :=
begin
intros Y Y_top f,
intros U,
end

Lean infoview:

Y_top: topological_space Y
 f: X → Y
 U: set Y
 U_open: Y_top.is_open U
 ⊢ (top_discrete X).is_open (f ⁻¹' U)

"We would like to evaluate this function (top_discrete X).is_open (preimage f U) to be "true’’ in Lean infoview, since in top_discrete’’ we defined this function using the lambda expression which turns out to be "True". When we #reduce (top_discrete X).is_open (preimage f U) outside of the tactics mode, then it evaluates it as being "true". So even though it can do it outside of tactics mode, this is not the case inside of the proof and now we are trying to find a way to make lean show that this expression is as true inside of proof.

Thanks in advance.

[Kevin Buzzard]

(deleted)

[Patrick Massot]

Could you read the link #mwe and adjust your post so that it becomes much easier to help you,

[Patrick Massot]

I moved the post to a new thread

[Kevin Buzzard]

yes, it's much easier to help if we can just cut and paste what you post -- so add in the imports, definitions etc

[Eric Wieser]

It looks like something has gone wrong with the #backticks above

[Kevin Buzzard]

Yes, the triple back ticks need to be on a line of their own like in #backticks

[Patrick Massot]

I still tried to reconstruct the #mwe and arrived at:

import topology.basic

open set

def cont {X Y : Type*} (X_top : topological_space X) (Y_top : topological_space Y) (f : X → Y) :=
  ∀ (U : set Y), (Y_top.is_open U) → (X_top.is_open (preimage f U))

def top_discrete (X : Type) : topological_space X := topological_space.mk
(λ (S : set X), true)
(trivial)
(begin
    intros H1 H2 H3 H4,
     trivial,
end)
(begin
 intros H1 H2,
trivial,
end)

theorem discrete_left_adjoint_forget {X : Type} : ∀ {Y : Type}
(Y_top : topological_space Y) (f : X → Y), cont (top_discrete X) Y_top f :=
begin
  intros Y Y_top f,
  intros U U_open,
  trivial
end

I don't really see any question here.

[Patrick Massot]

And I need to go to bed now, sorry.

[Reid Barton]

There's no tactic that applies #reduce to the current goal, but since you already know the goal reduces to true you can change the goal with change true, or just provide a proof of true directly with trivial.

[Eric Wieser]

I think the answer is dsimp only [top_discrete], if the question is what I think it is

[Elif Sacikara (Alumni)]

Reid Barton said:

There's no tactic that applies #reduce to the current goal, but since you already know the goal reduces to true you can change the goal with change true, or just provide a proof of true directly with trivial.

Thanks for the comment and the suggestion. We can complete the proof by "trivial" for sure but we suppose that some day in the future while we are working in a long proof and while doing so when we give our definition a while ago before our proof and if we suppose that we do not remember if it exactly turns out to be ``true" in the definition, is there is a way of seeing this value inside of the proof or a way of making Lean possible to do it?

[Kevin Buzzard]

If you open a quote with ` then close it with ` and not " (you can just edit your post just above)

[Elif Sacikara (Alumni)]

This is a full code, sorry for the clumsiness:

import tactic
open set

class topological_space (X : Type) :=
 (is_open : set X → Prop)
 (is_open_univ : is_open univ)
 (is_open_inter : ∀ U V : set X, is_open U → is_open V → is_open (U ∩ V))
 (is_open_sUnion : ∀ C : set (set X), (∀ U ∈ C, is_open U) → is_open (sUnion C))

#check topological_space.is_open_univ

 lemma empty_set_open {X : Type} [topological_space X]  : topological_space.is_open (∅ : set X)  :=
 begin
   have hEmptyUnion := topological_space.is_open_sUnion ∅,
   have H2 : ∀ U : set X, U ∈ ∅ → false := begin exact not_mem_empty end,

   rw sUnion_empty at hEmptyUnion,
   apply hEmptyUnion,
   intro h,
   have H4 := H2 h,
   intro h1,
   exfalso,
   exact H4 h1,
 end

lemma finite_inter_open {X : Type} [topological_space X] (C : set (set X))
 (hC : finite C) : (∀ x ∈ C, topological_space.is_open x) → topological_space.is_open (sInter C) :=
 begin
   apply finite.induction_on hC,
   rw sInter_empty,
   {
     intro H,
     exact topological_space.is_open_univ,
   },
   intros a s a_not_in_s s_finite s_family_open hAllOpen,
   rw sInter_insert,
   apply topological_space.is_open_inter,
   {
     apply hAllOpen,
     simp,
   },
   {
     apply s_family_open,
     intro F,
     have f_aux := hAllOpen F,
     intro H_aux_2,
     apply f_aux,
     exact mem_insert_of_mem a H_aux_2,
   }
 end

def continuous {X Y : Type} [topological_space X] [topological_space Y] (f : X → Y) : Prop :=
 ∀ (U : set Y), (topological_space.is_open U) → (topological_space.is_open (preimage f U))

def top_discrete (X : Type) : topological_space X := topological_space.mk
 (λ (S : set X), true)
 (trivial)
 (
   begin
     intros H1 H2 H3 H4,
     trivial,
   end
 )
 (
   begin
     intros H1 H2,
     trivial,
   end
 )

[Kevin Buzzard]

You can reduce things by hand in the middle of a proof, using tactics like dunfold, delta and dsimp