From 6b691bbd2101fd39395c0d2135fd7c06a8915e14 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Fri, 24 Dec 2010 11:53:29 +0100 Subject: Imported Upstream version 8.3pl1 --- theories/Numbers/Natural/BigN/NMake_gen.ml | 10 +++++----- theories/Numbers/Natural/BigN/Nbasic.v | 11 ++--------- theories/Program/Equality.v | 26 +++++++++++++++++++++----- theories/Program/Tactics.v | 11 +++++++---- theories/Sorting/Mergesort.v | 5 +++-- theories/ZArith/BinInt.v | 23 +++++++++++------------ 6 files changed, 49 insertions(+), 37 deletions(-) (limited to 'theories') diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml index 8f6c59fd..052d9c92 100644 --- a/theories/Numbers/Natural/BigN/NMake_gen.ml +++ b/theories/Numbers/Natural/BigN/NMake_gen.ml @@ -8,7 +8,7 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id: NMake_gen.ml 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: NMake_gen.ml 13734 2010-12-21 18:21:56Z letouzey $ i*) (*S NMake_gen.ml : this file generates NMake.v *) @@ -1299,7 +1299,7 @@ let _ = pr " (iter _"; for i = 0 to size do pr " compare_%i" i; - pr " (fun n x y => opp_compare (comparen_%i (S n) y x))" i; + pr " (fun n x y => CompOpp (comparen_%i (S n) y x))" i; pr " (fun n => comparen_%i (S n))" i; done; pr " comparenm)."; @@ -1339,9 +1339,9 @@ let _ = pp " Let spec_opp_compare: forall c (u v: Z),"; pp " match c with Eq => u = v | Lt => u < v | Gt => u > v end ->"; - pp " match opp_compare c with Eq => v = u | Lt => v < u | Gt => v > u end."; + pp " match CompOpp c with Eq => v = u | Lt => v < u | Gt => v > u end."; pp " Proof."; - pp " intros c u v; case c; unfold opp_compare; auto with zarith."; + pp " intros c u v; case c; unfold CompOpp; auto with zarith."; pp " Qed."; pp ""; @@ -1362,7 +1362,7 @@ let _ = pp " end)"; for i = 0 to size do pp " compare_%i" i; - pp " (fun n x y => opp_compare (comparen_%i (S n) y x))" i; + pp " (fun n x y => CompOpp (comparen_%i (S n) y x))" i; pp " (fun n => comparen_%i (S n)) _ _ _" i; done; pp " comparenm _)."; diff --git a/theories/Numbers/Natural/BigN/Nbasic.v b/theories/Numbers/Natural/BigN/Nbasic.v index a531b92e..3741c95d 100644 --- a/theories/Numbers/Natural/BigN/Nbasic.v +++ b/theories/Numbers/Natural/BigN/Nbasic.v @@ -8,7 +8,7 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id: Nbasic.v 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: Nbasic.v 13734 2010-12-21 18:21:56Z letouzey $ i*) Require Import ZArith. Require Import BigNumPrelude. @@ -260,13 +260,6 @@ Section ReduceRec. End ReduceRec. -Definition opp_compare cmp := - match cmp with - | Lt => Gt - | Eq => Eq - | Gt => Lt - end. - Section CompareRec. Variable wm w : Type. @@ -447,7 +440,7 @@ End AddS. | Lt => y < x | Gt => y > x end -> - match opp_compare u with + match CompOpp u with | Eq => x = y | Lt => x < y | Gt => x > y diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index 53e12723..b9eb8f80 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Equality.v 13492 2010-10-04 21:20:01Z herbelin $ i*) +(*i $Id: Equality.v 13730 2010-12-19 13:32:01Z msozeau $ i*) (** Tactics related to (dependent) equality and proof irrelevance. *) @@ -320,19 +320,35 @@ Hint Unfold solution_left solution_right deletion simplification_heq constructor forms). Compare with the lemma 16 of the paper. We don't have a [noCycle] procedure yet. *) +Ltac block_equality id := + match type of id with + | @eq ?A ?t ?u => change (block (@eq A t u)) in id + | _ => idtac + end. + +Ltac revert_blocking_until id := + Tactics.on_last_hyp ltac:(fun id' => + match id' with + | id => idtac + | _ => block_equality id' ; revert id' ; revert_blocking_until id + end). + Ltac simplify_one_dep_elim_term c := match c with | @JMeq _ _ _ _ -> _ => refine (simplification_heq _ _ _ _ _) | ?t = ?t -> _ => intros _ || refine (simplification_K _ t _ _) - | eq (existT _ _ _) (existT _ _ _) -> _ => + | eq (existT _ ?p _) (existT _ ?q _) -> _ => refine (simplification_existT2 _ _ _ _ _ _ _) || - refine (simplification_existT1 _ _ _ _ _ _ _ _) + match goal with + | H : p = q |- _ => intro + | _ => refine (simplification_existT1 _ _ _ _ _ _ _ _) + end | ?x = ?y -> _ => (* variables case *) (let hyp := fresh in intros hyp ; - move hyp before x ; revert_until hyp ; generalize dependent x ; + move hyp before x ; revert_blocking_until hyp ; generalize dependent x ; refine (solution_left _ _ _ _)(* ; intros until 0 *)) || (let hyp := fresh in intros hyp ; - move hyp before y ; revert_until hyp ; generalize dependent y ; + move hyp before y ; revert_blocking_until hyp ; generalize dependent y ; refine (solution_right _ _ _ _)(* ; intros until 0 *)) | ?f ?x = ?g ?y -> _ => let H := fresh in progress (intros H ; injection H ; clear H) | ?t = ?u -> _ => let hyp := fresh in diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v index 333dd7a6..4a41d9c9 100644 --- a/theories/Program/Tactics.v +++ b/theories/Program/Tactics.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Tactics.v 13332 2010-07-26 22:12:43Z msozeau $ i*) +(*i $Id: Tactics.v 13693 2010-12-08 15:32:25Z msozeau $ i*) (** This module implements various tactics used to simplify the goals produced by Program, which are also generally useful. *) @@ -308,11 +308,14 @@ Ltac program_simplify := subst*; autoinjections ; try discriminates ; try (solve [ red ; intros ; destruct_conjs ; autoinjections ; discriminates ]). -Ltac program_solve_wf := +(** We only try to solve proposition goals automatically. *) + +Ltac program_solve := match goal with - |- well_founded _ => auto with * + | |- well_founded _ => auto with * + | |- ?T => match type of T with Prop => auto end end. -Ltac program_simpl := program_simplify ; auto; try program_solve_wf. +Ltac program_simpl := program_simplify ; try program_solve. Obligation Tactic := program_simpl. diff --git a/theories/Sorting/Mergesort.v b/theories/Sorting/Mergesort.v index e576db2b..04de1bfc 100644 --- a/theories/Sorting/Mergesort.v +++ b/theories/Sorting/Mergesort.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Mergesort.v 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: Mergesort.v 13678 2010-12-04 10:34:28Z herbelin $ i*) (** A modular implementation of mergesort (the complexity is O(n.log n) in the length of the list) *) @@ -61,6 +61,7 @@ Fixpoint merge l1 l2 := For instance, here is how [6;2;3;1;5] is sorted: +<< operation stack list iter_merge [] [6;2;3;1;5] = append_list_to_stack [ + [6]] [2;3;1;5] @@ -77,7 +78,7 @@ Fixpoint merge l1 l2 := = append_list_to_stack [[1;2;3;6];; + [5]] [] -> merge_stack [[1;2;3;6];;[5]] = [1;2;3;5;6] - +>> The complexity of the algorithm is n*log n, since there are 2^(p-1) mergings to do of length 2, 2^(p-2) of length 4, ..., 2^0 of length 2^p for a list of length 2^p. The algorithm does not need diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index 2a615311..357d0b7e 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: BinInt.v 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: BinInt.v 13697 2010-12-09 18:48:04Z herbelin $ i*) (***********************************************************) (** Binary Integers (Pierre Crégut, CNET, Lannion, France) *) @@ -223,7 +223,6 @@ Qed. (**********************************************************************) - (** ** Properties of opposite on binary integer numbers *) Theorem Zopp_0 : Zopp Z0 = Z0. @@ -270,21 +269,21 @@ Qed. (**********************************************************************) (** * Properties of the addition on integers *) -(** ** zero is left neutral for addition *) +(** ** Zero is left neutral for addition *) Theorem Zplus_0_l : forall n:Z, Z0 + n = n. Proof. intro x; destruct x; reflexivity. Qed. -(** *** zero is right neutral for addition *) +(** ** Zero is right neutral for addition *) Theorem Zplus_0_r : forall n:Z, n + Z0 = n. Proof. intro x; destruct x; reflexivity. Qed. -(** ** addition is commutative *) +(** ** Addition is commutative *) Theorem Zplus_comm : forall n m:Z, n + m = m + n. Proof. @@ -296,7 +295,7 @@ Proof. rewrite Pplus_comm; reflexivity. Qed. -(** ** opposite distributes over addition *) +(** ** Opposite distributes over addition *) Theorem Zopp_plus_distr : forall n m:Z, - (n + m) = - n + - m. Proof. @@ -310,7 +309,7 @@ Proof. intro; unfold Zsucc; now rewrite Zopp_plus_distr. Qed. -(** ** opposite is inverse for addition *) +(** ** Opposite is inverse for addition *) Theorem Zplus_opp_r : forall n:Z, n + - n = Z0. Proof. @@ -327,7 +326,7 @@ Qed. Hint Local Resolve Zplus_0_l Zplus_0_r. -(** ** addition is associative *) +(** ** Addition is associative *) Lemma weak_assoc : forall (p q:positive) (n:Z), Zpos p + (Zpos q + n) = Zpos p + Zpos q + n. @@ -495,7 +494,7 @@ Proof. rewrite (Zplus_comm p n); trivial with arith. Qed. -(** ** addition simplifies *) +(** ** Addition simplifies *) Theorem Zplus_reg_l : forall n m p:Z, n + m = n + p -> m = p. intros n m p H; cut (- n + (n + m) = - n + (n + p)); @@ -504,7 +503,7 @@ Theorem Zplus_reg_l : forall n m p:Z, n + m = n + p -> m = p. | rewrite H; trivial with arith ]. Qed. -(** ** addition and successor permutes *) +(** ** Addition and successor permutes *) Lemma Zplus_succ_l : forall n m:Z, Zsucc n + m = Zsucc (n + m). Proof. @@ -575,7 +574,7 @@ Proof. trivial with arith. Qed. -(** successor and predecessor are inverse functions *) +(** ** Successor and predecessor are inverse functions *) Theorem Zsucc_pred : forall n:Z, n = Zsucc (Zpred n). Proof. @@ -600,7 +599,7 @@ Proof. Qed. (*************************************************************************) -(** ** Properties of the direct definition of successor and predecessor *) +(** ** Properties of the direct definition of successor and predecessor *) Theorem Zsucc_succ' : forall n:Z, Zsucc n = Zsucc' n. Proof. -- cgit v1.2.3