Reasoning Principles for ITrees

[gilhur]

I write down the generalized principles we want to achieve.

It is possible that one can explicitly define "euttG" but it might be also possible that it can naturally derived from the generalized companion theory.

I will update my progress in this issue.

Context {E : Type -> Type} {R1 R2 : Type} (RR : R1 -> R2 -> Prop).

Variable euttG: forall (r rl rh: itree E R1 -> itree E R2 -> Prop), itree E R1 -> itree E R2 -> Prop.

(**
   Correctness
 **)

Axiom eutt_le_euttG:
  eutt RR <2= euttG bot2 bot2 bot2.

Axiom euttG_le_eutt:
  euttG bot2 bot2 bot2 <2= eutt RR.

(**
   Reasoning Principles
 **)

(* Make new hypotheses *)

Axiom euttG_coind: forall r rl rh (INV: r <2= rl /\ rl <2= rh) x,
  (x <2= euttG r (rl \2/ x) (rh \2/ x)) -> (x <2= euttG r rl rh).

(* Process itrees *)

Axiom euttG_ret: forall r rl rh (INV: r <2= rl /\ rl <2= rh) v1 v2,
  RR v1 v2 -> euttG r rl rh (Ret v1) (Ret v2).

Axiom euttG_bind: forall r rl rh (INV: r <2= rl /\ rl <2= rh) t1 t2,
  eutt_bind_clo (euttG r rl rh) t1 t2 -> euttG r rl rh t1 t2.

Axiom euttG_trans_eq: forall r rl rh (INV: r <2= rl /\ rl <2= rh) t1 t2,
  eq_trans_clo (euttG r rl rh) t1 t2 -> euttG r rl rh t1 t2.

(* Lose weak hypotheses after general rewriting *)

Axiom euttG_trans_eutt: forall r rl rh (INV: r <2= rl /\ rl <2= rh) t1 t2,
  eutt_trans_clo (euttG r r rh) t1 t2 -> euttG r rl rh t1 t2.

(* Make available weak hypotheses *)

Axiom euttG_tau: forall r rl rh (INV: r <2= rl /\ rl <2= rh) t1 t2,
  euttG rl rl rh t1 t2 -> euttG r rl rh (Tau t1) (Tau t2).

(* Make available strong hypotheses *)

Axiom euttG_vis: forall r rl rh (INV: r <2= rl /\ rl <2= rh) u (e: E u) k1 k2,
  (forall v, euttG rh rh rh (k1 v) (k2 v)) -> euttG r rl rh (Vis e k1) (Vis e k2).

(* Use available hypotheses *)

Axiom euttG_base: forall r rl rh (INV: r <2= rl /\ rl <2= rh) t1 t2,
  r t1 t2 -> euttG r rl rh t1 t2.

[gilhur]

I found that the above rules are unsound, and what I presented at the meeting is right.

Variable euttH: forall (r rh: itree E R1 -> itree E R2 -> Prop), itree E R1 -> itree E R2 -> Prop.
Variable euttL: forall (r rl rh: itree E R1 -> itree E R2 -> Prop), itree E R1 -> itree E R2 -> Prop.

(**
   Correctness
 **)

Axiom eutt_le_euttL:
  eutt RR <2= euttL bot2 bot2 bot2.

Axiom euttL_le_euttH:
  euttL bot2 bot2 bot2 <2= euttH bot2 bot2.

Axiom euttH_le_eutt:
  euttH bot2 bot2 <2= eutt RR.

(**
   euttH
 **)

(* Make strong hypotheses *)

Axiom euttH_coind: forall r rh (INV: r <2= rh) x,
  (x <2= euttH r (rh \2/ x)) -> (x <2= euttH r rh).

(* Process itrees *)

Axiom euttH_ret: forall r rh (INV: r <2= rh) v1 v2,
  RR v1 v2 -> euttH r rh (Ret v1) (Ret v2).

Axiom euttH_bind: forall r rh (INV: r <2= rh) t1 t2,
  eutt_bind_clo (euttH r rh) t1 t2 -> euttH r rh t1 t2.

Axiom euttH_trans: forall r rh (INV: r <2= rh) t1 t2,
  eutt_trans_clo (euttH r rh) t1 t2 -> euttH r rh t1 t2.

(* Make hypotheses available *)

Axiom euttH_vis: forall r rh (INV: r <2= rh) u (e: E u) k1 k2,
  (forall v, euttH rh rh (k1 v) (k2 v)) -> euttH r rh (Vis e k1) (Vis e k2).

(* Use available hypotheses *)

Axiom euttH_base: forall r rh (INV: r <2= rh) t1 t2,
  r t1 t2 -> euttH r rh t1 t2.

(* Transition to lower-level *)

Axiom euttH_lower: forall r rh (INV: r <2= rh) t1 t2,
  euttL r r rh t1 t2 -> euttH r rh t1 t2.

(**
   euttL
 **)

(* Make weak hypothesis *)

Axiom euttL_coind: forall r rl rh (INV: r <2= rl /\ rl <2= rh) x,
  (x <2= euttL r (rl \2/ x) (rh \2/ x)) -> (x <2= euttL r rl rh).

(* Process itrees *)

Axiom euttL_ret: forall r rl rh (INV: r <2= rl /\ rl <2= rh) v1 v2,
  RR v1 v2 -> euttL r rl rh (Ret v1) (Ret v2).

Axiom euttL_bind: forall r rl rh (INV: r <2= rl /\ rl <2= rh) t1 t2,
  eutt_bind_clo (euttL r rl rh) t1 t2 -> euttL r rl rh t1 t2.

Axiom euttL_trans: forall r rl rh (INV: r <2= rl /\ rl <2= rh) t1 t2,
  eq_trans_clo (euttL r rl rh) t1 t2 -> euttL r rl rh t1 t2.

(* Make hypotheses available *)

Axiom euttL_tau: forall r rl rh (INV: r <2= rl /\ rl <2= rh) t1 t2,
  euttL rl rl rh t1 t2 -> euttL r rl rh (Tau t1) (Tau t2).

(* Use available hypotheses *)

Axiom euttL_base: forall r rl rh (INV: r <2= rl /\ rl <2= rh) t1 t2,
  r t1 t2 -> euttL r rl rh t1 t2.

(* Transition to higher-level *)

Axiom euttL_higher: forall r rl rh (INV: r <2= rl /\ rl <2= rh) u (e: E u) k1 k2,
  (forall v, euttH rh rh (k1 v) (k2 v)) -> euttL r rl rh (Vis e k1) (Vis e k2).

[gilhur]

I finished proving the following principles, which I think is the most general ones.

Variable euttG: forall (rH rL gL gH: itree E R1 -> itree E R2 -> Prop), itree E R1 -> itree E R2 -> Prop.

(**
   Correctness
 **)

Lemma euttG_le_eutt:
  euttG bot2 bot2 bot2 bot2 <2= eutt RR.

Lemma eutt_le_euttG:
  eutt RR <2= euttG bot2 bot2 bot2 bot2.

(* Make new hypotheses *)

Lemma euttG_cofix: forall rH rL gL gH x,
    (x <2= euttG rH rL (gL \2/ x) (gH \2/ x)) -> (x <2= euttG rH rL gL gH).

(* Process itrees *)

Lemma euttG_ret: forall rH rL gL gH v1 v2,
  RR v1 v2 -> euttG rH rL gL gH (Ret v1) (Ret v2).

Lemma euttG_bind: forall rH rL gL gH t1 t2,
  bindC (euttG rH rL gL gH) t1 t2 -> euttG rH rL gL gH t1 t2.

Lemma euttG_transD: forall rH rL gL gH t1 t2,
  transD (euttG rH rL gL gH) t1 t2 -> euttG rH rL gL gH t1 t2.

(* Drop weak hypotheses for general rewriting *)

Lemma euttG_drop rH rL gL gH t1 t2:
  euttG rH rH rH gH t1 t2 -> euttG rH rL gL gH t1 t2.

Lemma euttG_transU_eutt rH gH t1 t2:
  transU (euttG rH rH rH gH) t1 t2 -> euttG rH rH rH gH t1 t2.

(* Make a weakly guarded progress *)

Lemma euttG_tau: forall rH rL gL gH t1 t2,
  euttG rH gL gL gH t1 t2 -> euttG rH rL gL gH (Tau t1) (Tau t2).

(* Make a strongly guarded progress *)

Lemma euttG_vis: forall rH rL gL gH u (e: E u) k1 k2,
  (forall v, euttG gH gH gH gH (k1 v) (k2 v)) -> euttG rH rL gL gH (Vis e k1) (Vis e k2).

(* Use available hypotheses *)

Lemma euttG_base: forall rH rL gL gH t1 t2,
  rH t1 t2 \/ rL t1 t2 -> euttG rH rL gL gH t1 t2.