add

formal source

 121notation work on `LogicNat` directly. -/
 122
 123/-- Addition by recursion on the second argument. -/
 124def add : LogicNat → LogicNat → LogicNat
 125  | n, .identity => n
 126  | n, .step m   => .step (add n m)
 127
 128instance : Add LogicNat := ⟨add⟩
 129instance : Zero LogicNat := ⟨zero⟩
 130instance : One LogicNat := ⟨succ zero⟩
 131
 132@[simp] theorem add_def (n m : LogicNat) : n + m = add n m := rfl
 133@[simp] theorem zero_def : (0 : LogicNat) = zero := rfl
 134@[simp] theorem one_def : (1 : LogicNat) = succ zero := rfl
 135
 136@[simp] theorem add_zero (n : LogicNat) : n + zero = n := rfl
 137
 138@[simp] theorem add_succ (n m : LogicNat) : n + succ m = succ (n + m) := rfl
 139
 140theorem zero_add (n : LogicNat) : zero + n = n := by
 141  induction n with
 142  | identity => rfl
 143  | step n ih =>
 144    show zero + succ n = succ n
 145    rw [add_succ, ih]
 146
 147theorem succ_add (n m : LogicNat) : succ n + m = succ (n + m) := by
 148  induction m with
 149  | identity => rfl
 150  | step m ih =>
 151    show succ n + succ m = succ (n + succ m)
 152    rw [add_succ, add_succ, ih]
 153
 154theorem add_assoc (a b c : LogicNat) : (a + b) + c = a + (b + c) := by