Commit 8f46113a authored by Robbert Krebbers's avatar Robbert Krebbers

Make `dint_eq` more powerful.

It can now handle cases like `0 = S x`.
parent aac741fe
......@@ -336,6 +336,14 @@ Arguments dint_le !_ !_ / : simpl nomatch.
Definition dint_eq (di1 di2 : dint) : dbool :=
match di1, di2 with
| dInt x1 None, dInt x2 None => dBoolKnown (bool_decide (x1 = x2))
| dInt x1 (Some (IntNat _)), dInt x2 None =>
if decide (x2 < x1)
then dBoolKnown false
else dBoolUnknown (bool_decide (dint_interp di1 = dint_interp di2))
| dInt x1 None, dInt x2 (Some (IntNat _)) =>
if decide (x1 < x2)
then dBoolKnown false
else dBoolUnknown (bool_decide (dint_interp di1 = dint_interp di2))
| _, _ => dBoolUnknown (bool_decide (dint_interp di1 = dint_interp di2))
end.
Arguments dint_eq !_ !_ / : simpl nomatch.
......@@ -536,7 +544,8 @@ Lemma dint_eq_correct di1 di2 :
dbool_interp (dint_eq di1 di2) = bool_decide (dint_interp di1 = dint_interp di2).
Proof.
rewrite /dint_eq !dint_interp_alt.
destruct di1 as [? [[]|]], di2 as [? [[]|]]; simpl; repeat case_bool_decide; auto with lia.
destruct di1 as [? [[]|]], di2 as [? [[]|]]; simpl;
repeat (case_decide || case_bool_decide); auto with lia.
Qed.
Lemma dloc_plus_correct E dl di :
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment