summaryrefslogtreecommitdiff
path: root/theories/Init
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Init')
-rw-r--r--theories/Init/Datatypes.v101
-rw-r--r--theories/Init/Logic.v63
-rw-r--r--theories/Init/Logic_Type.v25
-rw-r--r--theories/Init/Notations.v2
-rw-r--r--theories/Init/Peano.v11
-rw-r--r--theories/Init/Prelude.v11
-rw-r--r--theories/Init/Specif.v59
-rw-r--r--theories/Init/Tactics.v85
-rw-r--r--theories/Init/Wf.v17
-rw-r--r--theories/Init/vo.itarget9
10 files changed, 284 insertions, 99 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 0163c01c..6040f58b 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -6,12 +6,14 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Datatypes.v 11735 2009-01-02 17:22:31Z herbelin $ i*)
+(*i $Id$ i*)
Set Implicit Arguments.
Require Import Notations.
Require Import Logic.
+Declare ML Module "nat_syntax_plugin".
+
(** [unit] is a singleton datatype with sole inhabitant [tt] *)
@@ -72,6 +74,16 @@ Hint Resolve andb_true_intro: bool.
Inductive eq_true : bool -> Prop := is_eq_true : eq_true true.
+Hint Constructors eq_true : eq_true.
+
+(** Another way of interpreting booleans as propositions *)
+
+Definition is_true b := b = true.
+
+(** [is_true] can be activated as a coercion by
+ (Local) Coercion is_true : bool >-> Prop.
+*)
+
(** Additional rewriting lemmas about [eq_true] *)
Lemma eq_true_ind_r :
@@ -94,7 +106,7 @@ Defined.
(** [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;
+ Numbers in [nat] can be denoted using a decimal notation;
e.g. [3%nat] abbreviates [S (S (S O))] *)
Inductive nat : Set :=
@@ -114,8 +126,8 @@ Inductive Empty_set : Set :=.
sole inhabitant is denoted [refl_identity A a] *)
Inductive identity (A:Type) (a:A) : A -> Type :=
- refl_identity : identity (A:=A) a a.
-Hint Resolve refl_identity: core.
+ identity_refl : identity a a.
+Hint Resolve identity_refl: core.
Implicit Arguments identity_ind [A].
Implicit Arguments identity_rec [A].
@@ -162,7 +174,7 @@ Section projections.
Definition snd (p:A * B) := match p with
| (x, y) => y
end.
-End projections.
+End projections.
Hint Resolve pair inl inr: core.
@@ -177,13 +189,13 @@ Lemma injective_projections :
fst p1 = fst p2 -> snd p1 = snd p2 -> p1 = p2.
Proof.
destruct p1; destruct p2; simpl in |- *; intros Hfst Hsnd.
- rewrite Hfst; rewrite Hsnd; reflexivity.
+ rewrite Hfst; rewrite Hsnd; reflexivity.
Qed.
-Definition prod_uncurry (A B C:Type) (f:prod A B -> C)
+Definition prod_uncurry (A B C:Type) (f:prod A B -> C)
(x:A) (y:B) : C := f (pair x y).
-Definition prod_curry (A B C:Type) (f:A -> B -> C)
+Definition prod_curry (A B C:Type) (f:A -> B -> C)
(p:prod A B) : C := match p with
| pair x y => f x y
end.
@@ -202,11 +214,84 @@ Definition CompOpp (r:comparison) :=
| Gt => Lt
end.
+Lemma CompOpp_involutive : forall c, CompOpp (CompOpp c) = c.
+Proof.
+ destruct c; reflexivity.
+Qed.
+
+Lemma CompOpp_inj : forall c c', CompOpp c = CompOpp c' -> c = c'.
+Proof.
+ destruct c; destruct c'; auto; discriminate.
+Qed.
+
+Lemma CompOpp_iff : forall c c', CompOpp c = c' <-> c = CompOpp c'.
+Proof.
+ split; intros; apply CompOpp_inj; rewrite CompOpp_involutive; auto.
+Qed.
+
+(** The [CompSpec] inductive will be used to relate a [compare] function
+ (returning a comparison answer) and some equality and order predicates.
+ Interest: [CompSpec] behave nicely with [case] and [destruct]. *)
+
+Inductive CompSpec {A} (eq lt : A->A->Prop)(x y:A) : comparison -> Prop :=
+ | CompEq : eq x y -> CompSpec eq lt x y Eq
+ | CompLt : lt x y -> CompSpec eq lt x y Lt
+ | CompGt : lt y x -> CompSpec eq lt x y Gt.
+Hint Constructors CompSpec.
+
+(** For having clean interfaces after extraction, [CompSpec] is declared
+ in Prop. For some situations, it is nonetheless useful to have a
+ version in Type. Interestingly, these two versions are equivalent.
+*)
+
+Inductive CompSpecT {A} (eq lt : A->A->Prop)(x y:A) : comparison -> Type :=
+ | CompEqT : eq x y -> CompSpecT eq lt x y Eq
+ | CompLtT : lt x y -> CompSpecT eq lt x y Lt
+ | CompGtT : lt y x -> CompSpecT eq lt x y Gt.
+Hint Constructors CompSpecT.
+
+Lemma CompSpec2Type : forall A (eq lt:A->A->Prop) x y c,
+ CompSpec eq lt x y c -> CompSpecT eq lt x y c.
+Proof.
+ destruct c; intros H; constructor; inversion_clear H; auto.
+Defined.
+
(** Identity *)
Definition ID := forall A:Type, A -> A.
Definition id : ID := fun A x => x.
+(** Polymorphic lists and some operations *)
+
+Inductive list (A : Type) : Type :=
+ | nil : list A
+ | cons : A -> list A -> list A.
+
+Implicit Arguments nil [A].
+Infix "::" := cons (at level 60, right associativity) : list_scope.
+Delimit Scope list_scope with list.
+Bind Scope list_scope with list.
+
+Local Open Scope list_scope.
+
+Definition length (A : Type) : list A -> nat :=
+ fix length l :=
+ match l with
+ | nil => O
+ | _ :: l' => S (length l')
+ end.
+
+(** Concatenation of two lists *)
+
+Definition app (A : Type) : list A -> list A -> list A :=
+ fix app l m :=
+ match l with
+ | nil => m
+ | a :: l1 => a :: app l1 m
+ end.
+
+Infix "++" := app (right associativity, at level 60) : list_scope.
+
(* begin hide *)
(* Compatibility *)
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index ae79744f..4fca1d1d 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 11735 2009-01-02 17:22:31Z herbelin $ i*)
+(*i $Id$ i*)
Set Implicit Arguments.
@@ -112,6 +112,16 @@ Proof.
intros; tauto.
Qed.
+Theorem and_comm : forall A B : Prop, A /\ B <-> B /\ A.
+Proof.
+intros; tauto.
+Qed.
+
+Theorem and_assoc : forall A B C : Prop, (A /\ B) /\ 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.
@@ -124,6 +134,16 @@ Proof.
intros; tauto.
Qed.
+Theorem or_comm : forall A B : Prop, (A \/ B) <-> (B \/ A).
+Proof.
+intros; tauto.
+Qed.
+
+Theorem or_assoc : forall A B C : Prop, (A \/ B) \/ 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,
@@ -243,7 +263,7 @@ End universal_quantification.
[A] which is true of [x] is also true of [y] *)
Inductive eq (A:Type) (x:A) : A -> Prop :=
- refl_equal : x = x :>A
+ eq_refl : x = x :>A
where "x = y :> A" := (@eq A x y) : type_scope.
@@ -251,11 +271,13 @@ Notation "x = y" := (x = y :>_) : type_scope.
Notation "x <> y :> T" := (~ x = y :>T) : type_scope.
Notation "x <> y" := (x <> y :>_) : type_scope.
+Implicit Arguments eq [ [A] ].
+
Implicit Arguments eq_ind [A].
Implicit Arguments eq_rec [A].
Implicit Arguments eq_rect [A].
-Hint Resolve I conj or_introl or_intror refl_equal: core.
+Hint Resolve I conj or_introl or_intror eq_refl: core.
Hint Resolve ex_intro ex_intro2: core.
Section Logic_lemmas.
@@ -271,17 +293,17 @@ Section Logic_lemmas.
Variable f : A -> B.
Variables x y z : A.
- Theorem sym_eq : x = y -> y = x.
+ Theorem eq_sym : x = y -> y = x.
Proof.
destruct 1; trivial.
Defined.
- Opaque sym_eq.
+ Opaque eq_sym.
- Theorem trans_eq : x = y -> y = z -> x = z.
+ Theorem eq_trans : x = y -> y = z -> x = z.
Proof.
destruct 2; trivial.
Defined.
- Opaque trans_eq.
+ Opaque eq_trans.
Theorem f_equal : x = y -> f x = f y.
Proof.
@@ -289,30 +311,26 @@ Section Logic_lemmas.
Defined.
Opaque f_equal.
- Theorem sym_not_eq : x <> y -> y <> x.
+ Theorem not_eq_sym : x <> y -> y <> x.
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.
-
End equality.
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.
+ intros A x P H y H0; elim eq_sym 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.
+ intros A x P H y H0; elim eq_sym 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.
+ intros A x P H y H0; elim eq_sym with (1 := H0); assumption.
Defined.
End Logic_lemmas.
@@ -349,7 +367,18 @@ Proof.
destruct 1; destruct 1; destruct 1; destruct 1; destruct 1; reflexivity.
Qed.
-Hint Immediate sym_eq sym_not_eq: core.
+(* Aliases *)
+
+Notation sym_eq := eq_sym (only parsing).
+Notation trans_eq := eq_trans (only parsing).
+Notation sym_not_eq := not_eq_sym (only parsing).
+
+Notation refl_equal := eq_refl (only parsing).
+Notation sym_equal := eq_sym (only parsing).
+Notation trans_equal := eq_trans (only parsing).
+Notation sym_not_equal := not_eq_sym (only parsing).
+
+Hint Immediate eq_sym not_eq_sym: core.
(** Basic definitions about relations and properties *)
@@ -411,7 +440,7 @@ intros A x y z H1 H2. rewrite <- H2; exact H1.
Qed.
Declare Left Step eq_stepl.
-Declare Right Step trans_eq.
+Declare Right Step eq_trans.
Lemma iff_stepl : forall A B C : Prop, (A <-> B) -> (A <-> C) -> (C <-> B).
Proof.
diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v
index c4e5f6c7..1333f354 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 10840 2008-04-23 21:29:34Z herbelin $ i*)
+(*i $Id$ i*)
(** This module defines type constructors for types in [Type]
([Datatypes.v] and [Logic.v] defined them for types in [Set]) *)
@@ -28,23 +28,23 @@ Section identity_is_a_congruence.
Variable f : A -> B.
Variables x y z : A.
-
- Lemma sym_id : identity x y -> identity y x.
+
+ Lemma identity_sym : identity x y -> identity y x.
Proof.
destruct 1; trivial.
Defined.
- Lemma trans_id : identity x y -> identity y z -> identity x z.
+ Lemma identity_trans : identity x y -> identity y z -> identity x z.
Proof.
destruct 2; trivial.
Defined.
- Lemma congr_id : identity x y -> identity (f x) (f y).
+ Lemma identity_congr : identity x y -> identity (f x) (f y).
Proof.
destruct 1; trivial.
Defined.
- Lemma sym_not_id : notT (identity x y) -> notT (identity y x).
+ Lemma not_identity_sym : notT (identity x y) -> notT (identity y x).
Proof.
red in |- *; intros H H'; apply H; destruct H'; trivial.
Qed.
@@ -53,17 +53,22 @@ End identity_is_a_congruence.
Definition identity_ind_r :
forall (A:Type) (a:A) (P:A -> Prop), P a -> forall y:A, identity y a -> P y.
- intros A x P H y H0; case sym_id with (1 := H0); trivial.
+ intros A x P H y H0; case identity_sym with (1 := H0); trivial.
Defined.
Definition identity_rec_r :
forall (A:Type) (a:A) (P:A -> Set), P a -> forall y:A, identity y a -> P y.
- intros A x P H y H0; case sym_id with (1 := H0); trivial.
+ intros A x P H y H0; case identity_sym with (1 := H0); trivial.
Defined.
Definition identity_rect_r :
forall (A:Type) (a:A) (P:A -> Type), P a -> forall y:A, identity y a -> P y.
- intros A x P H y H0; case sym_id with (1 := H0); trivial.
+ intros A x P H y H0; case identity_sym with (1 := H0); trivial.
Defined.
-Hint Immediate sym_id sym_not_id: core v62.
+Hint Immediate identity_sym not_identity_sym: core v62.
+
+Notation refl_id := identity_refl (only parsing).
+Notation sym_id := identity_sym (only parsing).
+Notation trans_id := identity_trans (only parsing).
+Notation sym_not_id := not_identity_sym (only parsing).
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index 5f18edcd..0c628298 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 12271 2009-08-11 10:29:45Z herbelin $ i*)
+(*i $Id$ i*)
(** These are the notations whose level and associativity are imposed by Coq *)
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index 43b1f634..12a8f7a4 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 11735 2009-01-02 17:22:31Z herbelin $ i*)
+(*i $Id$ i*)
(** The type [nat] of Peano natural numbers (built from [O] and [S])
is defined in [Datatypes.v] *)
@@ -77,8 +77,7 @@ Definition IsSucc (n:nat) : Prop :=
Theorem O_S : forall n:nat, 0 <> S n.
Proof.
- unfold not; intros n H.
- inversion H.
+ discriminate.
Qed.
Hint Resolve O_S: core.
@@ -90,7 +89,7 @@ Hint Resolve n_Sn: core.
(** Addition *)
-Fixpoint plus (n m:nat) {struct n} : nat :=
+Fixpoint plus (n m:nat) : nat :=
match n with
| O => m
| S p => S (p + m)
@@ -130,7 +129,7 @@ Notation plus_succ_r_reverse := plus_n_Sm (only parsing).
(** Multiplication *)
-Fixpoint mult (n m:nat) {struct n} : nat :=
+Fixpoint mult (n m:nat) : nat :=
match n with
| O => 0
| S p => m + p * m
@@ -161,7 +160,7 @@ 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 :=
+Fixpoint minus (n m:nat) : nat :=
match n, m with
| O, _ => n
| S k, O => n
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index 6492c948..685c7247 100644
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Prelude.v 10064 2007-08-08 15:32:36Z msozeau $ i*)
+(*i $Id$ i*)
Require Export Notations.
Require Export Logic.
@@ -15,3 +15,12 @@ Require Export Specif.
Require Export Peano.
Require Export Coq.Init.Wf.
Require Export Coq.Init.Tactics.
+(* Initially available plugins
+ (+ nat_syntax_plugin loaded in Datatypes) *)
+Declare ML Module "extraction_plugin".
+Declare ML Module "cc_plugin".
+Declare ML Module "ground_plugin".
+Declare ML Module "dp_plugin".
+Declare ML Module "recdef_plugin".
+Declare ML Module "subtac_plugin".
+Declare ML Module "xml_plugin".
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index c0f5c42a..7141f26c 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 10923 2008-05-12 18:25:06Z herbelin $ i*)
+(*i $Id$ i*)
(** Basic specifications : sets that may contain logical information *)
@@ -18,9 +18,9 @@ Require Import Logic.
(** 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 type [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 type [A] which satisfy both [P] and [Q]. *)
Inductive sig (A:Type) (P:A -> Prop) : Type :=
@@ -29,7 +29,7 @@ Inductive sig (A:Type) (P:A -> Prop) : Type :=
Inductive sig2 (A:Type) (P Q:A -> Prop) : Type :=
exist2 : forall x:A, P x -> Q x -> sig2 P Q.
-(** [(sigT A P)], or more suggestively [{x:A & (P x)}] is a Sigma-type.
+(** [(sigT A P)], or more suggestively [{x:A & (P x)}] is a Sigma-type.
Similarly for [(sigT2 A P Q)], also written [{x:A & (P x) & (Q x)}]. *)
Inductive sigT (A:Type) (P:A -> Type) : Type :=
@@ -123,7 +123,7 @@ Coercion sig_of_sigT : sigT >-> sig.
Inductive sumbool (A B:Prop) : Set :=
| left : A -> {A} + {B}
- | right : B -> {A} + {B}
+ | right : B -> {A} + {B}
where "{ A } + { B }" := (sumbool A B) : type_scope.
Add Printing If sumbool.
@@ -133,7 +133,7 @@ Add Printing If sumbool.
Inductive sumor (A:Type) (B:Prop) : Type :=
| inleft : A -> A + {B}
- | inright : B -> A + {B}
+ | inright : B -> A + {B}
where "A + { B }" := (sumor A B) : type_scope.
Add Printing If sumor.
@@ -148,50 +148,57 @@ Section Choice_lemmas.
Variables R1 R2 : S -> Prop.
Lemma Choice :
- (forall x:S, sig (fun y:S' => R x y)) ->
- sig (fun f:S -> S' => forall z:S, R z (f z)).
+ (forall x:S, {y:S' | R x y}) -> {f:S -> S' | forall z:S, R z (f z)}.
Proof.
intro H.
- exists (fun z:S => match H z with
- | exist y _ => y
- end).
+ exists (fun z => proj1_sig (H z)).
intro z; destruct (H z); trivial.
Qed.
Lemma Choice2 :
- (forall x:S, sigT (fun y:S' => R' x y)) ->
- sigT (fun f:S -> S' => forall z:S, R' z (f z)).
+ (forall x:S, {y:S' & R' x y}) -> {f:S -> S' & forall z:S, R' z (f z)}.
Proof.
intro H.
- exists (fun z:S => match H z with
- | existT y _ => y
- end).
+ exists (fun z => projT1 (H z)).
intro z; destruct (H z); trivial.
Qed.
Lemma bool_choice :
(forall x:S, {R1 x} + {R2 x}) ->
- sig
- (fun f:S -> bool =>
- forall x:S, f x = true /\ R1 x \/ f x = false /\ R2 x).
+ {f:S -> bool | forall x:S, f x = true /\ R1 x \/ f x = false /\ R2 x}.
Proof.
intro H.
- exists
- (fun z:S => match H z with
- | left _ => true
- | right _ => false
- end).
+ exists (fun z:S => if H z then true else false).
intro z; destruct (H z); auto.
Qed.
End Choice_lemmas.
- (** A result of type [(Exc A)] is either a normal value of type [A] or
+Section Dependent_choice_lemmas.
+
+ Variables X : Set.
+ Variable R : X -> X -> Prop.
+
+ Lemma dependent_choice :
+ (forall x:X, {y | R x y}) ->
+ forall x0, {f : nat -> X | f O = x0 /\ forall n, R (f n) (f (S n))}.
+ Proof.
+ intros H x0.
+ set (f:=fix f n := match n with O => x0 | S n' => proj1_sig (H (f n')) end).
+ exists f.
+ split. reflexivity.
+ induction n; simpl; apply proj2_sig.
+ Qed.
+
+End Dependent_choice_lemmas.
+
+
+ (** A result of type [(Exc A)] is either a normal value of type [A] or
an [error] :
[Inductive Exc [A:Type] : Type := value : A->(Exc A) | error : (Exc A)].
- It is implemented using the option type. *)
+ It is implemented using the option type. *)
Definition Exc := option.
Definition value := Some.
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index 48b4568d..3e860fd4 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -6,45 +6,52 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Tactics.v 13198 2010-06-25 22:36:20Z letouzey $ i*)
+(*i $Id$ i*)
Require Import Notations.
Require Import Logic.
+Require Import Specif.
(** * Useful tactics *)
-(** A tactic for proof by contradiction. With contradict H,
+(** Ex falso quodlibet : a tactic for proving False instead of the current goal.
+ This is just a nicer name for tactics such as [elimtype False]
+ and other [cut False]. *)
+
+Ltac exfalso := elimtype False.
+
+(** 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,
+ 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
+ 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))
+ let pospos H :=
+ let A := type of H in (exfalso; revert H; try fold (~A))
in
let posneg H := save pospos H
- in
- let neg H := match goal with
+ in
+ let neg H := match goal with
| |- (~_) => negneg H
| |- (_->False) => negneg H
| |- _ => negpos H
- end in
- let pos H := match goal with
+ end in
+ let pos H := match goal with
| |- (~_) => posneg H
| |- (_->False) => posneg H
| |- _ => pospos H
end in
- match type of H with
+ match type of H with
| (~_) => neg H
| (_->False) => neg H
| _ => (elim H;fail) || pos H
@@ -52,20 +59,20 @@ Ltac contradict H :=
(* Transforming a negative goal [ H:~A |- ~B ] into a positive one [ B |- A ]*)
-Ltac swap H :=
+Ltac swap H :=
idtac "swap is OBSOLETE: use contradict instead.";
intro; apply H; clear H.
(* To contradict an hypothesis without copying its type. *)
-Ltac absurd_hyp H :=
+Ltac absurd_hyp H :=
idtac "absurd_hyp is OBSOLETE: use contradict instead.";
- let T := type of H in
+ let T := type of H in
absurd T.
(* A useful complement to contradict. Here H:A while G allows to conclude ~A *)
-Ltac false_hyp H G :=
+Ltac false_hyp H G :=
let T := type of H in absurd T; [ apply G | assumption ].
(* A case with no loss of information. *)
@@ -76,13 +83,21 @@ Ltac case_eq x := generalize (refl_equal x); pattern x at -1; case x.
Tactic Notation "destruct_with_eqn" constr(x) :=
destruct x as []_eqn.
-Tactic Notation "destruct_with_eqn" ident(n) :=
+Tactic Notation "destruct_with_eqn" ident(n) :=
try intros until n; destruct n as []_eqn.
Tactic Notation "destruct_with_eqn" ":" ident(H) constr(x) :=
destruct x as []_eqn:H.
-Tactic Notation "destruct_with_eqn" ":" ident(H) ident(n) :=
+Tactic Notation "destruct_with_eqn" ":" ident(H) ident(n) :=
try intros until n; destruct n as []_eqn:H.
+(** Break every hypothesis of a certain type *)
+
+Ltac destruct_all t :=
+ match goal with
+ | x : t |- _ => destruct x; destruct_all t
+ | _ => idtac
+ end.
+
(* Rewriting in all hypothesis several times everywhere *)
Tactic Notation "rewrite_all" constr(eq) := repeat rewrite eq in *.
@@ -148,7 +163,7 @@ bapply lemma ltac:(fun H => destruct H as [_ H]; apply H in J).
(** An experimental tactic simpler than auto that is useful for ending
proofs "in one step" *)
-
+
Ltac easy :=
let rec use_hyp H :=
match type of H with
@@ -167,14 +182,42 @@ Ltac easy :=
solve [reflexivity | symmetry; trivial] ||
contradiction ||
(split; do_atom)
- with do_ccl := trivial; repeat do_intro; do_atom in
+ with do_ccl := trivial with eq_true; repeat do_intro; do_atom in
(use_hyps; do_ccl) || fail "Cannot solve this goal".
Tactic Notation "now" tactic(t) := t; easy.
(** A tactic to document or check what is proved at some point of a script *)
+
Ltac now_show c := change c.
+(** Support for rewriting decidability statements *)
+
+Set Implicit Arguments.
+
+Lemma decide_left : forall (C:Prop) (decide:{C}+{~C}),
+ C -> forall P:{C}+{~C}->Prop, (forall H:C, P (left _ H)) -> P decide.
+Proof.
+intros; destruct decide. apply H0. contradiction.
+Qed.
+
+Lemma decide_right : forall (C:Prop) (decide:{C}+{~C}),
+ ~C -> forall P:{C}+{~C}->Prop, (forall H:~C, P (right _ H)) -> P decide.
+Proof.
+intros; destruct decide. contradiction. apply H0.
+Qed.
+
+Tactic Notation "decide" constr(lemma) "with" constr(H) :=
+ let try_to_merge_hyps H :=
+ try (clear H; intro H) ||
+ (let H' := fresh H "bis" in intro H'; try clear H') ||
+ (let H' := fresh in intro H'; try clear H') in
+ match type of H with
+ | ~ ?C => apply (decide_right lemma H); try_to_merge_hyps H
+ | ?C -> False => apply (decide_right lemma H); try_to_merge_hyps H
+ | _ => apply (decide_left lemma H); try_to_merge_hyps H
+ end.
+
(** Clear an hypothesis and its dependencies *)
Tactic Notation "clear" "dependent" hyp(h) :=
diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v
index d3f8f1ab..3209860f 100644
--- a/theories/Init/Wf.v
+++ b/theories/Init/Wf.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Wf.v 11251 2008-07-24 08:28:40Z herbelin $ i*)
+(*i $Id$ i*)
(** * This module proves the validity of
- well-founded recursion (also known as course of values)
@@ -65,14 +65,14 @@ Section Well_founded.
exact (fun P:A -> Prop => well_founded_induction_type P).
Defined.
-(** Well-founded 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.
- Fixpoint Fix_F (x:A) (a:Acc x) {struct a} : P x :=
+ Fixpoint Fix_F (x:A) (a:Acc x) : 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.
@@ -80,13 +80,13 @@ Section Well_founded.
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.
+ Proof.
destruct r using Acc_inv_dep; auto.
Qed.
Definition Fix (x:A) := Fix_F (Rwf x).
- (** Proof that [well_founded_induction] satisfies the fixpoint equation.
+ (** Proof that [well_founded_induction] satisfies the fixpoint equation.
It requires an extra property of the functional *)
Hypothesis
@@ -111,7 +111,7 @@ Section Well_founded.
End FixPoint.
-End Well_founded.
+End Well_founded.
(** Well-founded fixpoints over pairs *)
@@ -120,7 +120,7 @@ Section Well_founded_2.
Variables A B : Type.
Variable R : A * B -> A * B -> Prop.
- Variable P : A -> B -> Type.
+ Variable P : A -> B -> Type.
Section FixPoint_2.
@@ -129,8 +129,7 @@ Section Well_founded_2.
forall (x:A) (x':B),
(forall (y:A) (y':B), R (y, y') (x, x') -> P y y') -> P x x'.
- Fixpoint Fix_F_2 (x:A) (x':B) (a:Acc R (x, x')) {struct a} :
- P x x' :=
+ Fixpoint Fix_F_2 (x:A) (x':B) (a:Acc R (x, x')) : P x x' :=
F
(fun (y:A) (y':B) (h:R (y, y') (x, x')) =>
Fix_F_2 (x:=y) (x':=y') (Acc_inv a (y,y') h)).
diff --git a/theories/Init/vo.itarget b/theories/Init/vo.itarget
new file mode 100644
index 00000000..f53d55e7
--- /dev/null
+++ b/theories/Init/vo.itarget
@@ -0,0 +1,9 @@
+Datatypes.vo
+Logic_Type.vo
+Logic.vo
+Notations.vo
+Peano.vo
+Prelude.vo
+Specif.vo
+Tactics.vo
+Wf.vo
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 21:09:21 +0000