diff options
-rw-r--r-- | theories/Numbers/Integer/Abstract/ZOrder.v | 103 | ||||
-rw-r--r-- | theories/Numbers/NatInt/NZOrder.v | 107 | ||||
-rw-r--r-- | theories/Numbers/Natural/Abstract/NAxioms.v | 4 | ||||
-rw-r--r-- | theories/Numbers/Natural/Abstract/NBase.v | 10 | ||||
-rw-r--r-- | theories/Numbers/Natural/Abstract/NIso.v | 2 | ||||
-rw-r--r-- | theories/Numbers/Natural/Abstract/NMinus.v | 2 | ||||
-rw-r--r-- | theories/Numbers/Natural/Abstract/NOrder.v | 91 | ||||
-rw-r--r-- | theories/Numbers/Natural/Binary/NBinary.v | 4 | ||||
-rw-r--r-- | theories/Numbers/Natural/Peano/NPeano.v | 6 | ||||
-rw-r--r-- | theories/Numbers/NumPrelude.v | 60 | ||||
-rw-r--r-- | theories/Numbers/QRewrite.v | 5 |
11 files changed, 279 insertions, 115 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZOrder.v b/theories/Numbers/Integer/Abstract/ZOrder.v index 7eed9a8ee..322d36cd3 100644 --- a/theories/Numbers/Integer/Abstract/ZOrder.v +++ b/theories/Numbers/Integer/Abstract/ZOrder.v @@ -153,34 +153,35 @@ Theorem Zleft_induction : forall n : Z, n <= z -> A n. Proof NZleft_induction. -Theorem Zorder_induction : +Theorem Zright_induction' : forall A : Z -> Prop, predicate_wd Zeq A -> - forall z : Z, A z -> + forall z : Z, + (forall n : Z, n <= z -> A n) -> (forall n : Z, z <= n -> A n -> A (S n)) -> - (forall n : Z, n < z -> A (S n) -> A n) -> forall n : Z, A n. -Proof NZorder_induction. +Proof NZright_induction'. -Theorem Zorder_induction' : +Theorem Zleft_induction' : forall A : Z -> Prop, predicate_wd Zeq A -> - forall z : Z, A z -> - (forall n : Z, z <= n -> A n -> A (S n)) -> - (forall n : Z, n <= z -> A n -> A (P n)) -> - forall n : Z, A n. -Proof. -intros A A_wd z Az AS AP n; apply Zorder_induction with (z := z); try assumption. -intros m H1 H2. apply AP in H2; [| now apply -> Zlt_le_succ]. -unfold predicate_wd, fun_wd in A_wd; apply -> (A_wd (P (S m)) m); -[assumption | apply Zpred_succ]. -Qed. + forall z : Z, + (forall n : NZ, z <= n -> A n) -> + (forall n : Z, n < z -> A (S n) -> A n) -> + forall n : NZ, A n. +Proof NZleft_induction'. -Theorem Zright_induction' : +Theorem Zstrong_right_induction : forall A : Z -> Prop, predicate_wd Zeq A -> forall z : Z, - (forall n : Z, n <= z -> A n) -> - (forall n : Z, z <= n -> A n -> A (S n)) -> - forall n : Z, A n. -Proof NZright_induction'. + (forall n : Z, z <= n -> (forall m : Z, z <= m -> m < n -> A m) -> A n) -> + forall n : Z, z <= n -> A n. +Proof NZstrong_right_induction. + +Theorem Zstrong_left_induction : + forall A : Z -> Prop, predicate_wd Zeq A -> + forall z : Z, + (forall n : Z, n <= z -> (forall m : Z, m <= z -> S n <= m -> A m) -> A n) -> + forall n : Z, n <= z -> A n. +Proof NZstrong_left_induction. Theorem Zstrong_right_induction' : forall A : Z -> Prop, predicate_wd Zeq A -> @@ -190,27 +191,71 @@ Theorem Zstrong_right_induction' : forall n : Z, A n. Proof NZstrong_right_induction'. +Theorem Zstrong_left_induction' : + forall A : Z -> Prop, predicate_wd Zeq A -> + forall z : Z, + (forall n : Z, z <= n -> A n) -> + (forall n : Z, n <= z -> (forall m : Z, m <= z -> S n <= m -> A m) -> A n) -> + forall n : Z, A n. +Proof NZstrong_left_induction'. + +Theorem Zorder_induction : + forall A : Z -> Prop, predicate_wd Zeq A -> + forall z : Z, A z -> + (forall n : Z, z <= n -> A n -> A (S n)) -> + (forall n : Z, n < z -> A (S n) -> A n) -> + forall n : Z, A n. +Proof NZorder_induction. + +Theorem Zorder_induction' : + forall A : Z -> Prop, predicate_wd Zeq A -> + forall z : Z, A z -> + (forall n : Z, z <= n -> A n -> A (S n)) -> + (forall n : Z, n <= z -> A n -> A (P n)) -> + forall n : Z, A n. +Proof NZorder_induction'. + +Theorem Zorder_induction_0 : + forall A : Z -> Prop, predicate_wd Zeq A -> + A 0 -> + (forall n : Z, 0 <= n -> A n -> A (S n)) -> + (forall n : Z, n < 0 -> A (S n) -> A n) -> + forall n : Z, A n. +Proof NZorder_induction_0. + +Theorem Zorder_induction'_0 : + forall A : Z -> Prop, predicate_wd Zeq A -> + A 0 -> + (forall n : Z, 0 <= n -> A n -> A (S n)) -> + (forall n : Z, n <= 0 -> A n -> A (P n)) -> + forall n : Z, A n. +Proof NZorder_induction'_0. + +Ltac Zinduct n := induction_maker n ltac:(apply Zorder_induction_0). + (** Elimintation principle for < *) Theorem Zlt_ind : forall A : Z -> Prop, predicate_wd Zeq A -> - forall n : Z, - A (S n) -> - (forall m : Z, n < m -> A m -> A (S m)) -> - forall m : Z, n < m -> A m. + forall n : Z, A (S n) -> + (forall m : Z, n < m -> A m -> A (S m)) -> forall m : Z, n < m -> A m. Proof NZlt_ind. (** Elimintation principle for <= *) Theorem Zle_ind : forall A : Z -> Prop, predicate_wd Zeq A -> - forall n : Z, - A n -> - (forall m : Z, n <= m -> A m -> A (S m)) -> - forall m : Z, n <= m -> A m. + forall n : Z, A n -> + (forall m : Z, n <= m -> A m -> A (S m)) -> forall m : Z, n <= m -> A m. Proof NZle_ind. -Ltac Zinduct n := induction_maker n ltac:(apply Zorder_induction with (z := 0)). +(** Well-founded relations *) + +Theorem Zlt_wf : forall z : Z, well_founded (fun n m : Z => z <= n /\ n < m). +Proof NZlt_wf. + +Theorem Zgt_wf : forall z : Z, well_founded (fun n m : Z => m < n /\ n <= z). +Proof NZgt_wf. (** Theorems that are either not valid on N or have different proofs on N and Z *) diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v index f4c39934f..c0ad96de3 100644 --- a/theories/Numbers/NatInt/NZOrder.v +++ b/theories/Numbers/NatInt/NZOrder.v @@ -400,6 +400,26 @@ Proof. intros Az RS; apply NZstrong_right_induction; now apply NZrs_rs'. Qed. +Theorem NZright_induction' : + (forall n : NZ, n <= z -> A n) -> right_step -> forall n : NZ, A n. +Proof. +intros L R n. +destruct (NZlt_trichotomy n z) as [H | [H | H]]. +apply L; now le_less. +apply L; now le_equal. +apply NZright_induction. apply L; now le_equal. assumption. now le_less. +Qed. + +Theorem NZstrong_right_induction' : + (forall n : NZ, n <= z -> A n) -> right_step' -> forall n : NZ, A n. +Proof. +intros L R n. +destruct (NZlt_trichotomy n z) as [H | [H | H]]. +apply L; now le_less. +apply L; now le_equal. +apply NZstrong_right_induction. assumption. now le_less. +Qed. + End RightInduction. Section LeftInduction. @@ -447,6 +467,26 @@ Proof. intros Az LS; apply NZstrong_left_induction; now apply NZls_ls'. Qed. +Theorem NZleft_induction' : + (forall n : NZ, z <= n -> A n) -> left_step -> forall n : NZ, A n. +Proof. +intros R L n. +destruct (NZlt_trichotomy n z) as [H | [H | H]]. +apply NZleft_induction. apply R. now le_equal. assumption. now le_less. +rewrite H; apply R; le_equal. +apply R; le_less. +Qed. + +Theorem NZstrong_left_induction' : + (forall n : NZ, z <= n -> A n) -> left_step' -> forall n : NZ, A n. +Proof. +intros R L n. +destruct (NZlt_trichotomy n z) as [H | [H | H]]. +apply NZstrong_left_induction; auto. le_less. +rewrite H; apply R; le_equal. +apply R; le_less. +Qed. + End LeftInduction. Theorem NZorder_induction : @@ -462,28 +502,16 @@ now rewrite H. now apply NZright_induction; [| | le_less]. Qed. -Theorem NZright_induction' : - (forall n : NZ, n <= z -> A n) -> +Theorem NZorder_induction' : + A z -> (forall n : NZ, z <= n -> A n -> A (S n)) -> + (forall n : NZ, n <= z -> A n -> A (P n)) -> forall n : NZ, A n. Proof. -intros L R n. -destruct (NZlt_trichotomy n z) as [H | [H | H]]. -apply L; now le_less. -apply L; now le_equal. -apply NZright_induction. apply L; now le_equal. assumption. now le_less. -Qed. - -Theorem NZstrong_right_induction' : - (forall n : NZ, n <= z -> A n) -> - (forall n : NZ, z <= n -> (forall m : NZ, z <= m -> m < n -> A m) -> A n) -> - forall n : NZ, A n. -Proof. -intros L R n. -destruct (NZlt_trichotomy n z) as [H | [H | H]]. -apply L; now le_less. -apply L; now le_equal. -apply NZstrong_right_induction. assumption. now le_less. +intros Az AS AP n; apply NZorder_induction; try assumption. +intros m H1 H2. apply AP in H2; [| now apply -> NZlt_le_succ]. +unfold predicate_wd, fun_wd in A_wd; apply -> (A_wd (P (S m)) m); +[assumption | apply NZpred_succ]. Qed. End Center. @@ -495,6 +523,13 @@ Theorem NZorder_induction_0 : forall n : NZ, A n. Proof (NZorder_induction 0). +Theorem NZorder_induction'_0 : + A 0 -> + (forall n : NZ, 0 <= n -> A n -> A (S n)) -> + (forall n : NZ, n <= 0 -> A n -> A (P n)) -> + forall n : NZ, A n. +Proof (NZorder_induction' 0). + (** Elimintation principle for < *) Theorem NZlt_ind : forall (n : NZ), @@ -530,21 +565,34 @@ Section WF. Variable z : NZ. -Let R (n m : NZ) := z <= n /\ n < m. +Let Rlt (n m : NZ) := z <= n /\ n < m. +Let Rgt (n m : NZ) := m < n /\ n <= z. + +Add Morphism Rlt with signature NZeq ==> NZeq ==> iff as Rlt_wd. +Proof. +intros x1 x2 H1 x3 x4 H2; unfold Rlt; rewrite H1; now rewrite H2. +Qed. -Add Morphism R with signature NZeq ==> NZeq ==> iff as R_wd. +Add Morphism Rgt with signature NZeq ==> NZeq ==> iff as Rgt_wd. Proof. -intros x1 x2 H1 x3 x4 H2; unfold R; rewrite H1; now rewrite H2. +intros x1 x2 H1 x3 x4 H2; unfold Rgt; rewrite H1; now rewrite H2. Qed. -Lemma NZAcc_lt_wd : predicate_wd NZeq (Acc R). +Lemma NZAcc_lt_wd : predicate_wd NZeq (Acc Rlt). Proof. unfold predicate_wd, fun_wd. intros x1 x2 H; split; intro H1; destruct H1 as [H2]; constructor; intros; apply H2; now (rewrite H || rewrite <- H). Qed. -Theorem NZlt_wf : well_founded R. +Lemma NZAcc_gt_wd : predicate_wd NZeq (Acc Rgt). +Proof. +unfold predicate_wd, fun_wd. +intros x1 x2 H; split; intro H1; destruct H1 as [H2]; +constructor; intros; apply H2; now (rewrite H || rewrite <- H). +Qed. + +Theorem NZlt_wf : well_founded Rlt. Proof. unfold well_founded. apply NZstrong_right_induction' with (z := z). @@ -554,6 +602,17 @@ apply <- NZnle_gt in H2. elim H2. now apply NZle_trans with z. intros n H1 H2; constructor; intros m [H3 H4]. now apply H2. Qed. +Theorem NZgt_wf : well_founded Rgt. +Proof. +unfold well_founded. +apply NZstrong_left_induction' with (z := z). +apply NZAcc_gt_wd. +intros n H; constructor; intros y [H1 H2]. +apply <- NZnle_gt in H2. elim H2. now apply NZle_lt_trans with n. +intros n H1 H2; constructor; intros m [H3 H4]. +apply H2. assumption. now apply -> NZlt_le_succ. +Qed. + End WF. End NZOrderPropFunct. diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v index 2a17754d5..052a18c3e 100644 --- a/theories/Numbers/Natural/Abstract/NAxioms.v +++ b/theories/Numbers/Natural/Abstract/NAxioms.v @@ -15,6 +15,8 @@ Notation P := NZpred. Notation plus := NZplus. Notation times := NZtimes. Notation minus := NZminus. +Notation lt := NZlt. +Notation le := NZle. Notation "x == y" := (NZeq x y) (at level 70) : NatScope. Notation "x ~= y" := (~ NZeq x y) (at level 70) : NatScope. Notation "0" := NZ0 : NatScope. @@ -36,7 +38,7 @@ Axiom pred_0 : P 0 == 0. Axiom recursion_wd : forall (A : Set) (Aeq : relation A), forall a a' : A, Aeq a a' -> - forall f f' : N -> A -> A, eq_fun2 Neq Aeq Aeq f f' -> + forall f f' : N -> A -> A, fun2_eq Neq Aeq Aeq f f' -> forall x x' : N, x == x' -> Aeq (recursion a f x) (recursion a' f' x'). diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v index c0c479dc8..7c4464632 100644 --- a/theories/Numbers/Natural/Abstract/NBase.v +++ b/theories/Numbers/Natural/Abstract/NBase.v @@ -59,7 +59,7 @@ Definition if_zero (A : Set) (a b : A) (n : N) : A := Add Morphism if_zero with signature @eq ==> @eq ==> Neq ==> @eq as if_zero_wd. Proof. intros; unfold if_zero. apply recursion_wd with (Aeq := (@eq A)). -reflexivity. unfold eq_fun2; now intros. assumption. +reflexivity. unfold fun2_eq; now intros. assumption. Qed. Theorem if_zero_0 : forall (A : Set) (a b : A), if_zero A a b 0 = a. @@ -198,7 +198,7 @@ End PairInduction. Section TwoDimensionalInduction. Variable R : N -> N -> Prop. -Hypothesis R_wd : rel_wd Neq Neq R. +Hypothesis R_wd : relation_wd Neq Neq R. Add Morphism R with signature Neq ==> Neq ==> iff as R_morph. Proof. @@ -223,12 +223,12 @@ End TwoDimensionalInduction. try intros until n; try intros until m; pattern n, m; apply two_dim_induction; clear n m; - [solve_rel_wd | | | ].*) + [solve_relation_wd | | | ].*) Section DoubleInduction. Variable R : N -> N -> Prop. -Hypothesis R_wd : rel_wd Neq Neq R. +Hypothesis R_wd : relation_wd Neq Neq R. Add Morphism R with signature Neq ==> Neq ==> iff as R_morph1. Proof. @@ -250,7 +250,7 @@ Ltac double_induct n m := try intros until n; try intros until m; pattern n, m; apply double_induction; clear n m; - [solve_rel_wd | | | ]. + [solve_relation_wd | | | ]. End NBasePropFunct. diff --git a/theories/Numbers/Natural/Abstract/NIso.v b/theories/Numbers/Natural/Abstract/NIso.v index b792beefe..35e93bbc7 100644 --- a/theories/Numbers/Natural/Abstract/NIso.v +++ b/theories/Numbers/Natural/Abstract/NIso.v @@ -26,7 +26,7 @@ unfold natural_isomorphism. intros n m Eqxy. apply NAxiomsMod1.recursion_wd with (Aeq := Eq2). reflexivity. -unfold eq_fun2. intros _ _ _ y' y'' H. now apply NBasePropMod2.succ_wd. +unfold fun2_eq. intros _ _ _ y' y'' H. now apply NBasePropMod2.succ_wd. assumption. Qed. diff --git a/theories/Numbers/Natural/Abstract/NMinus.v b/theories/Numbers/Natural/Abstract/NMinus.v index 5ac1f70fb..fe0ec4e62 100644 --- a/theories/Numbers/Natural/Abstract/NMinus.v +++ b/theories/Numbers/Natural/Abstract/NMinus.v @@ -41,7 +41,7 @@ Qed. Theorem minus_gt : forall n m : N, n > m -> n - m ~= 0. Proof. intros n m H; elim H using lt_ind_rel; clear n m H. -solve_rel_wd. +solve_relation_wd. intro; rewrite minus_0_r; apply neq_succ_0. intros; now rewrite minus_succ. Qed. diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v index 3e338825e..8f68716bb 100644 --- a/theories/Numbers/Natural/Abstract/NOrder.v +++ b/theories/Numbers/Natural/Abstract/NOrder.v @@ -163,14 +163,6 @@ Theorem left_induction : forall n : N, n <= z -> A n. Proof NZleft_induction. -Theorem order_induction : - forall A : N -> Prop, predicate_wd Neq A -> - forall z : N, A z -> - (forall n : N, z <= n -> A n -> A (S n)) -> - (forall n : N, n < z -> A (S n) -> A n) -> - forall n : N, A n. -Proof NZorder_induction. - Theorem right_induction' : forall A : N -> Prop, predicate_wd Neq A -> forall z : N, @@ -179,6 +171,28 @@ Theorem right_induction' : forall n : N, A n. Proof NZright_induction'. +Theorem left_induction' : + forall A : N -> Prop, predicate_wd Neq A -> + forall z : N, + (forall n : NZ, z <= n -> A n) -> + (forall n : N, n < z -> A (S n) -> A n) -> + forall n : NZ, A n. +Proof NZleft_induction'. + +Theorem strong_right_induction : + forall A : N -> Prop, predicate_wd Neq A -> + forall z : N, + (forall n : N, z <= n -> (forall m : N, z <= m -> m < n -> A m) -> A n) -> + forall n : N, z <= n -> A n. +Proof NZstrong_right_induction. + +Theorem strong_left_induction : + forall A : N -> Prop, predicate_wd Neq A -> + forall z : N, + (forall n : N, n <= z -> (forall m : N, m <= z -> S n <= m -> A m) -> A n) -> + forall n : N, n <= z -> A n. +Proof NZstrong_left_induction. + Theorem strong_right_induction' : forall A : N -> Prop, predicate_wd Neq A -> forall z : N, @@ -187,6 +201,33 @@ Theorem strong_right_induction' : forall n : N, A n. Proof NZstrong_right_induction'. +Theorem strong_left_induction' : + forall A : N -> Prop, predicate_wd Neq A -> + forall z : N, + (forall n : N, z <= n -> A n) -> + (forall n : N, n <= z -> (forall m : N, m <= z -> S n <= m -> A m) -> A n) -> + forall n : N, A n. +Proof NZstrong_left_induction'. + +Theorem order_induction : + forall A : N -> Prop, predicate_wd Neq A -> + forall z : N, A z -> + (forall n : N, z <= n -> A n -> A (S n)) -> + (forall n : N, n < z -> A (S n) -> A n) -> + forall n : N, A n. +Proof NZorder_induction. + +Theorem order_induction' : + forall A : N -> Prop, predicate_wd Neq A -> + forall z : N, A z -> + (forall n : N, z <= n -> A n -> A (S n)) -> + (forall n : N, n <= z -> A n -> A (P n)) -> + forall n : N, A n. +Proof NZorder_induction'. + +(* We don't need order_induction_0 and order_induction'_0 (see NZOrder and +ZOrder) since they boil down to regular induction *) + (** Elimintation principle for < *) Theorem lt_ind : @@ -207,6 +248,24 @@ Theorem le_ind : forall m : N, n <= m -> A m. Proof NZle_ind. +(** Well-founded relations *) + +Theorem lt_wf : forall z : N, well_founded (fun n m : N => z <= n /\ n < m). +Proof NZlt_wf. + +Theorem gt_wf : forall z : N, well_founded (fun n m : N => m < n /\ n <= z). +Proof NZgt_wf. + +Theorem lt_wf_0 : well_founded lt. +Proof. +assert (H : relations_eq lt (fun n m : N => 0 <= n /\ n < m)). +intros x y; split. +intro H; split; [apply le_0_l | assumption]. now intros [_ H]. +rewrite H; apply lt_wf. +(* does not work: +setoid_replace lt with (fun n m : N => 0 <= n /\ n < m) using relation relations_eq.*) +Qed. + (** Theorems that are true for natural numbers but not for integers *) (* "le_0_l : forall n : N, 0 <= n" was proved in NBase.v *) @@ -247,18 +306,6 @@ split; intro H; [now elim H | intro; now apply lt_irrefl with 0]. intro n; split; intro H; [apply lt_0_succ | apply neq_succ_0]. Qed. -Lemma Acc_nonneg_lt : forall n : N, - Acc (fun n m => 0 <= n /\ n < m) n -> Acc NZlt n. -Proof. -intros n H; induction H as [n _ H2]; -constructor; intros y H; apply H2; split; [apply le_0_l | assumption]. -Qed. - -Theorem lt_wf : well_founded NZlt. -Proof. -unfold well_founded; intro n; apply Acc_nonneg_lt. apply NZlt_wf. -Qed. - (** Elimination principlies for < and <= for relations *) Section RelElim. @@ -266,7 +313,7 @@ Section RelElim. (* FIXME: Variable R : relation N. -- does not work *) Variable R : N -> N -> Prop. -Hypothesis R_wd : rel_wd Neq Neq R. +Hypothesis R_wd : relation_wd Neq Neq R. Add Morphism R with signature Neq ==> Neq ==> iff as R_morph2. Proof R_wd. @@ -359,7 +406,7 @@ Qed. Theorem pred_le_mono : forall n m : N, n <= m -> P n <= P m. (* Converse is false for n == 1, m == 0 *) Proof. intros n m H; elim H using le_ind_rel. -solve_rel_wd. +solve_relation_wd. intro; rewrite pred_0; apply le_0_l. intros p q H1 _; now do 2 rewrite pred_succ. Qed. diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v index b35af2e01..abd98ebef 100644 --- a/theories/Numbers/Natural/Binary/NBinary.v +++ b/theories/Numbers/Natural/Binary/NBinary.v @@ -137,11 +137,11 @@ Qed. Theorem recursion_wd : forall (A : Set) (Aeq : relation A), forall a a' : A, Aeq a a' -> - forall f f' : N -> A -> A, eq_fun2 NZeq Aeq Aeq f f' -> + forall f f' : N -> A -> A, fun2_eq NZeq Aeq Aeq f f' -> forall x x' : N, x = x' -> Aeq (recursion a f x) (recursion a' f' x'). Proof. -unfold fun2_wd, NZeq, eq_fun2. +unfold fun2_wd, NZeq, fun2_eq. intros A Aeq a a' Eaa' f f' Eff'. intro x; pattern x; apply Nind. intros x' H; now rewrite <- H. diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v index a3109fc6d..0a59ab520 100644 --- a/theories/Numbers/Natural/Peano/NPeano.v +++ b/theories/Numbers/Natural/Peano/NPeano.v @@ -145,11 +145,11 @@ Qed. Theorem recursion_wd : forall (A : Set) (Aeq : relation A), forall a a' : A, Aeq a a' -> - forall f f' : nat -> A -> A, eq_fun2 (@eq nat) Aeq Aeq f f' -> + forall f f' : nat -> A -> A, fun2_eq (@eq nat) Aeq Aeq f f' -> forall n n' : nat, n = n' -> Aeq (recursion a f n) (recursion a' f' n'). Proof. -unfold eq_fun2; induction n; intros n' Enn'; rewrite <- Enn' in *; simpl; auto. +unfold fun2_eq; induction n; intros n' Enn'; rewrite <- Enn' in *; simpl; auto. Qed. Theorem recursion_0 : @@ -163,7 +163,7 @@ Theorem recursion_succ : Aeq a a -> fun2_wd (@eq nat) Aeq Aeq f -> forall n : nat, Aeq (recursion a f (S n)) (f n (recursion a f n)). Proof. -unfold eq_fun2; induction n; simpl; auto. +induction n; simpl; auto. Qed. End NPeanoAxiomsMod. diff --git a/theories/Numbers/NumPrelude.v b/theories/Numbers/NumPrelude.v index 5f945701f..5505efd49 100644 --- a/theories/Numbers/NumPrelude.v +++ b/theories/Numbers/NumPrelude.v @@ -6,6 +6,7 @@ Theorem eq_true_or : forall b1 b2 : bool, b1 || b2 <-> b1 \/ b2, then it needs to know about bool and have a notation ||. *) Require Export QRewrite. +Set Implicit Arguments. (* Contents: - Coercion from bool to Prop @@ -102,30 +103,51 @@ Definition fun_wd (f : A -> B) := forall x y : A, Aeq x y -> Beq (f x) (f y). Definition fun2_wd (f : A -> B -> C) := forall x x' : A, Aeq x x' -> forall y y' : B, Beq y y' -> Ceq (f x y) (f x' y'). -Definition eq_fun : relation (A -> B) := +Definition fun_eq : relation (A -> B) := fun f f' => forall x x' : A, Aeq x x' -> Beq (f x) (f' x'). -(* Note that reflexivity of eq_fun means that every function +(* Note that reflexivity of fun_eq means that every function is well-defined w.r.t. Aeq and Beq, i.e., forall x x' : A, Aeq x x' -> Beq (f x) (f x') *) -Definition eq_fun2 (f f' : A -> B -> C) := +Definition fun2_eq (f f' : A -> B -> C) := forall x x' : A, Aeq x x' -> forall y y' : B, Beq y y' -> Ceq (f x y) (f' x' y'). End ExtensionalProperties. -Implicit Arguments fun_wd [A B]. -Implicit Arguments fun2_wd [A B C]. -Implicit Arguments eq_fun [A B]. -Implicit Arguments eq_fun2 [A B C]. +(* The following definitions instantiate Beq or Ceq to iff; therefore, they +have to be outside the ExtensionalProperties section *) Definition predicate_wd (A : Type) (Aeq : relation A) := fun_wd Aeq iff. -Definition rel_wd (A B : Type) (Aeq : relation A) (Beq : relation B) := +Definition relation_wd (A B : Type) (Aeq : relation A) (Beq : relation B) := fun2_wd Aeq Beq iff. -Implicit Arguments predicate_wd [A]. -Implicit Arguments rel_wd [A B]. +Definition relations_eq (A B : Type) (R1 R2 : A -> B -> Prop) := + forall (x : A) (y : B), R1 x y <-> R2 x y. + +Theorem relations_eq_equiv : + forall (A B : Type), equiv (A -> B -> Prop) (@relations_eq A B). +Proof. +intros A B; unfold equiv. split; [| split]; +unfold reflexive, symmetric, transitive, relations_eq. +reflexivity. +intros R1 R2 R3 H1 H2 x y; rewrite H1; apply H2. +now symmetry. +Qed. + +Add Relation (fun A B : Type => A -> B -> Prop) relations_eq + reflexivity proved by (fun A B : Type => proj1 (relations_eq_equiv A B)) + symmetry proved by (fun A B : Type => proj2 (proj2 (relations_eq_equiv A B))) + transitivity proved by (fun A B : Type => proj1 (proj2 (relations_eq_equiv A B))) +as relations_eq_rel. + +Add Morphism well_founded with signature relations_eq ==> iff as well_founded_wd. +Proof. +unfold relations_eq, well_founded; intros A R1 R2 H; +split; intros H1 a; induction (H1 a) as [x H2 H3]; constructor; +intros y H4; apply H3; [now apply <- H | now apply -> H]. +Qed. Ltac solve_predicate_wd := unfold predicate_wd; @@ -134,8 +156,8 @@ let y := fresh "y" in let H := fresh "H" in intros x y H; qiff x y H. -Ltac solve_rel_wd := -unfold rel_wd, fun2_wd; +Ltac solve_relation_wd := +unfold relation_wd, fun2_wd; let x1 := fresh "x" in let y1 := fresh "y" in let H1 := fresh "H" in @@ -145,7 +167,7 @@ let H2 := fresh "H" in intros x1 y1 H1 x2 y2 H2; qsetoid_rewrite H1; qiff x2 y2 H2. -(* The tactic solve_rel_wd is not very efficient because qsetoid_rewrite +(* 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 time. It is better to analyze the formula once and generalize qiff to take @@ -296,21 +318,15 @@ Qed. Definition LE_Set : forall A : Set, relation A := (@eq). -Lemma eq_equiv : forall A : Set, equiv A (LE_Set A). +Lemma eq_equiv : forall A : Set, equiv A (@LE_Set A). Proof. intro A; unfold equiv, LE_Set, reflexive, symmetric, transitive. repeat split; [exact (@trans_eq A) | exact (@sym_eq A)]. (* It is interesting how the tactic split proves reflexivity *) Qed. -Add Relation (fun A : Set => A) LE_Set +(*Add Relation (fun A : Set => A) LE_Set reflexivity proved by (fun A : Set => (proj1 (eq_equiv A))) symmetry proved by (fun A : Set => (proj2 (proj2 (eq_equiv A)))) transitivity proved by (fun A : Set => (proj1 (proj2 (eq_equiv A)))) -as EA_rel. - -(* - Local Variables: - tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" - End: -*) +as EA_rel.*) diff --git a/theories/Numbers/QRewrite.v b/theories/Numbers/QRewrite.v index e41052f95..439fc6847 100644 --- a/theories/Numbers/QRewrite.v +++ b/theories/Numbers/QRewrite.v @@ -181,8 +181,3 @@ end. ra (eqcons H0 (eqcons H1 eqnil)).*) -(* - Local Variables: - tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" - End: -*) |