Coq 8.6

.gitignore

@@ -0,0 +1,33 @@
+.*.aux
+*.a
+*.bak
+*.cma
+*.cmi
+*.cmo
+*.cmx
+*.cmxa
+*.cmxs
+*.coq
+*.glob
+*.ml.d
+*.ml4.d
+*.mli.d
+*.mllib.d
+*.mlpack.d
+*.native
+*.o
+*.v.d
+*.vio
+*.vo
+.coq-native/
+.csdp.cache
+.lia.cache
+.nia.cache
+.nlia.cache
+.nra.cache
+csdp.cache
+lia.cache
+nia.cache
+nlia.cache
+nra.cache
+

.travis.yml

@@ -0,0 +1,21 @@
+language: generic
+dist: trusty
+sudo: required
+group: edge
+
+os:
+    - osx
+    - linux
+
+install:
+    case $TRAVIS_OS_NAME in
+    osx)
+    brew update &&
+    brew install coq ;;
+    linux)
+    wget https://raw.github.com/ocaml/opam/master/shell/opam_installer.sh -O - | sh -s /usr/local/bin &&
+    opam install coq -y &&
+    eval $(opam config env) ;;
+    esac
+script:
+    make -C bast0-coq -j

README.md

@@ -1,4 +1,5 @@
 veriFTL
 =======
+[![Build Status](https://travis-ci.org/liyishuai/veriFTL.svg?branch=master)](https://travis-ci.org/liyishuai/veriFTL)
 
 Formal model and verification of FTLs

bast0-coq/Bast0.v

@@ -24,6 +24,7 @@ ChangeLog:
 (* ************* ************************************* *****)
 (* ftl interface *)
 
+Require Import Omega.
 Require Import ListEx.
 Require Import Monad.
 Require Import Data.

bast0-coq/FTLLems2.v

@@ -11,6 +11,7 @@
 (*                                                                            *)
 (* ************************************************************************** *)
 
+Require Import Omega.
 Require Import LibEx.
 Require Import List.
 Require Import ListEx.

bast0-coq/Inv2.v

@@ -11,7 +11,7 @@
 (*                                                                            *)
 (* ************************************************************************** *)
 
-
+Require Import Omega.
 Require Import List.
 Require Import ListEx.
 Require Import LibEx.

bast0-coq/InvLems.v

@@ -11,6 +11,7 @@
 (*                                                                            *)
 (* ************************************************************************** *)
 
+Require Import Omega.
 Require Import List.
 Require Import ListEx.
 Require Import LibEx.
@@ -590,7 +591,9 @@ Proof.
       intros.
       subst x bmrd.
       assert (Hy := bmt_update_pbn_in_bmt_lbn_neq_rev _ _ _ _ _ _ Hu (neq_sym Hlbn12) Hpbn1).
-      eapply HI71; eauto.
+      eapply HI71.
+      apply Hlbn12.
+      apply Hy.
       left.
       exists bmrl.
       trivial.

bast0-coq/LibEx.v

@@ -28,15 +28,15 @@ Proof.
   intros.
   subst; trivial.
 Qed.
-Implicit Arguments eq_sym [A n m].
+Arguments eq_sym [A n m].
 
 (* deprecated, use "neq_sym" instead *)
 Lemma neq_refl : forall n m : nat, n <> m -> m <> n.
 Proof.
   intros.
   intro HF; subst; auto.
 Qed.
-Implicit Arguments neq_refl [n m].
+Arguments neq_refl [n m].
 
 Lemma neq_sym : forall {A: Type} (n m : A), n <> m -> m <> n.
 Proof.

bast0-coq/ListEx.v

@@ -430,7 +430,6 @@ Proof.
       solvebnat.
     destruct (H2 (refl_equal _)) as [H3 [H4 H5]].
     subst.
-    subst a.
     simpl; split; trivial.
   simpl in H.
   destruct (@list_get_list_append_some_elim _ _ _ _ _ H) as [H1 H2].

bast0-coq/Makefile

@@ -1,154 +1,10 @@
-#############################################################
-#                                                           #
-#    GNUMakefile for coq code                               #
-#                                                           #
-#        by Guo Yu					    #
-#    	 1.1beta           				    #
-#        - 2014-05-03                                       #
-#                                                           #
-#############################################################
+.PHONY: clean
 
-SHELL = /bin/bash
-ECHO := /bin/echo
+all: Makefile.coq
+	$(MAKE) -f Makefile.coq
 
-COQC := $(COQBIN)coqc
-COQFLAGS = $(COQLIBS)
-COQDEP := $(COQBIN)coqdep
-COQDOC := $(COQBIN)coqdoc
-GALLINA := $(COQBIN)gallina
-
-COQLIBS := -I .
-
-.PHONY: noargs FORCE
-
-noargs : Verification.vo
-
-FORCE: ;
-
-###########################################
-#   Source Code
-###########################################
-
-SRC := $(wildcard *.v)
-
-###########################################
-#   Modules
-###########################################
-
-# .PHONY: modules
-
-# mods.inc:
-# 	@$(ECHO) -n 'MOD :='> $@
-# 	@find -type d ! -name '.' | grep -v '.svn' | grep -v 'CVS' \
-# 	| sed -e 's/^\.\///g' | xargs echo -n >> $@
-
-# -include mods.inc
-
-# MOD_MK := $(patsubst %, %/module.mk, $(MOD))
-# MOD_MK2 := $(patsubst %, %/makefile, $(MOD))
-
-# %/module.mk:
-# 	@$(ECHO) "generating $@ ..."
-# 	@$(ECHO) "MODULE := $*" > $@
-# 	@$(ECHO) 'SRC += $$(wildcard $$(MODULE)/*.v)' >> $@
-# 	@$(ECHO) 'COQLIBS += -I $$(MODULE) ' >> $@
-# 	@$(ECHO) "generating $*/makefile ..."
-# 	@$(ECHO) "include module.mk" > $*/makefile
-# 	@$(ECHO) -e '\n.PHONY: all FORCE\n' >> $*/makefile
-# 	@$(ECHO) -e 'SRC := $$(wildcard *.v)\n' >> $*/makefile
-# 	@$(ECHO) -e 'OBJ := $$(SRC:.v=.vo)\n' >> $*/makefile
-# 	@$(ECHO) -e 'all: $$(OBJ) ;\n' >> $*/makefile
-# 	@$(ECHO) -e 'FORCE: ;\n' >> $*/makefile
-# 	@$(ECHO) -e '%.vo: FORCE \n\tmake -C $(shell echo "$*" \
-# 	| sed -e "s/[^/]\+/../g") $$(MODULE)/$$@' >> $*/makefile
-# 	@$(ECHO) -e '\ntestmk:\n\tmake -f module.mk\n' >> $*/makefile
-# 	@$(ECHO) -e '\nclean:\n\trm -f *.vo *.d\n\trm -f *.html\n' >> $*/makefile
-
-# -include $(MOD_MK)
-
-###########################################
-#   Objective File
-###########################################
-
-DEP := $(SRC:.v=.d)
-OBJ := $(SRC:.v=.vo)
-SPEC := $(SRC:.v=.vi)
-GOBJ := $(SRC:.v=.g)
-HTML := $(SRC:.v=.html)
-GHTML := $(SRC:.v=.g.html)
-
-.PHONY: test
-test:
-	@echo "######################################################"
-	@echo -n "MOD = "
-	@echo $(MOD)
-	@echo "MAIN_MOD = " $(MAIN_MOD)
-	@echo -n "Modules Makfile = "
-	@echo $(MOD_MK)
-	@echo -n "SRC = "
-	@echo $(SRC)
-	@echo -n "OBJ = "
-	@echo $(OBJ)
-	@echo -n "VMOD = "
-	@echo $(VMOD)
-	@echo -n "MODRPATH = "
-	@echo $(MODRPATH)
-	@echo -n "COQFLAGS = "
-	@echo $(COQFLAGS)
-
-###########################################
-#    Special targets
-###########################################
-
-.PHONY: all depends
-
-all : $(OBJ)
-
-%.vo:	%.v %.d
-	$(COQC) $(COQFLAGS) $<
-
-%.d:	%.v
-	$(COQDEP) $(COQFLAGS) $< > $@
-
-%.g: 	%.v
-	$(GALLINA) $<
-
-# %.tex: %.g
-# 	$(COQDOC) -latex -g $< -o $@
-
-# %.html: %.g
-# 	$(COQDOC) -html -g $< -o $@
-
--include $(DEP)
-
-###########################################
-#  User-defined targets
-###########################################
-
-#.PHONY: ocap
-#pcap: ocap/ocap.vo
-
-###########################################
-#  deploy makefile
-###########################################
-
-.PHONY: deploy
-deploy: 
-	make depends
-
-###########################################
-#   clean
-###########################################
-
-.PHONY: archclean clean
+Makefile.coq:
+	coq_makefile -f _CoqProject -o Makefile.coq
 
 clean:
-	rm -f $(OBJ)
-	rm -f $(DEP)
-	rm -f $(HTMLFILES) $(GHTMLFILES)
-
-archclean: 
-	rm -f *.cmx *.o *.vo *.glob *.d
-	rm -f $(MOD_MK) $(MOD_MK2)
-	rm -f mods.inc
-
+	$(MAKE) -f Makefile.coq clean

bast0-coq/_CoqProject

@@ -0,0 +1,20 @@
+-R . Top
+LibEx.v
+bnat.v
+ListEx.v
+Monad.v
+Data.v
+Params.v
+Nand.v
+NandLems.v
+Bast0.v
+FTLProp.v
+Framework.v
+FTLLems.v
+Inv.v
+Inv2.v
+InvLems.v
+FTLLems2.v
+FTLLems3.v
+FTLLems4.v
+Verification.v