subterm selection

Stream: general

[Assia Mahboubi]

Many of the features of the ssreflect tactic language are thought of as instruments for eliminating the need for a certain kind of brittle code.
In some cases, the solutions proposed by ssreflect have already been made available in Lean from very early on, in some others the same needs are addressed using different solutions.
But here is an example of ssreflect feature that I use on a daily basis and do not know how to transpose in the current lean/mathlib context. It is about selecting meaningful parts of terms (e.g., of the formula to be proved in a goal) without having to insert fragile information in the script. Here is an example of this feature, combined with the rewrite tactic (analogue of rw):

[Assia Mahboubi]

From mathcomp Require Import all_ssreflect.

(* rewrite all occurrences of `a` under `F` *)
Lemma test1 (F : nat -> nat) (a b : nat) :
  a = b ->  a + (a + F (a + 1)) = a + (a + F (b + 1)).
Proof.
  intro e.
  rewrite [in X in F X]e.
  done.
Qed.

(* same script despite the different association of sums *)
Lemma test2 (F : nat -> nat) (n a b : nat) :
  a = b ->  (a + a) + F (a + 3) = (a + a) + F (b + 3).
Proof.
  intro e.
  rewrite [in X in F X]e.
  done.
Qed.

(* rw only in the occurrence of `a` under the `F` on the right-hand side *)
Lemma test3 (F : nat -> nat) (n a b : nat) :
  a = b ->  (a + a) + F b = (a + a) + F a.
Proof.
  intro e.
  rewrite [in X in _ = _ (F X)]e.
  done.
Qed.

[Eric Wieser]

Here's the Lean translation of the first one:

import Mathlib

theorem test1 (F : Nat -> Nat) (a b : Nat) :
    a = b ->  a + (a + F (a + 1)) = a + (a + F (b + 1)) := by
  intro e
  conv in F _ => rw [e]

[Eric Wieser]

I guess the pattern matching of F _ isn't quite the same; I don't think we have a syntax for entering a subexpression of a match

[Mario Carneiro]

we do, conv in pat => ... is shorthand for conv => pattern pat; ... and you can iterate pattern

[Eric Wieser]

It's not clear to me how to make the X in _ = _ (F X) pattern work

[Assia Mahboubi]

Thanks! What would be the Lean analogue for test3 then?

[Eric Wieser]

I think the ideal lean spelling would be something like

-- not legal today
pattern _ = _ (F ?a) with
| a => _

[Assia Mahboubi]

Btw, there is an old paperabout this.

[Mario Carneiro]

lemma test3 (F : Nat -> Nat) (n a b : Nat) :
    a = b ->  (a + a) + F b = (a + a) + F a := by
  intro e
  conv => rhs; pattern F _; rw [e]

[Eric Wieser]

I think test3 is not a good example; it's using an overpowered feature for an example which doesn't require it

[Mario Carneiro]

I could be misunderstanding the spec though

[Eric Wieser]

I think you took the spec to be "solve the lemma", but it was actually intended to be something else.

[Mario Carneiro]

no, I read the spec as the comment rw only in the occurrence of `a` under the `F` on the right-hand side

[Mario Carneiro]

I suppose I didn't zoom in on a like the spec says but it's already zoomed in

[Eric Wieser]

It's interesting that _ (F X) works in Coq; Lean is unwilling to do the higher order unification to fill the _ here

[Assia Mahboubi]

Indeed, this was the spec. But what is too specific in my example is the "right-hand side".

[Mario Carneiro]

The thing that the pattern grammar lacks, as Eric points out, is a way to name subexpression metavariables

[Mario Carneiro]

or rather, to do something useful with the name - the syntax ?a exists

[Mario Carneiro]

Still, conv blocks are rare, pattern even more rare, and this kind of subexpression match essentially nonexistent. It could be that we're just used to finding alternative ways through it though

[Assia Mahboubi]

May I ask what would be idiomatic on this extra example?

(* rw only the occurrence of a of the left of the product *)
Lemma test4 (P : nat -> nat -> Prop) (F : nat -> nat) (a b : nat) :
  a = b -> P (F a) ((F a) + (F (a * 3))).
Proof.
  intro e.
  rewrite [X in X * _]e.

[Mario Carneiro]

I guess one way to dodge the issue as stated is with something like

lemma test4 (P : Nat → Nat → Prop) (F : Nat → Nat) (a b : Nat) :
    a = b → P (F a) ((F a) + (F (a * 3))) := by
  intro e
  convert_to P (F a) (F a + F (b * 3)); rw [← e]

[Assia Mahboubi]

But this script is more fragile, as it depends on more context-specific information.

[Mario Carneiro]

other possibilities:

lemma test4 (P : Nat → Nat → Prop) (F : Nat → Nat) (a b : Nat) :
    a = b → P (F a) ((F a) + (F (a * 3))) := by
  intro e
  conv in (occs := 3) a => rw [e]

lemma test4 (P : Nat → Nat → Prop) (F : Nat → Nat) (a b : Nat) :
    a = b → P (F a) ((F a) + (F (a * 3))) := by
  intro e
  conv => enter [2, 2]; rw [e]

[Mario Carneiro]

Oh I'm aware. I understand why you would find these solutions to be not as good

[Mario Carneiro]

I think the example is a bit contrived though

[Mario Carneiro]

I think beyond a certain point it's not necessarily a good thing to avoid stating the goal in the proof script

[Assia Mahboubi]

Also, it seems to me that your first solution is relying on the fact that I am using here a term P (a variable in this case), when the Coq version would be the same for an arbitrary concrete context P.

[Eric Wieser]

Mario Carneiro said:

or rather, to do something useful with the name - the syntax ?a exists

Presumably the main barrier here is that conv is used so rarely that there's little motivation for anyone to add this feature?

[Assia Mahboubi]

And the other solutions rely on occurrence numbers, which are quite not robust to changes in your proof as well.

[Mario Carneiro]

Actually I should have mentioned this as well:

lemma test4 (P : Nat → Nat → Prop) (F : Nat → Nat) (a b : Nat) :
    a = b → P (F a) ((F a) + (F (a * 3))) := by
  intro e
  conv in _*_ => rw [e]

[Mario Carneiro]

that one is certainly closest to your requirements

[Assia Mahboubi]

Indeed, it is.

[Mario Carneiro]

There are of course ways to fool this matching pattern as well

[Kyle Miller]

This is not idiomatic, but I was a bit surprised it actually worked:

theorem test4 (P : Nat → Nat → Prop) (F : Nat → Nat) (a b : Nat) :
    a = b → P (F a) ((F a) + (F (a * 3))) := by
  intro e
  rw [show _*_ = ?_ from ?h]
  case h => rw [e]; exact rfl
  /-
  ⊢ P (F a) (F a + F (b * 3))
  -/

[Eric Wieser]

Is it worth splitting this conv-related thread?

[Eric Wieser]

(maybe from this message)

[Notification Bot]

37 messages were moved here from #general > Small Scale Reflection for the Working Lean user by Kyle Miller.

[Kyle Miller]

(Feel free to adjust the topic name. I thought splitting made sense to get more visibility.)

[Assia Mahboubi]

Mario Carneiro said:

I think beyond a certain point it's not necessarily a good thing to avoid stating the goal in the proof script

I am a big fan of declarative style. But this kind of feature is precisely useful when it is not at all a good thing to include your goal in the proof script, e.g., you are in the process of writing a proof and your algebraic expression's parentheses/values of constants/names of variables/etc are changing slightly at each iteration. In this case, it is desirable, when possible, to provide a "meaningful" description of your pattern.

[Assia Mahboubi]

Also, I am not sure that the current number of occurrences of conv blocks alone is a good measure of the relevance of the feature: enhancing the features of subterm selections could lead to a wider usage of the supporting tactics, whatever they are :grinning_face_with_smiling_eyes: .
It seems to me that the more meaningful question would be to know whether users feel limitations in the current way of selecting subterms (for rewriting, but not only).

[Assia Mahboubi]

On a more subjective note, from my experience binders (and the other features of the pattern language) provide a quite convenient language for selection, even if you could often come up with a binder-free variant. But again, that's more a matter of habit I guess.

[Vladimir Gladstein]

@Assia Mahboubi thanks for mentioning this ssreflect feature. You are welcome to open an issue on LeanSSR repo, and I will try to add it. For now, we only support occurrences selection.

[Notification Bot]

Assia Mahboubi has marked this topic as resolved.

[Notification Bot]

Assia Mahboubi has marked this topic as unresolved.

[Norman Paskus]

(deleted)

[Notification Bot]

A message was moved here from #general > String diagrams by Gramps Grampa.