From 2280477a96e19ba5060de2d48dcc8fd7c8079d22 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 13 Nov 2015 11:31:34 +0100 Subject: Imported Upstream version 8.5~beta3+dfsg --- theories/Arith/intro.tex | 55 ------------------------- theories/Bool/intro.tex | 16 -------- theories/Classes/CMorphisms.v | 8 ++-- theories/Classes/RelationClasses.v | 5 +++ theories/Compat/Coq84.v | 77 +++++++++++++++++++++++++++++++++++ theories/Compat/Coq85.v | 9 ++++ theories/Compat/vo.itarget | 2 + theories/Lists/List.v | 20 ++++----- theories/Lists/intro.tex | 20 --------- theories/Logic/WeakFan.v | 11 ++--- theories/Logic/intro.tex | 8 ---- theories/NArith/intro.tex | 5 --- theories/Numbers/Cyclic/Int31/Int31.v | 2 +- theories/Numbers/NaryFunctions.v | 2 +- theories/PArith/intro.tex | 4 -- theories/Program/Syntax.v | 7 ---- theories/Program/Tactics.v | 2 +- theories/Reals/intro.tex | 4 -- theories/Relations/intro.tex | 23 ----------- theories/Setoids/intro.tex | 1 - theories/Sets/intro.tex | 24 ----------- theories/Sorting/intro.tex | 1 - theories/Vectors/Fin.v | 32 +++++++-------- theories/Vectors/VectorSpec.v | 45 +++++++++++--------- theories/Wellfounded/intro.tex | 4 -- theories/ZArith/intro.tex | 6 --- theories/theories.itarget | 1 + 27 files changed, 156 insertions(+), 238 deletions(-) delete mode 100755 theories/Arith/intro.tex delete mode 100644 theories/Bool/intro.tex create mode 100644 theories/Compat/Coq84.v create mode 100644 theories/Compat/Coq85.v create mode 100644 theories/Compat/vo.itarget delete mode 100755 theories/Lists/intro.tex delete mode 100755 theories/Logic/intro.tex delete mode 100644 theories/NArith/intro.tex delete mode 100644 theories/PArith/intro.tex delete mode 100644 theories/Reals/intro.tex delete mode 100755 theories/Relations/intro.tex delete mode 100644 theories/Setoids/intro.tex delete mode 100755 theories/Sets/intro.tex delete mode 100644 theories/Sorting/intro.tex delete mode 100755 theories/Wellfounded/intro.tex delete mode 100755 theories/ZArith/intro.tex (limited to 'theories') diff --git a/theories/Arith/intro.tex b/theories/Arith/intro.tex deleted file mode 100755 index 655de34c..00000000 --- a/theories/Arith/intro.tex +++ /dev/null @@ -1,55 +0,0 @@ -\section{Arith}\label{Arith} - -The {\tt Arith} library deals with various arithmetical notions and -their properties. - -\subsection*{Standard {\tt Arith} library} - -The following files are automatically loaded by {\tt Require Arith}. - -\begin{itemize} - -\item {\tt Le.v} states and proves properties of the large order {\tt le}. - -\item {\tt Lt.v} states and proves properties of the strict order {\tt -lt} (especially, the relationship with {\tt le}). - -\item {\tt Plus.v} states and proves properties on the addition. - -\item {\tt Gt.v} states and proves properties on the strict order {\tt gt}. - -\item {\tt Minus.v} defines the difference on -{\tt nat} and proves properties of it. On {\tt nat}, {\tt (minus n p)} is -{\tt O} if {\tt n} $<$ {\tt p}. - -\item {\tt Mult.v} states and proves properties on the multiplication. - -\item {\tt Between.v} defines modalities on {\tt nat} and proves properties -of them. - -\end{itemize} - -\subsection*{Additional {\tt Arith} library} - -\begin{itemize} - -\item {\tt Compare.v}, {\tt Compare\_dec.v} and {\tt Peano\_dec.v} state -and prove various decidability results on {\tt nat}. - -\item {\tt Wf\_nat.v} states and proves various induction and recursion -principles on {\tt nat}. Especially, recursion for objects measurable by -a natural number and recursion on {\tt nat * nat} are provided. - -\item {\tt Min.v} defines the minimum of two natural numbers and proves -properties of it. - -\item {\tt Eqnat.v} defines a specific equality on {\tt nat} and shows -the equivalence with Leibniz' equality. - -\item {\tt Euclid.v} proves that the euclidean -division specification is realisable. Conversely, {\tt Div.v} exhibits -two different algorithms and semi-automatically reconstruct the proof of -their correctness. These files emphasize the extraction of program vs -reconstruction of proofs paradigm. - -\end{itemize} diff --git a/theories/Bool/intro.tex b/theories/Bool/intro.tex deleted file mode 100644 index 22ee38aa..00000000 --- a/theories/Bool/intro.tex +++ /dev/null @@ -1,16 +0,0 @@ -\section{Bool}\label{Bool} - -The BOOL library includes the following files: - -\begin{itemize} - -\item {\tt Bool.v} defines standard operations on booleans and states - and proves simple facts on them. -\item {\tt IfProp.v} defines a disjunction which contains its proof - and states its properties. -\item {\tt Zerob.v} defines the test against 0 on natural numbers and - states and proves properties of it. -\item {\tt Orb.v} states and proves facts on the boolean or. -\item {\tt DecBool.v} defines a conditional from a proof of - decidability and states its properties. -\end{itemize} diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v index 048faa91..fdedbf67 100644 --- a/theories/Classes/CMorphisms.v +++ b/theories/Classes/CMorphisms.v @@ -266,11 +266,12 @@ Section GenericInstances. transitivity (y x0)... Qed. - (** The complement of a crelation conserves its proper elements. *) + Unset Strict Universe Declaration. - Program Definition complement_proper + (** The complement of a crelation conserves its proper elements. *) + Program Definition complement_proper (A : Type@{k}) (RA : crelation A) `(mR : Proper (A -> A -> Prop) (RA ==> RA ==> iff) R) : - Proper (RA ==> RA ==> iff) (complement R) := _. + Proper (RA ==> RA ==> iff) (complement@{i j Prop} R) := _. Next Obligation. Proof. @@ -280,7 +281,6 @@ Section GenericInstances. Qed. (** The [flip] too, actually the [flip] instance is a bit more general. *) - Program Definition flip_proper `(mor : Proper (A -> B -> C) (RA ==> RB ==> RC) f) : Proper (RB ==> RA ==> RC) (flip f) := _. diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 1a40e5d5..15cb02d3 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -89,6 +89,11 @@ Section Defs. Global Instance Equivalence_PER {R} `(E:Equivalence R) : PER R | 10 := { }. + (** An Equivalence is a PreOrder plus symmetry. *) + + Global Instance Equivalence_PreOrder {R} `(E:Equivalence R) : PreOrder R | 10 := + { }. + (** We can now define antisymmetry w.r.t. an equivalence relation on the carrier. *) Class Antisymmetric eqA `{equ : Equivalence eqA} (R : relation A) := diff --git a/theories/Compat/Coq84.v b/theories/Compat/Coq84.v new file mode 100644 index 00000000..b04d5168 --- /dev/null +++ b/theories/Compat/Coq84.v @@ -0,0 +1,77 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* error - | x :: _ => value x + | [] => None + | x :: _ => Some x end. Definition tl (l:list A) := @@ -69,7 +69,7 @@ Section Facts. Variable A : Type. - (** *** Genereric facts *) + (** *** Generic facts *) (** Discrimination *) Theorem nil_cons : forall (x:A) (l:list A), [] <> x :: l. @@ -393,11 +393,11 @@ Section Elts. simpl; auto. Qed. - Fixpoint nth_error (l:list A) (n:nat) {struct n} : Exc A := + Fixpoint nth_error (l:list A) (n:nat) {struct n} : option A := match n, l with - | O, x :: _ => value x + | O, x :: _ => Some x | S n, _ :: l => nth_error l n - | _, _ => error + | _, _ => None end. Definition nth_default (default:A) (l:list A) (n:nat) : A := @@ -622,9 +622,9 @@ Section Elts. Qed. - (****************************************) - (** ** Counting occurences of a element *) - (****************************************) + (******************************************) + (** ** Counting occurrences of an element *) + (******************************************) Fixpoint count_occ (l : list A) (x : A) : nat := match l with @@ -2202,7 +2202,7 @@ Section ForallPairs. Proof. induction 1. inversion 1. - simpl; destruct 1; destruct 1; repeat subst; auto. + simpl; destruct 1; destruct 1; subst; auto. right; left. apply -> Forall_forall; eauto. right; right. apply -> Forall_forall; eauto. Qed. diff --git a/theories/Lists/intro.tex b/theories/Lists/intro.tex deleted file mode 100755 index d372de8e..00000000 --- a/theories/Lists/intro.tex +++ /dev/null @@ -1,20 +0,0 @@ -\section{Lists}\label{Lists} - -This library includes the following files: - -\begin{itemize} - -\item {\tt List.v} contains definitions of (polymorphic) lists, - functions on lists such as head, tail, map, append and prove some - properties of these functions. Implicit arguments are used in this - library, so you should read the Reference Manual about implicit - arguments before using it. - -\item {\tt ListSet.v} contains definitions and properties of finite - sets, implemented as lists. - -\item {\tt Streams.v} defines the type of infinite lists (streams). It is a - co-inductive type. Basic facts are stated and proved. The streams are - also polymorphic. - -\end{itemize} diff --git a/theories/Logic/WeakFan.v b/theories/Logic/WeakFan.v index 49cc12b8..2f84ebe5 100644 --- a/theories/Logic/WeakFan.v +++ b/theories/Logic/WeakFan.v @@ -89,17 +89,14 @@ Qed. Theorem WeakFanTheorem : forall P, barred P -> inductively_barred P []. Proof. intros P Hbar. -destruct (Hbar (X P)) as (l,(Hd,HP)). +destruct Hbar with (X P) as (l,(Hd/Y_approx,HP)). assert (inductively_barred P l) by (apply (now P l), HP). clear Hbar HP. -induction l. +induction l as [|a l]. - assumption. - destruct Hd as (Hd,HX). apply (IHl Hd). clear IHl. destruct a; unfold X in HX; simpl in HX. - + apply propagate. - * apply H. - * destruct HX as (l',(Hl,(HY,Ht))); firstorder. - apply Y_approx in Hd. rewrite <- (Y_unique P l' l Hl); trivial. - + destruct HX. exists l. split; auto using Y_approx. + + apply propagate; assumption. + + exfalso; destruct (HX H). Qed. diff --git a/theories/Logic/intro.tex b/theories/Logic/intro.tex deleted file mode 100755 index 1fb294f2..00000000 --- a/theories/Logic/intro.tex +++ /dev/null @@ -1,8 +0,0 @@ -\section{Logic}\label{Logic} - -This library deals with classical logic and its properties. -The main file is {\tt Classical.v}. - -This library also provides some facts on equalities for dependent -types. See the files {\tt Eqdep.v} and {\tt JMeq.v}. - diff --git a/theories/NArith/intro.tex b/theories/NArith/intro.tex deleted file mode 100644 index bf39bc36..00000000 --- a/theories/NArith/intro.tex +++ /dev/null @@ -1,5 +0,0 @@ -\section{Binary natural numbers : NArith}\label{NArith} - -Here are defined various arithmetical notions and their properties, -similar to those of {\tt Arith}. - diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v index 4e28b5b9..f5e936cf 100644 --- a/theories/Numbers/Cyclic/Int31/Int31.v +++ b/theories/Numbers/Cyclic/Int31/Int31.v @@ -19,7 +19,7 @@ Require Export DoubleType. arithmetic. In fact it is more general than that. The only reason for this use of 31 is the underlying mecanism for hardware-efficient computations by A. Spiwack. Apart from this, a switch to, say, - 63-bit integers is now just a matter of replacing every occurences + 63-bit integers is now just a matter of replacing every occurrences of 31 by 63. This is actually made possible by the use of dependently-typed n-ary constructions for the inductive type [int31], its constructor [I31] and any pattern matching on it. diff --git a/theories/Numbers/NaryFunctions.v b/theories/Numbers/NaryFunctions.v index 6fdf0a2a..376620dd 100644 --- a/theories/Numbers/NaryFunctions.v +++ b/theories/Numbers/NaryFunctions.v @@ -15,7 +15,7 @@ Require Import List. (** * Generic dependently-typed operators about [n]-ary functions *) (** The type of [n]-ary function: [nfun A n B] is - [A -> ... -> A -> B] with [n] occurences of [A] in this type. *) + [A -> ... -> A -> B] with [n] occurrences of [A] in this type. *) Fixpoint nfun A n B := match n with diff --git a/theories/PArith/intro.tex b/theories/PArith/intro.tex deleted file mode 100644 index ffce881e..00000000 --- a/theories/PArith/intro.tex +++ /dev/null @@ -1,4 +0,0 @@ -\section{Binary positive integers : PArith}\label{PArith} - -Here are defined various arithmetical notions and their properties, -similar to those of {\tt Arith}. diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v index 67e9a20c..892305b4 100644 --- a/theories/Program/Syntax.v +++ b/theories/Program/Syntax.v @@ -32,10 +32,3 @@ Require List. Export List.ListNotations. Require Import Bvector. - -(** Treating n-ary exists *) - -Tactic Notation "exists" constr(x) := exists x. -Tactic Notation "exists" constr(x) constr(y) := exists x ; exists y. -Tactic Notation "exists" constr(x) constr(y) constr(z) := exists x ; exists y ; exists z. -Tactic Notation "exists" constr(x) constr(y) constr(z) constr(w) := exists x ; exists y ; exists z ; exists w. diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v index 0cf8d733..c1d958b9 100644 --- a/theories/Program/Tactics.v +++ b/theories/Program/Tactics.v @@ -41,7 +41,7 @@ Ltac do_nat n tac := (** Do something on the last hypothesis, or fail *) Ltac on_last_hyp tac := - match goal with [ H : _ |- _ ] => first [ tac H | fail 1 ] end. + lazymatch goal with [ H : _ |- _ ] => tac H end. (** Destructs one pair, without care regarding naming. *) diff --git a/theories/Reals/intro.tex b/theories/Reals/intro.tex deleted file mode 100644 index 43317258..00000000 --- a/theories/Reals/intro.tex +++ /dev/null @@ -1,4 +0,0 @@ -\section{Reals}\label{Reals} - -This library contains an axiomatization of real numbers. -The main file is \texttt{Reals.v}. diff --git a/theories/Relations/intro.tex b/theories/Relations/intro.tex deleted file mode 100755 index 5056f36f..00000000 --- a/theories/Relations/intro.tex +++ /dev/null @@ -1,23 +0,0 @@ -\section{Relations}\label{Relations} - -This library develops closure properties of relations. - -\begin{itemize} -\item {\tt Relation\_Definitions.v} deals with the general notions - about binary relations (orders, equivalences, ...) - -\item {\tt Relation\_Operators.v} and {\tt Rstar.v} define various - closures of relations (by symmetry, by transitivity, ...) and - lexicographic orderings. - -\item {\tt Operators\_Properties.v} states and proves facts on the - various closures of a relation. - -\item {\tt Relations.v} puts {\tt Relation\_Definitions.v}, {\tt - Relation\_Operators.v} and \\ - {\tt Operators\_Properties.v} together. - -\item {\tt Newman.v} proves Newman's lemma on noetherian and locally - confluent relations. - -\end{itemize} diff --git a/theories/Setoids/intro.tex b/theories/Setoids/intro.tex deleted file mode 100644 index 50cd025d..00000000 --- a/theories/Setoids/intro.tex +++ /dev/null @@ -1 +0,0 @@ -\section{Setoids}\label{Setoids} diff --git a/theories/Sets/intro.tex b/theories/Sets/intro.tex deleted file mode 100755 index 83c2177f..00000000 --- a/theories/Sets/intro.tex +++ /dev/null @@ -1,24 +0,0 @@ -\section{Sets}\label{Sets} - -This is a library on sets defined by their characteristic predicate. -It contains the following modules: - -\begin{itemize} -\item {\tt Ensembles.v} -\item {\tt Constructive\_sets.v}, {\tt Classical\_sets.v} -\item {\tt Relations\_1.v}, {\tt Relations\_2.v}, - {\tt Relations\_3.v}, {\tt Relations\_1\_facts.v}, \\ - {\tt Relations\_2\_facts.v}, {\tt Relations\_3\_facts.v} -\item {\tt Partial\_Order.v}, {\tt Cpo.v} -\item {\tt Powerset.v}, {\tt Powerset\_facts.v}, - {\tt Powerset\_Classical\_facts.v} -\item {\tt Finite\_sets.v}, {\tt Finite\_sets\_facts.v} -\item {\tt Image.v} -\item {\tt Infinite\_sets.v} -\item {\tt Integers.v} -\end{itemize} - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: t -%%% End: diff --git a/theories/Sorting/intro.tex b/theories/Sorting/intro.tex deleted file mode 100644 index 64ae4c88..00000000 --- a/theories/Sorting/intro.tex +++ /dev/null @@ -1 +0,0 @@ -\section{Sorting}\label{Sorting} diff --git a/theories/Vectors/Fin.v b/theories/Vectors/Fin.v index b9bf6c7f..2955184f 100644 --- a/theories/Vectors/Fin.v +++ b/theories/Vectors/Fin.v @@ -152,18 +152,18 @@ Fixpoint L {m} n (p : t m) : t (m + n) := Lemma L_sanity {m} n (p : t m) : proj1_sig (to_nat (L n p)) = proj1_sig (to_nat p). Proof. induction p. - reflexivity. - simpl; destruct (to_nat (L n p)); simpl in *; rewrite IHp. now destruct (to_nat p). +- reflexivity. +- simpl; destruct (to_nat (L n p)); simpl in *; rewrite IHp. now destruct (to_nat p). Qed. - + (** The p{^ th} element of [fin m] viewed as the p{^ th} element of [fin (n + m)] Really really ineficient !!! *) Definition L_R {m} n (p : t m) : t (n + m). Proof. induction n. - exact p. - exact ((fix LS k (p: t k) := +- exact p. +- exact ((fix LS k (p: t k) := match p with |@F1 k' => @F1 (S k') |FS p' => FS (LS _ p') @@ -178,8 +178,8 @@ Fixpoint R {m} n (p : t m) : t (n + m) := Lemma R_sanity {m} n (p : t m) : proj1_sig (to_nat (R n p)) = n + proj1_sig (to_nat p). Proof. induction n. - reflexivity. - simpl; destruct (to_nat (R n p)); simpl in *; rewrite IHn. now destruct (to_nat p). +- reflexivity. +- simpl; destruct (to_nat (R n p)); simpl in *; rewrite IHn. now destruct (to_nat p). Qed. Fixpoint depair {m n} (o : t m) (p : t n) : t (m * n) := @@ -192,9 +192,9 @@ Lemma depair_sanity {m n} (o : t m) (p : t n) : proj1_sig (to_nat (depair o p)) = n * (proj1_sig (to_nat o)) + (proj1_sig (to_nat p)). Proof. induction o ; simpl. - rewrite L_sanity. now rewrite Mult.mult_0_r. +- rewrite L_sanity. now rewrite Mult.mult_0_r. - rewrite R_sanity. rewrite IHo. +- rewrite R_sanity. rewrite IHo. rewrite Plus.plus_assoc. destruct (to_nat o); simpl; rewrite Mult.mult_succ_r. now rewrite (Plus.plus_comm n). Qed. @@ -210,10 +210,10 @@ end. Lemma eqb_nat_eq : forall m n (p : t m) (q : t n), eqb p q = true -> m = n. Proof. intros m n p; revert n; induction p; destruct q; simpl; intros; f_equal. -+ now apply EqNat.beq_nat_true. -+ easy. -+ easy. -+ eapply IHp. eassumption. +- now apply EqNat.beq_nat_true. +- easy. +- easy. +- eapply IHp. eassumption. Qed. Lemma eqb_eq : forall n (p q : t n), eqb p q = true <-> p = q. @@ -231,9 +231,9 @@ Qed. Lemma eq_dec {n} (x y : t n): {x = y} + {x <> y}. Proof. - case_eq (eqb x y); intros. - + left; now apply eqb_eq. - + right. intros Heq. apply <- eqb_eq in Heq. congruence. +case_eq (eqb x y); intros. +- left; now apply eqb_eq. +- right. intros Heq. apply <- eqb_eq in Heq. congruence. Defined. Definition cast: forall {m} (v: t m) {n}, m = n -> t n. diff --git a/theories/Vectors/VectorSpec.v b/theories/Vectors/VectorSpec.v index 7f4228dd..c5278b91 100644 --- a/theories/Vectors/VectorSpec.v +++ b/theories/Vectors/VectorSpec.v @@ -22,6 +22,11 @@ Definition cons_inj {A} {a1 a2} {n} {v1 v2 : t A n} with | eq_refl => conj eq_refl eq_refl end. +Lemma eta {A} {n} (v : t A (S n)) : v = hd v :: tl v. +Proof. +intros; apply caseS with (v:=v); intros; reflexivity. +Defined. + (** Lemmas are done for functions that use [Fin.t] but thanks to [Peano_dec.le_unique], all is true for the one that use [lt] *) @@ -29,12 +34,12 @@ Lemma eq_nth_iff A n (v1 v2: t A n): (forall p1 p2, p1 = p2 -> v1 [@ p1 ] = v2 [@ p2 ]) <-> v1 = v2. Proof. split. - revert n v1 v2; refine (@rect2 _ _ _ _ _); simpl; intros. - reflexivity. - f_equal. apply (H0 Fin.F1 Fin.F1 eq_refl). +- revert n v1 v2; refine (@rect2 _ _ _ _ _); simpl; intros. + + reflexivity. + + f_equal. apply (H0 Fin.F1 Fin.F1 eq_refl). apply H. intros p1 p2 H1; apply (H0 (Fin.FS p1) (Fin.FS p2) (f_equal (@Fin.FS n) H1)). - intros; now f_equal. +- intros; now f_equal. Qed. Lemma nth_order_last A: forall n (v: t A (S n)) (H: n < S n), @@ -47,8 +52,8 @@ Lemma shiftin_nth A a n (v: t A n) k1 k2 (eq: k1 = k2): nth (shiftin a v) (Fin.L_R 1 k1) = nth v k2. Proof. subst k2; induction k1. - generalize dependent n. apply caseS ; intros. now simpl. - generalize dependent n. refine (@caseS _ _ _) ; intros. now simpl. +- generalize dependent n. apply caseS ; intros. now simpl. +- generalize dependent n. refine (@caseS _ _ _) ; intros. now simpl. Qed. Lemma shiftin_last A a n (v: t A n): last (shiftin a v) = a. @@ -60,8 +65,8 @@ Lemma shiftrepeat_nth A: forall n k (v: t A (S n)), nth (shiftrepeat v) (Fin.L_R 1 k) = nth v k. Proof. refine (@Fin.rectS _ _ _); lazy beta; [ intros n v | intros n p H v ]. - revert n v; refine (@caseS _ _ _); simpl; intros. now destruct t. - revert p H. +- revert n v; refine (@caseS _ _ _); simpl; intros. now destruct t. +- revert p H. refine (match v as v' in t _ m return match m as m' return t A m' -> Prop with |S (S n) => fun v => forall p : Fin.t (S n), (forall v0 : t A (S n), (shiftrepeat v0) [@ Fin.L_R 1 p ] = v0 [@p]) -> @@ -84,8 +89,8 @@ Lemma nth_map {A B} (f: A -> B) {n} v (p1 p2: Fin.t n) (eq: p1 = p2): (map f v) [@ p1] = f (v [@ p2]). Proof. subst p2; induction p1. - revert n v; refine (@caseS _ _ _); now simpl. - revert n v p1 IHp1; refine (@caseS _ _ _); now simpl. +- revert n v; refine (@caseS _ _ _); now simpl. +- revert n v p1 IHp1; refine (@caseS _ _ _); now simpl. Qed. Lemma nth_map2 {A B C} (f: A -> B -> C) {n} v w (p1 p2 p3: Fin.t n): @@ -93,8 +98,8 @@ Lemma nth_map2 {A B C} (f: A -> B -> C) {n} v w (p1 p2 p3: Fin.t n): Proof. intros; subst p2; subst p3; revert n v w p1. refine (@rect2 _ _ _ _ _); simpl. - exact (Fin.case0 _). - intros n v1 v2 H a b p; revert n p v1 v2 H; refine (@Fin.caseS _ _ _); +- exact (Fin.case0 _). +- intros n v1 v2 H a b p; revert n p v1 v2 H; refine (@Fin.caseS _ _ _); now simpl. Qed. @@ -103,17 +108,17 @@ Lemma fold_left_right_assoc_eq {A B} {f: A -> B -> A} {n} (v: t B n): forall a, fold_left f a v = fold_right (fun x y => f y x) v a. Proof. assert (forall n h (v: t B n) a, fold_left f (f a h) v = f (fold_left f a v) h). - induction v0. - now simpl. - intros; simpl. rewrite<- IHv0, assoc. now f_equal. - induction v. - reflexivity. - simpl. intros; now rewrite<- (IHv). +- induction v0. + + now simpl. + + intros; simpl. rewrite<- IHv0, assoc. now f_equal. +- induction v. + + reflexivity. + + simpl. intros; now rewrite<- (IHv). Qed. Lemma to_list_of_list_opp {A} (l: list A): to_list (of_list l) = l. Proof. induction l. - reflexivity. - unfold to_list; simpl. now f_equal. +- reflexivity. +- unfold to_list; simpl. now f_equal. Qed. diff --git a/theories/Wellfounded/intro.tex b/theories/Wellfounded/intro.tex deleted file mode 100755 index 126071e2..00000000 --- a/theories/Wellfounded/intro.tex +++ /dev/null @@ -1,4 +0,0 @@ -\section{Well-founded relations}\label{Wellfounded} - -This library gives definitions and results about well-founded relations. - diff --git a/theories/ZArith/intro.tex b/theories/ZArith/intro.tex deleted file mode 100755 index 21e52c19..00000000 --- a/theories/ZArith/intro.tex +++ /dev/null @@ -1,6 +0,0 @@ -\section{Binary integers : ZArith} -The {\tt ZArith} library deals with binary integers (those used -by the {\tt Omega} decision tactic). -Here are defined various arithmetical notions and their properties, -similar to those of {\tt Arith}. - diff --git a/theories/theories.itarget b/theories/theories.itarget index 4519070e..b7de4164 100644 --- a/theories/theories.itarget +++ b/theories/theories.itarget @@ -1,6 +1,7 @@ Arith/vo.otarget Bool/vo.otarget Classes/vo.otarget +Compat/vo.otarget FSets/vo.otarget MSets/vo.otarget MMaps/vo.otarget -- cgit v1.2.3