proof mode terms for icases

Stream: iris-lean

[Michael Sammler]

Hi, I am currently looking into extending some tactics to support proof mode terms. So far, this is working quite well, but there is an issue with icases: Currently icases H with pat destructs H with the pattern pat, but with proof mode terms icases H with HL would instantiate H with the hypothesis HL before destructing it. So the problem is that there are two different meanings of with for icases. In Rocq, this is not a problem since (i)Destruct uses as instead of with. I see multiple options to resolve this conflict:

• use something else than with for proof mode terms (what exactly? Something like $$ to mirror $!? Something else?)
• use something else than with for icases (making it inconsistent with cases)
• something else?

What do you think about this? Any other ideas?

[Shreyas Srinivas]

So in regular lean, we use rcases or obtain to destruct into a pattern

[Shreyas Srinivas]

And there is some editor support for generation of case arms with the current usage if with

[Shreyas Srinivas]

One idea would be to extend icases with as but keep the with part. It would feel like more idiomatic lean

[Shreyas Srinivas]

You could also borrow the cases h : HL pattern into icases for naming the hypothesis

[Shreyas Srinivas]

This is how the latter syntax works in a trivial demo:

import Batteries

example : ∀ n : Nat, n = n := by
  intro n
  cases hn : n with
  | zero => -- hypothesis hn
      rfl
  | succ n => -- hypothesis hn
      rfl

[Shreyas Srinivas]

Here is one more example of regular style lean usage with named hypothesis:

example : ∀ n : Nat × Nat, n = n := by
  intro n
  rcases h : n with ⟨⟨hz₁, hsucc₁⟩, ⟨hz₂, hsucc₂⟩⟩
  all_goals rfl

[Shreyas Srinivas]

All these options come with code action support which could be extended to icases if Batteries is imported

[Shreyas Srinivas]

This style of naming hypothesis is also available for match statements in lean. So it's one of the canonical ways of naming hypothesis (not pattern destruction).

[Shreyas Srinivas]

@Michael Sammler : On second thoughts, I must mention that the above makes sense if the preference is to align iris-lean tactic syntax with regular lean syntax as opposed to matching that of Rocq-iris, which seems to take inspiration from regular Rocq tactic syntax. I am not sure the latter makes much sense, but that's just an aesthetic preference.

[Zongyuan Liu]

Is it possible to handle proof mode terms in Lean without using $! and with as separators? I feel like all subsequent terms and patterns in a proof mode term simply specify how to specialise the hypothesis. So it is also intuitive without them. Related: #99

[Michael Sammler]

Shreyas Srinivas said:

So in regular lean, we use rcases or obtain to destruct into a pattern

Good point, I guess icases is more like rcases instead of cases.

Zongyuan Liu said:

Is it possible to handle proof mode terms in Lean without using $! and with as separators? I feel like all subsequent terms and patterns in a proof mode term simply specify how to specialise the hypothesis. So it is also intuitive without them

That is also an interesting option to investigate.

[Shreyas Srinivas]

with is not necessarily for pattern destruction. As I pointed about, in the wider lean world, with is the standard separator for match, cases, and even induction.

[Shreyas Srinivas]

It’s not necessary to define it that way, but it’s something a lot of lean users might have muscle memory for.

[Michael Sammler]

Shreyas Srinivas said:

with is not necessarily for pattern destruction. As I pointed about, in the wider lean world, with is the standard separator for match, cases, and even induction.

I see, thanks for pointing this out! So the usage of with in the Iris sense would probably be unfamiliar to Lean users since it means something quite different.

[Shreyas Srinivas]

As the rcases example shows, it is a bit complicated. rcases began it's life in mathlib IIRC

[Shreyas Srinivas]

But yes, the lean4 style is closer to the cases example I described above

[Shreyas Srinivas]

Here's the obtain style:

example : ∀ n : Nat × Nat, n = n := by
  intro n
  obtain ⟨⟨hz₁, hsucc₁⟩, ⟨hz₂, hsucc₂⟩⟩ := n
  all_goals rfl

[Shreyas Srinivas]

or one with a Sum type :

example : ∀ n : Nat ⊕ Nat, n = n := by
  intro n
  obtain (⟨hz₁, hsucc₁⟩ | ⟨hz₂, hsucc₂⟩) := n
  all_goals rfl

[Shreyas Srinivas]

The advantage of the cases style approach is all the relevant variables are introduced in the arm they are needed and the recursive structure of the proof is obvious

[Zongyuan Liu]

On a side note, I think there are some duplicate code for specialisation and/or instantiation of universally quantified variables in tactics taking proof mode terms like ispecialize, ipose, and iapply. We should refactor these tactics to use a unified logic like how it's done in the Rocq implementation.

[Michael Sammler]

Indeed. I hope to have a PR open in the next days to clean this up.

[Markus de Medeiros]

Speaking of, you should probably have merge access Micahel. You can definitely review the metaprogramming stuff better than I can and I'm going to be very short on time until the LICS deadline anyways.

@Mario Carneiro

[Shreyas Srinivas]

Zongyuan Liu said:

On a side note, I think there are some duplicate code for specialisation and/or instantiation of universally quantified variables in tactics taking proof mode terms like ispecialize, ipose, and iapply. We should refactor these tactics to use a unified logic like how it's done in the Rocq implementation.

Slightly disagree there. I am personally biased towards keeping Iris-lean tactics nominally and functionally similar to their regular lean counterparts as opposed to matching Rocq-Iris one-one.

[Shreyas Srinivas]

Users of Iris-lean will need to learn some amount of regular lean to use it and integrate it with mathlib for instance.

[Shreyas Srinivas]

It will be very confusing to context switch between regular lean tactic behaviour and Rocq-like behaviour for Iris tactics.

[Shreyas Srinivas]

ispecialize maps to lean’s specialize to specialise a hypothesis given its assumption. Mathlib has a backwards reasoning style apply … at … which applies an implication to an assumption and changes the assumption. The regular lean apply is only applicable in goals. Some of the internal implementation could definitely be harmonised.

[Zongyuan Liu]

Shreyas Srinivas said:

ispecialize maps to lean’s specialize to specialise a hypothesis given its assumption. Mathlib has a backwards reasoning style apply … at … which applies an implication to an assumption and changes the assumption. The regular lean apply is only applicable in goals. Some of the internal implementation could definitely be harmonised.

I only meant to harmonise the internal implementation. I get your point, but iApply in Iris-Rocq is also only applicable in goals; one needs to use iSpecialize (and iDestruct etc) to specialise a hypothesis. So I think we are good.

[Michael Sammler]

Michael Sammler said:

Indeed. I hope to have a PR open in the next days to clean this up.

The PR is here: https://github.com/leanprover-community/iris-lean/pull/107
Feedback is welcome!

[Shreyas Srinivas]

you probably want to translate Idents to Names

[Shreyas Srinivas]

since the metaprogramming API makes use of those

[Shreyas Srinivas]

But definitely worth checking with someone who knows better

[Mario Carneiro]

Ident carries position information, you need to make sure to hold on to it long enough to give the ident the right hover info

[Shreyas Srinivas]

Oh right. sorry, I have gotten used to Lean.Name from #mpil . It lets you use only names available in context very conveniently

[Markus de Medeiros]

The PR looks impressive! I can look through on Saturday but like I mentioned above, I think Michael is probably the right person to review these anyhow.

Re. the syntax, maybe we could be consistent by using the syntax from intros? We already have one syntax for determining which context something lives in, so maybe we could use ispecialize HPQ %y %Hy HP2 instead of ispecialize HPQ $! y Hy with HP2

[Markus de Medeiros]

I really hate the $! in Iris-Rocq, for some reason I get it confused with !$ or $? or ?$ haha.