Library IMP

Require Export Omega Coq.Setoids.Setoid List Util AutoIndTac TraceSemantics Base TailRecursion.

Set Implicit Arguments.
Unset Printing Records.

Require Import Autosubst.

Section Imp.

Axiomatization


  Variable test: Type.
  Parameter inj_test_action : test → nat.
  Axiom inj_test_action_inj : ∀ x y : test, inj_test_action x = inj_test_action y → x = y.
  Coercion inj_test_action : test >-> nat.
  Variable state: Type.
  Variable exec: nat → state → state → Prop.
  Variable comp: test → test.
  Axiom comp_charact: ∀ (b: test) σ σ', ¬ exec b σ σ' ↔ exec (comp b) σ σ'.
  Axiom test_charact: ∀ (b: test) σ σ', exec b σ σ' → σ = σ'.

  Definition notBlock (b:test) σ := exec b σ σ.

Abstract IMP


  Inductive cmd :=
  | CmdSkip: cmd
  | CmdAct : nat → cmd
  | CmdSeq : cmd → cmd → cmd
  | CmdIf : test → cmd → cmd → cmd
  | CmdWhile : test → cmd → cmd.

Big-step semantics


  Inductive sem
    : state → cmd → state → Prop :=
  | SemCmdSkip σ
    : sem σ CmdSkip σ
  | SemCmdInput σ σ' (a: nat)
    : exec a σ σ'
      → sem σ (CmdAct a) σ'
  | SemCmdSeq σ σ' σ'' c1 c2
    : sem σ c1 σ'
        → sem σ' c2 σ''
        → sem σ (CmdSeq c1 c2) σ''
  | SemCmdIfTrue σ σ' (t:test) c d
    : notBlock t σ
      → sem σ c σ'
      → sem σ (CmdIf t c d) σ'
  | SemCmdIfFalse σ σ' t c d
    : ~(notBlock t σ)
      → sem σ d σ'
      → sem σ (CmdIf t c d) σ'
  | SemCmdWhileTrue σ σ' σ'' t c
    : notBlock t σ
      → sem σ c σ'
      → sem σ' (CmdWhile t c) σ''
      → sem σ (CmdWhile t c) σ''
  | SemCmdWhileFalse σ t c
    : ~(notBlock t σ)
      → sem σ (CmdWhile t c) σ.

Context-free abstractions


  Fixpoint cfa c :=
    match c with
    | (CmdSkip) ⇒ CFPEps
    | (CmdAct a) ⇒ CFPVar a
    | (CmdSeq c d) ⇒ CFPSeq (cfa c) (cfa d)
    | (CmdIf b c d) ⇒ CFPChoice (CFPSeq (CFPVar b) (cfa c)) (CFPSeq (CFPVar (comp b)) (cfa d))
    | (CmdWhile b c) ⇒ CFPFix (CFPChoice (CFPSeq (CFPVar (S b)) (CFPSeq (cfa c).[ren(+1)] (CFPVar 0)))(CFPSeq (CFPVar (S (comp b))) (CFPEps)))
    end.

Inversion lemmas for cfa


  Lemma inv_cfa_Var c a
    : cfa c = CFPVar a → c = CmdAct a.
  Proof.
    intros. general induction c. eauto.
  Qed.

  Lemma inv_cfa_Seq c s t
    : cfa c = CFPSeq s t → ∃ c' d, c = CmdSeq c' d ∧ cfa c' = s ∧ cfa d = t.
  Proof.
    intros. general induction c.
    ∃ c1, c2. split; eauto.
  Qed.

  Lemma inv_cfa_Choice c s t
    : cfa c = CFPChoice s t
      → ∃ (b:test) c' d, c = CmdIf b c' d
                               ∧ CFPSeq (CFPVar b) (cfa c') = s
                               ∧ CFPSeq (CFPVar (comp b)) (cfa d) = t.
  Proof.
    intros. general induction c.
    ∃ t, c1, c2. split; eauto.
  Qed.

  Lemma inv_cfa_Fix c s
    : cfa c = CFPFix s
      → ∃ (b:test) d, c = CmdWhile b d
                            ∧ CFPChoice (CFPSeq (CFPVar (S b)) (CFPSeq (cfa d).[ren(+1)] (CFPVar 0)))(CFPSeq (CFPVar (S (comp b))) CFPEps) = s.
  Proof.
    intros. general induction c.
    ∃ t, c. split; eauto.
  Qed.

  Lemma inv_cfa_Eps c
    : cfa c = CFPEps → c = CmdSkip.
  Proof.
    intros. general induction c. eauto.
  Qed.

Tail recursion of context-free abstractions


  Lemma tailrec_cfa c
    : tailrec 0 (cfa c).
  Proof.
    general induction c; simpl; eauto using tailrec.
    - constructor; eauto using bound_zero.
    - constructor; eauto using bound_zero, tailrec.
    - constructor. constructor.
      + constructor; eauto using tailrec.
        × constructor 3. omega.
        × constructor; eauto using tailrec, tailrec_lift.
          apply bound_ren. intros. left. simpl. omega.
      + constructor; eauto using tailrec.
        constructor 3. omega.
  Qed.

Execution of traces on states


  Inductive run : state → trace → state → Prop :=
  | RunT σ
    : run σ T σ
  | RunV x xi σ σ' σ''
    : exec x σ σ' → run σ' xi σ'' → run σ (V x xi) σ''.

Correspondance of IMP and CFP


  Lemma run_concat σ σ' σ'' xi1 xi2
    : run σ xi1 σ' → run σ' xi2 σ'' → run σ (concat xi1 xi2) σ''.
  Proof.
    intros. general induction H.
    - rewrite <- concat_T_iden_left. eauto.
    - simpl. apply RunV with (σ' := σ'); eauto.
  Qed.

  Lemma run_concat2 σ σ'' xi1 xi2
    : run σ (concat xi1 xi2) σ''
      → ∃ σ', run σ xi1 σ' ∧ run σ' xi2 σ''.
  Proof.
    intros. general induction xi1.
    - rewrite concat_partial_absorb_right in H; eauto using partial.
      inv H.
    - rewrite <- concat_T_iden_left in H.
      ∃ σ. split; eauto using run.
    - simpl in H. inv H.
      destruct (IHxi1 test comp σ' σ'' xi2) as [σ2 [A1 A2]]; eauto.
      ∃ σ2. split; eauto.
      apply RunV with (σ' := σ'); eauto.
  Qed.

  Lemma sem_trace σ σ' c
    : sem σ c σ' →
      ∃ xi, TC (cfa c) xi ∧ run σ xi σ'.
  Proof.
    intros. general induction H; simpl.
    - ∃ T. split; eauto using TC, run.
    - ∃ (V a T). split; eauto using TC, run.
    - destruct (IHsem1) as [xi1 [A1 A2]].
      destruct (IHsem2) as [xi2 [B1 B2]].
      ∃ (concat xi1 xi2). split; eauto using TC.
      apply run_concat with (σ' := σ'); eauto.
    - destruct (IHsem) as [xi [A1 A2]].
      ∃ (concat (V t T) xi). split; eauto using TC.
      apply run_concat with (σ' := σ); eauto.
      apply RunV with (σ' := σ); eauto using run.
    - destruct (IHsem) as [xi [A1 A2]].
      ∃ (concat (V (comp t) T) xi). split; eauto using TC.
      apply run_concat with (σ' := σ); eauto.
      apply RunV with (σ' := σ); eauto using run.
      unfold notBlock in H. rewrite <- comp_charact.
      eauto.
    - destruct (IHsem1) as [xi1 [A1 A2]].
      destruct (IHsem2) as [xi2 [B1 B2]].
      ∃ (concat (V t T) (concat xi1 xi2)).
      split.
      + constructor. constructor. constructor; asimpl; eauto using TC.
      + apply run_concat with (σ' := σ).
        × apply RunV with (σ' := σ); eauto using run.
        × apply run_concat with (σ' := σ'); eauto.
    - ∃ (V (comp t) T). split.
      + constructor. constructor 7. asimpl.
        assert (V (comp t) T = concat (V (comp t) T) T); eauto.
        rewrite H0. eauto using TC.
      + apply RunV with (σ' := σ); eauto using run.
        rewrite <- comp_charact. eauto.
  Qed.

  Lemma trace_sem xi σ σ' c
    : TC (cfa c) xi → run σ xi σ' → sem σ c σ'.
  Proof.
    intros. general induction H.
    - inv H0.
    - symmetry in Heqc0. apply inv_cfa_Eps in Heqc0.
      rewrite Heqc0. inv H0. eauto using sem.
    - inv H0. inv H5.
    - symmetry in Heqc0.
      apply inv_cfa_Var in Heqc0. inv H0.
      inv H5. eauto using sem.
    - symmetry in Heqc0.
      destruct (inv_cfa_Seq Heqc0) as [s1 [t1 [A1 [A2 A3]]]].
      apply run_concat2 in H1 as [σ1 [B1 B2]].
      symmetry in A2. symmetry in A3.
      rewrite A1. specialize (IHTC1 σ σ1 s1 A2 B1).
      specialize (IHTC2 σ1 σ' t1 A3 B2).
      eauto using sem.
    - symmetry in Heqc0.
      destruct (inv_cfa_Choice Heqc0) as [b [c' [d [A1 [A2 A3]]]]].
      symmetry in A2.
      specialize (IHTC σ σ' (CmdSeq (CmdAct b) c') A2 H0).
      inv IHTC. inv H4. constructor.
      + assert (σ = σ'0).
        { apply test_charact with (b:= b). eauto. }
        unfold notBlock. rewrite <- H1 in H3. eauto.
      + assert (σ = σ'0).
        { apply test_charact with (b:= b). eauto. }
        rewrite H1. eauto.
    - symmetry in Heqc0.
      destruct (inv_cfa_Choice Heqc0) as [b [c' [d [A1 [A2 A3]]]]].
      symmetry in A3.
      specialize (IHTC σ σ' (CmdSeq (CmdAct (comp b)) d) A3 H0).
      inv IHTC. inv H4.
      assert (σ = σ'0).
      { apply test_charact with (b:= comp b). eauto. }
      constructor 5; eauto.
      + intros A. unfold notBlock in A.
        apply comp_charact in H3. apply H3.
        rewrite <- H1. eauto.
      + rewrite <- H1 in H6. eauto.
    - symmetry in Heqc0. destruct (inv_cfa_Fix Heqc0) as [b [d [A1 A2]]].
      rewrite A1. rewrite <- A2 in H. asimpl in H. inv H.
      + inv H0.
      + inv H4.
        × inv H0.
        × destruct (run_concat2 H0) as [σ1 [A1 A2]].
          inv H6.
          { inv A2. }
          { destruct (run_concat2 A2) as [σ2 [A3 A4]].
            inv H8.
            - inv A4.
            - asimpl in IHTC.
              assert (CFPChoice
                        (CFPSeq (ids b)
                                (CFPSeq (cfa d)
                                        (CFPFix
                                           (CFPChoice
                                              (CFPSeq (CFPVar (S b))
                                                      (CFPSeq (cfa d).[ren (+1)] (CFPVar 0)))
                                              (CFPSeq (CFPVar (S (comp b))) CFPEps)))))
                        (CFPSeq (ids (comp b)) CFPEps) =
                      cfa (CmdIf b (CmdSeq d (CmdWhile b d)) (CmdSkip))).
              { asimpl. eauto. }
              specialize (IHTC σ σ' (CmdIf b (CmdSeq d (CmdWhile b d)) (CmdSkip)) H1 H0).
              inv IHTC.
              + inv H14. apply SemCmdWhileTrue with (σ' := σ'0); eauto.
              + inv H14. constructor. eauto. }
      + inv H4.
        × inv H0.
        × destruct (run_concat2 H0) as [σ1 [A1 A2]].
          inv H3; inv A1; inv H9.
          inv H6; inv A2.
          assert (σ = σ').
          { apply test_charact with (b:= comp b); eauto. }
          rewrite H1. constructor.
          intros A. unfold notBlock in A.
          apply comp_charact in H7. apply H7.
          rewrite <- H1 in A. rewrite <- H1. eauto.
  Qed.

  Definition eqSem c d := ∀ σ σ', sem σ c σ' ↔ sem σ d σ'.
  Notation "s =B t" := (eqSem s t) (at level 70).

  Lemma cfa_correspondence c d
    : (cfa c) =T (cfa d) → c =B d.
  Proof.
    intros. split; intros.
    - apply sem_trace in H0.
      destruct H0 as [xi [A1 A2]].
      apply H in A1. apply (trace_sem A1 A2).
    - apply sem_trace in H0.
      destruct H0 as [xi [A1 A2]].
      apply H in A1. apply (trace_sem A1 A2).
  Qed.

End Imp.