I do not understand why I cannot rewrite using G in H to simplify it. What could be going wrong?

```
p, q : form
V : valuation
H : match match find_vars p ++ find_vars q with
| [] => if false && valid' (_ !-> false) q then Some (_ !-> false) else None
| s :: l => match find_valuation_aux <{ p /\ q }> l with
| Some tail_map => if valid' (s !-> true; tail_map) p && valid' (s !-> true; tail_map) q then Some (s !-> true; tail_map) else if valid' (s !-> false; tail_map) p && valid' (s !-> false; tail_map) q then Some (s !-> false; tail_map) else None
| None => None
end
end with
| Some _ => true
| None => false
end = true
val_p : find_valuation p = None
G : forall m : valuation, valid' m p = false
```

I was able to rewrite `valid' (_ !-> false) p`

, but not `valid' (s !-> true; tail_map) p`

for instance.

A problem is that in the second rewrite, tail_map is bound inside the expression, and the rewrite tactic cannot handle that. However, setoid_rewrite can.

Last updated: Jun 23 2024 at 05:02 UTC