Click on a command or tactic to see a detailed view of its use.
%% Results on (potentially) infinite lists CoDefine colist nil. CoDefine colist (X :: L) := colist L. CoDefine eqi nil nil. CoDefine eqi (X :: L) (X :: R) := eqi L R. Define tk z L nil. Define tk N nil nil. Define tk (s N) (X :: L) (X :: R) := tk N L R. Define 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. [Show Proof][Hide Proof] induction on 2. intros. case H2. search. case H1. search. case H1. apply IH to H4 H3. search. Theorem eqi_sym : forall L R, eqi L R -> eqi R L. [Show Proof][Hide Proof] coinduction. intros. case H1. search. apply CH to H2. search. Theorem eqi_eqf : forall L R, eqi L R -> eqf L R. [Show Proof][Hide Proof] intros. unfold. intros. apply eqi_take to H1 H2. search. intros. apply eqi_sym to H1. apply eqi_take to H3 H2. search. %% Second we show eqf implies eqi Theorem eqf_nil : forall L, eqf nil L -> L = nil. [Show Proof][Hide Proof] intros. case H1. apply H2 to _ with N = s z. case H4. search. Theorem eqf_cons : forall X L R, eqf (X :: L) R -> exists S, R = X :: S. [Show Proof][Hide Proof] intros. case H1. apply H2 to _ with N = s z. case H4. search. Theorem eqf_sym : forall L R, eqf L R -> eqf R L. [Show Proof][Hide Proof] intros. case H1. search. Theorem eqf_downward : forall X L R, eqf (X :: L) (X :: R) -> eqf L R. [Show Proof][Hide Proof] intros. case H1. unfold. intros. assert tk (s N) (X :: L) (X :: S). apply H2 to H5. case H6. search. intros. assert tk (s N) (X :: R) (X :: S). apply H3 to H5. case H6. search. Theorem eqf_eqi : forall L R, colist L -> eqf L R -> eqi L R. [Show Proof][Hide Proof] coinduction. intros. case H1. apply eqf_nil to H2. search. apply eqf_cons to H2. apply eqf_downward to H2. apply CH to H3 H4. search. % We define co-inductive append and show it is associative CoDefine coapp (X :: A) B (X :: C) := coapp A B C. CoDefine coapp nil (X :: B) (X :: C) := coapp nil B C. CoDefine 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. [Show Proof][Hide Proof] coinduction. intros. case H1. case H2. apply CH to H4 H5 H3. search. case H2. case H3. apply CH to H4 H5 H6. search. case H2. case H3. apply CH to _ H4 H5. search. case H3. search.