Library Imp_LangTrick.Imp.Imp_LangLogHoare

From Coq Require Import List String Arith Program.Equality.

From Imp_LangTrick Require Import Imp_LangTrickLanguage Imp_LangLogProp Imp_LangLogSubst LogicProp
Imp_LangLogicHelpers.

Definition triple_Imp_Lang (P: AbsEnv) (i: imp_Imp_Lang) (Q: AbsEnv) (fenv: fun_env) : Prop :=
  forall dbenv nenv nenv',
  i_Imp_Lang i dbenv fenv nenv nenv' ->
  AbsEnv_rel P fenv dbenv nenv ->
  AbsEnv_rel Q fenv dbenv nenv'.

Definition atrueImp_Lang (b: bexp_Imp_Lang) (P: AbsEnv): AbsEnv :=
  (AbsEnvAnd P (AbsEnvLP (Imp_Lang_lp_bool (UnaryProp _ _
                                            (fun bval => bval = true)
                                            b)))).

Definition afalseImp_Lang (b: bexp_Imp_Lang) (P: AbsEnv): AbsEnv :=
  (AbsEnvAnd P (AbsEnvLP (Imp_Lang_lp_bool (UnaryProp _ _
                                            (fun bval => bval = false)
                                            b)))).

Definition aimpImp_Lang (P Q: AbsEnv) (fenv: fun_env): Prop :=
  forall dbenv nenv,
    AbsEnv_rel P fenv dbenv nenv -> AbsEnv_rel Q fenv dbenv nenv.

Definition aandImp_Lang (P Q: assertion): assertion :=
  fun dbenv nenv => P dbenv nenv /\ Q dbenv nenv.

Definition implication_env := list (AbsEnv * AbsEnv).

Definition fact_env_valid (fact_env : implication_env) fenv :=
  forall P Q,
  List.In (P, Q) fact_env ->
  aimpImp_Lang P Q fenv.

Inductive hl_Imp_Lang :
forall (P : AbsEnv) (i: imp_Imp_Lang) (Q: AbsEnv) (facts: implication_env) (fenv: fun_env), Type :=
| hl_Imp_Lang_skip :
  forall P fact_env fenv,
    hl_Imp_Lang P SKIP_Imp_Lang P fact_env fenv
| hl_Imp_Lang_assign :
  forall P fact_env fenv x a,
    hl_Imp_Lang (subst_AbsEnv x a P) (ASSIGN_Imp_Lang x a) P fact_env fenv
| hl_Imp_Lang_seq :
  forall P Q R fact_env fenv i1 i2,
    hl_Imp_Lang P i1 R fact_env fenv ->
    hl_Imp_Lang R i2 Q fact_env fenv ->
    hl_Imp_Lang P (SEQ_Imp_Lang i1 i2) Q fact_env fenv
| hl_Imp_Lang_if :
  forall P Q b i1 i2 fact_env fenv,
    hl_Imp_Lang (atrueImp_Lang b P) i1 Q fact_env fenv ->
    hl_Imp_Lang (afalseImp_Lang b P) i2 Q fact_env fenv ->
    hl_Imp_Lang P (IF_Imp_Lang b i1 i2) Q fact_env fenv
| hl_Imp_Lang_while :
  forall P b i fact_env fenv,
    hl_Imp_Lang (atrueImp_Lang b P) i P fact_env fenv ->
    hl_Imp_Lang P (WHILE_Imp_Lang b i) (afalseImp_Lang b P) fact_env fenv
| hl_Imp_Lang_consequence_pre :
  forall P Q P' c n fact_env fenv,
    hl_Imp_Lang P c Q fact_env fenv ->
    List.nth_error fact_env n = Some (P', P) ->
    aimpImp_Lang P' P fenv ->
    hl_Imp_Lang P' c Q fact_env fenv
| hl_Imp_Lang_consequence_post :
  forall P Q Q' c n fact_env fenv,
    hl_Imp_Lang P c Q fact_env fenv ->
    List.nth_error fact_env n = Some (Q, Q') ->
    aimpImp_Lang Q Q' fenv ->
    hl_Imp_Lang P c Q' fact_env fenv.


Lemma triple_Imp_Lang_skip :
  forall P fenv,
    triple_Imp_Lang P SKIP_Imp_Lang P fenv.
Proof.
unfold triple_Imp_Lang. intros. inversion H. subst. eauto.
Qed.

Lemma triple_Imp_Lang_assign :
  forall P x a fenv,
  triple_Imp_Lang (subst_AbsEnv x a P) (ASSIGN_Imp_Lang x a) P fenv.
Proof.
unfold triple_Imp_Lang. intros. inversion H. subst.
pose proof (aupdate_subst_equiv P fenv dbenv nenv a n x H7 H0).
unfold aupdate in H1. apply H1. eauto.
Qed.

Lemma triple_Imp_Lang_seq :
  forall P Q R i1 i2 fenv,
    triple_Imp_Lang P i1 Q fenv ->
    triple_Imp_Lang Q i2 R fenv ->
    triple_Imp_Lang P (SEQ_Imp_Lang i1 i2) R fenv.
Proof.
  unfold triple_Imp_Lang. intros.
  inversion H1. subst.
  pose proof (H dbenv nenv nenv'0 H5 H2).
  pose proof (H0 dbenv nenv'0 nenv' H10 H3).
  eauto.
Qed.

Lemma triple_Imp_Lang_ifthenelse :
  forall P Q b (i1 i2 : imp_Imp_Lang) fenv,
    triple_Imp_Lang (atrueImp_Lang b P) i1 Q fenv ->
    triple_Imp_Lang (afalseImp_Lang b P) i2 Q fenv ->
    triple_Imp_Lang P (IF_Imp_Lang b i1 i2) Q fenv.
Proof.
  unfold triple_Imp_Lang; intros.
  inversion H1; subst.
  - eapply H.
    eassumption. econstructor.
    eassumption.
    repeat econstructor.
    assumption.
  - eapply H0; try eassumption.
    econstructor; try eassumption; repeat econstructor.
    eassumption.
Qed.

Lemma triple_Imp_Lang_while :
  forall P b l fenv,
  triple_Imp_Lang (atrueImp_Lang b P) l P fenv ->
  triple_Imp_Lang P (WHILE_Imp_Lang b l) (afalseImp_Lang b P) fenv.
Proof.
  unfold triple_Imp_Lang; intros P b l fenv TRUE.
  intros dbenv nenv nenv' IIMP_LANG.
  dependent induction IIMP_LANG; intros.
  - econstructor; try eassumption.
    repeat econstructor.
    assumption.
  -
    eapply IHIIMP_LANG2.
    eassumption.
    reflexivity.
    eapply TRUE. eassumption. econstructor. eassumption. repeat econstructor. eassumption.
Qed.


Lemma triple_Imp_Lang_consequence_pre :
  forall P Q P' c n fact_env fenv,
    triple_Imp_Lang P c Q fenv ->
    List.nth_error fact_env n = Some (P', P) ->
    aimpImp_Lang P' P fenv ->
    triple_Imp_Lang P' c Q fenv.
Proof.
  unfold triple_Imp_Lang, aimpImp_Lang in *. intros.
  apply (H dbenv nenv nenv' H2).
  apply H1. assumption.
Qed.

Lemma triple_Imp_Lang_consequence_post :
  forall P Q Q' c n fact_env fenv,
    triple_Imp_Lang P c Q fenv ->
    List.nth_error fact_env n = Some (Q, Q') ->
    aimpImp_Lang Q Q' fenv ->
    triple_Imp_Lang P c Q' fenv.
Proof.
  unfold triple_Imp_Lang, aimpImp_Lang in *. intros.
  specialize (H dbenv nenv nenv' H2 H3).
  apply H1. assumption.
Qed.
Theorem Hoare_Imp_Lang_sound :
  forall P i Q fact_env fenv,
    hl_Imp_Lang P i Q fact_env fenv ->
    triple_Imp_Lang P i Q fenv.
Proof.
  induction 1;
    eauto using triple_Imp_Lang_skip, triple_Imp_Lang_assign, triple_Imp_Lang_seq, triple_Imp_Lang_ifthenelse, triple_Imp_Lang_while, triple_Imp_Lang_consequence_pre, triple_Imp_Lang_consequence_post.
Qed.