targetted definitional reduction

Stream: general

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

and I was told that this theorem had no name

[Kevin Buzzard]

because it was true by refl

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

"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

[Kevin Buzzard]

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

[Kevin Buzzard]

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!

[Kevin Buzzard]

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

[Kevin Buzzard]

and the line after my show line was a complicated rw

[Kevin Buzzard]

Here's what I want to do

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

Is this possible?

[Kevin Buzzard]

I don't think so.

[Kevin Buzzard]

conv offers me exciting commands such as "to_lhs"

[Kevin Buzzard]

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

[Kevin Buzzard]

Can conv do that?

[Kevin Buzzard]

Can I do dsimp in conv?

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

I can do dsimp in conv mode :-)

[Kevin Buzzard]

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

[Kevin Buzzard]

goal is f x y = g z

[Kevin Buzzard]

and I want to run dsimp on y only

[Kevin Buzzard]

how do I do that?

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

This gets me back to the original problem though

[Kevin Buzzard]

I do not want to run dsimp in my head

[Kevin Buzzard]

I am too lazy

[Kevin Buzzard]

I am a big boy now

[Mario Carneiro]

what's wrong with dsimp?

[Kevin Buzzard]

simplifies too much

[Kevin Buzzard]

that's the wrong question

[Mario Carneiro]

no, that's the standard solution

[Kevin Buzzard]

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

[Kevin Buzzard]

Let me go back to my usage case

[Mario Carneiro]

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

[Chris Hughes]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

and function x y z creates a structure

[Kevin Buzzard]

by saying what all the bits and pieces are

[Kevin Buzzard]

including F

[Kevin Buzzard]

dsimp does nothing

[Kevin Buzzard]

I can't get conv to get to it

[Kevin Buzzard]

is it because it's a pi type?

[Kevin Buzzard]

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

[Kevin Buzzard]

That can't be the best way

[Kevin Buzzard]

that's not even true

[Kevin Buzzard]

#reduce didn't do it

[Kevin Buzzard]

no wait

[Kevin Buzzard]

it half did it

[Kevin Buzzard]

it did enough of it

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

What my code looks like

[Kevin Buzzard]

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)

[Mario Carneiro]

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

[Mario Carneiro]

alternatively, you can dsimp [function] to unfold it

[Kevin Buzzard]

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?

[Kevin Buzzard]

alternatively, you can dsimp [function] to unfold it

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

like (f x y z).F

[Mario Carneiro]

right