From c720b6f20a4bef54c570d9a3002938828779654b Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Wed, 21 Jun 2017 13:49:15 +0200 Subject: Remove unused Makefiles in dev/tools/ They seem unused since 8f4b7f1 (2007). --- dev/README | 4 -- dev/tools/Makefile.devel | 74 -------------------------- dev/tools/Makefile.dir | 131 ---------------------------------------------- dev/tools/Makefile.subdir | 7 --- 4 files changed, 216 deletions(-) delete mode 100644 dev/tools/Makefile.devel delete mode 100644 dev/tools/Makefile.dir delete mode 100644 dev/tools/Makefile.subdir diff --git a/dev/README b/dev/README index 814f609576..b446c3e974 100644 --- a/dev/README +++ b/dev/README @@ -40,10 +40,6 @@ Documentation of ML interfaces using ocamldoc (directory ocamldoc/html) Other development tools (directory tools) ----------------------- -Makefile.dir: makefile dedicated to intensive work in a given directory -Makefile.subdir: makefile dedicated to intensive work in a given subdirectory -Makefile.devel: utilities to automatically launch coq in various states -Makefile.common: used by other Makefiles objects.el: various development utilities at emacs level anomaly-traces-parser.el: a .emacs-ready elisp snippet to parse location of Anomaly backtraces and jump to them conveniently from diff --git a/dev/tools/Makefile.devel b/dev/tools/Makefile.devel deleted file mode 100644 index ffdb1bdca9..0000000000 --- a/dev/tools/Makefile.devel +++ /dev/null @@ -1,74 +0,0 @@ -# to be linked to makefile (lowercase - takes precedence over Makefile) -# in main directory -# make devel in main directory should do this for you. - -TOPDIR=. -BASEDIR= - -SOURCEDIRS=lib kernel library pretyping parsing proofs tactics toplevel API - -default: usage noargument - -usage:: - @echo Usage: make \ - @echo Targets are: - -usage:: - @echo " setup-devel -- set the devel makefile" -setup-devel: - @ln -sfv dev/tools/Makefile.devel makefile - @(for i in $(SOURCEDIRS); do \ - (cd $(TOPDIR)/$$i; ln -sfv ../dev/tools/Makefile.dir Makefile) \ - done) - - -usage:: - @echo " clean-devel -- clear all devel files" -clean-devel: - echo rm -f makefile .depend.devel - echo rm -f $(foreach dir,$(SOURCEDIRS), $(TOPDIR)/$(dir)/Makefile) - - -usage:: - @echo " coqtop -- make until the bytecode executable, make the link" -coqtop: bin/coqtop.byte - ln -sf bin/coqtop.byte coqtop - - -usage:: - @echo " quick -- make bytecode executable and states" -quick: - $(MAKE) states BEST=byte - -include Makefile - -include $(TOPDIR)/dev/tools/Makefile.common - -# this file is better described in dev/tools/Makefile.dir -include .depend.devel - -#if dev/tools/Makefile.local exists, it is included -ifneq ($(wildcard $(TOPDIR)/dev/tools/Makefile.local),) -include $(TOPDIR)/dev/tools/Makefile.local -endif - - -usage:: - @echo " total -- runs coqtop with all theories required" -total: - ledit ./bin/coqtop.byte $(foreach th,$(THEORIESVO),-require $(notdir $(basename $(th)))) - - -usage:: - @echo " run -- makes and runs bytecode coqtop using ledit and the history file" - @echo " if you want to pass arguments to coqtop, use make run ARG=" -run: $(TOPDIR)/coqtop - ledit -h $(TOPDIR)/dev/debug_history -x $(TOPDIR)/coqtop $(ARG) $(ARGS) - - -usage:: - @echo " vars -- echos commands to set COQTOP and COQBIN variables" -vars: - @(cd $(TOPDIR); \ - echo export COQTOP=`pwd`/ ; \ - echo export COQBIN=`pwd`/bin/ ) diff --git a/dev/tools/Makefile.dir b/dev/tools/Makefile.dir deleted file mode 100644 index 1a1bb90b44..0000000000 --- a/dev/tools/Makefile.dir +++ /dev/null @@ -1,131 +0,0 @@ -# make a link to this file if you are working hard in one directory of Coq -# ln -s ../dev/tools/Makefile.dir Makefile -# if you are working in a sub/dir/ make a link to dev/tools/Makefile.subdir instead -# this Makefile provides many useful facilities to develop Coq -# it is not completely compatible with .ml4 files unfortunately - -ifndef TOPDIR -TOPDIR=.. -endif - -# this complicated thing should work for subsubdirs as well -BASEDIR=$(shell (dir=`pwd`; cd $(TOPDIR); top=`pwd`; echo $$dir | sed -e "s|$$top/||")) - -noargs: dir - -test-dir: - @echo TOPDIR=$(TOPDIR) - @echo BASEDIR=$(BASEDIR) - -include $(TOPDIR)/dev/tools/Makefile.common - -# make this directory -dir: - $(MAKE) -C $(TOPDIR) $(notdir $(BASEDIR)) - -# make all cmo's in this directory. Useful in case the main Makefile is not -# up-to-date -all: - @( ( for i in *.ml; do \ - echo -n $(BASEDIR)/`basename $$i .ml`.cmo "" ; \ - done; \ - for i in *.ml4; do \ - echo -n $(BASEDIR)/`basename $$i .ml4`.cmo "" ; \ - done ) \ - | xargs $(MAKE) -C $(TOPDIR) ) - -# lists all files that should be compiled in this directory -list: - @(for i in *.mli; do \ - ls -l `basename $$i .mli`.cmi; \ - done) - @(for i in *.ml; do \ - ls -l `basename $$i .ml`.cmo; \ - done) - @(for i in *.ml4; do \ - ls -l `basename $$i .ml4`.cmo; \ - done) - - -clean:: - rm -f *.cmi *.cmo *.cmx *.o - - -# if grammar.cmo files cannot be compiled and main .depend cannot be -# rebuilt, this is quite useful -depend: - (cd $(TOPDIR); ocamldep -I $(BASEDIR) $(BASEDIR)/*.ml $(BASEDIR)/*.mli > .depend.devel) - - -# displays the dependency graph of the current directory (vertically, -# unlike in doc/) -graph: - (ocamldep *.ml *.mli | ocamldot | dot -Tps | gv -) & - - -# the pretty entry draws a dependency graph marking red those nodes -# which do not have their .cmo files - -.INTERMEDIATE: depend.dot depend.2.dot -.PHONY: depend.ps - -depend.dot: - ocamldep *.ml *.mli | ocamldot > $@ - -depend.2.dot: depend.dot - (i=`cat $< | wc -l`; i=`expr $$i - 1`; head -n $$i $<) > $@ - (for ml in *.ml; do \ - base=`basename $$ml .ml`; \ - fst=`echo $$base | cut -c1 | tr [:lower:] [:upper:]`; \ - rest=`echo $$base | cut -c2-`; \ - name=`echo $$fst $$rest | tr -d " "`; \ - cmo=$$base.cmo; \ - if [ ! -e $$cmo ]; then \ - echo \"$$name\" [color=red]\; >> $@;\ - fi;\ - done;\ - echo } >> $@) - -depend.ps: depend.2.dot - dot -Tps $< > $@ - -clean:: - rm -f depend.ps - -pretty: depend.ps - (gv -spartan $<; rm $<) & -# gv -spartan $< & - - - -# generating file.ml.mli by tricking make to pass -i to ocamlc - -%.ml.mli: FORCE - @(cmo=`basename $@ .ml.mli`.cmo ; \ - mv -f $$cmo $$cmo.tmp ; \ - $(MAKE) -s -C $(TOPDIR) $(BASEDIR)/$$cmo CAMLDEBUG=-i > $@ ; \ - echo Generated interface file $@ ; \ - mv -f $$cmo.tmp $$cmo) - -%.annot: FORCE - @(cmo=`basename $@ .annot`.cmo ; \ - mv -f $$cmo $$cmo.tmp ; \ - $(MAKE) -s -C $(TOPDIR) $(BASEDIR)/$$cmo CAMLDEBUG=-dtypes ; \ - echo Generated annotation file $@ ; \ - mv -f $$cmo.tmp $$cmo) - -FORCE: - -clean:: - rm -f *.ml.mli - -# this is not perfect but mostly WORKS! It just calls the main makefile - -%.cmi: FORCE - $(MAKE) -C $(TOPDIR) $(BASEDIR)/$@ - -%.cmo: FORCE - $(MAKE) -C $(TOPDIR) $(BASEDIR)/$@ - -coqtop: - $(MAKE) -C $(TOPDIR) bin/coqtop.byte diff --git a/dev/tools/Makefile.subdir b/dev/tools/Makefile.subdir deleted file mode 100644 index cb914bd129..0000000000 --- a/dev/tools/Makefile.subdir +++ /dev/null @@ -1,7 +0,0 @@ -# if you work in a sub/sub-rectory of Coq -# you should make a link to that makefile -# ln -s ../../dev/tools/Makefile.subdir Makefile -# in order to have all the facilities of dev/tools/Makefile.dir - -TOPDIR=../.. -include $(TOPDIR)/dev/tools/Makefile.dir -- cgit v1.2.3 From 98af6dfee8ec5a03580cf580d7e09b3e49265322 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Wed, 21 Jun 2017 15:23:58 +0200 Subject: Fix syntax-v8.tex bad parenthesizing Introduced c1e9a27d383688e44ba34ada24fe08151cb5846e --- dev/v8-syntax/syntax-v8.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/dev/v8-syntax/syntax-v8.tex b/dev/v8-syntax/syntax-v8.tex index fa2864cec9..6b7960c92f 100644 --- a/dev/v8-syntax/syntax-v8.tex +++ b/dev/v8-syntax/syntax-v8.tex @@ -1158,7 +1158,7 @@ $$ \nlsep \TERM{Abort}~\NT{ident} \nlsep \TERM{Existential}~\NT{num}~\KWD{:=}~\NT{constr-body} \nlsep \TERM{Qed} -\nlsep \TERM{Save}~\NT{ident}} +\nlsep \TERM{Save}~\NT{ident} \nlsep \TERM{Defined}~\OPT{\NT{ident}} \nlsep \TERM{Suspend} \nlsep \TERM{Resume}~\OPT{\NT{ident}} -- cgit v1.2.3 From 6c7b8057a2baa27d3f420e199df354c22466c783 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Wed, 21 Jun 2017 15:24:27 +0200 Subject: Remove dev/TODO --- dev/TODO | 22 ---------------------- 1 file changed, 22 deletions(-) delete mode 100644 dev/TODO diff --git a/dev/TODO b/dev/TODO deleted file mode 100644 index e62ee6e537..0000000000 --- a/dev/TODO +++ /dev/null @@ -1,22 +0,0 @@ - - o options de la ligne de commande - - reporter les options de l'ancien script coqtop sur le nouveau coqtop.ml - - o arguments implicites - - les calculer une fois pour toutes à la déclaration (dans Declare) - et stocker cette information dans le in_variable, in_constant, etc. - - o Environnements compilés (type Environ.compiled_env) - - pas de timestamp mais plutôt un checksum avec Digest (mais comment ?) - - o Efficacité - - utiliser DOPL plutôt que DOPN (sauf pour Case) - - batch mode => pas de undo, ni de reset - - conversion : déplier la constante la plus récente - - un cache pour type_of_const, type_of_inductive, type_of_constructor, - lookup_mind_specif - - o Toplevel - - parsing de la ligne de commande : utiliser Arg ??? - - -- cgit v1.2.3 From 6f1e5ff85d736b80a6d3490a21a30c8d37ea18de Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Wed, 21 Jun 2017 16:48:38 +0200 Subject: Add .v extension to dev/doc/notes-on-conversion This gives syntax highlighting in Coq-aware editors. --- dev/doc/notes-on-conversion | 73 ------------------------------------------- dev/doc/notes-on-conversion.v | 73 +++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 73 insertions(+), 73 deletions(-) delete mode 100644 dev/doc/notes-on-conversion create mode 100644 dev/doc/notes-on-conversion.v diff --git a/dev/doc/notes-on-conversion b/dev/doc/notes-on-conversion deleted file mode 100644 index a81f170c63..0000000000 --- a/dev/doc/notes-on-conversion +++ /dev/null @@ -1,73 +0,0 @@ -(**********************************************************************) -(* A few examples showing the current limits of the conversion algorithm *) -(**********************************************************************) - -(*** We define (pseudo-)divergence from Ackermann function ***) - -Definition ack (n : nat) := - (fix F (n0 : nat) : nat -> nat := - match n0 with - | O => S - | S n1 => - fun m : nat => - (fix F0 (n2 : nat) : nat := - match n2 with - | O => F n1 1 - | S n3 => F n1 (F0 n3) - end) m - end) n. - -Notation OMEGA := (ack 4 4). - -Definition f (x:nat) := x. - -(* Evaluation in tactics can somehow be controlled *) -Lemma l1 : OMEGA = OMEGA. -reflexivity. (* succeed: identity *) -Qed. (* succeed: identity *) - -Lemma l2 : OMEGA = f OMEGA. -reflexivity. (* fail: conversion wants to convert OMEGA with f OMEGA *) -Abort. (* but it reduces the right side first! *) - -Lemma l3 : f OMEGA = OMEGA. -reflexivity. (* succeed: reduce left side first *) -Qed. (* succeed: expected concl (the one with f) is on the left *) - -Lemma l4 : OMEGA = OMEGA. -assert (f OMEGA = OMEGA) by reflexivity. (* succeed *) -unfold f in H. (* succeed: no type-checking *) -exact H. (* succeed: identity *) -Qed. (* fail: "f" is on the left *) - -(* This example would fail whatever the preferred side is *) -Lemma l5 : OMEGA = f OMEGA. -unfold f. -assert (f OMEGA = OMEGA) by reflexivity. -unfold f in H. -exact H. -Qed. (* needs to convert (f OMEGA = OMEGA) and (OMEGA = f OMEGA) *) - -(**********************************************************************) -(* Analysis of the inefficiency in Nijmegen/LinAlg/LinAlg/subspace_dim.v *) -(* (proof of span_ind_uninject_prop *) - -In the proof, a problem of the form (Equal S t1 t2) -is "simpl"ified, then "red"uced to (Equal S' t1 t1) -where the new t1's are surrounded by invisible coercions. -A reflexivity steps conclude the proof. - -The trick is that Equal projects the equality in the setoid S, and -that (Equal S) itself reduces to some (fun x y => Equal S' (f x) (g y)). - -At the Qed time, the problem to solve is (Equal S t1 t2) = (Equal S' t1 t1) -and the algorithm is to first compare S and S', and t1 and t2. -Unfortunately it does not work, and since t1 and t2 involve concrete -instances of algebraic structures, it takes a lot of time to realize that -it is not convertible. - -The only hope to improve this problem is to observe that S' hides -(behind two indirections) a Setoid constructor. This could be the -argument to solve the problem. - - diff --git a/dev/doc/notes-on-conversion.v b/dev/doc/notes-on-conversion.v new file mode 100644 index 0000000000..a81f170c63 --- /dev/null +++ b/dev/doc/notes-on-conversion.v @@ -0,0 +1,73 @@ +(**********************************************************************) +(* A few examples showing the current limits of the conversion algorithm *) +(**********************************************************************) + +(*** We define (pseudo-)divergence from Ackermann function ***) + +Definition ack (n : nat) := + (fix F (n0 : nat) : nat -> nat := + match n0 with + | O => S + | S n1 => + fun m : nat => + (fix F0 (n2 : nat) : nat := + match n2 with + | O => F n1 1 + | S n3 => F n1 (F0 n3) + end) m + end) n. + +Notation OMEGA := (ack 4 4). + +Definition f (x:nat) := x. + +(* Evaluation in tactics can somehow be controlled *) +Lemma l1 : OMEGA = OMEGA. +reflexivity. (* succeed: identity *) +Qed. (* succeed: identity *) + +Lemma l2 : OMEGA = f OMEGA. +reflexivity. (* fail: conversion wants to convert OMEGA with f OMEGA *) +Abort. (* but it reduces the right side first! *) + +Lemma l3 : f OMEGA = OMEGA. +reflexivity. (* succeed: reduce left side first *) +Qed. (* succeed: expected concl (the one with f) is on the left *) + +Lemma l4 : OMEGA = OMEGA. +assert (f OMEGA = OMEGA) by reflexivity. (* succeed *) +unfold f in H. (* succeed: no type-checking *) +exact H. (* succeed: identity *) +Qed. (* fail: "f" is on the left *) + +(* This example would fail whatever the preferred side is *) +Lemma l5 : OMEGA = f OMEGA. +unfold f. +assert (f OMEGA = OMEGA) by reflexivity. +unfold f in H. +exact H. +Qed. (* needs to convert (f OMEGA = OMEGA) and (OMEGA = f OMEGA) *) + +(**********************************************************************) +(* Analysis of the inefficiency in Nijmegen/LinAlg/LinAlg/subspace_dim.v *) +(* (proof of span_ind_uninject_prop *) + +In the proof, a problem of the form (Equal S t1 t2) +is "simpl"ified, then "red"uced to (Equal S' t1 t1) +where the new t1's are surrounded by invisible coercions. +A reflexivity steps conclude the proof. + +The trick is that Equal projects the equality in the setoid S, and +that (Equal S) itself reduces to some (fun x y => Equal S' (f x) (g y)). + +At the Qed time, the problem to solve is (Equal S t1 t2) = (Equal S' t1 t1) +and the algorithm is to first compare S and S', and t1 and t2. +Unfortunately it does not work, and since t1 and t2 involve concrete +instances of algebraic structures, it takes a lot of time to realize that +it is not convertible. + +The only hope to improve this problem is to observe that S' hides +(behind two indirections) a Setoid constructor. This could be the +argument to solve the problem. + + -- cgit v1.2.3 From 93567ef987f22a19ff538ac2617c27f6832c3ce3 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 22 Jun 2017 13:18:08 +0200 Subject: Remove obsolete files db_printers just isn't used. api.txt is superseded by the API OCaml interface. --- dev/db_printers.ml | 16 ---------------- dev/doc/api.txt | 10 ---------- 2 files changed, 26 deletions(-) delete mode 100644 dev/db_printers.ml delete mode 100644 dev/doc/api.txt diff --git a/dev/db_printers.ml b/dev/db_printers.ml deleted file mode 100644 index f4b4a425e2..0000000000 --- a/dev/db_printers.ml +++ /dev/null @@ -1,16 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* y) -> 2 = 3). @@ -69,13 +71,13 @@ Check (Prop::Set::nil). Require Import Bvector. -Print vector. +Print Vector.t. -Check (Vnil nat). +Check (Vector.nil nat). -Check (fun (A:Type)(a:A)=> Vcons _ a _ (Vnil _)). +Check (fun (A:Type)(a:A)=> Vector.cons _ a _ (Vector.nil _)). -Check (Vcons _ 5 _ (Vcons _ 3 _ (Vnil _))). +Check (Vector.cons _ 5 _ (Vector.cons _ 3 _ (Vector.nil _))). Lemma eq_3_3 : 2 + 1 = 3. Proof. @@ -146,6 +148,7 @@ Proof. intros; absurd (p < p); eauto with arith. Qed. +Require Extraction. Extraction max. @@ -300,8 +303,8 @@ Section Le_case_analysis. (HS : forall m, n <= m -> Q (S m)). Check ( match H in (_ <= q) return (Q q) with - | le_n => H0 - | le_S m Hm => HS m Hm + | le_n _ => H0 + | le_S _ m Hm => HS m Hm end ). @@ -317,16 +320,16 @@ Proof. Qed. Definition Vtail_total - (A : Type) (n : nat) (v : vector A n) : vector A (pred n):= -match v in (vector _ n0) return (vector A (pred n0)) with -| Vnil => Vnil A -| Vcons _ n0 v0 => v0 + (A : Type) (n : nat) (v : Vector.t A n) : Vector.t A (pred n):= +match v in (Vector.t _ n0) return (Vector.t A (pred n0)) with +| Vector.nil _ => Vector.nil A +| Vector.cons _ _ n0 v0 => v0 end. -Definition Vtail' (A:Type)(n:nat)(v:vector A n) : vector A (pred n). +Definition Vtail' (A:Type)(n:nat)(v:Vector.t A n) : Vector.t A (pred n). intros A n v; case v. simpl. - exact (Vnil A). + exact (Vector.nil A). simpl. auto. Defined. @@ -498,10 +501,8 @@ Inductive typ : Type := Definition typ_inject: typ. split. -exact typ. +Fail exact typ. (* -Defined. - Error: Universe Inconsistency. *) Abort. @@ -920,7 +921,6 @@ Defined. Print minus_decrease. - Definition div_aux (x y:nat)(H: Acc lt x):nat. fix 3. intros. @@ -969,40 +969,40 @@ let rec div_aux x y = | Right -> div_aux (minus x y) y) *) -Lemma vector0_is_vnil : forall (A:Type)(v:vector A 0), v = Vnil A. +Lemma vector0_is_vnil : forall (A:Type)(v:Vector.t A 0), v = Vector.nil A. Proof. intros A v;inversion v. Abort. (* - Lemma vector0_is_vnil_aux : forall (A:Type)(n:nat)(v:vector A n), - n= 0 -> v = Vnil A. + Lemma vector0_is_vnil_aux : forall (A:Type)(n:nat)(v:Vector.t A n), + n= 0 -> v = Vector.nil A. Toplevel input, characters 40281-40287 -> Lemma vector0_is_vnil_aux : forall (A:Set)(n:nat)(v:vector A n), n= 0 -> v = Vnil A. +> Lemma vector0_is_vnil_aux : forall (A:Set)(n:nat)(v:Vector.t A n), n= 0 -> v = Vector.nil A. > ^^^^^^ Error: In environment A : Set n : nat -v : vector A n +v : Vector.t A n e : n = 0 -The term "Vnil A" has type "vector A 0" while it is expected to have type - "vector A n" +The term "Vector.nil A" has type "Vector.t A 0" while it is expected to have type + "Vector.t A n" *) Require Import JMeq. (* On devrait changer Set en Type ? *) -Lemma vector0_is_vnil_aux : forall (A:Type)(n:nat)(v:vector A n), - n= 0 -> JMeq v (Vnil A). +Lemma vector0_is_vnil_aux : forall (A:Type)(n:nat)(v:Vector.t A n), + n= 0 -> JMeq v (Vector.nil A). Proof. destruct v. auto. intro; discriminate. Qed. -Lemma vector0_is_vnil : forall (A:Type)(v:vector A 0), v = Vnil A. +Lemma vector0_is_vnil : forall (A:Type)(v:Vector.t A 0), v = Vector.nil A. Proof. intros a v;apply JMeq_eq. apply vector0_is_vnil_aux. @@ -1010,56 +1010,56 @@ Proof. Qed. -Implicit Arguments Vcons [A n]. -Implicit Arguments Vnil [A]. -Implicit Arguments Vhead [A n]. -Implicit Arguments Vtail [A n]. +Implicit Arguments Vector.cons [A n]. +Implicit Arguments Vector.nil [A]. +Implicit Arguments Vector.hd [A n]. +Implicit Arguments Vector.tl [A n]. -Definition Vid : forall (A : Type)(n:nat), vector A n -> vector A n. +Definition Vid : forall (A : Type)(n:nat), Vector.t A n -> Vector.t A n. Proof. destruct n; intro v. - exact Vnil. - exact (Vcons (Vhead v) (Vtail v)). + exact Vector.nil. + exact (Vector.cons (Vector.hd v) (Vector.tl v)). Defined. -Eval simpl in (fun (A:Type)(v:vector A 0) => (Vid _ _ v)). +Eval simpl in (fun (A:Type)(v:Vector.t A 0) => (Vid _ _ v)). -Eval simpl in (fun (A:Type)(v:vector A 0) => v). +Eval simpl in (fun (A:Type)(v:Vector.t A 0) => v). -Lemma Vid_eq : forall (n:nat) (A:Type)(v:vector A n), v=(Vid _ n v). +Lemma Vid_eq : forall (n:nat) (A:Type)(v:Vector.t A n), v=(Vid _ n v). Proof. destruct v. reflexivity. reflexivity. Defined. -Theorem zero_nil : forall A (v:vector A 0), v = Vnil. +Theorem zero_nil : forall A (v:Vector.t A 0), v = Vector.nil. Proof. intros. - change (Vnil (A:=A)) with (Vid _ 0 v). + change (Vector.nil (A:=A)) with (Vid _ 0 v). apply Vid_eq. Defined. Theorem decomp : - forall (A : Type) (n : nat) (v : vector A (S n)), - v = Vcons (Vhead v) (Vtail v). + forall (A : Type) (n : nat) (v : Vector.t A (S n)), + v = Vector.cons (Vector.hd v) (Vector.tl v). Proof. intros. - change (Vcons (Vhead v) (Vtail v)) with (Vid _ (S n) v). + change (Vector.cons (Vector.hd v) (Vector.tl v)) with (Vid _ (S n) v). apply Vid_eq. Defined. Definition vector_double_rect : - forall (A:Type) (P: forall (n:nat),(vector A n)->(vector A n) -> Type), - P 0 Vnil Vnil -> - (forall n (v1 v2 : vector A n) a b, P n v1 v2 -> - P (S n) (Vcons a v1) (Vcons b v2)) -> - forall n (v1 v2 : vector A n), P n v1 v2. + forall (A:Type) (P: forall (n:nat),(Vector.t A n)->(Vector.t A n) -> Type), + P 0 Vector.nil Vector.nil -> + (forall n (v1 v2 : Vector.t A n) a b, P n v1 v2 -> + P (S n) (Vector.cons a v1) (Vector.cons b v2)) -> + forall n (v1 v2 : Vector.t A n), P n v1 v2. induction n. intros; rewrite (zero_nil _ v1); rewrite (zero_nil _ v2). auto. @@ -1069,24 +1069,23 @@ Defined. Require Import Bool. -Definition bitwise_or n v1 v2 : vector bool n := - vector_double_rect bool (fun n v1 v2 => vector bool n) - Vnil - (fun n v1 v2 a b r => Vcons (orb a b) r) n v1 v2. - +Definition bitwise_or n v1 v2 : Vector.t bool n := + vector_double_rect bool (fun n v1 v2 => Vector.t bool n) + Vector.nil + (fun n v1 v2 a b r => Vector.cons (orb a b) r) n v1 v2. -Fixpoint vector_nth (A:Type)(n:nat)(p:nat)(v:vector A p){struct v} +Fixpoint vector_nth (A:Type)(n:nat)(p:nat)(v:Vector.t A p){struct v} : option A := match n,v with - _ , Vnil => None - | 0 , Vcons b _ _ => Some b - | S n', Vcons _ p' v' => vector_nth A n' p' v' + _ , Vector.nil => None + | 0 , Vector.cons b _ => Some b + | S n', @Vector.cons _ _ p' v' => vector_nth A n' p' v' end. Implicit Arguments vector_nth [A p]. -Lemma nth_bitwise : forall (n:nat) (v1 v2: vector bool n) i a b, +Lemma nth_bitwise : forall (n:nat) (v1 v2: Vector.t bool n) i a b, vector_nth i v1 = Some a -> vector_nth i v2 = Some b -> vector_nth i (bitwise_or _ v1 v2) = Some (orb a b). -- cgit v1.2.3