Implement custom elaboration for do notation

[sonmarcho]

1. The following Lean monadic expression:

let (a, b) <- f x
...

actually gets elaborated to:

let tmp <- f x
match tmp with
| (a, b) => ...

2. Moreover, the elaboration introduces auxiliary functions for the if then else like so:

let x <- if b then pure 0 else pure 1
...

-- Gets elaborated to:

have __f := fun x => ...
if b then do
  let y <- pure 0
  __f y
else do
  let y <- pure 1
  __f y

In order to fix those we should implement our own elaboration for the do notation (we could even remove the need to write do at all). For 1., it is possible to do something similar to the weakest precondition notation:

aeneas/backends/lean/Aeneas/Std/WP.lean

Lines 203 to 219 in 55d3f62

	/-- Macro expansion for a single element -/
	macro_rules
	| `($e ⦃ $x => $p ⦄) => do `(_root_.Aeneas.Std.WP.spec $e fun $x => $p)
	/-- Macro expansion for multiple elements -/
	macro_rules
	| `($e ⦃ $x $xs:term* => $p ⦄) => do
	let mut xs : List (TSyntax `term) := x :: xs.toList
	let rec run (xs : List (TSyntax `term)) : MacroM (TSyntax `term) := do
	match xs with
	| [] => `($p)
	| [x] => `(fun $x => $p)
	| x :: xs =>
	let xs ← run xs
	`(_root_.Aeneas.Std.WP.predn fun $x => $xs)
	let post ← run xs
	`(Aeneas.Std.WP.spec $e $post)