ZeroExpr must check for a disjonction for multiplication (#132)

* zeroExpr must check for a disjonction for multiplication

* mirror was not mirroring the mult

Author: samuelchassot

tutorials/const-fold/ConstFold.scala

@@ -26,11 +26,17 @@ object ConstFold:
       case Var(_) => false
       case Add(e1, e2) => zeroExpr(e1) && zeroExpr(e2)
       case Minus(e1, e2) => zeroExpr(e1) && zeroExpr(e2)
-      case Mul(e1, e2) => zeroExpr(e1) && zeroExpr(e2)
+      case Mul(e1, e2) => zeroExpr(e1) || zeroExpr(e2)
 
-  def lemma(ctx: Env, @induct e: Expr): Unit = {
+  def lemma(ctx: Env, e: Expr): Unit = {
     require(zeroExpr(e))
-    ()
+    e match
+      case Number(_) => ()
+      case Var(_) => ()
+      case Add(e1, e2) => lemma(ctx, e1); lemma(ctx, e2)
+      case Minus(e1, e2) => lemma(ctx, e1); lemma(ctx, e2)
+      case Mul(e1, e2) => if (zeroExpr(e1)) then lemma(ctx, e1) else lemma(ctx, e2)
+    
   }.ensuring(_ => evaluate(ctx, e) == 0)
 
   def mirror(e: Expr)(anyCtx: Env = zeroEnv): Expr = {
@@ -39,7 +45,7 @@ object ConstFold:
       case Var(name) => e
       case Add(e1, e2) => Add(mirror(e2)(anyCtx), mirror(e1)(anyCtx))
       case Minus(e1, e2) => Minus(mirror(e1)(anyCtx), mirror(e2)(anyCtx))
-      case Mul(e1, e2) => Mul(mirror(e1)(anyCtx), mirror(e2)(anyCtx))
+      case Mul(e1, e2) => Mul(mirror(e2)(anyCtx), mirror(e1)(anyCtx))
   }.ensuring(evaluate(anyCtx, _) == evaluate(anyCtx,e))
 
   abstract class SoundSimplifier: