Zulip Chat Archive

Stream: general

Topic: targetted definitional reduction


view this post on Zulip Kevin Buzzard (May 29 2018 at 11:36):

The history of this question is the following: I had a complicated goal which could be reduced using a definitional unfolding which for some reason wasn't happening -- "unfold" wouldn't work

view this post on Zulip Kevin Buzzard (May 29 2018 at 11:36):

I wanted to do the unfold manually with a rw so I asked the name of the theorem that {a := x, b := y}.a = x

view this post on Zulip Kevin Buzzard (May 29 2018 at 11:37):

and I was told that this theorem had no name

view this post on Zulip Kevin Buzzard (May 29 2018 at 11:37):

because it was true by refl

view this post on Zulip Kevin Buzzard (May 29 2018 at 11:37):

On the other hand, browsing through the library I see a bunch of things with names whose proof is rfl

view this post on Zulip Kevin Buzzard (May 29 2018 at 11:38):

All the other suggestions for what to do were not good for me.

view this post on Zulip Kevin Buzzard (May 29 2018 at 11:38):

"Change it yourself with show" -- yeah but this is a PITA because my structure is a very complicated structure with a very long name and it is being constructed using very long terms

view this post on Zulip Kevin Buzzard (May 29 2018 at 11:38):

and I know precisely how I want this precise term to unfold and I don't want to do anything else to the goal

view this post on Zulip Kevin Buzzard (May 29 2018 at 11:39):

If I change it myself with show then I have to work out what I want the goal to be using pencil and paper! It's 2018!

view this post on Zulip Kevin Buzzard (May 29 2018 at 11:39):

I _need_ to change it because rw is really fussy, it won't rw something defeq to what you want sometimes -- it sometimes needs help

view this post on Zulip Kevin Buzzard (May 29 2018 at 11:39):

and the line after my show line was a complicated rw

view this post on Zulip Kevin Buzzard (May 29 2018 at 11:40):

Here's what I want to do

view this post on Zulip Kevin Buzzard (May 29 2018 at 11:40):

I want to zoom in to the area I am interested in using conv

view this post on Zulip Kevin Buzzard (May 29 2018 at 11:40):

and I want to run dsimp or some such thing just on that one term

view this post on Zulip Kevin Buzzard (May 29 2018 at 11:40):

Is this possible?

view this post on Zulip Kevin Buzzard (May 29 2018 at 11:40):

I don't think so.

view this post on Zulip Kevin Buzzard (May 29 2018 at 11:40):

conv offers me exciting commands such as "to_lhs"

view this post on Zulip Kevin Buzzard (May 29 2018 at 11:41):

what about "to 3rd input of this function"?

view this post on Zulip Kevin Buzzard (May 29 2018 at 11:41):

Can conv do that?

view this post on Zulip Kevin Buzzard (May 29 2018 at 11:41):

Can I do dsimp in conv?

view this post on Zulip Kevin Buzzard (May 29 2018 at 11:41):

I use tactic mode precisely because I like the precise control I have over what is going on

view this post on Zulip Kevin Buzzard (May 29 2018 at 11:41):

but as I get older and wiser and understand more about what is happening, I want more precise tools

view this post on Zulip Kevin Buzzard (May 29 2018 at 11:42):

I can do dsimp in conv mode :-)

view this post on Zulip Kevin Buzzard (May 29 2018 at 11:42):

so my question becomes how to access the 3rd input to a function

view this post on Zulip Kevin Buzzard (May 29 2018 at 11:42):

goal is f x y = g z

view this post on Zulip Kevin Buzzard (May 29 2018 at 11:43):

and I want to run dsimp on y only

view this post on Zulip Kevin Buzzard (May 29 2018 at 11:43):

how do I do that?

view this post on Zulip Kevin Buzzard (May 29 2018 at 11:43):

Ok I just thought of a solution which again will work in many cases

view this post on Zulip Kevin Buzzard (May 29 2018 at 11:43):

just define exactly the rewrite I want, call it H, and rw H

view this post on Zulip Kevin Buzzard (May 29 2018 at 11:43):

This gets me back to the original problem though

view this post on Zulip Kevin Buzzard (May 29 2018 at 11:43):

I do not want to run dsimp in my head

view this post on Zulip Kevin Buzzard (May 29 2018 at 11:43):

I am too lazy

view this post on Zulip Kevin Buzzard (May 29 2018 at 11:44):

I am a big boy now

view this post on Zulip Mario Carneiro (May 29 2018 at 11:44):

what's wrong with dsimp?

view this post on Zulip Kevin Buzzard (May 29 2018 at 11:44):

simplifies too much

view this post on Zulip Kevin Buzzard (May 29 2018 at 11:44):

that's the wrong question

view this post on Zulip Mario Carneiro (May 29 2018 at 11:44):

no, that's the standard solution

view this post on Zulip Kevin Buzzard (May 29 2018 at 11:44):

unless you are genuinely convinced that I really never want to run dsimp on just a subterm

view this post on Zulip Kevin Buzzard (May 29 2018 at 11:45):

Let me go back to my usage case

view this post on Zulip Mario Carneiro (May 29 2018 at 11:45):

you can use dsimp only or other such tricks to limit the unnecessary simping

view this post on Zulip Chris Hughes (May 29 2018 at 15:35):

unfold structure.a sometimes works for me in these situations.

view this post on Zulip Kevin Buzzard (May 29 2018 at 18:29):

In my usage case, dsimp doesn't do anything at all

view this post on Zulip Kevin Buzzard (May 29 2018 at 18:37):

the goal is (function x y z).F H -> Z`

view this post on Zulip Kevin Buzzard (May 29 2018 at 18:37):

and function x y z creates a structure

view this post on Zulip Kevin Buzzard (May 29 2018 at 18:37):

by saying what all the bits and pieces are

view this post on Zulip Kevin Buzzard (May 29 2018 at 18:37):

including F

view this post on Zulip Kevin Buzzard (May 29 2018 at 18:37):

dsimp does nothing

view this post on Zulip Kevin Buzzard (May 29 2018 at 18:38):

I can't get conv to get to it

view this post on Zulip Kevin Buzzard (May 29 2018 at 18:38):

is it because it's a pi type?

view this post on Zulip Kevin Buzzard (May 29 2018 at 18:39):

In the end I copied the context, scrolled to the end of the proof, pasted it, changed X : y, to (X : y) about ten times and made them all variables, and then used #reduce and then cut and pasted the answer back in the proof and wrote "show" in front of it, and then farted around with some pp.proof on to get it to work and I was done

view this post on Zulip Kevin Buzzard (May 29 2018 at 18:39):

That can't be the best way

view this post on Zulip Kevin Buzzard (May 29 2018 at 18:40):

that's not even true

view this post on Zulip Kevin Buzzard (May 29 2018 at 18:40):

#reduce didn't do it

view this post on Zulip Kevin Buzzard (May 29 2018 at 18:40):

no wait

view this post on Zulip Kevin Buzzard (May 29 2018 at 18:40):

it half did it

view this post on Zulip Kevin Buzzard (May 29 2018 at 18:40):

it did enough of it

view this post on Zulip Kevin Buzzard (May 29 2018 at 18:40):

it unfolded (function x y z).F into (some function of x y and z)

view this post on Zulip Kevin Buzzard (May 29 2018 at 18:41):

Why did this cause me such pain? What did I miss?

view this post on Zulip Kevin Buzzard (May 29 2018 at 18:50):

import analysis.topology.topological_space scheme

set_option pp.proofs true

theorem presheaves_iso (X : Type) [H : topological_space X] (F : presheaf_of_types X) :
are_isomorphic_presheaves_of_types
    (presheaf_of_types_pullback_under_open_immersion F id
      (topological_space.open_immersion_id _))
    F
:=
begin
  constructor,tactic.swap,
  { constructor,tactic.swap,
    { intros U HU,
      have Hid := topological_space.open_immersion_id X,
      -- goal now
      show (presheaf_of_types_pullback_under_open_immersion F id Hid).F HU  F.F HU,
      --unfold presheaf_of_types_pullback_under_open_immersion, -- fails
      show (F.F ((Hid.fopens U).mp HU))  F.F HU, -- obtained by "#reduce" calculation below
      show (F.F (_ : is_open (id '' U))  F.F HU), -- obtained by more out-of-proof unravelling

      sorry
    },sorry,

  },
  sorry
end
variables
(X : Type)
(H : topological_space X)
(F : presheaf_of_types X)
(U : set X)
(HU : topological_space.is_open H U)
(Hid : topological_space.open_immersion (@id X))

#reduce (presheaf_of_types_pullback_under_open_immersion F id Hid).F
-- λ (U : X → Prop) (HU : topological_space.is_open H U), F.F ((Hid.fopens U).mp HU)
#check (Hid.fopens U).mp -- is_open U → is_open (id '' U)


#exit

view this post on Zulip Kevin Buzzard (May 29 2018 at 18:50):

What my code looks like

view this post on Zulip Kevin Buzzard (May 29 2018 at 18:58):

It doesn't run for people who don't have my repo because it needs scheme.lean but I hope it explicitly shows the problem. I don't know how to get Lean to unfold (presheaf_of_types_pullback_under_open_immersion F id Hid).F, possibily because it's in a lambda, but it is defeq to something much simpler which I work out outside the proof after some copying of context (IRL the context was huge and I just did the unravelling using cut and paste)

view this post on Zulip Mario Carneiro (May 29 2018 at 18:59):

You should have a simp lemma for the value of .F

view this post on Zulip Mario Carneiro (May 29 2018 at 19:00):

alternatively, you can dsimp [function] to unfold it

view this post on Zulip Kevin Buzzard (May 29 2018 at 22:37):

You should have a simp lemma for the value of .F

Talking through pnat was very instructional. I realise that I have a very poor feeling about what should be a simp lemma. I made that structure though -- these lemmas aren't automatically added when I make the structure? What is added to the simp machine?

view this post on Zulip Kevin Buzzard (May 29 2018 at 22:37):

alternatively, you can dsimp [function] to unfold it

This is what I needed to know :-) Thanks!

view this post on Zulip Kevin Buzzard (May 29 2018 at 22:38):

Even though my function isn't a simp lemma :-)

view this post on Zulip Mario Carneiro (May 29 2018 at 22:38):

simp will reduce terms that look like <a, b, c>.2

view this post on Zulip Mario Carneiro (May 29 2018 at 22:38):

where <> is the builtin structure constructor and .2 is a builtin projection

view this post on Zulip Mario Carneiro (May 29 2018 at 22:39):

If there are any definitions shielding the redex from looking like that, simp won't find it

view this post on Zulip Kevin Buzzard (May 29 2018 at 22:39):

like (f x y z).F

view this post on Zulip Mario Carneiro (May 29 2018 at 22:39):

right


Last updated: May 09 2021 at 19:11 UTC