Various results about lists

Executable Specification

[View lists.sig] [View lists.mod]
sig lists.

kind    i, list       type.

type    nl            list.
type    cons          i -> list -> list.

type    list          list -> o.
type    append        list -> list -> list -> o.
type    rev, perm     list -> list -> o.
type    select        list -> i -> list -> o.

module lists.

list nl.
list (cons X L) :- list L.

append nl C C.
append (cons X A) B (cons X C) :- append A B C.

rev nl nl.
rev (cons X A) B :- rev A A', append A' (cons X nl) B.

select (cons X A) X A.
select (cons Y A) X (cons Y B) :- select A X B.

perm nl nl.
perm (cons X A') B :- select B X B', perm A' B'.


[View lists.thm]

Click on a command or tactic to see a detailed view of its use.

%% (append, reverse, perm)

Specification "lists".

% Append is total
Theorem app_total : forall A B,
  {list A} -> {list B} -> exists C, {append A B C}.

% Append is deterministic
Theorem app_det : forall A B C C',
 {append A B C} -> {append A B C'} -> C = C'.

% Append is associative
Theorem app_assoc : forall A B C AB ABC,
 {append A B AB} -> {append AB C ABC} ->
   exists BC, {append B C BC} /\ {append A BC ABC}.

Theorem rev_lemma : forall A A' B X,
 {rev A A'} -> {append A (cons X nl) B} -> {rev B (cons X A')}.

% Reverse is its own inverse
Theorem rev_rev : forall A B,
 {rev A B} -> {rev B A}.

Theorem perm_lemma : forall A B B' X,
 {perm B' A} -> {select B X B'} -> {perm B (cons X A)}.

% Permutations are invertible
Theorem perm_perm : forall A B,
 {perm A B} -> {perm B A}.

%% We can define append at the meta-level and show a connection
Define app : list -> list -> list -> prop by
  app nl C C ;
  app (cons X A) B (cons X C) := app A B C.

Theorem meta_implies_obj : forall A B C,
  app A B C -> {append A B C}.

Theorem obj_implies_meta : forall A B C,
  {append A B C} -> app A B C.