summaryrefslogtreecommitdiff
path: root/theories/Init
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Init')
-rw-r--r--[-rwxr-xr-x]theories/Init/Datatypes.v22
-rw-r--r--[-rwxr-xr-x]theories/Init/Logic.v101
-rw-r--r--[-rwxr-xr-x]theories/Init/Logic_Type.v62
-rw-r--r--theories/Init/Notations.v11
-rw-r--r--[-rwxr-xr-x]theories/Init/Peano.v56
-rw-r--r--[-rwxr-xr-x]theories/Init/Prelude.v5
-rw-r--r--[-rwxr-xr-x]theories/Init/Specif.v54
-rw-r--r--theories/Init/Tactics.v72
-rw-r--r--[-rwxr-xr-x]theories/Init/Wf.v99
9 files changed, 297 insertions, 185 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 6aeabe13..f71f58c6 100755..100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -6,19 +6,19 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Datatypes.v,v 1.26.2.1 2004/07/16 19:31:03 herbelin Exp $ i*)
+(*i $Id: Datatypes.v 8642 2006-03-17 10:09:02Z notin $ i*)
+
+Set Implicit Arguments.
Require Import Notations.
Require Import Logic.
-Set Implicit Arguments.
-
(** [unit] is a singleton datatype with sole inhabitant [tt] *)
Inductive unit : Set :=
tt : unit.
-(** [bool] is the datatype of the booleans values [true] and [false] *)
+(** [bool] is the datatype of the boolean values [true] and [false] *)
Inductive bool : Set :=
| true : bool
@@ -27,7 +27,9 @@ Inductive bool : Set :=
Add Printing If bool.
(** [nat] is the datatype of natural numbers built from [O] and successor [S];
- note that zero is the letter O, not the numeral 0 *)
+ note that the constructor name is the letter O.
+ Numbers in [nat] can be denoted using a decimal notation;
+ e.g. [3%nat] abbreviates [S (S (S O))] *)
Inductive nat : Set :=
| O : nat
@@ -53,7 +55,7 @@ Implicit Arguments identity_ind [A].
Implicit Arguments identity_rec [A].
Implicit Arguments identity_rect [A].
-(** [option A] is the extension of A with a dummy element None *)
+(** [option A] is the extension of [A] with an extra element [None] *)
Inductive option (A:Set) : Set :=
| Some : A -> option A
@@ -61,7 +63,13 @@ Inductive option (A:Set) : Set :=
Implicit Arguments None [A].
-(** [sum A B], equivalently [A + B], is the disjoint sum of [A] and [B] *)
+Definition option_map (A B:Set) (f:A->B) o :=
+ match o with
+ | Some a => Some (f a)
+ | None => None
+ end.
+
+(** [sum A B], written [A + B], is the disjoint sum of [A] and [B] *)
(* Syntax defined in Specif.v *)
Inductive sum (A B:Set) : Set :=
| inl : A -> sum A B
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index bae8d4a1..cbf8d7a7 100755..100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -6,13 +6,13 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Logic.v,v 1.29.2.1 2004/07/16 19:31:03 herbelin Exp $ i*)
+(*i $Id: Logic.v 8642 2006-03-17 10:09:02Z notin $ i*)
Set Implicit Arguments.
Require Import Notations.
-(** * Propositional connectives *)
+(** *** Propositional connectives *)
(** [True] is the always true proposition *)
Inductive True : Prop :=
@@ -28,13 +28,6 @@ Notation "~ x" := (not x) : type_scope.
Hint Unfold not: core.
-Inductive and (A B:Prop) : Prop :=
- conj : A -> B -> A /\ B
- where "A /\ B" := (and A B) : type_scope.
-
-
-Section Conjunction.
-
(** [and A B], written [A /\ B], is the conjunction of [A] and [B]
[conj p q] is a proof of [A /\ B] as soon as
@@ -42,6 +35,13 @@ Section Conjunction.
[proj1] and [proj2] are first and second projections of a conjunction *)
+Inductive and (A B:Prop) : Prop :=
+ conj : A -> B -> A /\ B
+
+where "A /\ B" := (and A B) : type_scope.
+
+Section Conjunction.
+
Variables A B : Prop.
Theorem proj1 : A /\ B -> A.
@@ -61,7 +61,8 @@ End Conjunction.
Inductive or (A B:Prop) : Prop :=
| or_introl : A -> A \/ B
| or_intror : B -> A \/ B
- where "A \/ B" := (or A B) : type_scope.
+
+where "A \/ B" := (or A B) : type_scope.
(** [iff A B], written [A <-> B], expresses the equivalence of [A] and [B] *)
@@ -94,20 +95,28 @@ End Equivalence.
Definition IF_then_else (P Q R:Prop) := P /\ Q \/ ~ P /\ R.
Notation "'IF' c1 'then' c2 'else' c3" := (IF_then_else c1 c2 c3)
- (at level 200) : type_scope.
-
-(** * First-order quantifiers
- - [ex A P], or simply [exists x, P x], expresses the existence of an
- [x] of type [A] which satisfies the predicate [P] ([A] is of type
- [Set]). This is existential quantification.
- - [ex2 A P Q], or simply [exists2 x, P x & Q x], expresses the
- existence of an [x] of type [A] which satisfies both the predicates
- [P] and [Q].
- - Universal quantification (especially first-order one) is normally
- written [forall x:A, P x]. For duality with existential quantification,
- the construction [all P] is provided too.
+ (at level 200, right associativity) : type_scope.
+
+(** *** First-order quantifiers *)
+
+(** [ex P], or simply [exists x, P x], or also [exists x:A, P x],
+ expresses the existence of an [x] of some type [A] in [Set] which
+ satisfies the predicate [P]. This is existential quantification.
+
+ [ex2 P Q], or simply [exists2 x, P x & Q x], or also
+ [exists2 x:A, P x & Q x], expresses the existence of an [x] of
+ type [A] which satisfies both predicates [P] and [Q].
+
+ Universal quantification is primitively written [forall x:A, Q]. By
+ symmetry with existential quantification, the construction [all P]
+ is provided too.
*)
+(* Remark: [exists x, Q] denotes [ex (fun x => Q)] so that [exists x,
+ P x] is in fact equivalent to [ex (fun x => P x)] which may be not
+ convertible to [ex P] if [P] is not itself an abstraction *)
+
+
Inductive ex (A:Type) (P:A -> Prop) : Prop :=
ex_intro : forall x:A, P x -> ex (A:=A) P.
@@ -119,19 +128,19 @@ Definition all (A:Type) (P:A -> Prop) := forall x:A, P x.
(* Rule order is important to give printing priority to fully typed exists *)
Notation "'exists' x , p" := (ex (fun x => p))
- (at level 200, x ident) : type_scope.
+ (at level 200, x ident, right associativity) : type_scope.
Notation "'exists' x : t , p" := (ex (fun x:t => p))
- (at level 200, x ident, format "'exists' '/ ' x : t , '/ ' p")
+ (at level 200, x ident, right associativity,
+ format "'[' 'exists' '/ ' x : t , '/ ' p ']'")
: type_scope.
Notation "'exists2' x , p & q" := (ex2 (fun x => p) (fun x => q))
- (at level 200, x ident, p at level 200) : type_scope.
+ (at level 200, x ident, p at level 200, right associativity) : type_scope.
Notation "'exists2' x : t , p & q" := (ex2 (fun x:t => p) (fun x:t => q))
- (at level 200, x ident, t at level 200, p at level 200,
- format "'exists2' '/ ' x : t , '/ ' '[' p & '/' q ']'")
+ (at level 200, x ident, t at level 200, p at level 200, right associativity,
+ format "'[' 'exists2' '/ ' x : t , '/ ' '[' p & '/' q ']' ']'")
: type_scope.
-
(** Derived rules for universal quantification *)
Section universal_quantification.
@@ -151,18 +160,21 @@ Section universal_quantification.
End universal_quantification.
-(** * Equality *)
+(** *** Equality *)
-(** [eq x y], or simply [x=y], expresses the (Leibniz') equality
- of [x] and [y]. Both [x] and [y] must belong to the same type [A].
+(** [eq x y], or simply [x=y] expresses the equality of [x] and
+ [y]. Both [x] and [y] must belong to the same type [A].
The definition is inductive and states the reflexivity of the equality.
The others properties (symmetry, transitivity, replacement of
- equals) are proved below. The type of [x] and [y] can be made explicit
- using the notation [x = y :> A] *)
+ equals by equals) are proved below. The type of [x] and [y] can be
+ made explicit using the notation [x = y :> A]. This is Leibniz equality
+ as it expresses that [x] and [y] are equal iff every property on
+ [A] which is true of [x] is also true of [y] *)
Inductive eq (A:Type) (x:A) : A -> Prop :=
refl_equal : x = x :>A
- where "x = y :> A" := (@eq A x y) : type_scope.
+
+where "x = y :> A" := (@eq A x y) : type_scope.
Notation "x = y" := (x = y :>_) : type_scope.
Notation "x <> y :> T" := (~ x = y :>T) : type_scope.
@@ -217,16 +229,6 @@ Section Logic_lemmas.
End equality.
-(* Is now a primitive principle
- Theorem eq_rect: (A:Type)(x:A)(P:A->Type)(P x)->(y:A)(eq ? x y)->(P y).
- Proof.
- Intros.
- Cut (identity A x y).
- NewDestruct 1; Auto.
- NewDestruct H; Auto.
- Qed.
-*)
-
Definition eq_ind_r :
forall (A:Type) (x:A) (P:A -> Prop), P x -> forall y:A, y = x -> P y.
intros A x P H y H0; elim sym_eq with (1 := H0); assumption.
@@ -277,3 +279,14 @@ Proof.
Qed.
Hint Immediate sym_eq sym_not_eq: core v62.
+
+(** Other notations *)
+
+Notation "'exists' ! x , P" :=
+ (exists x', (fun x => P) x' /\ forall x'', (fun x => P) x'' -> x' = x'')
+ (at level 200, x ident, right associativity,
+ format "'[' 'exists' ! '/ ' x , '/ ' P ']'") : type_scope.
+Notation "'exists' ! x : A , P" :=
+ (exists x' : A, (fun x => P) x' /\ forall x'':A, (fun x => P) x'' -> x' = x'')
+ (at level 200, x ident, right associativity,
+ format "'[' 'exists' ! '/ ' x : A , '/ ' P ']'") : type_scope.
diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v
index 0e62e842..857ffe94 100755..100644
--- a/theories/Init/Logic_Type.v
+++ b/theories/Init/Logic_Type.v
@@ -6,18 +6,48 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Logic_Type.v,v 1.19.2.1 2004/07/16 19:31:03 herbelin Exp $ i*)
+(*i $Id: Logic_Type.v 8642 2006-03-17 10:09:02Z notin $ i*)
-Set Implicit Arguments.
+(** This module defines type constructors for types in [Type]
+ ([Datatypes.v] and [Logic.v] defined them for types in [Set]) *)
-(** This module defines quantification on the world [Type]
- ([Logic.v] was defining it on the world [Set]) *)
+Set Implicit Arguments.
Require Import Datatypes.
Require Export Logic.
+(** Negation of a type in [Type] *)
+
Definition notT (A:Type) := A -> False.
+(** Conjunction of types in [Type] *)
+
+Inductive prodT (A B:Type) : Type :=
+ pairT : A -> B -> prodT A B.
+
+Section prodT_proj.
+
+ Variables A B : Type.
+
+ Definition fstT (H:prodT A B) := match H with
+ | pairT x _ => x
+ end.
+ Definition sndT (H:prodT A B) := match H with
+ | pairT _ y => y
+ end.
+
+End prodT_proj.
+
+Definition prodT_uncurry (A B C:Type) (f:prodT A B -> C)
+ (x:A) (y:B) : C := f (pairT x y).
+
+Definition prodT_curry (A B C:Type) (f:A -> B -> C)
+ (p:prodT A B) : C := match p with
+ | pairT x y => f x y
+ end.
+
+(** Properties of [identity] *)
+
Section identity_is_a_congruence.
Variables A B : Type.
@@ -62,28 +92,4 @@ Definition identity_rect_r :
intros A x P H y H0; case sym_id with (1 := H0); trivial.
Defined.
-Inductive prodT (A B:Type) : Type :=
- pairT : A -> B -> prodT A B.
-
-Section prodT_proj.
-
- Variables A B : Type.
-
- Definition fstT (H:prodT A B) := match H with
- | pairT x _ => x
- end.
- Definition sndT (H:prodT A B) := match H with
- | pairT _ y => y
- end.
-
-End prodT_proj.
-
-Definition prodT_uncurry (A B C:Type) (f:prodT A B -> C)
- (x:A) (y:B) : C := f (pairT x y).
-
-Definition prodT_curry (A B C:Type) (f:A -> B -> C)
- (p:prodT A B) : C := match p with
- | pairT x y => f x y
- end.
-
Hint Immediate sym_id sym_not_id: core v62.
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index e0a18747..3ca93067 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Notations.v,v 1.24.2.2 2004/08/01 09:36:44 herbelin Exp $ i*)
+(*i $Id: Notations.v 6410 2004-12-06 11:34:35Z herbelin $ i*)
(** These are the notations whose level and associativity are imposed by Coq *)
@@ -54,15 +54,12 @@ Reserved Notation "x ^ y" (at level 30, right associativity).
Reserved Notation "( x , y , .. , z )" (at level 0).
(** Notation "{ x }" is reserved and has a special status as component
- of other notations; it is at level 0 to factor with {x:A|P} etc *)
+ of other notations such as "{ A } + { B }" and "A + { B }" (which
+ are at the same level than "x + y");
+ "{ x }" is at level 0 to factor with "{ x : A | P }" *)
Reserved Notation "{ x }" (at level 0, x at level 99).
-(** Notations for sum-types *)
-
-Reserved Notation "{ A } + { B }" (at level 50, left associativity).
-Reserved Notation "A + { B }" (at level 50, left associativity).
-
(** Notations for sigma-types or subsets *)
Reserved Notation "{ x : A | P }" (at level 0, x at level 99).
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index 789a020f..c0416b63 100755..100644
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -6,9 +6,10 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Peano.v,v 1.23.2.1 2004/07/16 19:31:03 herbelin Exp $ i*)
+(*i $Id: Peano.v 8642 2006-03-17 10:09:02Z notin $ i*)
-(** Natural numbers [nat] built from [O] and [S] are defined in Datatypes.v *)
+(** The type [nat] of Peano natural numbers (built from [O] and [S])
+ is defined in [Datatypes.v] *)
(** This module defines the following operations on natural numbers :
- predecessor [pred]
@@ -19,13 +20,15 @@
- greater or equal [ge]
- greater [gt]
- This module states various lemmas and theorems about natural numbers,
- including Peano's axioms of arithmetic (in Coq, these are in fact provable)
- Case analysis on [nat] and induction on [nat * nat] are provided too *)
+ It states various lemmas and theorems about natural numbers,
+ including Peano's axioms of arithmetic (in Coq, these are provable).
+ Case analysis on [nat] and induction on [nat * nat] are provided too
+ *)
Require Import Notations.
Require Import Datatypes.
Require Import Logic.
+Unset Boxed Definitions.
Open Scope nat_scope.
@@ -47,6 +50,8 @@ Proof.
auto.
Qed.
+(** Injectivity of successor *)
+
Theorem eq_add_S : forall n m:nat, S n = S m -> n = m.
Proof.
intros n m H; change (pred (S n) = pred (S m)) in |- *; auto.
@@ -54,21 +59,20 @@ Qed.
Hint Immediate eq_add_S: core v62.
-(** A consequence of the previous axioms *)
-
Theorem not_eq_S : forall n m:nat, n <> m -> S n <> S m.
Proof.
red in |- *; auto.
Qed.
Hint Resolve not_eq_S: core v62.
+(** Zero is not the successor of a number *)
+
Definition IsSucc (n:nat) : Prop :=
match n with
| O => False
| S p => True
end.
-
Theorem O_S : forall n:nat, 0 <> S n.
Proof.
red in |- *; intros n H.
@@ -88,13 +92,14 @@ Hint Resolve n_Sn: core v62.
Fixpoint plus (n m:nat) {struct n} : nat :=
match n with
| O => m
- | S p => S (plus p m)
- end.
+ | S p => S (p + m)
+ end
+
+where "n + m" := (plus n m) : nat_scope.
+
Hint Resolve (f_equal2 plus): v62.
Hint Resolve (f_equal2 (A1:=nat) (A2:=nat)): core.
-Infix "+" := plus : nat_scope.
-
Lemma plus_n_O : forall n:nat, n = n + 0.
Proof.
induction n; simpl in |- *; auto.
@@ -122,11 +127,12 @@ Qed.
Fixpoint mult (n m:nat) {struct n} : nat :=
match n with
| O => 0
- | S p => m + mult p m
- end.
-Hint Resolve (f_equal2 mult): core v62.
+ | S p => m + p * m
+ end
-Infix "*" := mult : nat_scope.
+where "n * m" := (mult n m) : nat_scope.
+
+Hint Resolve (f_equal2 mult): core v62.
Lemma mult_n_O : forall n:nat, 0 = n * 0.
Proof.
@@ -142,27 +148,25 @@ Proof.
Qed.
Hint Resolve mult_n_Sm: core v62.
-(** Definition of subtraction on [nat] : [m-n] is [0] if [n>=m] *)
+(** Truncated subtraction: [m-n] is [0] if [n>=m] *)
Fixpoint minus (n m:nat) {struct n} : nat :=
match n, m with
| O, _ => 0
| S k, O => S k
- | S k, S l => minus k l
- end.
+ | S k, S l => k - l
+ end
-Infix "-" := minus : nat_scope.
+where "n - m" := (minus n m) : nat_scope.
(** Definition of the usual orders, the basic properties of [le] and [lt]
can be found in files Le and Lt *)
-(** An inductive definition to define the order *)
-
Inductive le (n:nat) : nat -> Prop :=
- | le_n : le n n
- | le_S : forall m:nat, le n m -> le n (S m).
+ | le_n : n <= n
+ | le_S : forall m:nat, n <= m -> n <= S m
-Infix "<=" := le : nat_scope.
+where "n <= m" := (le n m) : nat_scope.
Hint Constructors le: core v62.
(*i equivalent to : "Hints Resolve le_n le_S : core v62." i*)
@@ -187,7 +191,7 @@ Notation "x <= y < z" := (x <= y /\ y < z) : nat_scope.
Notation "x < y < z" := (x < y /\ y < z) : nat_scope.
Notation "x < y <= z" := (x < y /\ y <= z) : nat_scope.
-(** Pattern-Matching on natural numbers *)
+(** Case analysis *)
Theorem nat_case :
forall (n:nat) (P:nat -> Prop), P 0 -> (forall m:nat, P (S m)) -> P n.
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index 2fe520c4..5f6f1eab 100755..100644
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -6,11 +6,12 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Prelude.v,v 1.11.2.1 2004/07/16 19:31:03 herbelin Exp $ i*)
+(*i $Id: Prelude.v 8642 2006-03-17 10:09:02Z notin $ i*)
Require Export Notations.
Require Export Logic.
Require Export Datatypes.
Require Export Specif.
Require Export Peano.
-Require Export Wf. \ No newline at end of file
+Require Export Wf.
+Require Export Tactics.
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index 6855e689..e7fc1ac4 100755..100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -6,21 +6,21 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Specif.v,v 1.25.2.1 2004/07/16 19:31:04 herbelin Exp $ i*)
+(*i $Id: Specif.v 8642 2006-03-17 10:09:02Z notin $ i*)
-Set Implicit Arguments.
+(** Basic specifications : sets that may contain logical information *)
-(** Basic specifications : Sets containing logical information *)
+Set Implicit Arguments.
Require Import Notations.
Require Import Datatypes.
Require Import Logic.
-(** Subsets *)
+(** Subsets and Sigma-types *)
-(** [(sig A P)], or more suggestively [{x:A | (P x)}], denotes the subset
+(** [(sig A P)], or more suggestively [{x:A | P x}], denotes the subset
of elements of the Set [A] which satisfy the predicate [P].
- Similarly [(sig2 A P Q)], or [{x:A | (P x) & (Q x)}], denotes the subset
+ Similarly [(sig2 A P Q)], or [{x:A | P x & Q x}], denotes the subset
of elements of the Set [A] which satisfy both [P] and [Q]. *)
Inductive sig (A:Set) (P:A -> Prop) : Set :=
@@ -29,8 +29,8 @@ Inductive sig (A:Set) (P:A -> Prop) : Set :=
Inductive sig2 (A:Set) (P Q:A -> Prop) : Set :=
exist2 : forall x:A, P x -> Q x -> sig2 (A:=A) P Q.
-(** [(sigS A P)], or more suggestively [{x:A & (P x)}], is a subtle variant
- of subset where [P] is now of type [Set].
+(** [(sigS A P)], or more suggestively [{x:A & (P x)}] is a Sigma-type.
+ It is a variant of subset where [P] is now of type [Set].
Similarly for [(sigS2 A P Q)], also written [{x:A & (P x) & (Q x)}]. *)
Inductive sigS (A:Set) (P:A -> Set) : Set :=
@@ -57,7 +57,13 @@ Add Printing Let sigS.
Add Printing Let sigS2.
-(** Projections of sig *)
+(** Projections of [sig]
+
+ An element [y] of a subset [{x:A & (P x)}] is the pair of an [a]
+ of type [A] and of a proof [h] that [a] satisfies [P]. Then
+ [(proj1_sig y)] is the witness [a] and [(proj2_sig y)] is the
+ proof of [(P a)] *)
+
Section Subset_projections.
@@ -76,18 +82,18 @@ Section Subset_projections.
End Subset_projections.
-(** Projections of sigS *)
+(** Projections of [sigS]
+
+ An element [x] of a sigma-type [{y:A & P y}] is a dependent pair
+ made of an [a] of type [A] and an [h] of type [P a]. Then,
+ [(projS1 x)] is the first projection and [(projS2 x)] is the
+ second projection, the type of which depends on the [projS1]. *)
Section Projections.
Variable A : Set.
Variable P : A -> Set.
- (** An element [y] of a subset [{x:A & (P x)}] is the pair of an [a] of
- type [A] and of a proof [h] that [a] satisfies [P].
- Then [(projS1 y)] is the witness [a]
- and [(projS2 y)] is the proof of [(P a)] *)
-
Definition projS1 (x:sigS P) : A := match x with
| existS a _ => a
end.
@@ -99,7 +105,8 @@ Section Projections.
End Projections.
-(** Extended_booleans *)
+(** [sumbool] is a boolean type equipped with the justification of
+ their value *)
Inductive sumbool (A B:Prop) : Set :=
| left : A -> {A} + {B}
@@ -108,6 +115,9 @@ Inductive sumbool (A B:Prop) : Set :=
Add Printing If sumbool.
+(** [sumor] is an option type equipped with the justification of why
+ it may not be a regular value *)
+
Inductive sumor (A:Set) (B:Prop) : Set :=
| inleft : A -> A + {B}
| inright : B -> A + {B}
@@ -115,12 +125,10 @@ Inductive sumor (A:Set) (B:Prop) : Set :=
Add Printing If sumor.
-(** Choice *)
+(** Various forms of the axiom of choice for specifications *)
Section Choice_lemmas.
- (** The following lemmas state various forms of the axiom of choice *)
-
Variables S S' : Set.
Variable R : S -> S' -> Prop.
Variable R' : S -> S' -> Set.
@@ -167,8 +175,10 @@ End Choice_lemmas.
(** A result of type [(Exc A)] is either a normal value of type [A] or
an [error] :
- [Inductive Exc [A:Set] : Set := value : A->(Exc A) | error : (Exc A)]
- it is implemented using the option type. *)
+
+ [Inductive Exc [A:Set] : Set := value : A->(Exc A) | error : (Exc A)].
+
+ It is implemented using the option type. *)
Definition Exc := option.
Definition value := Some.
@@ -189,7 +199,7 @@ Qed.
Hint Resolve left right inleft inright: core v62.
-(** Sigma Type at Type level [sigT] *)
+(** Sigma-type for types in [Type] *)
Inductive sigT (A:Type) (P:A -> Type) : Type :=
existT : forall x:A, P x -> sigT (A:=A) P.
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
new file mode 100644
index 00000000..ce37715e
--- /dev/null
+++ b/theories/Init/Tactics.v
@@ -0,0 +1,72 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(*i $Id: Tactics.v 8100 2006-02-27 12:10:03Z letouzey $ i*)
+
+Require Import Notations.
+Require Import Logic.
+
+(** Useful tactics *)
+
+(* A shorter name for generalize + clear, can be seen as an anti-intro *)
+
+Ltac revert H := generalize H; clear H.
+
+(* to contradict an hypothesis without copying its type. *)
+
+Ltac absurd_hyp h :=
+ let T := type of h in
+ absurd T.
+
+(* Transforming a negative goal [ H:~A |- ~B ] into a positive one [ B |- A ]*)
+
+Ltac swap H := intro; apply H; clear H.
+
+(* A case with no loss of information. *)
+
+Ltac case_eq x := generalize (refl_equal x); pattern x at -1; case x.
+
+(* A tactic for easing the use of lemmas f_equal, f_equal2, ... *)
+
+Ltac f_equal :=
+ let cg := try congruence in
+ let r := try reflexivity in
+ match goal with
+ | |- ?f ?a = ?f' ?a' => cut (a=a'); [cg|r]
+ | |- ?f ?a ?b = ?f' ?a' ?b' =>
+ cut (b=b');[cut (a=a');[cg|r]|r]
+ | |- ?f ?a ?b ?c = ?f' ?a' ?b' ?c'=>
+ cut (c=c');[cut (b=b');[cut (a=a');[cg|r]|r]|r]
+ | |- ?f ?a ?b ?c ?d= ?f' ?a' ?b' ?c' ?d'=>
+ cut (d=d');[cut (c=c');[cut (b=b');[cut (a=a');[cg|r]|r]|r]|r]
+ | |- ?f ?a ?b ?c ?d ?e= ?f' ?a' ?b' ?c' ?d' ?e'=>
+ cut (e=e');[cut (d=d');[cut (c=c');[cut (b=b');[cut (a=a');[cg|r]|r]|r]|r]|r]
+ | _ => idtac
+ end.
+
+(* Rewriting in all hypothesis. *)
+
+Ltac rewrite_all Eq := match type of Eq with
+ ?a = ?b =>
+ generalize Eq; clear Eq;
+ match goal with
+ | H : context [a] |- _ => intro Eq; rewrite Eq in H; rewrite_all Eq
+ | _ => intro Eq; try rewrite Eq
+ end
+ end.
+
+Ltac rewrite_all_rev Eq := match type of Eq with
+ ?a = ?b =>
+ generalize Eq; clear Eq;
+ match goal with
+ | H : context [b] |- _ => intro Eq; rewrite <- Eq in H; rewrite_all_rev Eq
+ | _ => intro Eq; try rewrite <- Eq
+ end
+ end.
+
+Tactic Notation "rewrite_all" "<-" constr(H) := rewrite_all_rev H.
diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v
index 7ab3723d..fde70225 100755..100644
--- a/theories/Init/Wf.v
+++ b/theories/Init/Wf.v
@@ -6,61 +6,59 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-Set Implicit Arguments.
-
-(*i $Id: Wf.v,v 1.17.2.1 2004/07/16 19:31:04 herbelin Exp $ i*)
+(*i $Id: Wf.v 8642 2006-03-17 10:09:02Z notin $ i*)
(** This module proves the validity of
- well-founded recursion (also called course of values)
- well-founded induction
- from a well-founded ordering on a given set *)
+ from a well-founded ordering on a given set *)
+
+Set Implicit Arguments.
Require Import Notations.
Require Import Logic.
Require Import Datatypes.
-(** Well-founded induction principle on Prop *)
+(** Well-founded induction principle on [Prop] *)
Section Well_founded.
- Variable A : Set.
+ Variable A : Type.
Variable R : A -> A -> Prop.
(** The accessibility predicate is defined to be non-informative *)
- Inductive Acc : A -> Prop :=
- Acc_intro : forall x:A, (forall y:A, R y x -> Acc y) -> Acc x.
+ Inductive Acc (x: A) : Prop :=
+ Acc_intro : (forall y:A, R y x -> Acc y) -> Acc x.
Lemma Acc_inv : forall x:A, Acc x -> forall y:A, R y x -> Acc y.
destruct 1; trivial.
Defined.
- (** the informative elimination :
+ (** Informative elimination :
[let Acc_rec F = let rec wf x = F x wf in wf] *)
Section AccRecType.
Variable P : A -> Type.
- Variable
- F :
- forall x:A,
- (forall y:A, R y x -> Acc y) -> (forall y:A, R y x -> P y) -> P x.
+ Variable F : forall x:A,
+ (forall y:A, R y x -> Acc y) -> (forall y:A, R y x -> P y) -> P x.
Fixpoint Acc_rect (x:A) (a:Acc x) {struct a} : P x :=
- F (Acc_inv a) (fun (y:A) (h:R y x) => Acc_rect (x:=y) (Acc_inv a h)).
+ F (Acc_inv a) (fun (y:A) (h:R y x) => Acc_rect (Acc_inv a h)).
End AccRecType.
Definition Acc_rec (P:A -> Set) := Acc_rect P.
- (** A simplified version of Acc_rec(t) *)
+ (** A simplified version of [Acc_rect] *)
Section AccIter.
- Variable P : A -> Type.
+ Variable P : A -> Type.
Variable F : forall x:A, (forall y:A, R y x -> P y) -> P x.
Fixpoint Acc_iter (x:A) (a:Acc x) {struct a} : P x :=
- F (fun (y:A) (h:R y x) => Acc_iter (x:=y) (Acc_inv a h)).
+ F (fun (y:A) (h:R y x) => Acc_iter (Acc_inv a h)).
End AccIter.
@@ -68,7 +66,7 @@ Section Well_founded.
Definition well_founded := forall a:A, Acc a.
- (** well-founded induction on Set and Prop *)
+ (** Well-founded induction on [Set] and [Prop] *)
Hypothesis Rwf : well_founded.
@@ -95,47 +93,48 @@ Section Well_founded.
(** Building fixpoints *)
-Section FixPoint.
+ Section FixPoint.
-Variable P : A -> Set.
-Variable F : forall x:A, (forall y:A, R y x -> P y) -> P x.
-
-Fixpoint Fix_F (x:A) (r:Acc x) {struct r} : P x :=
- F (fun (y:A) (p:R y x) => Fix_F (x:=y) (Acc_inv r p)).
+ Variable P : A -> Type.
+ Variable F : forall x:A, (forall y:A, R y x -> P y) -> P x.
-Definition Fix (x:A) := Fix_F (Rwf x).
+ Notation Fix_F := (Acc_iter P F) (only parsing). (* alias *)
-(** Proof that [well_founded_induction] satisfies the fixpoint equation.
- It requires an extra property of the functional *)
+ Definition Fix (x:A) := Acc_iter P F (Rwf x).
-Hypothesis
- F_ext :
- forall (x:A) (f g:forall y:A, R y x -> P y),
- (forall (y:A) (p:R y x), f y p = g y p) -> F f = F g.
+ (** Proof that [well_founded_induction] satisfies the fixpoint equation.
+ It requires an extra property of the functional *)
-Scheme Acc_inv_dep := Induction for Acc Sort Prop.
+ Hypothesis
+ F_ext :
+ forall (x:A) (f g:forall y:A, R y x -> P y),
+ (forall (y:A) (p:R y x), f y p = g y p) -> F f = F g.
-Lemma Fix_F_eq :
- forall (x:A) (r:Acc x),
- F (fun (y:A) (p:R y x) => Fix_F (Acc_inv r p)) = Fix_F r.
-destruct r using Acc_inv_dep; auto.
-Qed.
+ Scheme Acc_inv_dep := Induction for Acc Sort Prop.
-Lemma Fix_F_inv : forall (x:A) (r s:Acc x), Fix_F r = Fix_F s.
-intro x; induction (Rwf x); intros.
-rewrite <- (Fix_F_eq r); rewrite <- (Fix_F_eq s); intros.
-apply F_ext; auto.
-Qed.
+ Lemma Fix_F_eq :
+ forall (x:A) (r:Acc x),
+ F (fun (y:A) (p:R y x) => Fix_F y (Acc_inv r p)) = Fix_F x r.
+ Proof.
+ destruct r using Acc_inv_dep; auto.
+ Qed.
+ Lemma Fix_F_inv : forall (x:A) (r s:Acc x), Fix_F x r = Fix_F x s.
+ Proof.
+ intro x; induction (Rwf x); intros.
+ rewrite <- (Fix_F_eq r); rewrite <- (Fix_F_eq s); intros.
+ apply F_ext; auto.
+ Qed.
-Lemma Fix_eq : forall x:A, Fix x = F (fun (y:A) (p:R y x) => Fix y).
-intro x; unfold Fix in |- *.
-rewrite <- (Fix_F_eq (x:=x)).
-apply F_ext; intros.
-apply Fix_F_inv.
-Qed.
+ Lemma Fix_eq : forall x:A, Fix x = F (fun (y:A) (p:R y x) => Fix y).
+ Proof.
+ intro x; unfold Fix in |- *.
+ rewrite <- (Fix_F_eq (x:=x)).
+ apply F_ext; intros.
+ apply Fix_F_inv.
+ Qed.
-End FixPoint.
+ End FixPoint.
End Well_founded.
@@ -169,3 +168,5 @@ Section Well_founded_2.
Defined.
End Well_founded_2.
+
+Notation Fix_F := Acc_iter (only parsing). (* compatibility *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-04 20:42:46 +0000