From a3905ee0898ca417a064af0e906a6e80301e8f88 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20Dupressoir?= Date: Mon, 11 Jul 2022 10:31:07 +0100 Subject: [PATCH] slightly reduce reliance on trivial SMT calls --- theories/core/Bool.ec | 10 +++---- theories/core/Core.ec | 61 ++++++++++++++++++++++---------------- theories/crypto/PRP.eca | 4 +-- theories/datatypes/Real.ec | 6 +++- 4 files changed, 47 insertions(+), 34 deletions(-) diff --git a/theories/core/Bool.ec b/theories/core/Bool.ec index 9d20c7b091..2cc58ca51c 100644 --- a/theories/core/Bool.ec +++ b/theories/core/Bool.ec @@ -5,19 +5,19 @@ require import FinType. op (^^) (b1 b2:bool) = b1 = !b2. lemma nosmt xor_false b: b ^^ false = b -by smt(). +by case: b. lemma nosmt xor_true b: b ^^ true = !b -by smt(). +by case: b. lemma nosmt xorA b1 b2 b3: (b1 ^^ b2) ^^ b3 = b1 ^^ (b2 ^^ b3) -by smt(). +by case: b1 b2 b3=> - [] []. lemma nosmt xorC b1 b2: b1 ^^ b2 = b2 ^^ b1 -by smt(). +by case: b1 b2=> - []. lemma nosmt xorK b: b ^^ b = false -by smt(). +by case: b. clone FinType as BoolFin with type t <- bool, diff --git a/theories/core/Core.ec b/theories/core/Core.ec index a4bcab3fc9..53faffbdbf 100644 --- a/theories/core/Core.ec +++ b/theories/core/Core.ec @@ -34,8 +34,12 @@ proof. by case: ox. qed. (* -------------------------------------------------------------------- *) lemma nosmt frefl (f : 'a -> 'b): f == f by []. -lemma nosmt fsym (f g : 'a -> 'b): f == g => g == f by smt(). -lemma nosmt ftrans (f g h : 'a -> 'b): f == g => g == h => f == h by smt(). + +lemma nosmt fsym (f g : 'a -> 'b): f == g => g == f. +proof. by move=> + x - /(_ x) ->. qed. + +lemma nosmt ftrans (f g h : 'a -> 'b): f == g => g == h => f == h. +proof. by move=> + + x - /(_ x) -> /(_ x). qed. (* -------------------------------------------------------------------- *) lemma econgr1 ['a 'b] (f g : 'a -> 'b) x y: f == g => x = y => f x = g y. @@ -43,8 +47,12 @@ proof. by move/fun_ext=> -> ->. qed. (* -------------------------------------------------------------------- *) lemma nosmt f2refl (f : 'a -> 'b -> 'c): f === f by []. -lemma nosmt f2sym (f g : 'a -> 'b -> 'c): f === g => g === f by smt(). -lemma nosmt f2trans (f g h : 'a -> 'b -> 'c): f === g => g === h => f === h by smt(). + +lemma nosmt f2sym (f g : 'a -> 'b -> 'c): f === g => g === f. +proof. by move=> + x y - /(_ x y) ->. qed. + +lemma nosmt f2trans (f g h : 'a -> 'b -> 'c): f === g => g === h => f === h. +proof. by move=> + + x y - /(_ x y) -> /(_ x y). qed. lemma rel_ext (f g : 'a -> 'b -> 'c) : f = g <=> f === g. proof. @@ -196,39 +204,40 @@ pred (< ) (p q:'a -> bool) = (* proper *) (* -------------------------------------------------------------------- *) lemma nosmt subpred_eqP (p1 p2 : 'a -> bool): - (forall x, p1 x <=> p2 x) <=> (p1 <= p2 /\ p2 <= p1) -by smt(). + (forall x, p1 x <=> p2 x) <=> (p1 <= p2 /\ p2 <= p1). +proof. +split=> [PQ|[] + + x]. ++ by split=> x /PQ. +by move=> /(_ x) + /(_ x). +qed. lemma nosmt subpred_refl (X : 'a -> bool): X <= X by []. lemma nosmt subpred_asym (X Y:'a -> bool): - X <= Y => Y <= X => X = Y -by (rewrite fun_ext; smt). + X <= Y => Y <= X => X = Y. +proof. by rewrite pred_ext subpred_eqP. qed. lemma nosmt subpred_trans (X Y Z:'a -> bool): - X <= Y => Y <= Z => X <= Z -by smt(). + X <= Y => Y <= Z => X <= Z. +proof. by move=> + + x - /(_ x) Xx /(_ x) Yx /Xx /Yx. qed. (* -------------------------------------------------------------------- *) lemma nosmt pred1E (c : 'a) : pred1 c = ((=) c). proof. by apply fun_ext=> x; rewrite (eq_sym c). qed. lemma nosmt predU1l (x y : 'a) b : x = y => (x = y) \/ b by []. -lemma nosmt predU1r (x y : 'a) b : b => (x = y) \/ b by smt(). -lemma nosmt eqVneq (x y : 'a) : x = y \/ x <> y by smt(). +lemma nosmt predU1r (x y : 'a) b : b => (x = y) \/ b by case: b. +lemma nosmt eqVneq (x y : 'a) : x = y \/ x <> y by case: (x = y). -lemma nosmt predT_comp ['a 'b] (p : 'a -> 'b) : predT \o p = predT. -proof. by []. qed. +lemma nosmt predT_comp ['a 'b] (p : 'a -> 'b) : predT \o p = predT by []. lemma nosmt predIC (p1 p2 : 'a -> bool) : predI p1 p2 = predI p2 p1. proof. by apply fun_ext=> x; rewrite /predI andbC. qed. -lemma nosmt predIT ['a] p : predI<:'a> p predT = p. -proof. by []. qed. +lemma nosmt predIT ['a] p : predI<:'a> p predT = p by []. -lemma nosmt predTI ['a] p : predI<:'a> predT p = p. -proof. by []. qed. +lemma nosmt predTI ['a] p : predI<:'a> predT p = p by []. lemma nosmt predCI (p : 'a -> bool) : predI (predC p) p = pred0. proof. by apply/fun_ext=> x /=; delta => /=; rewrite andNb. qed. @@ -237,20 +246,20 @@ lemma nosmt predCU (p : 'a -> bool) : predU (predC p) p = predT. proof. by apply/fun_ext=> x /=; delta => /=; case: (p x). qed. lemma nosmt subpredUl (p1 p2 : 'a -> bool): - p1 <= predU p1 p2 -by smt(). + p1 <= predU p1 p2. +proof. by move=> x @/predU ->. qed. lemma nosmt subpredUr (p1 p2 : 'a -> bool): - p2 <= predU p1 p2 -by smt(). + p2 <= predU p1 p2. +proof. by move=> x @/predU ->. qed. lemma nosmt predIsubpredl (p1 p2 : 'a -> bool): - predI p1 p2 <= p1 -by smt(). + predI p1 p2 <= p1. +proof. by move=> x @/predI [] ->. qed. lemma nosmt predIsubpredr (p1 p2 : 'a -> bool): - predI p1 p2 <= p2 -by smt(). + predI p1 p2 <= p2. +proof. by move=> x @/predI [] _ ->. qed. lemma nosmt predTofV (f : 'a -> 'b): predT \o f = predT. proof. by apply/fun_ext=> x. qed. diff --git a/theories/crypto/PRP.eca b/theories/crypto/PRP.eca index 0d19e518b5..3fc416c722 100644 --- a/theories/crypto/PRP.eca +++ b/theories/crypto/PRP.eca @@ -293,8 +293,8 @@ qed. lemma collision_stable (m:(D,D) fmap) y y': collision m => y \notin m => - collision m.[y <- y'] -by smt(collision_add). + collision m.[y <- y']. +proof. by move=> h /collision_add /= ->; rewrite h. qed. (** To factor out the difficult step, we parameterize the PRP by a procedure that samples its output, and provide two instantiations diff --git a/theories/datatypes/Real.ec b/theories/datatypes/Real.ec index a48a969c85..7fc21f4e0c 100644 --- a/theories/datatypes/Real.ec +++ b/theories/datatypes/Real.ec @@ -23,8 +23,12 @@ lemma nosmt fromint0 : 0%r = CoreReal.zero by []. lemma nosmt fromint1 : 1%r = CoreReal.one by []. lemma nosmt fromintN (z : int) : (-z)%r = - z%r by smt(). + lemma nosmt fromintD (z1 z2 : int) : (z1 + z2)%r = z1%r + z2%r by smt(). -lemma nosmt fromintB (z1 z2 : int) : (z1 - z2)%r = z1%r - z2%r by smt(). + +lemma nosmt fromintB (z1 z2 : int) : (z1 - z2)%r = z1%r - z2%r. +proof. by rewrite fromintD fromintN. qed. + lemma nosmt fromintM (z1 z2 : int) : (z1 * z2)%r = z1%r * z2%r by smt(). lemma nosmt eq_fromint (z1 z2 : int) :