---

Step * 1 of Lemma C_Struct_vs_DVALp


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
BY
{ ((BLemma `iff_imp_equal_bool` THENA Auto)
   THEN (RWO "assert-bdd-all assert-bl-all" 0 THENA Auto)
   THEN DatatypeD 5
   THEN All Reduce
   THEN Try (Trivial)) }

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. lbls : Atom List
6. d2 : {a:Atom| (a ∈ lbls)}  ─→ C_DVALUEp()
7. C_STOREp-welltyped(env;store)@i
8. True@i
9. True
⊢ ∀i:ℕ||fields||. (↑eval a = fst(fields[i]) in a ∈b lbls) ∧b (let v2,v3 = fields[i] in C_TYPE_vs_DVALp(env;v3) (d2 a)))
⇐⇒ (∀p∈map(λp.<fst(p), C_TYPE_vs_DVALp(env;snd(p))>;fields).↑let a,wt = p 
                                                              in a ∈b lbls) ∧b (wt (d2 a)))

---

Latex:



1.  store  :  C\_STOREp()@i
2.  fields  :  (Atom  \mtimes{}  C\_TYPE())  List@i
3.  (\mforall{}u\mmember{}fields.let  u1,u2  =  u 
                            in  \mforall{}env:C\_TYPE\_env().  \mforall{}dval:C\_DVALUEp().
                                      (C\_STOREp-welltyped(env;store)
                                      {}\mRightarrow{}  (\muparrow{}C\_Struct?(u2))
                                      {}\mRightarrow{}  C\_TYPE\_vs\_DVALp(env;u2)  dval 
                                            =  if  DVp\_Struct?(dval)
                                                then  (\mforall{}p\mmember{}map(\mlambda{}p.<fst(p),  C\_TYPE\_vs\_DVALp(env;snd(p))>C\_Struct-fields(u2)).
                                                                let  a,wt  =  p 
                                                                in  a  \mmember{}\msubb{}  DVp\_Struct-lbls(dval))
                                                                      \mwedge{}\msubb{}  (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.  \muparrow{}DVp\_Struct?(dval)
\mvdash{}  bdd-all(||fields||;i.eval  a  =  fst(fields[i])  in
                                              a  \mmember{}\msubb{}  DVp\_Struct-lbls(dval))
                                              \mwedge{}\msubb{}  (let  v2,v3  =  fields[i] 
                                                      in  C\_TYPE\_vs\_DVALp(env;v3) 
                                                      (DVp\_Struct-struct(dval)  a))) 
=  (\mforall{}p\mmember{}map(\mlambda{}p.<fst(p),  C\_TYPE\_vs\_DVALp(env;snd(p))>fields).let  a,wt  =  p 
                                                                                                                      in  a  \mmember{}\msubb{}  DVp\_Struct-lbls(dval))
                                                                                                                            \mwedge{}\msubb{}  (wt  (DVp\_Struct-struct(dval)  a)))\_b


By

((BLemma  `iff\_imp\_equal\_bool`  THENA  Auto)
  THEN  (RWO  "assert-bdd-all  assert-bl-all"  0  THENA  Auto)
  THEN  DatatypeD  5
  THEN  All  Reduce
  THEN  Try  (Trivial))

---

Home Index