rext

Stream: general

[Reid Barton]

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

[Reid Barton]

Or ext + rcases depending on your point of view

[Simon Hudon]

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]

@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]

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]

I prefer to think of it as undocumented feature :D

[Scott Morrison]

:-)

[Simon Hudon]

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

[Reid Barton]

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]

:fingers_crossed:

[Reid Barton]

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

[Reid Barton]

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]

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]

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

[Reid Barton]

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

[Reid Barton]

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

[Johannes Hölzl]

rext is very nice!

[Reid Barton]

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

[Simon Hudon]

I think that's probably it

[Simon Hudon]

We can add it though

[Simon Hudon]

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

[Reid Barton]

only constants and Pi types are supported: Prop

[Reid Barton]

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]

: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]

expr.sort, I guess?

[Reid Barton]

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

[Simon Hudon]

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

[Reid Barton]

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

[Reid Barton]

But I can also provide it

[Simon Hudon]

Or a link to the issue please

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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]

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

[Reid Barton]

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

[Simon Hudon]

Are you on the east coast of the US?

[Simon Hudon]

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

[Simon Hudon]

... including sleeping

[Reid Barton]

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

[Simon Hudon]

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]

Yeah, my metaphors are not that enlightening ...

[Reid Barton]

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

[Simon Hudon]

For today at least