summaryrefslogtreecommitdiff
path: root/theories/Init
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Init')
-rw-r--r--theories/Init/Datatypes.v60
-rw-r--r--theories/Init/Logic.v135
-rw-r--r--theories/Init/Logic_Type.v8
-rw-r--r--theories/Init/Notations.v11
-rw-r--r--theories/Init/Peano.v24
-rw-r--r--theories/Init/Prelude.v6
-rw-r--r--theories/Init/Specif.v21
-rw-r--r--theories/Init/Tactics.v154
-rw-r--r--theories/Init/Wf.v69
9 files changed, 371 insertions, 117 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 56dc7e95..e5e6fd23 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Datatypes.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Datatypes.v 11073 2008-06-08 20:24:51Z herbelin $ i*)
Set Implicit Arguments.
@@ -26,6 +26,52 @@ Inductive bool : Set :=
Add Printing If bool.
+Delimit Scope bool_scope with bool.
+
+Bind Scope bool_scope with bool.
+
+(** Basic boolean operators *)
+
+Definition andb (b1 b2:bool) : bool := if b1 then b2 else false.
+
+Definition orb (b1 b2:bool) : bool := if b1 then true else b2.
+
+Definition implb (b1 b2:bool) : bool := if b1 then b2 else true.
+
+Definition xorb (b1 b2:bool) : bool :=
+ match b1, b2 with
+ | true, true => false
+ | true, false => true
+ | false, true => true
+ | false, false => false
+ end.
+
+Definition negb (b:bool) := if b then false else true.
+
+Infix "||" := orb : bool_scope.
+Infix "&&" := andb : bool_scope.
+
+(*******************************)
+(** * Properties of [andb] *)
+(*******************************)
+
+Lemma andb_prop : forall a b:bool, andb a b = true -> a = true /\ b = true.
+Proof.
+ destruct a; destruct b; intros; split; try (reflexivity || discriminate).
+Qed.
+Hint Resolve andb_prop: bool v62.
+
+Lemma andb_true_intro :
+ forall b1 b2:bool, b1 = true /\ b2 = true -> andb b1 b2 = true.
+Proof.
+ destruct b1; destruct b2; simpl in |- *; tauto || auto with bool.
+Qed.
+Hint Resolve andb_true_intro: bool v62.
+
+(** Interpretation of booleans as propositions *)
+
+Inductive eq_true : bool -> Prop := is_eq_true : eq_true true.
+
(** [nat] is the datatype of natural numbers built from [O] and successor [S];
note that the constructor name is the letter O.
Numbers in [nat] can be denoted using a decimal notation;
@@ -70,7 +116,7 @@ Definition option_map (A B:Type) (f:A->B) o :=
end.
(** [sum A B], written [A + B], is the disjoint sum of [A] and [B] *)
-(* Syntax defined in Specif.v *)
+
Inductive sum (A B:Type) : Type :=
| inl : A -> sum A B
| inr : B -> sum A B.
@@ -82,6 +128,7 @@ Notation "x + y" := (sum x y) : type_scope.
Inductive prod (A B:Type) : Type :=
pair : A -> B -> prod A B.
+
Add Printing Let prod.
Notation "x * y" := (prod x y) : type_scope.
@@ -135,6 +182,13 @@ Definition CompOpp (r:comparison) :=
| Gt => Lt
end.
+(** Identity *)
+
+Definition ID := forall A:Type, A -> A.
+Definition id : ID := fun A x => x.
+
+(* begin hide *)
+
(* Compatibility *)
Notation prodT := prod (only parsing).
@@ -146,3 +200,5 @@ Notation fstT := fst (only parsing).
Notation sndT := snd (only parsing).
Notation prodT_uncurry := prod_uncurry (only parsing).
Notation prodT_curry := prod_curry (only parsing).
+
+(* end hide *)
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 8b487432..6a636ccc 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Logic.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Logic.v 10304 2007-11-08 17:06:32Z emakarov $ i*)
Set Implicit Arguments.
@@ -16,10 +16,10 @@ Require Import Notations.
(** [True] is the always true proposition *)
Inductive True : Prop :=
- I : True.
+ I : True.
(** [False] is the always false proposition *)
-Inductive False : Prop :=.
+Inductive False : Prop :=.
(** [not A], written [~A], is the negation of [A] *)
Definition not (A:Prop) := A -> False.
@@ -30,14 +30,14 @@ Hint Unfold not: core.
(** [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
+ [conj p q] is a proof of [A /\ B] as soon as
[p] is a proof of [A] and [q] a proof of [B]
[proj1] and [proj2] are first and second projections of a conjunction *)
Inductive and (A B:Prop) : Prop :=
- conj : A -> B -> A /\ B
-
+ conj : A -> B -> A /\ B
+
where "A /\ B" := (and A B) : type_scope.
Section Conjunction.
@@ -60,7 +60,7 @@ End Conjunction.
Inductive or (A B:Prop) : Prop :=
| or_introl : A -> A \/ B
- | or_intror : B -> A \/ B
+ | or_intror : B -> A \/ B
where "A \/ B" := (or A B) : type_scope.
@@ -89,6 +89,67 @@ Theorem iff_sym : forall A B:Prop, (A <-> B) -> (B <-> A).
End Equivalence.
+Hint Unfold iff: extcore.
+
+(** Some equivalences *)
+
+Theorem neg_false : forall A : Prop, ~ A <-> (A <-> False).
+Proof.
+intro A; unfold not; split.
+intro H; split; [exact H | intro H1; elim H1].
+intros [H _]; exact H.
+Qed.
+
+Theorem and_cancel_l : forall A B C : Prop,
+ (B -> A) -> (C -> A) -> ((A /\ B <-> A /\ C) <-> (B <-> C)).
+Proof.
+intros; tauto.
+Qed.
+
+Theorem and_cancel_r : forall A B C : Prop,
+ (B -> A) -> (C -> A) -> ((B /\ A <-> C /\ A) <-> (B <-> C)).
+Proof.
+intros; tauto.
+Qed.
+
+Theorem or_cancel_l : forall A B C : Prop,
+ (B -> ~ A) -> (C -> ~ A) -> ((A \/ B <-> A \/ C) <-> (B <-> C)).
+Proof.
+intros; tauto.
+Qed.
+
+Theorem or_cancel_r : forall A B C : Prop,
+ (B -> ~ A) -> (C -> ~ A) -> ((B \/ A <-> C \/ A) <-> (B <-> C)).
+Proof.
+intros; tauto.
+Qed.
+
+(** Backward direction of the equivalences above does not need assumptions *)
+
+Theorem and_iff_compat_l : forall A B C : Prop,
+ (B <-> C) -> (A /\ B <-> A /\ C).
+Proof.
+intros; tauto.
+Qed.
+
+Theorem and_iff_compat_r : forall A B C : Prop,
+ (B <-> C) -> (B /\ A <-> C /\ A).
+Proof.
+intros; tauto.
+Qed.
+
+Theorem or_iff_compat_l : forall A B C : Prop,
+ (B <-> C) -> (A \/ B <-> A \/ C).
+Proof.
+intros; tauto.
+Qed.
+
+Theorem or_iff_compat_r : forall A B C : Prop,
+ (B <-> C) -> (B \/ A <-> C \/ A).
+Proof.
+intros; tauto.
+Qed.
+
(** [(IF_then_else P Q R)], written [IF P then Q else R] denotes
either [P] and [Q], or [~P] and [Q] *)
@@ -103,7 +164,7 @@ Notation "'IF' c1 'then' c2 'else' c3" := (IF_then_else c1 c2 c3)
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
+ [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].
@@ -123,14 +184,14 @@ Inductive ex (A:Type) (P:A -> Prop) : Prop :=
Inductive ex2 (A:Type) (P Q:A -> Prop) : Prop :=
ex_intro2 : forall x:A, P x -> Q x -> ex2 (A:=A) P Q.
-Definition all (A:Type) (P:A -> Prop) := forall x:A, P x.
+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, right associativity) : type_scope.
Notation "'exists' x : t , p" := (ex (fun x:t => p))
- (at level 200, x ident, right associativity,
+ (at level 200, x ident, right associativity,
format "'[' 'exists' '/ ' x : t , '/ ' p ']'")
: type_scope.
@@ -165,14 +226,14 @@ End universal_quantification.
(** [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
+ The others properties (symmetry, transitivity, replacement of
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
+ refl_equal : x = x :>A
where "x = y :> A" := (@eq A x y) : type_scope.
@@ -222,7 +283,7 @@ Section Logic_lemmas.
Proof.
red in |- *; intros h1 h2; apply h1; destruct h2; trivial.
Qed.
-
+
Definition sym_equal := sym_eq.
Definition sym_not_equal := sym_not_eq.
Definition trans_equal := trans_eq.
@@ -233,12 +294,12 @@ Section Logic_lemmas.
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.
Defined.
-
+
Definition eq_rec_r :
forall (A:Type) (x:A) (P:A -> Set), P x -> forall y:A, y = x -> P y.
intros A x P H y H0; elim sym_eq with (1 := H0); assumption.
Defined.
-
+
Definition eq_rect_r :
forall (A:Type) (x:A) (P:A -> Type), P x -> forall y:A, y = x -> P y.
intros A x P H y H0; elim sym_eq with (1 := H0); assumption.
@@ -246,14 +307,14 @@ Section Logic_lemmas.
End Logic_lemmas.
Theorem f_equal2 :
- forall (A1 A2 B:Type) (f:A1 -> A2 -> B) (x1 y1:A1)
+ forall (A1 A2 B:Type) (f:A1 -> A2 -> B) (x1 y1:A1)
(x2 y2:A2), x1 = y1 -> x2 = y2 -> f x1 x2 = f y1 y2.
Proof.
destruct 1; destruct 1; reflexivity.
Qed.
Theorem f_equal3 :
- forall (A1 A2 A3 B:Type) (f:A1 -> A2 -> A3 -> B) (x1 y1:A1)
+ forall (A1 A2 A3 B:Type) (f:A1 -> A2 -> A3 -> B) (x1 y1:A1)
(x2 y2:A2) (x3 y3:A3),
x1 = y1 -> x2 = y2 -> x3 = y3 -> f x1 x2 x3 = f y1 y2 y3.
Proof.
@@ -261,7 +322,7 @@ Proof.
Qed.
Theorem f_equal4 :
- forall (A1 A2 A3 A4 B:Type) (f:A1 -> A2 -> A3 -> A4 -> B)
+ forall (A1 A2 A3 A4 B:Type) (f:A1 -> A2 -> A3 -> A4 -> B)
(x1 y1:A1) (x2 y2:A2) (x3 y3:A3) (x4 y4:A4),
x1 = y1 -> x2 = y2 -> x3 = y3 -> x4 = y4 -> f x1 x2 x3 x4 = f y1 y2 y3 y4.
Proof.
@@ -295,7 +356,7 @@ Definition uniqueness (A:Type) (P:A->Prop) := forall x y, P x -> P y -> x = y.
Notation "'exists' ! x , P" := (ex (unique (fun x => P)))
(at level 200, x ident, right associativity,
format "'[' 'exists' ! '/ ' x , '/ ' P ']'") : type_scope.
-Notation "'exists' ! x : A , P" :=
+Notation "'exists' ! x : A , P" :=
(ex (unique (fun x:A => P)))
(at level 200, x ident, right associativity,
format "'[' 'exists' ! '/ ' x : A , '/ ' P ']'") : type_scope.
@@ -305,15 +366,47 @@ Lemma unique_existence : forall (A:Type) (P:A->Prop),
Proof.
intros A P; split.
intros ((x,Hx),Huni); exists x; red; auto.
- intros (x,(Hx,Huni)); split.
+ intros (x,(Hx,Huni)); split.
exists x; assumption.
intros x' x'' Hx' Hx''; transitivity x.
symmetry; auto.
auto.
Qed.
-(** Being inhabited *)
+(** * Being inhabited *)
+
+(** The predicate [inhabited] can be used in different contexts. If [A] is
+ thought as a type, [inhabited A] states that [A] is inhabited. If [A] is
+ thought as a computationally relevant proposition, then
+ [inhabited A] weakens [A] so as to hide its computational meaning.
+ The so-weakened proof remains computationally relevant but only in
+ a propositional context.
+*)
Inductive inhabited (A:Type) : Prop := inhabits : A -> inhabited A.
Hint Resolve inhabits: core.
+
+Lemma exists_inhabited : forall (A:Type) (P:A->Prop),
+ (exists x, P x) -> inhabited A.
+Proof.
+ destruct 1; auto.
+Qed.
+
+(** Declaration of stepl and stepr for eq and iff *)
+
+Lemma eq_stepl : forall (A : Type) (x y z : A), x = y -> x = z -> z = y.
+Proof.
+intros A x y z H1 H2. rewrite <- H2; exact H1.
+Qed.
+
+Declare Left Step eq_stepl.
+Declare Right Step trans_eq.
+
+Lemma iff_stepl : forall A B C : Prop, (A <-> B) -> (A <-> C) -> (C <-> B).
+Proof.
+intros; tauto.
+Qed.
+
+Declare Left Step iff_stepl.
+Declare Right Step iff_trans.
diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v
index dbe944b0..c4e5f6c7 100644
--- a/theories/Init/Logic_Type.v
+++ b/theories/Init/Logic_Type.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Logic_Type.v 8866 2006-05-28 16:21:04Z herbelin $ i*)
+(*i $Id: Logic_Type.v 10840 2008-04-23 21:29:34Z herbelin $ i*)
(** This module defines type constructors for types in [Type]
([Datatypes.v] and [Logic.v] defined them for types in [Set]) *)
@@ -32,17 +32,17 @@ Section identity_is_a_congruence.
Lemma sym_id : identity x y -> identity y x.
Proof.
destruct 1; trivial.
- Qed.
+ Defined.
Lemma trans_id : identity x y -> identity y z -> identity x z.
Proof.
destruct 2; trivial.
- Qed.
+ Defined.
Lemma congr_id : identity x y -> identity (f x) (f y).
Proof.
destruct 1; trivial.
- Qed.
+ Defined.
Lemma sym_not_id : notT (identity x y) -> notT (identity y x).
Proof.
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index 416647b4..3dc6385d 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 8866 2006-05-28 16:21:04Z herbelin $ i*)
+(*i $Id: Notations.v 11073 2008-06-08 20:24:51Z herbelin $ i*)
(** These are the notations whose level and associativity are imposed by Coq *)
@@ -19,13 +19,13 @@ Reserved Notation "~ x" (at level 75, right associativity).
(** Notations for equality and inequalities *)
-Reserved Notation "x = y :> T"
+Reserved Notation "x = y :> T"
(at level 70, y at next level, no associativity).
Reserved Notation "x = y" (at level 70, no associativity).
Reserved Notation "x = y = z"
(at level 70, no associativity, y at next level).
-Reserved Notation "x <> y :> T"
+Reserved Notation "x <> y :> T"
(at level 70, y at next level, no associativity).
Reserved Notation "x <> y" (at level 70, no associativity).
@@ -49,6 +49,11 @@ Reserved Notation "- x" (at level 35, right associativity).
Reserved Notation "/ x" (at level 35, right associativity).
Reserved Notation "x ^ y" (at level 30, right associativity).
+(** Notations for booleans *)
+
+Reserved Notation "x || y" (at level 50, left associativity).
+Reserved Notation "x && y" (at level 40, left associativity).
+
(** Notations for pairs *)
Reserved Notation "( x , y , .. , z )" (at level 0).
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index 3df2b566..9ef63cc8 100644
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Peano.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Peano.v 11115 2008-06-12 16:03:32Z werner $ i*)
(** The type [nat] of Peano natural numbers (built from [O] and [S])
is defined in [Datatypes.v] *)
@@ -40,7 +40,7 @@ Hint Resolve (f_equal (A:=nat)): core.
(** The predecessor function *)
Definition pred (n:nat) : nat := match n with
- | O => 0
+ | O => n
| S u => u
end.
Hint Resolve (f_equal pred): v62.
@@ -123,6 +123,11 @@ Proof.
auto.
Qed.
+(** Standard associated names *)
+
+Notation plus_0_r_reverse := plus_n_O (only parsing).
+Notation plus_succ_r_reverse := plus_n_Sm (only parsing).
+
(** Multiplication *)
Fixpoint mult (n m:nat) {struct n} : nat :=
@@ -149,12 +154,21 @@ Proof.
Qed.
Hint Resolve mult_n_Sm: core v62.
+(** Standard associated names *)
+
+Notation mult_0_r_reverse := mult_n_O (only parsing).
+Notation mult_succ_r_reverse := mult_n_Sm (only parsing).
+
(** 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
+ | O, _ => n
+ | S k, O => n
+(*=======
+
+ | O, _ => n
+ | S k, O => S k *)
| S k, S l => k - l
end
@@ -211,5 +225,3 @@ Proof.
induction n; auto.
destruct m as [| n0]; auto.
Qed.
-
-(** Notations *)
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index 5f6f1eab..6492c948 100644
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -6,12 +6,12 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Prelude.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id: Prelude.v 10064 2007-08-08 15:32:36Z msozeau $ i*)
Require Export Notations.
Require Export Logic.
Require Export Datatypes.
Require Export Specif.
Require Export Peano.
-Require Export Wf.
-Require Export Tactics.
+Require Export Coq.Init.Wf.
+Require Export Coq.Init.Tactics.
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index dd2f7697..c0f5c42a 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Specif.v 8866 2006-05-28 16:21:04Z herbelin $ i*)
+(*i $Id: Specif.v 10923 2008-05-12 18:25:06Z herbelin $ i*)
(** Basic specifications : sets that may contain logical information *)
@@ -46,12 +46,12 @@ Arguments Scope sigT [type_scope type_scope].
Arguments Scope sigT2 [type_scope type_scope type_scope].
Notation "{ x | P }" := (sig (fun x => P)) : type_scope.
-Notation "{ x | P & Q }" := (sig2 (fun x => P) (fun x => Q)) : type_scope.
+Notation "{ x | P & Q }" := (sig2 (fun x => P) (fun x => Q)) : type_scope.
Notation "{ x : A | P }" := (sig (fun x:A => P)) : type_scope.
-Notation "{ x : A | P & Q }" := (sig2 (fun x:A => P) (fun x:A => Q)) :
+Notation "{ x : A | P & Q }" := (sig2 (fun x:A => P) (fun x:A => Q)) :
type_scope.
-Notation "{ x : A & P }" := (sigT (fun x:A => P)) : type_scope.
-Notation "{ x : A & P & Q }" := (sigT2 (fun x:A => P) (fun x:A => Q)) :
+Notation "{ x : A & P }" := (sigT (fun x:A => P)) : type_scope.
+Notation "{ x : A & P & Q }" := (sigT2 (fun x:A => P) (fun x:A => Q)) :
type_scope.
Add Printing Let sig.
@@ -107,6 +107,16 @@ Section Projections.
End Projections.
+(** [sigT] of a predicate is equivalent to [sig] *)
+
+Lemma sig_of_sigT : forall (A:Type) (P:A->Prop), sigT P -> sig P.
+Proof. destruct 1 as (x,H); exists x; trivial. Defined.
+
+Lemma sigT_of_sig : forall (A:Type) (P:A->Prop), sig P -> sigT P.
+Proof. destruct 1 as (x,H); exists x; trivial. Defined.
+
+Coercion sigT_of_sig : sig >-> sigT.
+Coercion sig_of_sigT : sigT >-> sig.
(** [sumbool] is a boolean type equipped with the justification of
their value *)
@@ -201,6 +211,7 @@ Proof.
Qed.
Hint Resolve left right inleft inright: core v62.
+Hint Resolve exist exist2 existT existT2: core.
(* Compatibility *)
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index ba210dd6..afe8297e 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -6,59 +6,143 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Tactics.v 9268 2006-10-24 12:56:16Z herbelin $ i*)
+(*i $Id: Tactics.v 11072 2008-06-08 16:13:37Z herbelin $ i*)
Require Import Notations.
Require Import Logic.
-(** Useful tactics *)
+(** * Useful tactics *)
+
+(** A tactic for proof by contradiction. With contradict H,
+ - H:~A |- B gives |- A
+ - H:~A |- ~B gives H: B |- A
+ - H: A |- B gives |- ~A
+ - H: A |- ~B gives H: B |- ~A
+ - H:False leads to a resolved subgoal.
+ Moreover, negations may be in unfolded forms,
+ and A or B may live in Type *)
+
+Ltac contradict H :=
+ let save tac H := let x:=fresh in intro x; tac H; rename x into H
+ in
+ let negpos H := case H; clear H
+ in
+ let negneg H := save negpos H
+ in
+ let pospos H :=
+ let A := type of H in (elimtype False; revert H; try fold (~A))
+ in
+ let posneg H := save pospos H
+ in
+ let neg H := match goal with
+ | |- (~_) => negneg H
+ | |- (_->False) => negneg H
+ | |- _ => negpos H
+ end in
+ let pos H := match goal with
+ | |- (~_) => posneg H
+ | |- (_->False) => posneg H
+ | |- _ => pospos H
+ end in
+ match type of H with
+ | (~_) => neg H
+ | (_->False) => neg H
+ | _ => (elim H;fail) || pos H
+ end.
-(* A shorter name for generalize + clear, can be seen as an anti-intro *)
+(* Transforming a negative goal [ H:~A |- ~B ] into a positive one [ B |- A ]*)
-Tactic Notation "revert" ne_hyp_list(l) := generalize l; clear l.
+Ltac swap H :=
+ idtac "swap is OBSOLETE: use contradict instead.";
+ intro; apply H; clear H.
-(* to contradict an hypothesis without copying its type. *)
+(* To contradict an hypothesis without copying its type. *)
-Ltac absurd_hyp h :=
- let T := type of h in
+Ltac absurd_hyp H :=
+ idtac "absurd_hyp is OBSOLETE: use contradict instead.";
+ let T := type of H in
absurd T.
-(* Transforming a negative goal [ H:~A |- ~B ] into a positive one [ B |- A ]*)
+(* A useful complement to contradict. Here H:A while G allows to conclude ~A *)
-Ltac swap H := intro; apply H; clear H.
+Ltac false_hyp H G :=
+ let T := type of H in absurd T; [ apply G | assumption ].
(* 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 several times everywhere *)
Tactic Notation "rewrite_all" constr(eq) := repeat rewrite eq in *.
Tactic Notation "rewrite_all" "<-" constr(eq) := repeat rewrite <- eq in *.
-(* Keeping a copy of an expression *)
-
-Ltac remembertac x a :=
- let x := fresh x in
- let H := fresh "Heq" x in
- (set (x:=a) in *; assert (H: x=a) by reflexivity; clearbody x).
-
-Tactic Notation "remember" constr(c) "as" ident(x) := remembertac x c.
+(** Tactics for applying equivalences.
+
+The following code provides tactics "apply -> t", "apply <- t",
+"apply -> t in H" and "apply <- t in H". Here t is a term whose type
+consists of nested dependent and nondependent products with an
+equivalence A <-> B as the conclusion. The tactics with "->" in their
+names apply A -> B while those with "<-" in the name apply B -> A. *)
+
+(* The idea of the tactics is to first provide a term in the context
+whose type is the implication (in one of the directions), and then
+apply it. The first idea is to produce a statement "forall ..., A ->
+B" (call this type T) and then do "assert (H : T)" for a fresh H.
+Thus, T can be proved from the original equivalence and then used to
+perform the application. However, currently in Ltac it is difficult
+to produce such T from the original formula.
+
+Therefore, we first pose the original equivalence as H. If the type of
+H is a dependent product, we create an existential variable and apply
+H to this variable. If the type of H has the form C -> D, then we do a
+cut on C. Once we eliminate all products, we split (i.e., destruct)
+the conjunction into two parts and apply the relevant one. *)
+
+Ltac find_equiv H :=
+let T := type of H in
+lazymatch T with
+| ?A -> ?B =>
+ let H1 := fresh in
+ let H2 := fresh in
+ cut A;
+ [intro H1; pose proof (H H1) as H2; clear H H1;
+ rename H2 into H; find_equiv H |
+ clear H]
+| forall x : ?t, _ =>
+ let a := fresh "a" with
+ H1 := fresh "H" in
+ evar (a : t); pose proof (H a) as H1; unfold a in H1;
+ clear a; clear H; rename H1 into H; find_equiv H
+| ?A <-> ?B => idtac
+| _ => fail "The given statement does not seem to end with an equivalence"
+end.
+
+Ltac bapply lemma todo :=
+let H := fresh in
+ pose proof lemma as H;
+ find_equiv H; [todo H; clear H | .. ].
+
+Tactic Notation "apply" "->" constr(lemma) :=
+bapply lemma ltac:(fun H => destruct H as [H _]; apply H).
+
+Tactic Notation "apply" "<-" constr(lemma) :=
+bapply lemma ltac:(fun H => destruct H as [_ H]; apply H).
+
+Tactic Notation "apply" "->" constr(lemma) "in" ident(J) :=
+bapply lemma ltac:(fun H => destruct H as [H _]; apply H in J).
+
+Tactic Notation "apply" "<-" constr(lemma) "in" ident(J) :=
+bapply lemma ltac:(fun H => destruct H as [_ H]; apply H in J).
+
+(** A tactic simpler than auto that is useful for ending proofs "in one step" *)
+Tactic Notation "now" tactic(t) :=
+t;
+match goal with
+| H : _ |- _ => solve [inversion H]
+| _ => solve [trivial | reflexivity | symmetry; trivial | discriminate | split]
+| _ => fail 1 "Cannot solve this goal"
+end.
+
+(** A tactic to document or check what is proved at some point of a script *)
+Ltac now_show c := change c.
diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v
index 4e0f3745..f46b2b11 100644
--- a/theories/Init/Wf.v
+++ b/theories/Init/Wf.v
@@ -6,12 +6,11 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Wf.v 8988 2006-06-25 22:15:32Z letouzey $ i*)
+(*i $Id: Wf.v 10712 2008-03-23 11:38:38Z herbelin $ i*)
-(** This module proves the validity of
- - well-founded recursion (also called course of values)
+(** * This module proves the validity of
+ - well-founded recursion (also known as course of values)
- well-founded induction
-
from a well-founded ordering on a given set *)
Set Implicit Arguments.
@@ -40,6 +39,7 @@ Section Well_founded.
[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.
@@ -51,17 +51,6 @@ Section Well_founded.
Definition Acc_rec (P:A -> Set) := Acc_rect P.
- (** A simplified version of [Acc_rect] *)
-
- Section AccIter.
- 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 (Acc_inv a h)).
-
- End AccIter.
-
(** A relation is well-founded if every element is accessible *)
Definition well_founded := forall a:A, Acc a.
@@ -74,7 +63,7 @@ Section Well_founded.
forall P:A -> Type,
(forall x:A, (forall y:A, R y x -> P y) -> P x) -> forall a:A, P a.
Proof.
- intros; apply (Acc_iter P); auto.
+ intros; apply Acc_rect; auto.
Defined.
Theorem well_founded_induction :
@@ -91,16 +80,26 @@ Section Well_founded.
exact (fun P:A -> Prop => well_founded_induction_type P).
Defined.
-(** Building fixpoints *)
+(** Well-founded fixpoints *)
Section FixPoint.
Variable P : A -> Type.
Variable F : forall x:A, (forall y:A, R y x -> P y) -> P x.
- Notation Fix_F := (Acc_iter P F) (only parsing). (* alias *)
+ Fixpoint Fix_F (x:A) (a:Acc x) {struct a} : P x :=
+ F (fun (y:A) (h:R y x) => Fix_F (Acc_inv a h)).
+
+ Scheme Acc_inv_dep := Induction for Acc Sort Prop.
+
+ Lemma Fix_F_eq :
+ forall (x:A) (r:Acc x),
+ F (fun (y:A) (p:R y x) => Fix_F (x:=y) (Acc_inv r p)) = Fix_F (x:=x) r.
+ Proof.
+ destruct r using Acc_inv_dep; auto.
+ Qed.
- Definition Fix (x:A) := Acc_iter P F (Rwf x).
+ Definition Fix (x:A) := Fix_F (Rwf x).
(** Proof that [well_founded_induction] satisfies the fixpoint equation.
It requires an extra property of the functional *)
@@ -110,16 +109,7 @@ Section Well_founded.
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.
- Scheme Acc_inv_dep := Induction for Acc Sort Prop.
-
- 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.
+ Lemma Fix_F_inv : forall (x:A) (r s:Acc x), Fix_F r = Fix_F s.
Proof.
intro x; induction (Rwf x); intros.
rewrite <- (Fix_F_eq r); rewrite <- (Fix_F_eq s); intros.
@@ -129,7 +119,7 @@ Section Well_founded.
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)).
+ rewrite <- Fix_F_eq.
apply F_ext; intros.
apply Fix_F_inv.
Qed.
@@ -138,27 +128,29 @@ Section Well_founded.
End Well_founded.
-(** A recursor over pairs *)
+(** Well-founded fixpoints over pairs *)
Section Well_founded_2.
- Variables A B : Set.
+ Variables A B : Type.
Variable R : A * B -> A * B -> Prop.
Variable P : A -> B -> Type.
- Section Acc_iter_2.
+ Section FixPoint_2.
+
Variable
F :
forall (x:A) (x':B),
(forall (y:A) (y':B), R (y, y') (x, x') -> P y y') -> P x x'.
- Fixpoint Acc_iter_2 (x:A) (x':B) (a:Acc R (x, x')) {struct a} :
+ Fixpoint Fix_F_2 (x:A) (x':B) (a:Acc R (x, x')) {struct a} :
P x x' :=
F
(fun (y:A) (y':B) (h:R (y, y') (x, x')) =>
- Acc_iter_2 (x:=y) (x':=y') (Acc_inv a (y, y') h)).
- End Acc_iter_2.
+ Fix_F_2 (x:=y) (x':=y') (Acc_inv a (y,y') h)).
+
+ End FixPoint_2.
Hypothesis Rwf : well_founded R.
@@ -167,9 +159,10 @@ Section Well_founded_2.
(forall (y:A) (y':B), R (y, y') (x, x') -> P y y') -> P x x') ->
forall (a:A) (b:B), P a b.
Proof.
- intros; apply Acc_iter_2; auto.
+ intros; apply Fix_F_2; auto.
Defined.
End Well_founded_2.
-Notation Fix_F := Acc_iter (only parsing). (* compatibility *)
+Notation Acc_iter := Fix_F (only parsing). (* compatibility *)
+Notation Acc_iter_2 := Fix_F_2 (only parsing). (* compatibility *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 06:02:02 +0000