simproc for ite

Stream: Is there code for X?

[Johan Commelin]

First of all, I know about docs#reduceIte, but it doesn't cover what I want.
Consider

example (P : Prop) [Decidable P] : (1:Nat) = if P then 1 else 0 := by
  sorry

Is there a simproc that will reduce the goal to P, by inspecting that the LHS (1:Nat) is equal to the true-branch of the ite, and more importantly is not equal to the false-branch of the ite. (And dually, reduce to \not P when appropriate.)

Maybe this is way to expensive, and a bad idea. But I think it could be useful in practice.

E.g, this came up when running the compute_degree tactic on natDegree (X^p - X) = p, where p is a prime and the coefficients are a field of characteristic 0.

import Mathlib

open Polynomial
example (K : Type*) [Field K] [CharZero K] (p : Nat) : natDegree (R := K) (X^p - X) = p := by
  compute_degree

The goal is now

(1 - if p = 1 then 1 else 0) \ne 0

and it would be great if we could automatically reduce this further to p \ne 1.

[Yaël Dillies]

What about simp [Ne.ite_eq_left_iff]? (docs#Ne.ite_eq_left_iff)

[Damiano Testa]

Did you mean to add Prime p to your assumptions?

[Yaël Dillies]

In your example, it seems like you first need a simproc to bubble up the ite to the top of the expression. I really wish we had something like this, because docs#apply_ite is really hard to use in practice

[Damiano Testa]

(or at the very least 1 < p!

[Yaël Dillies]

Damiano Testa said:

Did you mean to add Prime p to your assumptions?

Lean should know that when a number theorist calls a variable p it should be a prime :see_no_evil:

[Damiano Testa]

Yaël Dillies said:

Damiano Testa said:

Did you mean to add Prime p to your assumptions?

Lean should know that when a number theorist calls a variable p it should be a prime :see_no_evil:

This should be added to the linter for common mistakes...

[Johan Commelin]

I didnt intend for my examples to be provable, merely illustrative

[Johan Commelin]

I guess the tricky thing is that there is nothing to key on? So it doesn't fit in a discrimination tree approach?

[Johan Commelin]

So maybe (if at all) this should be a separate tactic...

[Yaël Dillies]

Yes I agree that's what's tricky. Isn't the point of simprocs that they don't use the discrimination tree and are basically "a separate tactic but integrated into simp"?

[Johan Commelin]

I think that simp still needs to decide when to run the tactic, and it does that using disctrees. But I'm not an expert, so I might be wrong.

[Yaël Dillies]

Let me read up about simprocs...

[Johan Commelin]

Maybe what I'm looking for can also be accomplished with chaining split_ifs and simp.

[Floris van Doorn]

simp basically already does what you want on the first example...

import Mathlib.Tactic.Common

example (P : Prop) [Decidable P] : (if P then (1:Nat) else 0) = (1:Nat) := by
  simp says simp only [ite_eq_left_iff, Nat.zero_ne_add_one, imp_false, Decidable.not_not]
  guard_target = P
  sorry

[Johan Commelin]

Yeah, I think the first example is too minimal in hindsight :oops:

[Floris van Doorn]

And with more aggresive simp-lemmas (e.g. sub_ne_zero_iff_ne the second example could also work)

[Johan Commelin]

I guess so. Do we want the default simp set to be able to handle this?

[Floris van Doorn]

I'm not sure. I've been thinking for a while now to have a single simp set (extra/extended/more/plus/...) where we can put all our lemmas that can be useful to simplify sometimes, but in other contexts might be undesirable. The user interaction I imagine is that if simp fails to simplify as much as you want, you can write simp [plus] to simplify further. But you might have to do the simp? [plus] -> simp [plus, - undesirable_lemma]-dance to simplify exactly how you wish.

[Floris van Doorn]

For a more complicated second version, you need to rewrite the goal so that the if-then-else is on one side of the equation, which lies outside the scope of simp in more complicated cases. We should have a more generic tactic solve_for x that solves for the term x (at least if the expression is linear in x)...

[Pri]

(deleted)