Properties of the Same predicate on Terms

This file contains lemmas about the Same predicate on Terms.

theorem Cedar.Thm.same_results_implies_exists_outcome {res : Spec.Result Spec.Value} {t : SymCC.Term} : res ∼ t → ∃ (o : Spec.Outcome Spec.Value), res ∼ o ∧ o ∼ t

theorem Cedar.Thm.same_outcomes_implies_eq {o₁ o₂ : Spec.Outcome Spec.Value} {t : SymCC.Term} : o₁ ∼ t → o₂ ∼ t → o₁ = o₂

theorem Cedar.Thm.same_error_implies {e : Spec.Error} {t : SymCC.Term} : Except.error e ∼ t → ¬e = Spec.Error.entityDoesNotExist ∧ ∃ (ty : SymCC.TermType), t = SymCC.Term.none ty

theorem Cedar.Thm.same_error_implies_ifSome_error {e : Spec.Error} {t₁ t₂ : SymCC.Term} {ty₂ : SymCC.TermType} : Except.error e ∼ t₁ → t₂.typeOf = ty₂.option → Except.error e ∼ SymCC.Factory.ifSome t₁ t₂

theorem Cedar.Thm.same_error_implies_ifAllSome_error {e : Spec.Error} {ts : List SymCC.Term} {t₁ t₂ : SymCC.Term} {ty₂ : SymCC.TermType} : Except.error e ∼ t₁ → t₁ ∈ ts → t₂.typeOf = ty₂.option → Except.error e ∼ SymCC.Factory.ifAllSome ts t₂

theorem Cedar.Thm.same_error_implied_by {e : Spec.Error} {ty : SymCC.TermType} : ¬e = Spec.Error.entityDoesNotExist → Except.error e ∼ SymCC.Term.none ty

theorem Cedar.Thm.same_error_foldr_ifSome {e : Spec.Error} {ts : List SymCC.Term} {P : SymCC.Term} {ty : SymCC.TermType} {tⱼ : SymCC.Term} (hP : P.typeOf = ty.option) (hj : tⱼ ∈ ts) (hsame : Except.error e ∼ tⱼ) : Except.error e ∼ List.foldr (fun (tᵢ acc : SymCC.Term) => SymCC.Factory.ifSome tᵢ acc) P ts

If some guard in the list corresponds to an errored evaluation (so it is a none), the whole ifSome fold reduces to that error.

theorem Cedar.Thm.same_ok_implies {v : Spec.Value} {t : SymCC.Term} : Except.ok v ∼ t → ∃ (t' : SymCC.Term), t = t'.some ∧ v ∼ t'

theorem Cedar.Thm.same_ok_some_implies {v : Spec.Value} {t : SymCC.Term} : Except.ok v ∼ t.some → v ∼ t

theorem Cedar.Thm.same_ok_some_iff {v : Spec.Value} {t : SymCC.Term} : Except.ok v ∼ t.some ↔ v ∼ t

theorem Cedar.Thm.same_some_implies_ok {r : Spec.Result Spec.Value} {t : SymCC.Term} : r ∼ t.some → ∃ (v : Spec.Value), r = Except.ok v ∧ v ∼ t

theorem Cedar.Thm.same_values_def {v : Spec.Value} {t : SymCC.Term} : v ∼ t ↔ t.value? = some v

theorem Cedar.Thm.same_value_implies_same {v : Spec.Value} {t : SymCC.Term} : SymCC.SameValues v t → v ∼ t

theorem Cedar.Thm.same_implies_same_value {v : Spec.Value} {t : SymCC.Term} : v ∼ t → SymCC.SameValues v t

theorem Cedar.Thm.same_value_implies_lit {v : Spec.Value} {t : SymCC.Term} : v ∼ t → t.isLiteral = true

theorem Cedar.Thm.same_ok_value_implies_lit {v : Spec.Value} {t : SymCC.Term} : Except.ok v ∼ t → t.isLiteral = true

theorem Cedar.Thm.same_bool_term_implies {v : Spec.Value} {b : Bool} : v ∼ SymCC.Term.prim (SymCC.TermPrim.bool b) → v = Spec.Value.prim (Spec.Prim.bool b)

theorem Cedar.Thm.same_ok_bool_term_implies {v : Spec.Value} {b : Bool} : Except.ok v ∼ (SymCC.Term.prim (SymCC.TermPrim.bool b)).some → v = Spec.Value.prim (Spec.Prim.bool b)

theorem Cedar.Thm.same_bool_implies {b : Bool} {t : SymCC.Term} : Spec.Value.prim (Spec.Prim.bool b) ∼ t → t = SymCC.Term.prim (SymCC.TermPrim.bool b)

theorem Cedar.Thm.same_ok_bool_implies {b : Bool} {t : SymCC.Term} : Except.ok (Spec.Value.prim (Spec.Prim.bool b)) ∼ t → t = (SymCC.Term.prim (SymCC.TermPrim.bool b)).some

theorem Cedar.Thm.same_bool {b : Bool} : Spec.Value.prim (Spec.Prim.bool b) ∼ SymCC.Term.prim (SymCC.TermPrim.bool b)

theorem Cedar.Thm.same_ok_bool {b : Bool} : Except.ok (Spec.Value.prim (Spec.Prim.bool b)) ∼ (SymCC.Term.prim (SymCC.TermPrim.bool b)).some

theorem Cedar.Thm.same_ok_bool_iff {b₁ b₂ : Bool} : b₁ = b₂ ↔ Except.ok (Spec.Value.prim (Spec.Prim.bool b₁)) ∼ (SymCC.Term.prim (SymCC.TermPrim.bool b₂)).some

theorem Cedar.Thm.same_set_term_implies {v : Spec.Value} {ts : Data.Set SymCC.Term} {ty : SymCC.TermType} : v ∼ SymCC.Term.set ts ty → ∃ (vs : Data.Set Spec.Value), v = Spec.Value.set vs ∧ (SymCC.Term.set ts ty).value? = some (Spec.Value.set vs)

theorem Cedar.Thm.same_set_implies {vs : Data.Set Spec.Value} {t : SymCC.Term} {ty : SymCC.TermType} : Spec.Value.set vs ∼ t → t.typeOf = ty.set → ∃ (ts : Data.Set SymCC.Term), t = SymCC.Term.set ts ty ∧ (SymCC.Term.set ts ty).value? = some (Spec.Value.set vs)

theorem Cedar.Thm.same_record_term_implies {v : Spec.Value} {rt : Data.Map Spec.Attr SymCC.Term} : SymCC.SameValues v (SymCC.Term.record rt) → ∃ (rv : Data.Map Spec.Attr Spec.Value), v = Spec.Value.record rv ∧ (SymCC.Term.record rt).value? = some (Spec.Value.record rv)

theorem Cedar.Thm.same_record_implies {avs : Data.Map Spec.Attr Spec.Value} {t : SymCC.Term} {rty : Data.Map Spec.Attr SymCC.TermType} : Spec.Value.record avs ∼ t → t.typeOf = SymCC.TermType.record rty → ∃ (ats : Data.Map Spec.Attr SymCC.Term), t = SymCC.Term.record ats ∧ (SymCC.Term.record ats).value? = some (Spec.Value.record avs)

@[simp]

theorem Cedar.Thm.value?_bool {b : Bool} : (SymCC.Term.prim (SymCC.TermPrim.bool b)).value? = some (Spec.Value.prim (Spec.Prim.bool b))

@[simp]

theorem Cedar.Thm.value?_entity {uid : Spec.EntityUID} : (SymCC.Term.prim (SymCC.TermPrim.entity uid)).value? = some (Spec.Value.prim (Spec.Prim.entityUID uid))

theorem Cedar.Thm.same_entity_term_implies {v : Spec.Value} {uid : Spec.EntityUID} : v ∼ SymCC.Term.prim (SymCC.TermPrim.entity uid) → v = Spec.Value.prim (Spec.Prim.entityUID uid)

theorem Cedar.Thm.same_entity_implies {uid : Spec.EntityUID} {t : SymCC.Term} : Spec.Value.prim (Spec.Prim.entityUID uid) ∼ t → t = SymCC.Term.prim (SymCC.TermPrim.entity uid)

theorem Cedar.Thm.same_string_term_implies {v : Spec.Value} {s : String} : v ∼ SymCC.Term.prim (SymCC.TermPrim.string s) → v = Spec.Value.prim (Spec.Prim.string s)

theorem Cedar.Thm.same_string_implies {s : String} {t : SymCC.Term} : Spec.Value.prim (Spec.Prim.string s) ∼ t → t = SymCC.Term.prim (SymCC.TermPrim.string s)

theorem Cedar.Thm.same_bitvec_term_implies {v : Spec.Value} {n : Nat} {bv : BitVec n} : v ∼ SymCC.Term.prim (SymCC.TermPrim.bitvec bv) → ∃ (i : Int64), v = Spec.Value.prim (Spec.Prim.int i) ∧ bv.toInt = i.toInt ∧ n = 64

theorem Cedar.Thm.same_bitvec64_term_implies {v : Spec.Value} {bv : BitVec 64} : v ∼ SymCC.Term.prim (SymCC.TermPrim.bitvec bv) → ∃ (i : Int64), v = Spec.Value.prim (Spec.Prim.int i) ∧ bv.toInt = i.toInt

theorem Cedar.Thm.same_int_implies {t : SymCC.Term} {bv : BitVec 64} {i : Int64} : bv.toInt = i.toInt → Spec.Value.prim (Spec.Prim.int i) ∼ t → t = SymCC.Term.prim (SymCC.TermPrim.bitvec bv)

theorem Cedar.Thm.same_int {i : Int} {bv : BitVec 64} (h₁ : Int64.MIN ≤ i ∧ i ≤ Int64.MAX) (h₂ : bv.toInt = i) : Spec.Value.prim (Spec.Prim.int (Int64.ofIntChecked i h₁)) ∼ SymCC.Term.prim (SymCC.TermPrim.bitvec bv)

theorem Cedar.Thm.same_bv {bv : BitVec 64} : Spec.Value.prim (Spec.Prim.int (Int64.ofInt bv.toInt)) ∼ SymCC.Term.prim (SymCC.TermPrim.bitvec bv)

theorem Cedar.Thm.same_int64 {i : Int64} : Spec.Value.prim (Spec.Prim.int i) ∼ SymCC.Term.prim (SymCC.TermPrim.bitvec i.toBitVec)

theorem Cedar.Thm.same_ext {x : Spec.Ext} : Spec.Value.ext x ∼ SymCC.Term.prim (SymCC.TermPrim.ext x)

theorem Cedar.Thm.same_ext_term_implies {v : Spec.Value} {x : Spec.Ext} : v ∼ SymCC.Term.prim (SymCC.TermPrim.ext x) → v = Spec.Value.ext x

theorem Cedar.Thm.same_ext_implies {x : Spec.Ext} {t : SymCC.Term} : Spec.Value.ext x ∼ t → t = SymCC.Term.prim (SymCC.TermPrim.ext x)

theorem Cedar.Thm.value?_some_implies_attrValue?_some {a : Spec.Attr} {tₐ : SymCC.Term} {vₐ : Spec.Value} (hv : tₐ.value? = some vₐ) : SymCC.Term.value?.attrValue? a tₐ = some (a, some vₐ)

theorem Cedar.Thm.value?_attrValue?_none_implies_none {a : Spec.Attr} {t : SymCC.Term} (hv : SymCC.Term.value?.attrValue? a t = some (a, none)) : ∃ (ty : SymCC.TermType), t = SymCC.Term.none ty

theorem Cedar.Thm.value?_attrValue?_some_implies_same {a : Spec.Attr} {t : SymCC.Term} {v : Spec.Value} : SymCC.Term.value?.attrValue? a t = some (a, some v) → match t.typeOf with | ty.option => ∃ (t' : SymCC.Term), t = t'.some ∧ v ∼ t' | x => v ∼ t

theorem Cedar.Thm.value?_attrValue?_fst {a : Spec.Attr} {t : SymCC.Term} {av : Spec.Attr × Option Spec.Value} : SymCC.Term.value?.attrValue? a t = some av → a = av.fst

theorem Cedar.Thm.record_value?_mapM' {rt : Data.Map Spec.Attr SymCC.Term} {rv : Data.Map Spec.Attr Spec.Value} (hr : (SymCC.Term.record rt).value? = some (Spec.Value.record rv)) : ∃ (avs : List (Spec.Attr × Option Spec.Value)), List.mapM' (fun (x : Spec.Attr × SymCC.Term) => SymCC.Term.value?.attrValue? x.fst x.snd) rt.toList = some avs ∧ Data.Map.mk (List.filterMap (fun (x : Spec.Attr × Option Spec.Value) => Option.map (Prod.mk x.fst) x.snd) avs) = rv

theorem Cedar.Thm.record_value_find? {a : Spec.Attr} {tₐ : SymCC.Term} {rt : Data.Map Spec.Attr SymCC.Term} {avs : List (Spec.Attr × Option Spec.Value)} (hf : rt.find? a = some tₐ) (hr : List.mapM' (fun (x : Spec.Attr × SymCC.Term) => SymCC.Term.value?.attrValue? x.fst x.snd) rt.toList = some avs) : ∃ (av : Spec.Attr × Option Spec.Value), av ∈ avs ∧ SymCC.Term.value?.attrValue? a tₐ = some av

theorem Cedar.Thm.record_value?_find?_required {a : Spec.Attr} {tₐ : SymCC.Term} {rt : Data.Map Spec.Attr SymCC.Term} {rv : Data.Map Spec.Attr Spec.Value} (hw : rt.WellFormed) (hty : ∀ (ty : SymCC.TermType), tₐ.typeOf = ty.option → False) (hf : rt.find? a = some tₐ) (hr : (SymCC.Term.record rt).value? = some (Spec.Value.record rv)) : ∃ (vₐ : Spec.Value), rv.find? a = some vₐ ∧ tₐ.value? = some vₐ

theorem Cedar.Thm.record_value?_find?_optional_some {a : Spec.Attr} {tₐ : SymCC.Term} {rt : Data.Map Spec.Attr SymCC.Term} {rv : Data.Map Spec.Attr Spec.Value} (hw : rt.WellFormed) (hf : rt.find? a = some tₐ.some) (hr : (SymCC.Term.record rt).value? = some (Spec.Value.record rv)) : ∃ (vₐ : Spec.Value), rv.find? a = some vₐ ∧ tₐ.value? = some vₐ

theorem Cedar.Thm.record_value?_find?_optional_none {a : Spec.Attr} {ty : SymCC.TermType} {rt : Data.Map Spec.Attr SymCC.Term} {rv : Data.Map Spec.Attr Spec.Value} (hw : rt.WellFormed) (hf : rt.find? a = some (SymCC.Term.none ty)) (hr : (SymCC.Term.record rt).value? = some (Spec.Value.record rv)) : rv.find? a = none

theorem Cedar.Thm.record_value?_find?_none {a : Spec.Attr} {rt : Data.Map Spec.Attr SymCC.Term} {rv : Data.Map Spec.Attr Spec.Value} (hw : rt.WellFormed) (hf : rt.find? a = none) (hr : (SymCC.Term.record rt).value? = some (Spec.Value.record rv)) : rv.find? a = none

theorem Cedar.Thm.same_prim_value_inj {v : Spec.Value} {p : SymCC.TermPrim} {t : SymCC.Term} : v ∼ SymCC.Term.prim p → v ∼ t → SymCC.Term.prim p = t

theorem Cedar.Thm.set_value?_implies_in_value {vs : Data.Set Spec.Value} {ts : Data.Set SymCC.Term} {ty : SymCC.TermType} : (SymCC.Term.set ts ty).value? = some (Spec.Value.set vs) → ∀ (t : SymCC.Term), t ∈ ts → ∃ (v : Spec.Value), v ∈ vs ∧ t.value? = some v

theorem Cedar.Thm.set_value?_implies_in_term {vs : Data.Set Spec.Value} {ts : Data.Set SymCC.Term} {ty : SymCC.TermType} : (SymCC.Term.set ts ty).value? = some (Spec.Value.set vs) → ∀ (v : Spec.Value), v ∈ vs → ∃ (t : SymCC.Term), t ∈ ts ∧ t.value? = some v

theorem Cedar.Thm.record_value?_some_implies {ats : List (Spec.Attr × SymCC.Term)} {avs : List (Spec.Attr × Spec.Value)} : (SymCC.Term.record (Data.Map.mk ats)).value? = some (Spec.Value.record (Data.Map.mk avs)) → ∃ (avs' : List (Spec.Attr × Option Spec.Value)), List.mapM (fun (x : Spec.Attr × SymCC.Term) => SymCC.Term.value?.attrValue? x.fst x.snd) ats = some avs' ∧ List.filterMap (fun (x : Spec.Attr × Option Spec.Value) => Option.map (Prod.mk x.fst) x.snd) avs' = avs

theorem Cedar.Thm.record_value?_some_implied_by {ats : List (Spec.Attr × SymCC.Term)} {avs : List (Spec.Attr × Spec.Value)} {avs' : List (Spec.Attr × Option Spec.Value)} : List.mapM (fun (x : Spec.Attr × SymCC.Term) => SymCC.Term.value?.attrValue? x.fst x.snd) ats = some avs' → List.filterMap (fun (x : Spec.Attr × Option Spec.Value) => Option.map (Prod.mk x.fst) x.snd) avs' = avs → (SymCC.Term.record (Data.Map.mk ats)).value? = some (Spec.Value.record (Data.Map.mk avs))

theorem Cedar.Thm.record_value?_cons {a : Spec.Attr} {t : SymCC.Term} {ats : List (Spec.Attr × SymCC.Term)} {avs : List (Spec.Attr × Spec.Value)} : (SymCC.Term.record (Data.Map.mk ((a, t) :: ats))).value? = some (Spec.Value.record (Data.Map.mk avs)) → ∃ (vₒ : Option Spec.Value), SymCC.Term.value?.attrValue? a t = some (a, vₒ) ∧ match vₒ with | some v => ∃ (avs' : List (Spec.Attr × Spec.Value)), avs = (a, v) :: avs' ∧ (SymCC.Term.record (Data.Map.mk ats)).value? = some (Spec.Value.record (Data.Map.mk avs')) | none => (SymCC.Term.record (Data.Map.mk ats)).value? = some (Spec.Value.record (Data.Map.mk avs))

theorem Cedar.Thm.record_value?_head_none {a : Spec.Attr} {t : SymCC.Term} {ats : List (Spec.Attr × SymCC.Term)} {avs : List (Spec.Attr × Spec.Value)} : List.SortedBy Prod.fst ((a, t) :: ats) → (SymCC.Term.record (Data.Map.mk ((a, t) :: ats))).value? = some (Spec.Value.record (Data.Map.mk avs)) → SymCC.Term.value?.attrValue? a t = some (a, none) → (Data.Map.mk avs).find? a = none

theorem Cedar.Thm.same_value_inj {t₁ t₂ : SymCC.Term} {v : Spec.Value} {εs : SymCC.SymEntities} : SymCC.Term.WellFormed εs t₁ → SymCC.Term.WellFormed εs t₂ → t₁.typeOf = t₂.typeOf → v ∼ t₁ → v ∼ t₂ → t₁ = t₂

theorem Cedar.Thm.term_value?_exists {t : SymCC.Term} {ty : Validation.CedarType} {εs : SymCC.SymEntities} : SymCC.Term.WellFormedLiteral εs t → t.typeOf.cedarType? = some ty → ∃ (v : Spec.Value), t.value? = some v