diff options
| -rw-r--r-- | theories/Init/Logic.v | 119 | ||||
| -rw-r--r-- | theories/NArith/BinNat.v | 5 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZOrder.v | 5 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NBase.v | 4 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NMinus.v | 12 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NPlus.v | 6 | ||||
| -rw-r--r-- | theories/Numbers/NumPrelude.v | 98 |
7 files changed, 134 insertions, 115 deletions
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index f38a651d0..3667c4eb0 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -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. @@ -91,6 +91,65 @@ 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] *) @@ -105,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]. @@ -125,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. @@ -167,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. @@ -224,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. @@ -235,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. @@ -248,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. @@ -263,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. @@ -297,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. @@ -307,7 +366,7 @@ 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. @@ -318,7 +377,7 @@ Qed. (** 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 + 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. @@ -328,8 +387,26 @@ Inductive inhabited (A:Type) : Prop := inhabits : A -> inhabited A. Hint Resolve inhabits: core. -Lemma exists_inhabited : forall (A:Type) (P:A->Prop), +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/NArith/BinNat.v b/theories/NArith/BinNat.v index d2ea7617b..d0ed874dd 100644 --- a/theories/NArith/BinNat.v +++ b/theories/NArith/BinNat.v @@ -99,8 +99,7 @@ Notation Nplus_reg_l := (fun n m p : N => proj1 (plus_cancel_l m p n)) (only par (** Properties of subtraction. *) -Notation Nminus_N0_Nle := - (fun n m : N => (conj (proj2 (le_minus_0 n m)) (proj1 (le_minus_0 n m)))). +Notation Nminus_N0_Nle := minus_0_le (only parsing). Notation Nminus_0_r := minus_0_r (only parsing). Notation Nminus_succ_r := minus_succ_r (only parsing). @@ -117,7 +116,7 @@ Notation Nmult_comm := times_comm (only parsing). Notation Nmult_assoc := times_assoc (only parsing). Notation Nmult_plus_distr_r := times_plus_distr_r (only parsing). Notation Nmult_reg_r := - (fun (n m p : N) (H : p <> N0) => proj1 (times_cancel_r n m p H)). + (fun (n m p : N) (H : p <> N0) => proj1 (times_cancel_r n m p H)) (only parsing). (** Properties of comparison *) diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v index 854542906..4ded2b892 100644 --- a/theories/Numbers/NatInt/NZOrder.v +++ b/theories/Numbers/NatInt/NZOrder.v @@ -116,7 +116,10 @@ Qed. Theorem NZlt_le_succ : forall n m : NZ, n < m <-> S n <= m. Proof. intro n; NZinduct m n. -rewrite_false (n < n) NZlt_irrefl. now rewrite_false (S n <= n) NZnle_succ_l. +setoid_replace (n < n) with False using relation iff by + (apply -> neg_false; apply NZlt_irrefl). +now setoid_replace (S n <= n) with False using relation iff by + (apply -> neg_false; apply NZnle_succ_l). intro m. rewrite NZlt_succ_le. rewrite NZle_succ_le_or_eq_succ. rewrite NZsucc_inj_wd. rewrite (NZle_lt_or_eq n m). rewrite or_cancel_r. diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v index 35d929f0c..d71f98057 100644 --- a/theories/Numbers/Natural/Abstract/NBase.v +++ b/theories/Numbers/Natural/Abstract/NBase.v @@ -163,7 +163,9 @@ Proof. cases n. rewrite pred_0. setoid_replace (0 == 1) with False using relation iff. tauto. split; intro H; [symmetry in H; false_hyp H neq_succ_0 | elim H]. -intro n. rewrite pred_succ. rewrite_false (S n == 0) neq_succ_0. +intro n. rewrite pred_succ. +setoid_replace (S n == 0) with False using relation iff by + (apply -> neg_false; apply neq_succ_0). rewrite succ_inj_wd. tauto. Qed. diff --git a/theories/Numbers/Natural/Abstract/NMinus.v b/theories/Numbers/Natural/Abstract/NMinus.v index f7abb82d8..c109ff904 100644 --- a/theories/Numbers/Natural/Abstract/NMinus.v +++ b/theories/Numbers/Natural/Abstract/NMinus.v @@ -99,7 +99,7 @@ intros n m p H; rewrite plus_comm in H; now apply plus_minus_eq_l. Qed. (* This could be proved by adding m to both sides. Then the proof would -use plus_minus_assoc and le_minus_0, which is proven below. *) +use plus_minus_assoc and minus_0_le, which is proven below. *) Theorem plus_minus_eq_nz : forall n m p : N, p ~= 0 -> n - m == p -> m + p == n. Proof. intros n m p H; double_induct n m. @@ -134,12 +134,12 @@ intros m IH. rewrite minus_succ_r. apply le_trans with (n - m); [apply le_pred_l | assumption]. Qed. -Theorem le_minus_0 : forall n m : N, n <= m <-> n - m == 0. +Theorem minus_0_le : forall n m : N, n - m == 0 <-> n <= m. Proof. double_induct n m. -intro m; split; intro; [apply minus_0_l | apply le_0_l]. +intro m; split; intro; [apply le_0_l | apply minus_0_l]. intro m; rewrite minus_0_r; split; intro H; -[false_hyp H nle_succ_0 | false_hyp H neq_succ_0]. +[false_hyp H neq_succ_0 | false_hyp H nle_succ_0]. intros n m H. rewrite <- succ_le_mono. now rewrite minus_succ. Qed. @@ -164,8 +164,8 @@ rewrite (plus_comm ((n - m) * p) p), (plus_comm (n * p) p). rewrite <- (plus_minus_assoc p (n * p) (m * p)); [now apply times_le_mono_r |]. now apply <- plus_cancel_l. assert (H1 : S n <= m); [now apply -> lt_le_succ |]. -setoid_replace (S n - m) with 0 by now apply -> le_minus_0. -setoid_replace ((S n * p) - m * p) with 0 by (apply -> le_minus_0; now apply times_le_mono_r). +setoid_replace (S n - m) with 0 by now apply <- minus_0_le. +setoid_replace ((S n * p) - m * p) with 0 by (apply <- minus_0_le; now apply times_le_mono_r). apply times_0_l. Qed. diff --git a/theories/Numbers/Natural/Abstract/NPlus.v b/theories/Numbers/Natural/Abstract/NPlus.v index 32912a73d..a033d95a0 100644 --- a/theories/Numbers/Natural/Abstract/NPlus.v +++ b/theories/Numbers/Natural/Abstract/NPlus.v @@ -67,8 +67,10 @@ intros n m; induct n. (* The next command does not work with the axiom plus_0_l from NPlusSig *) rewrite plus_0_l. intuition reflexivity. intros n IH. rewrite plus_succ_l. -rewrite_false (S (n + m) == 0) neq_succ_0. -rewrite_false (S n == 0) neq_succ_0. tauto. +setoid_replace (S (n + m) == 0) with False using relation iff by + (apply -> neg_false; apply neq_succ_0). +setoid_replace (S n == 0) with False using relation iff by + (apply -> neg_false; apply neq_succ_0). tauto. Qed. Theorem plus_eq_succ : diff --git a/theories/Numbers/NumPrelude.v b/theories/Numbers/NumPrelude.v index 663395389..e66bc8ebf 100644 --- a/theories/Numbers/NumPrelude.v +++ b/theories/Numbers/NumPrelude.v @@ -11,7 +11,7 @@ (*i i*) Require Export Setoid. -Require Export Bool. +(*Require Export Bool.*) (* Standard library. Export, not Import, because if a file importing the current file wants to use. e.g., Theorem eq_true_or : forall b1 b2 : bool, b1 || b2 <-> b1 \/ b2, @@ -31,13 +31,13 @@ Contents: (** Coercion from bool to Prop *) -Definition eq_bool := (@eq bool). +(*Definition eq_bool := (@eq bool).*) (*Inductive eq_true : bool -> Prop := is_eq_true : eq_true true.*) (* This has been added to theories/Datatypes.v *) -Coercion eq_true : bool >-> Sortclass. +(*Coercion eq_true : bool >-> Sortclass.*) -Theorem eq_true_unfold_pos : forall b : bool, b <-> b = true. +(*Theorem eq_true_unfold_pos : forall b : bool, b <-> b = true. Proof. intro b; split; intro H. now inversion H. now rewrite H. Qed. @@ -72,7 +72,7 @@ now rewrite H. destruct b1; destruct b2; simpl; try reflexivity. apply -> eq_true_unfold_neg. rewrite H. now intro. symmetry; apply -> eq_true_unfold_neg. rewrite <- H; now intro. -Qed. +Qed.*) (** Extension of the tactics stepl and stepr to make them applicable to hypotheses *) @@ -161,6 +161,9 @@ split; intros H1 a; induction (H1 a) as [x H2 H3]; constructor; intros y H4; apply H3; [now apply <- H | now apply -> H]. Qed. +(* solve_predicate_wd solves the goal [predicate_wd P] for P consisting of +morhisms and quatifiers *) + Ltac solve_predicate_wd := unfold predicate_wd; let x := fresh "x" in @@ -168,6 +171,9 @@ let y := fresh "y" in let H := fresh "H" in intros x y H; qiff x y H. +(* solve_relation_wd solves the goal [relation_wd R] for R consisting of +morhisms and quatifiers *) + Ltac solve_relation_wd := unfold relation_wd, fun2_wd; let x1 := fresh "x" in @@ -179,6 +185,7 @@ let H2 := fresh "H" in intros x1 y1 H1 x2 y2 H2; qsetoid_rewrite H1; qiff x2 y2 H2. + (* The tactic solve_relation_wd is not very efficient because qsetoid_rewrite uses qiff to take the formula apart in order to make it quantifier-free, and then qiff is called again and takes the formula apart for the second @@ -191,6 +198,7 @@ We declare it to take the tactic that applies the induction theorem and not the induction theorem itself because the tactic may, for example, supply additional arguments, as does NZinduct_center in NZBase.v *) + Ltac induction_maker n t := try intros until n; pattern n; t; clear n; @@ -244,77 +252,7 @@ Implicit Arguments prod_rel_equiv [A B]. (** Miscellaneous *) -Theorem neg_false : forall P : Prop, ~ P <-> (P <-> False). -Proof. -intro P; unfold not; split; intro H; [split; intro H1; -[apply H; assumption | elim H1] | apply (proj1 H)]. -Qed. - -(* This tactic replaces P in the goal with False. -The goal ~ P should be solvable by "apply H". *) -Ltac rewrite_false P H := -setoid_replace P with False using relation iff; -[| apply -> neg_false; apply H]. - -Ltac rewrite_true P H := -setoid_replace P with True using relation iff; -[| split; intro; [constructor | apply H]]. - -(*Ltac symmetry Eq := -lazymatch Eq with -| ?E ?t1 ?t2 => setoid_replace (E t1 t2) with (E t2 t1) using relation iff; - [| split; intro; symmetry; assumption] -| _ => fail Eq "does not have the form (E t1 t2)" -end.*) -(* This does not work because there already is a tactic "symmetry". -Declaring "symmetry" a tactic notation does not work because it conflicts -with "symmetry in": it thinks that "in" is a term. *) - -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. - -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. - -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. - -Definition comp_bool (x y : comparison) : bool := +(*Definition comp_bool (x y : comparison) : bool := match x, y with | Lt, Lt => true | Eq, Eq => true @@ -326,13 +264,11 @@ Theorem comp_bool_correct : forall x y : comparison, comp_bool x y <-> x = y. Proof. destruct x; destruct y; simpl; split; now intro. -Qed. - -Definition LE_Set : forall A : Set, relation A := (@eq). +Qed.*) -Lemma eq_equiv : forall A : Set, equiv A (@LE_Set A). +Lemma eq_equiv : forall A : Set, equiv A (@eq A). Proof. -intro A; unfold equiv, LE_Set, reflexive, symmetric, transitive. +intro A; unfold equiv, reflexive, symmetric, transitive. repeat split; [exact (@trans_eq A) | exact (@sym_eq A)]. (* It is interesting how the tactic split proves reflexivity *) Qed. |