Results on (potentially) infinite lists

Reasoning

[View colist.thm]

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

Kind     nat          type.
Type     z            nat.
Type     s            nat -> nat.

CoDefine colist : olist -> prop by
  colist nil ;
  colist (X :: L) := colist L.

CoDefine eqi : olist -> olist -> prop by
  eqi nil nil ;
  eqi (X :: L) (X :: R) := eqi L R.

Define tk : nat -> olist -> olist -> prop by
  tk z L nil ;
  tk N nil nil ;
  tk (s N) (X :: L) (X :: R) := tk N L R.

Define eqf : olist -> olist -> prop by
  eqf L R := (forall N S, tk N L S -> tk N R S) /\
             (forall N S, tk N R S -> tk N L S).


%% First we show eqi implies eqf

Theorem eqi_take : forall L R S N,
  eqi L R -> tk N L S -> tk N R S.

Theorem eqi_sym : forall L R,
  eqi L R -> eqi R L.

Theorem eqi_eqf : forall L R,
  eqi L R -> eqf L R.


%% Second we show eqf implies eqi

Theorem eqf_nil : forall L,
  eqf nil L -> L = nil.

Theorem eqf_cons : forall X L R,
  eqf (X :: L) R -> exists S, R = X :: S.

Theorem eqf_sym : forall L R,
  eqf L R -> eqf R L.

Theorem eqf_downward : forall X L R,
  eqf (X :: L) (X :: R) -> eqf L R.

Theorem eqf_eqi : forall L R,
  colist L -> eqf L R -> eqi L R.


% We define co-inductive append and show it is associative

CoDefine coapp : olist -> olist -> olist -> prop by
  coapp (X :: A) B (X :: C) := coapp A B C ;
  coapp nil (X :: B) (X :: C) := coapp nil B C ;
  coapp nil nil nil.

Theorem coapp_assoc : forall A B C AB ABC BC,
  coapp A B AB -> coapp AB C ABC -> coapp B C BC -> coapp A BC ABC.