Skip to content

Instantly share code, notes, and snippets.

@robstewart57

robstewart57/example.idr

Created September 17, 2018 13:46
Show Gist options
  • Save robstewart57/fab94a8c69320f99017bd67ddccf65c5 to your computer and use it in GitHub Desktop.
Save robstewart57/fab94a8c69320f99017bd67ddccf65c5 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
example.idr
ones : List Nat -> List Nat
ones = map (const 1)
f : (input:List Nat) -> (sum (ones input) = length input)
f input = case input of
[] => Refl
(x::xs) => ?hole
@clayrat
Copy link

clayrat commented Sep 17, 2018 •
edited
Loading

Ok, so List is recursive, and you usually prove stuff about such types also in a recursive manner. You've done the corner case of [], now you prove by induction (basically a dependent version of recursion) - assume f xs and use it to prove f (x :: xs) somehow. Try writing let fx = f xs in ?hole.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment