---

Step * of Lemma C_Struct_vs_DVALp

∀store:C_STOREp(). ∀ctyp:C_TYPE(). ∀env:C_TYPE_env(). ∀dval:C_DVALUEp().
  (C_STOREp-welltyped(env;store)
  ⇒ (↑C_Struct?(ctyp))
  ⇒ C_TYPE_vs_DVALp(env;ctyp) dval 
     = if DVp_Struct?(dval)
       then let r = map(λp.<fst(p), C_TYPE_vs_DVALp(env;snd(p))>;C_Struct-fields(ctyp)) in
             let lbls = DVp_Struct-lbls(dval) in
             let g = DVp_Struct-struct(dval) in
             (∀p∈r.let a,wt = p 
                   in a ∈b lbls) ∧b (wt (g a)))_b
       else ff
       fi )
BY
{ ((D 0 THENA Auto)
   THEN BLemma `C_TYPE-induction`
   THEN Reduce 0
   THEN (RepUR ``let`` 0 THEN Auto)
   THEN UnfoldAtAddr [2;1] 0⋅
   THEN Reduce 0
   THEN AutoSplit
   THEN Fold `C_TYPE_vs_DVALp` 0
   THEN RepUR ``let`` 0
   THEN Auto) }

1
1. store : C_STOREp()@i
2. fields : (Atom × C_TYPE()) List@i
3. (∀u∈fields.let u1,u2 = u 
              in ∀env:C_TYPE_env(). ∀dval:C_DVALUEp().
                   (C_STOREp-welltyped(env;store)
                   ⇒ (↑C_Struct?(u2))
                   ⇒ C_TYPE_vs_DVALp(env;u2) dval 
                      = if DVp_Struct?(dval)
                        then (∀p∈map(λp.<fst(p), C_TYPE_vs_DVALp(env;snd(p))>;C_Struct-fields(u2)).
                                let a,wt = p 
                                in a ∈b DVp_Struct-lbls(dval)) ∧b (wt (DVp_Struct-struct(dval) a)))_b
                        else ff
                        fi ))@i
4. env : C_TYPE_env()@i
5. dval : C_DVALUEp()@i
6. C_STOREp-welltyped(env;store)@i
7. True@i
8. ↑DVp_Struct?(dval)
⊢ bdd-all(||fields||;i.eval a = fst(fields[i]) in
                       a ∈b DVp_Struct-lbls(dval))
                       ∧b (let v2,v3 = fields[i] in C_TYPE_vs_DVALp(env;v3) (DVp_Struct-struct(dval) a))) 
= (∀p∈map(λp.<fst(p), C_TYPE_vs_DVALp(env;snd(p))>;fields).let a,wt = p 
                                                           in a ∈b DVp_Struct-lbls(dval))
                                                              ∧b (wt (DVp_Struct-struct(dval) a)))_b

---

Latex:


\mforall{}store:C\_STOREp().  \mforall{}ctyp:C\_TYPE().  \mforall{}env:C\_TYPE\_env().  \mforall{}dval:C\_DVALUEp().
    (C\_STOREp-welltyped(env;store)
    {}\mRightarrow{}  (\muparrow{}C\_Struct?(ctyp))
    {}\mRightarrow{}  C\_TYPE\_vs\_DVALp(env;ctyp)  dval 
          =  if  DVp\_Struct?(dval)
              then  let  r  =  map(\mlambda{}p.<fst(p),  C\_TYPE\_vs\_DVALp(env;snd(p))>C\_Struct-fields(ctyp))  in
                          let  lbls  =  DVp\_Struct-lbls(dval)  in
                          let  g  =  DVp\_Struct-struct(dval)  in
                          (\mforall{}p\mmember{}r.let  a,wt  =  p 
                                      in  a  \mmember{}\msubb{}  lbls)  \mwedge{}\msubb{}  (wt  (g  a)))\_b
              else  ff
              fi  )


By

((D  0  THENA  Auto)
  THEN  BLemma  `C\_TYPE-induction`
  THEN  Reduce  0
  THEN  (RepUR  ``let``  0  THEN  Auto)
  THEN  UnfoldAtAddr  [2;1]  0\mcdot{}
  THEN  Reduce  0
  THEN  AutoSplit
  THEN  Fold  `C\_TYPE\_vs\_DVALp`  0
  THEN  RepUR  ``let``  0
  THEN  Auto)

---

Home Index