HyPre.sstep.ApplyLfMulti

From HyPre Require Export
  ListExtra.

From HyPre Require Export
  Semantics
  ApplyLf
  MultiStep.

Import ListNotations.

Section with_lf.
  Context {X Y Z : Type}.
  Context (lf : X*Z -> list Y) (step : X*Z -> X*Z).

  Definition apply_lf_trace (x : X) (z : Z) : list Y -> Prop
  := fun sl => apply_lf' lf (multi_step' step (x,z) (length sl)) = sl.

  Lemma apply_lf_linear_semantics
    (* TODO this assumpton Hi should somehow be avoided by stating multi_step' differently *)
    (Hi : forall i, {s : Y | lf i = [s]})
    (* TODO this assumption Hstep should be generalised to >= *)
    (Hstep : forall sl, | lf (step sl) | = 1)
    : forall p, rad_semantics (apply_lf_trace p).
  Proof.
    intros.
    unfold apply_lf_trace.
    econstructor;intros.
    - cbn in *.
      reflexivity.
    - destruct sl.
      + cbn.
        rewrite app_nil_r.
        eapply Hi.
      + cbn in H.
        exists (hd y (apply_lf' lf ([step (multi_step_hd step (p,i) (|sl|))]))).
        cbn.
        rewrite <-multi_step_S.
        rewrite multi_step_S2.
        rewrite app_nil_r.
        rewrite cons_app.
        setoid_rewrite apply_lf'_app.
        setoid_rewrite H.
        cbn.
        rewrite app_nil_r.
        rewrite cons_app with (xl:= y :: sl).
        rewrite hd_len1.
        * reflexivity.
        * eapply Hstep.
    - cbn in H0, H1.
      rewrite H0 in H1.
      inversion H1.
      reflexivity.
    - destruct sl;cbn.
      + reflexivity.
      + cbn in H.
        rewrite <-multi_step_S in H.
        rewrite multi_step_S2 in H.
        rewrite cons_app in H.
        rewrite apply_lf'_app in H.
        cbn in H.
        rewrite app_nil_r in H.
        setoid_rewrite <-hd_len1 with (x:=s) in H at 2.
        * rewrite <-cons_app in H.
          inversion H.
          reflexivity.
        * eapply Hstep.
  Qed.
End with_lf.