Commit 7383a08b authored by charguer's avatar charguer

porting_1

parent 8b3960d6
This diff is collapsed.
......@@ -251,23 +251,23 @@ Local Open Scope tag_scope.
(* ** Notation for applied characteristic formulae [tag_goal] *)
Notation "P1 '==>' P2" :=
(@pred_le heap P1 P2) (at level 55, right associativity,
(@pred_incl heap P1 P2) (at level 55, right associativity,
format "'[v' '[' P1 ']' '/' '==>' '/' '[' P2 ']' ']'" )
: charac.
Notation " Q1 '===>' Q2" :=
(@rel_le _ heap Q1 Q2) (at level 55, right associativity,
(@rel_incl' _ heap Q1 Q2) (at level 55, right associativity,
format "'[v' '[' Q1 ']' '/' '===>' '/' '[' Q2 ']' ']'")
: charac.
Notation "'PRE' P1 '==>' 'POST' P2" :=
(@pred_le heap P1 P2) (at level 69,
(@pred_incl heap P1 P2) (at level 69,
format "'[v' '[' 'PRE' P1 ']' '/' '==>' '/' '[' 'POST' P2 ']' ']'",
only parsing)
: charac.
Notation "'PRE' Q1 '===>' 'POST' Q2" :=
(@rel_le _ heap Q1 Q2) (at level 69,
(@rel_incl' _ heap Q1 Q2) (at level 69,
format "'[v' '[' 'PRE' Q1 ']' '/' '===>' '/' '[' 'POST' Q2 ']' ']'",
only parsing)
: charac.
......
......@@ -210,8 +210,8 @@ Tactic Notation "xclean" :=
*)
Ltac xok_core cont := (* see [xok] spec further *)
solve [ hnf; apply rel_le_refl
| apply pred_le_refl
solve [ hnf; apply rel_incl_refl
| apply pred_incl_refl
| apply hsimpl_to_qunit; reflexivity
| hsimpl; cont tt ].
......@@ -396,7 +396,7 @@ Ltac xpost_core Q :=
| _ => constr:(Q)
end in
match cfml_postcondition_is_evar tt with
| true => apply (@fix_post _ Q'); [ try xlocal | xtag_pre_post | apply rel_le_refl ]
| true => apply (@fix_post _ Q'); [ try xlocal | xtag_pre_post | apply rel_incl_refl ]
| false => apply (@fix_post _ Q'); [ try xlocal | xtag_pre_post | ]
end.
......@@ -742,7 +742,7 @@ Ltac xchange_forwards L modif cont :=
match modif with
| __ =>
match type of K with
| _ = _ => xchange_apply (@pred_le_proj1 _ _ _ K) cont
| _ = _ => xchange_apply (@pred_incl_proj1 _ _ _ K) cont
| _ => xchange_apply K cont
end
| _ => xchange_apply (@modif _ _ _ K) cont
......@@ -774,7 +774,7 @@ Tactic Notation "xchange" "*" constr(E) :=
xchange E; xauto*.
Tactic Notation "xchange" "<-" constr(E) :=
xchange_base ltac:(fun tt => hsimpl) E pred_le_proj2.
xchange_base ltac:(fun tt => hsimpl) E pred_incl_proj2.
Tactic Notation "xchange" "~" "<-" constr(E) :=
xchange <- E; xauto~.
Tactic Notation "xchange" "*" "<-" constr(E) :=
......@@ -783,18 +783,18 @@ Tactic Notation "xchange" "*" "<-" constr(E) :=
Tactic Notation "xchange_no_simpl" constr(E) :=
xchange_base ltac:(fun tt => idtac) E __.
Tactic Notation "xchange_no_simpl" "<-" constr(E) :=
xchange_base ltac:(fun tt => idtac) E pred_le_proj2.
xchange_base ltac:(fun tt => idtac) E pred_incl_proj2.
Tactic Notation "xchange_show" constr(E) :=
xchange_forwards E __ ltac:(idcont).
Tactic Notation "xchange_show" "<-" constr(E) :=
xchange_forwards pred_le_proj2 ltac:(idcont).
xchange_forwards pred_incl_proj2 ltac:(idcont).
(* DEPRECATED:
Tactic Notation "xchange" "->" constr(E) :=
xchange_base ltac:(fun tt => hsimpl) E pred_le_proj1.
xchange_base ltac:(fun tt => hsimpl) E pred_incl_proj1.
Tactic Notation "xchange" constr(E) "as" :=
xchange E; try xpull.
......@@ -1028,7 +1028,7 @@ Ltac xgen_abstract H E :=
Ltac xgen_no_simpl E :=
match goal with |- ?H ==> _ =>
let J := xgen_abstract H E in
eapply pred_le_trans; [ apply (@xgen_lemma _ J E) | ] end.
eapply pred_incl_trans; [ apply (@xgen_lemma _ J E) | ] end.
Ltac xgen_base E :=
xgen_no_simpl E.
......
......@@ -3,48 +3,12 @@ Set Implicit Arguments.
(********************************************************************)
(** Notation for functions expecting tuples as arguments *)
(** Note: this will later move to TLC *)
Notation "'fun' ''' ( x1 , x2 ) ':' T '=>' E" :=
(fun p : T => let '(x1,x2) := p in E)
(at level 200) : fun_scope.
Notation "'fun' ''' ( x1 , x2 ) '=>' E" :=
(fun p => let '(x1,x2) := p in E)
(at level 200, format "'fun' ''' ( x1 , x2 ) '=>' E") : fun_scope.
Notation "'fun' ''' ( x1 , x2 , x3 ) ':' T '=>' E" :=
(fun p : T => let '(x1,x2,x3) := p in E)
(at level 200) : fun_scope.
Notation "'fun' ''' ( x1 , x2 , x3 ) '=>' E" :=
(fun p => let '(x1,x2,x3) := p in E)
(at level 200, format "'fun' ''' ( x1 , x2 , x3 ) '=>' E") : fun_scope.
(* TODO: coqbug?
Notation "'fun' ''' ( x1 , x2 , x3 , x4) ':' T '=>' E" :=
(fun p : T => let '(x1,x2,x3,x4) := p in E)
(at level 60, E at level 200) : fun_scope.
Notation "'fun' ''' ( x1 , x2 , x3 , x4 ) '=>' E" :=
(fun p => match p with (x1,x2,x3,x4) => E end)
(at level 60, E at level 200, format "'fun' ''' ( x1 , x2 , x3 , x4 ) '=>' E") : fun_scope.
*)
Open Scope fun_scope.
(********************************************************************)
(** Treatment of partially-applied equality *)
Require Import LibTactics LibCore LibEpsilon.
Hint Unfold pred_le.
Hint Unfold pred_incl.
Tactic Notation "false" "~" constr(E) :=
false E; instantiate; auto_tilde.
......@@ -67,19 +31,19 @@ Ltac app_evar t A cont ::=
Lemma if_eq_1 : forall A (x:bool) (v1 v2 y : A),
((if x then = v1 else = v2) y) -> (y = (if x then v1 else v2)).
Proof. tautob~. Qed.
Proof. tautob. Qed.
Lemma if_eq_2 : forall A (x:bool) (v1 v2 y : A),
((if x then eq v1 else = v2) y) -> (y = (if x then v1 else v2)).
Proof. tautob~. Qed.
Proof. tautob. Qed.
Lemma if_eq_3 : forall A (x:bool) (v1 v2 y : A),
((if x then = v1 else eq v2) y) -> (y = (if x then v1 else v2)).
Proof. tautob~. Qed.
Proof. tautob. Qed.
Lemma if_eq_4 : forall A (x:bool) (v1 v2 y : A),
((if x then eq v1 else eq v2) y) -> (y = (if x then v1 else v2)).
Proof. tautob~. Qed.
Proof. tautob. Qed.
Tactic Notation "if_eq" "in" hyp(H) :=
let go L := apply L in H in
......@@ -118,7 +82,7 @@ Ltac injects_core :=
end.
Ltac substs_base :=
try fold_bool; calc_partial_eq tt; repeat substs_core;
try rew_bool_eq in *; calc_partial_eq tt; repeat substs_core;
try injects_core;
try injects_core;
try injects_core;
......@@ -138,6 +102,18 @@ Ltac subst_hyp_core H :=
| ?x = ?y => first [ subst x | subst y ]
end.
Lemma istrue_isTrue_forw : forall (P:Prop),
istrue (isTrue P) -> P.
Proof using. intros. rew_istrue~ in *. Qed.
Lemma eq_true_r_back : forall (b:bool),
b -> b = true.
Proof using. tautob. Qed.
Lemma eq_false_r_back : forall (b:bool),
!b -> b = false.
Proof using. tautob. Qed.
Ltac subst_hyp_base H :=
match type of H with
| ?x = ?y => first [ subst x | subst y ]
......@@ -153,9 +129,11 @@ Ltac subst_hyp_base H :=
Tactic Notation "subst_hyp" hyp(H) :=
subst_hyp_base H.
(* DEPRECATED
Lemma demo_subst_hyp_1 : forall (x y : int),
x '= y -> y '= x.
Proof. introv H. subst_hyp H. fold_prop. auto. Qed.
*)
Lemma demo_subst_hyp_2 : forall (x y : bool),
x -> !y -> x <> y.
......@@ -202,7 +180,7 @@ Proof. constructors. eauto. Qed.
Definition blocker (A:Type) (X:A) := proj1_sig (blocker_def X).
Implicit Arguments blocker [ A ].
Arguments blocker [A].
Definition blocker_eq : forall (A:Type) (X:A), blocker X = X.
Proof. intros. unfold blocker. apply (proj2_sig (blocker_def X)). Qed.
......@@ -269,10 +247,10 @@ Lemma bool_of_True : bool_of P b -> P -> b.
Proof. unfold bool_of. intros. subst~. Qed.
Lemma bool_of_False : bool_of P b -> ~ P -> !b.
Proof. unfold bool_of. intros. subst~. rew_reflect~. Qed.
Proof. unfold bool_of. intros. subst~. rew_istrue~. Qed.
Lemma bool_of_prove : (b <-> P) -> bool_of P b.
Proof. intros. extens*. Qed.
Proof. intros. unfold bool_of. extens*. Qed.
(* todo: add isTrue true = P to fold_prop *)
End BoolOf.
......@@ -280,7 +258,7 @@ End BoolOf.
Lemma bool_of_eq : forall (P Q : Prop),
(P <-> Q) -> ((bool_of P) = (bool_of Q)).
Proof.
intros. apply prop_ext_1. intros_all. unfold bool_of;
intros. extens. intros_all. unfold bool_of;
iff; rewrite H0; apply* prop_ext.
Qed.
......@@ -298,17 +276,17 @@ Proof. unfold bool_of. intros. subst. extens*. Qed.
Lemma bool_of_impl_neg : forall (P Q : Prop) x,
bool_of P x -> (~P <-> Q) -> bool_of Q (!x).
Proof. unfold bool_of. intros. subst. extens. rew_reflect*. Qed.
Proof. unfold bool_of. intros. subst. extens. rew_istrue~. Qed.
Lemma bool_of_neg_impl : forall (P Q : Prop) x,
bool_of P (!x) -> (~P <-> Q) -> bool_of Q x.
Proof.
unfold bool_of. introv M K. subst. extens.
rew_reflect in K. rew_logic in K. auto.
rew_istrue in K. rew_logic in K. auto.
Qed.
Lemma pred_le_bool_of : forall (P Q : Prop),
(P <-> Q) -> (pred_le (bool_of P) (bool_of Q)).
(P <-> Q) -> (pred_incl (bool_of P) (bool_of Q)).
Proof. unfold bool_of; intros_all. rewrite H0. apply~ prop_ext. Qed.
(** Tactics for normalizing hypotheses *)
......@@ -318,9 +296,6 @@ Lemma true_eq_P : forall (P:Prop),
Proof. intros. apply prop_ext. iff. subst~. apply* prop_ext. Qed.
Hint Rewrite true_eq_P : rew_reflect.
Hint Rewrite isTrue_istrue istrue_isTrue : rew_istrue.
Ltac rew_istrue := autorewrite with rew_istrue.
Ltac fix_bool_of_known tt :=
match goal with
| H: bool_of ?P true |- _ =>
......@@ -353,11 +328,11 @@ Tactic Notation "boolofs" "*" := boolofs; auto_star.
(* ** Clean boolean reflection and partially applied equality *)
(** [reflect_clean tt] normalizes partially-applied equality
and calls the tactic [logics], which normalizes bool/prop
and calls the tactic [rew_bool_eq], which normalizes bool/prop
coercions. *)
Ltac reflect_clean tt :=
calc_partial_eq tt; logics.
calc_partial_eq tt; rew_bool_eq in *.
......@@ -376,20 +351,32 @@ Ltac invert_first_hyp ::=
(********************************************************************)
(* ** Predicate weakening *)
Notation "P ==> Q" := (pred_le P Q)
Notation "P ==> Q" := (pred_incl P Q)
(at level 55, right associativity) : func.
Open Scope func.
Hint Resolve pred_le_refl.
Hint Resolve pred_incl_refl.
Lemma weaken_bool_of : forall (P Q : Prop),
(P <-> Q) -> ((bool_of P) ==> (bool_of Q)).
Proof. unfold bool_of. intros_all. rewrite H0. extens*. Qed.
Notation "P ===> Q" := (rel_le P Q)
(* [rel_incl'] is like [rel_incl] but defined in terms of [pred_incl]
so that after [intros r] we get an entailment. *)
Definition rel_incl' A B (P Q:A->B->Prop) :=
forall r, (P r ==> Q r).
Notation "P ===> Q" := (rel_incl' P Q)
(at level 55, right associativity) : func.
Lemma refl_rel_incl' : forall A B (P:A->B->Prop),
P ===> P.
Proof using. apply refl_rel_incl. Qed.
Hint Resolve refl_rel_incl'.
Open Scope func.
Lemma pred_le_extens : forall A (H1 H2 : A->Prop),
......@@ -404,16 +391,15 @@ Lemma pred_le_proj2 : forall A (H1 H2 : A->Prop),
H1 = H2 -> H2 ==> H1.
Proof. intros. subst~. Qed.
Implicit Arguments pred_le_proj1 [A H1 H2].
Implicit Arguments pred_le_proj2 [A H1 H2].
Implicit Arguments pred_le_extens [A H1 H2].
Arguments pred_le_proj1 [A] [H1] [H2].
Arguments pred_le_proj2 [A] [H1] [H2].
Arguments pred_le_extens [A] [H1] [H2].
(********************************************************************)
(* Hints *)
Hint Constructors Mem. (* todo: should be put in the developments *)
Hint Resolve rel_le_refl.
Hint Constructors mem. (* todo: should be put in the developments *)
(* todo: is this needed? *)
Lemma not_True_to_False : ~ True -> False.
......@@ -434,7 +420,7 @@ Hint Resolve @pair : typeclass_instances.
(* todo: move *)
Lemma Inhab_intro : forall (A:Type),
A -> Inhab A.
Proof. introv x. apply (prove_Inhab x). Qed.
Proof. introv x. apply (Inhab_of_val x). Qed.
Ltac inhab :=
intros; apply Inhab_intro; intros; try solve
......@@ -444,9 +430,9 @@ Ltac inhab :=
| apply @arbitrary; eauto 10 with typeclass_instances ].
Instance Z_inhab : Inhab Z.
Proof. apply (prove_Inhab 0%Z). Qed.
Proof. apply (Inhab_of_val 0%Z). Qed.
Hint Resolve bool_inhab.
Hint Resolve Inhab_bool.
Lemma inhab_demo : Inhab Z.
Proof. inhab. Qed.
......@@ -455,13 +441,16 @@ Proof. inhab. Qed.
(********************************************************************)
(* Maths *)
Hint Rewrite downto_def nat_upto_wf upto_def : rew_maths.
Hint Rewrite downto_eq upto_eq : rew_maths.
Hint Resolve wf_nat_upto : wf.
(** Hack for Zsub to be opaque. Use "Import ZsubNoSimpl."
to prevent unwanted simplifications of "-", while still
allowing "omega" tactic to work. *)
(* TODO: see whether this could be removed in coq-8.6. *)
Module ZsubNoSimpl.
Definition Zsub := Zminus.
......@@ -477,7 +466,7 @@ Module ZsubNoSimpl.
Hint Rewrite Zsub_eq : rew_maths.
End ZsubNoSimpl.
End ZsubNoSimpl.
......@@ -4,15 +4,15 @@ pwd
COQBIN=
if [ -f ./settings.sh ]
then
source settings.sh
source settings.sh
fi
if [ -f ../settings.sh ]
then
source ../settings.sh
source ../settings.sh
fi
if [ -f ../../settings.sh ]
then
source ../../settings.sh
source ../../settings.sh
fi
# TODO: improve with a while loop?
......@@ -43,10 +43,11 @@ then
fi
echo ${COQBIN}coqide ${COQINCLUDE} ${FILE}
${COQBIN}coqide ${COQINCLUDE} ${FILE}
echo "using single worker"
${COQBIN}coqide ${COQINCLUDE} ${FILE} -async-proofs off -async-proofs-command-error-resilience off
#-dont-load-proofs -async-proofs-j 1
#-dont-load-proofs -async-proofs-j 1 -async-proofs 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