Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: Flat rintro

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.

Mario Carneiro (Jan 22 2021 at 16:08):

doesn't rintro do that already?

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

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"

Mario Carneiro (Jan 22 2021 at 16:46):

oh I missed that it was a conjunction

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

Patrick Massot (Jan 22 2021 at 17:33):

I think I'll always want to fully expand.

Mario Carneiro (Jan 22 2021 at 17:38):

are the types required?

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)

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.

Mario Carneiro (Jan 22 2021 at 18:09):

also definitions that unfold to a conjunction

Patrick Massot (Jan 22 2021 at 18:18):

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

Mario Carneiro (Jan 22 2021 at 18:18):

What do you want to do about disjunctive things?

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.

Patrick Massot (Jan 22 2021 at 18:19):

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

Mario Carneiro (Jan 22 2021 at 18:20):

and are the types for decoration or are they required

Patrick Massot (Jan 22 2021 at 18:20):

Decoration is better, but they could be required.

Mario Carneiro (Jan 22 2021 at 18:21):

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

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

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?

Mario Carneiro (Jan 22 2021 at 18:23):

yeah

Mario Carneiro (Jan 22 2021 at 18:23):

that's what rintro does now

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

Mario Carneiro (Jan 22 2021 at 18:25):

unless you want rintro _ to work

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.

Patrick Massot (Jan 22 2021 at 18:25):

And I don't want rintro _ to work.

Mario Carneiro (Jan 22 2021 at 18:26):

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

Mario Carneiro (Jan 22 2021 at 18:29):

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

Mario Carneiro (Jan 22 2021 at 18:29):

or is this not part of the syntax anymore

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.

Patrick Massot (Jan 22 2021 at 18:30):

The casesm thing is after introducing stuff, right?

Mario Carneiro (Jan 22 2021 at 18:30):

yeah

Mario Carneiro (Jan 22 2021 at 18:30):

so it would be something like intros names, casesm

Mario Carneiro (Jan 22 2021 at 18:30):

it's not a perfect match

Patrick Massot (Jan 22 2021 at 18:31):

casesm doesn't seem to like exists

Mario Carneiro (Jan 22 2021 at 18:31):

did you try [Exists _]?

Mario Carneiro (Jan 22 2021 at 18:32):

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

Patrick Massot (Jan 22 2021 at 18:33):

I didn't try, and it works.

Mario Carneiro (Jan 22 2021 at 18:33):

dunno if that makes it too easy

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 $\varepsilon > 0$ ".