Library OracleLanguages.Imp.RHL


Relational Hoare Logic on Imp
This module defines several variants of Relational Hoare Logic as described by Gilles Barthe, Juan Manuel Crespo and César Kunz in Product programs and relational program logics Soundness proofs for those RHL variants are available in the following modules:

Require Import Common.
Require Import Imp.Lang.
Require Import Imp.BigStep.
Require Import Imp.Hoare.
Require Import Imp.DisjointStates.

Module Make
       (Var_as_DT : UsualDecidableTypeOrig)
       (Import Lang : ImpProgrammingLanguage Var_as_DT)
       (BigStep : ImpBigStep Var_as_DT Lang).

  Module DisjointStates := Imp.DisjointStates.Make Var_as_DT Lang.
  Module Hoare := Imp.Hoare.Make Var_as_DT Lang BigStep.

  Import DisjointStates.
  Import Hoare.

  Inductive minimal_rhl_proof :
    assertion → cmd → cmd → assertion → Type :=
  | MinimalSkip : ∀ P,
    minimal_rhl_proof P Skip Skip P
  | MinimalAssign : ∀ P x e y e',
    minimal_rhl_proof (P [x ↦ e] [y ↦ e']) (Assign x e) (Assign y e') P
  | MinimalAssert : ∀ P b₁ b₂,
    P ⇒ (λ S, (assertion_of_bexp b₁) S ∧ (assertion_of_bexp b₂) S) →
    minimal_rhl_proof P (Assert b₁) (Assert b₂) P
  | MinimalSeq : ∀ P Q R c₁₁ c₂₁ c₁₂ c₂₂,
    minimal_rhl_proof P c₁₁ c₂₁ Q →
    minimal_rhl_proof Q c₁₂ c₂₂ R →
    minimal_rhl_proof P (Seq c₁₁ c₁₂) (Seq c₂₁ c₂₂) R
  | MinimalITE : ∀ P Q b₁ b₂ c₁₁ c₂₁ c₁₂ c₂₂,
    minimal_rhl_proof (λ S, P S ∧ assertion_of_bexp b₁ S)
                      c₁₁ c₂₁ Q →
    minimal_rhl_proof (λ S, P S ∧ assertion_of_bexp (NOT b₁) S)
                      c₁₂ c₂₂ Q →
    P ⇒ (λ S, eval_bexp S b₁ = eval_bexp S b₂) →
    P ⇒ (λ S, eval_bexp S b₁ ≠ None ∧ eval_bexp S b₂ ≠ None) →
    minimal_rhl_proof P (ITE b₁ c₁₁ c₁₂) (ITE b₂ c₂₁ c₂₂) Q
  | MinimalWhile : ∀ P b₁ b₂ c₁ c₂,
    minimal_rhl_proof (λ S, P S ∧ assertion_of_bexp b₁ S)
                      c₁ c₂ P →
    P ⇒ (λ S, eval_bexp S b₁ = eval_bexp S b₂) →
    P ⇒ (λ S, eval_bexp S b₁ ≠ None ∧ eval_bexp S b₂ ≠ None) →
    minimal_rhl_proof P
                      (While b₁ c₁) (While b₂ c₂)
                      (λ S, P S ∧ assertion_of_bexp (NOT b₁) S)
  | MinimalSub: ∀ P P' Q Q' c₁ c₂,
    minimal_rhl_proof P c₁ c₂ Q →
    P' ⇒ P →
    Q ⇒ Q' →
    minimal_rhl_proof P' c₁ c₂ Q'.

  Inductive core_rhl_proof :
    assertion → cmd → cmd → assertion → Type :=
  | CoreSkip : ∀ P,
    core_rhl_proof P Skip Skip P
  | CoreAssign : ∀ P x e y e',
    core_rhl_proof (P [x ↦ e] [y ↦ e']) (Assign x e) (Assign y e') P
  | CoreAssert : ∀ P b₁ b₂,
    P ⇒ (λ S, (assertion_of_bexp b₁) S ∧ (assertion_of_bexp b₂) S) →
    core_rhl_proof P (Assert b₁) (Assert b₂) P
  | CoreSeq : ∀ P Q R c₁₁ c₂₁ c₁₂ c₂₂,
    core_rhl_proof P c₁₁ c₂₁ Q →
    core_rhl_proof Q c₁₂ c₂₂ R →
    core_rhl_proof P (Seq c₁₁ c₁₂) (Seq c₂₁ c₂₂) R
  | CoreITE : ∀ P Q b₁ b₂ c₁₁ c₂₁ c₁₂ c₂₂,
    core_rhl_proof (λ S, P S ∧ assertion_of_bexp b₁ S)
                   c₁₁ c₂₁ Q →
    core_rhl_proof (λ S, P S ∧ assertion_of_bexp (NOT b₁) S)
                   c₁₂ c₂₂ Q →
    P ⇒ (λ S, eval_bexp S b₁ = eval_bexp S b₂) →
    P ⇒ (λ S, eval_bexp S b₁ ≠ None ∧ eval_bexp S b₂ ≠ None) →
    core_rhl_proof P (ITE b₁ c₁₁ c₁₂) (ITE b₂ c₂₁ c₂₂) Q
  | CoreWhile : ∀ P b₁ b₂ c₁ c₂,
    core_rhl_proof (λ S, P S ∧ assertion_of_bexp b₁ S)
                   c₁ c₂ P →
    P ⇒ (λ S, eval_bexp S b₁ = eval_bexp S b₂) →
    P ⇒ (λ S, eval_bexp S b₁ ≠ None ∧ eval_bexp S b₂ ≠ None) →
    core_rhl_proof P
                   (While b₁ c₁) (While b₂ c₂)
                   (λ S, P S ∧ assertion_of_bexp (NOT b₁) S)
  | CoreSub: ∀ P P' Q Q' c₁ c₂,
    core_rhl_proof P c₁ c₂ Q →
    P' ⇒ P →
    Q ⇒ Q' →
    core_rhl_proof P' c₁ c₂ Q'
  
  
  | CoreAssignLeft : ∀ P Q x e c,
    core_rhl_proof P Skip c Q →
    core_rhl_proof (P [ x ↦ e ]) (Assign x e) c Q
  | CoreAssignRight : ∀ P Q x e c,
    core_rhl_proof P c Skip Q →
    core_rhl_proof (P [ x ↦ e ]) c (Assign x e) Q
  
  | CoreAssertLeft : ∀ P Q b c,
    core_rhl_proof P Skip c Q →
    P ⇒ (λ S, assertion_of_bexp b S) →
    core_rhl_proof P (Assert b) c Q
  | CoreAssertRight : ∀ P Q b c,
    core_rhl_proof P c Skip Q →
    P ⇒ (λ S, assertion_of_bexp b S) →
    core_rhl_proof P c (Assert b) Q
  
  | CoreSeqSkipLeft : ∀ P Q R c₁₁ c₁₂ c₂,
      core_rhl_proof P c₁₁ Skip Q →
      core_rhl_proof Q c₁₂ c₂ R →
      core_rhl_proof P (Seq c₁₁ c₁₂) c₂ R
  | CoreSeqSkipRight : ∀ P Q R c₁ c₂₁ c₂₂,
      core_rhl_proof P Skip c₂₁ Q →
      core_rhl_proof Q c₁ c₂₂ R →
      core_rhl_proof P c₁ (Seq c₂₁ c₂₂) R
  
  | CoreITELeft : ∀ P Q b c₁ c₂ c,
    core_rhl_proof (λ S, P S ∧ assertion_of_bexp b S) c₁ c Q →
    core_rhl_proof (λ S, P S ∧ assertion_of_bexp (NOT b) S) c₂ c Q →
    P ⇒ (λ S, eval_bexp S b ≠ None) →
    core_rhl_proof P (ITE b c₁ c₂) c Q
  | CoreITERight : ∀ P Q b c₁ c₂ c,
    core_rhl_proof (λ S, P S ∧ assertion_of_bexp b S) c c₁ Q →
    core_rhl_proof (λ S, P S ∧ assertion_of_bexp (NOT b) S) c c₂ Q →
    P ⇒ (λ S, eval_bexp S b ≠ None) →
    core_rhl_proof P c (ITE b c₁ c₂) Q.

  Inductive core_rhl_sc_proof :
    assertion → cmd → cmd → assertion → Type :=
  | CoreSCSkip : ∀ P,
    core_rhl_sc_proof P Skip Skip P
  | CoreSCAssign : ∀ P x e y e',
    core_rhl_sc_proof (P [x ↦ e] [y ↦ e']) (Assign x e) (Assign y e') P
  | CoreSCAssert : ∀ P b₁ b₂,
    P ⇒ (λ S, (assertion_of_bexp b₁) S ∧ (assertion_of_bexp b₂) S) →
    core_rhl_sc_proof P (Assert b₁) (Assert b₂) P
  | CoreSCSeq : ∀ P Q R c₁₁ c₂₁ c₁₂ c₂₂,
    core_rhl_sc_proof P c₁₁ c₂₁ Q →
    core_rhl_sc_proof Q c₁₂ c₂₂ R →
    core_rhl_sc_proof P (Seq c₁₁ c₁₂) (Seq c₂₁ c₂₂) R
  | CoreSCITE : ∀ P Q b₁ b₂ c₁₁ c₂₁ c₁₂ c₂₂,
    core_rhl_sc_proof (λ S, P S ∧ assertion_of_bexp b₁ S)
                      c₁₁ c₂₁ Q →
    core_rhl_sc_proof (λ S, P S ∧ assertion_of_bexp (NOT b₁) S)
                      c₁₂ c₂₂ Q →
    P ⇒ (λ S, eval_bexp S b₁ = eval_bexp S b₂) →
    P ⇒ (λ S, eval_bexp S b₁ ≠ None ∧ eval_bexp S b₂ ≠ None) →
    core_rhl_sc_proof P (ITE b₁ c₁₁ c₁₂) (ITE b₂ c₂₁ c₂₂) Q
  | CoreSCWhile : ∀ P b₁ b₂ c₁ c₂,
    core_rhl_sc_proof (λ S, P S ∧ assertion_of_bexp b₁ S)
                      c₁ c₂ P →
    P ⇒ (λ S, eval_bexp S b₁ = eval_bexp S b₂) →
    P ⇒ (λ S, eval_bexp S b₁ ≠ None ∧ eval_bexp S b₂ ≠ None) →
    core_rhl_sc_proof P
                      (While b₁ c₁) (While b₂ c₂)
                      (λ S, P S ∧ assertion_of_bexp (NOT b₁) S)
  | CoreSCSub: ∀ P P' Q Q' c₁ c₂,
    core_rhl_sc_proof P c₁ c₂ Q →
    P' ⇒ P →
    Q ⇒ Q' →
    core_rhl_sc_proof P' c₁ c₂ Q'
  
  
  | CoreSCAssignLeft : ∀ P Q x e c,
    core_rhl_sc_proof P Skip c Q →
    core_rhl_sc_proof (P [ x ↦ e ]) (Assign x e) c Q
  | CoreSCAssignRight : ∀ P Q x e c,
    core_rhl_sc_proof P c Skip Q →
    core_rhl_sc_proof (P [ x ↦ e ]) c (Assign x e) Q
  
  | CoreSCAssertLeft : ∀ P Q b c,
    core_rhl_sc_proof P Skip c Q →
    P ⇒ (λ S, assertion_of_bexp b S) →
    core_rhl_sc_proof P (Assert b) c Q
  | CoreSCAssertRight : ∀ P Q b c,
    core_rhl_sc_proof P c Skip Q →
    P ⇒ (λ S, assertion_of_bexp b S) →
    core_rhl_sc_proof P c (Assert b) Q
  
  | CoreSCSeqSkipLeft : ∀ P Q R c₁₁ c₁₂ c₂,
      core_rhl_sc_proof P c₁₁ Skip Q →
      core_rhl_sc_proof Q c₁₂ c₂ R →
      core_rhl_sc_proof P (Seq c₁₁ c₁₂) c₂ R
  | CoreSCSeqSkipRight : ∀ P Q R c₁ c₂₁ c₂₂,
      core_rhl_sc_proof P Skip c₂₁ Q →
      core_rhl_sc_proof Q c₁ c₂₂ R →
      core_rhl_sc_proof P c₁ (Seq c₂₁ c₂₂) R
  
  | CoreSCITELeft : ∀ P Q b c₁ c₂ c,
    core_rhl_sc_proof (λ S, P S ∧ assertion_of_bexp b S) c₁ c Q →
    core_rhl_sc_proof (λ S, P S ∧ assertion_of_bexp (NOT b) S) c₂ c Q →
    P ⇒ (λ S, eval_bexp S b ≠ None) →
    core_rhl_sc_proof P (ITE b c₁ c₂) c Q
  | CoreSCITERight : ∀ P Q b c₁ c₂ c,
    core_rhl_sc_proof (λ S, P S ∧ assertion_of_bexp b S) c c₁ Q →
    core_rhl_sc_proof (λ S, P S ∧ assertion_of_bexp (NOT b) S) c c₂ Q →
    P ⇒ (λ S, eval_bexp S b ≠ None) →
    core_rhl_sc_proof P c (ITE b c₁ c₂) Q
  | CoreSCSelfComp : ∀ P Q c₁ c₂,
      hoare_proof P (Seq c₁ c₂) Q →
      core_rhl_sc_proof P c₁ c₂ Q.
End Make.