understanding syntax

Stream: new members

[William Sealy Gosset]

I have the following in my local state:

M: Type u
_inst_1: monoid M
P: Prop
_inst_2: decidable P
ab: M
h: P
⊢ ite P (a * b) 1 = ite P a 1 * ite P b 1

I've spent a good part of the last few hours trying to figure out the syntax I need to type to evolve the goal forward. When I trace the simp[h], I get the following:

0. [simplify.rewrite] [h]: P ==> true
1. [simplify.rewrite] [if_true]: ite true (a * b) 1 ==> a * b
2. [simplify.rewrite] [h]: P ==> true
3. [simplify.rewrite] [if_true]: ite true a 1 ==> a
4. [simplify.rewrite] [h]: P ==> true
5. [simplify.rewrite] [if_true]: ite true b 1 ==> b
6. [simplify.rewrite] [eq_self_iff_true]: a * b = a * b ==> true

But I just don't understand the syntax I am supposed to use. Any assistance would be greatly appreciated.

[Kyle Miller]

Does simp [h] work?

[William Sealy Gosset]

Maybe I need to state the broader context here. I was trying to break down the lemma ite_mul_one in the basic.lean file in the algebra.group portion of the library just to try to understand the syntax. Here is what I have so far:

@[to_additive]
lemma ite_mul_one {P : Prop} [decidable P] {a b : M} :
  ite P (a * b) 1 = ite P a 1 * ite P b 1 :=
begin
  by_cases h : P,
  {
    simp[h],
  },
  {
    simp[h],
  }
end

This clears the proof, but I want to replace the first simp[h] with what simp[h] is trying to do. That's where I am getting stuck.

[Kyle Miller]

Oh sorry, I didn't read what you wrote carefully enough. If you do squeeze_simp [h] you can see which lemmas simp is using.

[Kyle Miller]

But this should probably just give you something like simp only [h, if_true, eq_self_iff_true], based on the simp trace.

[Kyle Miller]

I'm not sure exactly what simp does with h, but you can use repeat { rw [if_pos h] } in the first case and repeat { rw [if_neg h] } in the second to simplify the ite's.

[William Sealy Gosset]

Thank you. This was enough to get me moving. I was able to close everything with the following.

@[to_additive]
lemma ite_mul_one {P : Prop} [decidable P] {a b : M} :
  ite P (a * b) 1 = ite P a 1 * ite P b 1 :=
begin
  by_cases h : P,
  {
    rw [if_pos h],
    rw [if_pos h],
    rw [if_pos h],
  },
  {
    rw [if_neg h],
    rw [if_neg h],
    rw [if_neg h],
    rw mul_one,
  }
end

[Kevin Buzzard]

There is also the split_ifs tactic

[William Sealy Gosset]

Kevin Buzzard said:

There is also the split_ifs tactic

Thank you, Kevin, both for the comment and the "The Future of Mathematics?" talk you gave, which is how I found out about Lean. I will try the split_ifs tactic later today.