Zulip Chat Archive

Stream: general

Topic: rext


Reid Barton (Sep 07 2018 at 10:41):

How about rext = ext + rintros? Is this going too far?

Reid Barton (Sep 07 2018 at 10:41):

Or ext + rcases depending on your point of view

Simon Hudon (Sep 07 2018 at 18:49):

That shouldn't be too hard. I thought of doing it before but I had to change the import structure to do it so in the end I didn't bother

Simon Hudon (Sep 09 2018 at 01:59):

@Reid Barton I just pushed this branch: https://travis-ci.org/leanprover/mathlib/builds/426239546 please let me know if it does what you wanted

Scott Morrison (Sep 09 2018 at 02:13):

Looks like there are problems in

/home/travis/build/leanprover/mathlib/tactic/pi_instances.lean:25:14: error: type mismatch at application
  cons x
term
  x
has type
  name
but is expected to have type
  rcases_patt

Simon Hudon (Sep 09 2018 at 02:15):

I prefer to think of it as undocumented feature :D

Scott Morrison (Sep 09 2018 at 02:17):

:-)

Simon Hudon (Sep 09 2018 at 03:47):

The documentation of that feature is getting complicated, I'll just remove it

Reid Barton (Sep 09 2018 at 11:38):

Simon I've just finished building mathlib with your patch; about to try it on my example (although it will require some preparatory work).

Simon Hudon (Sep 09 2018 at 11:39):

:fingers_crossed:

Reid Barton (Sep 09 2018 at 11:48):

I see ext no longer applied propext to my goal, is that intentional?

Reid Barton (Sep 09 2018 at 11:49):

I had something like (\lam a b, f a b) = (\lam a b, g a b) and I want to intro a and b and get the goal f a b \iff g a b -- where f a b and g a b are propositions

Reid Barton (Sep 09 2018 at 11:50):

anyways, it worked! I changed

ext a₁ a₂, rcases a₁ with ⟨⟨i'₁, f₁, j₁, rcases a₂ with ⟨⟨i'₂, f₂, j₂,

to

ext ⟨⟨i'₁, f₁, j₁ ⟨⟨i'₂, f₂, j₂,

Simon Hudon (Sep 09 2018 at 11:52):

It is not intentional. Can you find where propext is labelled with extentionality?

Reid Barton (Sep 09 2018 at 11:53):

It... doesn't appear to be so marked anywhere that I can find

Reid Barton (Sep 09 2018 at 11:54):

Is there a way to tell ext to trace what it is doing?

Johannes Hölzl (Sep 09 2018 at 11:57):

rext is very nice!

Reid Barton (Sep 09 2018 at 11:57):

Wait, maybe it never used to apply propext? I might have been confused because set.ext is very similar.

Simon Hudon (Sep 09 2018 at 12:01):

I think that's probably it

Simon Hudon (Sep 09 2018 at 12:02):

We can add it though

Simon Hudon (Sep 09 2018 at 12:02):

Check what happens if you add attribute [extensionality] propext before your proof.

Reid Barton (Sep 09 2018 at 12:03):

only constants and Pi types are supported: Prop

Reid Barton (Sep 09 2018 at 12:05):

Aha, I understand why the behavior changed.
Before, it applied funext once and then, by chance, it happened to apply set.ext which is funext plus propext.
Now, it (correctly) prefers to apply funext twice and then it gets stuck.

Simon Hudon (Sep 09 2018 at 12:08):

:face_palm: oh dear! I was discussing this with Mario and saying that each type we care about is a named constant ... except for pi types. And now, the type of Prop is also not names so I have to think about making more exceptions

Reid Barton (Sep 09 2018 at 12:12):

expr.sort, I guess?

Reid Barton (Sep 09 2018 at 12:12):

Also don't forget to implement univalence for equalities between types

Simon Hudon (Sep 09 2018 at 12:14):

Now then next exception should be easier to add. Can you send me your example so that I can try it out?

Reid Barton (Sep 09 2018 at 12:15):

I think I included one in the github issue (my real one has some dependencies)

Reid Barton (Sep 09 2018 at 12:15):

But I can also provide it

Simon Hudon (Sep 09 2018 at 12:18):

Or a link to the issue please

Reid Barton (Sep 09 2018 at 12:18):

https://gist.github.com/rwbarton/1966db9e4ba470f2a5865f5086776f84, it should compile against your branch

Reid Barton (Sep 09 2018 at 12:18):

https://github.com/leanprover/mathlib/issues/246

Reid Barton (Sep 09 2018 at 12:18):

import data.set
example {α : Type} (f g : α  α  Prop) : f = g := begin
  ext a b,
  -- ⊢ b ∈ f a ↔ b ∈ g a
end

Reid Barton (Sep 09 2018 at 12:19):

My real example is no more interesting than this as far as the propext issue is concerned--it's just a test case for the rext feature.

Simon Hudon (Sep 09 2018 at 12:34):

Cool, that works now. I'll push it and then get some sleep :)

Reid Barton (Sep 09 2018 at 12:36):

(Wait aren't we in the same time zone...)

Simon Hudon (Sep 09 2018 at 12:37):

Are you on the east coast of the US?

Simon Hudon (Sep 09 2018 at 12:37):

But to answer your surprise, when I program, time flies and I forget to do all kinds of stuff

Simon Hudon (Sep 09 2018 at 12:38):

... including sleeping

Reid Barton (Sep 09 2018 at 12:40):

Yes. But still have not adjusted from being in Europe and have been up for 4 hours today...

Simon Hudon (Sep 09 2018 at 12:41):

Were you in the UK? You seem to be driving on the wrong side of the road ... the road being a stand-in for the night, and the wrong side is being awake after 4 rather than awake until 4 :D

Simon Hudon (Sep 09 2018 at 12:42):

Yeah, my metaphors are not that enlightening ...

Reid Barton (Sep 09 2018 at 12:42):

So we seem to be off by a full 12 hours from each other, yes

Simon Hudon (Sep 09 2018 at 12:44):

For today at least


Last updated: Aug 03 2023 at 10:10 UTC