Library Scat.Conditions

Syntax and semantics of conditions

Conditions are zeroth order formula used as boolean expressions in programs

Require Export ZArith.
Require Export ZArith_dec.
Require Export String.
Require Import PArith.
Require Import PArith.POrderedType.
Require Export MiscUtils.

Open Scope Z_scope.

Inductive binop : Set := PLUS | MINUS | MULT | DIV.

Definition evalop (op: binop) : Z → Z → Z
:= match op with PLUS ⇒ Zplus | MINUS ⇒ Zminus | MULT ⇒ Zmult | DIV ⇒ Zdiv end.

An abstract type of values: useful to avoid computations on values during proofs.

Module Type ValueTypeAbstraction.

Parameter value: Set.
Parameter vcte: Z → value.
Parameter Zof: value → Z.

Parameter Zof_vcte: ∀ z, Zof (vcte z) = z.
Parameter vcte_Zof: ∀ v, vcte (Zof v) = v.

Parameter vbin: binop → value → value → value.

Parameter Zof_vbin: ∀ op v1 v2, Zof (vbin op v1 v2) = evalop op (Zof v1) (Zof v2).

End ValueTypeAbstraction.

Module Value: ValueTypeAbstraction.

Definition value := Z.
Definition vcte := fun (x:Z) ⇒ x.
Definition Zof := vcte.
Definition vbin := evalop.

Lemma Zof_vcte: ∀ z, Zof (vcte z) = z.
Proof.
  auto.
Qed.

Lemma vcte_Zof: ∀ v, vcte (Zof v) = v.
Proof.
  auto.
Qed.

Lemma Zof_vbin: ∀ op v1 v2, Zof (vbin op v1 v2) = evalop op (Zof v1) (Zof v2).
Proof.
  auto.
Qed.

End Value.

Export Value.

Lemma Zof_intro v1 v2: Zof v1 = Zof v2 → v1 = v2.
Proof.
  intros; rewrite <- (vcte_Zof v1). rewrite <- (vcte_Zof v2).
  eqtriv.
Qed.

Hint Rewrite Zof_vcte Zof_vbin: zof_value.

Inductive vle (n1 n2: value): Prop :=
| vlecons: (Zof n1) ≤ (Zof n2) → vle n1 n2.

Below, each ctefun x (with x:positive) represents a symbol of unary function. (e.g. an unidimensional constant array)

We may reason on such an array by using axioms...

Parameter ctefun: positive → value → value.

Lemma ctefun_Zof (x:positive) (v: value): ctefun x v = ctefun x (vcte (Zof v)).
Proof.
rewrite vcte_Zof.
auto.
Qed.

Syntax of terms (expressions computing only in Z)

Record var: Set := mkvar {
vtag: string ;

this is for pretty-printing only

vid: positive

identifier of the variable

}.

Inductive term: Set :=
  | tvar (x: var)
  | tcte (c: Z)
  | tbin (op: binop) (tl tr: term)
  | told (t:term)
  | tapp (f:var) (t:term).

Coercion tvar: var >-> term.
Coercion tcte: Z >-> term.

Semantics of terms. A state is a mapping from variable identifiers to values

Definition state := positive → value.

Fixpoint teval (t:term) (s: state) : value :=
match t with
| tvar x ⇒ s (vid x)
| tcte c ⇒ vcte c
| tbin op tl tr ⇒ vbin op (teval tl s) (teval tr s)
| told t ⇒ teval t s
| tapp f t ⇒ ctefun (vid f) (teval t s)
end.

Definition ext (s s': state) := ∀ x, s x = s' x.

Lemma ext_teval (t: term): ∀ s s',
   ext s s' →
      teval t s = teval t s'.
Proof.
  induction t; simpl; intuition.
  erewrite IHt1; eauto.
  erewrite IHt2; eauto.
  erewrite IHt; eauto.
Qed.

add x val s = push the pair (x,val) into s

Definition add (x: positive) (val:value) (s: state) : state
  := fun x' ⇒ if Positive_as_DT.eq_dec x x' then val else (s x').

Lemma add_in x val s: add x val s x = val.
Proof.
  unfold add.
  case (Positive_as_DT.eq_dec x x); tauto.
Qed.

Hint Resolve add_in: checker.

Lemma add_out x val s x': (Zpos x )<>(Zpos x') → add x val s x' = s x'.
Proof.
  unfold add; case (Positive_as_DT.eq_dec x x'); try (intros; subst; tauto).
Qed.

Hint Resolve add_out: checker.

Lemma add_out2 x val s x': x ≠x' → add x val s x' = s x'.
Proof.
  unfold add; case (Positive_as_DT.eq_dec x x'); try (intros; subst; tauto).
Qed.

Hint Resolve add_out2: checker.

Lemma add_id x y s: add x (s x) s y = s y.
Proof.
  unfold add; intros. case (Positive_as_DT.eq_dec x y); auto.
  intros H; inversion_clear H; auto.
Qed.

Hint Rewrite add_id: rchecker.

Syntax of conditions

Inductive bincmp : Set := LE | EQ.

Definition evalcmp (cmp: bincmp): value → value → Prop
:= match cmp with LE ⇒ vle | EQ ⇒ @eq value end.

Inductive binlog: Set := AND | OR.

Definition evallog (og: binlog) : Prop → Prop → Prop
:= if og then and else or.

Inductive cond: Set :=
  | basic (b: bool)
  | atom (oc: bincmp) (tl tr: term)
  | bin (og: binlog) (cl cr: cond)
  | not (c: cond).

Definition ceq (x:var) (t:term) := atom EQ (tvar x) t.
Definition tauto := basic true.
Definition absurd := basic false.

Semantics of conditions

Fixpoint eval (c:cond) (s: state): Prop :=
     match c with
     | basic b ⇒ Is_true b
     | atom oc tl tr ⇒ evalcmp oc (teval tl s) (teval tr s)
     | bin og cl cr ⇒ evallog og (eval cl s) (eval cr s)
     | not c ⇒ ~(eval c s )
     end.

Lemma ext_eval c: ∀ s s',
  ext s s' →
     eval c s = eval c s'.
Proof.
  induction c; simpl; intuition.
  erewrite ext_teval; eauto.
  erewrite ext_teval with (s:=s); eauto.
  erewrite IHc1; eauto.
  erewrite IHc2; eauto.
  erewrite IHc; eauto.
Qed.

Semantics of told

Fixpoint oteval (t:term) (old new: state) : value :=
match t with
| tvar x ⇒ new (vid x)
| tcte c ⇒ vcte c
| tbin op tl tr ⇒ vbin op (oteval tl old new) (oteval tr old new)
| told t ⇒ teval t old
| tapp f t ⇒ ctefun (vid f) (oteval t old new)
end.

Lemma oteval_teval t s: oteval t s s = teval t s.
Proof.
  induction t; simpl; congruence.
Qed.
Hint Rewrite oteval_teval: rchecker.

Fixpoint oeval (c:cond) (old new: state): Prop :=
     match c with
     | basic b ⇒ Is_true b
     | atom oc tl tr ⇒ evalcmp oc (oteval tl old new) (oteval tr old new)
     | bin og cl cr ⇒ evallog og (oeval cl old new) (oeval cr old new)
     | not c ⇒ ~(oeval c old new )
     end.

Lemma oeval_eval c s: oeval c s s = eval c s.
Proof.
  induction c; simpl; autorewrite with rchecker; try congruence.
Qed.
Hint Rewrite oeval_eval: rchecker.

lframeeq l s s' indicates that only variables in the frame l (a list of variables) may have changed between states s and s'.

Open Scope list_scope.

Fixpoint labsent (x:positive) (l: list var) : Prop :=
  match l with
  | nil ⇒ True
  | y::l ⇒ x <>(vid y) ∧ (labsent x l )
  end.

Definition lframeeq (l:list var) (s s': state) : Prop
:= ∀ x, labsent x l → (s x )=(s' x ).
Hint Unfold lframeeq: checker.

Syntactic equalities: necessary only for concrete conditions

Definition binop_eq (x y: binop) :=
  match x,y with
  | PLUS, PLUS ⇒ true
  | MINUS, MINUS ⇒ true
  | MULT, MULT ⇒ true
  | DIV, DIV ⇒ true
  | _,_ ⇒ false
  end.

Lemma binop_eq_eq x y: binop_eq x y =true → x =y.
Proof.
  decide_eqb_eq x y.
Qed.
Hint Resolve binop_eq_eq: eqtrue.

NB: lemma only used here to check binop_eq

Lemma binop_eq_refl x: binop_eq x x =true.
Proof.
  destruct x; simpl; auto.
Qed.

Definition var_eq (x1 x2: var) := Peqb (vid x1) (vid x2).

Lemma var_eq_eq x y: var_eq x y = true → (vid x )=(vid y ).
Proof.
  unfold var_eq; eqtrue.
Qed.
Hint Resolve var_eq_eq: eqtrue.

Fixpoint term_eq (t1 t2: term) :=
  match t1,t2 with
  | tvar x1, tvar x2 ⇒ var_eq x1 x2
  | tcte c1, tcte c2 ⇒ Zeq_bool c1 c2
  | tbin op1 tl1 tr1, tbin op2 tl2 tr2 ⇒
      binop_eq op1 op2 &&& term_eq tl1 tl2 &&& term_eq tr1 tr2
  | told t1, told t2 ⇒ term_eq t1 t2
  | tapp f1 t1, tapp f2 t2 ⇒ var_eq f1 f2 &&& term_eq t1 t2
  | _, _ ⇒ false
  end.

Lemma term_eq_eval t1 t2 s: term_eq t1 t2 = true → teval t1 s =teval t2 s.
Proof.
  decide_eqb_eq t1 t2; eqtrue; intros; eqtriv.
Qed.
Hint Resolve term_eq_eval: eqtrue.

Lemma term_eq_oeval t1 t2 old s: term_eq t1 t2 = true → oteval t1 old s =oteval t2 old s.
Proof.
  decide_eqb_eq t1 t2; eqtrue; simpl; intros; eqtriv.
Qed.
Hint Resolve term_eq_oeval: eqtrue.

Definition bincmp_eq (x y: bincmp) :=
  match x,y with
  | LE, LE ⇒ true
  | EQ, EQ ⇒ true
  | _,_ ⇒ false
  end.

Lemma bincmp_eq_eq x y: bincmp_eq x y =true → x =y.
Proof.
  decide_eqb_eq x y.
Qed.
Hint Resolve bincmp_eq_eq: eqtrue.

NB: lemma only used here to check bincmp_eq

Lemma bincmp_eq_refl x: bincmp_eq x x =true.
Proof.
  destruct x; simpl; auto.
Qed.

Definition binlog_eq (x y: binlog) :=
  match x,y with
  | AND, AND ⇒ true
  | OR, OR ⇒ true
  | _,_ ⇒ false
  end.

Lemma binlog_eq_eq x y: binlog_eq x y =true → x =y.
Proof.
  decide_eqb_eq x y.
Qed.
Hint Resolve binlog_eq_eq: eqtrue.

NB: lemma only used here to check binlog_eq

Lemma binlog_eq_refl x: binlog_eq x x =true.
Proof.
  destruct x; simpl; auto.
Qed.

Fixpoint cond_eq (c1 c2: cond) :=
  match c1, c2 with
  | basic b1, basic b2 ⇒ eqb b1 b2
  | atom oc1 tl1 tr1, atom oc2 tl2 tr2 ⇒
      bincmp_eq oc1 oc2 &&&
      term_eq tl1 tl2 &&&
      term_eq tr1 tr2
  | bin og1 cl1 cr1, bin og2 cl2 cr2 ⇒
       binlog_eq og1 og2 &&&
       cond_eq cl1 cl2 &&&
       cond_eq cr1 cr2
  | not c1, not c2 ⇒ cond_eq c1 c2
  | _, _ ⇒ false
  end.

Lemma cond_eq_eval c1 c2 s: cond_eq c1 c2 = true → eval c1 s =eval c2 s.
Proof.
  decide_eqb_eq c1 c2; eqtrue; intros; eqtriv.
Qed.
Hint Resolve cond_eq_eval: eqtrue.

Lemma cond_eq_oeval c1 c2 old s: cond_eq c1 c2 = true → oeval c1 old s =oeval c2 old s.
Proof.
  decide_eqb_eq c1 c2; eqtrue; simpl; intros; eqtriv.
Qed.
Hint Resolve cond_eq_oeval: eqtrue.

Equality of frames (list of variables)

Fixpoint lvar_eq (l1 l2: list var) :=
  match l1, l2 with
  | nil, nil ⇒ true
  | x1::l1, x2::l2 ⇒ var_eq x1 x2 &&& lvar_eq l1 l2
  | _, _ ⇒ false
  end.

Lemma lvar_eq_labsent l1 l2 x: lvar_eq l1 l2 = true → labsent x l1 =labsent x l2.
Proof.
  decide_eqb_eq l1 l2; eqtrue; intros; eqtriv.
Qed.
Hint Resolve lvar_eq_labsent: eqtrue.

Lemma lvar_eq_lframeeq l1 l2 s s':
lvar_eq l1 l2 = true → lframeeq l2 s s' → lframeeq l1 s s'.
Proof.
unfold lframeeq. intros H H0 x H1. apply H0; erewrite <- lvar_eq_labsent; eauto.
Qed.
Hint Resolve lvar_eq_lframeeq: eqtrue.

Substitution on terms

Fixpoint tsubst (t:term) (x: positive) t2: term :=
match t with
| tvar x' ⇒ if Positive_as_DT.eq_dec x (vid x') then t2 else t
| tcte c ⇒ t
| tbin op tl tr ⇒ tbin op (tsubst tl x t2) (tsubst tr x t2)
| told t ⇒ tsubst t x t2
| tapp f t ⇒ tapp f (tsubst t x t2)
end.

Lemma tsubst_teval t x t2 s:
  teval (tsubst t x t2) s = teval t (add x (teval t2 s) s).
Proof.
  induction t; simpl; auto.
  unfold add; case (Positive_as_DT.eq_dec x (vid x0)); simpl; auto.
  rewrite IHt1; rewrite IHt2; auto.
  rewrite IHt; auto.
Qed.