diff options
-rw-r--r-- | .travis.yml | 1 | ||||
-rw-r--r-- | META.coq | 23 | ||||
-rw-r--r-- | Makefile.ci | 2 | ||||
-rw-r--r-- | Makefile.common | 4 | ||||
-rwxr-xr-x | dev/ci/ci-fiat-parsers.sh | 12 | ||||
-rw-r--r-- | plugins/micromega/coq_micromega.ml | 1 | ||||
-rw-r--r-- | printing/printer.ml | 71 | ||||
-rw-r--r-- | theories/Arith/Between.v | 72 | ||||
-rw-r--r-- | theories/Init/Datatypes.v | 6 | ||||
-rw-r--r-- | theories/Init/Logic.v | 19 | ||||
-rw-r--r-- | theories/PArith/BinPos.v | 28 | ||||
-rw-r--r-- | theories/ZArith/BinInt.v | 45 | ||||
-rw-r--r-- | theories/ZArith/Zorder.v | 6 |
13 files changed, 208 insertions, 82 deletions
diff --git a/.travis.yml b/.travis.yml index de16f2d0b..5ed0809a5 100644 --- a/.travis.yml +++ b/.travis.yml @@ -30,6 +30,7 @@ env: - TEST_TARGET="ci-cpdt" - TEST_TARGET="ci-geocoq" - TEST_TARGET="ci-fiat-crypto" + - TEST_TARGET="ci-fiat-parsers" - TEST_TARGET="ci-flocq" - TEST_TARGET="ci-hott" - TEST_TARGET="ci-iris-coq" @@ -56,7 +56,7 @@ package "vm" ( package "kernel" ( - description = "The Coq's Kernel" + description = "Coq's Kernel" version = "8.6" directory = "kernel" @@ -95,7 +95,7 @@ package "intf" ( package "engine" ( - description = "Coq Libraries (vo) support" + description = "Coq Tactic Engine" version = "8.6" requires = "coq.library" @@ -172,7 +172,7 @@ package "parsing" ( package "printing" ( - description = "Coq Printing Libraries" + description = "Coq Printing Engine" version = "8.6" requires = "coq.parsing" @@ -185,7 +185,7 @@ package "printing" ( package "tactics" ( - description = "Coq Tactics" + description = "Coq Basic Tactics" version = "8.6" requires = "coq.printing" @@ -196,12 +196,25 @@ package "tactics" ( ) +package "vernac" ( + + description = "Coq Vernacular Interpreter" + version = "8.6" + + requires = "coq.tactics" + directory = "vernac" + + archive(byte) = "vernac.cma" + archive(native) = "vernac.cmxa" + +) + package "stm" ( description = "Coq State Transactional Machine" version = "8.6" - requires = "coq.tactics" + requires = "coq.vernac" directory = "stm" archive(byte) = "stm.cma" diff --git a/Makefile.ci b/Makefile.ci index e4b5832f6..897318c4d 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -1,5 +1,5 @@ CI_TARGETS=ci-all ci-hott ci-math-comp ci-compcert ci-sf ci-cpdt \ - ci-color ci-math-classes ci-tlc ci-fiat-crypto \ + ci-color ci-math-classes ci-tlc ci-fiat-crypto ci-fiat-parsers \ ci-coquelicot ci-flocq ci-iris-coq ci-metacoq ci-geocoq \ ci-unimath diff --git a/Makefile.common b/Makefile.common index df705034e..1e71bcf7d 100644 --- a/Makefile.common +++ b/Makefile.common @@ -122,12 +122,12 @@ DERIVECMO:=plugins/derive/derive_plugin.cmo LTACCMO:=plugins/ltac/ltac_plugin.cmo SSRMATCHINGCMO:=plugins/ssrmatching/ssrmatching_plugin.cmo -PLUGINSCMO:=$(OMEGACMO) $(ROMEGACMO) $(MICROMEGACMO) $(DECLMODECMO) \ +PLUGINSCMO:=$(LTACCMO) $(OMEGACMO) $(ROMEGACMO) $(MICROMEGACMO) $(DECLMODECMO) \ $(QUOTECMO) $(RINGCMO) \ $(FOURIERCMO) $(EXTRACTIONCMO) \ $(CCCMO) $(FOCMO) $(RTAUTOCMO) $(BTAUTOCMO) \ $(FUNINDCMO) $(NSATZCMO) $(NATSYNTAXCMO) $(OTHERSYNTAXCMO) \ - $(DERIVECMO) $(SSRMATCHINGCMO) $(LTACCMO) + $(DERIVECMO) $(SSRMATCHINGCMO) ifeq ($(HASNATDYNLINK)-$(BEST),false-opt) STATICPLUGINS:=$(PLUGINSCMO) diff --git a/dev/ci/ci-fiat-parsers.sh b/dev/ci/ci-fiat-parsers.sh new file mode 100755 index 000000000..15d73078f --- /dev/null +++ b/dev/ci/ci-fiat-parsers.sh @@ -0,0 +1,12 @@ +#!/bin/bash + +# $0 is not the safest way, but... +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +fiat_parsers_CI_BRANCH=master +fiat_parsers_CI_GITURL=https://github.com/mit-plv/fiat.git + +git_checkout ${fiat_parsers_CI_BRANCH} ${fiat_parsers_CI_GITURL} fiat + +( cd fiat && make -j ${NJOBS} parsers ) diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index e4b58a56f..97f29df82 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -383,7 +383,6 @@ struct let coq_and = lazy (init_constant "and") let coq_or = lazy (init_constant "or") let coq_not = lazy (init_constant "not") - let coq_not_gl_ref = (Nametab.locate ( Libnames.qualid_of_string "Coq.Init.Logic.not")) let coq_iff = lazy (init_constant "iff") let coq_True = lazy (init_constant "True") diff --git a/printing/printer.ml b/printing/printer.ml index bfc2e1bc9..00c2b636b 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -296,6 +296,9 @@ let pr_named_context_of env sigma = let psl = List.rev (fold_named_context make_decl_list env ~init:[]) in hv 0 (prlist_with_sep (fun _ -> ws 2) (fun x -> x) psl) +let pr_var_list_decl env sigma decl = + hov 0 (pr_compacted_decl env sigma decl) + let pr_named_context env sigma ne_context = hv 0 (Context.Named.fold_outside (fun d pps -> pps ++ ws 2 ++ pr_named_decl env sigma d) @@ -329,39 +332,43 @@ let pr_ne_context_of header env sigma = List.is_empty (Environ.named_context env) then (mt ()) else let penv = pr_context_unlimited env sigma in (header ++ penv ++ fnl ()) -let pr_context_limit n env sigma = - let named_context = Environ.named_context env in - let lgsign = List.length named_context in - if n >= lgsign then - pr_context_unlimited env sigma - else - let k = lgsign-n in - let _,sign_env = - Context.Compacted.fold - (fun d (i,pps) -> - if i < k then - (i+1, (pps ++str ".")) - else - let pidt = pr_compacted_decl env sigma d in - (i+1, (pps ++ fnl () ++ - str (emacs_str "") ++ - pidt))) - (Termops.compact_named_context (Environ.named_context env)) ~init:(0,(mt ())) - in - let db_env = - fold_rel_context - (fun env d pps -> - let pnat = pr_rel_decl env sigma d in - (pps ++ fnl () ++ - str (emacs_str "") ++ - pnat)) - env ~init:(mt ()) - in - (sign_env ++ db_env) +let rec bld_sign_env env sigma ctxt pps = + match ctxt with + | [] -> pps + | d:: ctxt' -> + let pidt = pr_var_list_decl env sigma d in + let pps' = pps ++ brk (0,0) ++ pidt in + bld_sign_env env sigma ctxt' pps' + + +let pr_context_limit_compact ?n env sigma = + let ctxt = Termops.compact_named_context (named_context env) in + let lgth = List.length ctxt in + let n_capped = + match n with + | None -> lgth + | Some n when n > lgth -> lgth + | Some n -> n in + let ctxt_chopped,ctxt_hidden = Util.List.chop n_capped ctxt in + (* a dot line hinting the number of hiden hyps. *) + let hidden_dots = String.make (List.length ctxt_hidden) '.' in + let sign_env = v 0 (str hidden_dots ++ (mt ()) + ++ bld_sign_env env sigma (List.rev ctxt_chopped) (mt ())) in + let db_env = + fold_rel_context + (fun env d pps -> pps ++ fnl () ++ pr_rel_decl env sigma d) + env ~init:(mt ()) in + (sign_env ++ db_env) + +(* compact printing an env (variables and de Bruijn). Separator: three + spaces between simple hyps, and newline otherwise *) +let pr_context_unlimited_compact env sigma = + pr_context_limit_compact env sigma -let pr_context_of env sigma = match Flags.print_hyps_limit () with - | None -> hv 0 (pr_context_unlimited env sigma) - | Some n -> hv 0 (pr_context_limit n env sigma) +let pr_context_of env sigma = + match Flags.print_hyps_limit () with + | None -> hv 0 (pr_context_limit_compact env sigma) + | Some n -> hv 0 (pr_context_limit_compact ~n env sigma) (* display goal parts (Proof mode) *) diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v index 58d3a2b38..5a3d5631d 100644 --- a/theories/Arith/Between.v +++ b/theories/Arith/Between.v @@ -24,7 +24,7 @@ Section Between. Lemma bet_eq : forall k l, l = k -> between k l. Proof. - induction 1; auto with arith. + intros * ->; auto with arith. Qed. Hint Resolve bet_eq: arith. @@ -37,9 +37,7 @@ Section Between. Lemma between_Sk_l : forall k l, between k l -> S k <= l -> between (S k) l. Proof. - intros k l H; induction H as [|l H]. - intros; absurd (S k <= k); auto with arith. - destruct H; auto with arith. + induction 1 as [|* [|]]; auto with arith. Qed. Hint Resolve between_Sk_l: arith. @@ -74,32 +72,32 @@ Section Between. Lemma in_int_intro : forall p q r, p <= r -> r < q -> in_int p q r. Proof. - red; auto with arith. + split; assumption. Qed. Hint Resolve in_int_intro: arith. Lemma in_int_lt : forall p q r, in_int p q r -> p < q. Proof. - induction 1; intros. - apply le_lt_trans with r; auto with arith. + intros * []. + eapply le_lt_trans; eassumption. Qed. Lemma in_int_p_Sq : - forall p q r, in_int p (S q) r -> in_int p q r \/ r = q :>nat. + forall p q r, in_int p (S q) r -> in_int p q r \/ r = q. Proof. - induction 1; intros. - elim (le_lt_or_eq r q); auto with arith. + intros p q r []. + destruct (le_lt_or_eq r q); auto with arith. Qed. Lemma in_int_S : forall p q r, in_int p q r -> in_int p (S q) r. Proof. - induction 1; auto with arith. + intros * []; auto with arith. Qed. Hint Resolve in_int_S: arith. Lemma in_int_Sp_q : forall p q r, in_int (S p) q r -> in_int p q r. Proof. - induction 1; auto with arith. + intros * []; auto with arith. Qed. Hint Immediate in_int_Sp_q: arith. @@ -107,10 +105,9 @@ Section Between. forall k l, between k l -> forall r, in_int k l r -> P r. Proof. induction 1; intros. - absurd (k < k); auto with arith. - apply in_int_lt with r; auto with arith. - elim (in_int_p_Sq k l r); intros; auto with arith. - rewrite H2; trivial with arith. + - absurd (k < k). { auto with arith. } + eapply in_int_lt; eassumption. + - destruct (in_int_p_Sq k l r) as [| ->]; auto with arith. Qed. Lemma in_int_between : @@ -120,17 +117,17 @@ Section Between. Qed. Lemma exists_in_int : - forall k l, exists_between k l -> exists2 m : nat, in_int k l m & Q m. + forall k l, exists_between k l -> exists2 m : nat, in_int k l m & Q m. Proof. - induction 1. - case IHexists_between; intros p inp Qp; exists p; auto with arith. - exists l; auto with arith. + induction 1 as [* ? (p, ?, ?)|]. + - exists p; auto with arith. + - exists l; auto with arith. Qed. Lemma in_int_exists : forall k l r, in_int k l r -> Q r -> exists_between k l. Proof. - destruct 1; intros. - elim H0; auto with arith. + intros * (?, lt_r_l) ?. + induction lt_r_l; auto with arith. Qed. Lemma between_or_exists : @@ -139,9 +136,11 @@ Section Between. (forall n:nat, in_int k l n -> P n \/ Q n) -> between k l \/ exists_between k l. Proof. - induction 1; intros; auto with arith. - elim IHle; intro; auto with arith. - elim (H0 m); auto with arith. + induction 1 as [|m ? IHle]. + - auto with arith. + - intros P_or_Q. + destruct IHle; auto with arith. + destruct (P_or_Q m); auto with arith. Qed. Lemma between_not_exists : @@ -150,14 +149,14 @@ Section Between. (forall n:nat, in_int k l n -> P n -> ~ Q n) -> ~ exists_between k l. Proof. induction 1; red; intros. - absurd (k < k); auto with arith. - absurd (Q l); auto with arith. - elim (exists_in_int k (S l)); auto with arith; intros l' inl' Ql'. - replace l with l'; auto with arith. - elim inl'; intros. - elim (le_lt_or_eq l' l); auto with arith; intros. - absurd (exists_between k l); auto with arith. - apply in_int_exists with l'; auto with arith. + - absurd (k < k); auto with arith. + - absurd (Q l). { auto with arith. } + destruct (exists_in_int k (S l)) as (l',[],?). + + auto with arith. + + replace l with l'. { trivial. } + destruct (le_lt_or_eq l' l); auto with arith. + absurd (exists_between k l). { auto with arith. } + eapply in_int_exists; eauto with arith. Qed. Inductive P_nth (init:nat) : nat -> nat -> Prop := @@ -168,15 +167,16 @@ Section Between. Lemma nth_le : forall (init:nat) l (n:nat), P_nth init l n -> init <= l. Proof. - induction 1; intros; auto with arith. - apply le_trans with (S k); auto with arith. + induction 1. + - auto with arith. + - eapply le_trans; eauto with arith. Qed. Definition eventually (n:nat) := exists2 k : nat, k <= n & Q k. Lemma event_O : eventually 0 -> Q 0. Proof. - induction 1; intros. + intros (x, ?, ?). replace 0 with x; auto with arith. Qed. diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index ddaf08bf7..11d80dbc3 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -262,6 +262,11 @@ Inductive comparison : Set := | Lt : comparison | Gt : comparison. +Lemma comparison_eq_stable : forall c c' : comparison, ~~ c = c' -> c = c'. +Proof. + destruct c, c'; intro H; reflexivity || destruct H; discriminate. +Qed. + Definition CompOpp (r:comparison) := match r with | Eq => Eq @@ -326,7 +331,6 @@ Lemma CompSpec2Type : forall A (eq lt:A->A->Prop) x y c, CompSpec eq lt x y c -> CompSpecT eq lt x y c. Proof. intros. apply CompareSpec2Type; assumption. Defined. - (******************************************************************) (** * Misc Other Datatypes *) diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 85123cc44..fb1a7ab1c 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -125,6 +125,25 @@ Proof. [apply Hl | apply Hr]; assumption. Qed. +Theorem imp_iff_compat_l : forall A B C : Prop, + (B <-> C) -> ((A -> B) <-> (A -> C)). +Proof. + intros ? ? ? [Hl Hr]; split; intros H ?; [apply Hl | apply Hr]; apply H; assumption. +Qed. + +Theorem imp_iff_compat_r : forall A B C : Prop, + (B <-> C) -> ((B -> A) <-> (C -> A)). +Proof. + intros ? ? ? [Hl Hr]; split; intros H ?; [apply H, Hr | apply H, Hl]; assumption. +Qed. + +Theorem not_iff_compat : forall A B : Prop, + (A <-> B) -> (~ A <-> ~B). +Proof. + intros; apply imp_iff_compat_r; assumption. +Qed. + + (** Some equivalences *) Theorem neg_false : forall A : Prop, ~ A <-> (A <-> False). diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v index 7baf102aa..d6385ee31 100644 --- a/theories/PArith/BinPos.v +++ b/theories/PArith/BinPos.v @@ -813,6 +813,34 @@ Proof. rewrite compare_cont_spec. unfold ge. destruct (p ?= q); easy'. Qed. +Lemma compare_cont_Lt_not_Lt p q : + compare_cont Lt p q <> Lt <-> p > q. +Proof. + rewrite compare_cont_Lt_Lt. + unfold gt, le, compare. + now destruct compare_cont; split; try apply comparison_eq_stable. +Qed. + +Lemma compare_cont_Lt_not_Gt p q : + compare_cont Lt p q <> Gt <-> p <= q. +Proof. + apply not_iff_compat, compare_cont_Lt_Gt. +Qed. + +Lemma compare_cont_Gt_not_Lt p q : + compare_cont Gt p q <> Lt <-> p >= q. +Proof. + apply not_iff_compat, compare_cont_Gt_Lt. +Qed. + +Lemma compare_cont_Gt_not_Gt p q : + compare_cont Gt p q <> Gt <-> p < q. +Proof. + rewrite compare_cont_Gt_Gt. + unfold ge, lt, compare. + now destruct compare_cont; split; try apply comparison_eq_stable. +Qed. + (** We can express recursive equations for [compare] *) Lemma compare_xO_xO p q : (p~0 ?= q~0) = (p ?= q). diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index 5aa397f8a..1e3ab6687 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -1367,7 +1367,7 @@ Lemma inj_testbit a n : 0<=n -> Z.testbit (Z.pos a) n = N.testbit (N.pos a) (Z.to_N n). Proof. apply Z.testbit_Zpos. Qed. -(** Some results concerning Z.neg *) +(** Some results concerning Z.neg and Z.pos *) Lemma inj_neg p q : Z.neg p = Z.neg q -> p = q. Proof. now injection 1. Qed. @@ -1375,18 +1375,54 @@ Proof. now injection 1. Qed. Lemma inj_neg_iff p q : Z.neg p = Z.neg q <-> p = q. Proof. split. apply inj_neg. intros; now f_equal. Qed. +Lemma inj_pos p q : Z.pos p = Z.pos q -> p = q. +Proof. now injection 1. Qed. + +Lemma inj_pos_iff p q : Z.pos p = Z.pos q <-> p = q. +Proof. split. apply inj_pos. intros; now f_equal. Qed. + Lemma neg_is_neg p : Z.neg p < 0. Proof. reflexivity. Qed. Lemma neg_is_nonpos p : Z.neg p <= 0. Proof. easy. Qed. +Lemma pos_is_pos p : 0 < Z.pos p. +Proof. reflexivity. Qed. + +Lemma pos_is_nonneg p : 0 <= Z.pos p. +Proof. easy. Qed. + +Lemma neg_le_pos p q : Zneg p <= Zpos q. +Proof. easy. Qed. + +Lemma neg_lt_pos p q : Zneg p < Zpos q. +Proof. easy. Qed. + +Lemma neg_le_neg p q : (q <= p)%positive -> Zneg p <= Zneg q. +Proof. intros; unfold Z.le; simpl. now rewrite <- Pos.compare_antisym. Qed. + +Lemma neg_lt_neg p q : (q < p)%positive -> Zneg p < Zneg q. +Proof. intros; unfold Z.lt; simpl. now rewrite <- Pos.compare_antisym. Qed. + +Lemma pos_le_pos p q : (p <= q)%positive -> Zpos p <= Zpos q. +Proof. easy. Qed. + +Lemma pos_lt_pos p q : (p < q)%positive -> Zpos p < Zpos q. +Proof. easy. Qed. + Lemma neg_xO p : Z.neg p~0 = 2 * Z.neg p. Proof. reflexivity. Qed. Lemma neg_xI p : Z.neg p~1 = 2 * Z.neg p - 1. Proof. reflexivity. Qed. +Lemma pos_xO p : Z.pos p~0 = 2 * Z.pos p. +Proof. reflexivity. Qed. + +Lemma pos_xI p : Z.pos p~1 = 2 * Z.pos p + 1. +Proof. reflexivity. Qed. + Lemma opp_neg p : - Z.neg p = Z.pos p. Proof. reflexivity. Qed. @@ -1402,6 +1438,9 @@ Proof. reflexivity. Qed. Lemma add_neg_pos p q : Z.neg p + Z.pos q = Z.pos_sub q p. Proof. reflexivity. Qed. +Lemma add_pos_pos p q : Z.pos p + Z.pos q = Z.pos (p+q). +Proof. reflexivity. Qed. + Lemma divide_pos_neg_r n p : (n|Z.pos p) <-> (n|Z.neg p). Proof. apply Z.divide_Zpos_Zneg_r. Qed. @@ -1412,6 +1451,10 @@ Lemma testbit_neg a n : 0<=n -> Z.testbit (Z.neg a) n = negb (N.testbit (Pos.pred_N a) (Z.to_N n)). Proof. apply Z.testbit_Zneg. Qed. +Lemma testbit_pos a n : 0<=n -> + Z.testbit (Z.pos a) n = N.testbit (N.pos a) (Z.to_N n). +Proof. apply Z.testbit_Zpos. Qed. + End Pos2Z. Module Z2Pos. diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v index 73dee0cf2..18915216a 100644 --- a/theories/ZArith/Zorder.v +++ b/theories/ZArith/Zorder.v @@ -339,7 +339,7 @@ Notation Zle_0_1 := Z.le_0_1 (compat "8.3"). Lemma Zle_neg_pos : forall p q:positive, Zneg p <= Zpos q. Proof. - easy. + exact Pos2Z.neg_le_pos. Qed. Lemma Zgt_pos_0 : forall p:positive, Zpos p > 0. @@ -350,12 +350,12 @@ Qed. (* weaker but useful (in [Z.pow] for instance) *) Lemma Zle_0_pos : forall p:positive, 0 <= Zpos p. Proof. - easy. + exact Pos2Z.pos_is_nonneg. Qed. Lemma Zlt_neg_0 : forall p:positive, Zneg p < 0. Proof. - easy. + exact Pos2Z.neg_is_neg. Qed. Lemma Zle_0_nat : forall n:nat, 0 <= Z.of_nat n. |