Module LiftDummy

Require Import FSets.
Require Import CoqlibC Maps Ordered Errors Lattice Kildall Integers.
Require Import AST Linking.
Require Import Values Memory Events Globalenvs SmallstepC.
Require Import sflib.



Section LIFTDUMMY.

Context {G ST: Type}.
Variable step: Senv.t -> G -> ST -> trace -> ST -> Prop.
Variable wf_tgt: ST -> Prop.
Variable strong_wf_tgt: ST -> Prop.
Hypothesis strong_wf_tgt_strong: strong_wf_tgt <1= wf_tgt.
Hypothesis strong_wf_tgt_spec: forall se ge st0 st1 tr0
    (HSWF: strong_wf_tgt st0)
    (HSTEP: step se ge st0 tr0 st1),
    <<HSWF: strong_wf_tgt st1>> \/ <<STUCK: forall tr1 st2 (HSTEP0: step se ge st1 tr1 st2), False>>.
Hypothesis wf_tgt_strengthen: forall se ge st0 tr st1
    (HWF0: strong_wf_tgt st0)
    (HSTEP: step se ge st0 tr st1)
    (HWF1: wf_tgt st1),
    <<WFTGT1: strong_wf_tgt st1>>.

Let strong_wf_tgt_spec_starN: forall se ge n st0 st1 tr0 tr1 st2
    (STEP: step se ge st0 tr0 st1)
    (STAR: starN (step) se ge n st1 tr1 st2)
    (DUMMYTGT: strong_wf_tgt st0)
    (STKAFTER: wf_tgt st2) ,
    <<WF: strong_wf_tgt st1>>.
Proof.
  ii. exploit strong_wf_tgt_spec; eauto. intro P. destruct n; ss.
  { inv STAR. des; ss. eapply wf_tgt_strengthen; eauto. }
  des; ss. exfalso. inv STAR. eapply STUCK; eauto.
Qed.

Let wf_step (se: Senv.t) (ge: G) (st0: ST) (tr: trace) (st1: ST) :=
  step se ge st0 tr st1 /\ wf_tgt st1.

Lemma lift_starN
      cnt tse tge st_tgt0 tr st_tgt1
      (STAR: starN step tse tge cnt st_tgt0 tr st_tgt1)
      (DUMMYTGT: strong_wf_tgt st_tgt0)
      (STKAFTER: wf_tgt st_tgt1):
    <<STAR: starN wf_step tse tge cnt st_tgt0 tr st_tgt1>> /\ <<DUMMYTGT: strong_wf_tgt st_tgt1>>.
Proof.
  induction STAR; ii; ss.
  { esplits; eauto. econs; et. }
  pose s as S1. pose s' as S2. pose s'' as S3.
  exploit strong_wf_tgt_spec_starN; eauto. i; des.
  exploit IHSTAR; eauto. i; des.
  esplits; eauto. econs; eauto. rr. esplits; eauto.
Qed.

Lemma lift_plus
      se ge st_tgt0 tr st_tgt1
      (PLUS: plus step se ge st_tgt0 tr st_tgt1)
      (DUMMYTGT: strong_wf_tgt st_tgt0)
      (STKAFTER: wf_tgt st_tgt1):
    <<PLUS: plus wf_step se ge st_tgt0 tr st_tgt1>> /\ <<DUMMYTGT: strong_wf_tgt st_tgt1>>.
Proof.
  apply starN_plus_iff in PLUS. des. apply lift_starN in PLUS; et. des. esplits; et. apply starN_plus_iff; et.
Qed.

End LIFTDUMMY.