WordExpressions.lean`

20 declarations, 0 contain sorry, 0 declared as axioms

inductive OAI.WLIdentification.WordExpressions.Expr line 11
Source documentation
A finite, first-order word language. Loops capture a word length; their body sees both a unary iteration index and the previous accumulator.
```
inductive Expr : ℕ → Type where
…
```
def OAI.WLIdentification.WordExpressions.Expr.stages line 22
def OAI.WLIdentification.WordExpressions.Expr.eval line 26
def OAI.WLIdentification.WordExpressions.Expr.Bounded line 38
theorem OAI.WLIdentification.WordExpressions.Expr.length_le line 52

def OAI.WLIdentification.WordExpressions.Expr.code line 80

Source documentation

The result register is separate from immutable inputs; all temporary register numbers are at least base and are cleared before return.

def code : {n : ℕ} → Expr n → (Fin n → ℕ) → ℕ → ℕ → StackModel.Command ℕ (Option Bool)
  | _, .var i, env, out, base => copy (env i) out base
  | _, .nil, _, out, _ => clear out
  | _, .snoc e b, env, out, base => .seq (e.code env out base) (.push out (fun _ => b))
  | _, .drop e, env, out, base => .seq (e.code env out base) (.pop out (fun _ _ => none))
  | _, .cases e p q r, env, out, base =>
      .seq (e.code env base (base+1))
        (.seq (StackModel.Command.read base)
          (.seq (.branch Option.isSome
             (.branch (fun x => x.getD false) (r.code env out (base+1)) (q.code env out (base+1)))
             (p.code env out (base+1))) (clear base)))
  | _, .bind e f, env, out, base =>
…

Mentions: OAI.WLIdentification.WordExpressions.Expr, OAI.WLIdentification.StackModel.Command, OAI.WLIdentification.StackModel.Command.read

def OAI.WLIdentification.WordExpressions.Expr.cost line 103

theorem OAI.WLIdentification.StackModel.Command.drain_indexed line 118

Source documentation

General indexed captured-count iteration, preserving an arbitrary counter prefix during each body execution.

theorem drain_indexed (body : Command K (Option Bool)) (counter : K)
    (X : ℕ → K → Word) (hX : ∀ i, X i counter = []) (cost start : ℕ) (w : Word)
    (hbody : ∀ i, start ≤ i → i < start+w.length → ∀ v s,
      ∃ t ≤ cost, Exec body s (Function.update (X i) counter v) none
        (Function.update (X (i+1)) counter v) t) (s : Option Bool) :
    ∃ n ≤ (cost+2)*w.length+2,
      Exec (drain counter body) s (Function.update (X start) counter w) none
        (X (start+w.length)) n := by
…

Mentions: OAI.WLIdentification.StackModel.Command, OAI.WLIdentification.Word, OAI.WLIdentification.StackModel.Command.Exec, OAI.WLIdentification.StackModel.Command.drain

def OAI.WLIdentification.WordExpressions.Expr.Clean line 165
theorem OAI.WLIdentification.WordExpressions.Expr.Clean.mono line 167
theorem OAI.WLIdentification.WordExpressions.Expr.Clean.update line 170
theorem OAI.WLIdentification.WordExpressions.Expr.update_clean line 175
def OAI.WLIdentification.WordExpressions.Expr.Correct line 178
theorem OAI.WLIdentification.WordExpressions.Expr.correct_var line 185
theorem OAI.WLIdentification.WordExpressions.Expr.correct_nil line 199
theorem OAI.WLIdentification.WordExpressions.Expr.correct_snoc line 204
theorem OAI.WLIdentification.WordExpressions.Expr.correct_drop line 211
theorem OAI.WLIdentification.WordExpressions.Expr.env_update line 219
Source documentation
An allocated temporary is invisible to the immutable environment.
```
theorem env_update {n} (S : ℕ → Word) (env : Fin n → ℕ) (base : ℕ) (w : Word)
    (h : ∀ i, env i < base) : Function.update S base w ∘ env = S ∘ env := by
…
```
Mentions: OAI.WLIdentification.Word
theorem OAI.WLIdentification.WordExpressions.Expr.snoc_env_update line 224
theorem OAI.WLIdentification.WordExpressions.Expr.correct_bind line 232