2024年5月21日

昨晩はMicrosoftのイベント.Copilot+PCの発表.Recallとかいうのがやばそう.時が戻せるらしい.

個人的には新たなSurfaceが気になる.予定通りSnapdragon X搭載のSurface ProとSurface Laptopが出るみたい.3月に発表されたよりも一世代後という位置づけになった.Intel搭載がなかったのはびっくりした.かなり自信があるということか.Microsoft以外のメーカーからもSnapdragon搭載PCの発表もあったみたい.

新しいSurface Proのキーボードは無線式になるらしい.キーボード外して使う展開があまり思い当たらないけど.予告通りのCopilotボタンも搭載.CPUは有機ELならばSnapdragon X Elite,そうでなければPlusと出てくるけど,予約ページを見るとPlusしかないように見える.でも製品の仕様にはどっちも書いてあるんだよなぁ.

と思ったらショップもEliteに変わっていた.間違いだったのかな?

2024年5月14日

前回書いた自明な等式の証明だけど,もっと強力なringというタクティクがあるらしい.ドキュメントはLean3のものしか見つからないのだが,import Mathlib.Tactic.RingすればLean4/Mathlib4でも使える.

import Mathlib.Tactic.Ring
lemma a (n m : Nat) : n + m + 1 = 1 + m + n := by ring
lemma b (n m : Nat) : 1 + n + 2 * m = m + n + 1 + m := by ring

すげーとか喜んでしまったが,別に示されるのは自明な式なんだよなぁ…….

2024年5月12日

Lean,結合律と可換性をきちんと意識して計算しないとならないのがうざくて,例えば$n + m + 1 = 1 + m + n$というどう考えても自明の式も(例えば)きちんと結合律一回可換法則二回を適用しないとならない.

lemma a (n m : Nat) : n + m + 1 = 1 + m + n := by
  rw[add_assoc 1 m n]
  rw[add_comm]
  rw[add_comm n m]

と思っていたのだが,ac_rflというタクティクがあることを知った.可換な結合的演算があった時にそれだけを使って示せる等式の証明をいっぱつでやってくれるらしい.少なくとも上の式はac_rfl一発で終わる.ただし他の法則は使えないので,例えば$1 + n + 2 * m = m + n + 1 + m$は駄目.rw[two_mul]で一度$2*m = m + m$と書き換えてからやればよい.

2024年5月7日

昨日の関数合成はなんか違ったかも…….でもよくわかってない.

import Mathlib.Tactic
open Nat

@[simp]
def fun_pow {α : Type u} (f : α → α) : (n : Nat) → (α → α)
  | 0 => id
  | succ n => (fun_pow f n) ∘ f

instance {α : Type u} : HPow (α → α) (Nat) (α → α) where
  hPow := fun_pow

def f : (Fin 2) → (Fin 2)
  | 0 => 1
  | 1 => 0

theorem a {α : Type u} (g : α → α) : g^(0) = id := by rfl
theorem aa : f^(0) = id := by
  rfl

最後のrflが通らない.simpすると1 = idとかに簡略化されてしまっているらしい.何だろう.うーむ.最初のimportがないと動くような.

2024年5月6日

Leanで遊んでいる.しかし簡単な命題の証明も大変だ…….書いているのに無駄が多い気もするけど.Lean勉強会の教材で遊んで,大体終わったのでなんか色々試しているところ.たまにあれこれどうするんだっけというやつをメモ.

  • h : Odd nを使いたいときは,rw[Odd] at hとするとOddの定義が展開される.これは∃k n = 2 * k + 1と定義されているので.apply Exists.elimの後intro k hkとすれば整数kとhk : n = 2 * k + 1が得られる.
  • 通常の自然数nに関する帰納法は
    induction n with
    | zero => ...
    | succ n => ...
    
    でできるが,n未満のすべてを仮定してnを示すという形の帰納法はNat.strongInductionOnという形で使える.とりあえず次のようにしたら動いた.
    apply Nat.strongInductionOn n
    intro n ih
    
    ihにはn未満での示したい命題(ゴール)の成立が入っている.この場合だと最初のステップは不要なのでnでの証明を試みればいいけど,0だけ議論が変わったりするならmatch n withで場合分けすればよい.ところでmatchcasesの違いがよくわかっていない.
  • 仮定がh ; A ∨ Bの時に場合分けするならば
    cases h with
    | inl h => ...
    | inr h => ...
    
    (基本ですね.)
  • 自明な式だがLeanが処理してくれない,ということはよくある.何か命題を持ってくる必要があるのだがapply?とすると対応するものを探してくれる……けど複雑な状況ではうまくいかない.必要な形でシンプルにしてtheorem tmp ***:*** := by apply?とかするとほしいものを出してくれる.
  • A ∧ Bを示す時は(And.Introでもよいが)constructorをするとAの証明とBの証明に集中する.
  • 次がだめなのはどうすればいいんだろう?(fの定義のRをℤ[X]にすれば通る.)R内の積が認識されていないらしい.
    open Polynomial
    
    def R := ℤ[X]
    noncomputable def f (n : Nat) : R := X^(n)
    
    theorem thm (n m : Nat) : (f n) * (f m) = f (n + m) := by
      simp[f]
      apply (pow_add X n m).symm
    
  • 関数のn回合成をf^nとかけるようにと思って次のようにしてみた.
    open Nat
    def fun_pow {α : Type u} (f : α → α) (n : Nat) : (α → α):=
    match n with
    | 0 => id
    | succ n => (fun_pow f n)∘ f
    
    instance {α : Type u} : Pow (α → α) (Nat) := ⟨fun_pow⟩
    
    def f : ℕ → ℕ
    | 0 => 0
    | succ n => n
    
    theorem a : fun_pow f 2 = f ∘ f := by simp
    theorem aa : f^(2) = f ∘ f := by simp
    
    aとaaは何が違うのだろう?(aは通るがaaは駄目,というかf^(n)の方を使うと何も示せない…….)

2024年5月4日

Typstの行取り改訂版.段間の取り方がわからない…….

#let gyodori(
  lines: 2,
  before_space: 0,
  after_space: 0,
  x
) = {
  context{
    // 和文文字の縦方向長さ
    let letter_height = measure(box[阿]).height
    // 段落間の長さ(block(spacing:**)のやつ)を計測
    let block_spacing = measure(block[#par[阿];#par[阿]]).height - 2 * letter_height
    // baselineskip
    let baselineskip = letter_height + par.leading
    let be_sp = {
      if type(before_space) == int { before_space * baselineskip }
      else { before_space }
    }
    let aft_sp = {
      if type(after_space) == int { after_space * baselineskip }
      else { after_space }
    }
    // 本文のテキスト長さの計算
    let textlen = {
      let totaltextlen = {
        page.width - {
          if page.margin == auto {
            (5/21) * {
              if page.width < page.height { page.width}
              else { page.height }
            }
          } else if(type(page.margin)) == dictionary {
            let margin_keys = page.margin.keys()
            let left_margin = {
              if(margin_keys.contains("left")) {
                page.margin.left
              } else if(margin_keys.contains("inside")){
                page.margin.inside
              } else { 0pt }
            }
            let right_margin = {
              if(margin_keys.contains("right")){
                page.margin.right
              } else if(margin_keys.contains("outside")){
                page.margin.outside
              } else { 0pt }
            }
            right_margin + left_margin
          } else { 2 * page.margin }
        }
      }
      // 段間の取得方法がわからない.2*は根拠なしというか多分間違っている
      (totaltextlen -  (page.columns - 1) * 2 * columns.gutter)/page.columns
    }
    // とりあえずブロックに入れる
    let b = block(width: textlen, x)
    // 長さ計算
    let total_len = baselineskip * (lines - 1) + letter_height
    let ue = (total_len - measure(b).height)/2 + be_sp
    let shita = (total_len - measure(b).height)/2 + aft_sp
    block[
      #v(ue)
      #b
      #v(shita)
    ]
  }
}

2024年5月3日

で,四日休みの方です.といっても特に予定もなく.いつも通りな感じで過ごしそう…….