🍃 RPC_arg.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Environment.V8.Proofs.Int32.
Require TezosOfOCaml.Environment.V8.Proofs.Int64.
Require TezosOfOCaml.Environment.V8.Proofs.Pervasives.
Module Valid.
Record t {a : Set} {domain : a → Prop} {arg : RPC_arg.t a} : Prop := {
destruct_construct v :
domain v →
arg.(RPC_arg.t.destruct) (arg.(RPC_arg.t.construct) v) =
Pervasives.Ok v;
construct_destruct s :
match arg.(RPC_arg.t.destruct) s with
| Pervasives.Ok v ⇒ arg.(RPC_arg.t.construct) v = s
| Pervasives.Error _ ⇒ True
end;
}.
Arguments t {_}.
Lemma implies {a : Set} {domain domain' : a → Prop} {arg : RPC_arg.t a}
: t domain arg →
(∀ x, domain' x → domain x) →
t domain' arg.
intros H H_implies; constructor; intros; apply H; now try apply H_implies.
Qed.
Axiom bool_value : t (fun _ ⇒ True) RPC_arg.bool_value.
Axiom int_value : t Pervasives.Int.Valid.t RPC_arg.int_value.
Axiom uint : t Pervasives.Int.Valid.non_negative RPC_arg.uint.
Axiom int32_value : t Int32.Valid.t RPC_arg.int32_value.
Axiom uint31 : t Int32.Valid.non_negative RPC_arg.uint31.
Axiom int64_value : t Int64.Valid.t RPC_arg.int64_value.
Axiom uint63 : t Int64.Valid.non_negative RPC_arg.uint63.
Axiom string_value : t (fun _ ⇒ True) RPC_arg.string_value.
Axiom option_value : ∀ {a : Set} (domain : a → Prop) arg,
t domain arg →
let option_domain x :=
match x with
| None ⇒ True
| Some x ⇒ domain x
end in
t option_domain (RPC_arg.option_value arg).
Axiom list_value : ∀ {a : Set} (domain : a → Prop) arg,
t domain arg →
let list_domain x :=
List.Forall domain x in
t list_domain (RPC_arg.list_value arg).
Axiom like : ∀ {a : Set} {domain} {arg : RPC_arg.t a} {description name},
t domain arg → t domain (RPC_arg.like arg description name).
End Valid.
Ltac valid_auto :=
repeat first [
apply Valid.bool_value |
apply Valid.int_value |
apply Valid.uint |
apply Valid.int32_value |
apply Valid.uint31 |
apply Valid.int64_value |
apply Valid.uint63 |
apply Valid.string_value |
apply Valid.option_value |
apply Valid.list_value |
apply Valid.like
].
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Environment.V8.Proofs.Int32.
Require TezosOfOCaml.Environment.V8.Proofs.Int64.
Require TezosOfOCaml.Environment.V8.Proofs.Pervasives.
Module Valid.
Record t {a : Set} {domain : a → Prop} {arg : RPC_arg.t a} : Prop := {
destruct_construct v :
domain v →
arg.(RPC_arg.t.destruct) (arg.(RPC_arg.t.construct) v) =
Pervasives.Ok v;
construct_destruct s :
match arg.(RPC_arg.t.destruct) s with
| Pervasives.Ok v ⇒ arg.(RPC_arg.t.construct) v = s
| Pervasives.Error _ ⇒ True
end;
}.
Arguments t {_}.
Lemma implies {a : Set} {domain domain' : a → Prop} {arg : RPC_arg.t a}
: t domain arg →
(∀ x, domain' x → domain x) →
t domain' arg.
intros H H_implies; constructor; intros; apply H; now try apply H_implies.
Qed.
Axiom bool_value : t (fun _ ⇒ True) RPC_arg.bool_value.
Axiom int_value : t Pervasives.Int.Valid.t RPC_arg.int_value.
Axiom uint : t Pervasives.Int.Valid.non_negative RPC_arg.uint.
Axiom int32_value : t Int32.Valid.t RPC_arg.int32_value.
Axiom uint31 : t Int32.Valid.non_negative RPC_arg.uint31.
Axiom int64_value : t Int64.Valid.t RPC_arg.int64_value.
Axiom uint63 : t Int64.Valid.non_negative RPC_arg.uint63.
Axiom string_value : t (fun _ ⇒ True) RPC_arg.string_value.
Axiom option_value : ∀ {a : Set} (domain : a → Prop) arg,
t domain arg →
let option_domain x :=
match x with
| None ⇒ True
| Some x ⇒ domain x
end in
t option_domain (RPC_arg.option_value arg).
Axiom list_value : ∀ {a : Set} (domain : a → Prop) arg,
t domain arg →
let list_domain x :=
List.Forall domain x in
t list_domain (RPC_arg.list_value arg).
Axiom like : ∀ {a : Set} {domain} {arg : RPC_arg.t a} {description name},
t domain arg → t domain (RPC_arg.like arg description name).
End Valid.
Ltac valid_auto :=
repeat first [
apply Valid.bool_value |
apply Valid.int_value |
apply Valid.uint |
apply Valid.int32_value |
apply Valid.uint31 |
apply Valid.int64_value |
apply Valid.uint63 |
apply Valid.string_value |
apply Valid.option_value |
apply Valid.list_value |
apply Valid.like
].