Paco tutorial&examples in SSReflect

paco_ex_ssr.v

(** printing \2/ $\cup$ #∪# *)
(** printing <2= $\subseteq$ #&sube;# *)
(** printing forall $\forall$ #&forall;# *)
(** printing -> $\rightarrow$ #&rarr;# *)
(** printing /\ $\land$ #&and;# *)

From Coq Require Export ssreflect.
From Paco Require Import paco.
Global Set Bullet Behavior "None".

Set Implicit Arguments.
Set Contextual Implicit.

(** * A Mixed Induction-Coinduction Example

    Written by Steve Zdancewic.
*)

CoInductive stream (A:Type) :=
| snil : stream A
| scons : A -> stream A -> stream A
.

Arguments scons {_} _ _.

Definition id_match_stream {A} (s:stream A) : stream A :=
  match s with
  | snil => snil
  | scons x t => scons x t
  end.

Lemma id_stream_eq : forall A (s:stream A), s = id_match_stream s.
Proof.
by move=>?; case.
Qed.

(* A more relaxed notion of equivalence where the 0's can be inserted finitely often in either
   stream. *)
Inductive seq_step (seq : stream nat -> stream nat -> Prop) : stream nat -> stream nat -> Prop :=
| seq_nil  : seq_step seq snil snil
| seq_cons : forall s1 s2 n (R : seq s1 s2), seq_step seq (scons n s1) (scons n s2)
| seq_cons_z_l : forall s1 s2, seq_step seq s1 s2 -> seq_step seq (scons 0 s1) s2
| seq_cons_z_r : forall s1 s2, seq_step seq s1 s2 -> seq_step seq s1 (scons 0 s2)
.
#[export] Hint Constructors seq_step : core.

Lemma seq_step_mono : monotone2 seq_step.
Proof.
rewrite /monotone2 => x0 x1 r r' IN LE.
elim: IN=>// s1 s2.
- by move=>n H; apply/seq_cons/LE.
- by move=>H1 H2; apply/seq_cons_z_l.
- by move=>H1 H2; apply/seq_cons_z_r.
Qed.
#[export] Hint Resolve seq_step_mono : paco.

Definition seq (s t : stream nat) := paco2 seq_step bot2 s t .
#[export] Hint Unfold seq : core.

Lemma seq_step_refl : forall (R:stream nat -> stream nat -> Prop),
    (forall d, R d d) -> forall d, seq_step R d d.
Proof.
move=>? H; case=>// ??.
by apply/seq_cons/H.
Qed.

Lemma seq_refl : forall s, seq s s.
Proof.
pcofix CIH=>s; pfold.
case: s=>// ??; apply: seq_cons.
by right; apply: CIH.
Qed.

Lemma seq_symm : forall s1 s2, seq s1 s2 -> seq s2 s1.
Proof.
pcofix CIH => s1 s2 H; pfold.
punfold H.
elim: H=>// s3 s4.
- move=>n R. apply: seq_cons. right. apply: CIH. by pclearbot.
- move=>H1 H2. by apply: seq_cons_z_r.
- move=>H1 H2. by apply: seq_cons_z_l.
Qed.

Inductive zeros_star (P: stream nat -> Prop) : stream nat -> Prop :=
| zs_base t (BASE: P t): zeros_star P t
| zs_step t (LZ: zeros_star P t): zeros_star P (scons 0 t)
.
#[export] Hint Constructors zeros_star : core.

Lemma zeros_star_mono : monotone1 zeros_star.
Proof.
move=>/= ??? IN LE.
elim: IN=>t.
- move=>H. by apply/zs_base/LE.
- move=>H1 H2. by apply: zs_step.
Qed.
#[export] Hint Resolve zeros_star_mono : core.

Inductive zeros_one (P: stream nat -> Prop) : stream nat -> Prop :=
| zo_step t (BASE: P t): zeros_one P (scons 0 t)
.
#[export] Hint Constructors zeros_one : core.

Lemma zeros_one_mono : monotone1 zeros_one.
Proof.
(* by move=>/= ??? IN LE; case: IN=>??; apply/zo_step/LE. *)
by pmonauto.
Qed.
#[export] Hint Resolve zeros_one_mono : paco.

Definition infzeros := paco1 zeros_one bot1.
#[export] Hint Unfold infzeros : core.

Inductive nonzero: stream nat -> Prop :=
| nz_nil: nonzero snil
| nz_cons n s (NZ: n <> 0): nonzero (scons n s)
.
#[export] Hint Constructors nonzero : core.

Inductive gseq_cons_or_nil (gseq: stream nat -> stream nat -> Prop) : stream nat -> stream nat -> Prop :=
| gseq_nil : gseq_cons_or_nil gseq snil snil
| gseq_cons s1 s2 n (R: gseq s1 s2) (NZ: n <> 0) : gseq_cons_or_nil gseq (scons n s1) (scons n s2)
.
#[export] Hint Constructors gseq_cons_or_nil : core.

Inductive gseq_step (gseq: stream nat -> stream nat -> Prop) : stream nat -> stream nat -> Prop :=
| gseq_inf s1 s2 (IZ1: infzeros s1) (IZ2: infzeros s2) : gseq_step gseq s1 s2
| gseq_fin s1 s2 t1 t2
     (ZS1: zeros_star (fun t => t = s1) t1)
     (ZS2: zeros_star (fun t => t = s2) t2)
     (R: gseq_cons_or_nil gseq s1 s2)
  : gseq_step gseq t1 t2
.
#[export] Hint Constructors gseq_step : core.

Lemma gseq_step_mono : monotone2 gseq_step.
Proof.
rewrite /monotone2=>???? IN LE.
elim: IN=>??.
- move=>??. by apply: gseq_inf.
- move=>???? H. inversion H=>/=; subst.
  - by apply/gseq_fin/gseq_nil.
  - by apply/gseq_fin/gseq_cons/NZ/LE/R.
Qed.
#[export] Hint Resolve gseq_step_mono : paco.

Definition gseq (s t : stream nat) := paco2 gseq_step bot2 s t .
#[export] Hint Unfold gseq : core.

Lemma nonzero_not_infzeros: forall s
    (ZST: zeros_star nonzero s), ~infzeros s.
Proof.
move=>s; elim=>t.
- move=>NZ INF; punfold INF. move: NZ. inversion_clear INF; subst.
  move=>NZ; by inversion_clear NZ.
- move=>Z IHZ INF. apply: IHZ. punfold INF. inversion_clear INF. by pclearbot.
Qed.

Lemma seq_infzeros_imply: forall s t
  (R: seq s t) (IZ: infzeros s), infzeros t.
Proof.
pcofix CIH=>s t Hs Hi.
punfold Hs. elim: Hs Hi.
- move=>Hi.
  by apply: (@paco1_mon _ _ _ bot1).
- move=>???? Hi.
  pfold. punfold Hi. inversion_clear Hi.
  apply: zo_step. right. pclearbot. by apply/CIH/BASE.
- move=>??? H Hi. apply: H. punfold Hi. inversion_clear Hi. by pclearbot.
- move=>??? H ?. pfold. apply: zo_step. left. by apply: H.
Qed.

Lemma seq_zeros_star_imply: forall s t
  (R: seq s t) (IZ: zeros_star nonzero s), zeros_star nonzero t.
Proof.
move=>s + + IZ. elim: IZ=>{s}t.
- move=>NZ p R. punfold R. elim: R NZ=>{p} //.
  - by apply: zs_base.
  - move=>??? U R. pclearbot. apply/zs_base. inversion_clear R. by apply/nz_cons.
  - move=>??? U R. by inversion_clear R.
  - move=>??? U R. by apply/zs_step/U.
- move=>NZ IH p. move EQ : (scons 0 t) => s R. punfold R.
  elim: R t NZ IH EQ =>//.
  - move=>?????? IH EQ. pclearbot. inversion EQ; subst. by apply/zs_step/IH.
  - move=>?? SS IH ?? U EQ. inversion EQ. rewrite -H0 in IH SS. apply/U. by pfold.
  - move=>?? SS IH t ?? EQ. rewrite -EQ in IH SS. by apply/zs_step/(IH t).
Qed.

Lemma seq_zero_l: forall s t
    (EQ : seq (scons 0 s) t), seq s t.
Proof.
move=>s t EQ. punfold EQ. pfold. move: EQ.
move H : (scons 0 s) => p EQ.
elim: EQ s H=>//.
- move=>??? R ? EQ. inversion EQ. pclearbot. by punfold R.
- move=>???? ? EQ. by inversion EQ.
- move=>??? IH ? EQ. rewrite -EQ in IH. by apply/seq_cons_z_r/IH.
Qed.

Lemma seq_zero_r: forall s t
    (EQ : seq s (scons 0 t)), seq s t.
Proof.
move=> s t EQ.
by apply/seq_symm/seq_zero_l/seq_symm.
Qed.

Lemma zero_gseq_l: forall r s t
    (R : paco2 gseq_step r s t),
  paco2 gseq_step r (scons 0 s) t.
Proof.
move=>??? R. punfold R. pfold. case: R.
- move=>????. apply/gseq_inf=>//. pfold. apply/zo_step. by left.
- move=>?????? H. apply/gseq_fin/H=>//. by apply/zs_step.
Qed.

Lemma zero_gseq_r: forall r s t
    (R : paco2 gseq_step r s t),
  paco2 gseq_step r s (scons 0 t).
Proof.
move=>??? R. punfold R. pfold. case: R.
- move=>????. apply/gseq_inf=>//. pfold. apply/zo_step. by left.
- move=>?????? H. apply/gseq_fin/H=>//. by apply/zs_step.
Qed.

Lemma gseq_implies_seq: forall s t
  (R: gseq s t), seq s t.
Proof.
pcofix CIH=>?? R. punfold R. case: R.
- move=>?? IZ1 IZ2. punfold IZ1. punfold IZ2. inversion IZ1. inversion IZ2.
  pclearbot. pfold. apply/seq_cons. right.
  apply/CIH. pfold. by apply/gseq_inf.
- move=>???? ZS1 ZS2 R. elim: ZS1=>?.
  - elim: ZS2=>?.
    - move=>->->. inversion R; pfold.
      - by apply: seq_nil.
      - apply: seq_cons; right. pclearbot. by apply/CIH.
    - move=>? /[apply] HEQ. by punfold HEQ.
  - move=>? H. by punfold H.
Qed.

Lemma gseq_cons_or_nil_nonzero_l: forall r s t
    (R : gseq_cons_or_nil r s t),
  nonzero s.
Proof.
move=>???; case=>// ???? Hz. by apply/nz_cons.
Qed.

Lemma gseq_cons_or_nil_nonzero_r: forall r s t
    (R : gseq_cons_or_nil r s t),
  nonzero t.
Proof.
move=>???; case=>// ???? Hz. by apply/nz_cons.
Qed.

Lemma zeros_star_nonzero_uniq: forall s1 s2 t
    (ZS1: zeros_star (fun s => s = s1) t)
    (ZS2: zeros_star (fun s => s = s2) t)
    (NZ1: nonzero s1)
    (NZ2: nonzero s2),
  s1 = s2.
Proof.
move=>s1 s2 t ZS1. elim: ZS1 s2=>t1.
- move=>-> {t t1} ? ZS2 NZ1 NZ2.
  elim: ZS2 NZ1 =>// t ZS2 IH NZ1.
  by inversion NZ1.
- move=>Z1 IH s2 ZS2 NZ1 NZ2.
  inversion ZS2; subst.
  - by inversion NZ2.
  - by apply/IH.
Qed.

Lemma gseq_trans : forall d1 d2 d3
  (EQL: gseq d1 d2) (EQR: gseq d2 d3), gseq d1 d3.
Proof.
pcofix CIH=>d1 d2 d3 EQL EQR. punfold EQL. punfold EQR.
case: {-1}_ {-1}_ / EQL (eq_refl d1) (eq_refl d2)=>s1 s2; case: {-1}_ {-1}_ / EQR (eq_refl d2) (eq_refl d3)=>s3 s4.
- move=>ZS3 ZD4 ?? ZS12 ZS2 ??. pfold. by apply/gseq_inf.
- move=>?? ZS1 ? R ??? Z2 ? EQ4; rewrite EQ4 in ZS1.
  exfalso.
  apply/nonzero_not_infzeros/Z2/zeros_star_mono; first by exact: ZS1.
  move=>/= ? ->; case: R.
  - by apply: nz_nil.
  - by move=>???? NZ; apply: nz_cons.
- move=>Z1 ?????? ZS2 R ? EQ4; rewrite -EQ4 in ZS2.
  exfalso.
  apply/nonzero_not_infzeros/Z1/zeros_star_mono; first by exact: ZS2.
  move=>/= ? ->; case: R.
  - by apply: nz_nil.
  - by move=>???? NZ; apply: nz_cons.
- move=>?? ZS1 ZS2 R1 ???? ZS3 ZS4 R2 ? EQ4; rewrite -EQ4 in ZS4.
  move: (gseq_cons_or_nil_nonzero_l R1).
  move: (gseq_cons_or_nil_nonzero_r R2).
  move: (zeros_star_nonzero_uniq ZS1 ZS4) => /[apply]/[apply] EQ.
  rewrite EQ in R1; pfold.
  apply/gseq_fin; [exact: ZS3 | exact: ZS2 |].
  inversion R2; rewrite -H0 in R1; inversion R1; first by apply: gseq_nil.
  pclearbot; apply: gseq_cons=>//.
  by right; apply/CIH/R0.
Qed.

Require Import Classical.

Lemma infzeros_or_finzeros: forall s,
  infzeros s \/ zeros_star nonzero s.
Proof.
move=>s. case: (classic (zeros_star nonzero s)); first by right.
left; move: s b; pcofix CIH; case.
- by move=>H; exfalso; apply/H/zs_base/nz_nil.
- move=>+ s; case.
  - move=>H; pfold.
    apply: zo_step; right.
    by apply: CIH=>H2; apply/H/zs_step.
  - by move=>n H; exfalso; apply/H/zs_base/nz_cons.
Qed.

Lemma seq_infzeros_or_finzeros: forall s t
    (R: seq s t),
  (infzeros s /\ infzeros t) \/
  (zeros_star nonzero s /\ zeros_star nonzero t).
Proof.
move=>s t R.
case: (@infzeros_or_finzeros s)=>Hs; [left|right]; split=>//.
- by apply/seq_infzeros_imply/Hs.
- by apply/seq_zeros_star_imply/Hs.
Qed.

Lemma seq_implies_gseq: forall s t
  (R: seq s t), gseq s t.
Proof.
pcofix CIH=>s t R.
case: (seq_infzeros_or_finzeros R); case=>H1 H2.
- by pfold; apply/gseq_inf.
- elim: H1 R=>{}s NZs R.
  - elim: H2 R=>{}t NZt R.
    - pfold. punfold R. inversion R; subst.
      - by apply/gseq_fin/gseq_nil; apply: zs_base.
      - inversion NZs. apply: (gseq_fin (s1:=scons n s1) (s2:=scons n s2)); try by apply: zs_base.
        apply: gseq_cons=>//. right. pclearbot. by apply/CIH.
      - by inversion NZs.
      - by inversion NZt.
    - move=>H. by apply/zero_gseq_r/R/seq_zero_r.
  - move=>H. by apply/zero_gseq_l/R/seq_zero_l.
Qed.

Lemma seq_trans : forall d1 d2 d3
  (EQL: seq d1 d2) (EQR: seq d2 d3), seq d1 d3.
Proof.
move=>??? H12 H23.
by apply/gseq_implies_seq/gseq_trans/seq_implies_gseq/H23/seq_implies_gseq.
Qed.

paco_tut_ssr.v

(* https://github.com/snu-sf/paco/blob/master/src/tutorial.v *)
 
From Coq Require Export ssreflect.
From Paco Require Import paco.
Global Set Bullet Behavior "None".

(* streams *)

CoInductive stream :=
  | cons : nat -> stream -> stream.

Definition st_unf s := match s with cons n s' => cons n s' end.

Lemma st_unf_eq : forall s, s = st_unf s.
Proof. by case. Qed.

CoFixpoint enumerate n : stream :=
  cons n (enumerate (S n)).

CoFixpoint map f s : stream :=
  match s with cons n s' => cons (f n) (map f s') end.

CoInductive streq0 : stream -> stream -> Prop :=
| streq_fold0 : forall n s1 s2 (R : streq0 s1 s2), streq0 (cons n s1) (cons n s2).

Inductive streq_gen streq : stream -> stream -> Prop :=
| _streq_gen : forall n s1 s2 (R : streq s1 s2 : Prop), streq_gen streq (cons n s1) (cons n s2).

#[export] Hint Constructors streq_gen : core.

CoInductive streq : stream -> stream -> Prop :=
| streq_fold : forall s1 s2, streq_gen streq s1 s2 -> streq s1 s2.

Theorem example : forall n, streq (enumerate n) (cons n (map S (enumerate n))).
Proof.
cofix CIH=>n.
apply: streq_fold.
rewrite [enumerate _]st_unf_eq [map _ _]st_unf_eq /=.
by apply/_streq_gen/CIH.
Qed.

Definition streq' s1 s2 := paco2 streq_gen bot2 s1 s2.

#[export] Hint Unfold streq' : core.
Lemma streq_gen_mon: monotone2 streq_gen.
Proof.
(* move=>?? r r' IN LE. case: IN=>??? r2. by apply/_streq_gen/LE. *)
by pmonauto.
Qed.

#[export] Hint Resolve streq_gen_mon : paco.

Theorem example' : forall n, streq' (enumerate n) (cons n (map S (enumerate n))).
Proof.
pcofix CIH=>n. pfold.
rewrite [enumerate _]st_unf_eq [map _ _]st_unf_eq /=.
by apply/_streq_gen; right; apply/CIH.
Qed.

Theorem streq_cons : forall n1 n2 s1 s2 (SEQ : streq (cons n1 s1) (cons n2 s2)),
  n1 = n2 /\ streq s1 s2.
Proof.
move=>n1 n2 s1 s2 SEQ.
inversion_clear SEQ; move: H=>SEQ.
by inversion_clear SEQ.
Qed.

Theorem streq'_cons : forall n1 n2 s1 s2 (streq : streq' (cons n1 s1) (cons n2 s2)),
  n1 = n2 /\ streq' s1 s2.
Proof.
move=>n1 n2 s1 s2 SEQ.
(*
punfold SEQ.
inversion_clear SEQ.
(* rewrite /streq'. *)
by pclearbot.
*)
by pinversion SEQ.
Qed.

(* trees *)

CoInductive inftree :=
  | node : nat -> inftree -> inftree -> inftree.

Definition tr_unf t : inftree :=
  match t with node n l r => node n l r end.

Lemma tr_unf_eq : forall t, t = tr_unf t.
Proof. by case. Qed.

CoFixpoint one : inftree := node 1 one two
  with two : inftree := node 2 one two.

CoFixpoint eins : inftree := node 1 eins (node 2 eins zwei)
with zwei : inftree := node 2 eins zwei.

Inductive treq_gen treq : inftree -> inftree -> Prop :=
  | _treq_gen : forall n l1 r1 l2 r2 (Rl : treq l1 l2 : Prop)
                   (Rr : treq r1 r2 : Prop), treq_gen treq (node n l1 r1) (node n l2 r2).

#[export] Hint Constructors treq_gen : core.

(*
CoInductive treq : inftree -> inftree -> Prop :=
  | treq_fold : forall t1 t2, treq_gen treq t1 t2 -> treq t1 t2.
  *)

CoInductive treq t1 t2 : Prop :=
  | treq_fold (IN : treq_gen treq t1 t2).

Theorem treq_one : treq one eins.
Proof.
cofix CIH. apply: treq_fold.
rewrite [one]tr_unf_eq [eins]tr_unf_eq /=.
apply: _treq_gen; first by apply: CIH.
apply: treq_fold.
rewrite [two]tr_unf_eq /=.
apply: _treq_gen; first by apply: CIH.
cofix CIH1. apply: treq_fold.
rewrite [two]tr_unf_eq [zwei]tr_unf_eq /=.
by apply: _treq_gen; [apply: CIH|apply: CIH1].
Qed.

Theorem treq_two : treq two zwei.
Proof.
cofix CIH. apply: treq_fold.
rewrite [two]tr_unf_eq [zwei]tr_unf_eq /=.
apply: _treq_gen; last by apply: CIH.
cofix CIH1. apply: treq_fold.
rewrite [one]tr_unf_eq [eins]tr_unf_eq /=.
apply: _treq_gen; first by apply: CIH1.
apply: treq_fold.
rewrite [two]tr_unf_eq /=.
by apply: _treq_gen; [apply: CIH1|apply: CIH].
Qed.

Definition treq' t1 t2 := paco2 treq_gen bot2 t1 t2.
#[export] Hint Unfold treq' : core.

Lemma treq_gen_mon : monotone2 treq_gen.
Proof.
(*
move=>?? r r' IN LE. case: IN=>???????.
by apply: _treq_gen; apply: LE.
*)
by pmonauto.
Qed.

Theorem treq'_one : treq' one eins.
Proof.
pcofix CIH. pfold.
rewrite [one]tr_unf_eq [eins]tr_unf_eq /=.
apply: _treq_gen; first by right; apply: CIH.
left; pfold.
rewrite [two]tr_unf_eq /=.
apply: _treq_gen; first by right; apply: CIH.
left. pcofix CIH1. pfold.
rewrite [two]tr_unf_eq [zwei]tr_unf_eq /=.
by apply: _treq_gen; right; [apply: CIH|apply: CIH1].
Qed.

Theorem treq'_two : treq' two zwei.
Proof.
pcofix CIH. pfold.
rewrite [two]tr_unf_eq [zwei]tr_unf_eq /=.
apply: _treq_gen; last by right; apply: CIH.
left. pcofix CIH1. pfold.
rewrite [one]tr_unf_eq [eins]tr_unf_eq /=.
apply: _treq_gen; first by right; apply: CIH1.
left. pfold.
rewrite [two]tr_unf_eq /=.
by apply: _treq_gen; right; [apply: CIH1|apply: CIH].
Qed.

Theorem treq_two_one_bad : treq two zwei -> treq one eins.
Proof.
rewrite [two]tr_unf_eq [zwei]tr_unf_eq /=; case=>tr2.
by inversion_clear tr2.
Qed.

Theorem treq_two_one : treq two zwei -> treq one eins.
Proof.
move=>tr2; cofix CIH.
apply: treq_fold.
rewrite [one]tr_unf_eq [eins]tr_unf_eq /=.
apply: _treq_gen; first by apply: CIH.
apply: treq_fold.
rewrite [two]tr_unf_eq /=.
by apply: _treq_gen.
Defined.

Theorem treq_one_two : treq one eins -> treq two zwei.
Proof.
move=>tr1; cofix CIH.
apply: treq_fold.
rewrite [two]tr_unf_eq [zwei]tr_unf_eq /=.
by apply: _treq_gen.
Defined.

Theorem treq_eins : treq one eins.
Proof.
cofix CIH.
by apply/treq_two_one/treq_one_two/CIH.
Qed.

Theorem treq_zwei : treq two zwei.
Proof.
cofix CIH.
by apply/treq_one_two/treq_two_one/CIH.
Qed.

Theorem treq_eins_bad : treq one eins.
Proof.
cofix CIH.
apply/treq_two_one_bad/treq_one_two/CIH.
Abort.

Theorem treq'_two_one : forall r, (r two zwei : Prop) -> paco2 treq_gen r one eins.
Proof.
move=>r r2. pcofix CIH. pfold.
rewrite [one]tr_unf_eq [eins]tr_unf_eq /=.
apply: _treq_gen; first by right; apply: CIH.
left; pfold.
rewrite [two]tr_unf_eq /=.
by apply: _treq_gen; right.
Qed.

Theorem treq'_one_two : forall r, (r one eins : Prop) -> paco2 treq_gen r two zwei.
Proof.
move=>r r1; pcofix CIH. pfold.
rewrite [two]tr_unf_eq [zwei]tr_unf_eq /=.
by apply: _treq_gen; right.
Qed.

Theorem treq'_eins : treq' one eins.
Proof.
pcofix CIH. pmult.
by apply/treq'_two_one/treq'_one_two/CIH.
Qed.

Theorem treq'_zwei : treq' two zwei.
Proof.
pcofix CIH. pmult.
by apply/treq'_one_two/treq'_two_one/CIH.
Qed.

(* mutual coinduction *)

CoInductive eqone : inftree -> Prop :=
| eqone_fold tl tr (EQL : eqone tl : Prop) (EQR : eqtwo tr : Prop):
    eqone (node 1 tl tr)
with eqtwo : inftree -> Prop :=
| eqtwo_fold tl tr (EQL : eqone tl : Prop) (EQR : eqtwo tr : Prop):
    eqtwo (node 2 tl tr).

Lemma eqone_eins : eqone eins.
Proof.
cofix CIH0.
rewrite [eins]tr_unf_eq /=.
apply: eqone_fold; first by apply: CIH0.
cofix CIH1.
apply: eqtwo_fold; first by apply: CIH0.
by rewrite [zwei]tr_unf_eq /=.
Qed.

Inductive eq12_gen eq12 : inftree+inftree -> Prop :=
| eq12_l : forall tl tr (EQL: eq12 (inl tl) : Prop) (EQR: eq12 (inr tr) : Prop),
     eq12_gen eq12 (inl (node 1 tl tr))
| eq12_r : forall tl tr (EQL: eq12 (inl tl) : Prop) (EQR: eq12 (inr tr) : Prop),
     eq12_gen eq12 (inr (node 2 tl tr)).
#[export] Hint Constructors eq12_gen : core.

Definition eq1' t := paco1 eq12_gen bot1 (inl t).
Definition eq2' t := paco1 eq12_gen bot1 (inr t).
#[export] Hint Unfold eq1' eq2' : core.

Lemma eq12_gen_mon : monotone1 eq12_gen.
Proof.
(* move=>??? IN LE.
by case: IN=>????; [apply: eq12_l|apply: eq12_r]; apply: LE. *)
by pmonauto.
Qed.

#[export] Hint Resolve eq12_gen_mon : core.

Lemma eq1'_eins : eq1' eins.
Proof.
pcofix CIH0. pfold.
rewrite [eins]tr_unf_eq /=.
apply: eq12_l; first by right; apply: CIH0.
left. pcofix CIH1. pfold.
apply: eq12_r; first by right; apply: CIH0.
right. by rewrite [zwei]tr_unf_eq /=.
Qed.