fix separateTupleEqs and put it behind an opt-in option

Aegis/Analyzer.lean

@@ -72,8 +72,8 @@ def processAndOrTree (finputs : List (Nat × Identifier)) (cs : AndOrTree) :
     let mut intRefs := intRefs
     -- Normalize conjunctions and disjunctions in the tree
     if ← Sierra.Options.aegis.normalize.isEnabled then cs := cs.normalize
-    -- Disassemble equalities between tuples (disabled for now)
-    -- let cs := cs.separateTupleEqs
+    -- Disassemble equalities between tuples (disabled by default)
+    if ← Sierra.Options.aegis.separateTuples.isEnabled then cs := cs.separateTupleEqs
     -- Contract equalities in the tree
     if ← Sierra.Options.aegis.contract.isEnabled then
       cs := cs.contractEqs (Prod.snd <$> intRefs).contains

Aegis/ExprUtil.lean

@@ -113,8 +113,16 @@ partial def AndOrTree.separateTupleEqs (t : AndOrTree) : AndOrTree :=
     | .some (_, lhs, rhs) =>
       match lhs.tuple?, rhs.tuple? with
       | .some ⟨α, β, x₁, y₁⟩, .some ⟨_, _, x₂, y₂⟩ =>
-        let fstEq := Sierra.Expr.mkEq α x₁ y₁
-        let sndEq := Sierra.Expr.mkEq β x₂ y₂
+        let fstEq := Sierra.Expr.mkEq α x₁ x₂
+        let sndEq := Sierra.Expr.mkEq β y₁ y₂
+        .cons fstEq [AndOrTree.separateTupleEqs (AndOrTree.cons sndEq ts)]
+      | .some ⟨α, β, x, y⟩, _ =>
+        let fstEq := Sierra.Expr.mkEq α x (Expr.proj `Prod 0 rhs)
+        let sndEq := Sierra.Expr.mkEq β y (Expr.proj `Prod 1 rhs)
+        .cons fstEq [AndOrTree.separateTupleEqs (AndOrTree.cons sndEq ts)]
+      | _, .some ⟨α, β, x, y⟩ =>
+        let fstEq := Sierra.Expr.mkEq α (Expr.proj `Prod 0 lhs) x
+        let sndEq := Sierra.Expr.mkEq β (Expr.proj `Prod 1 lhs) y
         .cons fstEq [AndOrTree.separateTupleEqs (AndOrTree.cons sndEq ts)]
       | _, _ => .cons e (AndOrTree.separateTupleEqs <$> ts)
     | .none => .cons e (AndOrTree.separateTupleEqs <$> ts)

Aegis/Options.lean

@@ -6,19 +6,23 @@ namespace Sierra.Options
 
 register_option aegis.normalize : Bool :=
   let descr := "Set whether to normalize conjunctions and disjunctions in the proof goal."
-  { defValue := true, group := "aesop", descr := descr }
+  { defValue := true, group := "aegis", descr := descr }
 
 register_option aegis.contract : Bool :=
   let descr := "Set whether the proof goal of `aegis_prove` should contract equalities."
-  { defValue := true, group := "aesop", descr := descr }
+  { defValue := true, group := "aegis", descr := descr }
 
 register_option aegis.filterUnused : Bool :=
   let descr := "Set whether to filter out intermediate variables which do not actually appear in the proof goal."
-  { defValue := true, group := "aesop", descr := descr }
+  { defValue := true, group := "aegis", descr := descr }
+
+register_option aegis.separateTuples : Bool :=
+  let descr := "Set whether replace equalities between tuples by equalities between the components."
+  { defValue := false, group := "aegis", descr := descr }
 
 register_option aegis.trace : Bool :=
   let descr := "Set whether to output trace information."
-  { defValue := false, group := "aesop", descr := descr }
+  { defValue := false, group := "aegis", descr := descr }
 
 
 end Sierra.Options

Aegis/Tests/Commands.lean

@@ -213,9 +213,10 @@ aegis_spec "test::u256_safe_divmod" :=
   ∧ U128_MOD * ZMod.val ρ.2.2 + ZMod.val ρ.2.1 =
     (U128_MOD * ZMod.val a.2 + ZMod.val a.1) % (U128_MOD * ZMod.val b.2 + ZMod.val b.1)
 
+set_option aegis.separateTuples true in
 aegis_prove "test::u256_safe_divmod" :=
   fun _ _ a b _ ρ => by
-  rintro ⟨_,_,h₁,h₂,rfl⟩
+  rintro ⟨_,_,_,h₁,h₂,rfl,rfl,rfl⟩
   exact ⟨h₁,h₂⟩
 
 aegis_load_string "type Array<felt252> = Array<felt252> [storable: true, drop: true, dup: false, zero_sized: false];