summaryrefslogtreecommitdiff
path: root/theories/Init
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Init')
-rw-r--r--theories/Init/Datatypes.v30
-rw-r--r--theories/Init/Logic.v18
-rw-r--r--theories/Init/Peano.v38
-rw-r--r--theories/Init/Tactics.v46
4 files changed, 93 insertions, 39 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index e5e6fd23..0163c01c 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 11073 2008-06-08 20:24:51Z herbelin $ i*)
+(*i $Id: Datatypes.v 11735 2009-01-02 17:22:31Z herbelin $ i*)
Set Implicit Arguments.
@@ -59,19 +59,39 @@ 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.
+Hint Resolve andb_prop: bool.
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.
+Hint Resolve andb_true_intro: bool.
(** Interpretation of booleans as propositions *)
Inductive eq_true : bool -> Prop := is_eq_true : eq_true true.
+(** Additional rewriting lemmas about [eq_true] *)
+
+Lemma eq_true_ind_r :
+ forall (P : bool -> Prop) (b : bool), P b -> eq_true b -> P true.
+Proof.
+ intros P b H H0; destruct H0 in H; assumption.
+Defined.
+
+Lemma eq_true_rec_r :
+ forall (P : bool -> Set) (b : bool), P b -> eq_true b -> P true.
+Proof.
+ intros P b H H0; destruct H0 in H; assumption.
+Defined.
+
+Lemma eq_true_rect_r :
+ forall (P : bool -> Type) (b : bool), P b -> eq_true b -> P true.
+Proof.
+ intros P b H H0; destruct H0 in H; assumption.
+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;
@@ -95,7 +115,7 @@ Inductive Empty_set : Set :=.
Inductive identity (A:Type) (a:A) : A -> Type :=
refl_identity : identity (A:=A) a a.
-Hint Resolve refl_identity: core v62.
+Hint Resolve refl_identity: core.
Implicit Arguments identity_ind [A].
Implicit Arguments identity_rec [A].
@@ -144,7 +164,7 @@ Section projections.
end.
End projections.
-Hint Resolve pair inl inr: core v62.
+Hint Resolve pair inl inr: core.
Lemma surjective_pairing :
forall (A B:Type) (p:A * B), p = pair (fst p) (snd p).
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 6a636ccc..ae79744f 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 10304 2007-11-08 17:06:32Z emakarov $ i*)
+(*i $Id: Logic.v 11735 2009-01-02 17:22:31Z herbelin $ i*)
Set Implicit Arguments.
@@ -150,6 +150,16 @@ Proof.
intros; tauto.
Qed.
+Lemma iff_and : forall A B : Prop, (A <-> B) -> (A -> B) /\ (B -> A).
+Proof.
+intros A B []; split; trivial.
+Qed.
+
+Lemma iff_to_and : forall A B : Prop, (A <-> B) <-> (A -> B) /\ (B -> 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] *)
@@ -245,8 +255,8 @@ 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 v62.
-Hint Resolve ex_intro ex_intro2: core v62.
+Hint Resolve I conj or_introl or_intror refl_equal: core.
+Hint Resolve ex_intro ex_intro2: core.
Section Logic_lemmas.
@@ -339,7 +349,7 @@ Proof.
destruct 1; destruct 1; destruct 1; destruct 1; destruct 1; reflexivity.
Qed.
-Hint Immediate sym_eq sym_not_eq: core v62.
+Hint Immediate sym_eq sym_not_eq: core.
(** Basic definitions about relations and properties *)
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index 9ef63cc8..43b1f634 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 11115 2008-06-12 16:03:32Z werner $ i*)
+(*i $Id: Peano.v 11735 2009-01-02 17:22:31Z herbelin $ i*)
(** The type [nat] of Peano natural numbers (built from [O] and [S])
is defined in [Datatypes.v] *)
@@ -47,7 +47,7 @@ Hint Resolve (f_equal pred): v62.
Theorem pred_Sn : forall n:nat, n = pred (S n).
Proof.
- simpl; reflexivity.
+ simpl; reflexivity.
Qed.
(** Injectivity of successor *)
@@ -59,13 +59,13 @@ Proof.
rewrite Sn_eq_Sm; trivial.
Qed.
-Hint Immediate eq_add_S: core v62.
+Hint Immediate eq_add_S: core.
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.
+Hint Resolve not_eq_S: core.
Definition IsSucc (n:nat) : Prop :=
match n with
@@ -80,13 +80,13 @@ Proof.
unfold not; intros n H.
inversion H.
Qed.
-Hint Resolve O_S: core v62.
+Hint Resolve O_S: core.
Theorem n_Sn : forall n:nat, n <> S n.
Proof.
induction n; auto.
Qed.
-Hint Resolve n_Sn: core v62.
+Hint Resolve n_Sn: core.
(** Addition *)
@@ -105,7 +105,7 @@ Lemma plus_n_O : forall n:nat, n = n + 0.
Proof.
induction n; simpl in |- *; auto.
Qed.
-Hint Resolve plus_n_O: core v62.
+Hint Resolve plus_n_O: core.
Lemma plus_O_n : forall n:nat, 0 + n = n.
Proof.
@@ -116,7 +116,7 @@ Lemma plus_n_Sm : forall n m:nat, S (n + m) = n + S m.
Proof.
intros n m; induction n; simpl in |- *; auto.
Qed.
-Hint Resolve plus_n_Sm: core v62.
+Hint Resolve plus_n_Sm: core.
Lemma plus_Sn_m : forall n m:nat, S n + m = S (n + m).
Proof.
@@ -138,13 +138,13 @@ Fixpoint mult (n m:nat) {struct n} : nat :=
where "n * m" := (mult n m) : nat_scope.
-Hint Resolve (f_equal2 mult): core v62.
+Hint Resolve (f_equal2 mult): core.
Lemma mult_n_O : forall n:nat, 0 = n * 0.
Proof.
induction n; simpl in |- *; auto.
Qed.
-Hint Resolve mult_n_O: core v62.
+Hint Resolve mult_n_O: core.
Lemma mult_n_Sm : forall n m:nat, n * m + n = n * S m.
Proof.
@@ -152,7 +152,7 @@ Proof.
destruct H; rewrite <- plus_n_Sm; apply (f_equal S).
pattern m at 1 3 in |- *; elim m; simpl in |- *; auto.
Qed.
-Hint Resolve mult_n_Sm: core v62.
+Hint Resolve mult_n_Sm: core.
(** Standard associated names *)
@@ -165,16 +165,12 @@ Fixpoint minus (n m:nat) {struct n} : nat :=
match n, m with
| O, _ => n
| S k, O => n
-(*=======
-
- | O, _ => n
- | S k, O => S k *)
| S k, S l => k - l
end
where "n - m" := (minus n m) : nat_scope.
-(** Definition of the usual orders, the basic properties of [le] and [lt]
+(** Definition of the usual orders, the basic properties of [le] and [lt]
can be found in files Le and Lt *)
Inductive le (n:nat) : nat -> Prop :=
@@ -183,21 +179,21 @@ Inductive le (n:nat) : nat -> Prop :=
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*)
+Hint Constructors le: core.
+(*i equivalent to : "Hints Resolve le_n le_S : core." i*)
Definition lt (n m:nat) := S n <= m.
-Hint Unfold lt: core v62.
+Hint Unfold lt: core.
Infix "<" := lt : nat_scope.
Definition ge (n m:nat) := m <= n.
-Hint Unfold ge: core v62.
+Hint Unfold ge: core.
Infix ">=" := ge : nat_scope.
Definition gt (n m:nat) := m < n.
-Hint Unfold gt: core v62.
+Hint Unfold gt: core.
Infix ">" := gt : nat_scope.
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index 10555fc0..2d7e2159 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Tactics.v 11309 2008-08-06 10:30:35Z herbelin $ i*)
+(*i $Id: Tactics.v 11741 2009-01-03 14:34:39Z herbelin $ i*)
Require Import Notations.
Require Import Logic.
@@ -72,6 +72,17 @@ Ltac false_hyp H G :=
Ltac case_eq x := generalize (refl_equal x); pattern x at -1; case x.
+(* Similar variants of destruct *)
+
+Tactic Notation "destruct_with_eqn" constr(x) :=
+ destruct x as []_eqn.
+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) :=
+ try intros until n; destruct n as []_eqn:H.
+
(* Rewriting in all hypothesis several times everywhere *)
Tactic Notation "rewrite_all" constr(eq) := repeat rewrite eq in *.
@@ -135,14 +146,31 @@ 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.
+(** 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
+ | _ /\ _ => exact H || destruct_hyp H
+ | _ => try solve [inversion H]
+ end
+ with do_intro := let H := fresh in intro H; use_hyp H
+ with destruct_hyp H := case H; clear H; do_intro; do_intro in
+ let rec use_hyps :=
+ match goal with
+ | H : _ /\ _ |- _ => exact H || (destruct_hyp H; use_hyps)
+ | H : _ |- _ => solve [inversion H]
+ | _ => idtac
+ end in
+ let rec do_atom :=
+ solve [reflexivity | symmetry; trivial] ||
+ contradiction ||
+ (split; do_atom)
+ with do_ccl := trivial; 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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 23:13:45 +0000