Commit 755ada18 authored by charguer's avatar charguer

progress

parent a375c221
clean up CFAsymptoticsDemos.v
=============
opam switch 4.03.0 opam switch 4.03.0
eval `opam config env` eval `opam config env`
......
...@@ -107,7 +107,7 @@ let formula_type = ...@@ -107,7 +107,7 @@ let formula_type =
(** Hprop entailment [H1 ==> H2] *) (** Hprop entailment [H1 ==> H2] *)
let heap_impl h1 h2 = let heap_impl h1 h2 =
coq_apps (Coq_var "TLC.LibLogic.pred_le") [h1;h2] coq_apps (Coq_var "TLC.LibLogic.pred_incl") [h1;h2]
(** Specialized Hprop entailment [H1 ==> Q2 tt] *) (** Specialized Hprop entailment [H1 ==> Q2 tt] *)
...@@ -117,7 +117,7 @@ let heap_impl_unit h1 q2 = ...@@ -117,7 +117,7 @@ let heap_impl_unit h1 q2 =
(** Postcondition entailment [Q1 ===> Q2] *) (** Postcondition entailment [Q1 ===> Q2] *)
let post_impl q1 q2 = let post_impl q1 q2 =
coq_apps (Coq_var "TLC.LibRelation.rel_le") [q1;q2] coq_apps (Coq_var "TLC.LibRelation.rel_incl'") [q1;q2]
(** Specialized post-conditions [fun (_:unit) => H], i.e. [# H] *) (** Specialized post-conditions [fun (_:unit) => H], i.e. [# H] *)
......
...@@ -345,10 +345,10 @@ let inlined_primitives_table = ...@@ -345,10 +345,10 @@ let inlined_primitives_table =
"Pervasives.||", (Primitive_binary_lazy, "TLC.LibBool.or"); "Pervasives.||", (Primitive_binary_lazy, "TLC.LibBool.or");
"Pervasives.=", (Primitive_binary_only_numbers, "(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (Coq.Init.Logic.eq x__ y__))"); "Pervasives.=", (Primitive_binary_only_numbers, "(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (Coq.Init.Logic.eq x__ y__))");
"Pervasives.<>", (Primitive_binary_only_numbers, "(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (Coq.Init.Logic.not (Coq.Init.Logic.eq x__ y__)))"); "Pervasives.<>", (Primitive_binary_only_numbers, "(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (Coq.Init.Logic.not (Coq.Init.Logic.eq x__ y__)))");
"Pervasives.<", (Primitive_binary_only_numbers, "(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.lt _ (@TLC.LibOrder.lt_from_le Coq.ZArith.BinInt.Z TLC.LibInt.le_int_inst) x__ y__))"); "Pervasives.<", (Primitive_binary_only_numbers, "(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.lt _ (@TLC.LibOrder.lt_of_le Coq.ZArith.BinInt.Z TLC.LibInt.le_int_inst) x__ y__))");
"Pervasives.<=", (Primitive_binary_only_numbers, "(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.le _ TLC.LibInt.le_int_inst x__ y__))"); "Pervasives.<=", (Primitive_binary_only_numbers, "(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.le _ TLC.LibInt.le_int_inst x__ y__))");
"Pervasives.>", (Primitive_binary_only_numbers, "(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.gt _ (@TLC.LibOrder.gt_from_le _ TLC.LibInt.le_int_inst) x__ y__))"); "Pervasives.>", (Primitive_binary_only_numbers, "(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.gt _ (@TLC.LibOrder.gt_of_le _ TLC.LibInt.le_int_inst) x__ y__))");
"Pervasives.>=", (Primitive_binary_only_numbers, "(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.ge _ (@TLC.LibOrder.ge_from_le _ TLC.LibInt.le_int_inst) x__ y__))"); "Pervasives.>=", (Primitive_binary_only_numbers, "(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.ge _ (@TLC.LibOrder.ge_of_le _ TLC.LibInt.le_int_inst) x__ y__))");
"Pervasives.max", (Primitive_binary_only_numbers, "Coq.ZArith.BinInt.Zmax"); "Pervasives.max", (Primitive_binary_only_numbers, "Coq.ZArith.BinInt.Zmax");
"Pervasives.min", (Primitive_binary_only_numbers, "Coq.ZArith.BinInt.Zmin"); "Pervasives.min", (Primitive_binary_only_numbers, "Coq.ZArith.BinInt.Zmin");
"List.length", (Primitive_unary, "(@TLC.LibListZ.length _)"); "List.length", (Primitive_unary, "(@TLC.LibListZ.length _)");
......
...@@ -13,11 +13,11 @@ Definition h x := g (f x). ...@@ -13,11 +13,11 @@ Definition h x := g (f x).
Definition proj1_exists (A:Type) (P:A->Prop) (H: exists x, P x) : A := Definition proj1_exists (A:Type) (P:A->Prop) (H: exists x, P x) : A :=
proj1_sig (indefinite_description H). proj1_sig (indefinite_description H).
Implicit Arguments proj1_exists [A P]. Arguments proj1_exists [A] [P].
Definition proj2_exists (A:Type) (P:A->Prop) (H: exists x, P x) : (P (proj1_exists H)) := Definition proj2_exists (A:Type) (P:A->Prop) (H: exists x, P x) : (P (proj1_exists H)) :=
proj2_sig (indefinite_description H). proj2_sig (indefinite_description H).
Implicit Arguments proj2_exists [A P]. Arguments proj2_exists [A P].
Lemma proj1_exists_prop : forall (A:Type) (P:A->Prop) (H: exists x, P x) x, Lemma proj1_exists_prop : forall (A:Type) (P:A->Prop) (H: exists x, P x) x,
x = proj1_exists H -> P x. x = proj1_exists H -> P x.
...@@ -25,7 +25,7 @@ Proof using. ...@@ -25,7 +25,7 @@ Proof using.
intros. subst. applys proj2_exists. intros. subst. applys proj2_exists.
Qed. Qed.
Implicit Arguments proj1_exists_prop [A P]. Arguments proj1_exists_prop [A] [P].
......
...@@ -29,7 +29,7 @@ Implicit Types x y z : int. ...@@ -29,7 +29,7 @@ Implicit Types x y z : int.
(** Additional lemmas on credits *) (** Additional lemmas on credits *)
Definition credits_nat_eq := Definition credits_nat_eq :=
func_eq_1 heap_is_credits_nat. args_eq_1 heap_is_credits_nat.
(* todo: state as a lemma instead *) (* todo: state as a lemma instead *)
Lemma credits_nat_zero_eq_prove : forall (n:nat), Lemma credits_nat_zero_eq_prove : forall (n:nat),
...@@ -495,15 +495,15 @@ Proof using. math. Qed. ...@@ -495,15 +495,15 @@ Proof using. math. Qed.
Lemma int_mul_succ_nat : forall (n:nat) x, Lemma int_mul_succ_nat : forall (n:nat) x,
(S n)%nat * x = x + n*x. (S n)%nat * x = x + n*x.
Proof using. intros. math_debug. ring. Qed. Proof using. intros. math_setup. ring. Qed.
Lemma int_mul_plus_one_nat : forall (n:nat) x, Lemma int_mul_plus_one_nat : forall (n:nat) x,
(1+n)%nat * x = x + n*x. (1+n)%nat * x = x + n*x.
Proof using. intros. math_debug. ring. Qed. Proof using. intros. math_setup. ring. Qed.
Lemma int_mul_assoc : forall x y z, Lemma int_mul_assoc : forall x y z,
x * (y*z) = x * y * z. x * (y*z) = x * y * z.
Proof using. intros. math_debug. ring. Qed. Proof using. intros. math_setup. ring. Qed.
Lemma int_add_assoc : forall x y z, Lemma int_add_assoc : forall x y z,
x + (y+z) = x + y + z. x + (y+z) = x + y + z.
...@@ -511,11 +511,11 @@ Proof using. math. Qed. ...@@ -511,11 +511,11 @@ Proof using. math. Qed.
Lemma int_mul_plus_one_l : forall n x, Lemma int_mul_plus_one_l : forall n x,
(1+n) * x = x + n*x. (1+n) * x = x + n*x.
Proof using. intros. math_debug. ring. Qed. Proof using. intros. math_setup. ring. Qed.
Lemma int_mul_plus_one_r : forall n x, Lemma int_mul_plus_one_r : forall n x,
x * (1+n) = x + x*n. x * (1+n) = x + x*n.
Proof using. intros. math_debug. ring. Qed. Proof using. intros. math_setup. ring. Qed.
Hint Rewrite int_mul_assoc int_add_assoc Hint Rewrite int_mul_assoc int_add_assoc
int_mul_zero_l int_mul_one_l int_mul_zero_nat_l int_mul_one_nat_l int_mul_zero_l int_mul_one_l int_mul_zero_nat_l int_mul_one_nat_l
...@@ -585,7 +585,7 @@ End SimplNonneg. ...@@ -585,7 +585,7 @@ End SimplNonneg.
Ltac simpl_nonneg_step tt := Ltac simpl_nonneg_step tt :=
match goal with |- ?G => match G with match goal with |- ?G => match G with
| ?x >= ?y => apply ineq_le_to_ge | ?x >= ?y => apply ineq_le_to_ge
| (0 <= my_Z_of_nat ?n)%I => apply nonneg_nat | (0 <= nat_to_Z ?n)%I => apply nonneg_nat
| (0 <= Z.of_nat)%I => apply nonneg_nat | (0 <= Z.of_nat)%I => apply nonneg_nat
| (0 <= ?x + ?y) => apply nonneg_add | (0 <= ?x + ?y) => apply nonneg_add
| (0 <= ?x * ?y) => apply nonneg_mul | (0 <= ?x * ?y) => apply nonneg_mul
......
...@@ -11,7 +11,7 @@ include $(CFML)/Makefile.common ...@@ -11,7 +11,7 @@ include $(CFML)/Makefile.common
PWD := $(shell pwd) PWD := $(shell pwd)
V := $(wildcard $(PWD)/*.v) V := $(wildcard $(PWD)/*.v)
ifdef ARTHUR ifdef INCLUDE_TLC_AS_DEPENDENCIES
# For Arthur: encompass TLC in the scope of the dependency graph. # For Arthur: encompass TLC in the scope of the dependency graph.
# This allows us to recompile part of TLC, if it has changed. # This allows us to recompile part of TLC, if it has changed.
V_AUX := $(wildcard $(TLC)/*.v) V_AUX := $(wildcard $(TLC)/*.v)
......
Set Implicit Arguments. Set Implicit Arguments.
Require Import CFLib. Require Import CFLib.
Require Import LibListZ. Require Import LibListZ LibListSub.
Require Sys_ml. Require Sys_ml.
Require Array_ml. Require Array_ml.
...@@ -124,7 +124,7 @@ Hint Extern 1 (RegisterSpec Array_ml.make) => Provide make_spec. ...@@ -124,7 +124,7 @@ Hint Extern 1 (RegisterSpec Array_ml.make) => Provide make_spec.
(* TEMPORARY clean up: *) (* TEMPORARY clean up: *)
Local Hint Resolve index_length_unfold int_index_prove. (* for array indexing *) Local Hint Resolve index_of_index_length int_index_prove. (* for array indexing *)
Lemma aaa: forall n, n <= n. Lemma aaa: forall n, n <= n.
Proof. math. Qed. Proof. math. Qed.
...@@ -142,8 +142,8 @@ Lemma singleton_prefix_make: ...@@ -142,8 +142,8 @@ Lemma singleton_prefix_make:
Proof. Proof.
intros. intros.
exists (make (n - 1) x). exists (make (n - 1) x).
rewrite app_cons_one. rewrite app_cons_one_r.
apply* cons_make. apply* cons_make_pred_same.
Qed. Qed.
Lemma prefix_snoc_write: Lemma prefix_snoc_write:
...@@ -159,7 +159,7 @@ Proof. ...@@ -159,7 +159,7 @@ Proof.
destruct ys as [| y ys ]. destruct ys as [| y ys ].
{ false. rewrite app_nil_r in Hp. subst xs. math. } { false. rewrite app_nil_r in Hp. subst xs. math. }
(* The witness is the tail of [ys], now also named [ys]. *) (* The witness is the tail of [ys], now also named [ys]. *)
exists ys. subst zs. rewrite* update_app_right_here. exists ys. subst zs. rewrite* update_middle.
Qed. Qed.
Lemma prefix_identity: Lemma prefix_identity:
...@@ -214,7 +214,7 @@ Proof. ...@@ -214,7 +214,7 @@ Proof.
(* 1. The invariant initially holds. *) (* 1. The invariant initially holds. *)
{ xsimpl (nil & x). { xsimpl (nil & x).
{ rewrite* length_make. } { rewrite* length_make. }
{ rewrite app_nil_l, length_singleton. eauto. } { rewrite app_nil_l, length_one. eauto. }
{ rewrite app_nil_l. apply* singleton_prefix_make. } { rewrite app_nil_l. apply* singleton_prefix_make. }
} }
(* 2. The loop body preserves the invariant. *) (* 2. The loop body preserves the invariant. *)
...@@ -223,7 +223,7 @@ Proof. ...@@ -223,7 +223,7 @@ Proof.
xapp*. xapp*.
xsimpl* (xs & x). xsimpl* (xs & x).
{ rewrite* length_update. } { rewrite* length_update. }
{ rew_length. math. } { rew_list. math. }
{ eauto using prefix_snoc_write. } { eauto using prefix_snoc_write. }
} }
(* 3. The invariant implies the postcondition. *) (* 3. The invariant implies the postcondition. *)
......
...@@ -32,8 +32,8 @@ V := $(patsubst %.ml,%_ml.v,$(ML)) \ ...@@ -32,8 +32,8 @@ V := $(patsubst %.ml,%_ml.v,$(ML)) \
$(patsubst %.ml,%_proof.v,$(ML)) \ $(patsubst %.ml,%_proof.v,$(ML)) \
Stdlib.v Stdlib.v
ifdef ARTHUR ifdef INCLUDE_TLC_AS_DEPENDENCIES
# For Arthur: encompass TLC in the scope of the dependency graph. # encompass TLC in the scope of the dependency graph.
# This allows us to recompile part of TLC, if it has changed. # This allows us to recompile part of TLC, if it has changed.
V_AUX := $(wildcard $(TLC)/*.v) \ V_AUX := $(wildcard $(TLC)/*.v) \
$(wildcard $(LIBCOQ)/*.v) $(wildcard $(LIBCOQ)/*.v)
...@@ -76,7 +76,7 @@ ifndef CFMLC ...@@ -76,7 +76,7 @@ ifndef CFMLC
CFMLC=$(CFML)/generator/main.native CFMLC=$(CFML)/generator/main.native
endif endif
$(PWD)/Pervasives_ml.v $(PWD)/Pervasives.cmj: $(PWD)/Pervasives.ml $(PWD)/Pervasives_ml.v $(PWD)/Pervasives.cmj: $(PWD)/Pervasives.ml $(CFMLC)
$(CFMLC) $(CFML_FLAGS) -nostdlib -nopervasives -I . $< || (rm -f $@; exit 1) $(CFMLC) $(CFML_FLAGS) -nostdlib -nopervasives -I . $< || (rm -f $@; exit 1)
$(PWD)/%_ml.v $(PWD)/%.cmj: $(PWD)/%.ml $(PWD)/Pervasives.cmj $(PWD)/%_ml.v $(PWD)/%.cmj: $(PWD)/%.ml $(PWD)/Pervasives.cmj
......
...@@ -28,7 +28,7 @@ else ...@@ -28,7 +28,7 @@ else
FILE=`find . -name ${FILE}` FILE=`find . -name ${FILE}`
fi fi
COQINCLUDE="-R ${TLC} TLC -R ${CFML}/lib/coq CFML" COQINCLUDE="-R ${TLC} TLC -R ${CFML}/lib/coq CFML -R ${CFML}/lib/stdlib CFML.Stdlib"
PWD=`pwd` PWD=`pwd`
if [[ ${FILE} == *"examples/"* ]] if [[ ${FILE} == *"examples/"* ]]
...@@ -42,12 +42,12 @@ then ...@@ -42,12 +42,12 @@ then
COQINCLUDE="${COQINCLUDE} -R ${EXAMPLE_PATH} EXAMPLE" COQINCLUDE="${COQINCLUDE} -R ${EXAMPLE_PATH} EXAMPLE"
fi fi
echo ${COQBIN}coqide ${COQINCLUDE} ${FILE} echo "${COQBIN}coqide ${COQIDE_OPTIONS} ${COQINCLUDE} ${FILE}"
echo "using single worker" ${COQBIN}coqide ${COQIDE_OPTIONS} ${COQINCLUDE} ${FILE}
${COQBIN}coqide ${COQINCLUDE} ${FILE} -async-proofs off -async-proofs-command-error-resilience off
#-dont-load-proofs -async-proofs-j 1 -async-proofs off #-dont-load-proofs -async-proofs-j 1 -async-proofs off
#-dont-load-proofs -async-proofs-j 1
# COQOPTIONS=-async-proofs off -async-proofs-command-error-resilience off
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment