Qcert.NRA.Optim.TNRARewrite

Section TOptim.









  Context {m:basic_model}.

  Lemma tand_comm {τin} (op1 op2 opl opr: τin ⇝ Bool) :
    (`opl = `op2 ∧ `op1) →
    (`opr = `op2 ∧ `op1) →
    opl ≡τ opr.

  Lemma tand_comm_arrow {τin} (op1 op2:nra) :
    m ⊢ₐ τin ↦ Bool ⊧ (op1 ∧ op2) ⇒ (op2 ∧ op1).


  Lemma tselect_and_aux (x: data) τin τ (op op1 op2:nra) :
    op ▷ τin >=> (Coll τ) →
    op1 ▷ τ >=> Bool →
    op2 ▷ τ >=> Bool →
    x ▹ τin →
    brand_relation_brands ⊢ (σ⟨ op1 ⟩(σ⟨ op2 ⟩(op))) @ₐ x =
    brand_relation_brands ⊢ (σ⟨ op2 ∧ op1 ⟩(op)) @ₐ x.

  Lemma tselect_and {τin τ} (op opl opr: τin ⇝ (Coll τ)) (op1 op2:τ ⇝ Bool) :
    (`opl = σ⟨ `op1 ⟩(σ⟨ `op2 ⟩(`op))) →
    (`opr = σ⟨ `op2 ∧ `op1 ⟩(`op)) →
    (opl ≡τ opr).


  Lemma tselect_comm_nra {τin τ} (op1 op2:τ ⇝ Bool) (op opl opr: τin ⇝ (Coll τ)) :
    (`opl = σ⟨ `op1 ⟩(σ⟨ `op2 ⟩(`op))) →
    (`opr = σ⟨ `op2 ⟩(σ⟨ `op1 ⟩(`op))) →
    opl ≡τ opr.

  Lemma tselect_comm {τin τ} x (op: τin ⇝ (Coll τ)) (op1 op2:τ ⇝ Bool) :
    x ▹ τin →
    (brand_relation_brands ⊢ σ⟨ `op1 ⟩(σ⟨ `op2 ⟩(`op)) @ₐ x ) = (brand_relation_brands ⊢ σ⟨ `op2 ⟩(σ⟨ `op1 ⟩(`op)) @ₐ x).


  Definition tunbox_bool (y:{ x:data | x ▹ Bool }) : bool.

  Definition typed_nra_total_bool {τ} (op:τ ⇝ Bool):
    {x:data|(x ▹ τ)} → bool.

  Lemma typed_nra_total_bool_consistent {τ} (op:τ ⇝ Bool) (d: {x:data|(x ▹ τ)}) :
    match (brand_relation_brands ⊢ `op@ₐ`d) with
      | Some (dbool b) ⇒ Some b
      | _ ⇒ None
    end = Some (typed_nra_total_bool op d).

  Lemma typed_nra_total_bool_consistent2 {τ} (op:τ ⇝ Bool) (x:data) (pf:(x ▹ τ)) :
    match (brand_relation_brands ⊢ `op@ₐx) with
      | Some (dbool b) ⇒ Some b
      | _ ⇒ None
    end = Some (typed_nra_total_bool op (exist _ x pf)).

  Lemma typed_lifted_predicate {τ} (op:τ ⇝ Bool) (d:data):
    data_type d τ →
    ∃ b' : bool,
      (fun x' : data ⇒
         match brand_relation_brands ⊢ (`op)@ₐ x' with
           | Some (dbool b) ⇒ Some b
           | _ ⇒ None
         end) d = Some b'.

  Lemma lift_filter_remove_one_false (l:list data) (f:data → option bool) (a:data) :
    f a = Some false →
    (lift_filter f (remove_one a l)) = lift_filter f l.

  Lemma lift_filter_remove_one {τ} (l:list data) (f:data → option bool) (a:data) :
    Forall (fun d : data ⇒ data_type d τ) l →
    data_type a τ →
    (∀ d : data, data_type d τ → ∃ b' : bool, f d = Some b') →
    (lift_filter f (remove_one a l)) = lift (remove_one a) (lift_filter f l).

  Lemma remove_still_well_typed {τ} (l:list data) (a:data) :
    Forall (fun d : data ⇒ data_type d τ) l →
    Forall (fun d : data ⇒ data_type d τ) (remove_one a l).

  Lemma lift_filter_over_bminus {τ} (l1 l2 : list data) (f:data → option bool):
    Forall (fun d : data ⇒ data_type d τ) l1 →
    Forall (fun d : data ⇒ data_type d τ) l2 →
    Forall (fun d : data ⇒ data_type d τ) (bminus l1 l2) →
    (∀ d : data, data_type d τ → ∃ b' : bool, f d = Some b') →
    lift dcoll (lift_filter f (bminus l1 l2)) =
    match lift dcoll (lift_filter f l1) with
      | Some d1 ⇒
        match lift dcoll (lift_filter f l2) with
          | Some d2 ⇒ rondcoll2 bminus d1 d2
          | None ⇒ None
        end
      | None ⇒ None
    end.

  Lemma minus_select_distr {τin τ} (op:τ ⇝ Bool) (op1 op2 opl opr: τin ⇝ (Coll τ)) :
    (`opl = σ⟨`op⟩(`op1 − `op2)) →
    (`opr = σ⟨`op⟩(`op1) − σ⟨`op⟩(`op2)) →
    opl ≡τ opr.

End TOptim.