we rebild the arithmetic library because lib/arithmetics/nat.ma has some problems:
- matitac does not compile it because of known time travel erropr
- too many indexed theorems make the search space explode during auto
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/notation/functions/zero_0.ma".
+include "ground/arith/pnat.ma".
+
+(* NON-NEGATIVE INTEGERS ****************************************************)
+
+(*** nat *)
+inductive nat: Type[0] ≝
+| nzero: nat
+| ninj : pnat → nat
+.
+
+coercion ninj.
+
+interpretation "zero (non-negative integers" 'Zero = nzero.
+
+(* Basic inversions *********************************************************)
+
+(* Note: destruct *)
+lemma eq_inv_ninj_bi: injective … ninj.
+#p #q #H destruct //
+qed-.
+
+(* Basic constructions ******************************************************)
+
+lemma eq_nat_dec (n1,n2:nat): Decidable (n1 = n2).
+* [| #p1 ] * [2,4: #p2 ]
+[1,4: @or_intror #H destruct
+| elim (eq_pnat_dec p1 p2)
+ /4 width=1 by eq_inv_ninj_bi, or_intror, or_introl/
+| /2 width=1 by or_introl/
+]
+qed-.
--- /dev/null
+"cic:/matita/arithmetics/nat/nat.ind"
+#
+"cic:/matita/arithmetics/nat/nat_ind.con"
+"cic:/matita/arithmetics/nat/nat_elim2.con"
+"cic:/matita/arithmetics/nat/injective_S.con"
+#
+"cic:/matita/arithmetics/nat/plus.con"
+"cic:/matita/arithmetics/nat/plus_n_O.con"
+"cic:/matita/arithmetics/nat/plus_n_Sm.con"
+"cic:/matita/arithmetics/nat/plus_O_n.con"
+"cic:/matita/arithmetics/nat/commutative_plus.con"
+"cic:/matita/arithmetics/nat/associative_plus.con"
+"cic:/matita/arithmetics/nat/plus_plus_comm_23.con"
+"cic:/matita/arithmetics/nat/assoc_plus1.con"
+"cic:/matita/arithmetics/nat/injective_plus_l.con"
+"cic:/matita/arithmetics/nat/injective_plus_r.con"
+"cic:/matita/arithmetics/nat/nat_ind_plus.con"
+#
+"cic:/matita/arithmetics/nat/le.ind"
+"cic:/matita/arithmetics/nat/le_ind.con"
+"cic:/matita/arithmetics/nat/le_n_Sn.con"
+"cic:/matita/arithmetics/nat/le_O_n.con"
+"cic:/matita/arithmetics/nat/le_S_S.con"
+"cic:/matita/arithmetics/nat/le_or_ge.con"
+"cic:/matita/arithmetics/nat/le_S_S_to_le.con"
+"cic:/matita/arithmetics/nat/le_n_O_to_eq.con"
+"cic:/matita/arithmetics/nat/le_to_le_to_eq.con"
+"cic:/matita/arithmetics/nat/transitive_le.con"
+"cic:/matita/arithmetics/nat/decidable_le.con"
+%
+"cic:/matita/arithmetics/nat/monotonic_le_plus_l.con"
+"cic:/matita/arithmetics/nat/monotonic_le_plus_r.con"
+"cic:/matita/arithmetics/nat/le_plus_n_r.con"
+"cic:/matita/arithmetics/nat/le_plus_n.con"
+"cic:/matita/arithmetics/nat/le_plus_b.con"
+"cic:/matita/arithmetics/nat/le_plus_a.con"
+"cic:/matita/arithmetics/nat/le_plus.con"
+"cic:/matita/arithmetics/nat/plus_le_0.con"
+"cic:/matita/arithmetics/nat/le_plus_to_le_r.con"
+"cic:/matita/arithmetics/nat/le_plus_to_le.con"
+#
+"cic:/matita/arithmetics/nat/lt.con"
+"cic:/matita/arithmetics/nat/lt_O_S.con"
+"cic:/matita/arithmetics/nat/le_to_or_lt_eq.con"
+"cic:/matita/arithmetics/nat/eq_or_gt.con"
+"cic:/matita/arithmetics/nat/lt_or_ge.con"
+"cic:/matita/arithmetics/nat/not_le_to_lt.con"
+"cic:/matita/arithmetics/nat/lt_to_le_to_lt.con"
+"cic:/matita/arithmetics/nat/le_to_lt_to_lt.con"
+"cic:/matita/arithmetics/nat/lt_to_not_le.con"
+"cic:/matita/arithmetics/nat/lt_to_not_eq.con"
+"cic:/matita/arithmetics/nat/lt_to_le.con"
+"cic:/matita/arithmetics/nat/ltn_to_ltO.con"
+"cic:/matita/arithmetics/nat/transitive_lt.con"
+"cic:/matita/arithmetics/nat/nat_elim1.con"
+"cic:/matita/arithmetics/nat/f_ind.con"
+"cic:/matita/arithmetics/nat/f2_ind.con"
+"cic:/matita/arithmetics/nat/f3_ind.con"
+
+####################################
+
+"cic:/matita/arithmetics/nat/lt_plus_Sn_r.con"
+"cic:/matita/arithmetics/nat/lt_plus_to_lt_l.con"
+"cic:/matita/arithmetics/nat/monotonic_lt_plus_l.con"
+"cic:/matita/arithmetics/nat/monotonic_lt_plus_r.con"
+
+"cic:/matita/arithmetics/nat/le_pred_n.con"
+"cic:/matita/arithmetics/nat/pred.con"
+"cic:/matita/arithmetics/nat/pred_Sn.con"
+"cic:/matita/arithmetics/nat/S_pred.con"
+"cic:/matita/arithmetics/nat/monotonic_pred.con"
+
+"cic:/matita/arithmetics/nat/discr_minus_x_xy.con"
+"cic:/matita/arithmetics/nat/discr_plus_xy_minus_xz.con"
+"cic:/matita/arithmetics/nat/eq_minus_O.con"
+"cic:/matita/arithmetics/nat/eq_minus_S_pred.con"
+"cic:/matita/arithmetics/nat/inv_eq_minus_O.con"
+"cic:/matita/arithmetics/nat/le_minus_to_plus.con"
+"cic:/matita/arithmetics/nat/le_minus_to_plus_r.con"
+"cic:/matita/arithmetics/nat/le_plus_minus_m_m.con"
+"cic:/matita/arithmetics/nat/le_plus_to_minus.con"
+"cic:/matita/arithmetics/nat/le_plus_to_minus_r.con"
+"cic:/matita/arithmetics/nat/lt_minus_to_plus.con"
+"cic:/matita/arithmetics/nat/lt_minus_to_plus_r.con"
+"cic:/matita/arithmetics/nat/lt_plus_to_minus.con"
+"cic:/matita/arithmetics/nat/lt_plus_to_minus_r.con"
+"cic:/matita/arithmetics/nat/minus.con"
+"cic:/matita/arithmetics/nat/minus_le.con"
+"cic:/matita/arithmetics/nat/minus_le_minus_minus_comm.con"
+"cic:/matita/arithmetics/nat/minus_minus_associative.con"
+"cic:/matita/arithmetics/nat/minus_minus_comm.con"
+"cic:/matita/arithmetics/nat/minus_minus.con"
+"cic:/matita/arithmetics/nat/minus_minus_m_m.con"
+"cic:/matita/arithmetics/nat/minus_n_n.con"
+"cic:/matita/arithmetics/nat/minus_n_O.con"
+"cic:/matita/arithmetics/nat/minus_O_n.con"
+"cic:/matita/arithmetics/nat/minus_plus.con"
+"cic:/matita/arithmetics/nat/minus_plus_m_m.con"
+"cic:/matita/arithmetics/nat/minus_plus_plus_l.con"
+"cic:/matita/arithmetics/nat/minus_pred_pred.con"
+"cic:/matita/arithmetics/nat/minus_Sn_m.con"
+"cic:/matita/arithmetics/nat/minus_Sn_n.con"
+"cic:/matita/arithmetics/nat/minus_S_S.con"
+"cic:/matita/arithmetics/nat/monotonic_le_minus_l.con"
+"cic:/matita/arithmetics/nat/monotonic_le_minus_r.con"
+"cic:/matita/arithmetics/nat/monotonic_lt_minus_l.con"
+"cic:/matita/arithmetics/nat/plus_minus_associative.con"
+"cic:/matita/arithmetics/nat/plus_minus.con"
+"cic:/matita/arithmetics/nat/plus_minus_m_m.con"
+"cic:/matita/arithmetics/nat/plus_minus_plus_plus_l.con"
+"cic:/matita/arithmetics/nat/plus_to_minus.con"
+"cic:/matita/arithmetics/nat/le_inv_plus_l.con"
+"cic:/matita/arithmetics/nat/lt_inv_plus_l.con"
+
+"cic:/matita/arithmetics/nat/to_max.con"
+"cic:/matita/arithmetics/nat/commutative_max.con"
+"cic:/matita/arithmetics/nat/leb.con"
+"cic:/matita/arithmetics/nat/leb_elim.con"
+"cic:/matita/arithmetics/nat/le_maxl.con"
+"cic:/matita/arithmetics/nat/le_maxr.con"
+"cic:/matita/arithmetics/nat/le_to_leb_true.con"
+"cic:/matita/arithmetics/nat/max.con"
+"cic:/matita/arithmetics/nat/not_le_to_leb_false.con"
+
+"cic:/matita/arithmetics/nat/nat_discr.con"
+"cic:/matita/arithmetics/nat/times.con"
+"cic:/matita/arithmetics/nat/times_n_1.con"
+"cic:/matita/arithmetics/nat/times_Sn_m.con"
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/arith/pnat_iter.ma".
+include "ground/arith/nat.ma".
+
+(* NON-NEGATIVE INTEGERS ****************************************************)
+
+definition niter (n:nat) (A:Type[0]) (f:A→A) (a:A) ≝
+match n with
+[ nzero ⇒ a
+| ninj p ⇒ f^{A}p a
+]
+.
+
+interpretation
+ "iterated function (non-negative integers)"
+ 'Exp A f n = (niter n A f).
+
+(* Basic rewrites ***********************************************************)
+
+lemma niter_zero (A) (f) (a): a = (f^{A}𝟎) a.
+// qed.
+
+lemma niter_inj (A) (f) (p) (a): f^p a = f^{A}(ninj p) a.
+// qed.
+
+(* Advanced rewrites ********************************************************)
+
+lemma niter_appl (A) (f) (n) (a): f (f^n a) = f^{A}n (f a).
+#A #f * //
+#p #a <niter_inj <niter_inj <piter_appl //
+qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/arith/nat_succ.ma".
+include "ground/arith/nat_iter.ma".
+
+(* NON-NEGATIVE INTEGERS ****************************************************)
+
+(* Rewrites with nsucc ******************************************************)
+
+lemma niter_succ (A) (f) (n) (a): f (f^n a) = f^{A}(↑n) a.
+#A #f * //
+qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/insert_eq/insert_eq_0.ma".
+include "ground/arith/nat_succ.ma".
+
+(* NON-NEGATIVE INTEGERS ****************************************************)
+
+(*** le *)
+(*** le_ind *)
+inductive nle (m:nat): predicate nat ≝
+| nle_refl : nle m m
+| nle_succ_dx: ∀n. nle m n → nle m (↑n)
+.
+
+interpretation
+ "less equal (non-negative integers)"
+ 'leq m n = (nle m n).
+
+(* Basic constructions ******************************************************)
+
+(*** le_n_Sn *)
+lemma nle_succ_dx_refl (m): m ≤ ↑m.
+/2 width=1 by nle_refl, nle_succ_dx/ qed.
+
+(*** le_O_n *)
+lemma nle_zero_sx (m): 𝟎 ≤ m.
+#m @(nat_ind … m) -m /2 width=1 by nle_succ_dx/
+qed.
+
+(*** le_S_S *)
+lemma nle_succ_bi (m) (n): m ≤ n → ↑m ≤ ↑n.
+#m #n #H elim H -n /2 width=1 by nle_refl, nle_succ_dx/
+qed.
+
+(*** le_or_ge *)
+lemma nle_ge_e (m) (n): ∨∨ m ≤ n | n ≤ m.
+#m @(nat_ind … m) -m [ /2 width=1 by or_introl/ ]
+#m #IH #n @(nat_ind … n) -n [ /2 width=1 by or_intror/ ]
+#n #_ elim (IH n) -IH /3 width=2 by nle_succ_bi, or_introl, or_intror/
+qed-.
+
+(* Basic inversions *********************************************************)
+
+lemma nle_inv_succ_sn (m) (n): ↑m ≤ n → m ≤ n.
+#m #n #H elim H -n /2 width=1 by nle_succ_dx/
+qed-.
+
+(*** le_S_S_to_le *)
+lemma nle_inv_succ_bi (m) (n): ↑m ≤ ↑n → m ≤ n.
+#m #n @(insert_eq_0 … (↑n))
+#y * -y
+[ #H <(eq_inv_nsucc_bi … H) -m //
+| #y #Hy #H >(eq_inv_nsucc_bi … H) -n /2 width=1 by nle_inv_succ_sn/
+]
+qed-.
+
+(*** le_n_O_to_eq *)
+lemma nle_inv_zero_dx (m): m ≤ 𝟎 → 𝟎 = m.
+#m @(insert_eq_0 … (𝟎))
+#y * -y
+[ #H destruct //
+| #y #_ #H elim (eq_inv_nzero_succ … H)
+]
+qed-.
+
+lemma nle_inv_succ_sn_refl (m): ↑m ≤ m → ⊥.
+#m @(nat_ind … m) -m [| #m #IH ] #H
+[ /3 width=2 by nle_inv_zero_dx, eq_inv_nzero_succ/
+| /3 width=1 by nle_inv_succ_bi/
+]
+qed-.
+
+(* Order properties *********************************************************)
+
+(*** le_to_le_to_eq *)
+theorem nle_antisym (m) (n): m ≤ n → n ≤ m → m = n.
+#m #n #H elim H -n //
+#n #_ #IH #Hn
+lapply (nle_inv_succ_sn … Hn) #H
+lapply (IH H) -IH -H #H destruct
+elim (nle_inv_succ_sn_refl … Hn)
+qed-.
+
+(*** transitive_le *)
+theorem nle_trans: Transitive … nle.
+#m #n #H elim H -n /3 width=1 by nle_inv_succ_sn/
+qed-.
+
+(* Advanced constructions ***************************************************)
+
+(*** decidable_le *)
+lemma nle_dec (m) (n): Decidable … (m ≤ n).
+#m #n elim (nle_ge_e m n) [ /2 width=1 by or_introl/ ]
+#Hnm elim (eq_nat_dec m n) [ #H destruct /2 width=1 by nle_refl, or_introl/ ]
+/4 width=1 by nle_antisym, or_intror/
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/arith/nat_plus.ma".
+include "ground/arith/nat_le.ma".
+
+(* NON-NEGATIVE INTEGERS ****************************************************)
+
+(* Basic constructions with plus ********************************************)
+
+(*** monotonic_le_plus_l *)
+lemma nle_plus_bi_dx (m) (n1) (n2): n1 ≤ n2 → n1 + m ≤ n2 + m.
+#m #n1 #n2 #H elim H -n2 /2 width=3 by nle_trans/
+qed.
+
+(*** monotonic_le_plus_r *)
+lemma nle_plus_bi_sn (m) (n1) (n2): n1 ≤ n2 → m + n1 ≤ m + n2.
+#m #n1 #n2 #H <nplus_comm <nplus_comm in ⊢ (??%);
+/2 width=1 by nle_plus_bi_dx/
+qed.
+
+(*** le_plus_n_r *)
+lemma nle_plus_dx_dx_refl (m) (n): m ≤ m + n.
+/2 width=1 by nle_plus_bi_sn/ qed.
+
+(*** le_plus_n *)
+lemma nle_plus_dx_sn_refl (m) (n): m ≤ n + m.
+/2 width=1 by nle_plus_bi_sn/ qed.
+
+(*** le_plus_b *)
+lemma nle_plus_dx_dx (m) (n) (o): n + o ≤ m → n ≤ m.
+/2 width=3 by nle_trans/ qed.
+
+(*** le_plus_a *)
+lemma nle_plus_dx_sn (m) (n) (o): n ≤ m → n ≤ o + m.
+/2 width=3 by nle_trans/ qed.
+
+(* Main constructions with plus *********************************************)
+
+(*** le_plus *)
+theorem nle_plus_bi (m1) (m2) (n1) (n2):
+ m1 ≤ m2 → n1 ≤ n2 → m1 + n1 ≤ m2 + n2.
+/3 width=3 by nle_plus_bi_dx, nle_plus_bi_sn, nle_trans/ qed.
+
+(* Basic inversions with plus ***********************************************)
+
+(*** plus_le_0 *)
+lemma nle_inv_plus_zero (m) (n): m + n ≤ 𝟎 → ∧∧ 𝟎 = m & 𝟎 = n.
+/3 width=1 by nle_inv_zero_dx, eq_inv_nzero_plus/ qed-.
+
+(*** le_plus_to_le_r *)
+lemma nle_inv_plus_bi_dx (o) (m) (n): n + o ≤ m + o → n ≤ m.
+#o @(nat_ind … o) -o /3 width=1 by nle_inv_succ_bi/
+qed-.
+
+(*** le_plus_to_le *)
+lemma nle_inv_plus_bi_sn (o) (m) (n): o + n ≤ o + m → n ≤ m.
+/2 width=2 by nle_inv_plus_bi_dx/ qed-.
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/arith/nat_le.ma".
+
+(* NON-NEGATIVE INTEGERS ****************************************************)
+
+(*** lt *)
+definition nlt: relation2 nat nat ≝
+ λm,n. ↑m ≤ n.
+
+interpretation
+ "less (non-negative integers)"
+ 'lt m n = (nlt m n).
+
+(* Basic constructions ******************************************************)
+
+(*** lt_O_S *)
+lemma nlt_zero_succ (m): 𝟎 < ↑m.
+/2 width=1 by nle_succ_bi/ qed.
+
+(*** le_to_or_lt_eq *)
+lemma nle_lt_eq_e (m) (n): m ≤ n → ∨∨ m < n | m = n.
+#m #n * -n /3 width=1 by nle_succ_bi, or_introl/
+qed-.
+
+(*** eq_or_gt *)
+lemma eq_gt_e (n): ∨∨ 𝟎 = n | 𝟎 < n.
+#n elim (nle_lt_eq_e (𝟎) n ?)
+/2 width=1 by or_introl, or_intror/
+qed-.
+
+(*** lt_or_ge *)
+lemma nlt_ge_e (m) (n): ∨∨ m < n | n ≤ m.
+#m #n elim (nle_ge_e m n) /2 width=1 by or_intror/
+#H elim (nle_lt_eq_e … H) -H /2 width=1 by nle_refl, or_introl, or_intror/
+qed-.
+
+(*** not_le_to_lt *)
+lemma le_false_nlt (m) (n): (n ≤ m → ⊥) → m < n.
+#m #n elim (nlt_ge_e m n) [ // ]
+#H #Hn elim Hn -Hn //
+qed.
+
+(*** lt_to_le_to_lt *)
+lemma nlt_le_trans (o) (m) (n): m < o → o ≤ n → m < n.
+/2 width=3 by nle_trans/ qed-.
+
+lemma le_nlt_trans (o) (m) (n): m ≤ o → o < n → m < n.
+/3 width=3 by nle_succ_bi, nle_trans/ qed-.
+
+(* Basic inversions *********************************************************)
+
+(*** lt_to_not_le *)
+lemma nlt_ge_false (m) (n): m < n → n ≤ m → ⊥.
+/3 width=4 by nle_inv_succ_sn_refl, nlt_le_trans/ qed-.
+
+(*** lt_to_not_eq *)
+lemma nlt_inv_refl (m): m < m → ⊥.
+/2 width=4 by nlt_ge_false/ qed-.
+
+lemma nlt_inv_zero_dx (m): m < 𝟎 → ⊥.
+/2 width=4 by nlt_ge_false/ qed-.
+
+(* Basic destructions *******************************************************)
+
+(*** lt_to_le *)
+lemma nlt_des_le (m) (n): m < n → m ≤ n.
+/2 width=3 by nle_trans/ qed-.
+
+(*** ltn_to_ltO *)
+lemma nlt_des_lt_O_sn (m) (n): m < n → 𝟎 < n.
+/3 width=3 by le_nlt_trans/ qed-.
+
+(* Main constructions *******************************************************)
+
+(*** transitive_lt *)
+theorem nlt_trans: Transitive … nlt.
+/3 width=3 by nlt_des_le, nlt_le_trans/ qed-.
+
+(* Advanced eliminations ****************************************************)
+
+lemma nat_ind_lt_le (Q:predicate …):
+ (∀n. (∀m. m < n → Q m) → Q n) → ∀n,m. m ≤ n → Q m.
+#Q #H1 #n @(nat_ind … n) -n
+[ #m #H <(nle_inv_zero_dx … H) -m
+ @H1 -H1 #o #H elim (nlt_inv_zero_dx … H)
+| /5 width=3 by nlt_le_trans, nle_inv_succ_bi/
+]
+qed-.
+
+(*** nat_elim1 *)
+lemma nat_ind_lt (Q:predicate …):
+ (∀n. (∀m. m < n → Q m) → Q n) → ∀n. Q n.
+/4 width=2 by nat_ind_lt_le/ qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/arith/nat_iter_succ.ma".
+
+(* NON-NEGATIVE INTEGERS ****************************************************)
+
+(*** plus *)
+definition nplus: nat → nat → nat ≝
+ λm,n. nsucc^n m.
+
+interpretation
+ "plus (positive integers"
+ 'plus m n = (nplus m n).
+
+(* Basic rewrites ***********************************************************)
+
+(*** plus_n_O *)
+lemma nplus_zero_dx (m): m = m + 𝟎.
+// qed.
+
+lemma nplus_one_dx (n): ↑n = n + 𝟏.
+// qed.
+
+(* Semigroup properties *****************************************************)
+
+(*** plus_n_Sm *)
+lemma nplus_succ_dx (m) (n): ↑(m+n) = m + ↑n.
+#m #n @(niter_succ … nsucc)
+qed.
+
+lemma nplus_succ_sn (m) (n): ↑(m+n) = ↑m + n.
+#m #n @(niter_appl … nsucc)
+qed.
+
+(*** plus_O_n.con *)
+lemma nplus_zero_sn (m): m = 𝟎 + m.
+#m @(nat_ind … m) -m //
+qed.
+
+(*** commutative_plus *)
+lemma nplus_comm: commutative … nplus.
+#m @(nat_ind … m) -m //
+qed-.
+
+lemma nplus_one_sn (n): ↑n = 𝟏 + n.
+#n <nplus_comm // qed.
+
+(*** associative_plus *)
+lemma nplus_assoc: associative … nplus.
+#m #n #o @(nat_ind … o) -o //
+#o #IH <nplus_succ_dx <nplus_succ_dx <nplus_succ_dx <IH -IH //
+qed.
+
+(*** assoc_plus1 *)
+lemma nplus_plus_comm_12 (o) (m) (n): m + n + o = n + (m + o).
+#o #m #n <nplus_comm in ⊢ (??(?%?)?); // qed.
+
+(*** plus_plus_comm_23 *)
+lemma nplus_plus_comm_23 (o) (m) (n): o + m + n = o + n + m.
+#o #m #n >nplus_assoc >nplus_assoc <nplus_comm in ⊢ (??(??%)?); //
+qed-.
+
+(* Basic inversions *********************************************************)
+
+lemma eq_inv_nzero_plus (m) (n): 𝟎 = m + n → ∧∧ 𝟎 = m & 𝟎 = n.
+#m #n @(nat_ind … n) -n /2 width=1 by conj/
+#n #_ <nplus_succ_dx #H
+elim (eq_inv_nzero_succ … H)
+qed-.
+
+(*** injective_plus_l *)
+lemma eq_inv_nplus_bi_dx (o) (m) (n): m + o = n + o → m = n.
+#o @(nat_ind … o) -o /3 width=1 by eq_inv_nsucc_bi/
+qed-.
+
+(*** injective_plus_r *)
+lemma eq_inv_nplus_bi_sn (o) (m) (n): o + m = o + n → m = n.
+#o #m #n <nplus_comm <nplus_comm in ⊢ (???%→?);
+/2 width=2 by eq_inv_nplus_bi_dx/ qed-.
+
+(* Advanced eliminations ****************************************************)
+
+(*** nat_ind_plus *)
+lemma nat_ind_plus (Q:predicate …):
+ Q (𝟎) → (∀n. Q n → Q (𝟏+n)) → ∀n. Q n.
+#Q #IH1 #IH2 #n @(nat_ind … n) -n /2 width=1 by/
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/arith/nat.ma".
+
+(* NON-NEGATIVE INTEGERS ****************************************************)
+
+definition nsucc: nat → nat ≝ λm. match m with
+[ nzero ⇒ ninj (𝟏)
+| ninj p ⇒ ninj (↑p)
+].
+
+interpretation
+ "successor (non-negative integers"
+ 'UpArrow m = (nsucc m).
+
+(* Basic rewrites ***********************************************************)
+
+lemma nsucc_zero: ninj (𝟏) = ↑𝟎.
+// qed.
+
+lemma nsucc_inj (p): ninj (↑p) = ↑(ninj p).
+// qed.
+
+(* Basic eliminations *******************************************************)
+
+(*** nat_ind *)
+lemma nat_ind (Q:predicate …):
+ Q (𝟎) → (∀n. Q n → Q (↑n)) → ∀n. Q n.
+#Q #IH1 #IH2 * //
+#p elim p -p /2 width=1 by/
+qed-.
+
+(*** nat_elim2 *)
+lemma nat_ind_2 (Q:relation2 …):
+ (∀n. Q (𝟎) n) →
+ (∀m. Q (↑m) (𝟎)) →
+ (∀m,n. Q m n → Q (↑m) (↑n)) →
+ ∀m,n. Q m n.
+#Q #IH1 #IH2 #IH3 #m elim m -m [ // ]
+#m #IH #n elim n -n /2 width=1 by/
+qed-.
+
+(* Basic inversions *********************************************************)
+
+(*** injective_S *)
+lemma eq_inv_nsucc_bi: injective … nsucc.
+* [| #p1 ] * [2,4: #p2 ]
+[1,4: <nsucc_zero <nsucc_inj #H destruct
+| <nsucc_inj <nsucc_inj #H destruct //
+| //
+]
+qed-.
+
+lemma eq_inv_nsucc_zero (m): ↑m = 𝟎 → ⊥.
+* [ <nsucc_zero | #p <nsucc_inj ] #H destruct
+qed-.
+
+lemma eq_inv_nzero_succ (m): 𝟎 = ↑m → ⊥.
+* [ <nsucc_zero | #p <nsucc_inj ] #H destruct
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/notation/functions/one_0.ma".
+include "ground/notation/functions/uparrow_1.ma".
+include "ground/lib/relations.ma".
+
+(* POSITIVE INTEGERS ********************************************************)
+
+inductive pnat: Type[0] ≝
+| punit: pnat
+| psucc: pnat → pnat
+.
+
+interpretation
+ "unit (positive integers)"
+ 'One = (punit).
+
+interpretation
+ "successor (positive integers)"
+ 'UpArrow p = (psucc p).
+
+(* Basic inversions *********************************************************)
+
+(* Note: destruct *)
+lemma eq_inv_psucc_bi: injective … psucc.
+#p #q #H destruct //
+qed.
+
+(* Basic constructions ******************************************************)
+
+lemma eq_pnat_dec (p1,p2:pnat): Decidable (p1 = p2).
+#p1 elim p1 -p1 [| #p1 #IH ] * [2,4: #p2 ]
+[1,4: @or_intror #H destruct
+| elim (IH p2) -IH #H destruct
+ /4 width=1 by eq_inv_psucc_bi, or_intror, or_introl/
+| /2 width=1 by or_introl/
+]
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/notation/functions/exp_3.ma".
+include "ground/arith/pnat.ma".
+
+(* POSITIVE INTEGERS ********************************************************)
+
+rec definition piter (p:pnat) (A:Type[0]) (f:A→A) (a:A) ≝
+match p with
+[ punit ⇒ f a
+| psucc q ⇒ f (piter q A f a)
+].
+
+interpretation
+ "iterated function (positive integers)"
+ 'Exp A f p = (piter p A f).
+
+(* Basic rewrites ***********************************************************)
+
+lemma piter_unit (A) (f) (a): f a = (f^{A}𝟏) a.
+// qed.
+
+lemma piter_succ (A) (f) (p) (a): f (f^p a) = f^{A}(↑p) a.
+// qed.
+
+(* Advanced rewrites ********************************************************)
+
+lemma piter_appl (A) (f) (p) (a): f (f^p a) = f^{A}p (f a).
+#A #f #p elim p -p //
+#p #IH #a <piter_succ <piter_succ //
+qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/arith/pnat_iter.ma".
+
+(* POSITIVE INTEGERS ********************************************************)
+
+definition pplus: pnat → pnat → pnat ≝
+ λp,q. psucc^q p.
+
+interpretation
+ "plus (positive integers"
+ 'plus p q = (pplus p q).
+
+(* Basic rewrites ***********************************************************)
+
+lemma pplus_one_dx (p): ↑p = p + 𝟏.
+// qed.
+
+lemma pplus_succ_dx (p) (q): ↑(p+q) = p + ↑q.
+// qed.
+
+(* Semigroup properties *****************************************************)
+
+lemma pplus_succ_sn (p) (q): ↑(p+q) = ↑p + q.
+#p #q @(piter_appl … psucc)
+qed.
+
+lemma pplus_one_sn (p): ↑p = 𝟏 + p.
+#p elim p -p //
+qed.
+
+lemma pplus_comm: commutative … pplus.
+#p elim p -p //
+qed.
+
+lemma pplus_assoc: associative … pplus.
+#p #q #r elim r -r //
+#r #IH <pplus_succ_dx <pplus_succ_dx <IH -IH //
+qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+
+notation < "hvbox( f ^ break x )"
+ left associative with precedence 75
+ for @{ 'Exp $X $f $x }.
+
+notation > "hvbox( f ^ break x )"
+ left associative with precedence 75
+ for @{ 'Exp ? $f $x }.
+
+notation > "hvbox( f ^{ break term 46 X } break term 75 x )"
+ non associative with precedence 75
+ for @{ 'Exp $X $f $x }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+
+notation "𝟏"
+ non associative with precedence 55
+ for @{ 'One }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+
+notation "𝟎"
+ non associative with precedence 55
+ for @{ 'Zero }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/arith/nat_lt.ma".
+
+(* WELL-FOUNDED INDUCTION ***************************************************)
+
+fact wf1_ind_nlt_aux (A1) (f:A1→nat) (Q:predicate …):
+ (∀n. (∀a1. f a1 < n → Q a1) → ∀a1. f a1 = n → Q a1) →
+ ∀n,a1. f a1 = n → Q a1.
+#A1 #f #Q #H #n @(nat_ind_lt … n) -n /3 width=3 by/
+qed-.
+
+(*** f_ind *)
+lemma wf1_ind_nlt (A1) (f:A1→nat) (Q:predicate …):
+ (∀n. (∀a1. f a1 < n → Q a1) → ∀a1. f a1 = n → Q a1) →
+ ∀a1. Q a1.
+#A #f #Q #H #a1 @(wf1_ind_nlt_aux … H) -H //
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/arith/nat_lt.ma".
+
+(* WELL-FOUNDED INDUCTION ***************************************************)
+
+fact wf2_ind_nlt_aux (A1) (A2) (f:A1→A2→nat) (Q:relation2 …):
+ (∀n. (∀a1,a2. f a1 a2 < n → Q a1 a2) → ∀a1,a2. f a1 a2 = n → Q a1 a2) →
+ ∀n,a1,a2. f a1 a2 = n → Q a1 a2.
+#A1 #A2 #f #Q #H #n @(nat_ind_lt … n) -n /3 width=3 by/
+qed-.
+
+(*** f2_ind *)
+lemma wf2_ind_nlt (A1) (A2) (f:A1→A2→nat) (Q:relation2 …):
+ (∀n. (∀a1,a2. f a1 a2 < n → Q a1 a2) → ∀a1,a2. f a1 a2 = n → Q a1 a2) →
+ ∀a1,a2. Q a1 a2.
+#A1 #A2 #f #Q #H #a1 #a2 @(wf2_ind_nlt_aux … H) -H //
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/arith/nat_lt.ma".
+
+(* WELL-FOUNDED INDUCTION ***************************************************)
+
+fact wf3_ind_nlt_aux (A1) (A2) (A3) (f:A1→A2→A3→nat) (Q:relation3 …):
+ (∀n. (∀a1,a2,a3. f a1 a2 a3 < n → Q a1 a2 a3) → ∀a1,a2,a3. f a1 a2 a3 = n → Q a1 a2 a3) →
+ ∀n,a1,a2,a3. f a1 a2 a3 = n → Q a1 a2 a3.
+#A1 #A2 #A3 #f #Q #H #n @(nat_ind_lt … n) -n /3 width=3 by/
+qed-.
+
+(*** f3_ind *)
+lemma wf3_ind_nlt (A1) (A2) (A3) (f:A1→A2→A3→nat) (Q:relation3 …):
+ (∀n. (∀a1,a2,a3. f a1 a2 a3 < n → Q a1 a2 a3) → ∀a1,a2,a3. f a1 a2 a3 = n → Q a1 a2 a3) →
+ ∀a1,a2,a3. Q a1 a2 a3.
+#A1 #A2 #A3 #f #Q #H #a1 #a2 #a3 @(wf3_ind_nlt_aux … H) -H //
+qed-.
projects / helm.git / commitdiff