Stream: Coq users

Topic: Cannot Rewrite and Unsure Why


view this post on Zulip Julia Dijkstra (Jan 07 2024 at 06:41):

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

view this post on Zulip Julia Dijkstra (Jan 07 2024 at 06:43):

I was able to rewrite valid' (_ !-> false) p, but not valid' (s !-> true; tail_map) p for instance.

view this post on Zulip Paolo Giarrusso (Jan 07 2024 at 12:43):

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