working around 'invalid simplification lemma'

Stream: new members

[Ryan Greenblatt]

I am running into 'invalid simplification lemma' and when I set trace.simp_lemmas it says:

[simp_lemmas.invalid] LHS of rule derived from '[anonymous]' occurs in one of the hypotheses

I am just trying to subsitute a propositon into an 'if then else' statement (dite in practice).
Are there any work arounds? Maybe some way to just subsitute it the first time which should get around where the hypothesis occurs.
(I've tried playing around with various approaches to simp, but I couldn't get any to work).

Unfortunately, making a minimal reproduction is non-trivial, so for now I'm just going to put my snippets of my code here and hope that the issue is obvious.

I have a function:

def compute_sat (g : choice_func) : formula → bool
| [] := tt
| f :=
  if h : f.join = [] then ff else
  let non_empty_f := (subtype.mk f h) in
  let l := g.val non_empty_f in
  have in_joined : l ∈ f.join ∨ l_not l ∈ f.join :=
    by apply g.property non_empty_f,
  have in_joined_flip : l_not l ∈ f.join ∨ l_not (l_not l) ∈ f.join :=
  begin
    apply or.symm,
    rw l_inv,
    exact in_joined,
  end,

  have first : num_literals (simplify (assign_lit l f))
      < num_literals f := reduces _ _ in_joined,
  have second : num_literals (simplify (assign_lit (l_not l) f))
      < num_literals f := reduces _ _ in_joined_flip,

  compute_sat (simplify (assign_lit l f)) ||
    compute_sat (simplify (assign_lit (l_not l) f))
using_well_founded {rel_tac := λ _ _,
                    `[exact ⟨_, measure_wf num_literals⟩]}

and a lemma:

set_option trace.simp_lemmas true

lemma compute_sat_ff (f : formula) (hd : clause) (g : choice_func) (h : (hd :: f).join = list.nil) :
compute_sat g (hd :: f) = ff := begin
  rw compute_sat,
  simp at h,
  cases h,
  simp [h_right], -- fails with 'invalid simplification lemma :(
end

Presumably the issue is because I branch on f.join = [] and also use that the prop is false in the else case.
If anyone wants to look at the full code I guess I can post it: https://github.com/rgreenblatt/verified_sat/blob/f75356e8e6b23f298cbaf8f0366315bbc7c3ff76/src/sat.lean#L217-L223

[Eric Wieser]

Can you give the full error message including the goal state?

[Alex J. Best]

The lemma you want is docs#dif_pos,

lemma compute_sat_ff (f : formula) (hd : clause) (g : choice_func) (h : (hd :: f).join = list.nil) :
compute_sat g (hd :: f) = ff := begin
  rw compute_sat,
  simp at h,
  rw dif_pos,
  simpa,
end