aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CREDITS3
-rw-r--r--doc/changelog/10-standard-library/09379-splitAt.rst5
-rw-r--r--stm/stm.ml13
-rw-r--r--theories/Init/Datatypes.v13
-rw-r--r--theories/Vectors/VectorDef.v10
-rw-r--r--theories/Vectors/VectorSpec.v34
-rw-r--r--toplevel/ccompile.ml6
-rw-r--r--toplevel/coqargs.ml19
-rw-r--r--toplevel/coqcargs.ml8
-rw-r--r--toplevel/vernac.ml2
10 files changed, 99 insertions, 14 deletions
diff --git a/CREDITS b/CREDITS
index 989e449cc5..888824aa31 100644
--- a/CREDITS
+++ b/CREDITS
@@ -112,6 +112,7 @@ of the Coq Proof assistant during the indicated time:
Hugo Herbelin (INRIA, 1996-now)
Sébastien Hinderer (INRIA, 2014)
Gérard Huet (INRIA, 1985-1997)
+ Konstantinos Kallas (U. Penn, 2019)
Matej Košík (INRIA, 2015-2017)
Leonidas Lampropoulos (University of Pennsylvania, 2018)
Pierre Letouzey (LRI, 2000-2004, PPS, 2005-2008,
@@ -119,7 +120,7 @@ of the Coq Proof assistant during the indicated time:
Yao Li (ORCID: https://orcid.org/0000-0001-8720-883X,
University of Pennsylvania, 2018)
Yishuai Li (ORCID: https://orcid.org/0000-0002-5728-5903
- U. Penn, 2018)
+ U. Penn, 2018-2019)
Patrick Loiseleur (Paris Sud, 1997-1999)
Evgeny Makarov (INRIA, 2007)
Gregory Malecha (Harvard University 2013-2015,
diff --git a/doc/changelog/10-standard-library/09379-splitAt.rst b/doc/changelog/10-standard-library/09379-splitAt.rst
new file mode 100644
index 0000000000..7ffe8e27f7
--- /dev/null
+++ b/doc/changelog/10-standard-library/09379-splitAt.rst
@@ -0,0 +1,5 @@
+- Added ``splitat`` function and lemmas about ``splitat`` and ``uncons``
+ (`#9379 <https://github.com/coq/coq/pull/9379>`_,
+ by Yishuai Li, with help of Konstantinos Kallas,
+ follow-up of `#8365 <https://github.com/coq/coq/pull/8365>`_,
+ which added ``uncons`` in 8.10+beta1).
diff --git a/stm/stm.ml b/stm/stm.ml
index 7f0632bd7c..1042061021 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2617,13 +2617,10 @@ let dirpath_of_file f =
let new_doc { doc_type ; iload_path; require_libs; stm_options } =
- let load_objs libs =
- let rq_file (dir, from, exp) =
- let mp = Libnames.qualid_of_string dir in
- let mfrom = Option.map Libnames.qualid_of_string from in
- Flags.silently (Vernacentries.vernac_require mfrom exp) [mp] in
- List.(iter rq_file (rev libs))
- in
+ let require_file (dir, from, exp) =
+ let mp = Libnames.qualid_of_string dir in
+ let mfrom = Option.map Libnames.qualid_of_string from in
+ Flags.silently (Vernacentries.vernac_require mfrom exp) [mp] in
(* Set the options from the new documents *)
AsyncOpts.cur_opt := stm_options;
@@ -2662,7 +2659,7 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } =
end;
(* Import initial libraries. *)
- load_objs require_libs;
+ List.iter require_file require_libs;
(* We record the state at this point! *)
State.define ~doc ~cache:true ~redefine:true (fun () -> ()) Stateid.initial;
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 3e0bf1d8ae..6984a7c2b6 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -243,6 +243,19 @@ Proof.
rewrite Hfst; rewrite Hsnd; reflexivity.
Qed.
+Lemma pair_equal_spec :
+ forall (A B : Type) (a1 a2 : A) (b1 b2 : B),
+ (a1, b1) = (a2, b2) <-> a1 = a2 /\ b1 = b2.
+Proof with auto.
+ split; intros.
+ - split.
+ + replace a1 with (fst (a1, b1)); replace a2 with (fst (a2, b2))...
+ rewrite H...
+ + replace b1 with (snd (a1, b1)); replace b2 with (snd (a2, b2))...
+ rewrite H...
+ - destruct H; subst...
+Qed.
+
Definition prod_uncurry (A B C:Type) (f:A * B -> C)
(x:A) (y:B) : C := f (x,y).
diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v
index 20a8581d46..cba4780bd4 100644
--- a/theories/Vectors/VectorDef.v
+++ b/theories/Vectors/VectorDef.v
@@ -189,6 +189,16 @@ Fixpoint append {A}{n}{p} (v:t A n) (w:t A p):t A (n+p) :=
Infix "++" := append.
+(** Split a vector into two parts *)
+Fixpoint splitat {A} (l : nat) {r : nat} :
+ t A (l + r) -> t A l * t A r :=
+ match l with
+ | 0 => fun v => ([], v)
+ | S l' => fun v =>
+ let (v1, v2) := splitat l' (tl v) in
+ (hd v::v1, v2)
+ end.
+
(** Two definitions of the tail recursive function that appends two lists but
reverses the first one *)
diff --git a/theories/Vectors/VectorSpec.v b/theories/Vectors/VectorSpec.v
index 55a55c0b2f..b27566458e 100644
--- a/theories/Vectors/VectorSpec.v
+++ b/theories/Vectors/VectorSpec.v
@@ -153,3 +153,37 @@ Proof.
- destruct v. inversion le. simpl. apply f_equal. apply IHp.
Qed.
+Lemma uncons_cons {A} : forall {n : nat} (a : A) (v : t A n),
+ uncons (a::v) = (a,v).
+Proof. reflexivity. Qed.
+
+Lemma append_comm_cons {A} : forall {n m : nat} (v : t A n) (w : t A m) (a : A),
+ a :: (v ++ w) = (a :: v) ++ w.
+Proof. reflexivity. Qed.
+
+Lemma splitat_append {A} : forall {n m : nat} (v : t A n) (w : t A m),
+ splitat n (v ++ w) = (v, w).
+Proof with simpl; auto.
+ intros n m v.
+ generalize dependent m.
+ induction v; intros...
+ rewrite IHv...
+Qed.
+
+Lemma append_splitat {A} : forall {n m : nat} (v : t A n) (w : t A m) (vw : t A (n+m)),
+ splitat n vw = (v, w) ->
+ vw = v ++ w.
+Proof with auto.
+ intros n m v.
+ generalize dependent m.
+ induction v; intros; inversion H...
+ destruct (splitat n (tl vw)) as [v' w'] eqn:Heq.
+ apply pair_equal_spec in H1.
+ destruct H1; subst.
+ rewrite <- append_comm_cons.
+ rewrite (eta vw).
+ apply cons_inj in H0.
+ destruct H0; subst.
+ f_equal...
+ apply IHv...
+Qed.
diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml
index fe5361c156..3600658e23 100644
--- a/toplevel/ccompile.ml
+++ b/toplevel/ccompile.ml
@@ -39,7 +39,7 @@ let load_vernacular opts ~state =
if !Flags.beautify
then Flags.with_option Flags.beautify_file load_vernac f_in
else load_vernac s
- ) state (List.rev opts.pre.load_vernacular_list)
+ ) state opts.pre.load_vernacular_list
let load_init_vernaculars opts ~state =
let state = load_init_file opts ~state in
@@ -193,7 +193,7 @@ let compile_file opts copts (f_in, echo) =
compile opts copts ~echo ~f_in ~f_out
let compile_files opts copts =
- let compile_list = List.rev copts.compile_list in
+ let compile_list = copts.compile_list in
List.iter (compile_file opts copts) compile_list
(******************************************************************************)
@@ -205,7 +205,7 @@ let check_vio_tasks copts =
let f_in = ensure ".vio" f f in
ensure_exists f_in;
Vio_checking.check_vio (n,f_in) && acc)
- true (List.rev copts.vio_tasks) in
+ true copts.vio_tasks in
if not rc then fatal_error Pp.(str "VIO Task Check failed")
(* vio files *)
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 0490c35970..113b1fb5d7 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -547,6 +547,23 @@ let parse_args ~help ~init arglist : t * string list =
parse init
with any -> fatal_error any
+(* We need to reverse a few lists *)
+let parse_args ~help ~init args =
+ let opts, extra = parse_args ~help ~init args in
+ let opts =
+ { opts with
+ pre = { opts.pre with
+ ml_includes = List.rev opts.pre.ml_includes
+ ; vo_includes = List.rev opts.pre.vo_includes
+ ; vo_requires = List.rev opts.pre.vo_requires
+ ; load_vernacular_list = List.rev opts.pre.load_vernacular_list
+ }
+ ; config = { opts.config with
+ set_options = List.rev opts.config.set_options
+ } ;
+ } in
+ opts, extra
+
(******************************************************************************)
(* Startup LoadPath and Modules *)
(******************************************************************************)
@@ -557,7 +574,7 @@ let require_libs opts =
if opts.pre.load_init then prelude_data :: opts.pre.vo_requires else opts.pre.vo_requires
let cmdline_load_path opts =
- List.rev opts.pre.vo_includes @ List.(rev opts.pre.ml_includes)
+ opts.pre.ml_includes @ opts.pre.vo_includes
let build_load_path opts =
Coqinit.libs_init_load_path ~load_init:opts.pre.load_init @
diff --git a/toplevel/coqcargs.ml b/toplevel/coqcargs.ml
index 0b5481fe72..c4e3571281 100644
--- a/toplevel/coqcargs.ml
+++ b/toplevel/coqcargs.ml
@@ -210,3 +210,11 @@ let parse arglist : t =
check_compilation_output_name_consistency args;
args
with any -> fatal_error any
+
+let parse args =
+ let opts = parse args in
+ { opts with
+ compile_list = List.rev opts.compile_list
+ ; vio_tasks = List.rev opts.vio_tasks
+ ; vio_files = List.rev opts.vio_files
+ }
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index e9d8263b85..bca6b48499 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -169,6 +169,6 @@ let beautify_pass ~doc ~comments ~ids ~filename =
let load_vernac ~echo ~check ~interactive ~state filename =
let ostate, ids, comments = load_vernac_core ~echo ~check ~interactive ~state filename in
(* Pass for beautify *)
- if !Flags.beautify then beautify_pass ~doc:ostate.State.doc ~comments ~ids:List.(rev ids) ~filename;
+ if !Flags.beautify then beautify_pass ~doc:ostate.State.doc ~comments ~ids:(List.rev ids) ~filename;
(* End pass *)
ostate
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 19:29:05 +0000