slightly reduce reliance on trivial SMT calls

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,

theories/core/Core.ec

@@ -34,17 +34,25 @@ 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.
 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.

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

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) :