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: Oct 13 2024 at 01:02 UTC