From Velus Require Import Common.
Module Type OPERATORS.
Parameter val :
Type.
Parameter type :
Type.
Parameter const :
Type.
Parameter type_const :
const ->
type.
Parameter sem_const :
const ->
val.
Parameter init_type :
type ->
const.
Parameter true_val :
val.
Parameter false_val :
val.
Conjecture true_not_false_val :
true_val <>
false_val.
Parameter bool_type :
type.
Parameter true_const :
const.
Parameter false_const :
const.
Conjecture sem_true_const :
sem_const true_const =
true_val.
Conjecture sem_false_const :
sem_const false_const =
false_val.
Conjecture type_true_const :
type_const true_const =
bool_type.
Conjecture type_false_const :
type_const false_const =
bool_type.
Parameter unop :
Type.
Parameter binop :
Type.
Parameter sem_unop :
unop ->
val ->
type ->
option val.
Parameter sem_binop :
binop ->
val ->
type ->
val ->
type ->
option val.
Parameter type_unop :
unop ->
type ->
option type.
Parameter type_binop :
binop ->
type ->
type ->
option type.
Parameter wt_val :
val ->
type ->
Prop.
Conjecture wt_val_bool :
forall v, (
v =
true_val \/
v =
false_val) <->
wt_val v bool_type.
Conjecture wt_val_const :
forall c,
wt_val (
sem_const c) (
type_const c).
Conjecture wt_init_type :
forall ty,
wt_val (
sem_const (
init_type ty))
ty.
Conjecture type_init_type :
forall ty,
type_const (
init_type ty) =
ty.
Conjecture pres_sem_unop:
forall op ty1 ty v1 v,
type_unop op ty1 =
Some ty ->
sem_unop op v1 ty1 =
Some v ->
wt_val v1 ty1 ->
wt_val v ty.
Conjecture pres_sem_binop:
forall op ty1 ty2 ty v1 v2 v,
type_binop op ty1 ty2 =
Some ty ->
sem_binop op v1 ty1 v2 ty2 =
Some v ->
wt_val v1 ty1 ->
wt_val v2 ty2 ->
wt_val v ty.
Conjecture val_dec :
forall v1 v2 :
val, {
v1 =
v2} + {
v1 <>
v2}.
Conjecture type_dec :
forall t1 t2 :
type, {
t1 =
t2} + {
t1 <>
t2}.
Conjecture const_dec :
forall c1 c2 :
const, {
c1 =
c2} + {
c1 <>
c2}.
Conjecture unop_dec :
forall op1 op2 :
unop, {
op1 =
op2} + {
op1 <>
op2}.
Conjecture binop_dec :
forall op1 op2 :
binop, {
op1 =
op2} + {
op1 <>
op2}.
End OPERATORS.
From Coq Require Export Classes.EquivDec.
Module Type OPERATORS_AUX (
Import Ops :
OPERATORS).
Close Scope equiv_scope.
Instance:
EqDec val eq := {
equiv_dec :=
val_dec }.
Instance:
EqDec type eq := {
equiv_dec :=
type_dec }.
Instance:
EqDec const eq := {
equiv_dec :=
const_dec }.
Instance:
EqDec unop eq := {
equiv_dec :=
unop_dec }.
Instance:
EqDec binop eq := {
equiv_dec :=
binop_dec }.
Lemma wt_val_true:
wt_val true_val bool_type.
Proof.
Lemma wt_val_false:
wt_val false_val bool_type.
Proof.
Definition val_to_bool (
v:
val) :
option bool :=
if equiv_decb v true_val then Some true
else if equiv_decb v false_val then Some false
else None.
Lemma val_to_bool_true:
val_to_bool true_val =
Some true.
Proof.
Lemma val_to_bool_false:
val_to_bool false_val =
Some false.
Proof.
Lemma val_to_bool_true':
forall v,
val_to_bool v =
Some true <->
v =
true_val.
Proof.
Lemma val_to_bool_false':
forall v,
val_to_bool v =
Some false <->
v =
false_val.
Proof.
Lemma wt_val_to_bool:
forall v,
wt_val v bool_type ->
exists b,
val_to_bool v =
Some b.
Proof.
Definition val_of_bool (
b :
bool) :
val :=
match b with
|
true =>
true_val
|
false =>
false_val
end.
Definition wt_vals vs (
xts:
list (
ident *
type))
:=
List.Forall2 (
fun v xt =>
wt_val v (
snd xt))
vs xts.
Definition wt_valo (
vo:
option val) (
ty:
type) :
Prop :=
match vo with
|
None =>
True
|
Some v =>
wt_val v ty
end.
A synchronous value is either an absence or a present constant
Inductive value :=
|
absent
|
present (
v:
val).
Implicit Type v :
value.
Definition value_dec (
v1 v2:
value) : {
v1 =
v2} + {
v1 <>
v2}.
decide equality.
apply val_dec.
Defined.
Proof.
Proof.
Proof.
Proof.
Proof.