counter_example.lean

-- リアルワールド例：カウンターボタンの実装と証明

-- カウンターの状態
structure Counter where
  value : Nat

-- カウンターの初期状態
def Counter.init : Counter := ⟨0⟩

-- インクリメント操作
def Counter.increment (c : Counter) : Counter :=
  ⟨c.value + 1⟩

-- デクリメント操作（0以下にはならない）
def Counter.decrement (c : Counter) : Counter :=
  match c.value with
  | 0 => c  -- 0の時は変更しない
  | n + 1 => ⟨n⟩

-- リセット操作
def Counter.reset : Counter := ⟨0⟩

-- 具体的な動作確認
#eval Counter.init  -- { value := 0 }
#eval Counter.init.increment  -- { value := 1 }
#eval Counter.init.increment.increment  -- { value := 2 }
#eval Counter.init.decrement  -- { value := 0 }
#eval (⟨5⟩ : Counter).decrement  -- { value := 4 }

-- ========== 証明 ==========

-- 性質1: インクリメントは必ず値を増やす
theorem increment_increases (c : Counter) :
  (c.increment).value = c.value + 1 := by
  rfl

-- 性質2: デクリメントは値を減らすか維持する
theorem decrement_decreases_or_maintains (c : Counter) :
  (c.decrement).value ≤ c.value := by
  unfold Counter.decrement
  split
  · -- c.value = 0 の場合
    -- c.value ≤ c.value を示す
    simp
  · -- c.value = n + 1 の場合
    -- デクリメントの結果は n で、元の値は n + 1
    next n =>
    -- { value := n }.value ≤ c.value
    -- c.value = n + 1 なので、n ≤ n + 1 を示せばよい
    simp
    omega

-- 性質3: デクリメントは0未満にならない
theorem decrement_non_negative (c : Counter) :
  (c.decrement).value ≥ 0 := by
  -- Natは常に0以上なので自明
  omega

-- 性質4: 0の時のデクリメントは何も変えない
theorem decrement_at_zero :
  Counter.init.decrement = Counter.init := by
  rfl

-- 性質5: インクリメント後のデクリメントは元に戻る
theorem increment_then_decrement (c : Counter) :
  c.increment.decrement = c := by
  simp [Counter.increment, Counter.decrement]

-- 性質6: n回インクリメントした値
def incrementN (c : Counter) : Nat → Counter
  | 0 => c
  | n + 1 => (incrementN c n).increment

theorem incrementN_value (c : Counter) (n : Nat) :
  (incrementN c n).value = c.value + n := by
  induction n with
  | zero => rfl
  | succ n ih =>
    simp [incrementN, Counter.increment]
    rw [ih]
    omega

-- ========== より複雑な操作 ==========

-- カウンターへの操作を表す型
inductive CounterAction
  | increment
  | decrement
  | reset

-- 操作を適用する関数
def applyAction (c : Counter) : CounterAction → Counter
  | CounterAction.increment => c.increment
  | CounterAction.decrement => c.decrement
  | CounterAction.reset => Counter.reset

-- 操作のリストを適用
def applyActions (c : Counter) : List CounterAction → Counter
  | [] => c
  | action :: actions => applyActions (applyAction c action) actions

-- 例：操作の列
def exampleActions : List CounterAction :=
  [.increment, .increment, .increment, .decrement, .increment]

#eval applyActions Counter.init exampleActions  -- { value := 3 }

-- ========== 上限付きカウンター ==========

structure BoundedCounter where
  value : Nat
  max : Nat
  invariant : value ≤ max

-- 上限付きインクリメント
def BoundedCounter.increment (c : BoundedCounter) : BoundedCounter :=
  if h : c.value < c.max then
    ⟨c.value + 1, c.max, by omega⟩
  else
    c  -- 上限に達したら変更しない

-- 性質8: 上限を超えない
theorem bounded_increment_respects_max (c : BoundedCounter) :
  (c.increment).value ≤ c.max := by
  simp [BoundedCounter.increment]
  split
  · -- c.value < c.max の場合
    rename_i h
    -- c.value + 1 ≤ c.max を示す
    exact Nat.succ_le_of_lt h
  · -- c.value ≥ c.max の場合
    exact c.invariant

-- ========== UIイベントのモデル化 ==========

-- クリックイベント
inductive UIEvent
  | click : String → UIEvent
  | keypress : Char → UIEvent

-- アプリケーション状態
structure AppState where
  counter : Counter
  clickCount : Nat

-- イベントハンドラ
def handleEvent (state : AppState) : UIEvent → AppState
  | UIEvent.click "increment" => 
    { state with 
      counter := state.counter.increment,
      clickCount := state.clickCount + 1 }
  | UIEvent.click "decrement" => 
    { state with 
      counter := state.counter.decrement,
      clickCount := state.clickCount + 1 }
  | UIEvent.click "reset" => 
    { state with 
      counter := Counter.reset,
      clickCount := state.clickCount + 1 }
  | _ => state

-- 性質9: クリック数は減らない
theorem click_count_never_decreases (state : AppState) (event : UIEvent) :
  (handleEvent state event).clickCount ≥ state.clickCount := by
  cases event with
  | click id => 
    -- 各ケースを個別に処理
    by_cases h1 : id = "increment"
    · simp [handleEvent, h1]
    · by_cases h2 : id = "decrement"
      · simp [handleEvent, h1, h2]
      · by_cases h3 : id = "reset"
        · simp [handleEvent, h1, h2, h3]
        · simp [handleEvent, h1, h2, h3]
  | keypress _ => 
    simp [handleEvent]

-- ========== 実用的な例：Undo機能 ==========

structure CounterWithHistory where
  current : Counter
  history : List Counter
  maxHistory : Nat := 10

def CounterWithHistory.push (cwh : CounterWithHistory) : CounterWithHistory :=
  let newHistory := cwh.current :: cwh.history.take cwh.maxHistory
  { cwh with history := newHistory }

def CounterWithHistory.increment (cwh : CounterWithHistory) : CounterWithHistory :=
  { cwh.push with current := cwh.current.increment }

def CounterWithHistory.undo (cwh : CounterWithHistory) : CounterWithHistory :=
  match cwh.history with
  | [] => cwh
  | prev :: rest => { cwh with current := prev, history := rest }

-- 性質10: 空の履歴でのundo後は変わらない
theorem undo_empty_history (cwh : CounterWithHistory) :
  cwh.history = [] → cwh.undo = cwh := by
  intro h
  simp [CounterWithHistory.undo, h]

-- エラーの説明コメント
/-
修正した主なエラー：

1. Line 44: `rfl` は等式の証明用。不等式には `omega` を使う
2. Line 46: `omega` が解けない場合は、より詳細な証明が必要
3. Line 127: `c.increment` の型が変わるので、フィールドアクセスも調整
4. Line 161: パターンマッチが不完全。`by_cases` で全ケースをカバー
5. Line 187: 構造体の等価性は各フィールドが等しいことを示す必要がある
-/