Zulip Chat Archive

Stream: general

Topic: rext


view this post on Zulip Reid Barton (Sep 07 2018 at 10:41):

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

view this post on Zulip Reid Barton (Sep 07 2018 at 10:41):

Or ext + rcases depending on your point of view

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Simon Hudon (Sep 09 2018 at 02:15):

I prefer to think of it as undocumented feature :D

view this post on Zulip Scott Morrison (Sep 09 2018 at 02:17):

:-)

view this post on Zulip Simon Hudon (Sep 09 2018 at 03:47):

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

view this post on Zulip 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).

view this post on Zulip Simon Hudon (Sep 09 2018 at 11:39):

:fingers_crossed:

view this post on Zulip Reid Barton (Sep 09 2018 at 11:48):

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

view this post on Zulip 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

view this post on Zulip 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₂,

view this post on Zulip Simon Hudon (Sep 09 2018 at 11:52):

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

view this post on Zulip Reid Barton (Sep 09 2018 at 11:53):

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

view this post on Zulip Reid Barton (Sep 09 2018 at 11:54):

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

view this post on Zulip Johannes Hölzl (Sep 09 2018 at 11:57):

rext is very nice!

view this post on Zulip 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.

view this post on Zulip Simon Hudon (Sep 09 2018 at 12:01):

I think that's probably it

view this post on Zulip Simon Hudon (Sep 09 2018 at 12:02):

We can add it though

view this post on Zulip Simon Hudon (Sep 09 2018 at 12:02):

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

view this post on Zulip Reid Barton (Sep 09 2018 at 12:03):

only constants and Pi types are supported: Prop

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Reid Barton (Sep 09 2018 at 12:12):

expr.sort, I guess?

view this post on Zulip Reid Barton (Sep 09 2018 at 12:12):

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

view this post on Zulip 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?

view this post on Zulip Reid Barton (Sep 09 2018 at 12:15):

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

view this post on Zulip Reid Barton (Sep 09 2018 at 12:15):

But I can also provide it

view this post on Zulip Simon Hudon (Sep 09 2018 at 12:18):

Or a link to the issue please

view this post on Zulip Reid Barton (Sep 09 2018 at 12:18):

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

view this post on Zulip Reid Barton (Sep 09 2018 at 12:18):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Simon Hudon (Sep 09 2018 at 12:34):

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

view this post on Zulip Reid Barton (Sep 09 2018 at 12:36):

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

view this post on Zulip Simon Hudon (Sep 09 2018 at 12:37):

Are you on the east coast of the US?

view this post on Zulip 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

view this post on Zulip Simon Hudon (Sep 09 2018 at 12:38):

... including sleeping

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip Simon Hudon (Sep 09 2018 at 12:42):

Yeah, my metaphors are not that enlightening ...

view this post on Zulip Reid Barton (Sep 09 2018 at 12:42):

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

view this post on Zulip Simon Hudon (Sep 09 2018 at 12:44):

For today at least


Last updated: May 13 2021 at 16:25 UTC