gistfile1.txt

inductive NatNum : Type | zero | succ (n:NatNum)


def add (a b:NatNum): NatNum := 
  match a with | .zero => b | .succ n => .succ (add n b)


#eval (add (.succ (.succ .zero)) (.succ (.succ .zero)))

#check add.induct

def add_2 (a b:NatNum): NatNum := 
  match b with | .zero => a | .succ n => .succ (add n a)

def is : add n k.succ = .succ (add n k) := by
  induction n
  repeat rw [add.eq_1]
  case _ i h =>
  repeat rw [add.eq_2]
  apply congrArg
  rw [h]


def add_comm : add a b = add b a := by
  refine add.induct (fun i1 i2 => add i1 i2 = add i2 i1) ?_ ?_ a b
  {
    intro i
    rewrite [add.eq_1]
    induction i
    rewrite [add.eq_1]
    rfl
    case _ i =>
    rw [add.eq_2]
    apply congrArg
    exact i
  }
  {
    intro n k h
    rw [add.eq_2]
    rw [h]
    rw [is]
  }