Indexed lists

(options removed from twelftag: check=true)

% Lists
% By Carsten Varming 2006
%sort tp %.
%name tp %.
%sort list {_ tp} %.
%name list %.
%term stuff tp %.
%freeze tp %.
%term cons {Tp} %pi (list Tp) %-> (list Tp) %.
%term nil {Tp} list Tp %.
%freeze list %.
%sort eq {_ list Tp} {_ list Tp} %.
%mode eq %in %out %.
%term eq_ref eq Ls Ls %.
%worlds () (eq _ _) %.
%freeze eq %.
%sort eq_symm {_ eq Ls Ls'} {_ eq Ls' Ls} %.
%mode eq_symm %in %out %.
%term eq_symm_rule eq_symm eq_ref eq_ref %.
%worlds () (eq_symm _ _) %.
%freeze eq_symm %.
%total {} (eq_symm _ _) %.
%sort eq_trans {_ eq Ls Ls'} {_ eq Ls' Ls''} {_ eq Ls Ls''} %.
%mode eq_trans %in %in %out %.
%term eq_trans_rule eq_trans eq_ref eq_ref eq_ref %.
%worlds () (eq_trans _ _ _) %.
%freeze eq_trans %.
%total {} (eq_trans _ _ _) %.
%sort rev {_ list Tp} {_ list Tp} {_ list Tp} %.
%mode rev %in %in %out %.
%term rev_nil rev (nil _) Ls' Ls' %.
%term rev_cons %pi (rev (cons E Ls) Ls'' Ls') %<- (rev Ls (cons E Ls'') Ls') %.
%worlds () (rev _ _ _) %.
%freeze rev %.
%total D (rev D _ _) %.
%sort rev_exists {Ls} {Ls'} {_ rev Ls Ls' Ls''} %.
%mode rev_exists %in %in %out %.
%term rev_exists_nil rev_exists (nil _) _ rev_nil %.
%term rev_exists_cons
  %pi (rev_exists (cons E Ls) Ls' (rev_cons Ls''))
  %<- (rev_exists Ls (cons E Ls') Ls'') %.
%worlds () (rev_exists _ _ _) %.
%freeze rev_exists %.
%total D (rev_exists D _ _) %.
%sort revDet {_ rev Ls Ls' Ls3} {_ rev Ls Ls' Ls4} {_ eq Ls3 Ls4} %.
%mode revDet %in %in %out %.
%term revDet_nil revDet rev_nil _ eq_ref %.
%term revDet_cons %pi (revDet (rev_cons R) (rev_cons R') Q) %<- (revDet R R' Q) %.
%worlds () (revDet _ _ _) %.
%freeze revDet %.
%total D (revDet D _ _) %.
%sort revrev_id_lem {_ rev Ls Ls' Ls''} {_ rev Ls'' (nil _) Ls4} {_ rev Ls' Ls Ls6} {_ eq Ls6 Ls4} %.
%mode revrev_id_lem %in %in %in %out %.
%term revrev_id_lem_nil %pi (revrev_id_lem rev_nil F F' Q) %<- (revDet F' F Q) %.
%term revrev_id_lem_cons
  %pi (revrev_id_lem (rev_cons R) R' R'' Q)
  %<- (revrev_id_lem R R' (rev_cons R'') Q) %.
%worlds () (revrev_id_lem _ _ _ _) %.
%freeze revrev_id_lem %.
%total D (revrev_id_lem D _ _ _) %.
%sort revrev_id {_ rev Ls (nil Tp) Ls'} {_ rev Ls' (nil Tp) Ls''} {_ eq Ls Ls''} %.
%mode revrev_id %in %in %out %.
%term revrev_id_rule %pi (revrev_id R R' Q) %<- (revrev_id_lem R R' rev_nil Q) %.
%worlds () (revrev_id _ _ _) %.
%freeze revrev_id %.
%total {} (revrev_id _ _ _) %.
%sort rev_injective {_ rev Ls (nil Tp) Ls'} {_ rev Ls'' (nil Tp) Ls'} {_ eq Ls Ls''} %.
%mode rev_injective %in %in %out %.
%term rev_injective_rule
  %pi (rev_injective (%the (rev Ls (nil Tp) Ls') R) R' Q)
  %<- (rev_exists Ls' (nil Tp) Rev)
  %<- (revrev_id R Rev Q')
  %<- (eq_symm Q' Q''')
  %<- (revrev_id R' Rev Q'')
  %<- (eq_trans Q'' Q''' Q1)
  %<- (eq_symm Q1 Q) %.
%worlds () (rev_injective _ _ _) %.
%freeze rev_injective %.
%total D (rev_injective D _ _) %.