# 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'.

```

# Reasoning

[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}.
induction on 1. intros. case H1.
search.
apply IH to H3 H2. search.
% Append is deterministic
Theorem app_det : forall A B C C',
{append A B C} -> {append A B C'} -> C = C'.
induction on 1. intros. case H1.
case H2. search.
case H2. apply IH to H3 H4. search.
% 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}.
induction on 1. intros. case H1.
search.
case H2. apply IH to H3 H4. search.
Theorem rev_lemma : forall A A' B X,
{rev A A'} -> {append A (cons X nl) B} -> {rev B (cons X A')}.
induction on 1. intros. case H1.
case H2. search.
case H2. apply IH to H3 H5. search.
% Reverse is its own inverse
Theorem rev_rev : forall A B,
{rev A B} -> {rev B A}.
induction on 1. intros. case H1.
search.
apply IH to H2. apply rev_lemma to H4 H3. search.
Theorem perm_lemma : forall A B B' X,
{perm B' A} -> {select B X B'} -> {perm B (cons X A)}.
induction on 2. intros. case H2.
search.
case H1. apply IH to H5 H3. search.
% Permutations are invertible
Theorem perm_perm : forall A B,
{perm A B} -> {perm B A}.
induction on 1. intros. case H1.
search.
apply IH to H3. apply perm_lemma to H4 H2. search.
%% 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}.
induction on 1. intros. case H1.
search.
apply IH to H2. search.
Theorem obj_implies_meta : forall A B C,
{append A B C} -> app A B C.
induction on 1. intros. case H1.
search.
apply IH to H2. search.
```