% Lists
% By Carsten Varming 2006

elem: type.

a : elem.
b : elem.
c : elem -> elem.

list : type. %name list Ls.

nil : list.
cons : elem -> list -> list.

eq : list -> list -> type.
eq/ref : eq Ls Ls.

eq-symm : eq Ls Ls' -> eq Ls' Ls -> type.
%mode eq-symm +Q -Q'.
- : eq-symm eq/ref eq/ref.
%worlds () (eq-symm _ _).
%total {} (eq-symm _ _).

eq-trans : eq Ls Ls' -> eq Ls' Ls'' -> eq Ls Ls'' -> type.
%mode eq-trans +Q +Q' -Q''.
- : eq-trans eq/ref eq/ref eq/ref.
%worlds () (eq-trans _ _ _).
%total {} (eq-trans _ _ _).

eq-cong-cons : {E} eq L1 L2 -> eq (cons E L1) (cons E L2) -> type.
%mode eq-cong-cons +E1 +E2 -E3.
- : eq-cong-cons _ eq/ref eq/ref.
%worlds () (eq-cong-cons _ _ _).
%total {} (eq-cong-cons _ _ _).

% ------------------------------------------------------------------------------
%  Reverse                                                                      
% ------------------------------------------------------------------------------

rev : list -> list -> list -> type.
rev/nil : rev nil Ls' Ls'.
rev/cons : rev (cons E Ls) Ls'' Ls'
               <- rev Ls (cons E Ls'') Ls'.

can-rev : {Ls} {Ls'} rev Ls Ls' Ls'' -> type.
%mode can-rev +Ls +Ls' -R.
- : can-rev nil _ rev/nil.
- : can-rev (cons E Ls) Ls' (rev/cons Ls'')
            <- can-rev Ls (cons E Ls') Ls''.
%worlds () (can-rev _ _ _).
%total D (can-rev D _ _).

%theorem 
can-rev' : forall {Ls : list} {Ls' : list} 
           exists {Ls'' : list} {D : rev Ls Ls' Ls''}
           true.
%prove 2 Ls (can-rev' Ls _ _ _).

rev-eq : eq L1 L2 -> eq L3 L4 -> eq L5 L6 -> rev L1 L3 L5 -> rev L2 L4 L6 -> type.
%mode rev-eq +E1 +E2 +E3 +R1 -R2.
- : rev-eq eq/ref eq/ref eq/ref R R.
%worlds () (rev-eq _ _ _ _ _).
%total {} (rev-eq _ _ _ _ _).

%theorem 
rev-eq' : forall* {L1 : list}{L2 : list}{L3 : list}{L4 : list}{L5 : list}{L6 : list} 
          forall {D1 : eq L1 L2} {D2 : eq L3 L4} {D3 : eq L5 L6} 
                 {D4 : rev L1 L3 L5}
           exists {D5 : rev L2 L4 L6}
           true.
%prove 2 {} (rev-eq' _ _ _ _ _).

rev-determ : rev Ls Ls' Ls3 -> rev Ls Ls' Ls4 -> eq Ls3 Ls4 -> type.
%mode rev-determ +R +R' -Q.
- : rev-determ rev/nil _ eq/ref.
- : rev-determ (rev/cons R) (rev/cons R') Q
         <- rev-determ R R' Q.
%worlds () (rev-determ _ _ _).
%total D (rev-determ D _ _).

%theorem 
rev-determ' : 
  forall* {L1 : list}{L2 : list}{L3 : list}{L4 : list}
  forall {D1 : rev L1 L2 L3} {D2 : rev L1 L2 L4}
  exists {D3 : eq L3 L4}
  true.
%prove 1 D1 (rev-determ' D1 _ _).

revrev-id-lem : rev Ls Ls' Ls'' -> rev Ls'' nil Ls4 -> rev Ls' Ls Ls6 -> eq Ls6 Ls4 -> type.
%mode revrev-id-lem +R +R' +R'' -Q.

- : revrev-id-lem rev/nil F F' Q
          <- rev-determ F' F Q.
- : revrev-id-lem (rev/cons R) R' R'' Q
          <- revrev-id-lem R R' (rev/cons R'') Q.

%worlds () (revrev-id-lem _ _ _ _).
%total D (revrev-id-lem D _ _ _).

%theorem 
revrev-id-lem' : 
  forall* {L1 : list}{L2 : list}{L3 : list}{L4 : list}{L5 : list}
  forall {D1 : rev L1 L2 L3} {D2 : rev L3 nil L4} {D3 : rev L2 L1 L5}
  exists {D4 : eq L5 L4}
  true.
%prove 2 D1 (revrev-id-lem' D1 _ _ _).

revrev-id : rev A nil B -> rev B nil A -> type.
%mode revrev-id +R -R'.
- : revrev-id R R'
  <- can-rev _ nil R1
  <- revrev-id-lem R R1 rev/nil E
  <- eq-symm E E'
  <- rev-eq eq/ref eq/ref E' R1 R'.
%worlds () (revrev-id _ _).
%total {} (revrev-id _ _).

%theorem 
revrev-id' : 
  forall* {L1 : list}{L2 : list}
  forall {D1 : rev L1 nil L2}
  exists {D2 : rev L2 nil L1}
  true.
%prove 1 D1 (revrev-id' D1 _).
a
%.
rev-injective : rev Ls nil Ls' -> rev Ls'' nil Ls' -> eq Ls Ls'' -> type.
%mode rev-injective +R +R' -Q.
- : rev-injective (R : rev Ls nil Ls') R' Q
      <- revrev-id R R1
      <- revrev-id R' R1'
      <- rev-determ R1 R1' Q.
%worlds () (rev-injective _ _ _).
%total D (rev-injective D _ _).

append : list -> list -> list -> type.  %name append A.

append/nil : append nil L L.
append/cons : append (cons E L1) L2 (cons E L3)
     <- append L1 L2 L3.

can-append : {L1}{L2} append L1 L2 L3 -> type.
%mode can-append +L1 +L2 -A.

- : can-append nil L append/nil.
- : can-append (cons E L1) L2 (append/cons A)
     <- can-append L1 L2 A.

%worlds () (can-append _ _ _).
%total D (can-append D _ _).

append-eq : eq L1 L2 -> eq L3 L4 -> eq L5 L6 -> append L1 L3 L5 -> append L2 L4 L6 -> type.
%mode append-eq +E1 +E2 +E3 +A1 -A2.

- : append-eq eq/ref eq/ref eq/ref A A.

%worlds () (append-eq _ _ _ _ _).
%total {} (append-eq _ _ _ _ _).

append-eq-nil : {L1} append L1 nil L1 -> type.
%mode append-eq-nil +L -A.

- : append-eq-nil nil append/nil.
- : append-eq-nil (cons E L) (append/cons A) 
     <- append-eq-nil L A.

%worlds () (append-eq-nil _ _).
%total D (append-eq-nil D _).

append-eq-nil : append L1 nil L2 -> eq L1 L2 -> type.
%mode append-eq-nil +A -E.

- : append-eq-nil append/nil eq/ref.
- : append-eq-nil (append/cons A) E
     <- append-eq-nil A E1
     <- eq-cong-cons _ E1 E.
%worlds () (append-eq-nil _ _).
%total D (append-eq-nil D _).

append-determ : append L1 L2 L3 -> append L1 L2 L4 -> eq L3 L4 -> type.
%mode append-determ +A1 +A2 -E.

- : append-determ append/nil append/nil eq/ref.
- : append-determ (append/cons A1) (append/cons A2) E
       <- append-determ A1 A2 E2
       <- eq-cong-cons _ E2 E.

%worlds () (append-determ _ _ _).
%total D (append-determ D _ _).

append-assoc1 : append L1 L2 L3 -> append L3 L4 L5 -> append L2 L4 L6 -> append L1 L6 L5 -> type.
%mode append-assoc1 +A1 +A2 -A3 -A4.

- : append-assoc1 append/nil A1 A1 append/nil.
- : append-assoc1 (append/cons A1) (append/cons A2) A3 (append/cons A4)
      <- append-assoc1 A1 A2 A3 A4.

%worlds () (append-assoc1 _ _ _ _).
%total D (append-assoc1 D _ _ _).

append-assoc2 : append L1 L2 L3 -> append L3 L4 L5 -> append L2 L4 L6 -> append L1 L6 L7 -> eq L5 L7 -> type.
%mode append-assoc2 +A1 +A2 +A3 +A4 -E.

- : append-assoc2 A1 A2 A3 A4 E
      <- append-assoc1 A1 A2 A3' A4'
      <- append-determ A3 A3' E3
      <- append-eq eq/ref E3 eq/ref A4 A4''
      <- append-determ A4' A4'' E.

%worlds () (append-assoc2 _ _ _ _ _).
%total {} (append-assoc2 _ _ _ _ _).

append-rev1 : append L1 L2 L3 -> rev L1 L4 L5 -> rev L2 L5 L6 -> rev L3 L4 L6 -> type.
%mode append-rev1 +A +R1 +R2 -R3.

- : append-rev1 append/nil rev/nil R R.
- : append-rev1 (append/cons A) (rev/cons R1) R3 (rev/cons R2) 
 <- append-rev1 A R1 R3 R2.

%worlds () (append-rev1 _ _ _ _).
%total D (append-rev1 D _ _ _).

append-rev2 : rev L1 L2 L3 -> append L2 L4 L5 -> append L3 L4 L6 -> rev L1 L5 L6 -> type.
%mode append-rev2 +R +A +A' -R'.

- : append-rev2 rev/nil A1 A2 R
  <- append-determ A1 A2 E
  <- rev-eq eq/ref eq/ref E rev/nil R.

- : append-rev2 (rev/cons R) A1 A2 (rev/cons R2)
  <- append-rev2 R (append/cons A1) A2 R2.

%worlds () (append-rev2 _ _ _ _).
%total D (append-rev2 D _ _ _).

append-rev : rev L1 L2 L3 -> rev LA LB LC -> append LC L3 LT -> rev L2 L1 L3' -> 
             rev LB LA LC' -> append L3' LC' LT' -> rev LT' nil LT -> type.
%mode append-rev +R1 +R2 +A1 +R3 +R4 +A2 -R3.

- : append-rev R1 (rev/cons R2) A1 R3 R4 A2 R5
    <- append-rev R1 R2 A1 R3 (rev/cons R4) A2 R5.

- : append-rev (rev/cons R1) rev/nil A1 R2 R3 A2 R5
    <- append-rev R1 rev/nil A1 (rev/cons R2) R3 A2 R5.

- : append-rev rev/nil rev/nil A1 R3 R4 A2 R5
  <- append-rev2 R3 append/nil A2 RC
  <- append-rev1 A1 R4 RC RB 
  <- revrev-id RB R5.

%worlds () (append-rev _ _ _ _ _ _ _).
%total [D E] (append-rev E D _ _ _ _ _).