search

EasyCrypt / easycrypt

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

Simple tactics in proof-terms. #581

Closed strub closed 2 months ago

strub commented 4 months ago

Simple tactics (//, //#, /#) can now been used in proof-terms.

strub commented 4 months ago

Example:

require import AllCore.

op p : int -> int -> bool.

axiom A (x y : int) : x <= y => x-1 <= y => x-2 <= y => p x y.

lemma L x : p x x.
proof. by have := A x x //# // /#; [smt() | apply]. qed.