https://gitlab.com/nomadic-labs/mi-cho-coq
Tip revision: 1b25d1381245ea477075b579877977a53d2fb5ce authored by Arvid Jakobsson on 10 March 2020, 17:36:01 UTC
Prove functional spec of guestbook contract and simple lifetime prop
Prove functional spec of guestbook contract and simple lifetime prop
Tip revision: 1b25d13
syntax_type.v
Inductive simple_comparable_type : Set :=
| string
| nat
| int
| bytes
| bool
| mutez
| address
| key_hash
| timestamp.
Inductive comparable_type : Set :=
| Comparable_type_simple : simple_comparable_type -> comparable_type
| Cpair : simple_comparable_type -> comparable_type -> comparable_type.
Lemma comparable_type_dec (a b : comparable_type) : {a = b} + {a <> b}.
Proof.
repeat decide equality.
Defined.
Inductive type : Set :=
| Comparable_type : simple_comparable_type -> type
| key : type
| unit : type
| signature : type
| option : type -> type
| list : type -> type
| set : comparable_type -> type
| contract : type -> type
| operation : type
| pair : type -> type -> type
| or : type -> type -> type
| lambda : type -> type -> type
| map : comparable_type -> type -> type
| big_map : comparable_type -> type -> type
| chain_id : type.
Fixpoint comparable_type_to_type (c : comparable_type) : type :=
match c with
| Comparable_type_simple a => Comparable_type a
| Cpair a b => pair (Comparable_type a) (comparable_type_to_type b)
end.
Coercion comparable_type_to_type : comparable_type >-> type.
Coercion Comparable_type_simple : simple_comparable_type >-> comparable_type.
(* Coercion Comparable_type : simple_comparable_type >-> type. *)
Fixpoint is_packable (a : type) : Datatypes.bool :=
match a with
| operation | big_map _ _ | contract _ => false
| Comparable_type _ | unit | signature | key | lambda _ _ | set _ | chain_id => true
| option ty
| list ty
| map _ ty => is_packable ty
| pair a b | or a b => is_packable a && is_packable b
end.
Lemma type_dec (a b : type) : {a = b} + {a <> b}.
Proof.
repeat decide equality.
Defined.
Lemma stype_dec (A B : Datatypes.list type) : {A = B} + {A <> B}.
Proof.
decide equality; apply type_dec.
Defined.
Infix ":::" := (@cons type) (at level 60, right associativity).
Infix "+++" := (@app type) (at level 60, right associativity).