Various results about lists

Executable Specification

[View lists.mod]

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

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

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

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

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

Reasoning

[View lists.thm] [Show All Proofs] [Hide All Proofs]

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

%% Various results about lists
%% (append, reverse, perm)

% Append is total
Theorem app_total : forall A B,
  {list A} -> {list B} -> exists C, {append A B C}. [Show Proof][Hide Proof]
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'. [Show Proof][Hide Proof]
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 BC ABC,
 {append A B AB} -> {append AB C ABC} -> {append B C BC} -> {append A BC ABC}. [Show Proof][Hide Proof]
induction on 1. intros. case H1.
  apply app_det to H2 H3. search.
  case H2. apply IH to H4 H5 H3. search.

Theorem rev_lemma : forall A A' B X,
 {rev A A'} -> {append A (cons X nil) B} -> {rev B (cons X A')}. [Show Proof][Hide Proof]
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}. [Show Proof][Hide Proof]
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)}. [Show Proof][Hide Proof]
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}. [Show Proof][Hide Proof]
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 append nil C C.
Define append (cons X A) B (cons X C) := append A B C.

Theorem meta_implies_obj : forall A B C,
  append A B C -> {append A B C}. [Show Proof][Hide Proof]
induction on 1. intros. case H1.
  search.
  apply IH to H2. search.

Theorem obj_implies_meta : forall A B C,
  {append A B C} -> append A B C. [Show Proof][Hide Proof]
induction on 1. intros. case H1.
  search.
  apply IH to H2. search.