Skip to content

Instantly share code, notes, and snippets.

@bvssvni

bvssvni/add_even.idr

Created April 6, 2017 00:04
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save bvssvni/88d0e2a762002151892ae1136f4044c5 to your computer and use it in GitHub Desktop.
Save bvssvni/88d0e2a762002151892ae1136f4044c5 to your computer and use it in GitHub Desktop.
Download ZIP
Managed to prove the path `add[even] <=> eq`
Raw
add_even.idr
prove_add_even : (x : Nat) -> (y : Nat) -> even (add x y) = eq (even x) (even y)
prove_add_even Z Z = Refl
prove_add_even Z (S Z) = Refl
prove_add_even Z (S (S k)) = prove_add_even Z k
prove_add_even (S Z) Z = Refl
prove_add_even (S (S k)) Z = prove_add_even k Z
prove_add_even (S Z) (S Z) = Refl
prove_add_even (S Z) (S (S k)) = prove_add_even (S Z) k
prove_add_even (S (S k)) (S j) = prove_add_even k (S j)
add_even : SymPath2 Nat Bool
add_even = add[even]^2 <=> eq by prove_add_even
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment