ite and decidability instances

Stream: new members

[Jake Levinson]

I just encountered a funny problem with (I think) decidability instances in an ite expression. Here's a #mwe:

example (p q : Prop) (a b c : ℕ) [decidable p] [decidable q]:
  ite (p ∧ q) a b = c :=
begin
  have hp : p := sorry,     -- first stage of proof proves p
  simp_rw and_iff_right hp, -- new goal is : ⊢ ite q a b = a
  have hq : q := sorry,     -- second stage of proof proves q
  --rw if_pos hq,
    -- rewrite tactic failed, did not find
    -- instance of the pattern in the target
    -- expression
    --   ite q ?m_2 ?m_3
    -- goal was:
    --   ⊢ ite q a b = a
  rw if_pos, exact hq, -- works!
end

Clicking on ite q a b in the infoview shows that the decidability instance for the q is eq.rec and.decidable _ (with propext (and_iff_right hp) deeper inside there). Whereas a plain ite q a b would just use the given decidability instance for q. In fact even change ite q a b = a fails ("not definitionally equal").

So somehow the simp_rw line is simplifying p ∧ q to q but making the decidability instance more complicated.

I don't know much about how simp_rw works. I guess I could just not do that line. But in my actual context, it is very convenient to simplify the ite expression in place after I get hp : p.

[Ruben Van de Velde]

You're missing some imports still

[Jake Levinson]

Ah, sorry - fixed.

[Kevin Buzzard]

Probably convert if_pos hq works in this case

[Jake Levinson]

Hmmm. It works in the mwe but not in the original context. I tried a few other convert/refine commands and didn't succeed.

[Jake Levinson]

Just found this thread which is helpful too: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Rewrite.20condition.20in.20.60ite.60.3F.

I'll try the split_ifs tactic tomorrow. Though, it would be nice to be able to rewrite in the conditional of an ite (just like rewriting anywhere else).

[Jake Levinson]

(and I'll see if I can figure out why my larger example doesn't work)

[Kevin Buzzard]

Yeah your error is a bit terrifying. I guess another possibility in your case is not to mess with p \and q until you've got the proofs of both p and q and then use if_pos without ever simping

[Jake Levinson]

Followup - having the goal be ite (p ∧ q) a b ≤ c (instead of = c) makes convert if_pos q no longer work.

Also, replacing the simp_rw line by simp [hp] actually works! ... I should look at what the simp is doing.

[Jake Levinson]

Aha! if_congr does this correctly. This seems like the intended way to rewrite in an ite conditional, actually. I wonder why simp_rw wasn't using it but simp was.

example (p q q' : Prop) (a b c : ℕ) [decidable p] [decidable q]:
  ite (p ∧ q) a b ≤ c :=
begin
  have hp : p := sorry,     -- first stage of proof proves p
  rw if_congr (and_iff_right hp) (eq.refl _) (eq.refl _),
  have hq : q := sorry,     -- second stage of proof proves q
  rw if_pos hq,             -- works!
  sorry,
end

[Jake Levinson]

Though, if_congr still doesn't seem to correctly infer the decidability instance...

[Reid Barton]

I thought there was something like if_pos' that uses {} brackets for the decidability instance--did it not actually get added?

[Reid Barton]

It also looks like you should be able to simp_rw the condition to true and then use docs#if_true which doesn't care about the instance

[Yaël Dillies]

Jake Levinson said:

Followup - having the goal be ite (p ∧ q) a b ≤ c (instead of = c) makes convert if_pos q no longer work.

Also, replacing the simp_rw line by simp [hp] actually works! ... I should look at what the simp is doing.

You should use convert (if_pos q).le (although I guess your hypothesis q is not called q again). The goal is an inequality and you tried to provide an equality.

[Jake Levinson]

@Reid Barton aha, simp_rw [hq, if_true] seems to work nicely.

@Yaël Dillies Hmm, when I try convert (if_pos hq).le the goal becomes c = a rather than a ≤ c. Something pattern-matching incorrectly?

[Yaël Dillies]

No, that's expected. I thought you wanted to reach that state.

[Yaël Dillies]

If you want to reach a ≤ c instead, try convert (if_pos hq).trans_le _.

[Jake Levinson]

Great, this all seems to work. Thanks!