Skip to content

Instantly share code, notes, and snippets.

@edwinb

edwinb/rewrite_pc.idr

Created July 9, 2013 14:24
Show Gist options
  • Save edwinb/5957728 to your computer and use it in GitHub Desktop.
Save edwinb/5957728 to your computer and use it in GitHub Desktop.
Download ZIP
rewrite ... ==> in ...
Raw
rewrite_pc.idr
plus_comm : (n : Nat) -> (m : Nat) -> n + m = m + n
-- Base case
(O + m = m + O) <== plus_comm =
rewrite ((m + O = m) <== plusZeroRightNeutral) ==> (m = m) in refl
-- Step case
(S k + m = m + S k) <== plus_comm =
rewrite ((k + m = m + k) <== plus_comm) ==> (S (m + k) = m + S k) in
rewrite ((S (m + k) = m + S k) <== plusSuccRightSucc) in
refl
-- QED
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment