Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: Flat rintro


view this post on Zulip Patrick Massot (Jan 22 2021 at 10:41):

@Mario Carneiro Do you think it would be possible to write an intro tactic that does rintros in a flattened way? I'm not asking for mathlib inclusion, this is part of my controlled natural language for teaching experimentation. I'd like

example (P Q : Prop) : Q  P  Q  P :=
begin
  my_intro (hQ : Q) (hP : P) (hQ' : Q),
  exact hP
end

to work.

view this post on Zulip Mario Carneiro (Jan 22 2021 at 16:08):

doesn't rintro do that already?

view this post on Zulip Bryan Gin-ge Chen (Jan 22 2021 at 16:10):

I think Patrick wants to avoid these angle brackets:

import tactic

example (P Q : Prop) : Q  P  Q  P :=
begin
  rintro (hQ : Q) ⟨(hP : P), (hQ : Q)⟩,
  exact hP
end

view this post on Zulip Eric Wieser (Jan 22 2021 at 16:12):

Presumably the heuristic Patrick wants is "insert angle brackets until the type annotation unifies with the field", as opposed to "unfold fully and ensure the type annotations still match"

view this post on Zulip Mario Carneiro (Jan 22 2021 at 16:46):

oh I missed that it was a conjunction

view this post on Zulip Mario Carneiro (Jan 22 2021 at 16:49):

@Patrick Massot Should this (1) always require that conjunctions are fully expanded or (2) split conjunctions only if the provided types don't match? (1) is easier and I think more stable because it doesn't require guessing and backtracking

view this post on Zulip Patrick Massot (Jan 22 2021 at 17:33):

I think I'll always want to fully expand.

view this post on Zulip Mario Carneiro (Jan 22 2021 at 17:38):

are the types required?

view this post on Zulip Mario Carneiro (Jan 22 2021 at 17:40):

Also I'm guessing you only want this for, say, conjunction and exists, not all inductive types (in particular splitting a nat seems bad)

view this post on Zulip Eric Wieser (Jan 22 2021 at 17:44):

Splitting a nat won't happen, because that's | not , notation. A better question would be whether prod should be split.

view this post on Zulip Mario Carneiro (Jan 22 2021 at 18:09):

also definitions that unfold to a conjunction

view this post on Zulip Patrick Massot (Jan 22 2021 at 18:18):

Yes, I'm thinking about conjunction and exists. Splitting a nat would be a disaster.

view this post on Zulip Mario Carneiro (Jan 22 2021 at 18:18):

What do you want to do about disjunctive things?

view this post on Zulip Patrick Massot (Jan 22 2021 at 18:18):

Definitions that unfold to a conjunction are not necessary, I can think of situation where you don't want to do that.

view this post on Zulip Patrick Massot (Jan 22 2021 at 18:19):

Disjunctive things are sufficiently rare that I don't really care.

view this post on Zulip Mario Carneiro (Jan 22 2021 at 18:20):

and are the types for decoration or are they required

view this post on Zulip Patrick Massot (Jan 22 2021 at 18:20):

Decoration is better, but they could be required.

view this post on Zulip Mario Carneiro (Jan 22 2021 at 18:21):

I can do decoration, that's probably easier while you are figuring out what to write

view this post on Zulip Mario Carneiro (Jan 22 2021 at 18:22):

the names could be required too; like you have to intro 1 or 3 things in your example

view this post on Zulip Patrick Massot (Jan 22 2021 at 18:23):

I don't understand what you mean by requiring name. How could you avoid providing names anyway? You mean autogenerating names?

view this post on Zulip Mario Carneiro (Jan 22 2021 at 18:23):

yeah

view this post on Zulip Mario Carneiro (Jan 22 2021 at 18:23):

that's what rintro does now

view this post on Zulip Mario Carneiro (Jan 22 2021 at 18:24):

I mean if the idea is to have a more strict version of rintro then it would make sense not to allow autogenerated names

view this post on Zulip Mario Carneiro (Jan 22 2021 at 18:25):

unless you want rintro _ to work

view this post on Zulip Patrick Massot (Jan 22 2021 at 18:25):

The idea is not really to have a more strict version, I want a simpler to use version.

view this post on Zulip Patrick Massot (Jan 22 2021 at 18:25):

And I don't want rintro _ to work.

view this post on Zulip Mario Carneiro (Jan 22 2021 at 18:26):

By the way you can accomplish something similar to splitting all conjunctions using casesm [_/\_] IIRC

view this post on Zulip Mario Carneiro (Jan 22 2021 at 18:29):

do you want <x,y> to still work?

view this post on Zulip Mario Carneiro (Jan 22 2021 at 18:29):

or is this not part of the syntax anymore

view this post on Zulip Patrick Massot (Jan 22 2021 at 18:29):

I don't care. I'd like to avoid students having to write it, but it doesn't matter if it actually still works.

view this post on Zulip Patrick Massot (Jan 22 2021 at 18:30):

The casesm thing is after introducing stuff, right?

view this post on Zulip Mario Carneiro (Jan 22 2021 at 18:30):

yeah

view this post on Zulip Mario Carneiro (Jan 22 2021 at 18:30):

so it would be something like intros names, casesm

view this post on Zulip Mario Carneiro (Jan 22 2021 at 18:30):

it's not a perfect match

view this post on Zulip Patrick Massot (Jan 22 2021 at 18:31):

casesm doesn't seem to like exists

view this post on Zulip Mario Carneiro (Jan 22 2021 at 18:31):

did you try [Exists _]?

view this post on Zulip Mario Carneiro (Jan 22 2021 at 18:32):

I can imagine the my_intro? version would also be useful for teaching

view this post on Zulip Patrick Massot (Jan 22 2021 at 18:33):

I didn't try, and it works.

view this post on Zulip Mario Carneiro (Jan 22 2021 at 18:33):

dunno if that makes it too easy

view this post on Zulip Patrick Massot (Jan 22 2021 at 18:34):

I'm also restricting this intro thing actually. My current version (which is based on regular intro, not rintro) has separate version for introducing data and Prop. Because on paper they are seen as completely different actions, and I'm tired of student starting proofs with "Assume there exists ε>0\varepsilon > 0".

view this post on Zulip Mario Carneiro (Jan 22 2021 at 18:36):

oh, so then you don't want (exists x, p x) -> Q to work as my_intro (x : A) (h : p x)?

view this post on Zulip Patrick Massot (Jan 22 2021 at 18:37):

Good question.

view this post on Zulip Patrick Massot (Jan 22 2021 at 18:37):

Damn it, consistency

view this post on Zulip Mario Carneiro (Jan 22 2021 at 18:38):

If this were first order logic, that would be two steps: the first intros x and leaves goal p x -> Q and the second would be an implication intro

view this post on Zulip Patrick Massot (Jan 22 2021 at 18:39):

Actually I think I want the current behavior (without rintro) with this one: an implication intro followed by a cases.

view this post on Zulip Patrick Massot (Jan 22 2021 at 18:40):

So actually I guess I only want automatic splitting of and

view this post on Zulip Mario Carneiro (Jan 22 2021 at 18:40):

cool

view this post on Zulip Mario Carneiro (Jan 22 2021 at 18:40):

and it only works on props?

view this post on Zulip Patrick Massot (Jan 22 2021 at 18:40):

Yes

view this post on Zulip Mario Carneiro (Jan 22 2021 at 18:41):

ok I'll try my hand at it

view this post on Zulip Patrick Massot (Jan 22 2021 at 18:41):

Thank you very much!


Last updated: May 09 2021 at 22:13 UTC