search

EasyCrypt / easycrypt

EasyCrypt: Computer-Aided Cryptographic Proofs
MIT License
306 stars 46 forks source link

feature request: comparison of record literals should simply to the conjunction of components #551

Closed alleystoughton closed 3 months ago

alleystoughton commented 3 months ago

When tuple literals are compared, it would be good to reduce them to the conjunction of the comparison of their fields, analogously to what happens with comparison of tuple literals.

E.g.,

type t = { x: int; y: int }.

lemma L x y :
  x = 0 => y = 1 => {| x = x; y = y |} = {| x = 0; y = 1 |}.
proof. move=> xE yE /=; split; assumption. qed.