add coq-stdpp as dependency, add abs_examples module (#12)

* add coq-stdpp as dependency, add abs_examples module

* Typing examples

* nits

---------

Co-authored-by: Aqissiaq <aqissiaq@gmail.com>

README.md

@@ -23,6 +23,7 @@ Formal metatheory in Coq for the ABS language.
 - Additional dependencies:
   - [Ott Coq library](https://github.com/ott-lang/ott) 0.33 or later
   - [Equations Coq library](https://github.com/mattam82/Coq-Equations) 1.3 or later
+  - [Coq-Std++](https://gitlab.mpi-sws.org/iris/stdpp) 1.9.0 or later
 - Coq namespace: `ABS`
 - Related publication(s):
   - [ABS: A Core Language for Abstract Behavioral Specification](https://link.springer.com/chapter/10.1007/978-3-642-25271-6_8) doi:[10.1007/978-3-642-25271-6_8](https://doi.org/10.1007/978-3-642-25271-6_8)
@@ -33,7 +34,7 @@ To install all dependencies, do:
 
 ```shell
 opam repo add coq-released https://coq.inria.fr/opam/released
-opam install coq.8.18.0 coq-ott
+opam install coq.8.18.0 coq-ott coq-equations coq-stdpp
 ```
 
 To build when dependencies are installed, do:

_CoqProject

@@ -3,4 +3,5 @@
 -arg -w -arg -deprecated-hint-without-locality
 
 theories/abs_defs.v
+theories/abs_examples.v
 theories/abs_functional_metatheory.v

coq-abs-metatheory.opam

@@ -20,6 +20,7 @@ depends: [
   "coq" {>= "8.16"}
   "coq-ott" {>= "0.33"}
   "coq-equations" {>= "1.3"}
+  "coq-stdpp" {>= "1.9.0"}
 ]
 
 tags: [

meta.yml

@@ -33,12 +33,16 @@ dependencies:
     version: '{>= "0.33"}'
   description: |-
     [Ott Coq library](https://github.com/ott-lang/ott) 0.33 or later
-
 - opam:
     name: coq-equations
     version: '{>= "1.3"}'
   description: |-
     [Equations Coq library](https://github.com/mattam82/Coq-Equations) 1.3 or later
+- opam:
+    name: coq-stdpp
+    version: '{>= "1.9.0"}'
+  description: |-
+    [Coq-Std++](https://gitlab.mpi-sws.org/iris/stdpp) 1.9.0 or later
 
 tested_coq_opam_versions:
 - version: '8.18'
@@ -60,7 +64,7 @@ build: |-
   
   ```shell
   opam repo add coq-released https://coq.inria.fr/opam/released
-  opam install coq.8.18.0 coq-ott
+  opam install coq.8.18.0 coq-ott coq-equations coq-stdpp
   ```
   
   To build when dependencies are installed, do:

theories/abs_examples.v

@@ -0,0 +1,37 @@
+From ABS Require Import abs_defs.
+From stdpp Require Import prelude base.
+
+(** * ABS Examples *)
+
+Definition e_const_5 : e := 
+  e_t (t_int 5%Z).
+
+Definition func_const_5 : F := 
+  F_fn T_int "const_5"%string [] e_const_5.
+
+Definition e_call_const_5 : e :=
+  e_fn_call "const_5"%string [].
+
+Definition Ctx : G :=
+  Map.add ("const_5"%string) (ctxv_sig (sig_sig [] T_int)) (Map.empty ctxv).
+
+Lemma e_const_5_T_int :
+ typ_e Ctx e_const_5 T_int.
+Proof. by apply typ_int. Qed.
+
+Lemma e_call_const_typ_F :
+ typ_F Ctx func_const_5.
+Proof.
+  apply typ_func_decl.
+  - easy.
+  - apply e_const_5_T_int.
+Qed.
+
+Lemma e_call_const_5_T_int :
+ typ_e Ctx e_call_const_5 T_int.
+Proof.
+  unfold e_call_const_5.
+  replace [] with (map (fun (pat_:(e*T)) => match pat_ with (e_,T_) => e_ end ) [])
+    by auto.
+  by apply typ_func_expr.
+Qed.