EasyCrypt / easycrypt

EasyCrypt: Computer-Aided Cryptographic Proofs
MIT License
320 stars 49 forks source link

anomaly with `hint simplify [reduce]` for equational lemma involving projection #613

Closed alleystoughton closed 2 months ago

alleystoughton commented 2 months ago

Should the following use of hint simplify [reduce] really be illegal? If so, a proper error message would be good.

require import AllCore.

lemma fst_eq (x y : int) :
  (x, y).`1 = x.
proof. trivial. qed.

hint simplify [reduce] fst_eq.
(*
anomaly: EcLib.EcReduction.User.InvalidUserRule(1)
*)
strub commented 2 months ago

Yes, there are two things here :

strub commented 2 months ago

Do you have a scenario of such rules not of the form (x1, ..., xn).'k = xk?

alleystoughton commented 2 months ago

Do you have a scenario of such rules not of the form (x1, ..., xn).'k = xk?

No.

alleystoughton commented 2 months ago

Do you have a scenario of such rules not of the form (x1, ..., xn).'k = xk?

No.

Sorry, let me try again. Actually, the above is already handled by simplification, so it's very useful to add as a simplification hint. (The issue of the error message is separate.)

But what about:

op x : int * bool = (3, false).

lemma x_1 :
  x.`1 = 3.
proof. trivial. qed.

lemma x_2 :
  x.`2 = false.
proof. trivial. qed.

hint simplify [reduce] x_1, x_2.

lemma goo :
  x.`1 = 3.
proof.
rewrite /=.
(*
Current goal

Type variables: <none>

------------------------------------------------------------------------
x.`1 = 3
*)

(this was under your P-R).

strub commented 2 months ago

Fixed