Cairn · module

Cairn.Text.Proofs

lean/Cairn/Text/Proofs.lean

Theorems about Cairn.Text.Field

  1. In bounds. Field.wf_empty, Field.wf_ofString, Field.wf_apply, Field.wf_applyAll, Field.wf_reachable, Field.view_wf: caret, anchor, marked range and every undo and redo entry stay within 0 … length, from any well-formed field, for every op.
  2. Round trip. Field.insert_deleteBackward, Field.insert_deleteBackward': typing s at a collapsed caret, then deleting backward s.length times, restores the text and selection.
  3. Undo. Field.undo_apply (one edit, outside a typing run or composition), Field.undo_typing_run (a run of coalesced typing), Field.undo_composition (a whole IME composition), Field.redo_undo.
  4. Selection replace. Field.insert_replaces_selection, Field.insert_replaces_selection', Field.insert_replace.
  5. Copy is pure. Field.apply_copy, Field.selected_spec.
  6. Movement never edits. Field.apply_movement_text.
  7. Single line. Field.singleLine_apply, Field.view_no_newline (and WF.single).
  8. Secure fields. SecureField.apply_no_clipboard (copy and cut, and every other op, never set the clipboard; SecureField.apply_copy, SecureField.apply_cut beep and change nothing), SecureField.history_empty, SecureField.applyAll_history (no undo or redo history, ever), SecureField.apply_edit (every other op edits as Field.apply does), SecureField.wf_apply, SecureField.view_text (the view holds a bullet per scalar) and SecureField.view_agree (the view depends on the text only through its length).

Imports Cairn.Text.Field

Order

Definitions 5

def

Cairn.TextOp.isMovement

lean/Cairn/Text/Proofs.lean:312
isMovement : TextOp → Bool
def

Cairn.TextOp.isHistory

lean/Cairn/Text/Proofs.lean:422
isHistory : TextOp → Bool
def

Cairn.TextOp.isTyping

lean/Cairn/Text/Proofs.lean:479
isTyping : TextOp → Bool

Ops that join an open typing step.

def

Cairn.Text.Field.ChangesEach

lean/Cairn/Text/Proofs.lean:507
ChangesEach : Field → List TextOp → Prop

Every op in ops changes the text when applied in turn.

def

Cairn.TextOp.isRefused

lean/Cairn/Text/Proofs.lean:592
isRefused : TextOp → Bool

Ops a secure field refuses.

Theorems 72

theorem

Cairn.Text.span_le

provedlean/Cairn/Text/Proofs.lean:29
span_le (p : Char → Bool) (l : List Char) : span p l ≤ l.length
theorem

Cairn.Text.wordLeft_le

provedlean/Cairn/Text/Proofs.lean:36
wordLeft_le (t : List Char) (i : Nat) : wordLeft t i ≤ i
theorem

Cairn.Text.le_wordRight

provedlean/Cairn/Text/Proofs.lean:39
le_wordRight (t : List Char) (i : Nat) : i ≤ wordRight t i
theorem

Cairn.Text.wordRight_le

provedlean/Cairn/Text/Proofs.lean:42
wordRight_le (t : List Char) (i : Nat) (h : i ≤ t.length) :
  wordRight t i ≤ t.length
theorem

Cairn.Text.length_splice

provedlean/Cairn/Text/Proofs.lean:49
length_splice (t s : List Char) (a b : Nat) (hab : a ≤ b) (hb : b ≤ t.length) :
  (splice t a b s).length = a + s.length + (t.length - b)
theorem

Cairn.Text.singleLine_splice

provedlean/Cairn/Text/Proofs.lean:54
singleLine_splice {t s : List Char} (a b : Nat) (ht : SingleLine t)
  (hs : SingleLine s) : SingleLine (splice t a b s)
theorem

Cairn.Text.singleLine_nil

provedlean/Cairn/Text/Proofs.lean:63
singleLine_nil : SingleLine []
theorem

Cairn.Text.singleLine_flatten

provedlean/Cairn/Text/Proofs.lean:65
singleLine_flatten (c : Char) : isLineBreak (flatten c) = false
theorem

Cairn.Text.singleLine_clean

provedlean/Cairn/Text/Proofs.lean:71
singleLine_clean (s : String) : SingleLine (clean s)
theorem

Cairn.Text.length_clean

provedlean/Cairn/Text/Proofs.lean:76
length_clean (s : String) : (clean s).length = s.length
theorem

Cairn.Text.map_flatten_of_singleLine

provedlean/Cairn/Text/Proofs.lean:79
map_flatten_of_singleLine {l : List Char} : SingleLine l → List.map flatten l = l
theorem

Cairn.Text.clean_of_singleLine

provedlean/Cairn/Text/Proofs.lean:86
clean_of_singleLine {s : String} (h : SingleLine s.toList) : clean s = s.toList
theorem

Cairn.Text.Field.wf_empty

provedlean/Cairn/Text/Proofs.lean:93
wf_empty (p : String) : (empty p).WF
theorem

Cairn.Text.Field.wf_ofString

provedlean/Cairn/Text/Proofs.lean:96
wf_ofString (s p : String) : (ofString s p).WF
theorem

Cairn.Text.Field.snapshot_wf

provedlean/Cairn/Text/Proofs.lean:99
snapshot_wf {f : Field} (h : f.WF) : f.snapshot.WF
theorem

Cairn.Text.Field.lo_le_hi

provedlean/Cairn/Text/Proofs.lean:102
lo_le_hi (f : Field) : f.lo ≤ f.hi
theorem

Cairn.Text.Field.hi_le

provedlean/Cairn/Text/Proofs.lean:104
hi_le {f : Field} (h : f.WF) : f.hi ≤ f.text.length
theorem

Cairn.Text.Field.target_wf

provedlean/Cairn/Text/Proofs.lean:107
target_wf {f : Field} (h : f.WF) :
  f.target.fst ≤ f.target.snd ∧ f.target.snd ≤ f.text.length
theorem

Cairn.Text.Field.targetOr_wf

provedlean/Cairn/Text/Proofs.lean:113
targetOr_wf {f : Field} (h : f.WF) (r : Option (Nat × Nat)) :
  (f.targetOr r).fst ≤ (f.targetOr r).snd ∧ (f.targetOr r).snd ≤ f.text.length
theorem

Cairn.Text.Field.edit_text

provedlean/Cairn/Text/Proofs.lean:119
edit_text (f : Field) (t : List Char) (c a : Nat) (p ty : Bool) :
  (f.edit t c a p ty).text = t
theorem

Cairn.Text.Field.edit_caret

provedlean/Cairn/Text/Proofs.lean:121
edit_caret (f : Field) (t : List Char) (c a : Nat) (p ty : Bool) :
  (f.edit t c a p ty).caret = c
theorem

Cairn.Text.Field.edit_anchor

provedlean/Cairn/Text/Proofs.lean:123
edit_anchor (f : Field) (t : List Char) (c a : Nat) (p ty : Bool) :
  (f.edit t c a p ty).anchor = a
theorem

Cairn.Text.Field.edit_marked

provedlean/Cairn/Text/Proofs.lean:125
edit_marked (f : Field) (t : List Char) (c a : Nat) (p ty : Bool) :
  (f.edit t c a p ty).marked = none
theorem

Cairn.Text.Field.wf_edit

provedlean/Cairn/Text/Proofs.lean:128
wf_edit {f : Field} (h : f.WF) {t : List Char} {c a : Nat} (p ty : Bool)
  (ht : SingleLine t) (hc : c ≤ t.length) (ha : a ≤ t.length) : (f.edit t c a p ty).WF
theorem

Cairn.Text.Field.wf_moveTo

provedlean/Cairn/Text/Proofs.lean:146
wf_moveTo {f : Field} (h : f.WF) {i : Nat} (hi : i ≤ f.text.length)
  (ext : Bool) : (f.moveTo i ext).WF
theorem

Cairn.Text.Field.wf_deleteRange

provedlean/Cairn/Text/Proofs.lean:151
wf_deleteRange {f : Field} (h : f.WF) {a b : Nat} (hab : a ≤ b)
  (hb : b ≤ f.text.length) (co : Bool := false) : (f.deleteRange a b co).WF
theorem

Cairn.Text.Field.wf_deleteSelOr

provedlean/Cairn/Text/Proofs.lean:156
wf_deleteSelOr {f : Field} (h : f.WF) {a b : Nat} (hab : a ≤ b)
  (hb : b ≤ f.text.length) (co : Bool := false) : (f.deleteSelOr a b co).WF
theorem

Cairn.Text.Field.wf_insert

provedlean/Cairn/Text/Proofs.lean:163
wf_insert {f : Field} (h : f.WF) (s : String)
  (r : Option (Nat × Nat) := none) : (f.insert s r).WF
theorem

Cairn.Text.Field.wf_paste

provedlean/Cairn/Text/Proofs.lean:170
wf_paste {f : Field} (h : f.WF) (s : String) : (f.paste s).WF
theorem

Cairn.Text.Field.mem_push

provedlean/Cairn/Text/Proofs.lean:176
mem_push {p : Prop} [Decidable p] {t x : Snapshot} {l : List Snapshot}
  (h : t ∈ if p then x :: l else l) : t = x ∨ t ∈ l
theorem

Cairn.Text.Field.mem_clear

provedlean/Cairn/Text/Proofs.lean:182
mem_clear {p : Prop} [Decidable p] {t : Snapshot} {l : List Snapshot}
  (h : t ∈ if p then [] else l) : t ∈ l
theorem

Cairn.Text.Field.wf_setMarked

provedlean/Cairn/Text/Proofs.lean:188
wf_setMarked {f : Field} (h : f.WF) (s : String) (i n : Nat)
  (r : Option (Nat × Nat) := none) : (f.setMarked s i n r).WF
theorem

Cairn.Text.Field.wf_undo

provedlean/Cairn/Text/Proofs.lean:209
wf_undo {f : Field} (h : f.WF) : f.undo.fst.WF
theorem

Cairn.Text.Field.wf_redo

provedlean/Cairn/Text/Proofs.lean:222
wf_redo {f : Field} (h : f.WF) : f.redo.fst.WF
theorem

Cairn.Text.Field.wf_apply

provedlean/Cairn/Text/Proofs.lean:239
wf_apply (op : TextOp) {f : Field} (h : f.WF) : (apply op f).fst.WF

Every op keeps every index (caret, anchor, marked range, and every undo and redo entry) within 0 … length, and the text a single line.

theorem

Cairn.Text.Field.wf_applyAll

provedlean/Cairn/Text/Proofs.lean:282
wf_applyAll (ops : List TextOp) {f : Field} : f.WF → (f.applyAll ops).WF
theorem

Cairn.Text.Field.wf_reachable

provedlean/Cairn/Text/Proofs.lean:287
wf_reachable (p : String) (ops : List TextOp) : ((empty p).applyAll ops).WF

Every field reachable from an empty one is well-formed.

theorem

Cairn.Text.Field.view_wf

provedlean/Cairn/Text/Proofs.lean:291
view_wf {f : Field} (h : f.WF) (focused : Bool) :
  (f.view focused).caret ≤ (f.view focused).text.length ∧
    (f.view focused).anchor ≤ (f.view focused).text.length ∧
      ∀ (a b : Nat),
        (f.view focused).marked = some (a, b) → a ≤ b ∧ b ≤ (f.view focused).text.length

What the view layer is given is in bounds too.

theorem

Cairn.Text.Field.singleLine_apply

provedlean/Cairn/Text/Proofs.lean:300
singleLine_apply (op : TextOp) {f : Field} (h : f.WF) :
  SingleLine (apply op f).fst.text
theorem

Cairn.Text.Field.view_no_newline

provedlean/Cairn/Text/Proofs.lean:303
view_no_newline {f : Field} (h : f.WF) (focused : Bool) :
  ¬'\n' ∈ (f.view focused).text.toList
theorem

Cairn.Text.Field.apply_movement_text

provedlean/Cairn/Text/Proofs.lean:317
apply_movement_text (op : TextOp) (hop : op.isMovement = true)
  (f : Field) : (apply op f).fst.text = f.text ∧ (apply op f).snd = []
theorem

Cairn.Text.Field.apply_unmark_text

provedlean/Cairn/Text/Proofs.lean:323
apply_unmark_text (f : Field) : (apply TextOp.unmark f).fst.text = f.text

Unmark and copy don't edit either.

theorem

Cairn.Text.Field.apply_copy

provedlean/Cairn/Text/Proofs.lean:327
apply_copy (f : Field) :
  apply TextOp.copy f =
    (f, if f.lo < f.hi then [Effect.setClipboard (String.ofList f.selected)] else [])
theorem

Cairn.Text.Field.selected_spec

provedlean/Cairn/Text/Proofs.lean:332
selected_spec {f : Field} (h : f.WF) :
  List.take f.lo f.text ++ f.selected ++ List.drop f.hi f.text = f.text ∧
    f.selected.length = f.hi - f.lo

The copied string is exactly text[lo, hi).

theorem

Cairn.Text.Field.insert_replaces_selection

provedlean/Cairn/Text/Proofs.lean:347
insert_replaces_selection (f : Field) (s : String) (hm : f.marked = none) :
  (apply (TextOp.insert s) f).fst.text =
      List.take f.lo f.text ++ clean s ++ List.drop f.hi f.text ∧
    (apply (TextOp.insert s) f).fst.caret = f.lo + (clean s).length ∧
      (apply (TextOp.insert s) f).fst.anchor = f.lo + (clean s).length

Inserting over a selection (with no composition) gives before ++ s ++ after, with line breaks removed from s, and the caret after s.

theorem

Cairn.Text.Field.insert_replaces_selection'

provedlean/Cairn/Text/Proofs.lean:354
insert_replaces_selection' (f : Field) (s : String) (hm : f.marked = none)
  (hs : SingleLine s.toList) :
  (apply (TextOp.insert s) f).fst.text =
    List.take f.lo f.text ++ s.toList ++ List.drop f.hi f.text

The same, for a string with no line breaks: exactly before ++ s ++ after.

theorem

Cairn.Text.Field.insert_replace

provedlean/Cairn/Text/Proofs.lean:360
insert_replace (f : Field) (s : String) {a b : Nat} (hab : a ≤ b)
  (hb : b ≤ f.text.length) :
  (f.insert s (some (a, b))).text = List.take a f.text ++ clean s ++ List.drop b f.text ∧
    (f.insert s (some (a, b))).caret = a + (clean s).length

With a replacement range from the input system, insert replaces exactly that range.

theorem

Cairn.Text.Field.deleteBackward_collapsed

provedlean/Cairn/Text/Proofs.lean:370
deleteBackward_collapsed (g : Field) (A B : List Char) (x : Char)
  (ht : g.text = A ++ x :: B) (hc : g.caret = A.length + 1) (ha : g.anchor = g.caret) :
  (apply TextOp.deleteBackward g).fst.text = A ++ B ∧
    (apply TextOp.deleteBackward g).fst.caret = A.length ∧
      (apply TextOp.deleteBackward g).fst.anchor = A.length
theorem

Cairn.Text.Field.iterate_deleteBackward

provedlean/Cairn/Text/Proofs.lean:380
iterate_deleteBackward (B u A : List Char) (g : Field) :
  g.text = A ++ u ++ B →
    g.caret = A.length + u.length →
      g.anchor = g.caret →
        (iterate TextOp.deleteBackward u.length g).text = A ++ B ∧
          (iterate TextOp.deleteBackward u.length g).caret = A.length ∧
            (iterate TextOp.deleteBackward u.length g).anchor = A.length
theorem

Cairn.Text.Field.insert_deleteBackward

provedlean/Cairn/Text/Proofs.lean:395
insert_deleteBackward {f : Field} (h : f.WF) (s : String)
  (hc : f.anchor = f.caret) (hm : f.marked = none) :
  have g := iterate TextOp.deleteBackward (clean s).length (apply (TextOp.insert s) f).fst;
  g.text = f.text ∧ g.caret = f.caret ∧ g.anchor = f.anchor

Typing a non-empty string at a collapsed caret, then deleting backward once per scalar, restores the text and the caret.

theorem

Cairn.Text.Field.insert_deleteBackward'

provedlean/Cairn/Text/Proofs.lean:412
insert_deleteBackward' {f : Field} (h : f.WF) (s : String)
  (hc : f.anchor = f.caret) (hm : f.marked = none) :
  have g := iterate TextOp.deleteBackward s.length (apply (TextOp.insert s) f).fst;
  g.text = f.text ∧ g.caret = f.caret ∧ g.anchor = f.anchor

The same in terms of the string typed: s.length deletions (each line break in s became one space, so the count is unchanged). For s without line breaks, the text in between is exactly before ++ s ++ after (insert_replaces_selection').

theorem

Cairn.Text.Field.edit_undoStack_of_ne

provedlean/Cairn/Text/Proofs.lean:426
edit_undoStack_of_ne (f : Field) {t : List Char} (c a : Nat) (ty : Bool)
  (ht : t ≠ f.text) : (f.edit t c a true ty).undoStack = f.snapshot :: f.undoStack
theorem

Cairn.Text.Field.apply_pushes

provedlean/Cairn/Text/Proofs.lean:432
apply_pushes (op : TextOp) (f : Field) (hop : op.isHistory = false)
  (htyping : f.typing = false) (hm : f.marked = none)
  (hch : (apply op f).fst.text ≠ f.text) :
  (apply op f).fst.undoStack = f.snapshot :: f.undoStack

An edit that changes the text and starts a new undo step pushes exactly the state before it.

theorem

Cairn.Text.Field.undo_apply

provedlean/Cairn/Text/Proofs.lean:463
undo_apply (op : TextOp) (f : Field) (hop : op.isHistory = false)
  (htyping : f.typing = false) (hm : f.marked = none)
  (hch : (apply op f).fst.text ≠ f.text) :
  have g := (apply op f).fst.undo;
  g.fst.text = f.text ∧
    g.fst.caret = f.caret ∧
      g.fst.anchor = f.anchor ∧
        g.fst.marked = none ∧ g.fst.undoStack = f.undoStack ∧ g.snd = []

Undo restores. After an op that changes the text, from a field that is not mid-typing (typing = false) and not composing (marked = none), undo restores the text and the selection exactly, ends any composition, and can be redone.

theorem

Cairn.Text.Field.undo_of_stack

provedlean/Cairn/Text/Proofs.lean:473
undo_of_stack (k : Field) {s : Snapshot} {rest : List Snapshot}
  (h : k.undoStack = s :: rest) :
  k.undo.fst.text = s.text ∧ k.undo.fst.caret = s.caret ∧ k.undo.fst.anchor = s.anchor

Undo restores whatever is on top of the undo stack.

theorem

Cairn.Text.Field.typing_step

provedlean/Cairn/Text/Proofs.lean:486
typing_step (op : TextOp) (g : Field) (hop : op.isTyping = true)
  (hm : g.marked = none) (hc : g.anchor = g.caret) (hch : (apply op g).fst.text ≠ g.text) :
  (apply op g).fst.typing = true ∧
    (apply op g).fst.marked = none ∧
      (apply op g).fst.anchor = (apply op g).fst.caret ∧
        (apply op g).fst.undoStack =
          if g.typing = true then g.undoStack else g.snapshot :: g.undoStack

One typing op at a collapsed caret that changes the text: it leaves the caret collapsed, no composition, the typing step open, and pushes the state before it only if no typing step was open.

theorem

Cairn.Text.Field.typing_run

provedlean/Cairn/Text/Proofs.lean:511
typing_run (ops : List TextOp) (g : Field) (s : Snapshot)
  (rest : List Snapshot) (hops : ∀ (o : TextOp), o ∈ ops → o.isTyping = true)
  (hch : g.ChangesEach ops) (ht : g.typing = true) (hm : g.marked = none)
  (hc : g.anchor = g.caret) (hu : g.undoStack = s :: rest) :
  (g.applyAll ops).undoStack = s :: rest
theorem

Cairn.Text.Field.undo_typing_run

provedlean/Cairn/Text/Proofs.lean:525
undo_typing_run (f : Field) (op : TextOp) (ops : List TextOp)
  (hop : op.isTyping = true) (hops : ∀ (o : TextOp), o ∈ ops → o.isTyping = true)
  (htyping : f.typing = false) (hm : f.marked = none) (hc : f.anchor = f.caret)
  (hch : f.ChangesEach (op :: ops)) :
  have g := (f.applyAll (op :: ops)).undo.fst;
  g.text = f.text ∧ g.caret = f.caret ∧ g.anchor = f.anchor

Coalesced typing. A run of typing (inserts, and single-scalar deletes) at a collapsed caret, each step changing the text, is one undo step: undo after the whole run restores the text and selection from before its first keystroke.

theorem

Cairn.Text.Field.undo_composition

provedlean/Cairn/Text/Proofs.lean:538
undo_composition (f : Field) (hm : f.marked = none) (s : String)
  (i n : Nat) (more : List (String × Nat × Nat)) (hs : 0 < s.length)
  (hmore : ∀ (x : String × Nat × Nat), x ∈ more → 0 < x.fst.length) :
  have ops :=
    TextOp.setMarked s i n ::
        List.map (fun x => TextOp.setMarked x.fst x.snd.fst x.snd.snd) more ++
      [TextOp.unmark];
  have g := (f.applyAll ops).undo.fst;
  g.text = f.text ∧ g.caret = f.caret ∧ g.anchor = f.anchor

Composition is one undo step. From a field with no composition, a composition (one or more non-empty setMarked) and its commit (unmark) undo back to the field before it.

theorem

Cairn.Text.Field.redo_undo

provedlean/Cairn/Text/Proofs.lean:578
redo_undo (f : Field) (hu : f.undoStack ≠ []) :
  have g := f.undo.fst.redo.fst;
  g.text = f.text ∧ g.caret = f.caret ∧ g.anchor = f.anchor

Redo undoes undo. After an undo, redo restores the text and selection undo replaced.

theorem

Cairn.Text.SecureField.field_apply_effects

provedlean/Cairn/Text/Proofs.lean:597
field_apply_effects (op : TextOp) (hop : op.isRefused = false)
  (f : Field) : (Field.apply op f).snd = []

The ops it doesn't refuse emit nothing on a plain field.

theorem

Cairn.Text.SecureField.apply_refused

provedlean/Cairn/Text/Proofs.lean:601
apply_refused (op : TextOp) (hop : op.isRefused = true)
  (f : SecureField) : apply op f = ({ field := forget f.field }, [Effect.beep])
theorem

Cairn.Text.SecureField.apply_other

provedlean/Cairn/Text/Proofs.lean:605
apply_other (op : TextOp) (hop : op.isRefused = false)
  (f : SecureField) : apply op f = ({ field := forget (Field.apply op f.field).fst }, [])
theorem

Cairn.Text.SecureField.apply_copy

provedlean/Cairn/Text/Proofs.lean:611
apply_copy (f : SecureField) :
  apply TextOp.copy f = ({ field := forget f.field }, [Effect.beep])

Copy is refused: it beeps, and the clipboard and the text are untouched.

theorem

Cairn.Text.SecureField.apply_cut

provedlean/Cairn/Text/Proofs.lean:614
apply_cut (f : SecureField) :
  apply TextOp.cut f = ({ field := forget f.field }, [Effect.beep])

Cut is refused: it beeps and deletes nothing.

theorem

Cairn.Text.SecureField.apply_effects

provedlean/Cairn/Text/Proofs.lean:617
apply_effects (op : TextOp) (f : SecureField) (e : Effect) :
  e ∈ (apply op f).snd → e = Effect.beep

No op on a secure field sets the clipboard: the only effect any op can have is a beep.

theorem

Cairn.Text.SecureField.apply_no_clipboard

provedlean/Cairn/Text/Proofs.lean:622
apply_no_clipboard (op : TextOp) (f : SecureField) (s : String) :
  ¬Effect.setClipboard s ∈ (apply op f).snd
theorem

Cairn.Text.SecureField.history_empty

provedlean/Cairn/Text/Proofs.lean:626
history_empty (op : TextOp) (f : SecureField) :
  (apply op f).fst.field.undoStack = [] ∧ (apply op f).fst.field.redoStack = []

No history: after any op, the undo and redo stacks are empty.

theorem

Cairn.Text.SecureField.applyAll_history

provedlean/Cairn/Text/Proofs.lean:633
applyAll_history (p : String) (ops : List TextOp) :
  ((empty p).applyAll ops).field.undoStack = [] ∧
    ((empty p).applyAll ops).field.redoStack = []

From an empty field, history stays empty through any ops.

theorem

Cairn.Text.SecureField.apply_edit

provedlean/Cairn/Text/Proofs.lean:648
apply_edit (op : TextOp) (hop : op.isRefused = false)
  (f : SecureField) :
  (apply op f).fst.field.text = (Field.apply op f.field).fst.text ∧
    (apply op f).fst.field.caret = (Field.apply op f.field).fst.caret ∧
      (apply op f).fst.field.anchor = (Field.apply op f.field).fst.anchor ∧
        (apply op f).fst.field.marked = (Field.apply op f.field).fst.marked

Editing is a field's: every op a secure field doesn't refuse changes its text, selection and composition exactly as Field.apply does.

theorem

Cairn.Text.SecureField.forget_wf

provedlean/Cairn/Text/Proofs.lean:655
forget_wf {f : Field} (h : f.WF) : (forget f).WF
theorem

Cairn.Text.SecureField.wf_apply

provedlean/Cairn/Text/Proofs.lean:659
wf_apply (op : TextOp) {f : SecureField} (h : f.field.WF) :
  (apply op f).fst.field.WF