hermit-1.0.1: examples/new_reverse/Reverse.hec

flatten-module
rule-to-lemma "++ []"

-- module main:Main where
--   absR :: forall a . ([a] -> H a) -> [a] -> [a]
--   repR :: forall a . ([a] -> [a]) -> [a] -> H a
--   rev :: forall a . [a] -> [a]
--   main :: IO ()
--   main :: IO ()

prove-lemma "++ []"

-- Goal:
-- forall * xs. (++) * xs ([] *) = xs

lhs (one-td (unfold-rule appendFix))

-- Goal:
-- forall *. (++) * = myAppend *

assume -- proven appendFix

-- Goal:
-- forall * xs. myAppend * xs ([] *) = xs

induction 'xs

-- Goal:
-- forall *. myAppend * (undefined *) ([] *) = undefined *

any-bu (unfold 'myAppend >>> undefined-expr)
any-bu (unfold 'myAppend >>> case-reduce)
simplify-lemma
foralls-body ; consequent
one-td (lemma-forward ind-hyp-0)
end-case

rule-to-lemma "myAppend-assoc"
prove-lemma "myAppend-assoc"
induction 'xs
{ foralls-body
    { conj-lhs
      any-bu ((unfold 'myAppend) >>> undefined-case)
      reflexivity
    }
    conj-rhs
    { conj-lhs
      any-bu ((unfold 'myAppend) >>> case-reduce)
      reflexivity
    }
    { conj-rhs
      foralls-body ; consequent
      any-bu (unfold 'myAppend)
      smash
      rhs (one-td (fold 'myAppend))
      one-td (lemma-forward ind-hyp-0)
      reflexivity
    }
}
end-proof

rule-to-lemma "repH []"

-- module main:Main where
--   absR :: forall a . ([a] -> H a) -> [a] -> [a]
--   repR :: forall a . ([a] -> [a]) -> [a] -> H a
--   rev :: forall a . [a] -> [a]
--   main :: IO ()
--   main :: IO ()

prove-lemma "repH []"

-- Goal:
-- forall *. repH * ([] *) = id *

lhs unfold

-- Goal:
-- forall *. (++) * ([] *) = id *

extensionality

-- Goal:
-- forall * x. (++) * ([] *) x = id * x

lhs (one-td (unfold-rule appendFix))

-- Goal:
-- forall * x. myAppend * ([] *) x = id * x

lhs unfold

-- Goal:
-- forall * x.
-- case [] * of wild *
--   [] -> x
--   (:) x xs -> (:) * x (myAppend * xs x)
-- =
-- id * x

both smash

-- Goal:
-- forall * x. x = x

end-proof -- proven "repH []"
rule-to-lemma "repH (:)"

-- module main:Main where
--   absR :: forall a . ([a] -> H a) -> [a] -> [a]
--   repR :: forall a . ([a] -> [a]) -> [a] -> H a
--   rev :: forall a . [a] -> [a]
--   main :: IO ()
--   main :: IO ()

prove-lemma "repH (:)"

-- Goal:
-- forall * x xs. repH * ((:) * x xs) = (.) * * * ((:) * x) (repH * xs)

both (any-call (unfold 'repH))

-- Goal:
-- forall * x xs. (++) * ((:) * x xs) = (.) * * * ((:) * x) ((++) * xs)

both (any-call (unfold-rule appendFix))

-- Goal:
-- forall * x xs. myAppend * ((:) * x xs) = (.) * * * ((:) * x) (myAppend * xs)

rhs unfold

-- Goal:
-- forall * x xs. myAppend * ((:) * x xs) = \ x -> (:) * x (myAppend * xs x)

lhs (unfold >>> smash)

-- Goal:
-- forall * x xs. \ ys -> (:) * x (myAppend * xs ys) = \ x -> (:) * x (myAppend * xs x)

end-proof -- proven "repH (:)"
rule-to-lemma "repH ++"

-- module main:Main where
--   absR :: forall a . ([a] -> H a) -> [a] -> [a]
--   repR :: forall a . ([a] -> [a]) -> [a] -> H a
--   rev :: forall a . [a] -> [a]
--   main :: IO ()
--   main :: IO ()

prove-lemma "repH ++"

-- Goal:
-- forall * xs ys. repH * ((++) * xs ys) = (.) * * * (repH * xs) (repH * ys)

both (any-call (unfold 'repH))

-- Goal:
-- forall * xs ys. (++) * ((++) * xs ys) = (.) * * * ((++) * xs) ((++) * ys)

both (any-call (unfold-rule appendFix))

-- Goal:
-- forall * xs ys. myAppend * (myAppend * xs ys) = (.) * * * (myAppend * xs) (myAppend * ys)

lhs (eta-expand 'x)

-- Goal:
-- forall * xs ys. \ x -> myAppend * (myAppend * xs ys) x = (.) * * * (myAppend * xs) (myAppend * ys)

rhs unfold

-- Goal:
-- forall * xs ys. \ x -> myAppend * (myAppend * xs ys) x = \ x -> myAppend * xs (myAppend * ys x)

extensionality 'zs
simplify
{ forall-body
  lemma "myAppend-assoc"
}
end-proof

-- module main:Main where
--   absR :: forall a . ([a] -> H a) -> [a] -> [a]
--   repR :: forall a . ([a] -> [a]) -> [a] -> H a
--   rev :: forall a . [a] -> [a]
--   main :: IO ()
--   main :: IO ()

binding-of 'rev

-- rev = \ * ds ->
--   case ds of wild *
--     [] -> [] *
--     (:) x xs -> (++) * (rev * xs) ((:) * x ([] *))

fix-intro

-- rev = \ * ->
--   fix *
--       (\ rev ds ->
--          case ds of wild *
--            [] -> [] *
--            (:) x xs -> (++) * (rev xs) ((:) * x ([] *)))

application-of 'fix

-- fix *
--     (\ rev ds ->
--        case ds of wild *
--          [] -> [] *
--          (:) x xs -> (++) * (rev xs) ((:) * x ([] *)))

split-1-beta rev [| absR |] [| repR |]

-- Goal:
-- fix *
--     ((.) * * * (absR *)
--          ((.) * * * (repR *)
--               (\ rev ds ->
--                  case ds of wild *
--                    [] -> [] *
--                    (:) x xs -> (++) * (rev xs) ((:) * x ([] *)))))
-- =
-- fix *
--     (\ rev ds ->
--        case ds of wild *
--          [] -> [] *
--          (:) x xs -> (++) * (rev xs) ((:) * x ([] *)))

both (unfold >>> smash)

-- Goal:
-- let rec x =
--           absR *
--                (repR *
--                      (\ ds ->
--                         case ds of wild *
--                           [] -> [] *
--                           (:) x xs -> (++) * (x xs) ((:) * x ([] *))))
-- in x
-- =
-- let rec x = \ ds ->
--           case ds of wild *
--             [] -> [] *
--             (:) x xs -> (++) * (x xs) ((:) * x ([] *))
-- in x

lhs (replicate 5 ((one-td unfold) >+> smash))

-- Goal:
-- let rec x = \ x ->
--           (++) *
--                (case x of wild *
--                   [] -> [] *
--                   (:) x xs -> (++) * (x xs) ((:) * x ([] *)))
--                ([] *)
-- in x
-- =
-- let rec x = \ ds ->
--           case ds of wild *
--             [] -> [] *
--             (:) x xs -> (++) * (x xs) ((:) * x ([] *))
-- in x

lhs (one-td (lemma-forward "++ []"))

-- Goal:
-- let rec x = \ x ->
--           case x of wild *
--             [] -> [] *
--             (:) x xs -> (++) * (x xs) ((:) * x ([] *))
-- in x
-- =
-- let rec x = \ ds ->
--           case ds of wild *
--             [] -> [] *
--             (:) x xs -> (++) * (x xs) ((:) * x ([] *))
-- in x

end-proof -- proven rev-assumption

-- let g =
--       (.) * * * (repR *)
--           ((.) * * *
--                (\ rev ds ->
--                   case ds of wild *
--                     [] -> [] *
--                     (:) x xs -> (++) * (rev xs) ((:) * x ([] *)))
--                (absR *))
--     worker = fix * g
-- in absR * worker

any-call (unfold ['absR,'repR])

-- let g =
--       (.) * * * (\ eta -> (\ f -> (.) * * * (repH *) f) eta)
--           ((.) * * *
--                (\ rev ds ->
--                   case ds of wild *
--                     [] -> [] *
--                     (:) x xs -> (++) * (rev xs) ((:) * x ([] *)))
--                (\ eta -> (\ g -> (.) * * * (absH *) g) eta))
--     worker = fix * g
-- in (\ g -> (.) * * * (absH *) g) worker

repeat (any-call (unfold '.)) ; smash

-- let worker =
--       fix *
--           (\ x x ->
--              repH *
--                   (case x of wild *
--                      [] -> [] *
--                      (:) x xs -> (++) * (absH * (x xs)) ((:) * x ([] *))))
-- in \ x -> absH * (worker x)

one-td (case-float-arg-lemma repHstrict)

-- Goal:
-- forall *. repH * (undefined *) = undefined *

lhs unfold

-- Goal:
-- forall *. (++) * (undefined *) = undefined *

lhs (one-td (unfold-rule appendFix))

-- Goal:
-- forall *. myAppend * (undefined *) = undefined *

lhs unfold

-- Goal:
-- forall *.
-- \ ys ->
--   case undefined * of wild *
--     [] -> ys
--     (:) x xs -> (:) * x (myAppend * xs ys)
-- =
-- undefined *

both (innermost undefined-expr)

-- Goal:
-- forall *. undefined * = undefined *

end-proof -- proven repHstrict

-- let worker =
--       fix *
--           (\ x x ->
--              case x of wild *
--                [] -> repH * ([] *)
--                (:) x xs -> repH * ((++) * (absH * (x xs)) ((:) * x ([] *))))
-- in \ x -> absH * (worker x)

one-td (lemma-forward "repH ++")

-- let worker =
--       fix *
--           (\ x x ->
--              case x of wild *
--                [] -> repH * ([] *)
--                (:) x xs -> (.) * * * (repH * (absH * (x xs))) (repH * ((:) * x ([] *))))
-- in \ x -> absH * (worker x)

repeat (any-call (unfold '.))

-- let worker =
--       fix *
--           (\ x x ->
--              case x of wild *
--                [] -> repH * ([] *)
--                (:) x xs -> \ x -> repH * (absH * (x xs)) (repH * ((:) * x ([] *)) x))
-- in \ x -> absH * (worker x)

one-td (unfold-rule repH-absH-fusion)

-- Goal:
-- forall * h. repH * (absH * h) = h

assume -- proven repH-absH-fusion

-- let worker =
--       fix *
--           (\ x x ->
--              case x of wild *
--                [] -> repH * ([] *)
--                (:) x xs -> \ x -> x xs (repH * ((:) * x ([] *)) x))
-- in \ x -> absH * (worker x)

one-td (lemma-forward "repH (:)")

-- let worker =
--       fix *
--           (\ x x ->
--              case x of wild *
--                [] -> repH * ([] *)
--                (:) x xs -> \ x -> x xs ((.) * * * ((:) * x) (repH * ([] *)) x))
-- in \ x -> absH * (worker x)

any-td (lemma-forward "repH []")

-- let worker =
--       fix *
--           (\ x x ->
--              case x of wild *
--                [] -> id *
--                (:) x xs -> \ x -> x xs ((.) * * * ((:) * x) (id *) x))
-- in \ x -> absH * (worker x)

any-call (unfold 'fix)

-- let worker =
--       let rec x =
--                 (\ x x ->
--                    case x of wild *
--                      [] -> id *
--                      (:) x xs -> \ x -> x xs ((.) * * * ((:) * x) (id *) x)) x
--       in x
-- in \ x -> absH * (worker x)

any-call (unfold 'absH)

-- let worker =
--       let rec x =
--                 (\ x x ->
--                    case x of wild *
--                      [] -> id *
--                      (:) x xs -> \ x -> x xs ((.) * * * ((:) * x) (id *) x)) x
--       in x
-- in \ x -> worker x ([] *)

bash

-- let rec x = \ x ->
--           case x of wild *
--             [] -> \ x -> x
--             (:) x xs -> \ x -> x xs ((:) * x x)
-- in \ x -> x x ([] *)

unshadow

-- let rec x = \ x0 ->
--           case x0 of wild *
--             [] -> \ x1 -> x1
--             (:) x1 xs -> \ x2 -> x xs ((:) * x1 x2)
-- in \ x0 -> x x0 ([] *)