fix-negbLR

Author: oskgo

examples/PIR.ec

@@ -289,8 +289,8 @@ proof.
         by rewrite restrS 1:/# Hjx Hof /= fset0U.
       smt (is_restrS is_restr_addS oflist_cons).
     + conseq H => />.
-      + move=> &hr ?? His Hof Hb.
-        rewrite restrS 1:/# (@negbRL _ _ Hb);case: (j0 = i{hr}) => /= [<<- | ?].
+      + move=> &hr ?? His Hof /negbDR->.
+        rewrite restrS 1:/#;case: (j0 = i{hr}) => /= [<<- | ?].
         + rewrite xorC xor_true /=.
           case (j0 \in x) => /= Hj0x /=.
           + by rewrite (@eq_sym (oflist s0)) (@is_restr_diff j0 (restr x j0) _ His).

examples/vonNeumann.eca

@@ -100,15 +100,15 @@ while true (b2i (b = b')) 1 (2%r * p * (1%r - p))=> />.
   + seq 1: (b' = !x) (mu1 dbiased (!x)) 1%r (mu1 dbiased x) (mu dvn (pred1 x \o fst)) (b = x)=> //.
     + by auto.
     + by rnd (pred1 (!x)); auto.
-    + by conseq ih=> />; rewrite negbLR.
+    + by conseq ih=> />; rewrite -negbDR.
     + by rnd (pred1 x); auto=> /#.
-    by conseq ih=> /> &0 /negbRL /=.
+    by conseq ih=> /> &0 /negbDR /=.
   + by rnd (pred1 (!x)); auto=> /#.
   + seq 1: (b' = x) _ 0%r (mu1 dbiased (!x)) (mu dvn (pred1 x \o fst)) (b <> x)=> //.
     + by auto.
-    + by conseq ih=> /> &0 /negbRL ->; rewrite negbLR.
+    + by conseq ih=> /> &0 ->.
     + by rnd (pred1 (!x)); auto=> /#.
-    by conseq ih=> /> &0 /negbRL -> /negbRL ->.
+    by conseq ih=> /> &0 /negbDR -> /negbDR ->.
   move=> {ih} _ -> /=; rewrite !vnE /svn /(\o)/ pred1 /= /b2i /=.
   by move: x=> [] /=; rewrite !dbiased1E /#.
 + by auto=> />; rewrite dbiased_ll.

theories/prelude/Logic.ec

@@ -340,8 +340,10 @@ lemma negbK    : involutive [!]  by [].
 lemma negbNE b : !!b => b        by [].
 
 lemma negb_inj : injective [!]      by smt().
-lemma negbLR b c : b = !c => !b = c by smt().
-lemma negbRL b c : !b = c => b = !c by smt().
+lemma negbLR b c :   b  = !c => (!b) =  c by smt().
+lemma negbRL b c : (!b) =  c =>   b  = !c by smt().
+lemma negbDL b c : !(b = c) <=> (!b) =  c by smt().
+lemma negbDR b c : !(b = c) <=>   b  = !c by smt().
 
 lemma contra   c b : (c => b) => !b => !c by smt().
 lemma contraL  c b : (c => !b) => b => !c by smt().