Documentation

GaudisCrypt.Logic.HoareSplit

Splitting a sequence into two blocks #

splitSeq k regroups a right-nested sequence x₁; …; xₙ as {x₁; …; xₙ₋ₖ}; {xₙ₋ₖ₊₁; …; xₙ}, with a proof of denotational equivalence, and the tactic hoare_split k does that to the statement of a hoareStmt goal.

source
partial def GaudisCrypt.HoareSplit.seqLength (s : Lean.Expr) :
Lean.MetaM ℕ

The number of statements along the right spine of a sequence: x₁; …; xₙ, nested to the right as flattenSeq leaves it, has n. A let in the spine counts as one statement.

source
partial def GaudisCrypt.HoareSplit.splitSeq (k : ℕ) (s₀ : Lean.Expr) :
Lean.MetaM (Lean.Expr × Lean.Expr)

Split x₁; …; xₙ (nested to the right) into the two blocks {x₁; …; xₙ₋ₖ}; {xₙ₋ₖ₊₁; …; xₙ}, returning the result and a proof of ‹input›.Equiv result. The second block is the input's own subterm, the first is rebuilt. At the ends, k = 0 gives {x₁; …; xₙ}; skip and k = n gives skip; {x₁; …; xₙ}. Fails if k > n.

source
partial def GaudisCrypt.HoareSplit.splitSeq.go (m : ℕ) (s₀ : Lean.Expr) :
Lean.MetaM (Lean.Expr × Lean.Expr)

Split off the first m statements, 0 < m and fewer than the sequence has: by induction on m, re-associating x; ({l}; b) to {x; l}; b at each step.

source
def GaudisCrypt.HoareSplit.hoareSplit (k : ℕ) (g : Lean.MVarId) :
Lean.MetaM Lean.MVarId

On a goal hoareStmt A {x₁; …; xₙ} B, regroup the statement as {x₁; …; xₙ₋ₖ}; {xₙ₋ₖ₊₁; …; xₙ}, the last k statements in the second block (splitSeq; k = 0 and k = n pad the empty side with skip).

Equations
Instances For
    source
    def GaudisCrypt.HoareSplit.tacticHoare_split_ :
    Lean.ParserDescr

    hoare_split k: hoareSplit k on the main goal.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For