Qcert.Basic.Data.RData
Data is:
- nil - used for undefined results.
- nat - a number
- bool - true or false
- string - a character string
- coll - a bag
- drec - a record
Context {fdata:foreign_data}.
Inductive data : Set :=
| dunit : data
| dnat : Z → data
| dbool : bool → data
| dstring : string → data
| dcoll : list data → data
| drec : list (string × data) → data
| dleft : data → data
| dright : data → data
| dbrand : brands → data → data
| dforeign : foreign_data_type → data
.
Induction principles used as backbone for inductive proofs on data
Definition data_rect (P : data → Type)
(funit : P dunit)
(fnat : ∀ n : Z, P (dnat n))
(fbool : ∀ b : bool, P (dbool b))
(fstring : ∀ s : string, P (dstring s))
(fcoll : ∀ c : list data, Forallt P c → P (dcoll c))
(frec : ∀ r : list (string × data), Forallt (fun ab ⇒ P (snd ab)) r → P (drec r))
(fleft: ∀ d, P d → P (dleft d))
(fright: ∀ d, P d → P (dright d))
(fbrand: ∀ b d, P d → P (dbrand b d))
(fforeign: ∀ fd, P (dforeign fd))
:=
fix F (d : data) : P d :=
match d as d0 return (P d0) with
| dunit ⇒ funit
| dnat x ⇒ fnat x
| dbool x ⇒ fbool x
| dstring x ⇒ fstring x
| dcoll x ⇒ fcoll x ((fix F2 (c : list data) : Forallt P c :=
match c as c0 with
| nil ⇒ Forallt_nil _
| cons d c0 ⇒ @Forallt_cons _ P d c0 (F d) (F2 c0)
end) x)
| drec x ⇒ frec x ((fix F3 (r : list (string×data)) : Forallt (fun ab ⇒ P (snd ab)) r :=
match r as c0 with
| nil ⇒ Forallt_nil _
| cons sd c0 ⇒ @Forallt_cons _ (fun ab ⇒ P (snd ab)) sd c0 (F (snd sd)) (F3 c0)
end) x)
| dleft x ⇒ fleft _ (F x)
| dright x ⇒ fright _ (F x)
| dbrand b x ⇒ fbrand b _ (F x)
| dforeign fd ⇒ fforeign fd
end.
Definition data_ind (P : data → Prop)
(funit : P dunit)
(fnat : ∀ n : Z, P (dnat n))
(fbool : ∀ b : bool, P (dbool b))
(fstring : ∀ s : string, P (dstring s))
(fcoll : ∀ c : list data, Forall P c → P (dcoll c))
(frec : ∀ r : list (string × data), Forall (fun ab ⇒ P (snd ab)) r → P (drec r))
(fleft: ∀ d, P d → P (dleft d))
(fright: ∀ d, P d → P (dright d))
(fbrand: ∀ b d, P d → P (dbrand b d))
(fforeign: ∀ fd, P (dforeign fd))
:=
fix F (d : data) : P d :=
match d as d0 return (P d0) with
| dunit ⇒ funit
| dnat x ⇒ fnat x
| dbool x ⇒ fbool x
| dstring x ⇒ fstring x
| dcoll x ⇒ fcoll x ((fix F2 (c : list data) : Forall P c :=
match c with
| nil ⇒ Forall_nil _
| cons d c0 ⇒ @Forall_cons _ P d c0 (F d) (F2 c0)
end) x)
| drec x ⇒ frec x ((fix F3 (r : list (string×data)) : Forall (fun ab ⇒ P (snd ab)) r :=
match r with
| nil ⇒ Forall_nil _
| cons sd c0 ⇒ @Forall_cons _ (fun ab ⇒ P (snd ab)) sd c0 (F (snd sd)) (F3 c0)
end) x)
| dleft d ⇒ fleft d (F d)
| dright d ⇒ fright d (F d)
| dbrand b d ⇒ fbrand b d (F d)
| dforeign fd ⇒ fforeign fd
end.
Definition data_rec (P:data→Set) := data_rect P.
Lemma dataInd2 (P : data → Prop)
(f : P dunit)
(f0 : ∀ n : Z, P (dnat n))
(fb : ∀ b : bool, P (dbool b))
(f1 : ∀ s : string, P (dstring s))
(f2 : ∀ c : list data, (∀ x, In x c → P x) → P (dcoll c))
(f3 : ∀ r : list (string × data), (∀ x y, In (x,y) r → P y) → P (drec r))
(f4 : ∀ d, P d → P (dleft d))
(f5 : ∀ d, P d → P (dright d))
(f6 : ∀ b d, P d → P (dbrand b d))
(fforeign : ∀ fd, P (dforeign fd)):
∀ d, P d.
Lemma brand_eq_dec : EqDec brand eq.
(funit : P dunit)
(fnat : ∀ n : Z, P (dnat n))
(fbool : ∀ b : bool, P (dbool b))
(fstring : ∀ s : string, P (dstring s))
(fcoll : ∀ c : list data, Forallt P c → P (dcoll c))
(frec : ∀ r : list (string × data), Forallt (fun ab ⇒ P (snd ab)) r → P (drec r))
(fleft: ∀ d, P d → P (dleft d))
(fright: ∀ d, P d → P (dright d))
(fbrand: ∀ b d, P d → P (dbrand b d))
(fforeign: ∀ fd, P (dforeign fd))
:=
fix F (d : data) : P d :=
match d as d0 return (P d0) with
| dunit ⇒ funit
| dnat x ⇒ fnat x
| dbool x ⇒ fbool x
| dstring x ⇒ fstring x
| dcoll x ⇒ fcoll x ((fix F2 (c : list data) : Forallt P c :=
match c as c0 with
| nil ⇒ Forallt_nil _
| cons d c0 ⇒ @Forallt_cons _ P d c0 (F d) (F2 c0)
end) x)
| drec x ⇒ frec x ((fix F3 (r : list (string×data)) : Forallt (fun ab ⇒ P (snd ab)) r :=
match r as c0 with
| nil ⇒ Forallt_nil _
| cons sd c0 ⇒ @Forallt_cons _ (fun ab ⇒ P (snd ab)) sd c0 (F (snd sd)) (F3 c0)
end) x)
| dleft x ⇒ fleft _ (F x)
| dright x ⇒ fright _ (F x)
| dbrand b x ⇒ fbrand b _ (F x)
| dforeign fd ⇒ fforeign fd
end.
Definition data_ind (P : data → Prop)
(funit : P dunit)
(fnat : ∀ n : Z, P (dnat n))
(fbool : ∀ b : bool, P (dbool b))
(fstring : ∀ s : string, P (dstring s))
(fcoll : ∀ c : list data, Forall P c → P (dcoll c))
(frec : ∀ r : list (string × data), Forall (fun ab ⇒ P (snd ab)) r → P (drec r))
(fleft: ∀ d, P d → P (dleft d))
(fright: ∀ d, P d → P (dright d))
(fbrand: ∀ b d, P d → P (dbrand b d))
(fforeign: ∀ fd, P (dforeign fd))
:=
fix F (d : data) : P d :=
match d as d0 return (P d0) with
| dunit ⇒ funit
| dnat x ⇒ fnat x
| dbool x ⇒ fbool x
| dstring x ⇒ fstring x
| dcoll x ⇒ fcoll x ((fix F2 (c : list data) : Forall P c :=
match c with
| nil ⇒ Forall_nil _
| cons d c0 ⇒ @Forall_cons _ P d c0 (F d) (F2 c0)
end) x)
| drec x ⇒ frec x ((fix F3 (r : list (string×data)) : Forall (fun ab ⇒ P (snd ab)) r :=
match r with
| nil ⇒ Forall_nil _
| cons sd c0 ⇒ @Forall_cons _ (fun ab ⇒ P (snd ab)) sd c0 (F (snd sd)) (F3 c0)
end) x)
| dleft d ⇒ fleft d (F d)
| dright d ⇒ fright d (F d)
| dbrand b d ⇒ fbrand b d (F d)
| dforeign fd ⇒ fforeign fd
end.
Definition data_rec (P:data→Set) := data_rect P.
Lemma dataInd2 (P : data → Prop)
(f : P dunit)
(f0 : ∀ n : Z, P (dnat n))
(fb : ∀ b : bool, P (dbool b))
(f1 : ∀ s : string, P (dstring s))
(f2 : ∀ c : list data, (∀ x, In x c → P x) → P (dcoll c))
(f3 : ∀ r : list (string × data), (∀ x y, In (x,y) r → P y) → P (drec r))
(f4 : ∀ d, P d → P (dleft d))
(f5 : ∀ d, P d → P (dright d))
(f6 : ∀ b d, P d → P (dbrand b d))
(fforeign : ∀ fd, P (dforeign fd)):
∀ d, P d.
Lemma brand_eq_dec : EqDec brand eq.
Equality is decidable for data