Library mcertikos.conlib.conmtlib.RegsetLessdef

Require Import Coqlib.
Require Import CommonTactic.
Require Import LAsm.
Require Import AlgebraicMem.
Require Import Values.
Require Import Maps.
Require Import Integers.

Section LessDef.

  Definition regset_lessdef (rs rs´: regset) :=
    ∀ i, Val.lessdef (rs i) (rs´ i).

  Lemma regset_lessdef_refl:
    ∀ rs,
      regset_lessdef rs rs.
  Proof.
    intros rs i.
    eapply Val.lessdef_refl.
  Qed.

  Lemma regset_lessdef_eq:
    ∀ rs rs´ r v,
      regset_lessdef rs rs´ →
      rs r = v →
      v ≠ Vundef →
      rs´ r = v.
  Proof.
    intros. specialize (H r).
    rewrite H0 in H. inv H; trivial.
    congruence.
  Qed.

  Lemma regset_lessdef_eq´:
    ∀ rs rs´ r v,
      regset_lessdef rs rs´ →
      rs´ r = v →
      rs r ≠ Vundef →
      rs r = v.
  Proof.
    intros. specialize (H r).
    rewrite H0 in H. inv H; trivial.
    congruence.
  Qed.

  Lemma regset_lessdef_neq:
    ∀ rs rs´ r,
      regset_lessdef rs rs´ →
      rs r ≠ Vundef →
      rs´ r ≠ Vundef.
  Proof.
    intros. specialize (H r).
    inv H; trivial. congruence.
  Qed.

  Lemma regset_lessdef_set:
    ∀ rs rs´ r v v´,
      regset_lessdef rs rs´ →
      Val.lessdef v v´ →
      regset_lessdef (rs # r <- v) (rs´ # r <- v´).
  Proof.
    unfold regset_lessdef. intros.
    destruct (PregEq.eq i r); subst.
    - repeat rewrite Pregmap.gss. assumption.
    - repeat rewrite Pregmap.gso; auto.
  Qed.

  Lemma Val_add_lessdef:
    ∀ v1 v1´ v2 v2´,
      Val.lessdef v1 v1´ →
      Val.lessdef v2 v2´ →
      Val.lessdef (Val.add v1 v2) (Val.add v1´ v2´).
  Proof.
    intros. destruct v1, v2; inv H; inv H0; try constructor.
  Qed.

  Lemma regset_lessdef_nextinstr:
    ∀ rs rs´,
      regset_lessdef rs rs´ →
      regset_lessdef (nextinstr rs) (nextinstr rs´).
  Proof.
    intros. unfold nextinstr.
    eapply regset_lessdef_set; auto.
    eapply Val_add_lessdef; eauto.
  Qed.

  Lemma regset_lessdef_undef_regs:
    ∀ vl rs rs´,
      regset_lessdef rs rs´ →
      regset_lessdef (undef_regs vl rs) (undef_regs vl rs´).
  Proof.
    induction vl.
    - intros. assumption.
    - intros.
      Local Transparent undef_regs.
      simpl. eapply IHvl.
      eapply regset_lessdef_set; eauto.
      Local Opaque undef_regs.
  Qed.

  Lemma regset_lessdef_nextinstr_nf:
    ∀ rs rs´,
      regset_lessdef rs rs´ →
      regset_lessdef (nextinstr_nf rs) (nextinstr_nf rs´).
  Proof.
    intros. unfold nextinstr_nf.
    eapply regset_lessdef_nextinstr; auto.
    eapply regset_lessdef_undef_regs; auto.
  Qed.

  Lemma regset_lessdef_set_regs:
    ∀ res vl vl´ rs rs´,
      regset_lessdef rs rs´ →
      Val.lessdef_list vl vl´ →
      regset_lessdef (set_regs res vl rs) (set_regs res vl´ rs´).
  Proof.
    induction res.
    - intros. assumption.
    - intros. simpl.
      destruct vl; inv H0.
      + assumption.
      + eapply IHres; eauto.
        eapply regset_lessdef_set; eauto.
  Qed.

  Lemma lessdef_list_refl:
    ∀ a,
      Val.lessdef_list a a.
  Proof.
    induction a.
    - constructor.
    - eapply Val.lessdef_list_cons; eauto.
  Qed.

  Lemma Val_lessdef_intoffloat:
    ∀ v v´,
      Val.lessdef v v´ →
      Val.lessdef (Val.maketotal (Val.intoffloat v)) (Val.maketotal (Val.intoffloat v´)).
  Proof.
    intros. destruct v; inv H; trivial.
  Qed.

  Lemma Val_lessdef_floatofint:
    ∀ v v´,
      Val.lessdef v v´ →
      Val.lessdef (Val.maketotal (Val.floatofint v)) (Val.maketotal (Val.floatofint v´)).
  Proof.
    intros. destruct v; inv H; trivial.
  Qed.

  Lemma Val_lessdef_neg:
    ∀ v v´,
      Val.lessdef v v´ →
      Val.lessdef (Val.neg v) (Val.neg v´).
  Proof.
    intros. destruct v; inv H; trivial.
  Qed.

  Lemma Val_lessdef_negf:
    ∀ v v´,
      Val.lessdef v v´ →
      Val.lessdef (Val.negf v) (Val.negf v´).
  Proof.
    intros. destruct v; inv H; trivial.
  Qed.

  Lemma Val_lessdef_absf:
    ∀ v v´,
      Val.lessdef v v´ →
      Val.lessdef (Val.absf v) (Val.absf v´).
  Proof.
    intros. destruct v; inv H; trivial.
  Qed.

  Lemma Val_lessdef_sub:
    ∀ v1 v1´ v2 v2´,
      Val.lessdef v1 v1´ →
      Val.lessdef v2 v2´ →
      Val.lessdef (Val.sub v1 v2) (Val.sub v1´ v2´).
  Proof.
    intros. destruct v1, v2; inv H; inv H0; trivial.
  Qed.

  Lemma Val_lessdef_subf:
    ∀ v1 v1´ v2 v2´,
      Val.lessdef v1 v1´ →
      Val.lessdef v2 v2´ →
      Val.lessdef (Val.subf v1 v2) (Val.subf v1´ v2´).
  Proof.
    intros. destruct v1, v2; inv H; inv H0; trivial.
  Qed.

  Lemma Val_lessdef_mul:
    ∀ v1 v1´ v2 v2´,
      Val.lessdef v1 v1´ →
      Val.lessdef v2 v2´ →
      Val.lessdef (Val.mul v1 v2) (Val.mul v1´ v2´).
  Proof.
    intros. destruct v1, v2; inv H; inv H0; trivial.
  Qed.

  Lemma Val_lessdef_mulf:
    ∀ v1 v1´ v2 v2´,
      Val.lessdef v1 v1´ →
      Val.lessdef v2 v2´ →
      Val.lessdef (Val.mulf v1 v2) (Val.mulf v1´ v2´).
  Proof.
    intros. destruct v1, v2; inv H; inv H0; trivial.
  Qed.

  Lemma Val_lessdef_addf:
    ∀ v1 v1´ v2 v2´,
      Val.lessdef v1 v1´ →
      Val.lessdef v2 v2´ →
      Val.lessdef (Val.addf v1 v2) (Val.addf v1´ v2´).
  Proof.
    intros. destruct v1, v2; inv H; inv H0; trivial.
  Qed.

  Lemma Val_lessdef_eval_addrmode:
    ∀ (ge: genv) a rs rs´,
      regset_lessdef rs rs´ →
      Val.lessdef (eval_addrmode ge a rs) (eval_addrmode ge a rs´).
  Proof.
    intros. unfold eval_addrmode.
    destruct a.
    destruct base, ofs, const; try destruct p;
    repeat eapply Val.add_lessdef; eauto;
    (destruct (Int.eq i2 Int.one)||
     destruct (Int.eq i1 Int.one)||
     destruct (Int.eq i0 Int.one));
    try eapply Val_lessdef_mul; eauto.
  Qed.

  Lemma Val_lessdef_mulhs:
    ∀ v1 v1´ v2 v2´,
      Val.lessdef v1 v1´ →
      Val.lessdef v2 v2´ →
      Val.lessdef (Val.mulhs v1 v2) (Val.mulhs v1´ v2´).
  Proof.
    intros. destruct v1, v2; inv H; inv H0; trivial.
  Qed.

  Lemma Val_lessdef_mulhu:
    ∀ v1 v1´ v2 v2´,
      Val.lessdef v1 v1´ →
      Val.lessdef v2 v2´ →
      Val.lessdef (Val.mulhu v1 v2) (Val.mulhu v1´ v2´).
  Proof.
    intros. destruct v1, v2; inv H; inv H0; trivial.
  Qed.

  Lemma Val_lessdef_and:
    ∀ v1 v1´ v2 v2´,
      Val.lessdef v1 v1´ →
      Val.lessdef v2 v2´ →
      Val.lessdef (Val.and v1 v2) (Val.and v1´ v2´).
  Proof.
    intros. destruct v1, v2; inv H; inv H0; trivial.
  Qed.

  Lemma Val_lessdef_or:
    ∀ v1 v1´ v2 v2´,
      Val.lessdef v1 v1´ →
      Val.lessdef v2 v2´ →
      Val.lessdef (Val.or v1 v2) (Val.or v1´ v2´).
  Proof.
    intros. destruct v1, v2; inv H; inv H0; trivial.
  Qed.

  Lemma Val_lessdef_xor:
    ∀ v1 v1´ v2 v2´,
      Val.lessdef v1 v1´ →
      Val.lessdef v2 v2´ →
      Val.lessdef (Val.xor v1 v2) (Val.xor v1´ v2´).
  Proof.
    intros. destruct v1, v2; inv H; inv H0; trivial.
  Qed.

  Lemma Val_lessdef_shl:
    ∀ v1 v1´ v2 v2´,
      Val.lessdef v1 v1´ →
      Val.lessdef v2 v2´ →
      Val.lessdef (Val.shl v1 v2) (Val.shl v1´ v2´).
  Proof.
    intros. destruct v1, v2; inv H; inv H0; trivial.
  Qed.

  Lemma Val_lessdef_shru:
    ∀ v1 v1´ v2 v2´,
      Val.lessdef v1 v1´ →
      Val.lessdef v2 v2´ →
      Val.lessdef (Val.shru v1 v2) (Val.shru v1´ v2´).
  Proof.
    intros. destruct v1, v2; inv H; inv H0; trivial.
  Qed.

  Lemma Val_lessdef_shr:
    ∀ v1 v1´ v2 v2´,
      Val.lessdef v1 v1´ →
      Val.lessdef v2 v2´ →
      Val.lessdef (Val.shr v1 v2) (Val.shr v1´ v2´).
  Proof.
    intros. destruct v1, v2; inv H; inv H0; trivial.
  Qed.

  Lemma Val_lessdef_ror:
    ∀ v1 v1´ v2 v2´,
      Val.lessdef v1 v1´ →
      Val.lessdef v2 v2´ →
      Val.lessdef (Val.ror v1 v2) (Val.ror v1´ v2´).
  Proof.
    intros. destruct v1, v2; inv H; inv H0; trivial.
  Qed.

  Lemma Val_lessdef_notint:
    ∀ v v´,
      Val.lessdef v v´ →
      Val.lessdef (Val.notint v) (Val.notint v´).
  Proof.
    intros. destruct v; inv H; trivial.
  Qed.

  Lemma Val_lessdef_divf:
    ∀ v1 v1´ v2 v2´,
      Val.lessdef v1 v1´ →
      Val.lessdef v2 v2´ →
      Val.lessdef (Val.divf v1 v2) (Val.divf v1´ v2´).
  Proof.
    intros. destruct v1, v2; inv H; inv H0; trivial.
  Qed.

  Lemma Val_lessdef_negative:
    ∀ v v´,
      Val.lessdef v v´ →
      Val.lessdef (Val.negative v) (Val.negative v´).
  Proof.
    intros. destruct v; inv H; trivial.
  Qed.

  Lemma Val_lessdef_sub_overflow:
    ∀ v1 v1´ v2 v2´,
      Val.lessdef v1 v1´ →
      Val.lessdef v2 v2´ →
      Val.lessdef (Val.sub_overflow v1 v2) (Val.sub_overflow v1´ v2´).
  Proof.
    intros. destruct v1, v2; inv H; inv H0; trivial.
  Qed.

  Lemma regset_lessdef_imply_Val:
    ∀ rs rs´ r,
      regset_lessdef rs rs´ →
      Val.lessdef (rs r) (rs´ r).
  Proof.
    intros. eauto.
  Qed.

  Lemma Val_lessdef_negl:
    ∀ v v´,
      Val.lessdef v v´ →
      Val.lessdef (Val.negl v) (Val.negl v´).
  Proof.
    intros. destruct v; inv H; trivial.
  Qed.

  Lemma Val_lessdef_addl:
    ∀ v1 v2 v1´ v2´,
      Val.lessdef v1 v1´ →
      Val.lessdef v2 v2´ →
      Val.lessdef (Val.addl v1 v2) (Val.addl v1´ v2´).
  Proof.
    intros. destruct v1, v2; inv H; inv H0; trivial.
  Qed.

  Lemma Val_lessdef_subl:
    ∀ v1 v2 v1´ v2´,
      Val.lessdef v1 v1´ →
      Val.lessdef v2 v2´ →
      Val.lessdef (Val.subl v1 v2) (Val.subl v1´ v2´).
  Proof.
    intros. destruct v1, v2; inv H; inv H0; trivial.
  Qed.

  Lemma Val_lessdef_mull´:
    ∀ v1 v2 v1´ v2´,
      Val.lessdef v1 v1´ →
      Val.lessdef v2 v2´ →
      Val.lessdef (Val.mull´ v1 v2) (Val.mull´ v1´ v2´).
  Proof.
    intros. destruct v1, v2; inv H; inv H0; trivial.
  Qed.

  Lemma regset_lessdef_eval_testcond:
    ∀ rs rs´ c b,
      eval_testcond c rs = Some b →
      regset_lessdef rs rs´ →
      eval_testcond c rs´ = Some b.
  Proof.
    intros.
    pose proof (H0 ZF) as Hzf.
    pose proof (H0 CF) as Hcf.
    pose proof (H0 OF) as Hof.
    pose proof (H0 SF) as Hsf.
    pose proof (H0 PF) as Hpf.
    destruct c; simpl in *;
    subdestruct.
    - inv Hzf; trivial.
    - inv Hzf; trivial.
    - inv Hcf; trivial.
    - inv Hcf; inv Hzf; trivial.
    - inv Hcf; trivial.
    - inv Hcf; inv Hzf; trivial.
    - inv Hof; inv Hsf; trivial.
    - inv Hof; inv Hsf; inv Hzf; trivial.
    - inv Hof; inv Hsf; trivial.
    - inv Hof; inv Hsf; inv Hzf; trivial.
    - inv Hpf; trivial.
    - inv Hpf; trivial.
  Qed.

  Lemma regset_lessdef_set_undef:
    ∀ rs rs´ r,
      regset_lessdef rs rs´ →
      regset_lessdef (rs # r <- Vundef) rs´.
  Proof.
    unfold regset_lessdef. intros.
    destruct (PregEq.eq i r); subst.
    - rewrite Pregmap.gss. constructor.
    - rewrite Pregmap.gso; auto.
  Qed.

  Lemma Val_divu_lessdef:
    ∀ v1´ v2´ v1 v2 v,
      Val.divu v1 v2 = Some v →
      Val.lessdef v1 v1´ →
      Val.lessdef v2 v2´ →
      ∃ v´,
        Val.divu v1´ v2´ = Some v´
        ∧ Val.lessdef v v´.
  Proof.
    intros. destruct v1, v2; inv H0; inv H1; inv H.
    simpl. subdestruct. inv H1.
    refine_split´; eauto.
  Qed.

  Lemma Val_divs_lessdef:
    ∀ v1´ v2´ v1 v2 v,
      Val.divs v1 v2 = Some v →
      Val.lessdef v1 v1´ →
      Val.lessdef v2 v2´ →
      ∃ v´,
        Val.divs v1´ v2´ = Some v´
        ∧ Val.lessdef v v´.
  Proof.
    intros. destruct v1, v2; inv H0; inv H1; inv H.
    simpl. subdestruct. inv H1.
    refine_split´; eauto.
  Qed.

  Lemma Val_modu_lessdef:
    ∀ v1´ v2´ v1 v2 v,
      Val.modu v1 v2 = Some v →
      Val.lessdef v1 v1´ →
      Val.lessdef v2 v2´ →
      ∃ v´,
        Val.modu v1´ v2´ = Some v´
        ∧ Val.lessdef v v´.
  Proof.
    intros. destruct v1, v2; inv H0; inv H1; inv H.
    simpl. subdestruct. inv H1.
    refine_split´; eauto.
  Qed.

  Lemma Val_mods_lessdef:
    ∀ v1´ v2´ v1 v2 v,
      Val.mods v1 v2 = Some v →
      Val.lessdef v1 v1´ →
      Val.lessdef v2 v2´ →
      ∃ v´,
        Val.mods v1´ v2´ = Some v´
        ∧ Val.lessdef v v´.
  Proof.
    intros. destruct v1, v2; inv H0; inv H1; inv H.
    simpl. subdestruct. inv H1.
    refine_split´; eauto.
  Qed.

  Lemma regset_lessdef_imply_list_lessdef:
    ∀ args rs rs0,
      regset_lessdef rs rs0 →
      Val.lessdef_list (map rs args) (map rs0 args).
  Proof.
    induction args.
    - simpl. intros. constructor.
    - intros. simpl. eapply Val.lessdef_list_cons; eauto.
  Qed.

End LessDef.

Ltac Val_lessdef_solve_tac :=
  match goal with
    | |- Val.lessdef ?v ?v ⇒
      eapply Val.lessdef_refl; eauto 2
    | |- Val.lessdef (_ _ _) _ ⇒
      match goal with
        | |- Val.lessdef (Val.zero_ext _ _) _ ⇒
          eapply Val.zero_ext_lessdef; eauto 2
        | |- Val.lessdef (Val.sign_ext _ _) _ ⇒
          eapply Val.sign_ext_lessdef; eauto 2
        | |- Val.lessdef (Val.sub _ _) _ ⇒
          eapply Val_lessdef_sub; eauto 2
        | |- Val.lessdef (Val.sub_overflow _ _) _ ⇒
          eapply Val_lessdef_sub_overflow; eauto 2
        | |- Val.lessdef (Val.subf _ _) _ ⇒
          eapply Val_lessdef_subf; eauto 2
        | |- Val.lessdef (Val.subl _ _) _ ⇒
          eapply Val_lessdef_subl; eauto 2
        | |- Val.lessdef (Val.add _ _) _ ⇒
          eapply Val.add_lessdef; eauto 2
        | |- Val.lessdef (Val.addf _ _) _ ⇒
          eapply Val_lessdef_addf; eauto 2
        | |- Val.lessdef (Val.addl _ _) _ ⇒
          eapply Val_lessdef_addl; eauto 2
        | |- Val.lessdef (Val.and _ _) _ ⇒
          eapply Val_lessdef_and; eauto 2
        | |- Val.lessdef (Val.or _ _) _ ⇒
          eapply Val_lessdef_or; eauto 2
        | |- Val.lessdef (Val.xor _ _) _ ⇒
          eapply Val_lessdef_xor; eauto 2
        | |- Val.lessdef (Val.ror _ _) _ ⇒
          eapply Val_lessdef_ror; eauto 2
        | |- Val.lessdef (Val.mul _ _) _ ⇒
          eapply Val_lessdef_mul; eauto 2
        | |- Val.lessdef (Val.mulf _ _) _ ⇒
          eapply Val_lessdef_mulf; eauto 2
        | |- Val.lessdef (Val.mull´ _ _) _ ⇒
          eapply Val_lessdef_mull´; eauto 2
        | |- Val.lessdef (Val.mulhs _ _) _ ⇒
          eapply Val_lessdef_mulhs; eauto 2
        | |- Val.lessdef (Val.mulhu _ _) _ ⇒
          eapply Val_lessdef_mulhu; eauto 2
        | |- Val.lessdef (Val.shl _ _) _ ⇒
          eapply Val_lessdef_shl; eauto 2
        | |- Val.lessdef (Val.shr _ _) _ ⇒
          eapply Val_lessdef_shr; eauto 2
        | |- Val.lessdef (Val.shru _ _) _ ⇒
          eapply Val_lessdef_shru; eauto 2
        | |- Val.lessdef (Val.divf _ _) _ ⇒
          eapply Val_lessdef_divf; eauto 2
        | |- Val.lessdef (Val.load_result _ _) _ ⇒
          eapply Val.load_result_lessdef; eauto 2
      end
    | |- Val.lessdef (_ _) _ ⇒
      match goal with
        | |- Val.lessdef (Val.singleoffloat _) _ ⇒
          eapply Val.singleoffloat_lessdef; eauto 2
        | |- Val.lessdef (Val.maketotal (Val.intoffloat _)) _ ⇒
          eapply Val_lessdef_intoffloat; eauto 2
        | |- Val.lessdef (Val.maketotal (Val.floatofint _)) _ ⇒
          eapply Val_lessdef_floatofint; eauto 2
        | |- Val.lessdef (Val.neg _) _ ⇒
          eapply Val_lessdef_neg; eauto 2
        | |- Val.lessdef (Val.negative _) _ ⇒
          eapply Val_lessdef_negative; eauto 2
        | |- Val.lessdef (Val.negf _) _ ⇒
          eapply Val_lessdef_negf; eauto 2
        | |- Val.lessdef (Val.negl _) _ ⇒
          eapply Val_lessdef_negl; eauto 2
        | |- Val.lessdef (Val.absf _) _ ⇒
          eapply Val_lessdef_absf; eauto 2
        | |- Val.lessdef (Val.notint _) _ ⇒
          eapply Val_lessdef_notint; eauto 2
        | |- Val.lessdef (Val.hiword _) _ ⇒
          eapply Val.hiword_lessdef; eauto 2
        | |- Val.lessdef (Val.loword _) _ ⇒
          eapply Val.loword_lessdef; eauto 2
      end
    | |- Val.lessdef (eval_addrmode _ _ _) _ ⇒
      eapply Val_lessdef_eval_addrmode; eauto 2
    | |- _ ⇒
      try eapply regset_lessdef_imply_Val; eauto 2
  end.

Ltac Val_lessdef_list_solve_tac :=
  repeat match goal with
           | |- Val.lessdef_list ?vl ?vl ⇒
             eapply lessdef_list_refl; eauto 2
           | |- Val.lessdef_list (_ :: _) _ ⇒
             constructor
           | |- Val.lessdef _ _ ⇒
             Val_lessdef_solve_tac
         end.

Require Import liblayers.compat.CompatData.
Require Import liblayers.compcertx.MemWithData.

Section WithMem.

  Context `{agmem: AlgebraicMemory}.
  Context {D} `{data_prf : CompatData D}.
  Context `{Hmwd: UseMemWithData mem}.

  Lemma Val_cmpu_disjoint_union_valid_pointer:
    ∀ m m0 gm v1 v2 v1´ v2´ C,
      Val.lessdef v1 v1´ →
      Val.lessdef v2 v2´ →
      mem_disjoint_union m m0 gm →
      Val.lessdef (Val.cmpu (Mem.valid_pointer m) C v1 v2)
                  (Val.cmpu (Mem.valid_pointer gm) C v1´ v2´).
  Proof.
    unfold Val.cmpu. intros. eapply Val.of_optbool_lessdef; try eassumption.
    intros. eapply Val.cmpu_bool_lessdef; try eassumption.
    intros. eapply mem_valid_pointer_disjoint_union; eauto.
  Qed.

  Lemma compare_ints_disjoint_union_lessdef:
    ∀ m m0 gm rs rs´ v1 v2 v1´ v2´ abd,
      mem_disjoint_union m m0 gm →
      regset_lessdef rs rs´ →
      Val.lessdef v1 v1´ →
      Val.lessdef v2 v2´ →
      regset_lessdef (compare_ints (mem:= mwd (cdata D)) v1 v2 rs (m, abd))
                     (compare_ints v1´ v2´ rs´ (gm, abd)).
  Proof.
    intros.
    unfold compare_ints. lift_unfold.
    repeat (eapply regset_lessdef_set; eauto 2).
    - eapply Val_cmpu_disjoint_union_valid_pointer; eauto.
    - eapply Val_cmpu_disjoint_union_valid_pointer; eauto.
    - repeat Val_lessdef_solve_tac.
    - repeat Val_lessdef_solve_tac.
  Qed.

End WithMem.

Ltac regset_lessdef_solve_tac :=
  repeat match goal with
           | |- regset_lessdef (nextinstr _) _ ⇒
             eapply regset_lessdef_nextinstr; eauto 2
           | |- regset_lessdef (nextinstr_nf _) _ ⇒
             eapply regset_lessdef_nextinstr_nf; eauto 2
           | |- regset_lessdef (undef_regs _ _) _ ⇒
             eapply regset_lessdef_undef_regs; eauto 2
           | |- regset_lessdef (set_regs _ _ _) _ ⇒
             eapply regset_lessdef_set_regs; eauto 2
           | |- regset_lessdef (_ # _ <- _) _ ⇒
             eapply regset_lessdef_set; eauto 2
           | |- regset_lessdef (compare_ints _ _ _ _) _ ⇒
             eapply compare_ints_disjoint_union_lessdef; eauto 2
           | |- Val.lessdef _ _ ⇒
             Val_lessdef_solve_tac
           | |- Val.lessdef_list _ _ ⇒
             eapply lessdef_list_refl; eauto 2
         end.

Section Others.

  Lemma compare_floats_lessdef:
    ∀ rs rs´ v1 v2 v1´ v2´,
      regset_lessdef rs rs´ →
      Val.lessdef v1 v1´ →
      Val.lessdef v2 v2´ →
      regset_lessdef (compare_floats v1 v2 rs)
                     (compare_floats v1´ v2´ rs´).
  Proof.
    intros.
    Local Transparent undef_regs.
    destruct v1, v2; inv H0; inv H1;
    try destruct v1´; try destruct v2´; simpl;
    regset_lessdef_solve_tac.
    Local Opaque undef_regs.
  Qed.

  Context `{agmem: AlgebraicMemory}.
  Context {D} `{data_prf : CompatData D}.
  Context `{Hmwd: UseMemWithData mem}.

  Lemma goto_label_disjoint_union:
    ∀ f l rs rs´ rs0 m m´ m0 gm abd abd´,
      goto_label (mem:= mwd (cdata D)) f l rs (m, abd) = Next rs´ (m´, abd´) →
      mem_disjoint_union m m0 gm →
      (Mem.nextblock m0 ≤ Mem.nextblock m)%positive →
      regset_lessdef rs rs0 →
      ∃ gm´ rs0´,
        goto_label f l rs0 (gm, abd) = Next rs0´ (gm´, abd´)
        ∧ mem_disjoint_union m´ m0 gm´
        ∧ regset_lessdef rs´ rs0´.
  Proof.
    unfold goto_label; intros.
    pose proof (H2 PC) as Hpc.
    subdestruct. inv Hpc.
    inv H; refine_split´; auto; regset_lessdef_solve_tac.
  Qed.

End Others.