Instantly share code, notes, and snippets.

# puffnfresh/ReverseLike.idr Last active Aug 29, 2015

 -- Originally an Idris translation of copumpkin's Agda code: -- https://gist.github.com/copumpkin/8758586 -- Extended using Matthew Brecknell's proof which only needs two properties: -- https://gist.github.com/mbrcknl/bfaa72c2ec6ff32a2826 -- Proves that List reverse is completely specified by: -- 1. f [x] = [x] -- 2. f (xs ++ ys) = f ys ++ f xs %default total reverse' : List a -> List a reverse' [] = [] reverse' (x :: xs) = reverse' xs ++ [x] record ReverseLike : (List a -> List a) -> Type where RL : {reverse : List a -> List a} -> (reverse1 : (x : a) -> reverse [x] = [x]) -> (reverseFlip : (xs, ys : List a) -> reverse (xs ++ ys) = reverse ys ++ reverse xs) -> ReverseLike reverse consElim : (x : a) -> (xs, ys : List a) -> x :: xs = x :: ys -> xs = ys consElim x [] [] prf = Refl consElim x [] (y :: xs) Refl impossible consElim x (x :: xs) [] Refl impossible consElim x (x :: xs) (x :: xs) Refl = Refl appEqNil : (xs, ys : List a) -> xs ++ ys = xs -> ys = [] appEqNil [] ys prf = prf appEqNil (x :: xs) [] prf = Refl appEqNil (x :: xs) (y :: ys) prf = appEqNil xs (y :: ys) (consElim x (xs ++ y :: ys) xs prf) reverse'Proof : (f : List a -> List a) -> ReverseLike f -> (xs : List a) -> f xs = reverse' xs reverse'Proof f (RL reverse1 reverseFlip) [] = ?reverse'ProofNilCase reverse'Proof f (RL reverse1 reverseFlip) (x :: xs) = let inductiveHypothesis = reverse'Proof f (RL reverse1 reverseFlip) xs in ?reverse'ProofStepCase ---------- Proofs ---------- reverse'ProofNilCase = proof intros rewrite appEqNil (f []) (f []) (sym (reverseFlip [] [])) trivial reverse'ProofStepCase = proof intros rewrite sym (reverseFlip [x] xs) rewrite sym (reverse1 x) rewrite inductiveHypothesis trivial
to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.
{"ft_lang_label":"__label__en","ft_lang_prob":0.76795745,"math_prob":0.9124878,"size":1807,"snap":"2019-13-2019-22","text_gpt3_token_len":604,"char_repetition_ratio":0.19079313,"word_repetition_ratio":0.07453416,"special_character_ratio":0.38904262,"punctuation_ratio":0.20065789,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":0.9763816,"pos_list":[0,1,2],"im_url_duplicate_count":[null,null,null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2019-03-26T04:25:19Z\",\"WARC-Record-ID\":\"<urn:uuid:6ba65f60-c24a-47f2-a2a5-09b97d09dce1>\",\"Content-Length\":\"56832\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:2716e0b5-7bb8-4292-aa7c-203271a2b7c6>\",\"WARC-Concurrent-To\":\"<urn:uuid:9ffa2df4-53c1-4c60-93d5-afb41b61c090>\",\"WARC-IP-Address\":\"192.30.253.118\",\"WARC-Target-URI\":\"https://gist.github.com/puffnfresh/99c139d4d0c4bdd155ac\",\"WARC-Payload-Digest\":\"sha1:MCCNS5XH52VWCO2TEL5GPVQEXRPNCGPK\",\"WARC-Block-Digest\":\"sha1:BJ6SK7GA3BMJPYEZPTYL55DM7GAKQUPN\",\"WARC-Identified-Payload-Type\":\"text/html\",\"warc_filename\":\"/cc_download/warc_2019/CC-MAIN-2019-13/CC-MAIN-2019-13_segments_1552912204790.78_warc_CC-MAIN-20190326034712-20190326060712-00014.warc.gz\"}"}