## 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

:-)

#### 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):

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

#### 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: May 13 2021 at 16:25 UTC