def reverse_append

qasim-bend-kit@0.1.0.2 · proof/JSON_ListProof.bend:41

import Base

41def reverse_append(-A: Data,
42                   +xs: List<&2, A>,
43                   +ys: List<&2, A>) -> {List.reverse(&2, A, List.append(&2, A, xs, ys)) == List.append(&2, A, List.reverse(&2, A, ys), List.reverse(&2, A, xs)) : List<&2, A>}:
44    match xs:
45        case Nil{}:
46            Equal.sym(List<&2, A>, List.append(&2, A, List.reverse(&2, A, ys), Nil{}),
47                List.reverse(&2, A, ys),
48                append_nil(A, List.reverse(&2, A, ys)))
49        case h <> t:
50            Equal.trans(List<&2, A>,
51                List.reverse(&2, A, List.append(&2, A, h <> t, ys)),
52                List.append(&2, A, List.reverse(&2, A, List.append(&2, A, t, ys)), h <> Nil{}),
53                List.append(&2, A, List.reverse(&2, A, ys), List.reverse(&2, A, h <> t)),
54                reverse_go_append(A, List.append(&2, A, t, ys), Nil{}, h <> Nil{}),
55                Equal.trans(List<&2, A>,
56                    List.append(&2, A, List.reverse(&2, A, List.append(&2, A, t, ys)), h <> Nil{}),
57                    List.append(&2, A, List.append(&2, A, List.reverse(&2, A, ys), List.reverse(&2, A, t)), h <> Nil{}),
58                    List.append(&2, A, List.reverse(&2, A, ys), List.reverse(&2, A, h <> t)),
59                    Equal.cong(List<&2, A>, List<&2, A>, xs => List.append(&2, A, xs, h <> Nil{}),
60                        List.reverse(&2, A, List.append(&2, A, t, ys)),
61                        List.append(&2, A, List.reverse(&2, A, ys), List.reverse(&2, A, t)),
62                        reverse_append(A, t, ys)),
63                    Equal.trans(List<&2, A>,
64                        List.append(&2, A, List.append(&2, A, List.reverse(&2, A, ys), List.reverse(&2, A, t)), h <> Nil{}),
65                        List.append(&2, A, List.reverse(&2, A, ys), List.append(&2, A, List.reverse(&2, A, t), h <> Nil{})),
66                        List.append(&2, A, List.reverse(&2, A, ys), List.reverse(&2, A, h <> t)),
67                        append_assoc(A, List.reverse(&2, A, ys), List.reverse(&2, A, t), h <> Nil{}),
68                        Equal.cong(List<&2, A>, List<&2, A>, xs => List.append(&2, A, List.reverse(&2, A, ys), xs),
69                            List.append(&2, A, List.reverse(&2, A, t), h <> Nil{}),
70                            List.reverse(&2, A, h <> t),
71                            Equal.sym(List<&2, A>,
72                                List.reverse(&2, A, h <> t),
73                                List.append(&2, A, List.reverse(&2, A, t), h <> Nil{}),
74                                reverse_go_append(A, t, Nil{}, h <> Nil{}))))))