Library CorrelatingProgram

Require Import Utf8.

Require Import ZArith.
Require Import List.
Import ListNotations.
Require Import Bool.

Require Import Equalities.
Require Import FMapWeakList.
Require Import FMapFacts.

Require Export CoqDefs.

Lemma Forall_app :
   {A} (P : A Prop) l1 l2,
  Forall P l1 Forall P l2 Forall P (l1 ++ l2).
Proof.
  intros A P l1 l2. induction l1.
  × intros. simpl. auto.
  × intros H1 H2. simpl. inversion H1. subst. auto.
Qed.

Definition ret {A : Type} (x : A) := Some x.
Definition bind {A B : Type} (a : option A) (f : A option B) :=
    match a with
    | NoneNone
    | Some xf x
    end.

Notation "a >>= f" := (bind a f) (at level 40, left associativity).

Module CP (Var_as_DT : UsualDecidableTypeOrig).
  Module VarMap := FMapWeakList.Make(Var_as_DT).
  Module VarMapFacts := FMapFacts.WFacts_fun Var_as_DT VarMap.
  Module VarMapProps := FMapFacts.WProperties_fun Var_as_DT VarMap.

  Module LangDefs := Languages (Var_as_DT).
  Export LangDefs.

  Hint Constructors big_step.
  Hint Constructors path_suffix.

  Proposition path_suffix_inv_S0:
     g π, path_suffix g (S0 π) path_suffix g π.
  Proof.
    intro g. induction g ; intros n H ; inversion H ; subst ; auto.
  Qed.

  Proposition path_suffix_inv_S1:
     g π, path_suffix g (S1 π) path_suffix g π.
  Proof.
    intro g. induction g ; intros n H ; inversion H ; subst ; auto.
  Qed.

  Hint Resolve path_suffix_inv_S0.
  Hint Resolve path_suffix_inv_S1.

  Fixpoint path_length (π : path) :=
    match π with
    | S0 π | S1 π ⇒ S (path_length π)
    | εO
    end.

  Lemma suffix_order_implies_length_order:
     g π, path_suffix g π path_length g path_length π.
  Proof.
    intros g π H. induction H.
    × auto.
    × simpl. auto.
    × simpl. auto.
  Qed.

  Lemma S0g_not_suffix_g:
     g, ¬ path_suffix g (S0 g).
  Proof.
    intros g H. pose proof (suffix_order_implies_length_order g (S0 g) H).
    simpl in ×. omega.
  Qed.

  Lemma S1g_not_suffix_g:
     g, ¬ path_suffix g (S1 g).
  Proof.
    intros g H. pose proof (suffix_order_implies_length_order g (S1 g) H).
    simpl in ×. omega.
  Qed.

  Hint Resolve S0g_not_suffix_g S1g_not_suffix_g.

  Lemma path_suffix_S0_S1_exclusive:
     π, path_suffix π (S0 ε) path_suffix π (S1 ε) False.
  Proof.
    intros π H. remember (S0 ε) as s eqn:Hs. induction H ; subst.
    × intro H'. inversion H' ; subst. inversion H0.
    × intro H'. apply IHpath_suffix.
      + auto.
      + inversion H' ; subst ; auto.
    × intro H'. inversion H' ; subst ; auto. inversion H.
  Qed.

  Hint Constructors big_step_g.

  Definition loop_broken G πl := GuardMap.find πl G = Some false.
  Definition loop_continued G πl := GuardMap.find (S1 πl) G = Some false.

  Fixpoint CI gl π c o :=
    match c with
    | Leaf SkipGSkip
    | Leaf (Assign x e) ⇒ GAtomic gl (GAAssign x e)
    | Seq c₁ c₂GSeq (CI gl (S0 π) c₁ o) (CI gl (S1 π) c₂ o)
    | IfThenElse b c₁ c₂ ⇒ (
      GAtomic gl (GAGAssign π b);
      CI (gl ++ [(true, π)]) (S1 π) c₁ o;
      CI (gl ++ [(false, π)]) (S0 π) c₂ o)%GAST
    | While b c ⇒ (
      GAtomic gl (GAGAssign π b);
      GWhile [gl ++ [(true, π)]] (
        GAtomic (gl ++ [(true, π)]) (GAGAssign (S1 π) BTrue);
        CI (gl ++ [(true, π)] ++ [(true, S1 π)]) (S1 (S1 π)) c (Some π);
        GAtomic (gl ++ [(true, π)]) (GAGAssign π b)
      ))%GAST
    | Leaf Breakmatch o with
      | Some πlGAtomic gl (GAGAssign πl BFalse)
      | NoneGSkip
      end
    | Leaf Continuematch o with
      | Some πlGAtomic gl (GAGAssign (S1 πl) BFalse)
      | NoneGSkip
      end
    end.

  Property guard_conj_evals_to_true_cons_inv:
     G bπ gl, guard_conj_evals_to G (bπ::gl) true
    guard_conj_evals_to G gl true.
  Proof.
    intros G bπ gl H.
    unfold guard_conj_evals_to in ×. simpl in H. destruct bπ as (b, π).
    destruct (GuardMap.find π G) as [b' | ] ; simpl in H ; [ | inversion H ].
    destruct b ; destruct b' ; simpl in H ; auto ; inversion H.
  Qed.

  Property guard_conj_evals_to_true_app_inv:
     G gl₀ gl₁, guard_conj_evals_to G (gl₀ ++ gl₁) true
    guard_conj_evals_to G gl₀ true guard_conj_evals_to G gl₁ true.
  Proof.
    intros G gl₀. induction gl₀ ; intros gl₁ Hgl₀₁.
    × split ; auto. unfold guard_conj_evals_to. simpl. auto.
    × destruct a as (b, π).
      unfold guard_conj_evals_to in Hgl₀₁. simpl in Hgl₀₁.
      remember (GuardMap.find π G) as ov.
      destruct ov as [v | ] ; [ | inversion Hgl₀₁ ].
      simpl in Hgl₀₁. destruct v ; destruct b ; simpl in ×.
      + destruct (IHgl₀ gl₁) ; auto. split ; auto.
        unfold guard_conj_evals_to. simpl. rewrite <- Heqov. simpl. auto.
      + inversion Hgl₀₁.
      + inversion Hgl₀₁.
      + destruct (IHgl₀ gl₁) ; auto. split ; auto.
        unfold guard_conj_evals_to. simpl. rewrite <- Heqov. simpl. auto.
  Qed.

  Property guard_conj_evals_to_true_app:
     G gl gl', guard_conj_evals_to G gl true
    guard_conj_evals_to G gl' true
    guard_conj_evals_to G (gl ++ gl') true.
  Proof.
    intros G gl. induction gl ; intros gl' Hgl Hgl'.
    × simpl. auto.
    × simpl. destruct a as (b, π). unfold guard_conj_evals_to. simpl.
      unfold guard_conj_evals_to in Hgl. simpl in Hgl. destruct (GuardMap.find π G) as [ v | ] ;
      simpl in Hgl ; [ | inversion Hgl ].
      destruct v ; destruct b ; simpl in × ; auto ; apply IHgl ; auto.
  Qed.

  Property guard_conj_evals_to_false_app_1:
     G gl gl', guard_conj_evals_to G gl false guard_conj_evals_to G (gl ++ gl') false.
  Proof.
    intros G gl. induction gl ; intros gl' Hgl.
    × unfold guard_conj_evals_to in Hgl. simpl in Hgl. inversion Hgl.
    × destruct a as (b, π).
      unfold guard_conj_evals_to.
      unfold guard_conj_evals_to in Hgl.
      simpl in ×. destruct (GuardMap.find π G) as [ v | ] ; simpl in Hgl ; [ | inversion Hgl ].
      destruct v ; destruct b ; simpl ; auto ;
      simpl in Hgl ; apply IHgl ; auto.
  Qed.

  Property guard_conj_evals_to_false_app_2:
     G gl gl',
    (guard_conj_evals_to G gl false guard_conj_evals_to G gl true)
    guard_conj_evals_to G gl' false
    guard_conj_evals_to G (gl ++ gl') false.
  Proof.
    intros G gl. induction gl ; intros gl' Hgl Hgl'.
    × simpl. auto.
    × unfold guard_conj_evals_to. unfold guard_conj_evals_to in Hgl.
      destruct a as (b, π). simpl in ×.
      destruct (GuardMap.find π G) as [ v | ] ; simpl in ×.
      + destruct v ; destruct b ; simpl ; auto ; apply IHgl ; auto.
      + destruct Hgl as [ Hgl | Hgl ] ; inversion Hgl.
  Qed.

  Property guard_conj_prop:
     gl G,
    guard_conj_evals_to G gl true
     Forall (λ bg, let '(b, g) := bg in GuardMap.find g G = Some b) gl.
  Proof.
    intros gl G. split.
    × intro H. apply Forall_forall. intros (b, g) HIn. induction gl.
      + inversion HIn.
      + inversion HIn.
        - clear HIn. subst. unfold guard_conj_evals_to in H. simpl in H.
          destruct (GuardMap.find g G).
          { simpl in H. destruct b0 ; destruct b ; simpl in H ; inversion H ; auto. }
          { simpl in H. inversion H. }
        - apply IHgl ; auto. apply (guard_conj_evals_to_true_cons_inv _ a). auto.
    × intro H. induction gl.
      + unfold guard_conj_evals_to. simpl. auto.
      + unfold guard_conj_evals_to. simpl.
        destruct a as (b, π). inversion H. subst. rewrite H2. simpl.
        rewrite eqb_reflx. apply IHgl. auto.
  Qed.

  Lemma C_false_noop:
     c S G gl π o, guard_conj_evals_to G gl false
    big_step_g S G (CI gl π c o) S G.
  Proof.
    intro c. induction c ; intros S G gl π o Hgl ; simpl ; eauto.
    × destruct c ; destruct o ; simpl ; eauto.
    × apply (j_gseq _ _ _ S G) ; auto.
      apply j_gwhile_false. simpl. apply Forall_cons ; auto.
      apply guard_conj_evals_to_false_app_1. auto.
    × apply (j_gseq S G _ S G _ S G) ; auto.
      apply (j_gseq S G _ S G _ S G) ; auto.
      + apply (IHc1 S G _). apply guard_conj_evals_to_false_app_1. auto.
      + apply (IHc2 S G _). apply guard_conj_evals_to_false_app_1. auto.
  Qed.

  Proposition guard_conservation_helper:
     G G' π gl,
    Forall (λ bg, let '(_, g) := bg in ¬ path_suffix g π) gl
    guard_conj_evals_to G gl true
    ( g, (¬ path_suffix g π) GuardMap.find g G' = GuardMap.find g G)
    guard_conj_evals_to G' gl true.
  Proof.
    intros G G' π gl Hgl H'gl HG'.
    apply guard_conj_prop. rewrite guard_conj_prop in H'gl.
    rewrite Forall_forall in ×.
    intros (b, g) Hbg.
    rewrite (HG' g).
    × pose proof (H'gl (b, g) Hbg) as H. simpl in H. auto.
    × pose proof (Hgl (b, g) Hbg) as H. simpl in H. auto.
  Qed.

  Property path_suffix_helper:
     (gl : guard_conj) π π',
    Forall (λ bg, let '(b, g) := bg in ¬ path_suffix g π) gl
    path_suffix π' π
    Forall (λ bg, let '(b, g) := bg in ¬ path_suffix g π') gl.
  Proof.
    intros gl π π' Hgl Hπ'π.
    apply Forall_forall. intros (b, g) bgIngl. simpl.
    rewrite Forall_forall in Hgl.
    pose proof (Hgl (b, g) bgIngl). simpl in H. intro H'. apply H.
    induction Hπ'π ; auto.
  Qed.

  Definition gstore_included (s s' : gstore) :=
     g b, GuardMap.MapsTo g b s GuardMap.MapsTo g b s'.

  Lemma guard_conj_evals_to_gstore_inclusion_1:
     G G' gl b, guard_conj_evals_to G gl b
    ( b π, In (b, π) gl
       b', GuardMap.MapsTo π b' G GuardMap.MapsTo π b' G')
    guard_conj_evals_to G' gl b.
  Proof.
    intros G G' gl. induction gl ; intros B Hgl HGG'.
    × destruct B ; unfold guard_conj_evals_to in × ; simpl in × ; auto.
    × destruct a as (b, π). unfold guard_conj_evals_to. simpl.
      unfold guard_conj_evals_to in Hgl, IHgl. simpl in Hgl.
      remember (GuardMap.find π G) as ov eqn:Hov.
      destruct ov as [ v | ].
      + symmetry in Hov. rewrite <- GuardMapFacts.find_mapsto_iff in Hov.
        pose proof (λ h, HGG' b π h v Hov) as H. rewrite GuardMapFacts.find_mapsto_iff in H.
        rewrite H ; [ | intuition ]. clear H.
        simpl. simpl in Hgl. destruct v ; destruct b ; simpl in × ; auto ;
        apply IHgl ; auto ; intros b' π' Hb'π' ; apply (HGG' b' π') ; auto.
      + simpl in Hgl. inversion Hgl.
  Qed.

  Lemma guard_conj_evals_to_gstore_inclusion_2:
     G G' gl b, guard_conj_evals_to G gl b
    ( b π, In (b, π) gl GuardMap.find π G' = GuardMap.find π G)
    guard_conj_evals_to G' gl b.
  Proof.
    intros G G' gl B Hgl HGG'.
    apply (guard_conj_evals_to_gstore_inclusion_1 G G' gl B) ; auto.
    intros b π Hbπ b' Hb'.
    rewrite GuardMapFacts.find_mapsto_iff in ×. rewrite <- Hb'. apply (HGG' b π) ; auto.
  Qed.

  Lemma guard_conj_evals_to_gstore_inclusion_3:
     G G' gl b, guard_conj_evals_to G gl b
    gstore_included G G'
    guard_conj_evals_to G' gl b.
  Proof.
    intros G G' gl B Hgl HGG'.
    apply (guard_conj_evals_to_gstore_inclusion_1 G G' gl B) ; auto.
  Qed.

  Lemma break_helper:
     G G' gl π πl,
    guard_conj_evals_to G gl true
    In (true, πl) gl
    Forall (λ bg, let '(_, g) := bg in ¬path_suffix g π) gl
    ( g, ¬path_suffix g π g πl GuardMap.find g G' = GuardMap.find g G)
    GuardMap.find πl G' = Some false
    guard_conj_evals_to G' gl false.
  Proof.
    intros G G' gl π πl H₁ H₂ Hgl H₃ Hπl.
    assert ( l₁ l₂, l₁ ++ ((true, πl)::l₂) = gl Forall (λ bg, let '(_, g) := bg in g πl ¬path_suffix g π) l₁) as H.
    { assert (¬ In (false, πl) gl) as H.
      { intro Hfalse. rewrite guard_conj_prop in H₁. rewrite Forall_forall in H₁.
        pose proof (H₁ (true, πl) H₂) as Htrue.
        pose proof (H₁ (false, πl) Hfalse) as Hfalse'.
        simpl in ×. rewrite Hfalse' in Htrue. inversion Htrue. }
      clear H₃ Hπl H₁ G G'.
      induction gl.
      × inversion H₂.
      × destruct a as (b, π'). destruct b ; destruct (eq_guard_dec π' πl).
        + subst. [], gl. intuition.
        + destruct IHgl as (l₁, (l₂, Hl₁l₂)) ; auto.
          { inversion H₂ ; auto. exfalso. inversion H0. apply n. subst. auto. }
          { inversion Hgl ; auto. }
          { intro Hfalse. apply H. right. auto. }
           ((true, π')::l₁), l₂. split ; simpl.
          - destruct Hl₁l₂ as (Hl₁l₂, Hl₁). rewrite Hl₁l₂. auto.
          - destruct Hl₁l₂ as (Hl₁l₂, Hl₁). apply Forall_cons ; auto.
            split ; auto.
            inversion Hgl ; auto.
        + subst. exfalso. apply H. left. auto.
        + destruct IHgl as (l₁, (l₂, Hl₁l₂)) ; auto.
          { inversion H₂ ; auto. exfalso. inversion H0. }
          { inversion Hgl ; auto. }
          { intro Hfalse. apply H. right. auto. }
           ((false, π')::l₁), l₂. split ; simpl.
          - destruct Hl₁l₂ as (Hl₁l₂, Hl₁). rewrite Hl₁l₂. auto.
          - destruct Hl₁l₂ as (Hl₁l₂, Hl₁). apply Forall_cons ; auto.
            split ; auto.
            inversion Hgl ; auto. }
    destruct H as (l₁, (l₂, (Hglsubst, Hl₁))). subst gl.
    apply guard_conj_evals_to_false_app_2.
    × right. destruct (guard_conj_evals_to_true_app_inv G _ _ H₁) as (Hl₁', _) ; auto.
      apply (guard_conj_evals_to_gstore_inclusion_2 G) ; auto.
      intros b g Hg. apply H₃. split.
      + intro Hfalse. rewrite Forall_forall in Hl₁. destruct (Hl₁ (b, g) Hg) as (_, H).
        apply H. auto.
      + rewrite Forall_forall in Hl₁. apply (Hl₁ (b, g)). auto.
    × unfold guard_conj_evals_to. simpl. rewrite Hπl. simpl. auto.
  Qed.

  Lemma continue_helper:
     G G' gl π πl,
    guard_conj_evals_to G gl true
    In (true, S1 πl) gl
    Forall (λ bg, let '(_, g) := bg in ¬path_suffix g π) gl
    ( g, ¬path_suffix g π g S1 πl GuardMap.find g G' = GuardMap.find g G)
    GuardMap.find (S1 πl) G' = Some false
    guard_conj_evals_to G' gl false.
  Proof.
    intros G G' gl π πl H₁ H₂ Hgl H₃ Hπl.
    apply (break_helper G G' gl π (S1 πl)) ; auto.
  Qed.

  Lemma CI_sound:
     S S' c m, big_step S c m S' (gl : guard_conj) π o G,
    (m MNormal πl, o = Some πl)
    Forall (λ bg, let '(b, g) := bg in ¬ path_suffix g π) gl
    ( πl, o = Some πl In (true, πl) gl In (true, S1 πl) gl)
    guard_conj_evals_to G gl true G',
    big_step_g S G (CI gl π c o) S' G'
    (m = MNormal
       (g : guard), (¬ path_suffix g π)
      GuardMap.find g G' = GuardMap.find g G)
    (m = MBreak
       πl, o = Some πl loop_broken G' πl (g : guard),
      (¬ path_suffix g π) g πl
      GuardMap.find g G' = GuardMap.find g G)
    (m = MContinue
       πl, o = Some πl loop_continued G' πl (g : guard),
      (¬ path_suffix g π) g S1 πl
      GuardMap.find g G' = GuardMap.find g G).
  Proof.
    intros S S' c m HStep. induction HStep ;
    intros gl π o G Hspecial Hgl Hoπ H'gl ; simpl.
    × G. repeat split ; auto.
      + apply (j_gassign _ _ v) ; auto.
      + intro Hfalse. inversion Hfalse.
      + intro Hfalse. inversion Hfalse.
    × G. repeat split ; auto.
      + intro Hfalse. inversion Hfalse.
      + intro Hfalse. inversion Hfalse.
    × destruct (IHHStep1 gl (S0 π) o G) as (G₁, H₁) ; auto.
      { rewrite Forall_forall in ×. intros (b, g) Hbg. intro Hfalse.
        apply (Hgl (b, g) Hbg).
        apply path_suffix_inv_S0 in Hfalse. auto. }
      destruct (IHHStep2 gl (S1 π) o G₁) as (G', H₂) ; auto.
      { rewrite Forall_forall in ×. intros (b, g) Hbg. intro Hfalse.
        apply (Hgl (b, g) Hbg).
        apply path_suffix_inv_S1 in Hfalse. auto. }
      { apply (guard_conservation_helper G _ π) ; auto.
        destruct H₁ as (_, (H₁, _)).
        intros g Hg. apply H₁ ; auto. }
       G'. simpl in ×. repeat split ; auto.
      + intuition (eauto).
      + intros Hrefl g Hg. destruct H₁ as (_, (H₁, _)), H₂ as (_, (H₂, _)).
        rewrite (H₂ Hrefl g), (H₁ eq_refl g) ; auto.
      + intro Hbreak. destruct H₂ as (_, (_, (H₂, _))).
        destruct (H₂ Hbreak) asl, H). clear H₂.
         πl. split ; [ | split ] ; try (intuition ; fail).
        intros g Hg.
        destruct H as (_, (_, H)).
        rewrite H ; auto ; [ | intuition].
        destruct H₁ as (_, (H₁, _)).
        apply H₁ ; intuition.
      + intro Hcontinue. destruct H₂ as (_, (_, (_, H₂))).
        destruct (H₂ Hcontinue) asl, H). clear H₂.
         πl. repeat split ; try (intuition ; fail).
        intros g Hg.
        destruct H as (_, (_, H)).
        rewrite H ; auto ; [ | intuition].
        destruct H₁ as (_, (H₁, _)).
        apply H₁ ; intuition.
    × pose (GuardMap.add π true G) as G₀.
      destruct (IHHStep (gl ++ [(true, π)]) (S1 π) o G₀) as (G', H') ; auto.
      { apply Forall_app ; auto.
        rewrite Forall_forall in ×. intros (b', g) Hb'g. intro Hfalse.
        apply (Hgl (b', g) Hb'g).
        apply path_suffix_inv_S1 in Hfalse. auto. }
      { intros πl Hπl. split.
        + apply in_or_app. left. apply Hoπ. auto.
        + apply in_or_app. left. apply Hoπ. auto. }
      { subst G₀. apply guard_conj_evals_to_true_app ; auto.
        + apply (guard_conservation_helper G _ π) ; auto.
          intros g Hg. rewrite GuardMapFacts.add_neq_o ; auto.
          intro Hfalse. subst. apply Hg. auto.
        + unfold guard_conj_evals_to. simpl.
          rewrite GuardMapFacts.add_eq_o ; auto. }
       G'. repeat split.
      + apply (j_gseq s G _ s G₀).
        - apply j_ggassign ; auto.
        - destruct m.
          { apply (j_gseq _ _ _ s' G') ; try (intuition ; fail).
            apply C_false_noop.
            apply guard_conj_evals_to_false_app_2.
            - right. apply (guard_conservation_helper G₀ _ π) ; intuition.
              apply (guard_conservation_helper G _ π) ; auto.
              intros g Hg. subst G₀. rewrite GuardMapFacts.add_neq_o ; auto.
              intro Hfalse. subst. apply Hg. auto.
            - unfold guard_conj_evals_to. simpl.
              destruct H' as (_, (H', _)). rewrite H' ; auto.
              subst G₀. rewrite GuardMapFacts.add_eq_o ; auto. }
          { apply (j_gseq _ _ _ s' G') ; auto.
            + intuition.
            + apply C_false_noop.
              destruct H' as (H', (_, ((πl, (Hoπl, (Hbroken, H''))), _))) ; auto.
              apply (guard_conj_evals_to_false_app_1 G' gl _) ; auto.
              apply (break_helper G₀ G' gl π πl) ; auto.
              - apply (guard_conservation_helper G _ π) ; auto.
                intros g Hg. subst G₀. rewrite GuardMapFacts.add_neq_o ; auto.
                intro Hfalse. apply Hg. subst. auto.
              - apply Hoπ. auto.
              - intros g Hg. apply H''. destruct Hg as (H₁, H₂). split ; auto. }
          { apply (j_gseq _ _ _ s' G') ; auto.
            + intuition.
            + apply C_false_noop.
              destruct H' as (H', (_, (_, (πl, (Hoπl, (Hcontinued, H'')))))) ; auto.
              apply (guard_conj_evals_to_false_app_1) ; auto.
              apply (continue_helper G₀ G' gl π πl) ; auto.
              - apply (guard_conservation_helper G _ π) ; auto.
                intros g Hg. subst G₀. rewrite GuardMapFacts.add_neq_o ; auto.
                intro Hfalse. apply Hg. subst. auto.
              - apply Hoπ. auto.
              - intros g Hg. apply H''. destruct Hg as (H₁, H₂). split ; auto. }
      + intros Hm g Hg.
        destruct m.
        - destruct H' as (_, (H', _)).
          rewrite (H' Hm g) ; simpl ; auto.
          subst G₀. apply GuardMapFacts.add_neq_o.
          intro Hfalse. subst π. intuition.
        - inversion Hm.
        - inversion Hm.
      + destruct H' as (_, (_, (H'', _))). intro Hbreak.
        destruct (H'' Hbreak) asl, (H₁, (H₂, H₃))).
         πl. split ; [ | split ] ; auto.
        subst G₀. pose proof (Hoπ πl H₁) as Hπl.
        intros g (Hg₁, Hg₂). rewrite <- ((GuardMapFacts.add_neq_o G) π _ true).
        - apply H₃. auto.
        - intro Hfalse. subst. apply Hg₁. auto.
      + destruct H' as (_, (_, (_, H''))). intro Hcontinue.
        destruct (H'' Hcontinue) asl, (H₁, (H₂, H₃))).
         πl. split ; [ | split ] ; auto.
        subst G₀. pose proof (Hoπ πl H₁) as Hπl.
        intros g (Hg₁, Hg₂). rewrite <- ((GuardMapFacts.add_neq_o G) π _ true).
        - apply H₃. auto.
        - intro Hfalse. subst. apply Hg₁. auto.
    × pose (GuardMap.add π false G) as G₀.
      destruct (IHHStep (gl ++ [(false, π)]) (S0 π) o G₀) as (G', H') ; auto.
      { apply Forall_app ; auto.
        rewrite Forall_forall in ×. intros (b', g) Hb'g. intro Hfalse.
        apply (Hgl (b', g) Hb'g).
        apply path_suffix_inv_S0 in Hfalse. auto. }
      { intros πl Hπl. split ; apply in_or_app ; left ; apply Hoπ ; auto. }
      { subst G₀. apply guard_conj_evals_to_true_app ; auto.
        + apply (guard_conservation_helper G _ π) ; auto.
          intros g Hg. rewrite GuardMapFacts.add_neq_o ; auto.
          intro Hfalse. subst. apply Hg. auto.
        + unfold guard_conj_evals_to. simpl.
          rewrite GuardMapFacts.add_eq_o ; auto. }
       G'. repeat split.
      + apply (j_gseq s G _ s G₀).
        - apply j_ggassign ; auto.
        - apply (j_gseq _ _ _ s G₀) ; try (intuition ; fail).
          apply C_false_noop.
          apply guard_conj_evals_to_false_app_2.
          { right. apply (guard_conservation_helper G₀ _ π) ; intuition.
            apply (guard_conservation_helper G _ π) ; auto.
            intros g Hg. subst G₀. rewrite GuardMapFacts.add_neq_o ; auto.
            intro Hfalse. subst. apply Hg. auto. }
          unfold guard_conj_evals_to. simpl.
          subst G₀. rewrite GuardMapFacts.add_eq_o ; auto.
      + intros Hm g Hg. destruct H' as (_, (H', _)).
        rewrite (H' Hm g) ; simpl ; auto.
        subst G₀. apply GuardMapFacts.add_neq_o.
        intro Hfalse. subst π. intuition.
      + destruct H' as (_, (_, (H'', _))). intro Hbreak.
        destruct (H'' Hbreak) asl, (H₁, (H₂, H₃))).
         πl. split ; [ | split ] ; auto.
        subst G₀.
        intros g (Hg₁, Hg₂). rewrite <- ((GuardMapFacts.add_neq_o G) π _ false).
        - apply H₃. auto.
        - intro Hfalse. subst. apply Hg₁. auto.
      + destruct H' as (_, (_, (_, H''))). intro Hcontinue.
        destruct (H'' Hcontinue) asl, (H₁, (H₂, H₃))).
         πl. split ; [ | split ] ; auto.
        subst G₀.
        intros g (Hg₁, Hg₂). rewrite <- ((GuardMapFacts.add_neq_o G) π _ false).
        - apply H₃. auto.
        - intro Hfalse. subst. apply Hg₁. auto.
    ×
       (GuardMap.add π false G).
      repeat split.
      + apply (j_gseq s G _ s (GuardMap.add π false G)).
        - apply j_ggassign ; auto.
        - apply j_gwhile_false. simpl. apply Forall_cons ; auto.
          apply guard_conj_evals_to_false_app_2 ; auto.
          { right. apply (guard_conservation_helper G _ π) ; intuition.
            rewrite GuardMapFacts.add_neq_o ; auto.
            intro Hfalse. subst. apply H0. auto. }
          unfold guard_conj_evals_to. simpl.
          rewrite GuardMapFacts.add_eq_o ; auto.
      + intros Hm g Hg. apply GuardMapFacts.add_neq_o.
        intro Hfalse. subst π. intuition.
      + intro Hfalse. inversion Hfalse.
      + intro Hfalse. inversion Hfalse.
    × pose (GuardMap.add π true G) as G₀.
      pose (GuardMap.add (S1 π) true G₀) as G₀'.
      destruct (IHHStep1 (gl ++ [(true, π)] ++ [(true, S1 π)]) (S1 (S1 π)) (Some π) G₀') as (G₁, H₁).
      { intro Hspecial'. π. auto. }
      { apply Forall_app ; auto ;
        rewrite Forall_forall in × ; intros (b', g) Hb'g ; intro Hfalse.
        apply (Hgl (b', g) Hb'g).
        apply path_suffix_inv_S1 in Hfalse. auto.
        inversion Hb'g.
        + inversion H1. subst. apply (S1g_not_suffix_g g). auto.
        + simpl in H1. destruct H1 ; [ | auto ].
          inversion H1. subst. apply (S1g_not_suffix_g (S1 π)). auto. }
      { intros πl Hπl. inversion Hπl. subst πl.
        split ; apply in_or_app ; right ; simpl ; auto. }
      { subst G₀' G₀. apply guard_conj_evals_to_true_app ; auto.
        + apply (guard_conservation_helper G _ π) ; auto.
          intros g Hg. repeat rewrite GuardMapFacts.add_neq_o ; auto.
          - intro Hfalse. subst. apply Hg. auto.
          - intro Hfalse. subst. apply Hg. auto.
        + unfold guard_conj_evals_to. simpl.
          rewrite GuardMapFacts.add_neq_o ; auto.
          - rewrite GuardMapFacts.add_eq_o ; auto.
            simpl. rewrite GuardMapFacts.add_eq_o ; auto.
          - intro Hfalse. apply (S1g_not_suffix_g π). rewrite Hfalse. auto. }
      destruct (IHHStep2 gl π o G₁) as (G', H') ; auto.
      { apply (guard_conservation_helper G₀' _ π) ; auto.
        + apply (guard_conservation_helper G₀ _ π) ; auto.
          - apply (guard_conservation_helper G _ π) ; auto.
            intros g Hg. subst G₀. rewrite GuardMapFacts.add_neq_o ; auto.
            intro Hfalse. subst g. apply Hg. auto.
          - intros g Hg. subst G₀'. rewrite GuardMapFacts.add_neq_o ; auto.
            intro Hfalse. subst g. apply Hg. auto.
        + destruct m.
          - destruct H₁ as (_, (H₁, _)).
            intros g Hg. apply H₁ ; auto.
          - destruct H₁ as (_, (_, (H₁, _))).
            intros g Hg. destruct H₁ asl, (H₁, (H₁', H₁''))) ; auto.
          - destruct H₁ as (_, (_, (_, H₁))).
            intros g Hg. destruct H₁ asl, (H₁, (H₁', H₁''))) ; auto.
            apply H₁''. intuition. subst g. apply Hg. inversion H₁. subst πl. auto. }
       G'. simpl in H'.
      destruct H' as (H', H'').
      inversion H' as [ | | | | S_ G_ c₁_ S₁' G₁' c₂_ S'_ G'_ H₂ H₃ | | | ].
      subst S_ G_ c₁_ c₂_ S'_ G'_.
      repeat split.
      + apply (j_gseq _ _ _ s G₀).
        { apply j_ggassign ; auto. }
        apply (j_gwhile_true _ _ S₁' G₁') ; auto.
        { apply Exists_cons. left.
          apply guard_conj_evals_to_true_app ; auto.
          + apply (guard_conservation_helper G _ π) ; auto.
            intros g Hg. subst G₀.
            rewrite GuardMapFacts.add_neq_o ; auto.
            intro Hfalse. apply Hg. subst g. auto.
          + subst G₀. unfold guard_conj_evals_to. simpl.
            rewrite GuardMapFacts.add_eq_o ; auto. }
        - apply (j_gseq _ _ _ s G₀') ; auto.
          { apply j_ggassign ; auto.
            apply guard_conj_evals_to_true_app.
            + apply (guard_conservation_helper G _ π) ; auto.
              intros g Hg. subst G₀. rewrite GuardMapFacts.add_neq_o ; auto.
              intro Hfalse. apply Hg. subst g. auto.
            + unfold guard_conj_evals_to. subst G₀. simpl.
              rewrite GuardMapFacts.add_eq_o ; auto. }
          apply (j_gseq _ _ _ s₁ G₁) ; auto.
          { intuition. }
          inversion H₂ as [ a_ s₁_ G₁_ gl_ H''gl | | g_ b_ v s₁_ G₁_ gl_ | | | | | ] ; [ subst a_ | subst g_ b_ ] ;
          subst s₁_ G₁_ gl_ s₁.
          { apply j_gatomic_false. apply guard_conj_evals_to_false_app_1 ; auto. }
          apply j_ggassign ; auto.
          apply guard_conj_evals_to_true_app ; auto.
          unfold guard_conj_evals_to. simpl.
          destruct m.
          { destruct H₁ as (_, (H₁, _)).
            rewrite H₁ ; auto.
            + subst G₀'. rewrite GuardMapFacts.add_neq_o ; auto.
              - subst G₀. rewrite GuardMapFacts.add_eq_o ; auto.
              - intros Hfalse. apply (S1g_not_suffix_g π). rewrite Hfalse. auto.
            + intro Hfalse. apply (S1g_not_suffix_g π) ; auto. }
          { exfalso. apply H0. auto. }
          { destruct H₁ as (_, (_, (_, H₁))).
            destruct (H₁ eq_refl) asl, (Hππl, (Hcontinued, H₁'))).
            rewrite H₁' ; auto.
            + subst G₀'. rewrite GuardMapFacts.add_neq_o ; auto.
              - subst G₀. rewrite GuardMapFacts.add_eq_o ; auto.
              - intros Hfalse. apply (S1g_not_suffix_g π). rewrite Hfalse. auto.
            + split.
              - intro Hfalse. apply (S1g_not_suffix_g π) ; auto.
              - inversion Hππl. subst πl. intro Hfalse. apply (S1g_not_suffix_g π) ; auto.
                rewrite <- Hfalse. auto. }
      + intros Hnormal g Hg.
        destruct m.
        - destruct H'' as (H'', _), H₁ as (_, (H₁, _)).
          rewrite (H'' Hnormal), H₁ ; simpl ; auto.
          subst G₀'. rewrite GuardMapFacts.add_neq_o.
          { subst G₀. apply GuardMapFacts.add_neq_o.
            intro Hfalse. subst π. intuition. }
          { intro Hfalse. apply Hg. subst g. auto. }
        - exfalso. apply H0. auto.
        - destruct H'' as (H'', _), H₁ as (_, (_, (_, H₁))).
          destruct H₁ asl, (Hππl, (Hcontinued, H₁))) ; auto.
          rewrite (H'' Hnormal), H₁ ; simpl ; auto.
          { subst G₀'. rewrite GuardMapFacts.add_neq_o.
            + subst G₀. apply GuardMapFacts.add_neq_o.
              intro Hfalse. subst π. intuition.
            + intro Hfalse. apply Hg. subst g. auto. }
          { split ; auto. inversion Hππl. subst πl.
            intro Hfalse. subst g. apply Hg. auto. }
      + intro Hfalse. inversion Hfalse.
      + intro Hfalse. inversion Hfalse.
    × destruct (IHHStep gl (S0 π) o G) as (G₁, (H₁, (_, (H₁', H₁'')))) ; auto.
      { rewrite Forall_forall in ×.
        intros (b', g) Hb'g. intro Hfalse.
        apply (Hgl (b', g) Hb'g).
        apply path_suffix_inv_S0 in Hfalse. auto. }
      clear IHHStep.
       G₁. simpl in ×. repeat split ; auto.
      + apply (j_gseq _ _ _ s' G₁) ; auto.
        destruct m.
        - exfalso. apply H. auto.
        - apply C_false_noop.
          destruct H₁' asl, (Ho, Hπl)) ; auto.
          subst o.
          destruct Hπl as (Hbroken, Hπl) ; auto.
          apply (break_helper G G₁ gl π πl) ; auto.
          { apply (Hoπ πl) ; auto. }
          intros g Hg. apply Hπl.
          destruct Hg as (Hg, Hg'). split ; auto.
        - apply C_false_noop.
          destruct H₁'' asl, (Ho, Hπl)) ; auto.
          apply (continue_helper G G₁ gl π πl) ; auto.
          { apply (Hoπ πl) ; auto. }
          { intros g Hg. apply Hπl. destruct Hg as (Hg, Hg'). split ; auto. }
          unfold loop_continued in ×. intuition.
      + intro Hnormal. exfalso. apply H. auto.
      + intros Hbreak. subst. destruct H₁' asl, H₁') ; auto.
          πl. intuition.
      + intros Hcontinue. subst. destruct H₁'' asl, H₁'') ; auto.
          πl. intuition.
    × pose (GuardMap.add π true G) as G₀.
      pose (GuardMap.add (S1 π) true G₀) as G₀'.
      destruct (IHHStep (gl ++ [(true, π)] ++ [(true, S1 π)]) (S1 (S1 π)) (Some π) G₀') as (G₁, (H₁, (H₁', H₁''))) ; auto.
      { intros _. π. auto. }
      { apply Forall_app ; auto ;
        rewrite Forall_forall in × ; intros (b', g) Hb'g Hfalse.
        apply (Hgl (b', g) Hb'g).
        apply path_suffix_inv_S1 in Hfalse. auto.
        inversion Hb'g ; auto.
        + inversion H0. subst. apply (S1g_not_suffix_g g) ; auto.
        + simpl in H0. destruct H0 ; auto. inversion H0. subst. apply (S1g_not_suffix_g (S1 π)) ; auto. }
      { intros πl Hπl. inversion Hπl. subst. split ;
        repeat (apply in_or_app ; right ; simpl ; auto). }
      { subst G₀'. apply guard_conj_evals_to_true_app ; auto.
        + apply (guard_conservation_helper G₀ _ π) ; auto.
          - subst G₀. apply (guard_conservation_helper G _ π) ; auto.
            intros g Hg. rewrite GuardMapFacts.add_neq_o ; auto.
            intro Hfalse. subst. apply Hg. auto.
          - intros g Hg. rewrite GuardMapFacts.add_neq_o ; auto.
            intro Hfalse. subst. apply Hg. auto.
        + unfold guard_conj_evals_to. simpl.
          rewrite GuardMapFacts.add_neq_o ; auto.
          - subst G₀. rewrite GuardMapFacts.add_eq_o ; auto.
            simpl. rewrite GuardMapFacts.add_eq_o ; auto.
          - intro Hfalse. apply (S1g_not_suffix_g π). rewrite Hfalse. auto. }
      destruct H₁'' as ((πl, (Hπl, Hbroken)), _) ; auto.
      unfold loop_broken in ×. inversion Hπl ; clear Hπl ; subst πl.
       G₁. simpl in ×. repeat split ; auto.
      + apply (j_gseq _ _ _ s G₀) ; auto.
        { subst G₀. apply j_ggassign ; auto. }
        apply (j_gwhile_true _ _ s₁ G₁) ; auto.
        { apply Exists_cons. left.
          apply guard_conj_evals_to_true_app ; auto.
          + apply (guard_conservation_helper G _ π) ; auto.
            intros g Hg. subst G₀. rewrite GuardMapFacts.add_neq_o ; auto.
            intro Hfalse. apply Hg. subst g. auto.
          + unfold guard_conj_evals_to. subst G₀. simpl.
            rewrite GuardMapFacts.add_eq_o ; auto. }
        { apply (j_gseq _ _ _ s G₀') ; auto.
          { apply j_ggassign ; auto. apply guard_conj_evals_to_true_app.
            + apply (guard_conservation_helper G _ π) ; auto.
              intros g Hg. subst G₀. rewrite GuardMapFacts.add_neq_o ; auto.
              intros Hfalse. apply Hg. subst g. auto.
            + unfold guard_conj_evals_to. subst G₀. simpl.
              rewrite GuardMapFacts.add_eq_o ; auto. }
          apply (j_gseq _ _ _ s₁ G₁) ; auto.
          apply j_gatomic_false.
          apply guard_conj_evals_to_false_app_2.
          + right. apply (guard_conservation_helper G₀' _ π) ; auto.
            - apply (guard_conservation_helper G₀ _ π) ; auto.
              { apply (guard_conservation_helper G _ π) ; auto.
                intros g Hg. subst G₀. rewrite GuardMapFacts.add_neq_o ; auto.
                intros Hfalse. subst g. apply Hg. auto. }
              intros g Hg. subst G₀'. rewrite GuardMapFacts.add_neq_o ; auto.
              intro Hfalse. subst g. apply Hg. auto.
            - intros g Hg. apply Hbroken. intuition. subst. apply Hg. auto.
          + unfold guard_conj_evals_to. simpl.
            destruct Hbroken as (Hbroken, _).
            rewrite Hbroken ; auto. }
        apply j_gwhile_false.
        apply Forall_cons ; auto.
        apply guard_conj_evals_to_false_app_2.
        - right. apply (guard_conservation_helper G₀' _ π) ; auto.
          { apply (guard_conservation_helper G₀ _ π) ; auto.
            { apply (guard_conservation_helper G _ π) ; auto.
              intros g Hg. subst G₀. rewrite GuardMapFacts.add_neq_o ; auto.
              intros Hfalse. subst g. apply Hg. auto. }
            intros g Hg. subst G₀'. rewrite GuardMapFacts.add_neq_o ; auto.
            intro Hfalse. subst g. apply Hg. auto. }
          { intros g Hg. apply Hbroken. intuition. subst. apply Hg. auto. }
        - unfold guard_conj_evals_to. simpl.
          destruct Hbroken as (Hbroken, _).
          rewrite Hbroken ; auto.
      + intros Hnormal g Hg.
        destruct Hbroken as (_, Hbroken).
        rewrite (Hbroken g) ; auto. subst G₀' G₀.
        - repeat rewrite GuardMapFacts.add_neq_o ; auto ;
          intro Hfalse ; subst g ; apply Hg ; auto.
        - intuition. subst g. apply Hg. auto.
      + discriminate.
      + discriminate.
    × destruct Hspecial asl, Hsubst) ; auto.
      { discriminate. }
       (GuardMap.add πl false G). subst o.
      repeat split ; auto.
      + discriminate.
      + intros _. πl. split ; [ | split ] ; auto.
         { unfold loop_broken. apply GuardMapFacts.add_eq_o ; auto. }
         intros g Hg. rewrite GuardMapFacts.add_neq_o ; auto.
         intro Hfalse. subst. destruct Hg as (Hg, Hg').
         apply Hg'. auto.
     + discriminate.
    × destruct Hspecial asl, Hsubst) ; auto.
      { discriminate. }
       (GuardMap.add (S1 πl) false G). subst o.
      repeat split ; auto.
      + discriminate.
      + discriminate.
      + intros _. πl. repeat split ; auto.
        { unfold loop_continued. apply GuardMapFacts.add_eq_o ; auto. }
        intros g Hg. rewrite GuardMapFacts.add_neq_o ; auto.
        intro Hfalse. subst. destruct Hg as (Hg, Hg').
        apply Hg'. auto.
  Qed.

  Definition to_gl π c :=
    CI [] π c None.

  Lemma to_gl_sound:
     S S' c, big_step S c MNormal S' G π, G',
    big_step_g S G (to_gl π c) S' G'.
  Proof.
    unfold to_gl.
    intros S S' c Hstep G π.
    destruct (CI_sound S S' c MNormal Hstep [] π None G) as (G', (H, H')) ; auto.
    { intro Hfalse. exfalso. apply Hfalse. auto. }
    { intros πl Hfalse. inversion Hfalse. }
    { unfold guard_conj_evals_to. simpl. auto. }
     G'. auto.
  Qed.

  Fixpoint simplify_diff cd :=
    match cd with
    | LeafSubst Skip aSeqInsL (Leaf a) (LeafSubst Skip Skip)
    | LeafSubst a SkipSeqDelL (Leaf a) (LeafSubst Skip Skip)
    | LeafSubst a a'LeafSubst a a'
    | SeqMut cd cd'SeqMut (simplify_diff cd) (simplify_diff cd')
    | SeqDelR cd cSeqMut (simplify_diff cd) (SeqDelL c (LeafSubst Skip Skip))
    | SeqInsR cd cSeqMut (simplify_diff cd) (SeqInsL c (LeafSubst Skip Skip))
    | SeqDelL c cdSeqDelL c (simplify_diff cd)
    | SeqInsL c cdSeqInsL c (simplify_diff cd)
    | IfMut (b, b') cd cd'IfMut (b, b') (simplify_diff cd) (simplify_diff cd')
    | WhileMut (b, b') cdWhileMut (b, b') (simplify_diff cd)
    | WhileAdd b cdWhileAdd b (simplify_diff cd)
    | WhileDel b cdWhileDel b (simplify_diff cd)
    | ITEAddIf b c cdITEAddIf b c (simplify_diff cd)
    | ITEAddElse b cd cITEAddElse b (simplify_diff cd) c
    | ITEDelIf b c cdITEDelIf b c (simplify_diff cd)
    | ITEDelElse b cd cITEDelElse b (simplify_diff cd) c
    | CPoint cdCPoint (simplify_diff cd)
    end.

  Fixpoint is_simple_diff cd : bool :=
    match cd with
    | SeqMut cd cd' | IfMut _ cd cd'andb (is_simple_diff cd) (is_simple_diff cd')
    | SeqDelL _ cd | SeqInsL _ cd | WhileAdd _ cd | WhileDel _ cd
    | WhileMut _ cd | ITEAddIf _ _ cd | ITEAddElse _ cd _
    | ITEDelIf _ _ cd | ITEDelElse _ cd _is_simple_diff cd
    | LeafSubst Skip Skiptrue
    | LeafSubst Skip _ | LeafSubst _ Skipfalse
    | LeafSubst _ _true
    | CPoint cdis_simple_diff cd
    | _false
    end.

  Lemma simplify_yields_simple_diff:
     cd, is_simple_diff (simplify_diff cd) = true.
  Proof.
    intro cd. induction cd ;
    try destruct p ; try destruct c ; try destruct c0 ; simpl in × ;
    try (rewrite IHcd || rewrite IHcd1, IHcd2) ; auto.
  Qed.

  Lemma simplify_diff_preserves_semantics:
     cd S S' m,
    (big_step S (Π₀ cd) m S' big_step S (Π₀ (simplify_diff cd)) m S')
     (big_step S (Π₁ cd) m S' big_step S (Π₁ (simplify_diff cd)) m S').
  Proof.
    intro cd. induction cd ; intros S S' m ; split ; simpl in × ; intro Hstep ; auto ;
    try (destruct (IHcd S S' m) ; eauto ; fail) ;
    try (destruct m ; eauto ; apply j_seq_interrupt ; eauto ; discriminate).
    × inversion Hstep as [ | | S_ m_ c_ S₁ c' S'_ | | | | | S_ c_ c' m_ S'_ | | | ] ;
      subst S_ m_ c_ c' S'_ ; clear Hstep.
      + apply (j_seq_normal _ _ _ S₁) ; auto.
        destruct (IHcd S₁ S' m). auto.
      + eauto.
    × inversion Hstep as [ | | S_ m_ c_ S₁ c' S'_ | | | | | S_ c_ c' m_ S'_ | | | ] ;
      subst S_ m_ c_ c' S'_ ; clear Hstep.
      + apply (j_seq_normal _ _ _ S₁) ; auto.
        - destruct (IHcd S S₁ MNormal). auto.
        - destruct m ; eauto ; apply j_seq_interrupt ; auto ; discriminate.
      + apply j_seq_interrupt ; auto.
        destruct (IHcd S S' m). auto.
    × destruct (IHcd S S' m) as (H₁, H₂). destruct m.
      + apply (j_seq_normal _ _ _ S') ; eauto.
      + apply j_seq_interrupt. discriminate. auto.
      + apply j_seq_interrupt. discriminate. auto.
    × inversion Hstep as [ | | S_ m_ c_ S₁ c' S'_ | | | | | S_ c_ c' m_ S'_ | | | ] ;
      subst S_ m_ c_ c' S'_ ; clear Hstep.
      + apply (j_seq_normal _ _ _ S₁) ; auto.
        destruct (IHcd S₁ S' m). auto.
      + eauto.
    × destruct (IHcd S S' m) as (H₁, H₂). destruct m.
      + apply (j_seq_normal _ _ _ S') ; eauto.
      + apply j_seq_interrupt. discriminate. auto.
      + apply j_seq_interrupt. discriminate. auto.
    × inversion Hstep as [ | | S_ m_ c_ S₁ c' S'_ | | | | | S_ c_ c' m_ S'_ | | | ] ;
      subst S_ m_ c_ c' S'_ ; clear Hstep.
      + apply (j_seq_normal _ _ _ S₁) ; auto.
        - destruct (IHcd S S₁ MNormal). auto.
        - destruct m ; eauto ; apply j_seq_interrupt ; auto ; discriminate.
      + apply j_seq_interrupt ; auto.
        destruct (IHcd S S' m). auto.
    × inversion Hstep as [ | | S_ m_ c_ S₁ c' S'_ | | | | | S_ c_ c' m_ S'_ | | | ] ;
      subst S_ m_ c_ c' S'_ ; clear Hstep.
      + apply (j_seq_normal _ _ _ S₁) ; auto.
        - destruct (IHcd1 S S₁ MNormal). auto.
        - destruct (IHcd2 S₁ S' m). auto.
      + apply j_seq_interrupt ; eauto. destruct (IHcd1 S S' m) ; auto.
    × inversion Hstep as [ | | S_ m_ c_ S₁ c' S'_ | | | | | S_ c_ c' m_ S'_ | | | ] ;
      subst S_ m_ c_ c' S'_ ; clear Hstep.
      + apply (j_seq_normal _ _ _ S₁) ; auto.
        - destruct (IHcd1 S S₁ MNormal). auto.
        - destruct (IHcd2 S₁ S' m). auto.
      + apply j_seq_interrupt ; eauto. destruct (IHcd1 S S' m) ; auto.
    × destruct p as (b, b'). simpl.
      inversion Hstep as [ | | | S_ m_ S'_ b_ c_ c' | S_ m_ S'_ b_ c_ c' | | | | | | ] ;
      subst S_ m_ S'_ b_ c_ c' ; clear Hstep.
      + apply j_if_then ; auto. destruct (IHcd1 S S' m) ; auto.
      + apply j_if_else ; auto. destruct (IHcd2 S S' m) ; auto.
    × destruct p as (b, b'). simpl.
      inversion Hstep as [ | | | S_ m_ S'_ b_ c_ c' | S_ m_ S'_ b_ c_ c' | | | | | | ] ;
      subst S_ m_ S'_ b_ c_ c' ; clear Hstep.
      + apply j_if_then ; auto. destruct (IHcd1 S S' m) ; auto.
      + apply j_if_else ; auto. destruct (IHcd2 S S' m) ; auto.
    × destruct p as (b, b').
      remember (While b (Π₀ cd)) as c eqn:Hc.
      induction Hstep as [ | | | | | S b_ c_ | S m S₁ S' b_ c_ | | S S₁ b_ c_ | | ] ;
      inversion Hc ; clear Hc ; subst b_ c_.
      + apply j_while_false ; eauto.
      + simpl. apply (j_while_true _ m S₁) ; eauto.
        destruct (IHcd S S₁ m). auto.
      + simpl. apply (j_while_break _ S₁) ; eauto.
        destruct (IHcd S S₁ MBreak). auto.
    × destruct p as (b, b').
      remember (While b' (Π₁ cd)) as c eqn:Hc.
      induction Hstep as [ | | | | | S b_ c_ | S m S₁ S' b_ c_ | | S S₁ b_ c_ | | ] ;
      inversion Hc ; clear Hc ; subst b_ c_.
      + apply j_while_false ; eauto.
      + simpl. apply (j_while_true _ m S₁) ; eauto.
        destruct (IHcd S S₁ m). auto.
      + simpl. apply (j_while_break _ S₁) ; eauto.
        destruct (IHcd S S₁ MBreak). auto.
    × inversion Hstep as [ | | | S_ m_ S'_ b_ c_ c' | S_ m_ S'_ b_ c_ c' | | | | | | ] ;
      subst S_ m_ S'_ b_ c_ c' ; clear Hstep.
      + apply j_if_then ; auto.
      + apply j_if_else ; auto. destruct (IHcd S S' m) ; auto.
    × inversion Hstep as [ | | | S_ m_ S'_ b_ c_ c' | S_ m_ S'_ b_ c_ c' | | | | | | ] ;
      subst S_ m_ S'_ b_ c_ c' ; clear Hstep.
      + apply j_if_then ; auto. destruct (IHcd S S' m) ; auto.
      + apply j_if_else ; auto.
    × inversion Hstep as [ | | | S_ m_ S'_ b_ c_ c' | S_ m_ S'_ b_ c_ c' | | | | | | ] ;
      subst S_ m_ S'_ b_ c_ c' ; clear Hstep.
      + apply j_if_then ; auto.
      + apply j_if_else ; auto. destruct (IHcd S S' m) ; auto.
    × inversion Hstep as [ | | | S_ m_ S'_ b_ c_ c' | S_ m_ S'_ b_ c_ c' | | | | | | ] ;
      subst S_ m_ S'_ b_ c_ c' ; clear Hstep.
      + apply j_if_then ; auto. destruct (IHcd S S' m) ; auto.
      + apply j_if_else ; auto.
    × remember (While b (Π₁ cd)) as c eqn:Hc.
      induction Hstep as [ | | | | | S b_ c_ | S m S₁ S' b_ c_ | | S S₁ b_ c_ | | ] ;
      inversion Hc ; clear Hc ; subst b_ c_.
      + apply j_while_false ; eauto.
      + simpl. apply (j_while_true _ m S₁) ; eauto.
        destruct (IHcd S S₁ m). auto.
      + simpl. apply (j_while_break _ S₁) ; eauto.
        destruct (IHcd S S₁ MBreak). auto.
    × remember (While b (Π₀ cd)) as c eqn:Hc.
      induction Hstep as [ | | | | | S b_ c_ | S m S₁ S' b_ c_ | | S S₁ b_ c_ | | ] ;
      inversion Hc ; clear Hc ; subst b_ c_.
      + apply j_while_false ; eauto.
      + simpl. apply (j_while_true _ m S₁) ; eauto.
        destruct (IHcd S S₁ m). auto.
      + simpl. apply (j_while_break _ S₁) ; eauto.
        destruct (IHcd S S₁ MBreak). auto.
    × destruct c ; destruct c0 ; simpl in × ; auto ;
        try (destruct m ; eauto ; apply j_seq_interrupt ; eauto ; discriminate).
    × destruct c ; destruct c0 ; simpl in × ; auto ;
        try (destruct m ; eauto ; apply j_seq_interrupt ; eauto ; discriminate).
  Qed.

  Lemma diff_completeness:
     c₁ c₂, cd, Π₀ cd = c₁ Π₁ cd = c₂.
  Proof.
    intro c₁. induction c₁.
    × intro c₂. induction c₂.
      + (LeafSubst c c0). intuition.
      + destruct IHc₂1 as (cd, H).
         (SeqInsR cd c₂2). intuition.
        simpl. rewrite H1. auto.
      + destruct IHc₂ as (cd, H).
         (WhileAdd b cd). simpl. intuition.
        rewrite H1. auto.
      + destruct IHc₂2 as (cd, H).
         (ITEAddIf b c₂1 cd). intuition.
        simpl. rewrite H1. auto.
    × intro c₂.
      destruct (IHc₁1 c₂) as (cd, H).
       (SeqDelR cd c₁2).
      simpl. destruct H as (H₁, H₂). rewrite H₁. rewrite H₂. auto.
    × intro c₂. destruct (IHc₁ c₂) as (cd, (H₁, H₂)).
       (WhileDel b cd). simpl. rewrite H₁, H₂. intuition.
    × intro c₂. destruct (IHc₁1 c₂) as (cd, (H₁, H₂)).
       (ITEDelElse b cd c₁2). simpl. rewrite H₁, H₂.
      auto.
  Qed.

  Inductive cmd_subtree : cmd cmd Prop :=
  | cmd_subtree_id : c, cmd_subtree c c
  | cmd_subtree_if_then : c c' c'' b, cmd_subtree c'' c cmd_subtree c'' (IfThenElse b c c')
  | cmd_subtree_if_else : c c' c'' b, cmd_subtree c'' c' cmd_subtree c'' (IfThenElse b c c')
  | cmd_subtree_seq_left : c c' c'', cmd_subtree c'' c cmd_subtree c'' (Seq c c')
  | cmd_subtree_seq_right : c c' c'', cmd_subtree c'' c' cmd_subtree c'' (Seq c c')
  | cmd_subtree_while : b c c'', cmd_subtree c'' c cmd_subtree c'' (While b c).

  Inductive diff_subtree : cmd_diff cmd_diff Prop :=
  | diff_subtree_id : cd, diff_subtree cd cd
  | diff_subtree_seq_del_l : cd cd' c, diff_subtree cd' cd diff_subtree cd' (SeqDelL c cd)
  | diff_subtree_seq_del_r : cd cd' c, diff_subtree cd' cd diff_subtree cd' (SeqDelR cd c)
  | diff_subtree_seq_ins_l : cd cd' c, diff_subtree cd' cd diff_subtree cd' (SeqInsL c cd)
  | diff_subtree_seq_ins_r : cd cd' c, diff_subtree cd' cd diff_subtree cd' (SeqInsR cd c)
  | diff_subtree_seq_l : cd cd' cd'', diff_subtree cd'' cd diff_subtree cd'' (SeqMut cd cd')
  | diff_subtree_seq_r : cd cd' cd'', diff_subtree cd'' cd' diff_subtree cd'' (SeqMut cd cd')
  | diff_subtree_ifmut_then : cd cd' cd'' b b', diff_subtree cd'' cd diff_subtree cd'' (IfMut (b, b') cd cd')
  | diff_subtree_ifmut_else : cd cd' cd'' b b', diff_subtree cd'' cd' diff_subtree cd'' (IfMut (b, b') cd cd')
  | diff_subtree_while_mut : cd cd' b b', diff_subtree cd' cd diff_subtree cd' (WhileMut (b, b') cd)
  | diff_subtree_add_if : cd cd' b c, diff_subtree cd' cd diff_subtree cd' (ITEAddIf b c cd)
  | diff_subtree_add_else : cd cd' b c, diff_subtree cd' cd diff_subtree cd' (ITEAddElse b cd c)
  | diff_subtree_del_if : cd cd' b c, diff_subtree cd' cd diff_subtree cd' (ITEDelIf b c cd)
  | diff_subtree_del_else : cd cd' b c, diff_subtree cd' cd diff_subtree cd' (ITEDelElse b cd c)
  | diff_subtree_while_add : cd cd' b, diff_subtree cd' cd diff_subtree cd' (WhileAdd b cd)
  | diff_subtree_while_del : cd cd' b, diff_subtree cd' cd diff_subtree cd' (WhileDel b cd).

  Hint Constructors cmd_subtree.

  Lemma diffmap_recursivity:
     cd cd', diff_subtree cd' cd cmd_subtree (Π₀ cd') (Π₀ cd) cmd_subtree (Π₁ cd') (Π₁ cd).
  Proof.
    intros cd cd' Hsubtree. induction Hsubtree ; simpl ; intuition.
  Qed.

  Fixpoint add_cpoints cd :=
    match cd with
    | SeqMut cd cd'SeqMut (add_cpoints cd) (add_cpoints cd')
    | SeqDelR cd cSeqDelR (add_cpoints cd) c
    | SeqDelL c cdSeqDelL c (add_cpoints cd)
    | SeqInsR cd cSeqInsR (add_cpoints cd) c
    | SeqInsL c cdSeqInsL c (add_cpoints cd)
    | IfMut (b, b') cd cd'IfMut (b, b') (add_cpoints cd) (add_cpoints cd')
    | WhileMut (b, b') cdWhileMut (b, b') (add_cpoints cd)
    | WhileAdd b cdWhileAdd b (add_cpoints cd)
    | WhileDel b cdWhileDel b (add_cpoints cd)
    | ITEAddIf b c cdITEAddIf b c (add_cpoints cd)
    | ITEDelIf b c cdITEDelIf b c (add_cpoints cd)
    | ITEAddElse b cd cITEAddElse b (add_cpoints cd) c
    | ITEDelElse b cd cITEDelElse b (add_cpoints cd) c
    | CPoint cdCPoint (add_cpoints cd)
    | LeafSubst Skip Skipcd
    | LeafSubst a a'if cmda_beq a a' then CPoint cd else cd
    end.

  Lemma add_cpoints_conserves_semantics:
     cd, S₀ S₀' S₁ S₁' m₀ m₁,
    (big_step S₀ (Π₀ cd) m₀ S₀' big_step S₀ (Π₀ (add_cpoints cd)) m₀ S₀')
    (big_step S₁ (Π₁ cd) m₁ S₁' big_step S₁ (Π₁ (add_cpoints cd)) m₁ S₁').
  Proof.
    intros cd. induction cd ; intros S₀ S₀' S₁ S₁' m₀ m₁ ; simpl in × ;
    split ; intro Hstep ; auto ; try (apply IHcd ; auto ; fail).
    × inversion Hstep ; subst.
      + apply (j_seq_normal _ _ _ s₁) ; auto. apply IHcd ; auto.
      + apply j_seq_interrupt ; auto.
    × inversion Hstep ; subst.
      + apply (j_seq_normal _ _ _ s₁) ; auto. apply IHcd ; auto.
      + apply j_seq_interrupt ; auto. apply IHcd ; auto.
    × inversion Hstep ; subst.
      + apply (j_seq_normal _ _ _ s₁) ; auto. apply IHcd ; auto.
      + apply j_seq_interrupt ; auto.
    × inversion Hstep ; subst.
      + apply (j_seq_normal _ _ _ s₁) ; auto ; apply IHcd ; auto.
      + apply j_seq_interrupt ; auto ; apply IHcd ; auto.
    × inversion Hstep ; subst.
      + apply (j_seq_normal _ _ _ s₁). apply IHcd1 ; auto. apply IHcd2 ; auto.
      + apply j_seq_interrupt ; auto. apply IHcd1 ; auto.
    × inversion Hstep ; subst.
      + apply (j_seq_normal _ _ _ s₁). apply IHcd1 ; auto. apply IHcd2 ; auto.
      + apply j_seq_interrupt ; auto. apply IHcd1 ; auto.
    × destruct p as (b, b'). simpl in ×. inversion Hstep ; subst.
      + apply j_if_then ; auto. apply IHcd1 ; auto.
      + apply j_if_else ; auto. apply IHcd2 ; auto.
    × destruct p as (b, b'). simpl in ×. inversion Hstep ; subst.
      + apply j_if_then ; auto. apply IHcd1 ; auto.
      + apply j_if_else ; auto. apply IHcd2 ; auto.
    × destruct p as (b, b'). simpl in ×. remember (While b (Π₀ cd)) as cd' eqn:Hcd'.
      induction Hstep ; inversion Hcd' ; subst.
      + apply j_while_false. auto.
      + apply (j_while_true _ m s₁) ; auto. apply IHcd ; auto.
      + apply j_while_break ; auto. apply IHcd ; auto.
    × destruct p as (b, b'). simpl in ×. remember (While b' (Π₁ cd)) as cd' eqn:Hcd'.
      induction Hstep ; inversion Hcd' ; subst.
      + apply j_while_false. auto.
      + apply (j_while_true _ m s₁) ; auto. apply IHcd ; auto.
      + apply j_while_break ; auto. apply IHcd ; auto.
    × inversion Hstep ; subst ; auto.
      apply j_if_else ; auto. apply IHcd ; auto.
    × inversion Hstep ; subst ; auto.
      apply j_if_then ; auto. apply IHcd ; auto.
    × inversion Hstep ; subst ; auto.
      apply j_if_else ; auto. apply IHcd ; auto.
    × inversion Hstep ; subst ; auto.
      apply j_if_then ; auto. apply IHcd ; auto.
    × remember (While b (Π₁ cd)) as cd' eqn:Hcd'.
      induction Hstep ; inversion Hcd' ; subst.
      + apply j_while_false ; auto.
      + apply (j_while_true _ m s₁) ; auto. apply IHcd ; auto.
      + apply j_while_break ; auto. apply IHcd ; auto.
    × remember (While b (Π₀ cd)) as cd' eqn:Hcd'.
      induction Hstep ; inversion Hcd' ; subst.
      + apply j_while_false ; auto.
      + apply (j_while_true _ m s₁) ; auto. apply IHcd ; auto.
      + apply j_while_break ; auto. apply IHcd ; auto.
    × destruct c ; destruct c0 ; simpl ; auto.
      destruct (lvalue_beq l l0) ;
      destruct (exp_beq e e0) ; simpl ; auto.
    × destruct c ; destruct c0 ; simpl ; auto.
      destruct (lvalue_beq l l0) ;
      destruct (exp_beq e e0) ; simpl ; auto.
  Qed.

  Fixpoint tag_lval t x :=
    match x with
    | Var yVar (t y)
    | ArrayAccess y nArrayAccess (tag_lval t y) (tag_exp t n)
    end
  with tag_exp t e :=
    match e with
    | Sum e₁ e₂Sum (tag_exp t e₁) (tag_exp t e₂)
    | Diff e₁ e₂Diff (tag_exp t e₁) (tag_exp t e₂)
    | Mult e₁ e₂Mult (tag_exp t e₁) (tag_exp t e₂)
    | Div e₁ e₂Div (tag_exp t e₁) (tag_exp t e₂)
    | Lval xLval (tag_lval t x)
    | Int nInt n
    end.

  Fixpoint tag_bexp t b :=
    match b with
    | BTrue | BFalseb
    | BNot b'BNot (tag_bexp t b')
    | BAnd b₁ b₂BAnd (tag_bexp t b₁) (tag_bexp t b₂)
    | BOr b₁ b₂BOr (tag_bexp t b₁) (tag_bexp t b₂)
    | BLE e₁ e₂BLE (tag_exp t e₁) (tag_exp t e₂)
    | BGE e₁ e₂BGE (tag_exp t e₁) (tag_exp t e₂)
    | BLT e₁ e₂BLT (tag_exp t e₁) (tag_exp t e₂)
    | BGT e₁ e₂BGT (tag_exp t e₁) (tag_exp t e₂)
    | BEQ e₁ e₂BEQ (tag_exp t e₁) (tag_exp t e₂)
    | BNEQ e₁ e₂BNEQ (tag_exp t e₁) (tag_exp t e₂)
    end.

  Definition tag_cmda t c :=
    match c with
    | SkipSkip
    | Assign x eAssign (tag_lval t x) (tag_exp t e)
    | BreakBreak
    | ContinueContinue
    end.

  Fixpoint tag_cmd t c :=
    match c with
    | Seq c₁ c₂Seq (tag_cmd t c₁) (tag_cmd t c₂)
    | While b cWhile (tag_bexp t b) (tag_cmd t c)
    | IfThenElse b c₁ c₂
      IfThenElse (tag_bexp t b) (tag_cmd t c₁) (tag_cmd t c₂)
    | Leaf aLeaf (tag_cmda t a)
    end.

  Lemma t_injective_store_proj :
     (t : var var), ( x y, t x = t y x = y)
     s, store_included_tagged t s (tag_store t s).
  Proof.
    unfold store_included_tagged, tag_store.
    intros t Ht.
    intros s x v.
    apply VarMapProps.fold_rec.
    × intros m Hm Hxv. exfalso. apply (Hm x v). auto.
    × intros k v' a m' m'' Hkv' Hkm' Hm'm'' IH Hxvm''.
      rewrite VarMapFacts.add_mapsto_iff.
      destruct (Var_as_DT.eq_dec x k).
      + left. subst. intuition.
        rewrite VarMapFacts.find_mapsto_iff in Hxvm''.
        rewrite Hm'm'' in Hxvm''.
        rewrite VarMapFacts.add_eq_o in Hxvm''. inversion Hxvm''. auto. auto.
      + right. split.
        - intro Hfalse. apply n. apply Ht. auto.
        - apply IH.
          rewrite VarMapFacts.find_mapsto_iff.
          rewrite VarMapFacts.find_mapsto_iff in Hxvm''.
          rewrite Hm'm'' in Hxvm''.
          rewrite VarMapFacts.add_neq_o in Hxvm'' ; auto.
  Qed.

  Lemma tagged_store_keys_tagged:
     (t : var var),
     s, x, VarMap.In x (tag_store t s) y, x = t y.
  Proof.
    unfold tag_store.
    intros t s.
    apply VarMapProps.fold_rec.
    × intros m Hm x Hx.
      rewrite VarMapFacts.empty_in_iff in Hx. exfalso. auto.
    × intros k v a m' m'' Hkv Hkm' Hm'm'' IH x Hx.
      destruct (Var_as_DT.eq_dec x (t k)).
      + k. auto.
      + apply IH. rewrite VarMapFacts.add_in_iff in Hx. intuition.
        exfalso. auto.
  Qed.

  Fixpoint tag_diffmap t t' cd :=
    match cd with
    | SeqDelL c cd
      SeqDelL (tag_cmd t c) (tag_diffmap t t' cd)
    | SeqInsL c cd
      SeqInsL (tag_cmd t' c) (tag_diffmap t t' cd)
    | SeqDelR cd c
      SeqDelR (tag_diffmap t t' cd) (tag_cmd t c)
    | SeqInsR cd c
      SeqInsR (tag_diffmap t t' cd) (tag_cmd t' c)
    | SeqMut cd₁ cd₂
      SeqMut (tag_diffmap t t' cd₁) (tag_diffmap t t' cd₂)
    | IfMut (b, b') cd₁ cd₂
      IfMut (tag_bexp t b, tag_bexp t' b') (tag_diffmap t t' cd₁)
                                           (tag_diffmap t t' cd₂)
    | WhileMut (b, b') cd
      WhileMut (tag_bexp t b, tag_bexp t' b') (tag_diffmap t t' cd)
    | ITEDelIf b c cd
      ITEDelIf (tag_bexp t b) (tag_cmd t c) (tag_diffmap t t' cd)
    | ITEAddIf b c cd
      ITEAddIf (tag_bexp t' b) (tag_cmd t' c) (tag_diffmap t t' cd)
    | ITEDelElse b cd c
      ITEDelElse (tag_bexp t b) (tag_diffmap t t' cd) (tag_cmd t c)
    | ITEAddElse b cd c
      ITEAddElse (tag_bexp t' b) (tag_diffmap t t' cd) (tag_cmd t' c)
    | WhileDel b cd
      WhileDel (tag_bexp t b) (tag_diffmap t t' cd)
    | WhileAdd b cd
      WhileAdd (tag_bexp t' b) (tag_diffmap t t' cd)
    
    | LeafSubst a a'LeafSubst (tag_cmda t a) (tag_cmda t' a')
    
    | CPoint cdCPoint (tag_diffmap t t' cd)
    end.

  Lemma tag_diffmap_proj_correct:
     (cd : cmd_diff) (t t' : var var),
    Π₀ (tag_diffmap t t' cd) = tag_cmd t (Π₀ cd)
    Π₁ (tag_diffmap t t' cd) = tag_cmd t' (Π₁ cd).
  Proof.
    intros cd t t'.
    split ; induction cd ; intuition ;
    simpl ; (rewrite IHcd || rewrite IHcd1, IHcd2) ; auto.
  Qed.

  Fixpoint cp (c : cmd_diff) (π π : path) (gl₀ gl₁ : guard_conj) (o₀ o₁ : option path) : cmd_g :=
    match c with
    | SeqDelL c cd
      (CI gl₀ (S0 π) c o₀ ; cp cd (S1 π) π gl₀ gl₁ o₀ o₁)%GAST
    | SeqDelR cd c
      (cp cd (S0 π) π gl₀ gl₁ o₀ o₁ ; CI gl₀ (S1 π) c o₀)%GAST
    | SeqInsL c cd
      (CI gl₁ (S0 π) c o₁ ; cp cd π (S1 π) gl₀ gl₁ o₀ o₁)%GAST
    | SeqInsR cd c
      (cp cd π (S0 π) gl₀ gl₁ o₀ o₁ ; CI gl₁ (S1 π) c o₁)%GAST
    | SeqMut cd₁ cd₂
      (cp cd₁ (S0 π) (S0 π) gl₀ gl₁ o₀ o₁ ; cp cd₂ (S1 π) (S1 π) gl₀ gl₁ o₀ o₁)%GAST
    | IfMut (b, b') cd₁ cd₂
      (GAtomic gl₀ (GAGAssign π b) ;
       GAtomic gl₁ (GAGAssign π b') ;
       cp cd₁ (S1 π) (S1 π) (gl₀ ++ [(true, π)]) (gl₁ ++ [(true, π)]) o₀ o₁ ;
       cp cd₂ (S0 π) (S0 π) (gl₀ ++ [(false, π)]) (gl₁ ++ [(false, π)]) o₀ o₁)%GAST
    | WhileMut (b, b') cd
      let gl₀' := gl₀ ++ [(true, π)] in
      let gl₁' := gl₁ ++ [(true, π)] in
      (GAtomic gl₀ (GAGAssign π b) ;
       GAtomic gl₁ (GAGAssign π b') ;
       GWhile (gl₀'::gl₁'::nil) (
         GAtomic gl₀' (GAGAssign (S1 π) BTrue);
         GAtomic gl₁' (GAGAssign (S1 π) BTrue);
         cp cd (S1 (S1 π)) (S1 (S1 π)) (gl₀' ++ [(true, S1 π)]) (gl₁' ++ [(true, S1 π)]) (Some π) (Some π) ;
         GAtomic gl₀' (GAGAssign π b) ;
         GAtomic gl₁' (GAGAssign π b'))
      )%GAST
    | ITEDelIf b c cd
      (GAtomic gl₀ (GAGAssign π b) ;
       CI (gl₀ ++ [(true, π)]) (S1 π) c o₀ ;
       cp cd (S0 π) π (gl₀ ++ [(false, π)]) gl₁ o₀ o₁)%GAST
    | ITEAddIf b c cd
      (GAtomic gl₁ (GAGAssign π b) ;
       CI (gl₁ ++ [(true, π)]) (S1 π) c o₁ ;
       cp cd π (S0 π) gl₀ (gl₁ ++ [(false, π)]) o₀ o₁)%GAST
    | ITEDelElse b cd c
      (GAtomic gl₀ (GAGAssign π b) ;
       cp cd (S1 π) π (gl₀ ++ [(true, π)]) gl₁ o₀ o₁ ;
       CI (gl₀ ++ [(false, π)]) (S0 π) c o₀)%GAST
    | ITEAddElse b cd c
      (GAtomic gl₁ (GAGAssign π b) ;
       cp cd π (S1 π) gl₀ (gl₁ ++ [(true, π)]) o₀ o₁ ;
       CI (gl₁ ++ [(false, π)]) (S0 π) c o₁)%GAST
    | WhileDel b cd
      let gl₀' := gl₀ ++ [(true, π)] in
      (GAtomic gl₀ (GAGAssign π b) ;
       GAtomic gl₀' (GAGAssign (S1 π) BTrue);
       cp cd (S1 (S1 π)) π (gl₀' ++ [(true, S1 π)]) gl₁ (Some π) o₁ ;
       GAtomic gl₀' (GAGAssign π b) ;
        GWhile ([gl₀']) (
          GAtomic gl₀' (GAGAssign (S1 π) BTrue);
          CI (gl₀' ++ [(true, S1 π)]) (S1 (S1 π)) (Π₀ cd) (Some π) ;
          GAtomic gl₀' (GAGAssign π b))
      )%GAST
    | WhileAdd b cd
      let gl₁' := gl₁ ++ [(true, π)] in
      (GAtomic gl₁ (GAGAssign π b) ;
       GAtomic gl₁' (GAGAssign (S1 π) BTrue);
       cp cd π (S1 (S1 π)) gl₀ (gl₁' ++ [(true, S1 π)]) o₀ (Some π) ;
       GAtomic gl₁' (GAGAssign π b) ;
       GWhile ([gl₁']) (
         GAtomic gl₁' (GAGAssign (S1 π) BTrue);
         CI (gl₁' ++ [(true, S1 π)]) (S1 (S1 π)) (Π₁ cd) (Some π) ;
         GAtomic gl₁' (GAGAssign π b))
      )%GAST
    
    | LeafSubst Skip a'
      CI gl₁ π (Leaf a') o₁
    | LeafSubst a Skip
      CI gl₀ π (Leaf a) o₀
    | LeafSubst a a'
      (CI gl₀ π (Leaf a) o₀;
       CI gl₁ π (Leaf a') o₁)%GAST
    
    | CPoint cdGSeq GCPoint (cp cd π π gl₀ gl₁ o₀ o₁)
    end.

  Inductive classification :=
    | ClsOrig
    | ClsDiff.

  Definition classification_fun := var option classification.

  Definition valid_classification_fun (f : classification_fun) (t t' : var var) : Prop :=
     x, f (t x) = Some ClsOrig f (t' x) = Some ClsDiff.

  Definition store_classified (f : classification_fun) (S₀ S₁ : store) :=
    ( x, VarMap.In x S₀ f x = Some ClsOrig)
     ( x, VarMap.In x S₁ f x = Some ClsDiff).

  Definition gstore_classified (G₀ G₁ : gstore) :=
    ( g, GuardMap.In g G₀ path_suffix g (S0 ε))
     ( g, GuardMap.In g G₁ path_suffix g (S1 ε)).

  Fixpoint lval_classified (f : classification_fun) x (cls : classification) :=
    match x with
    | Var yf y = Some cls
    | ArrayAccess y nlval_classified f y cls exp_classified f n cls
    end
  with exp_classified (f : classification_fun) e (cls : classification) :=
    match e with
    | Sum e₁ e₂ | Diff e₁ e₂ | Mult e₁ e₂ | Div e₁ e₂
        exp_classified f e₁ cls exp_classified f e₂ cls
    | Int _True
    | Lval xlval_classified f x cls
    end.

  Fixpoint bexp_classified (f : classification_fun) b (cls : classification) :=
    match b with
    | BTrue | BFalseTrue
    | BAnd b₁ b₂ | BOr b₁ b₂bexp_classified f b₁ cls bexp_classified f b₂ cls
    | BNot bbexp_classified f b cls
    | BLE e₁ e₂ | BGE e₁ e₂ | BLT e₁ e₂ | BGT e₁ e₂ | BEQ e₁ e₂ | BNEQ e₁ e₂
      exp_classified f e₁ cls exp_classified f e₂ cls
    end.

  Definition cmda_classified (f : classification_fun) c (cls : classification) :=
    match c with
    | Skip | Break | ContinueTrue
    | Assign x elval_classified f x cls exp_classified f e cls
    end.

  Fixpoint cmd_classified (f : classification_fun) c (cls : classification) :=
    match c with
    | Leaf acmda_classified f a cls
    | Seq c₁ c₂cmd_classified f c₁ cls cmd_classified f c₂ cls
    | IfThenElse b c₁ c₂
      bexp_classified f b cls cmd_classified f c₁ cls
       cmd_classified f c₂ cls
    | While b cbexp_classified f b cls cmd_classified f c cls
    end.

  Definition guard_classified (g : guard) (cls : classification) :=
    path_suffix g (match cls with ClsOrigS0 ε | ClsDiffS1 ε end).

  Definition guard_conj_classified (gl : guard_conj) cls :=
    List.Forall (λ bg, let '(_, g) := bg in guard_classified g cls) gl.

  Definition guard_disj_classified (cl : guard_disj) cls :=
    List.Forall (λ gl, guard_conj_classified gl cls) cl.

  Fixpoint cmdg_classified (f : classification_fun) c (cls : classification) :=
    match c with
    | GSkip
      True
    | GSeq c₁ c₂
      cmdg_classified f c₁ cls cmdg_classified f c₂ cls
    | GWhile cl c
      guard_disj_classified cl cls cmdg_classified f c cls
    | GAtomic gl (GAAssign x e) ⇒
      guard_conj_classified gl cls lval_classified f x cls exp_classified f e cls
    | GAtomic gl (GAGAssign g b) ⇒
      guard_conj_classified gl cls
       guard_classified g cls bexp_classified f b cls
    | GCPoint
      True
    end.

  Lemma guard_classified_succ:
     cls π, guard_classified π cls
    guard_classified (S0 π) cls guard_classified (S1 π) cls.
  Proof.
    intros cls π Hπ.
    split ; destruct cls ; unfold guard_classified in × ; simpl in × ; auto.
  Qed.

  Hint Resolve guard_classified_succ.

  Lemma translation_preserves_classification:
     f cls c π o gl,
    ( πl, o = Some πl guard_classified πl cls)
    guard_conj_classified gl cls
    guard_classified π cls
    cmd_classified f c cls
    cmdg_classified f (CI gl π c o) cls.
  Proof.
    intros f cls c.
    induction c ; intros π o gl Ho Hgl Hπ Hc ; simpl in × ; auto.
    × destruct c ; auto.
      + destruct o ; auto. simpl. intuition.
      + destruct o ; auto. simpl. intuition. apply guard_classified_succ. auto.
      + simpl in ×. intuition.
    × intuition.
      + apply IHc1 ; auto. apply guard_classified_succ. auto.
      + apply IHc2 ; auto. apply guard_classified_succ. auto.
    × intuition.
      + unfold guard_disj_classified. apply Forall_cons, Forall_nil. apply Forall_app ; auto.
      + apply Forall_app ; auto.
      + apply guard_classified_succ. auto.
      + apply IHc ; auto.
        - intros πl Hπl. inversion Hπl. subst. auto.
        - apply Forall_app ; auto. apply Forall_cons ; auto.
          apply Forall_cons ; auto. apply guard_classified_succ. auto.
        - repeat apply guard_classified_succ. auto.
      + apply Forall_app ; auto.
    × intuition.
      + apply IHc1 ; auto.
        - apply Forall_app ; auto.
        - apply guard_classified_succ. auto.
      + apply IHc2 ; auto.
        - apply Forall_app ; auto.
        - apply guard_classified_succ. auto.
  Qed.

  Fixpoint diffmap_classified (f : classification_fun) cd :=
    match cd with
    | SeqDelL c cd | SeqDelR cd c
      cmd_classified f c ClsOrig diffmap_classified f cd
    | SeqInsL c cd | SeqInsR cd c
      cmd_classified f c ClsDiff diffmap_classified f cd
    | SeqMut cd₁ cd₂
      diffmap_classified f cd₁ diffmap_classified f cd₂
    | IfMut (b, b') cd₁ cd₂
      bexp_classified f b ClsOrig bexp_classified f b' ClsDiff
       diffmap_classified f cd₁ diffmap_classified f cd₂
    | WhileMut (b, b') cd
      bexp_classified f b ClsOrig bexp_classified f b' ClsDiff
       diffmap_classified f cd
    | ITEDelIf b c cd | ITEDelElse b cd c
      bexp_classified f b ClsOrig cmd_classified f c ClsOrig
       diffmap_classified f cd
    | ITEAddIf b c cd | ITEAddElse b cd c
      bexp_classified f b ClsDiff cmd_classified f c ClsDiff
       diffmap_classified f cd
    | WhileDel b cd
      bexp_classified f b ClsOrig diffmap_classified f cd
    | WhileAdd b cd
      bexp_classified f b ClsDiff diffmap_classified f cd
    
    | LeafSubst a a'cmda_classified f a ClsOrig cmda_classified f a' ClsDiff
    
    | CPoint cddiffmap_classified f cd
    end.

  Lemma diffmap_classification:
     (f : classification_fun), cd, diffmap_classified f cd
     cmd_classified f (Π₀ cd) ClsOrig cmd_classified f (Π₁ cd) ClsDiff.
  Proof.
    intros f cd. split.
    × intros H.
      induction cd as [ | | | | | (b, b') | (b, b') | | | | | | | | ] ; simpl in × ; intuition.
    × intros (H₁, H₂).
      induction cd as [ | | | | | (b, b') | (b, b') | | | | | | | | ] ; simpl in × ; intuition.
  Qed.

  Property tag_exp_classification:
     f t t', valid_classification_fun f t t'
     e, exp_classified f (tag_exp t e) ClsOrig
     exp_classified f (tag_exp t' e) ClsDiff.
  Proof.
    unfold valid_classification_fun.
    intros f t t' H e. apply (exp_mut (λ e, exp_classified f (tag_exp t e) ClsOrig exp_classified f (tag_exp t' e) ClsDiff)
    (λ x, lval_classified f (tag_lval t x) ClsOrig lval_classified f (tag_lval t' x) ClsDiff)) ; simpl in × ; intuition.
  Qed.

TODO: how to factor this proof?
  Property tag_lval_classification:
     f t t', valid_classification_fun f t t'
     x, lval_classified f (tag_lval t x) ClsOrig
     lval_classified f (tag_lval t' x) ClsDiff.
  Proof.
    unfold valid_classification_fun.
    intros f t t' H e. apply (lvalue_mut (λ e, exp_classified f (tag_exp t e) ClsOrig exp_classified f (tag_exp t' e) ClsDiff)
    (λ x, lval_classified f (tag_lval t x) ClsOrig lval_classified f (tag_lval t' x) ClsDiff)) ; simpl in × ; intuition.
  Qed.

  Property tag_bexp_classification:
     f t t', valid_classification_fun f t t'
     b, bexp_classified f (tag_bexp t b) ClsOrig
     bexp_classified f (tag_bexp t' b) ClsDiff.
  Proof.
    intros f t t' H.
    intro b. induction b ; simpl in × ; intuition ; apply (tag_exp_classification f t t' H).
  Qed.

  Property tag_cmda_classification:
     f t t', valid_classification_fun f t t'
     a, cmda_classified f (tag_cmda t a) ClsOrig
     cmda_classified f (tag_cmda t' a) ClsDiff.
  Proof.
    intros f t t' H.
    intro a. destruct a ; simpl in × ; intuition ;
    apply (tag_exp_classification f t t' H) || apply (tag_lval_classification f t t' H).
  Qed.

  Property tag_cmd_classification:
     f t t', valid_classification_fun f t t'
     c, cmd_classified f (tag_cmd t c) ClsOrig
     cmd_classified f (tag_cmd t' c) ClsDiff.
  Proof.
    intros f t t' H.
    intro c. induction c ; simpl in × ; intuition ;
    apply (tag_cmda_classification f t t' H) || apply (tag_bexp_classification f t t' H).
  Qed.

  Property tag_diffmap_classification:
     f t t', valid_classification_fun f t t'
     cd, diffmap_classified f (tag_diffmap t t' cd).
  Proof.
    intros f t t' H.
    intro cd. apply diffmap_classification.
    destruct (tag_diffmap_proj_correct cd t t') as (H₁, H₂).
    rewrite H₁, H₂.
    split ; apply (tag_cmd_classification f t t' H).
  Qed.

  Definition store_included (s s' : store) :=
     x v, VarMap.MapsTo x v s VarMap.MapsTo x v s'.

  Lemma classified_cmdg_preserves_classified_stores:
     f S₀ S₁ G₀ G₁ S' G' c,
    store_classified f S₀ S₁
    gstore_classified G₀ G₁
    (cmdg_classified f c ClsOrig big_step_g S₀ G₀ c S' G'
      store_classified f S' S₁ gstore_classified G' G₁)
     (cmdg_classified f c ClsDiff big_step_g S₁ G₁ c S' G'
      store_classified f S₀ S' gstore_classified G₀ G').
  Proof.
    intros f S₀ S₁ G₀ G₁ S' G' c HS₀S₁ HG₀G₁.
    split.
    × intros Hc Hstep. induction Hstep ; simpl in × ; try (intuition ; fail).
      + split ; auto.
Lemma truc:
   f S₀ S₁ x v,
  store_classified f S₀ S₁
  (lval_classified f x ClsOrig S₀', set_lval x v S₀ = Some S₀' store_classified f S₀' S₁)
   (lval_classified f x ClsDiff S₁', set_lval x v S₁ = Some S₁' store_classified f S₀ S₁').
Proof.
  intros f S₀ S₁ lval v H. split.
  × intros H' S₀'. revert v. induction lval as [ x | lval IH n ].
    + intros v H''. unfold store_classified in ×. simpl in ×. destruct H as (H₁, H₂). split.
      - intros y H. destruct (Var_as_DT.eq_dec x y).
        { subst x. auto. }
        { apply H₁. inversion H''. clear H''. subst S₀'. rewrite VarMapFacts.add_neq_in_iff in H ; auto. }
      - intros y H. destruct (Var_as_DT.eq_dec x y).
        { subst x. auto. }
        { apply H₂. inversion H''. clear H''. subst S₀'. auto. }
    + intros v H''. simpl in H''. destruct H' as (H', _).
      destruct (interp_exp n S₀) ; destruct (read_lval lval S₀) ; simpl in H'' ; try discriminate H''.
      destruct v0 ; simpl in H'' ; try discriminate H''.
      destruct (z_to_nat z) ; simpl in H'' ; try discriminate H''.
      apply (IH H' _ H'').
  × intros H' S₀'. revert v. induction lval as [ x | lval IH n ].
    + intros v H''. unfold store_classified in ×. simpl in ×. destruct H as (H₁, H₂). split.
      - intros y H. destruct (Var_as_DT.eq_dec x y).
        { subst x. auto. }
        { apply H₁. inversion H''. clear H''. subst S₀'. auto. }
      - intros y H. destruct (Var_as_DT.eq_dec x y).
        { subst x. auto. }
        { apply H₂. inversion H''. clear H''. subst S₀'. rewrite VarMapFacts.add_neq_in_iff in H ; auto. }
    + intros v H''. simpl in H''. destruct H' as (H', _).
      destruct (interp_exp n S₁) ; destruct (read_lval lval S₁) ; simpl in H'' ; try discriminate H''.
      destruct v0 ; destruct (z_to_nat z) ; simpl in H'' ; try discriminate H''.
      apply (IH H' _ H'').
Qed.
  destruct (truc f s S₁ x (IntValue v)) as (H', _). auto. apply H' ; intuition.
      + split ; auto. unfold gstore_classified. intuition.
        - destruct (guard_as_DT.eq_dec g g0).
          { subst. auto. }
          { destruct HG₀G₁. rewrite GuardMapFacts.add_neq_in_iff in H2 ; auto. }
        - destruct HG₀G₁. apply H6. auto.
    × intros Hc Hstep. induction Hstep ; simpl in × ; try (intuition ; fail).
      + simpl in ×. split ; auto. destruct (truc f S₀ s x (IntValue v)) as (_, H'). auto. apply H' ; intuition.
      + simpl in ×. split ; auto. unfold gstore_classified. intuition.
        - destruct HG₀G₁. apply H5. auto.
        - destruct (guard_as_DT.eq_dec g g0).
          { subst. auto. }
          { destruct HG₀G₁. rewrite GuardMapFacts.add_neq_in_iff in H2 ; auto. }
  Qed.

  Property store_inclusion_preserves_exp_eval:
     e S S' v, store_included S S' interp_exp e S = Some v
    interp_exp e S' = Some v.
  Proof.
    intro e.
    apply (exp_mut
      (λ e, S S' v, store_included S S' interp_exp e S = Some v interp_exp e S' = Some v)
      (λ x, S S' v, store_included S S' read_lval x S = Some v read_lval x S' = Some v)).
    × intros x IH S S' val HSS' Hx. simpl in ×.
      pose proof (IH S S') as H. clear IH. destruct (read_lval x S) as [v | ].
      + rewrite (H v) ; simpl in × ; auto.
      + simpl in Hx. discriminate Hx.
    × intros n S S' val HSS' He. simpl in ×. auto.
    × intros e₁ IHe₁ e₂ IHe₂ S S' val HSS' He.
      simpl in ×.
      remember (interp_exp e₁ S) as o₁.
      remember (interp_exp e₂ S) as o₂.
      destruct o₁ as [ v₁ | ] ; simpl in × ; [ | inversion He ].
      destruct o₂ as [ v₂ | ] ; simpl in × ; [ | inversion He ].
      inversion He as [H]. subst val. symmetry in Heqo₁. symmetry in Heqo₂.
      rewrite (IHe₁ S S' v₁ HSS' Heqo₁).
      rewrite (IHe₂ S S' v₂ HSS' Heqo₂).
      simpl. auto.
    × intros e₁ IHe₁ e₂ IHe₂ S S' val HSS' He.
      simpl in ×.
      remember (interp_exp e₁ S) as o₁.
      remember (interp_exp e₂ S) as o₂.
      destruct o₁ as [ v₁ | ] ; simpl in × ; [ | inversion He ].
      destruct o₂ as [ v₂ | ] ; simpl in × ; [ | inversion He ].
      inversion He as [H]. subst val. symmetry in Heqo₁. symmetry in Heqo₂.
      rewrite (IHe₁ S S' v₁ HSS' Heqo₁).
      rewrite (IHe₂ S S' v₂ HSS' Heqo₂).
      simpl. auto.
    × intros e₁ IHe₁ e₂ IHe₂ S S' val HSS' He.
      simpl in ×.
      remember (interp_exp e₁ S) as o₁.
      remember (interp_exp e₂ S) as o₂.
      destruct o₁ as [ v₁ | ] ; simpl in × ; [ | inversion He ].
      destruct o₂ as [ v₂ | ] ; simpl in × ; [ | inversion He ].
      inversion He as [H]. subst val. symmetry in Heqo₁. symmetry in Heqo₂.
      rewrite (IHe₁ S S' v₁ HSS' Heqo₁).
      rewrite (IHe₂ S S' v₂ HSS' Heqo₂).
      simpl. auto.
    × intros e₁ IHe₁ e₂ IHe₂ S S' val HSS' He.
      simpl in ×.
      remember (interp_exp e₁ S) as o₁.
      remember (interp_exp e₂ S) as o₂.
      destruct o₁ as [ v₁ | ] ; simpl in × ; [ | inversion He ].
      destruct o₂ as [ v₂ | ] ; simpl in × ; [ | inversion He ].
      inversion He as [H]. subst val. symmetry in Heqo₁. symmetry in Heqo₂.
      rewrite (IHe₁ S S' v₁ HSS' Heqo₁).
      rewrite (IHe₂ S S' v₂ HSS' Heqo₂).
      simpl. auto.
    × intros x S S' v HSS' Hx. simpl in ×.
      rewrite <- VarMapFacts.find_mapsto_iff in ×. apply HSS'. auto.
    × intros a IHa n IHn S S' v HSS' He.
      simpl in ×.
      pose proof (IHn S S') as IHn'. clear IHn.
      pose proof (IHa S S') as IHa'. clear IHa.
      destruct (interp_exp n S) as [n' | ] ;
      destruct (read_lval a S) as [a' | ] ;
      simpl in × ; try discriminate He.
      rewrite (IHn' n') ; auto. rewrite (IHa' a') ; auto.
  Qed.

  Property store_inclusion_preserves_lval_eval:
     x S S' v, store_included S S' read_lval x S = Some v
    read_lval x S' = Some v.
  Proof.
    intro e.
    apply (lvalue_mut
      (λ e, S S' v, store_included S S' interp_exp e S = Some v interp_exp e S' = Some v)
      (λ x, S S' v, store_included S S' read_lval x S = Some v read_lval x S' = Some v)).
    × intros x IH S S' val HSS' Hx. simpl in ×.
      pose proof (IH S S') as H. clear IH. destruct (read_lval x S) as [v | ].
      + rewrite (H v) ; simpl in × ; auto.
      + simpl in Hx. discriminate Hx.
    × intros n S S' val HSS' He. simpl in ×. auto.
    × intros e₁ IHe₁ e₂ IHe₂ S S' val HSS' He.
      simpl in ×.
      remember (interp_exp e₁ S) as o₁.
      remember (interp_exp e₂ S) as o₂.
      destruct o₁ as [ v₁ | ] ; simpl in × ; [ | inversion He ].
      destruct o₂ as [ v₂ | ] ; simpl in × ; [ | inversion He ].
      inversion He as [H]. subst val. symmetry in Heqo₁. symmetry in Heqo₂.
      rewrite (IHe₁ S S' v₁ HSS' Heqo₁).
      rewrite (IHe₂ S S' v₂ HSS' Heqo₂).
      simpl. auto.
    × intros e₁ IHe₁ e₂ IHe₂ S S' val HSS' He.
      simpl in ×.
      remember (interp_exp e₁ S) as o₁.
      remember (interp_exp e₂ S) as o₂.
      destruct o₁ as [ v₁ | ] ; simpl in × ; [ | inversion He ].
      destruct o₂ as [ v₂ | ] ; simpl in × ; [ | inversion He ].
      inversion He as [H]. subst val. symmetry in Heqo₁. symmetry in Heqo₂.
      rewrite (IHe₁ S S' v₁ HSS' Heqo₁).
      rewrite (IHe₂ S S' v₂ HSS' Heqo₂).
      simpl. auto.
    × intros e₁ IHe₁ e₂ IHe₂ S S' val HSS' He.
      simpl in ×.
      remember (interp_exp e₁ S) as o₁.
      remember (interp_exp e₂ S) as o₂.
      destruct o₁ as [ v₁ | ] ; simpl in × ; [ | inversion He ].
      destruct o₂ as [ v₂ | ] ; simpl in × ; [ | inversion He ].
      inversion He as [H]. subst val. symmetry in Heqo₁. symmetry in Heqo₂.
      rewrite (IHe₁ S S' v₁ HSS' Heqo₁).
      rewrite (IHe₂ S S' v₂ HSS' Heqo₂).
      simpl. auto.
    × intros e₁ IHe₁ e₂ IHe₂ S S' val HSS' He.
      simpl in ×.
      remember (interp_exp e₁ S) as o₁.
      remember (interp_exp e₂ S) as o₂.
      destruct o₁ as [ v₁ | ] ; simpl in × ; [ | inversion He ].
      destruct o₂ as [ v₂ | ] ; simpl in × ; [ | inversion He ].
      inversion He as [H]. subst val. symmetry in Heqo₁. symmetry in Heqo₂.
      rewrite (IHe₁ S S' v₁ HSS' Heqo₁).
      rewrite (IHe₂ S S' v₂ HSS' Heqo₂).
      simpl. auto.
    × intros x S S' v HSS' Hx. simpl in ×.
      rewrite <- VarMapFacts.find_mapsto_iff in ×. apply HSS'. auto.
    × intros a IHa n IHn S S' v HSS' He.
      simpl in ×.
      pose proof (IHn S S') as IHn'. clear IHn.
      pose proof (IHa S S') as IHa'. clear IHa.
      destruct (interp_exp n S) as [n' | ] ;
      destruct (read_lval a S) as [a' | ] ;
      simpl in × ; try discriminate He.
      rewrite (IHn' n') ; auto. rewrite (IHa' a') ; auto.
  Qed.

  Property store_inclusion_preserves_bexp_eval:
     b S S' v, store_included S S' interp_bexp b S = Some v
    interp_bexp b S' = Some v.
  Proof.
    intro b. induction b ; intros S S' val HSS' Hb ; auto.
    × simpl in ×.
      remember (interp_bexp b1 S) as o₁.
      remember (interp_bexp b2 S) as o₂.
      destruct o₁ as [ v₁ | ] ; simpl in × ; [ | inversion Hb ].
      destruct o₂ as [ v₂ | ] ; simpl in × ; [ | inversion Hb ].
      inversion Hb as [H]. subst val. symmetry in Heqo₁. symmetry in Heqo₂.
      rewrite (IHb1 S S' v₁ HSS' Heqo₁), (IHb2 S S' v₂ HSS' Heqo₂).
      simpl. auto.
    × simpl in ×.
      remember (interp_bexp b1 S) as o₁.
      remember (interp_bexp b2 S) as o₂.
      destruct o₁ as [ v₁ | ] ; simpl in × ; [ | inversion Hb ].
      destruct o₂ as [ v₂ | ] ; simpl in × ; [ | inversion Hb ].
      inversion Hb as [H]. subst val. symmetry in Heqo₁. symmetry in Heqo₂.
      rewrite (IHb1 S S' v₁ HSS' Heqo₁), (IHb2 S S' v₂ HSS' Heqo₂).
      simpl. auto.
    × simpl in ×.
      remember (interp_bexp b S) as o₁.
      destruct o₁ as [ v₁ | ] ; simpl in × ; inversion Hb.
      subst val. symmetry in Heqo₁.
      rewrite (IHb S S' v₁ HSS' Heqo₁) ; simpl ; auto.
    × simpl in ×.
      remember (interp_exp e S) as o₁.
      remember (interp_exp e0 S) as o₂.
      destruct o₁ as [ v₁ | ] ; simpl in × ; [ | inversion Hb ].
      destruct o₂ as [ v₂ | ] ; simpl in × ; [ | inversion Hb ].
      inversion Hb as [H]. subst val. symmetry in Heqo₁, Heqo₂.
      rewrite (store_inclusion_preserves_exp_eval e S S' v₁ HSS' Heqo₁),
                   (store_inclusion_preserves_exp_eval e0 S S' v₂ HSS' Heqo₂).
      simpl. auto.
    × simpl in ×.
      remember (interp_exp e S) as o₁.
      remember (interp_exp e0 S) as o₂.
      destruct o₁ as [ v₁ | ] ; simpl in × ; [ | inversion Hb ].
      destruct o₂ as [ v₂ | ] ; simpl in × ; [ | inversion Hb ].
      inversion Hb as [H]. subst val. symmetry in Heqo₁, Heqo₂.
      rewrite (store_inclusion_preserves_exp_eval e S S' v₁ HSS' Heqo₁),
                   (store_inclusion_preserves_exp_eval e0 S S' v₂ HSS' Heqo₂).
      simpl. auto.
    × simpl in ×.
      remember (interp_exp e S) as o₁.
      remember (interp_exp e0 S) as o₂.
      destruct o₁ as [ v₁ | ] ; simpl in × ; [ | inversion Hb ].
      destruct o₂ as [ v₂ | ] ; simpl in × ; [ | inversion Hb ].
      inversion Hb as [H]. subst val. symmetry in Heqo₁, Heqo₂.
      rewrite (store_inclusion_preserves_exp_eval e S S' v₁ HSS' Heqo₁),
                   (store_inclusion_preserves_exp_eval e0 S S' v₂ HSS' Heqo₂).
      simpl. auto.
    × simpl in ×.
      remember (interp_exp e S) as o₁.
      remember (interp_exp e0 S) as o₂.
      destruct o₁ as [ v₁ | ] ; simpl in × ; [ | inversion Hb ].
      destruct o₂ as [ v₂ | ] ; simpl in × ; [ | inversion Hb ].
      inversion Hb as [H]. subst val. symmetry in Heqo₁, Heqo₂.
      rewrite (store_inclusion_preserves_exp_eval e S S' v₁ HSS' Heqo₁),
                   (store_inclusion_preserves_exp_eval e0 S S' v₂ HSS' Heqo₂).
      simpl. auto.
    × simpl in ×.
      remember (interp_exp e S) as o₁.
      remember (interp_exp e0 S) as o₂.
      destruct o₁ as [ v₁ | ] ; simpl in × ; [ | inversion Hb ].
      destruct o₂ as [ v₂ | ] ; simpl in × ; [ | inversion Hb ].
      inversion Hb as [H]. subst val. symmetry in Heqo₁, Heqo₂.
      rewrite (store_inclusion_preserves_exp_eval e S S' v₁ HSS' Heqo₁),
                   (store_inclusion_preserves_exp_eval e0 S S' v₂ HSS' Heqo₂).
      simpl. auto.
    × simpl in ×.
      remember (interp_exp e S) as o₁.
      remember (interp_exp e0 S) as o₂.
      destruct o₁ as [ v₁ | ] ; simpl in × ; [ | inversion Hb ].
      destruct o₂ as [ v₂ | ] ; simpl in × ; [ | inversion Hb ].
      inversion Hb as [H]. subst val. symmetry in Heqo₁, Heqo₂.
      rewrite (store_inclusion_preserves_exp_eval e S S' v₁ HSS' Heqo₁),
                   (store_inclusion_preserves_exp_eval e0 S S' v₂ HSS' Heqo₂).
      simpl. auto.
  Qed.

  Lemma tagged_store_inclusion_exp_eval:
     t e S S' v,
    store_included_tagged t S S'
    interp_exp e S = Some v
    interp_exp (tag_exp t e) S' = Some v.
  Proof.
    intros t e.
    apply (exp_mut
      (λ e, S S' v, store_included_tagged t S S' interp_exp e S = Some v interp_exp (tag_exp t e) S' = Some v)
      (λ x, S S' v, store_included_tagged t S S' read_lval x S = Some v read_lval (tag_lval t x) S' = Some v)).
    × intros x IH S S' val HSS' Hx. simpl in ×.
      pose proof (IH S S') as H. clear IH. destruct (read_lval x S) as [v | ].
      + rewrite (H v) ; simpl in × ; auto.
      + simpl in Hx. discriminate Hx.
    × intros n S S' n' HSS' He. simpl in ×. auto.
    × intros e₁ IHe₁ e₂ IHe₂ S S' v HSS' He. simpl in ×.
      remember (interp_exp e₁ S) as o1.
      remember (interp_exp e₂ S) as o2.
      destruct o1 ; destruct o2 ; simpl in × ; try (discriminate He).
      rewrite (IHe₁ S S' z) ; auto.
      rewrite (IHe₂ S S' z0) ; auto.
    × intros e₁ IHe₁ e₂ IHe₂ S S' v HSS' He. simpl in ×.
      remember (interp_exp e₁ S) as o1.
      remember (interp_exp e₂ S) as o2.
      destruct o1 ; destruct o2 ; simpl in × ; try (discriminate He).
      rewrite (IHe₁ S S' z) ; auto.
      rewrite (IHe₂ S S' z0) ; auto.
    × intros e₁ IHe₁ e₂ IHe₂ S S' v HSS' He. simpl in ×.
      remember (interp_exp e₁ S) as o1.
      remember (interp_exp e₂ S) as o2.
      destruct o1 ; destruct o2 ; simpl in × ; try (discriminate He).
      rewrite (IHe₁ S S' z) ; auto.
      rewrite (IHe₂ S S' z0) ; auto.
    × intros e₁ IHe₁ e₂ IHe₂ S S' v HSS' He. simpl in ×.
      remember (interp_exp e₁ S) as o1.
      remember (interp_exp e₂ S) as o2.
      destruct o1 ; destruct o2 ; simpl in × ; try (discriminate He).
      rewrite (IHe₁ S S' z) ; auto.
      rewrite (IHe₂ S S' z0) ; auto.
    × intros x S S' v HSS' Hx. simpl in ×.
      rewrite <- VarMapFacts.find_mapsto_iff in ×. apply HSS'. auto.
    × intros a IHa n IHn S S' v HSS' He.
      simpl in ×.
      pose proof (IHn S S') as IHn'. clear IHn.
      pose proof (IHa S S') as IHa'. clear IHa.
      destruct (interp_exp n S) as [n' | ] ;
      destruct (read_lval a S) as [a' | ] ;
      simpl in × ; try discriminate He.
      rewrite (IHn' n') ; auto. rewrite (IHa' a') ; auto.
  Qed.

  Lemma tagged_store_inclusion_lval_eval:
     t x S S' v,
    store_included_tagged t S S'
    read_lval x S = Some v
    read_lval (tag_lval t x) S' = Some v.
  Proof.
    intros t e.
    apply (lvalue_mut
      (λ e, S S' v, store_included_tagged t S S' interp_exp e S = Some v interp_exp (tag_exp t e) S' = Some v)
      (λ x, S S' v, store_included_tagged t S S' read_lval x S = Some v read_lval (tag_lval t x) S' = Some v)).
    × intros x IH S S' val HSS' Hx. simpl in ×.
      pose proof (IH S S') as H. clear IH. destruct (read_lval x S) as [v | ].
      + rewrite (H v) ; simpl in × ; auto.
      + simpl in Hx. discriminate Hx.
    × intros n S S' n' HSS' He. simpl in ×. auto.
    × intros e₁ IHe₁ e₂ IHe₂ S S' v HSS' He. simpl in ×.
      remember (interp_exp e₁ S) as o1.
      remember (interp_exp e₂ S) as o2.
      destruct o1 ; destruct o2 ; simpl in × ; try (discriminate He).
      rewrite (IHe₁ S S' z) ; auto.
      rewrite (IHe₂ S S' z0) ; auto.
    × intros e₁ IHe₁ e₂ IHe₂ S S' v HSS' He. simpl in ×.
      remember (interp_exp e₁ S) as o1.
      remember (interp_exp e₂ S) as o2.
      destruct o1 ; destruct o2 ; simpl in × ; try (discriminate He).
      rewrite (IHe₁ S S' z) ; auto.
      rewrite (IHe₂ S S' z0) ; auto.
    × intros e₁ IHe₁ e₂ IHe₂ S S' v HSS' He. simpl in ×.
      remember (interp_exp e₁ S) as o1.
      remember (interp_exp e₂ S) as o2.
      destruct o1 ; destruct o2 ; simpl in × ; try (discriminate He).
      rewrite (IHe₁ S S' z) ; auto.
      rewrite (IHe₂ S S' z0) ; auto.
    × intros e₁ IHe₁ e₂ IHe₂ S S' v HSS' He. simpl in ×.
      remember (interp_exp e₁ S) as o1.
      remember (interp_exp e₂ S) as o2.
      destruct o1 ; destruct o2 ; simpl in × ; try (discriminate He).
      rewrite (IHe₁ S S' z) ; auto.
      rewrite (IHe₂ S S' z0) ; auto.
    × intros x S S' v HSS' Hx. simpl in ×.
      rewrite <- VarMapFacts.find_mapsto_iff in ×. apply HSS'. auto.
    × intros a IHa n IHn S S' v HSS' He.
      simpl in ×.
      pose proof (IHn S S') as IHn'. clear IHn.
      pose proof (IHa S S') as IHa'. clear IHa.
      destruct (interp_exp n S) as [n' | ] ;
      destruct (read_lval a S) as [a' | ] ;
      simpl in × ; try discriminate He.
      rewrite (IHn' n') ; auto. rewrite (IHa' a') ; auto.
  Qed.

  Lemma tagged_store_inclusion_bexp_eval:
     t b S S' v,
    store_included_tagged t S S'
    interp_bexp b S = Some v
    interp_bexp (tag_bexp t b) S' = Some v.
  Proof.
    intros t b. induction b ;
    intros S S' v' HSS' HbS ; simpl in × ; auto.
    × remember (interp_bexp b1 S) as o1.
      remember (interp_bexp b2 S) as o2.
      destruct o1 ; destruct o2 ; simpl in × ; try discriminate HbS.
      rewrite (IHb1 S S' b) ; auto.
      rewrite (IHb2 S S' b0) ; auto.
    × remember (interp_bexp b1 S) as o1.
      remember (interp_bexp b2 S) as o2.
      destruct o1 ; destruct o2 ; simpl in × ; try discriminate HbS.
      rewrite (IHb1 S S' b) ; auto.
      rewrite (IHb2 S S' b0) ; auto.
    × remember (interp_bexp b S) as o1.
      destruct o1 ; simpl in × ; try discriminate HbS.
      rewrite (IHb S S' b0) ; auto.
    × remember (interp_exp e S) as o1.
      remember (interp_exp e0 S) as o2.
      destruct o1 ; destruct o2 ; simpl in × ; try discriminate HbS.
      rewrite (tagged_store_inclusion_exp_eval t e S S' z) ; auto.
      rewrite (tagged_store_inclusion_exp_eval t e0 S S' z0) ; auto.
    × remember (interp_exp e S) as o1.
      remember (interp_exp e0 S) as o2.
      destruct o1 ; destruct o2 ; simpl in × ; try discriminate HbS.
      rewrite (tagged_store_inclusion_exp_eval t e S S' z) ; auto.
      rewrite (tagged_store_inclusion_exp_eval t e0 S S' z0) ; auto.
    × remember (interp_exp e S) as o1.
      remember (interp_exp e0 S) as o2.
      destruct o1 ; destruct o2 ; simpl in × ; try discriminate HbS.
      rewrite (tagged_store_inclusion_exp_eval t e S S' z) ; auto.
      rewrite (tagged_store_inclusion_exp_eval t e0 S S' z0) ; auto.
    × remember (interp_exp e S) as o1.
      remember (interp_exp e0 S) as o2.
      destruct o1 ; destruct o2 ; simpl in × ; try discriminate HbS.
      rewrite (tagged_store_inclusion_exp_eval t e S S' z) ; auto.
      rewrite (tagged_store_inclusion_exp_eval t e0 S S' z0) ; auto.
    × remember (interp_exp e S) as o1.
      remember (interp_exp e0 S) as o2.
      destruct o1 ; destruct o2 ; simpl in × ; try discriminate HbS.
      rewrite (tagged_store_inclusion_exp_eval t e S S' z) ; auto.
      rewrite (tagged_store_inclusion_exp_eval t e0 S S' z0) ; auto.
    × remember (interp_exp e S) as o1.
      remember (interp_exp e0 S) as o2.
      destruct o1 ; destruct o2 ; simpl in × ; try discriminate HbS.
      rewrite (tagged_store_inclusion_exp_eval t e S S' z) ; auto.
      rewrite (tagged_store_inclusion_exp_eval t e0 S S' z0) ; auto.
  Qed.

  Lemma tagged_store_inclusion_sorta_trans:
     t S S' S'',
    store_included_tagged t S S'
    store_included S' S''
    store_included_tagged t S S''.
  Proof.
    intros t S S' S'' HtSS' HS'S''.
    unfold store_included, store_included_tagged in ×.
    intros x v Hxv.
    apply HS'S''.
    apply HtSS'.
    auto.
  Qed.

  Lemma gstore_inclusion_preserves_conj:
     gl G G' b, gstore_included G G'
    guard_conj_evals_to G gl b
    guard_conj_evals_to G' gl b.
  Proof.
    intros gl G G' b HGG' Hgl. destruct b ; simpl in × ;
    apply (guard_conj_evals_to_gstore_inclusion_1 G) ; auto.
  Qed.

  Lemma gstore_inclusion_preserves_disj:
     cl G G' b, gstore_included G G'
    guard_disj_evals_to G cl b
    guard_disj_evals_to G' cl b.
  Proof.
    intros cl G G' b HGG' Hcl. destruct b ; unfold guard_disj_evals_to in ×.
    × rewrite Exists_exists in ×. destruct Hcl as (gl, Hgl). gl. intuition.
      apply (gstore_inclusion_preserves_conj gl G G') ; auto.
    × rewrite Forall_forall in ×. intros gl Hgl.
      apply (gstore_inclusion_preserves_conj gl G G') ; auto.
  Qed.

  Lemma tagged_execution:
     t, ( x y, t x = t y x = y)
     S₀ S₀' m c,
    big_step S₀ c m S₀'
     S, store_included_tagged t S₀ S
     S',
    big_step S (tag_cmd t c) m S' store_included_tagged t S₀' S'.
  Proof.
    intros t t_inj S₀ S₀' m c Hstep.
    induction Hstep ;
    intros S HS₀S ; simpl in ×.
    ×
Lemma toto_TODO:
   t, ( x y, t x = t y x = y) S S' S₁₂ x,
  store_included_tagged t S S₁₂
   v, set_lval x v S = Some S'
   S₁₂', set_lval (tag_lval t x) v S₁₂ = Some S₁₂' store_included_tagged t S' S₁₂'.
Proof.
  intros t Ht S S' S₁₂ x HSS₁₂.
  induction x as [ x | x IHx n ] ; intros v HSS'.
  × simpl in ×. (VarMap.add (t x) v S₁₂) ; intuition.
    unfold store_included_tagged in ×.
    inversion HSS'. subst S'. clear HSS'.
    intros y v' Hyv'. rewrite VarMapFacts.add_mapsto_iff in Hyv'.
    destruct Hyv' as [(H, H') | (H, H')].
    + subst y v'. rewrite VarMapFacts.add_mapsto_iff. intuition.
    + rewrite VarMapFacts.add_neq_mapsto_iff ; auto.
  × simpl in ×.
    remember (interp_exp n S) as idx eqn:Hidx.
    remember (read_lval x S) as x' eqn:Hx'.
    destruct idx as [idx | ] ; destruct x' as [v' | ] ; simpl in HSS' ; try discriminate HSS'.
    destruct v' ; simpl in HSS' ; try discriminate HSS'.
    remember (z_to_nat idx) as idx_n eqn:Hidx_n.
    destruct idx_n as [idx_n | ] ; simpl in HSS' ; try discriminate HSS'.
    destruct (IHx _ HSS') as (S₁₂', (H₁, H₂)).
     S₁₂'.
    rewrite (tagged_store_inclusion_exp_eval t n S S₁₂ idx HSS₁₂) ; auto.
    simpl.
    rewrite (tagged_store_inclusion_lval_eval t x S S₁₂ (ArrayValue l)) ; auto.
    simpl.
    rewrite <- Hidx_n.
    simpl.
    intuition.
Qed.
    destruct (toto_TODO t t_inj s s' S x HS₀S _ H0) as (S', (H₁, H₂)). S'.
    split ; auto.
    apply (j_assign _ _ v) ; auto.
    apply (tagged_store_inclusion_exp_eval t _ s S v) ; auto.
    × S. intuition.
    × destruct (IHHstep1 S) as (Si, Hi) ; try (intuition ; fail).
      destruct (IHHstep2 Si) as (S', H') ; try (intuition ; fail).
       S'. intuition. eauto.
    × destruct (IHHstep S) as (S', H') ; try (intuition ; fail).
       S'. intuition. apply j_if_then.
      + apply (tagged_store_inclusion_bexp_eval t _ s S true) ; auto.
      + auto.
    × destruct (IHHstep S) as (S', H') ; try (intuition ; fail).
       S'. intuition. apply j_if_else.
      + apply (tagged_store_inclusion_bexp_eval t _ s S false) ; auto.
      + auto.
    × S. intuition. apply j_while_false.
      apply (tagged_store_inclusion_bexp_eval t _ s S false) ; auto.
    × destruct (IHHstep1 S) as (Si, Hi) ; try (intuition ; fail).
      destruct (IHHstep2 Si) as (S', H') ; try (intuition ; fail).
       S'. intuition.
      apply (j_while_true _ m Si) ; auto.
      apply (tagged_store_inclusion_bexp_eval t _ s S true) ; auto.
    × destruct (IHHstep S) as (S', H') ; auto.
       S'. split ; auto.
      + a