agda example

infixr 2 _⟨_⟩_
_⟨_⟩_ : forall {a : Set} -> (x : a) -> {y z : a} -> x == y -> y == z -> x == z
x ⟨ p ⟩ q = trans p q

infixr 3 _∎
_∎ : {a : Set} -> (x : a) -> x == x
x ∎ = Refl

-- Visible reduction steps make the proof more explicit
definition : {a : Set} -> {x : a} -> x == x
definition = Refl

infixr 2 _`trans`_
_`trans`_ : forall {a : Set} -> {x y z : a} -> x == y -> y == z -> x == z
p `trans` q = trans p q

plusZero : (n : Nat) -> (n + 0) == n
plusZero Zero = Refl
plusZero (Succ n) = cong Succ (plusZero n)

plusSucc : (n m : Nat) -> Succ (n + m) == (n + Succ m)
plusSucc Zero _ = Refl
plusSucc (Succ n) m = cong Succ (plusSucc n m)

plusCommutes : (n m : Nat) -> (n + m) == (m + n)
plusCommutes Zero Zero = Refl
plusCommutes Zero (Succ m) = cong Succ (plusCommutes Zero m)
plusCommutes (Succ n) Zero = cong Succ (plusCommutes n Zero)
plusCommutes (Succ n) (Succ m) =
   Succ n + Succ m
     ⟨ definition ⟩
   Succ (n + Succ m)
     ⟨ cong Succ (
             n + Succ m    ⟨ sym (plusSucc n m) ⟩
             Succ (n + m)  ⟨ plusCommutes (Succ n) m ⟩
             m + Succ n    ∎ )
     ⟩
   Succ (m + Succ n)
     ⟨ definition ⟩
   Succ m + Succ n
   ∎