shorter cases tactic

Stream: lean4

[Chris Lovett]

I finally figured out how to port level 8 in advanced proposition world to lean4, but it's not pretty. See solution.

lemma and_or_distrib_left (P Q R : Prop) : P ∧ (Q ∨ R) ↔ (P ∧ Q) ∨ (P ∧ R) := by
  constructor
  intro h
  cases h with
  | intro hP hQR =>
    cases hQR with
    | inl hQ =>
      left
      constructor
      assumption
      assumption
    | inr hR =>
      right
      constructor
      assumption
      assumption
  intro h
  cases h with
  | inl hPQ =>
    cases hPQ with
    | intro hP hQ =>
      constructor
      assumption
      left
      assumption
  | inr hPR =>
    cases hPR with
    | intro hP hR =>
      constructor
      assumption
      right
      assumption

Here's the lean 3 solution for comparison:

lemma and_or_distrib_left (P Q R : Prop) : P ∧ (Q ∨ R) ↔ (P ∧ Q) ∨ (P ∧ R) :=
begin
  split,
  intro h,
  cases h with hp hqr,
  cases hqr with q r,
  left, split, assumption, assumption,
  right, split, assumption, assumption,
  intro h,
  cases h with hpq hpr,
  cases hpq with p q,
  split, assumption,
  left, assumption,
  cases hpr with hp hr,
  split, assumption,
  right, assumption,
end

Notice how the single line cases tactics make for a much more condensed proof. Is there another way to simplify my lean4 proof (using tactic proofs)?

[Heather Macbeth]

I see that mathlib4 has a cases' tactic for backwards compatibility.
https://github.com/leanprover-community/mathlib4/blob/f275d4b0c8762abd3eb75a4e5c2e9a8e9e2a2254/Mathlib/Tactic/Cases.lean

[Kevin Buzzard]

Right now the lean 4 version looks much harder to teach, not least because of the syntax and spacing. I didn't even teach { tac } brackets in lean 3, instead saying "tactics operate on the top goal".

[Mario Carneiro]

You can put multiple tactics on one line by separating them with ; (instead of ,), which should give you the ability to more or less directly copy the lean 3 proof

[Mario Carneiro]

Here's an approximation of a literal port of the lean 3 proof in lean 4, using the cases' and left/right tactics from mathlib:

import Mathlib.Tactic.Cases
import Mathlib.Tactic.LeftRight

theorem and_or_distrib_left (P Q R : Prop) : P ∧ (Q ∨ R) ↔ (P ∧ Q) ∨ (P ∧ R) := by
  constructor
  · intro h
    cases' h with hp hqr
    cases' hqr with q r
    left; constructor; assumption; assumption
    right; constructor; assumption; assumption
  · intro h
    cases' h with hpq hpr
    · cases' hpq with p q
      constructor; assumption
      left; assumption
    · cases' hpr with hp hr
      constructor; assumption
      right; assumption

The use of · for subgoals is required only because of a bug in cases' which appears to cause it to drop goals when it is applied on a goal state already containing multiple goals (which of course you shouldn't have in a well structured proof, but in this example we're specifically going for the stream of consciousness style so those · are undesirable).

[Scott Morrison]

I just found the same bug. :-)

[Mario Carneiro]

Here's a version that uses only core lean 4 but retains the lean 3 style as much as possible:

theorem and_or_distrib_left (P Q R : Prop) : P ∧ (Q ∨ R) ↔ (P ∧ Q) ∨ (P ∧ R) := by
  constructor
  intro h
  cases h with | _ hp hqr => ?_
  cases hqr with | inl q => ?_ | _ r => ?_
  apply Or.inl; constructor; assumption; assumption
  apply Or.inr; constructor; assumption; assumption
  intro h
  cases h with | inl hpq => ?_ | _ hpr => ?_
  cases hpq with | _ hp hq => ?_
  constructor; assumption
  apply Or.inl; assumption
  cases hpr with | _ hp hr => ?_
  constructor; assumption
  apply Or.inr; assumption

[Sebastian Ullrich]

If @Patrick Massot's NNG version takes care of "deemphasizing syntax worries as much as possible", I'd argue teaching some structuring in this "pure Lean" version is not wrong

[Mario Carneiro]

here's a version with the natural structuring suggested by the cases tactic:

theorem and_or_distrib_left (P Q R : Prop) : P ∧ (Q ∨ R) ↔ (P ∧ Q) ∨ (P ∧ R) := by
  constructor
  intro h
  cases h with | _ hp hqr =>
    cases hqr with
    | inl q =>
      apply Or.inl; constructor; assumption; assumption
    | _ r =>
      apply Or.inr; constructor; assumption; assumption
  intro h
  cases h with
  | inl hpq =>
    cases hpq with
    | _ hp hq =>
      constructor; assumption
      apply Or.inl; assumption
  | _ hpr =>
    cases hpr with
    | _ hp hr =>
      constructor; assumption
      apply Or.inr; assumption

[Mario Carneiro]

(as usual, a syntax error after the proof caused me to write nonsense that lean wasn't actually checking... -_- Should be fixed now.)

[Mario Carneiro]

now I have to go find out why cases h with | _ hpq => ?_ | _ hpr => ?_ doesn't work to destructure an or

[Sebastian Ullrich]

How do you expect that to work? _ means "all remaining cases"

[Mario Carneiro]

posted in lean4#1718. In short, uses of _ before the last pattern should target the first constructor that has not yet been claimed by an earlier arm

[Mario Carneiro]

and the last | _ => arm is applied to all remaining goals if there is more than one

[Sebastian Ullrich]

Yeah, I just saw the issue. I feel like it's overloading the meaning of _ in cases a bit too much - why not use next/all_goals at that point to be explicit.

[Mario Carneiro]

In this particular case, the point is so that we can use the => ?_ form of cases to dump the goals in the main context. next and case and all_goals are all block tactics

[Mario Carneiro]

I think cases tries a little too hard to be a half-assed version of match. It's not doing pattern matching, but it has some similar features and the combination is confusing

[Sebastian Ullrich]

Seems like your proposal would move it further away from match :)

[Mario Carneiro]

it would

[Mario Carneiro]

I don't think they should be using similar syntax, because that just invites misunderstandings when people try to write cases x with | inl (a, b) => ...

[Mario Carneiro]

or why name resolution on the variants works differently, you can't write cases x with | Or.inl a => ... but you have to write it like that (or use .inl) in match

[Mario Carneiro]

Also ?_ at the end of cases / match is non-compositional, you can't put any tactics before it. I would prefer if this was just a general mechanism to get out of a block context

[Sebastian Ullrich]

Mario Carneiro said:

or why name resolution on the variants works differently, you can't write cases x with | Or.inl a => ... but you have to write it like that (or use .inl) in match

Heh, in the other thread I was arguing for moving that closer to match

[Mario Carneiro]

I mean, I think it's mostly fine, but I think the data is in that it's a lot more cumbersome to write compared to lean 3 cases

[Mario Carneiro]

I don't think we should be going back to the unstructured list of names approach, but something like rcases patterns seems like a reasonable compromise

[Mario Carneiro]

and that PR is just the smallest delta I can make on current lean 4 to make it possible to do lean 3 style cases in lean 4

[Mario Carneiro]

(I don't think cases' is an adequate solution because it is mainly intended for backward compatibility and will go away eventually if it doesn't make the bar to go into official lean 4)

[Sébastien Michelland]

Maybe a naive question but... here's the same proof in Coq:

Theorem and_or_distrib_left {P Q R : Prop} : P /\ (Q \/ R) <-> (P /\ Q) \/ (P /\ R).
  split.
  * intros [HP [HQ|HR]].
    - left. split; assumption.
    - right. split; assumption.
  * intros [[HP HQ]|[HP HR]].
    - split. assumption. left; assumption.
    - split. assumption. right; assumption.

What's wrong with having a linear/non-structured case (or here intros) and then structuring with bullets?

[Mario Carneiro]

that's what I mean by rcases patterns

[Mario Carneiro]

rcases was in large part inspired by coq's syntax for pattern matching intros

[Mario Carneiro]

Here's a lean 4 transcription of the coq proof:

import Std.Tactic.RCases
import Mathlib.Tactic.LeftRight

theorem and_or_distrib_left {P Q R : Prop} : P ∧ (Q ∨ R) ↔ (P ∧ Q) ∨ (P ∧ R) := by
  constructor
  · rintro ⟨HP, HQ | HR⟩
    · left; constructor <;> assumption
    · right; constructor <;> assumption
  · rintro (⟨HP, HQ⟩ | ⟨HP, HR⟩)
    · constructor; assumption; left <;> assumption
    · constructor; assumption; right <;> assumption

[Mario Carneiro]

There was a lot of support for somehow unifying intro and rintro from the mathlib crowd, but they are fairly syntactically incompatible even though they are very similar

[Mario Carneiro]

I would like rcases to land in lean core in some way, maybe with some syntax modifications but essentially the same interface

[Kevin Buzzard]

@Sébastien Michelland the natural number game was written for mathematicians who have no programming background and I made a conscious decision not to teach any structuring. You would not believe the horrors I saw when I was beta testing with mathematics undergraduates. If we add some sort of structuring in Lean 4 then part of me thinks that this is a great idea to teach mathematicians about how to think correctly about a proof being a program, but another part of me is just worried that this will confuse them (certainly I do not want to assume that they have ever seen functional programming, for example). Perhaps one solution that we could have in Lean 4 is that whenever a proof breaks into 2, we literally end up with 2 windows where they can type.

[Sébastien Michelland]

Right, it seems reasonable to separate these concerns. (I mean I would never have doubted that mathematicians have an intuition of a subproof within a proof, but you've clearly seen more than I have. xD) So in that regard, separating the splitting/recursing from the structuring does make sense.

[François G. Dorais]

For the sake of listing one more option, one can also use next to avoid the with | ... syntax.

-- Plain Lean, no imports
theorem and_or_distrib_left {P Q R : Prop} : P ∧ (Q ∨ R) ↔ (P ∧ Q) ∨ (P ∧ R) := by
  constructor
  · intro ⟨HP,HQR⟩
    cases HQR
    next HQ =>
      apply Or.inl
      constructor
      · exact HP
      · exact HQ
    next HR =>
      apply Or.inr
      constructor
      · exact HP
      · exact HR
  · intro H
    cases H
    next HPQ =>
      constructor
      · exact HPQ.left
      · apply Or.inl
        exact HPQ.right
    next HPR =>
      constructor
      · exact HPR.left
      · apply Or.inr
        exact HPR.right

[Heather Macbeth]

Mario Carneiro said:

here's a version with the natural structuring suggested by the cases tactic:

theorem and_or_distrib_left (P Q R : Prop) : P ∧ (Q ∨ R) ↔ (P ∧ Q) ∨ (P ∧ R) := by
  constructor
  intro h
  cases h with | _ hp hqr =>
    cases hqr with
    | inl q =>
      apply Or.inl; constructor; assumption; assumption
    | _ r =>
      apply Or.inr; constructor; assumption; assumption
  intro h

@Mario Carneiro In this proof of yours (cropped for clarity), is it conventional that you indented

    cases hqr with
    | inl q =>
      apply Or.inl; constructor; assumption; assumption
    | _ r =>
      apply Or.inr; constructor; assumption; assumption

? In Lean 3 we wouldn't brace after a step which doesn't increase the number of goals.

[Mario Carneiro]

I indented it because the thing after cases is a block of tactics, it's like all_goals or other tactic combinator. When you say "we wouldn't brace after a step which doesn't increase the number of goals", that implies that cases h with | _ hp hqr => is a tactic, and it's not. The standalone tactic version would be written cases h with | _ hp hqr => ?_, and I would not indent after that since you can put parentheses around that tactic without causing a syntax error

[Mario Carneiro]

In particular, you can see the intro h is not indented along with the cases hqr. If you were to dedent the block, it would actually change the meaning of the code, since the intro h would be brought into the block as well

[Heather Macbeth]

Mario Carneiro said:

In particular, you can see the intro h is not indented along with the cases hqr. If you were to dedent the block, it would actually change the meaning of the code, since the intro h would be brought into the block as well

To check, you mean the second intro h?

[Mario Carneiro]

yes

[Heather Macbeth]

Thanks!

[Chris Lovett]

Speaking of semi-colons, the NNG for lean3 says "Note the semicolon**! It means "do the next tactic to all the goals, not just the top one". I take it this is not the case in lean4, where it just means the same as a newline?

[Mario Carneiro]

in lean 4 that remark is directed to <;>

[Chris Lovett]

Can someone explain why/what the "dot" is exactly so I can explain it in the updated version of the tutorial ? Specifically, why can't an indent do the same thing? I noticed the inner dots on the rintro subgoals where not needed, what are the guidelines, only use dot when necessary? Or use them everywhere for consistency?

lemma and_or_distrib_left (P Q R : Prop) : P ∧ (Q ∨ R) ↔ (P ∧ Q) ∨ (P ∧ R) := by
  constructor
  · rintro ⟨HP, HQ | HR⟩
    left; constructor <;> assumption
    right; constructor <;> assumption
  · rintro (⟨HP, HQ⟩ | ⟨HP, HR⟩)
    constructor; assumption; left; assumption
    constructor; assumption; right; assumption

[Scott Morrison]

The dot focuses, so the other goals disappear from view, until you reach the next dot.

[Scott Morrison]

So it's cleaner to use the dot, and helpful if someone is ever going to read the proof. Using the dot consistently prevents you from writing proofs in which the reader has to track multiple goals in their head, and work out from the proof where the argument close one and moves on to the next.

[Mario Carneiro]

The dot is valuable for readers because of all the ways you could have written the code that wouldn't compile with the dots. For example, this doesn't compile:

lemma and_or_distrib_left (P Q R : Prop) : P ∧ (Q ∨ R) ↔ (P ∧ Q) ∨ (P ∧ R) := by
  constructor
  · rintro ⟨HP, HQ | HR⟩
  · left; constructor <;> assumption
  · right; constructor <;> assumption
  · rintro (⟨HP, HQ⟩ | ⟨HP, HR⟩)
  · constructor; assumption; left; assumption
  · constructor; assumption; right; assumption

That's because the first goal is not closed by the rintro line, it still has two subgoals and you get an error saying the proof isn't done yet. So by looking at a proof like this I can immediately see that constructor would have to produce six goals for the proof to compile. While it is true that the inner dots are not required, the following proof has the same structure and also compiles:

lemma and_or_distrib_left (P Q R : Prop) : P ∧ (Q ∨ R) ↔ (P ∧ Q) ∨ (P ∧ R) := by
  constructor
  · rintro ⟨HP, HQ | HR⟩
    left; constructor <;> assumption
    right; constructor <;> assumption
  · rintro (⟨HP, HQ⟩ | ⟨HP, HR⟩)
    constructor; assumption; left
    assumption; constructor
    assumption; right; assumption

but now that I've scrambled the lines it's not clear where one goal ends and the next one starts. Adding the dots provides visual proof that I didn't scramble the goals like this.

[Chris Lovett]

My question though was about this case which also compiles, but it seems the inner dots are not needed.

lemma and_or_distrib_left (P Q R : Prop) : P ∧ (Q ∨ R) ↔ (P ∧ Q) ∨ (P ∧ R) := by
  constructor
  · rintro ⟨HP, HQ | HR⟩
    . left; constructor <;> assumption
    . right; constructor <;> assumption
  · rintro (⟨HP, HQ⟩ | ⟨HP, HR⟩)
    . constructor; assumption; left; assumption
    . constructor; assumption; right; assumption

it's almost like the mathlib left tactic is also acting like a dot? So is it recommended i include these inner dots or not?

Can I think of dot almost like a "push tail; pop tail" operation that hides all the trailing goals so I can focus on the topmost goal? If I am to believe the tactic state I see in the InfoView as I move my cursor around, it seems like "pop" is automatic as soon as the goals are accomplished the remaining goal re-appears, so I'm not sure why I need a dot on the second rintro.

[Mario Carneiro]

Dots are never needed if you have placed them correctly

[Mario Carneiro]

The value of placing dots is to say "the fact that it still compiles means my proof must actually have this structure"

[Mario Carneiro]

The actual effect of the dot is the following:

Given a goal state [g1, g2, ... gn], . tacs is a tactic which first changes the goal state to [g1], then runs tacs. If the resulting goal state is not [], throw an error. Then restore the remaining goals [g2, ..., gn].

[Mario Carneiro]

In other words, it's a checkpoint at the end of tacs which ensures that at that point the goal g1 has been completely dealt with. It's just like an assert() in the middle of some code - if you remove it, stuff still works, but that doesn't mean the assert doesn't have value

[Mario Carneiro]

it seems like "pop" is automatic as soon as the goals are accomplished the remaining goal re-appears, so I'm not sure why I need a dot on the second rintro.

When there is only one goal remaining, the dot is a no-op, and sometimes people will leave off the dot on the last case, especially if the cases are very asymmetric like in a proof by induction where the base case is one line and the induction step is the rest of the proof, and they want to avoid indenting the rest of the proof. But you might keep the dots in if you want to emphasize the symmetry of the cases like in a by_cases proof or one that destructures an \/ as in this case. If we were to leave off the last-case dots, it would look like this:

lemma and_or_distrib_left (P Q R : Prop) : P ∧ (Q ∨ R) ↔ (P ∧ Q) ∨ (P ∧ R) := by
  constructor
  · rintro ⟨HP, HQ | HR⟩
    . left; constructor <;> assumption
    right; constructor <;> assumption
  rintro (⟨HP, HQ⟩ | ⟨HP, HR⟩)
  . constructor; assumption; left; assumption
  constructor; assumption; right; assumption

[Mario Carneiro]

this is similar to whether you like to format a function with a big if statement as:

void foo() {
  if (cond) {
    then_stuff();
    return;
  }
  else_stuff();
}

or

void foo() {
  if (cond) {
    then_stuff();
  } else {
    else_stuff();
  }
}

[Mario Carneiro]

So is it recommended i include these inner dots or not?

It is recommended you always add the dots after any tactic that produces more than one goal. When the tactics are on one line, my personal preference is to use { } (which is the lean 3 version of the dot which is still available in lean 4) instead of (. tacs); .... With that style, the proof would look like:

lemma and_or_distrib_left (P Q R : Prop) : P ∧ (Q ∨ R) ↔ (P ∧ Q) ∨ (P ∧ R) := by
  constructor
  · rintro ⟨HP, HQ | HR⟩
    . left; constructor <;> assumption
    . right; constructor <;> assumption
  · rintro (⟨HP, HQ⟩ | ⟨HP, HR⟩)
    . constructor; {assumption}; left; assumption
    . constructor; {assumption}; right; assumption

[Mario Carneiro]

Now I can tell by looking at the proof that the constructor on the last line made two goals and assumption clears the first one and right; assumption clears the second.

[Chris Lovett]

Thanks very helpful, if you prefer curly braces why not write this instead?

lemma and_or_distrib_left (P Q R : Prop) : P ∧ (Q ∨ R) ↔ (P ∧ Q) ∨ (P ∧ R) := by
  constructor
  { rintro ⟨HP, HQ | HR⟩
    left; constructor <;> assumption
    right; constructor <;> assumption
  }
  { rintro (⟨HP, HQ⟩ | ⟨HP, HR⟩)
    constructor; {assumption}; left; assumption
    constructor; {assumption}; right; assumption
  }

[Mario Carneiro]

that used to not work at all in lean 4, does that work now?

[Mario Carneiro]

the lean 3 style looks like this

lemma and_or_distrib_left (P Q R : Prop) : P ∧ (Q ∨ R) ↔ (P ∧ Q) ∨ (P ∧ R) := by
  constructor
  { rintro ⟨HP, HQ | HR⟩
    left; constructor <;> assumption
    right; constructor <;> assumption }
  { rintro (⟨HP, HQ⟩ | ⟨HP, HR⟩)
    constructor; {assumption}; left; assumption
    constructor; {assumption}; right; assumption }

[Mario Carneiro]

and it does work now in lean 4, but I think the dots are more in keeping with the whitespace sensitive and newline-terminated style of lean 4

[Chris Lovett]

Yep I'm getting Goals accomplished :tada: with the curly bracket version.

[Mario Carneiro]

although you are still missing some braces there

[Mario Carneiro]

it's more like this

lemma and_or_distrib_left (P Q R : Prop) : P ∧ (Q ∨ R) ↔ (P ∧ Q) ∨ (P ∧ R) := by
  constructor
  { rintro ⟨HP, HQ | HR⟩
    { left; constructor <;> assumption }
    { right; constructor <;> assumption } }
  { rintro (⟨HP, HQ⟩ | ⟨HP, HR⟩)
    { constructor; {assumption}; left; assumption }
    { constructor; {assumption}; right; assumption } }

[Chris Lovett]

Well hmmm. Gets a bit much. I ended up documenting both styles and including your nice definition of dot here http://lovettsoftware.com/NaturalNumbers/AdvancedPropositionWorld/Level8.lean.html

[Mario Carneiro]

the dots definitely look cleaner

[Chris Lovett]

But it is interesting one can mix the style of grouping with parens when necessary, but also chipping away at the top goal without parens also works, so you can "simplify" the use of braces...

[Mario Carneiro]

the idea with the "structured style" is to never call a tactic when more than one goal is visible

[Mario Carneiro]

mathlib would reject your proof if you use the unstructured style

[Mario Carneiro]

it's good for hacking on the problem but it isn't "professional looking" and more importantly it's difficult to maintain

[Mario Carneiro]

if a tactic goes from closing a goal to no longer closing the goal, then the next tactic will be called on the wrong goal and you get all sorts of crazy cascading errors

[Mario Carneiro]

so "simplifying" the braces is not allowed - every brace there is required (although you can write it using . or case or next if you prefer, or use a tactic with built in structuring like cases e with | a => tac | b => tac)

[Mario Carneiro]

Also, just to be clear, parentheses in tactics are also legal but they have no block structuring effect. (tac1; tac2); tac3 means the same as tac1; tac2; tac3. The main reason to use parentheses is to clear up a precedence or parsing issue, or run multiple tactics in a slot where only one tactic is allowed like tac1 <;> (tac2; tac3) (which would run tac2 then tac3 on every subgoal produced by tac1).

[Chris Lovett]

I see, good to know, I definitely follow the maintainability argument. It was surprising to me to learn that tactics that do nothing don't report an error in general. Some do, like intro tells you when there's no way to introduce a new hypothesis, but rw silently fails...

[Mario Carneiro]

Example? We had a conversation about finding and removing those issues earlier, so I'm interested to see where that happens

[Mario Carneiro]

if you mean rw [], that one is defined to do nothing (other than the reducible rfl at the end) so it shouldn't fail, but if a rewrite is attempted it should not fail silently

[Mario Carneiro]

in lean 3 tactics would fail by convention if they make no progress, and I think we want to adopt the same behavior in lean 4

[Chris Lovett]

Ok, good to know. I know I've seen it but can't reproduce it right now, I will file a bug if I see it again with a repro.
PS: thanks for the tac1 <;> (tac2; tac3) tip, that indeed seems handy.

[Chris Lovett]

It is apply that silently fails, not rw.

[Mario Carneiro]

Again, can you show an #mwe, I have not experienced this

[Chris Lovett]

It might be an incremental editing issue. If I have unfinished work ahead in the proof then apply produces no error:

image.png

But if I fix the missing syntax ahead, then apply shows the error:

image.png

[Jireh Loreaux]

one way to deal with that is to make sure your proof always compiles (unless you are mid-line) by placing sorrys that fill in all the holes in you proof.