wp: use named cases instead of positional rcases in the exec unfold lemmas (#128)

`exec_loop_cons_unfold`, `exec_block_cons` and `exec_iff_cons` destructure an
`exec …` result with a positional constructor pattern
(`⟨_,_⟩ | ⟨n,_,_⟩ | … `), which silently depends on the declaration order of
`Continuation`'s constructors — reordering them would break these proofs in a
confusing way. This switches each to a named `cases … with | Fallthrough .. | …`
form. Purely internal to the tactic blocks; the theorem statements and the proof
behaviour of every arm are unchanged.

Author: El3ssar

interpreter/Interpreter/Wasm/Semantics/Lemmas.lean

@@ -400,15 +400,15 @@ theorem exec_block_cons
            { s' with values := s'.values.take rs ++ s.values.drop ps } rest env
        | other                => other) := by
   simp only [exec, execOne.eq_def]
-  rcases exec fuel m st s body env with _ | ⟨n, _, _⟩ | _ | _ | _ | _ | _ | _
-  · rfl
-  · cases n <;> rfl
-  · rfl
-  · rfl
-  · rfl
-  · rfl
-  · rfl
-  · rfl
+  cases exec fuel m st s body env with
+  | Fallthrough _ _ => rfl
+  | Break n _ _ => cases n <;> rfl
+  | Return _ _ => rfl
+  | Trap _ _ => rfl
+  | Invalid _ => rfl
+  | OutOfFuel => rfl
+  | ReturnCall _ _ _ => rfl
+  | Throwing _ _ _ _ => rfl
 
 theorem exec_iff_cons
     {m : Module} {env : HostEnv α} {st : Store α} {s : Locals}
@@ -428,17 +428,26 @@ theorem exec_iff_cons
        | other                => other) := by
   simp only [exec, execOne.eq_def, hStack]
   by_cases hc : c ≠ 0
-  all_goals first
-    | (simp only [if_pos hc]
-       rcases exec fuel m st { s with values := vs } thn env with _ | ⟨n, _, _⟩ | _ | _ | _ | _
-       · rfl
-       · cases n <;> rfl
-       all_goals rfl)
-    | (simp only [if_neg hc]
-       rcases exec fuel m st { s with values := vs } els env with _ | ⟨n, _, _⟩ | _ | _ | _ | _
-       · rfl
-       · cases n <;> rfl
-       all_goals rfl)
+  · simp only [if_pos hc]
+    cases exec fuel m st { s with values := vs } thn env with
+    | Fallthrough _ _ => rfl
+    | Break n _ _ => cases n <;> rfl
+    | Return _ _ => rfl
+    | Trap _ _ => rfl
+    | Invalid _ => rfl
+    | OutOfFuel => rfl
+    | ReturnCall _ _ _ => rfl
+    | Throwing _ _ _ _ => rfl
+  · simp only [if_neg hc]
+    cases exec fuel m st { s with values := vs } els env with
+    | Fallthrough _ _ => rfl
+    | Break n _ _ => cases n <;> rfl
+    | Return _ _ => rfl
+    | Trap _ _ => rfl
+    | Invalid _ => rfl
+    | OutOfFuel => rfl
+    | ReturnCall _ _ _ => rfl
+    | Throwing _ _ _ _ => rfl
 
 theorem exec_call_cons
     {m : Module} {env : HostEnv α} {st : Store α} {s : Locals}

interpreter/Interpreter/Wasm/Wp/Loop.lean

@@ -36,15 +36,28 @@ private theorem exec_loop_cons_unfold {α : Type} (fuel : Nat) (m : Module)
        | .Break (k+1) st' s' => .Break k st' s'
        | other => other) := by
   simp only [exec, execOne_loop_succ]
-  rcases hb : exec fuel m st s body env with
-    ⟨_, _⟩ | ⟨n, _, _⟩ | ⟨_, _⟩ | _ | _ | _ | ⟨_, _, _⟩ | ⟨_, _, _, _⟩
-  · rfl
-  · cases n
-    · simp only
-      rcases hk : execOne fuel _ _ _ (.loop ps rs body) env
-        with ⟨_, _⟩ | ⟨_, _, _⟩ | ⟨_, _⟩ | _ | _ | _ | ⟨_, _, _⟩ | ⟨_, _, _, _⟩ <;> rfl
-    · rfl
-  all_goals rfl
+  cases hb : exec fuel m st s body env with
+  | Fallthrough _ _ => rfl
+  | Break n _ _ =>
+    cases n with
+    | zero =>
+      simp only
+      cases hk : execOne fuel _ _ _ (.loop ps rs body) env with
+      | Fallthrough _ _ => rfl
+      | Break _ _ _ => rfl
+      | Return _ _ => rfl
+      | Trap _ _ => rfl
+      | Invalid _ => rfl
+      | OutOfFuel => rfl
+      | ReturnCall _ _ _ => rfl
+      | Throwing _ _ _ _ => rfl
+    | succ _ => rfl
+  | Return _ _ => rfl
+  | Trap _ _ => rfl
+  | Invalid _ => rfl
+  | OutOfFuel => rfl
+  | ReturnCall _ _ _ => rfl
+  | Throwing _ _ _ _ => rfl
 
 theorem wp_loop_cons {ps rs : Nat} {body rest : Program} {Q : Assertion α}
     (Inv : AssertionF α) (μ : Store α → Locals → Nat)