English
Evaln is monotone in the bound: if k1 ≤ k2 and x ∈ evaln k1 c n, then x ∈ evaln k2 c n.
Русский
Evaln монотонно по границе: если k1 ≤ k2 и x ∈ evaln k1 c n, то x ∈ evaln k2 c n.
LaTeX
$$$\\forall k_1\\,k_2\\,c\\,n\\,x,\\ k_1 \\le k_2 \\rightarrow x \\in evaln k_1 c n \\rightarrow x \\in evaln k_2 c n$$$
Lean4
theorem evaln_mono : ∀ {k₁ k₂ c n x}, k₁ ≤ k₂ → x ∈ evaln k₁ c n → x ∈ evaln k₂ c n
| 0, k₂, c, n, x, _, h => by simp [evaln] at h
| k + 1, k₂ + 1, c, n, x, hl, h => by
have hl' := Nat.le_of_succ_le_succ hl
have :
∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ},
k ≤ k₂ →
(x ∈ o₁ → x ∈ o₂) →
x ∈ do {
guard (n ≤ k);
o₁
} →
x ∈ do {
guard (n ≤ k₂);
o₂
} :=
by
simp only [Option.mem_def, bind, Option.bind_eq_some_iff, Option.guard_eq_some', exists_and_left, exists_const,
and_imp]
introv h h₁ h₂ h₃
exact ⟨le_trans h₂ h, h₁ h₃⟩
simp? at h ⊢ says simp only [Option.mem_def] at h ⊢
induction c generalizing x n <;> rw [evaln] at h ⊢ <;> refine this hl' (fun h => ?_) h
iterate 4 exact h
case pair cf cg hf hg
_ =>
simp? [Seq.seq, Option.bind_eq_some_iff] at h ⊢ says
simp only [Seq.seq, Option.map_eq_map, Option.mem_def, Option.bind_eq_some_iff, Option.map_eq_some_iff,
exists_exists_and_eq_and] at h ⊢
exact h.imp fun a => And.imp (hf _ _) <| Exists.imp fun b => And.imp_left (hg _ _)
case comp cf cg hf hg
_ =>
simp? [Bind.bind, Option.bind_eq_some_iff] at h ⊢ says
simp only [bind, Option.mem_def, Option.bind_eq_some_iff] at h ⊢
exact h.imp fun a => And.imp (hg _ _) (hf _ _)
case prec cf cg hf hg _ =>
revert h
simp only [unpaired, bind, Option.mem_def]
induction n.unpair.2 <;> simp [Option.bind_eq_some_iff]
· apply hf
· exact fun y h₁ h₂ => ⟨y, evaln_mono hl' h₁, hg _ _ h₂⟩
case rfind' cf hf
_ =>
simp? [Bind.bind, Option.bind_eq_some_iff] at h ⊢ says
simp only [unpaired, bind, pair_unpair, Option.pure_def, Option.mem_def, Option.bind_eq_some_iff] at h ⊢
refine h.imp fun x => And.imp (hf _ _) ?_
by_cases x0 : x = 0 <;> simp [x0]
exact evaln_mono hl'
