Library CFML.Stdlib.Pervasives_ml
Set Implicit Arguments.
Require Coq.ZArith.BinInt TLC.LibLogic TLC.LibRelation TLC.LibInt TLC.LibListZ CFML.Shared CFML.CFHeaps CFML.CFApp CFML.CFPrint CFML.CFBuiltin.
Require Import Coq.ZArith.BinIntDef CFML.CFHeader.
Delimit Scope Z_scope with Z.
Local Open Scope cfheader_scope.
Parameter raise : CFML.CFApp.func.
Parameter failwith : CFML.CFApp.func.
Parameter magic : CFML.CFApp.func.
Parameter not : CFML.CFApp.func.
Parameter not__cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (1)%nat not) (
forall x : Coq.Init.Datatypes.bool,
forall H : CFML.CFHeaps.hprop,
forall Q : Coq.Init.Datatypes.bool -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_if (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
Coq.Init.Logic.eq x Coq.Init.Datatypes.true ->
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (
Q (Coq.Init.Datatypes.false : Coq.Init.Datatypes.bool)
)
)
) H Q
) (
Coq.Init.Logic.eq x Coq.Init.Datatypes.false ->
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (
Q (Coq.Init.Datatypes.true : Coq.Init.Datatypes.bool)
)
)
) H Q
)
)
) H Q ->
CFML.CFApp.app_def not (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn Coq.Init.Datatypes.bool x) Coq.Lists.List.nil
) H Q
)
)
).
Hint Extern 1 (RegisterCF not) => CFHeader_Provide not__cf.
Parameter infix_eq_eq__ : CFML.CFApp.func.
Parameter infix_emark_eq__ : CFML.CFApp.func.
Parameter infix_emark_eq____cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (2)%nat infix_emark_eq__) (
forall A_ : Type,
forall x : A_,
forall y : A_,
forall H : CFML.CFHeaps.hprop,
forall Q : Coq.Init.Datatypes.bool -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def infix_eq_eq__ (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn A_ x) (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn A_ y) Coq.Lists.List.nil
)
) Coq.Init.Datatypes.bool
)
) (
fun x0__ : Coq.Init.Datatypes.bool =>
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (Q (TLC.LibBool.neg x0__))
)
)
)
)
) H Q ->
CFML.CFApp.app_def infix_emark_eq__ (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn A_ x) (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn A_ y) Coq.Lists.List.nil
)
) H Q
)
)
).
Hint Extern 1 (RegisterCF infix_emark_eq__) => CFHeader_Provide infix_emark_eq____cf.
Parameter infix_eq__ : CFML.CFApp.func.
Parameter infix_lt_gt__ : CFML.CFApp.func.
Parameter infix_lt__ : CFML.CFApp.func.
Parameter infix_gt__ : CFML.CFApp.func.
Parameter infix_lt_eq__ : CFML.CFApp.func.
Parameter infix_gt_eq__ : CFML.CFApp.func.
Parameter min : CFML.CFApp.func.
Parameter min__cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (2)%nat min) (
forall x : Coq.ZArith.BinInt.Z,
forall y : Coq.ZArith.BinInt.Z,
forall H : CFML.CFHeaps.hprop,
forall Q : Coq.ZArith.BinInt.Z -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_if (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
Coq.Init.Logic.eq (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.le _ TLC.LibInt.le_int_inst x__ y__)) x y
) Coq.Init.Datatypes.true ->
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (Q x)
)
) H Q
) (
Coq.Init.Logic.eq (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.le _ TLC.LibInt.le_int_inst x__ y__)) x y
) Coq.Init.Datatypes.false ->
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (Q y)
)
) H Q
)
)
) H Q ->
CFML.CFApp.app_def min (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z x) (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z y) Coq.Lists.List.nil
)
) H Q
)
)
).
Hint Extern 1 (RegisterCF min) => CFHeader_Provide min__cf.
Parameter max : CFML.CFApp.func.
Parameter max__cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (2)%nat max) (
forall x : Coq.ZArith.BinInt.Z,
forall y : Coq.ZArith.BinInt.Z,
forall H : CFML.CFHeaps.hprop,
forall Q : Coq.ZArith.BinInt.Z -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_if (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
Coq.Init.Logic.eq (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.ge _ (@TLC.LibOrder.ge_of_le _ TLC.LibInt.le_int_inst) x__ y__)) x y
) Coq.Init.Datatypes.true ->
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (Q x)
)
) H Q
) (
Coq.Init.Logic.eq (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.ge _ (@TLC.LibOrder.ge_of_le _ TLC.LibInt.le_int_inst) x__ y__)) x y
) Coq.Init.Datatypes.false ->
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (Q y)
)
) H Q
)
)
) H Q ->
CFML.CFApp.app_def max (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z x) (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z y) Coq.Lists.List.nil
)
) H Q
)
)
).
Hint Extern 1 (RegisterCF max) => CFHeader_Provide max__cf.
Parameter infix_amp_amp__ : CFML.CFApp.func.
Parameter infix_bar_bar__ : CFML.CFApp.func.
Parameter infix_tilde_minus__ : CFML.CFApp.func.
Parameter infix_plus__ : CFML.CFApp.func.
Parameter infix_minus__ : CFML.CFApp.func.
Parameter infix_star__ : CFML.CFApp.func.
Parameter infix_slash__ : CFML.CFApp.func.
Parameter mod : CFML.CFApp.func.
Parameter succ : CFML.CFApp.func.
Parameter succ__cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (1)%nat succ) (
forall n : Coq.ZArith.BinInt.Z,
forall H : CFML.CFHeaps.hprop,
forall Q : Coq.ZArith.BinInt.Z -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (Q (Coq.ZArith.BinInt.Z.add n (1)%Z))
)
) H Q ->
CFML.CFApp.app_def succ (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z n) Coq.Lists.List.nil
) H Q
)
)
).
Hint Extern 1 (RegisterCF succ) => CFHeader_Provide succ__cf.
Parameter pred : CFML.CFApp.func.
Parameter pred__cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (1)%nat pred) (
forall n : Coq.ZArith.BinInt.Z,
forall H : CFML.CFHeaps.hprop,
forall Q : Coq.ZArith.BinInt.Z -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (Q (Coq.ZArith.BinInt.Z.sub n (1)%Z))
)
) H Q ->
CFML.CFApp.app_def pred (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z n) Coq.Lists.List.nil
) H Q
)
)
).
Hint Extern 1 (RegisterCF pred) => CFHeader_Provide pred__cf.
Parameter abs : CFML.CFApp.func.
Parameter abs__cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (1)%nat abs) (
forall x : Coq.ZArith.BinInt.Z,
forall H : CFML.CFHeaps.hprop,
forall Q : Coq.ZArith.BinInt.Z -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_if (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
Coq.Init.Logic.eq (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.ge _ (@TLC.LibOrder.ge_of_le _ TLC.LibInt.le_int_inst) x__ y__)) x (
0
)%Z
) Coq.Init.Datatypes.true ->
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (Q x)
)
) H Q
) (
Coq.Init.Logic.eq (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.ge _ (@TLC.LibOrder.ge_of_le _ TLC.LibInt.le_int_inst) x__ y__)) x (
0
)%Z
) Coq.Init.Datatypes.false ->
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (Q (Coq.ZArith.BinInt.Z.opp x))
)
) H Q
)
)
) H Q ->
CFML.CFApp.app_def abs (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z x) Coq.Lists.List.nil
) H Q
)
)
).
Hint Extern 1 (RegisterCF abs) => CFHeader_Provide abs__cf.
Parameter land : CFML.CFApp.func.
Parameter lor : CFML.CFApp.func.
Parameter lxor : CFML.CFApp.func.
Parameter lnot : CFML.CFApp.func.
Parameter lsl : CFML.CFApp.func.
Parameter lsr : CFML.CFApp.func.
Parameter asr : CFML.CFApp.func.
Definition ref_ : _ := fun A_ : Type => CFML.CFHeaps.loc.
Definition contents' : Coq.Init.Datatypes.nat := (0)%nat.
Parameter ref : CFML.CFApp.func.
Parameter ref__cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (1)%nat ref) (
forall A_ : Type,
forall x : A_,
forall H : CFML.CFHeaps.hprop,
forall Q : ref_ A_ -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_record_new (
CFML.CFApp.app_record_new (
fun _ : CFHeaps.loc =>
Coq.Lists.List.cons (contents', @CFML.CFHeaps.dyn A_ x) Coq.Lists.List.nil
)
) H Q ->
CFML.CFApp.app_def ref (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn A_ x) Coq.Lists.List.nil
) H Q
)
)
).
Hint Extern 1 (RegisterCF ref) => CFHeader_Provide ref__cf.
Parameter infix_emark__ : CFML.CFApp.func.
Parameter infix_emark____cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (1)%nat infix_emark__) (
forall A_ : Type,
forall r : ref_ A_,
forall H : CFML.CFHeaps.hprop,
forall Q : A_ -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def CFML.CFApp.record_get (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn (ref_ A_) r) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.Init.Datatypes.nat contents'
) Coq.Lists.List.nil
)
) A_
) H Q ->
CFML.CFApp.app_def infix_emark__ (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn (ref_ A_) r) Coq.Lists.List.nil
) H Q
)
)
).
Hint Extern 1 (RegisterCF infix_emark__) => CFHeader_Provide infix_emark____cf.
Parameter infix_colon_eq__ : CFML.CFApp.func.
Parameter infix_colon_eq____cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (2)%nat infix_colon_eq__) (
forall A_ : Type,
forall r : ref_ A_,
forall x : A_,
forall H : CFML.CFHeaps.hprop,
forall Q : Coq.Init.Datatypes.unit -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def CFML.CFApp.record_set (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn (ref_ A_) r) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.Init.Datatypes.nat contents'
) (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn A_ x) Coq.Lists.List.nil
)
)
) Coq.Init.Datatypes.unit
) H Q ->
CFML.CFApp.app_def infix_colon_eq__ (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn (ref_ A_) r) (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn A_ x) Coq.Lists.List.nil
)
) H Q
)
)
).
Hint Extern 1 (RegisterCF infix_colon_eq__) => CFHeader_Provide infix_colon_eq____cf.
Parameter incr : CFML.CFApp.func.
Parameter incr__cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (1)%nat incr) (
forall r : ref_ Coq.ZArith.BinInt.Z,
forall H : CFML.CFHeaps.hprop,
forall Q : Coq.Init.Datatypes.unit -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def infix_emark__ (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (ref_ Coq.ZArith.BinInt.Z) r
) Coq.Lists.List.nil
) Coq.ZArith.BinInt.Z
)
) (
fun x0__ : Coq.ZArith.BinInt.Z =>
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def infix_colon_eq__ (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (ref_ Coq.ZArith.BinInt.Z) r
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z (
Coq.ZArith.BinInt.Z.add x0__ (1)%Z
)
) Coq.Lists.List.nil
)
) Coq.Init.Datatypes.unit
)
)
)
) H Q ->
CFML.CFApp.app_def incr (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn (ref_ Coq.ZArith.BinInt.Z) r) Coq.Lists.List.nil
) H Q
)
)
).
Hint Extern 1 (RegisterCF incr) => CFHeader_Provide incr__cf.
Parameter decr : CFML.CFApp.func.
Parameter decr__cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (1)%nat decr) (
forall r : ref_ Coq.ZArith.BinInt.Z,
forall H : CFML.CFHeaps.hprop,
forall Q : Coq.Init.Datatypes.unit -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def infix_emark__ (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (ref_ Coq.ZArith.BinInt.Z) r
) Coq.Lists.List.nil
) Coq.ZArith.BinInt.Z
)
) (
fun x0__ : Coq.ZArith.BinInt.Z =>
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def infix_colon_eq__ (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (ref_ Coq.ZArith.BinInt.Z) r
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z (
Coq.ZArith.BinInt.Z.sub x0__ (1)%Z
)
) Coq.Lists.List.nil
)
) Coq.Init.Datatypes.unit
)
)
)
) H Q ->
CFML.CFApp.app_def decr (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn (ref_ Coq.ZArith.BinInt.Z) r) Coq.Lists.List.nil
) H Q
)
)
).
Hint Extern 1 (RegisterCF decr) => CFHeader_Provide decr__cf.
Parameter fst : CFML.CFApp.func.
Parameter fst__cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (1)%nat fst) (
forall B_ : Type,
forall A_ : Type,
forall x0__ : Coq.Init.Datatypes.prod A_ B_,
forall H : CFML.CFHeaps.hprop,
forall Q : A_ -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_match (
CFML.CFHeaps.local (
CFML.CFPrint.tag CFML.CFPrint.tag_case (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
forall x : A_,
forall y : B_,
Coq.Init.Logic.eq x0__ (x, y) ->
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (Q x)
)
) H Q
) (
(
forall x : A_,
forall y : B_,
Coq.Init.Logic.not (Coq.Init.Logic.eq x0__ (x, y))
) ->
CFML.CFPrint.tag CFML.CFPrint.tag_done (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.True
)
) H Q
)
)
)
)
) H Q ->
CFML.CFApp.app_def fst (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (Coq.Init.Datatypes.prod A_ B_) x0__
) Coq.Lists.List.nil
) H Q
)
)
).
Hint Extern 1 (RegisterCF fst) => CFHeader_Provide fst__cf.
Parameter snd : CFML.CFApp.func.
Parameter snd__cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (1)%nat snd) (
forall B_ : Type,
forall A_ : Type,
forall x0__ : Coq.Init.Datatypes.prod A_ B_,
forall H : CFML.CFHeaps.hprop,
forall Q : B_ -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_match (
CFML.CFHeaps.local (
CFML.CFPrint.tag CFML.CFPrint.tag_case (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
forall x : A_,
forall y : B_,
Coq.Init.Logic.eq x0__ (x, y) ->
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (Q y)
)
) H Q
) (
(
forall x : A_,
forall y : B_,
Coq.Init.Logic.not (Coq.Init.Logic.eq x0__ (x, y))
) ->
CFML.CFPrint.tag CFML.CFPrint.tag_done (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.True
)
) H Q
)
)
)
)
) H Q ->
CFML.CFApp.app_def snd (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (Coq.Init.Datatypes.prod A_ B_) x0__
) Coq.Lists.List.nil
) H Q
)
)
).
Hint Extern 1 (RegisterCF snd) => CFHeader_Provide snd__cf.
Parameter ignore : CFML.CFApp.func.
Parameter ignore__cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (1)%nat ignore) (
forall A_ : Type,
forall x : A_,
forall H : CFML.CFHeaps.hprop,
forall Q : Coq.Init.Datatypes.unit -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (
Q (Coq.Init.Datatypes.tt : Coq.Init.Datatypes.unit)
)
)
) H Q ->
CFML.CFApp.app_def ignore (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn A_ x) Coq.Lists.List.nil
) H Q
)
)
).
Hint Extern 1 (RegisterCF ignore) => CFHeader_Provide ignore__cf.
Parameter infix_at__ : CFML.CFApp.func.
Parameter infix_at____cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (2)%nat infix_at__) (
forall A_ : Type,
forall l1 : Coq.Init.Datatypes.list A_,
forall l2 : Coq.Init.Datatypes.list A_,
forall H : CFML.CFHeaps.hprop,
forall Q : Coq.Init.Datatypes.list A_ -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_match (
CFML.CFHeaps.local (
CFML.CFPrint.tag CFML.CFPrint.tag_case (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
Coq.Init.Logic.eq l1 (
Coq.Lists.List.nil : Coq.Init.Datatypes.list A_
) ->
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (Q l2)
)
) H Q
) (
Coq.Init.Logic.not (
Coq.Init.Logic.eq l1 (
Coq.Lists.List.nil : Coq.Init.Datatypes.list A_
)
) ->
CFML.CFPrint.tag CFML.CFPrint.tag_case (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
forall hd : A_,
forall tl : Coq.Init.Datatypes.list A_,
Coq.Init.Logic.eq l1 (
Coq.Lists.List.cons hd tl : Coq.Init.Datatypes.list A_
) ->
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (
Q (
Coq.Lists.List.cons hd (
(@TLC.LibList.app _) tl l2
) : Coq.Init.Datatypes.list A_
)
)
)
) H Q
) (
(
forall hd : A_,
forall tl : Coq.Init.Datatypes.list A_,
Coq.Init.Logic.not (
Coq.Init.Logic.eq l1 (
Coq.Lists.List.cons hd tl : Coq.Init.Datatypes.list A_
)
)
) ->
CFML.CFPrint.tag CFML.CFPrint.tag_done (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.True
)
) H Q
)
)
) H Q
)
)
)
)
) H Q ->
CFML.CFApp.app_def infix_at__ (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) l1
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) l2
) Coq.Lists.List.nil
)
) H Q
)
)
).
Hint Extern 1 (RegisterCF infix_at__) => CFHeader_Provide infix_at____cf.
Require Coq.ZArith.BinInt TLC.LibLogic TLC.LibRelation TLC.LibInt TLC.LibListZ CFML.Shared CFML.CFHeaps CFML.CFApp CFML.CFPrint CFML.CFBuiltin.
Require Import Coq.ZArith.BinIntDef CFML.CFHeader.
Delimit Scope Z_scope with Z.
Local Open Scope cfheader_scope.
Parameter raise : CFML.CFApp.func.
Parameter failwith : CFML.CFApp.func.
Parameter magic : CFML.CFApp.func.
Parameter not : CFML.CFApp.func.
Parameter not__cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (1)%nat not) (
forall x : Coq.Init.Datatypes.bool,
forall H : CFML.CFHeaps.hprop,
forall Q : Coq.Init.Datatypes.bool -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_if (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
Coq.Init.Logic.eq x Coq.Init.Datatypes.true ->
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (
Q (Coq.Init.Datatypes.false : Coq.Init.Datatypes.bool)
)
)
) H Q
) (
Coq.Init.Logic.eq x Coq.Init.Datatypes.false ->
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (
Q (Coq.Init.Datatypes.true : Coq.Init.Datatypes.bool)
)
)
) H Q
)
)
) H Q ->
CFML.CFApp.app_def not (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn Coq.Init.Datatypes.bool x) Coq.Lists.List.nil
) H Q
)
)
).
Hint Extern 1 (RegisterCF not) => CFHeader_Provide not__cf.
Parameter infix_eq_eq__ : CFML.CFApp.func.
Parameter infix_emark_eq__ : CFML.CFApp.func.
Parameter infix_emark_eq____cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (2)%nat infix_emark_eq__) (
forall A_ : Type,
forall x : A_,
forall y : A_,
forall H : CFML.CFHeaps.hprop,
forall Q : Coq.Init.Datatypes.bool -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def infix_eq_eq__ (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn A_ x) (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn A_ y) Coq.Lists.List.nil
)
) Coq.Init.Datatypes.bool
)
) (
fun x0__ : Coq.Init.Datatypes.bool =>
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (Q (TLC.LibBool.neg x0__))
)
)
)
)
) H Q ->
CFML.CFApp.app_def infix_emark_eq__ (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn A_ x) (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn A_ y) Coq.Lists.List.nil
)
) H Q
)
)
).
Hint Extern 1 (RegisterCF infix_emark_eq__) => CFHeader_Provide infix_emark_eq____cf.
Parameter infix_eq__ : CFML.CFApp.func.
Parameter infix_lt_gt__ : CFML.CFApp.func.
Parameter infix_lt__ : CFML.CFApp.func.
Parameter infix_gt__ : CFML.CFApp.func.
Parameter infix_lt_eq__ : CFML.CFApp.func.
Parameter infix_gt_eq__ : CFML.CFApp.func.
Parameter min : CFML.CFApp.func.
Parameter min__cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (2)%nat min) (
forall x : Coq.ZArith.BinInt.Z,
forall y : Coq.ZArith.BinInt.Z,
forall H : CFML.CFHeaps.hprop,
forall Q : Coq.ZArith.BinInt.Z -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_if (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
Coq.Init.Logic.eq (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.le _ TLC.LibInt.le_int_inst x__ y__)) x y
) Coq.Init.Datatypes.true ->
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (Q x)
)
) H Q
) (
Coq.Init.Logic.eq (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.le _ TLC.LibInt.le_int_inst x__ y__)) x y
) Coq.Init.Datatypes.false ->
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (Q y)
)
) H Q
)
)
) H Q ->
CFML.CFApp.app_def min (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z x) (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z y) Coq.Lists.List.nil
)
) H Q
)
)
).
Hint Extern 1 (RegisterCF min) => CFHeader_Provide min__cf.
Parameter max : CFML.CFApp.func.
Parameter max__cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (2)%nat max) (
forall x : Coq.ZArith.BinInt.Z,
forall y : Coq.ZArith.BinInt.Z,
forall H : CFML.CFHeaps.hprop,
forall Q : Coq.ZArith.BinInt.Z -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_if (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
Coq.Init.Logic.eq (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.ge _ (@TLC.LibOrder.ge_of_le _ TLC.LibInt.le_int_inst) x__ y__)) x y
) Coq.Init.Datatypes.true ->
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (Q x)
)
) H Q
) (
Coq.Init.Logic.eq (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.ge _ (@TLC.LibOrder.ge_of_le _ TLC.LibInt.le_int_inst) x__ y__)) x y
) Coq.Init.Datatypes.false ->
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (Q y)
)
) H Q
)
)
) H Q ->
CFML.CFApp.app_def max (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z x) (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z y) Coq.Lists.List.nil
)
) H Q
)
)
).
Hint Extern 1 (RegisterCF max) => CFHeader_Provide max__cf.
Parameter infix_amp_amp__ : CFML.CFApp.func.
Parameter infix_bar_bar__ : CFML.CFApp.func.
Parameter infix_tilde_minus__ : CFML.CFApp.func.
Parameter infix_plus__ : CFML.CFApp.func.
Parameter infix_minus__ : CFML.CFApp.func.
Parameter infix_star__ : CFML.CFApp.func.
Parameter infix_slash__ : CFML.CFApp.func.
Parameter mod : CFML.CFApp.func.
Parameter succ : CFML.CFApp.func.
Parameter succ__cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (1)%nat succ) (
forall n : Coq.ZArith.BinInt.Z,
forall H : CFML.CFHeaps.hprop,
forall Q : Coq.ZArith.BinInt.Z -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (Q (Coq.ZArith.BinInt.Z.add n (1)%Z))
)
) H Q ->
CFML.CFApp.app_def succ (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z n) Coq.Lists.List.nil
) H Q
)
)
).
Hint Extern 1 (RegisterCF succ) => CFHeader_Provide succ__cf.
Parameter pred : CFML.CFApp.func.
Parameter pred__cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (1)%nat pred) (
forall n : Coq.ZArith.BinInt.Z,
forall H : CFML.CFHeaps.hprop,
forall Q : Coq.ZArith.BinInt.Z -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (Q (Coq.ZArith.BinInt.Z.sub n (1)%Z))
)
) H Q ->
CFML.CFApp.app_def pred (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z n) Coq.Lists.List.nil
) H Q
)
)
).
Hint Extern 1 (RegisterCF pred) => CFHeader_Provide pred__cf.
Parameter abs : CFML.CFApp.func.
Parameter abs__cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (1)%nat abs) (
forall x : Coq.ZArith.BinInt.Z,
forall H : CFML.CFHeaps.hprop,
forall Q : Coq.ZArith.BinInt.Z -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_if (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
Coq.Init.Logic.eq (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.ge _ (@TLC.LibOrder.ge_of_le _ TLC.LibInt.le_int_inst) x__ y__)) x (
0
)%Z
) Coq.Init.Datatypes.true ->
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (Q x)
)
) H Q
) (
Coq.Init.Logic.eq (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.ge _ (@TLC.LibOrder.ge_of_le _ TLC.LibInt.le_int_inst) x__ y__)) x (
0
)%Z
) Coq.Init.Datatypes.false ->
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (Q (Coq.ZArith.BinInt.Z.opp x))
)
) H Q
)
)
) H Q ->
CFML.CFApp.app_def abs (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z x) Coq.Lists.List.nil
) H Q
)
)
).
Hint Extern 1 (RegisterCF abs) => CFHeader_Provide abs__cf.
Parameter land : CFML.CFApp.func.
Parameter lor : CFML.CFApp.func.
Parameter lxor : CFML.CFApp.func.
Parameter lnot : CFML.CFApp.func.
Parameter lsl : CFML.CFApp.func.
Parameter lsr : CFML.CFApp.func.
Parameter asr : CFML.CFApp.func.
Definition ref_ : _ := fun A_ : Type => CFML.CFHeaps.loc.
Definition contents' : Coq.Init.Datatypes.nat := (0)%nat.
Parameter ref : CFML.CFApp.func.
Parameter ref__cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (1)%nat ref) (
forall A_ : Type,
forall x : A_,
forall H : CFML.CFHeaps.hprop,
forall Q : ref_ A_ -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_record_new (
CFML.CFApp.app_record_new (
fun _ : CFHeaps.loc =>
Coq.Lists.List.cons (contents', @CFML.CFHeaps.dyn A_ x) Coq.Lists.List.nil
)
) H Q ->
CFML.CFApp.app_def ref (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn A_ x) Coq.Lists.List.nil
) H Q
)
)
).
Hint Extern 1 (RegisterCF ref) => CFHeader_Provide ref__cf.
Parameter infix_emark__ : CFML.CFApp.func.
Parameter infix_emark____cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (1)%nat infix_emark__) (
forall A_ : Type,
forall r : ref_ A_,
forall H : CFML.CFHeaps.hprop,
forall Q : A_ -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def CFML.CFApp.record_get (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn (ref_ A_) r) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.Init.Datatypes.nat contents'
) Coq.Lists.List.nil
)
) A_
) H Q ->
CFML.CFApp.app_def infix_emark__ (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn (ref_ A_) r) Coq.Lists.List.nil
) H Q
)
)
).
Hint Extern 1 (RegisterCF infix_emark__) => CFHeader_Provide infix_emark____cf.
Parameter infix_colon_eq__ : CFML.CFApp.func.
Parameter infix_colon_eq____cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (2)%nat infix_colon_eq__) (
forall A_ : Type,
forall r : ref_ A_,
forall x : A_,
forall H : CFML.CFHeaps.hprop,
forall Q : Coq.Init.Datatypes.unit -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def CFML.CFApp.record_set (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn (ref_ A_) r) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.Init.Datatypes.nat contents'
) (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn A_ x) Coq.Lists.List.nil
)
)
) Coq.Init.Datatypes.unit
) H Q ->
CFML.CFApp.app_def infix_colon_eq__ (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn (ref_ A_) r) (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn A_ x) Coq.Lists.List.nil
)
) H Q
)
)
).
Hint Extern 1 (RegisterCF infix_colon_eq__) => CFHeader_Provide infix_colon_eq____cf.
Parameter incr : CFML.CFApp.func.
Parameter incr__cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (1)%nat incr) (
forall r : ref_ Coq.ZArith.BinInt.Z,
forall H : CFML.CFHeaps.hprop,
forall Q : Coq.Init.Datatypes.unit -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def infix_emark__ (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (ref_ Coq.ZArith.BinInt.Z) r
) Coq.Lists.List.nil
) Coq.ZArith.BinInt.Z
)
) (
fun x0__ : Coq.ZArith.BinInt.Z =>
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def infix_colon_eq__ (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (ref_ Coq.ZArith.BinInt.Z) r
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z (
Coq.ZArith.BinInt.Z.add x0__ (1)%Z
)
) Coq.Lists.List.nil
)
) Coq.Init.Datatypes.unit
)
)
)
) H Q ->
CFML.CFApp.app_def incr (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn (ref_ Coq.ZArith.BinInt.Z) r) Coq.Lists.List.nil
) H Q
)
)
).
Hint Extern 1 (RegisterCF incr) => CFHeader_Provide incr__cf.
Parameter decr : CFML.CFApp.func.
Parameter decr__cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (1)%nat decr) (
forall r : ref_ Coq.ZArith.BinInt.Z,
forall H : CFML.CFHeaps.hprop,
forall Q : Coq.Init.Datatypes.unit -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def infix_emark__ (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (ref_ Coq.ZArith.BinInt.Z) r
) Coq.Lists.List.nil
) Coq.ZArith.BinInt.Z
)
) (
fun x0__ : Coq.ZArith.BinInt.Z =>
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def infix_colon_eq__ (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (ref_ Coq.ZArith.BinInt.Z) r
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z (
Coq.ZArith.BinInt.Z.sub x0__ (1)%Z
)
) Coq.Lists.List.nil
)
) Coq.Init.Datatypes.unit
)
)
)
) H Q ->
CFML.CFApp.app_def decr (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn (ref_ Coq.ZArith.BinInt.Z) r) Coq.Lists.List.nil
) H Q
)
)
).
Hint Extern 1 (RegisterCF decr) => CFHeader_Provide decr__cf.
Parameter fst : CFML.CFApp.func.
Parameter fst__cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (1)%nat fst) (
forall B_ : Type,
forall A_ : Type,
forall x0__ : Coq.Init.Datatypes.prod A_ B_,
forall H : CFML.CFHeaps.hprop,
forall Q : A_ -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_match (
CFML.CFHeaps.local (
CFML.CFPrint.tag CFML.CFPrint.tag_case (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
forall x : A_,
forall y : B_,
Coq.Init.Logic.eq x0__ (x, y) ->
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (Q x)
)
) H Q
) (
(
forall x : A_,
forall y : B_,
Coq.Init.Logic.not (Coq.Init.Logic.eq x0__ (x, y))
) ->
CFML.CFPrint.tag CFML.CFPrint.tag_done (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.True
)
) H Q
)
)
)
)
) H Q ->
CFML.CFApp.app_def fst (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (Coq.Init.Datatypes.prod A_ B_) x0__
) Coq.Lists.List.nil
) H Q
)
)
).
Hint Extern 1 (RegisterCF fst) => CFHeader_Provide fst__cf.
Parameter snd : CFML.CFApp.func.
Parameter snd__cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (1)%nat snd) (
forall B_ : Type,
forall A_ : Type,
forall x0__ : Coq.Init.Datatypes.prod A_ B_,
forall H : CFML.CFHeaps.hprop,
forall Q : B_ -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_match (
CFML.CFHeaps.local (
CFML.CFPrint.tag CFML.CFPrint.tag_case (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
forall x : A_,
forall y : B_,
Coq.Init.Logic.eq x0__ (x, y) ->
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (Q y)
)
) H Q
) (
(
forall x : A_,
forall y : B_,
Coq.Init.Logic.not (Coq.Init.Logic.eq x0__ (x, y))
) ->
CFML.CFPrint.tag CFML.CFPrint.tag_done (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.True
)
) H Q
)
)
)
)
) H Q ->
CFML.CFApp.app_def snd (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (Coq.Init.Datatypes.prod A_ B_) x0__
) Coq.Lists.List.nil
) H Q
)
)
).
Hint Extern 1 (RegisterCF snd) => CFHeader_Provide snd__cf.
Parameter ignore : CFML.CFApp.func.
Parameter ignore__cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (1)%nat ignore) (
forall A_ : Type,
forall x : A_,
forall H : CFML.CFHeaps.hprop,
forall Q : Coq.Init.Datatypes.unit -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (
Q (Coq.Init.Datatypes.tt : Coq.Init.Datatypes.unit)
)
)
) H Q ->
CFML.CFApp.app_def ignore (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn A_ x) Coq.Lists.List.nil
) H Q
)
)
).
Hint Extern 1 (RegisterCF ignore) => CFHeader_Provide ignore__cf.
Parameter infix_at__ : CFML.CFApp.func.
Parameter infix_at____cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (2)%nat infix_at__) (
forall A_ : Type,
forall l1 : Coq.Init.Datatypes.list A_,
forall l2 : Coq.Init.Datatypes.list A_,
forall H : CFML.CFHeaps.hprop,
forall Q : Coq.Init.Datatypes.list A_ -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_match (
CFML.CFHeaps.local (
CFML.CFPrint.tag CFML.CFPrint.tag_case (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
Coq.Init.Logic.eq l1 (
Coq.Lists.List.nil : Coq.Init.Datatypes.list A_
) ->
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (Q l2)
)
) H Q
) (
Coq.Init.Logic.not (
Coq.Init.Logic.eq l1 (
Coq.Lists.List.nil : Coq.Init.Datatypes.list A_
)
) ->
CFML.CFPrint.tag CFML.CFPrint.tag_case (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
forall hd : A_,
forall tl : Coq.Init.Datatypes.list A_,
Coq.Init.Logic.eq l1 (
Coq.Lists.List.cons hd tl : Coq.Init.Datatypes.list A_
) ->
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (
Q (
Coq.Lists.List.cons hd (
(@TLC.LibList.app _) tl l2
) : Coq.Init.Datatypes.list A_
)
)
)
) H Q
) (
(
forall hd : A_,
forall tl : Coq.Init.Datatypes.list A_,
Coq.Init.Logic.not (
Coq.Init.Logic.eq l1 (
Coq.Lists.List.cons hd tl : Coq.Init.Datatypes.list A_
)
)
) ->
CFML.CFPrint.tag CFML.CFPrint.tag_done (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.True
)
) H Q
)
)
) H Q
)
)
)
)
) H Q ->
CFML.CFApp.app_def infix_at__ (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) l1
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) l2
) Coq.Lists.List.nil
)
) H Q
)
)
).
Hint Extern 1 (RegisterCF infix_at__) => CFHeader_Provide infix_at____cf.