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
    | None ⇒ None
    | Some x ⇒ f 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 Skip ⇒ GSkip
    | 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 Break ⇒ match o with
      | Some πl ⇒ GAtomic gl (GAGAssign πl BFalse)
      | None ⇒ GSkip
      end
    | Leaf Continue ⇒ match o with
      | Some πl ⇒ GAtomic gl (GAGAssign (S1 πl) BFalse)
      | None ⇒ GSkip
      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) as (πl, 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) as (πl, 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) as (πl, (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) as (πl, (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) as (πl, (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) as (πl, (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₁ as (πl, (H₁, (H₁', H₁''))) ; auto.
          - destruct H₁ as (_, (_, (_, H₁))).
            intros g Hg. destruct H₁ as (πl, (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) as (πl, (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₁ as (πl, (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₁' as (πl, (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₁'' as (πl, (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₁' as (πl, H₁') ; auto.
         ∃ πl. intuition.
      + intros Hcontinue. subst. destruct H₁'' as (πl, 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 as (πl, 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 as (πl, 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 a ⇒ SeqInsL (Leaf a) (LeafSubst Skip Skip)
    | LeafSubst a Skip ⇒ SeqDelL (Leaf a) (LeafSubst Skip Skip)
    | LeafSubst a a' ⇒ LeafSubst a a'
    | SeqMut cd cd' ⇒ SeqMut (simplify_diff cd) (simplify_diff cd')
    | SeqDelR cd c ⇒ SeqMut (simplify_diff cd) (SeqDelL c (LeafSubst Skip Skip))
    | SeqInsR cd c ⇒ SeqMut (simplify_diff cd) (SeqInsL c (LeafSubst Skip Skip))
    | SeqDelL c cd ⇒ SeqDelL c (simplify_diff cd)
    | SeqInsL c cd ⇒ SeqInsL c (simplify_diff cd)
    | IfMut (b, b') cd cd' ⇒ IfMut (b, b') (simplify_diff cd) (simplify_diff cd')
    | WhileMut (b, b') cd ⇒ WhileMut (b, b') (simplify_diff cd)
    | WhileAdd b cd ⇒ WhileAdd b (simplify_diff cd)
    | WhileDel b cd ⇒ WhileDel b (simplify_diff cd)
    | ITEAddIf b c cd ⇒ ITEAddIf b c (simplify_diff cd)
    | ITEAddElse b cd c ⇒ ITEAddElse b (simplify_diff cd) c
    | ITEDelIf b c cd ⇒ ITEDelIf b c (simplify_diff cd)
    | ITEDelElse b cd c ⇒ ITEDelElse b (simplify_diff cd) c
    | CPoint cd ⇒ CPoint (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 Skip ⇒ true
    | LeafSubst Skip _ | LeafSubst _ Skip ⇒ false
    | LeafSubst _ _ ⇒ true
    | CPoint cd ⇒ is_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 c ⇒ SeqDelR (add_cpoints cd) c
    | SeqDelL c cd ⇒ SeqDelL c (add_cpoints cd)
    | SeqInsR cd c ⇒ SeqInsR (add_cpoints cd) c
    | SeqInsL c cd ⇒ SeqInsL c (add_cpoints cd)
    | IfMut (b, b') cd cd' ⇒ IfMut (b, b') (add_cpoints cd) (add_cpoints cd')
    | WhileMut (b, b') cd ⇒ WhileMut (b, b') (add_cpoints cd)
    | WhileAdd b cd ⇒ WhileAdd b (add_cpoints cd)
    | WhileDel b cd ⇒ WhileDel b (add_cpoints cd)
    | ITEAddIf b c cd ⇒ ITEAddIf b c (add_cpoints cd)
    | ITEDelIf b c cd ⇒ ITEDelIf b c (add_cpoints cd)
    | ITEAddElse b cd c ⇒ ITEAddElse b (add_cpoints cd) c
    | ITEDelElse b cd c ⇒ ITEDelElse b (add_cpoints cd) c
    | CPoint cd ⇒ CPoint (add_cpoints cd)
    | LeafSubst Skip Skip ⇒ cd
    | 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 y ⇒ Var (t y)
    | ArrayAccess y n ⇒ ArrayAccess (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 x ⇒ Lval (tag_lval t x)
    | Int n ⇒ Int n
    end.

  Fixpoint tag_bexp t b :=
    match b with
    | BTrue | BFalse ⇒ b
    | 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
    | Skip ⇒ Skip
    | Assign x e ⇒ Assign (tag_lval t x) (tag_exp t e)
    | Break ⇒ Break
    | Continue ⇒ Continue
    end.

  Fixpoint tag_cmd t c :=
    match c with
    | Seq c₁ c₂ ⇒ Seq (tag_cmd t c₁) (tag_cmd t c₂)
    | While b c ⇒ While (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 a ⇒ Leaf (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 cd ⇒ CPoint (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 cd ⇒ GSeq 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 y ⇒ f y = Some cls
    | ArrayAccess y n ⇒ lval_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 x ⇒ lval_classified f x cls
    end.

  Fixpoint bexp_classified (f : classification_fun) b (cls : classification) :=
    match b with
    | BTrue | BFalse ⇒ True
    | BAnd b₁ b₂ | BOr b₁ b₂ ⇒ bexp_classified f b₁ cls ∧ bexp_classified f b₂ cls
    | BNot b ⇒ bexp_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 | Continue ⇒ True
    | Assign x e ⇒ lval_classified f x cls ∧ exp_classified f e cls
    end.

  Fixpoint cmd_classified (f : classification_fun) c (cls : classification) :=
    match c with
    | Leaf a ⇒ cmda_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 c ⇒ bexp_classified f b cls ∧ cmd_classified f c cls
    end.

  Definition guard_classified (g : guard) (cls : classification) :=
    path_suffix g (match cls with ClsOrig ⇒ S0 ε | ClsDiff ⇒ S1 ε 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 cd ⇒ diffmap_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.