From df7a2aa19e98dc28e7f22129275a175cead49e2d Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 19 Dec 2020 20:18:17 +0100 Subject: [PATCH] =?utf8?q?arithmetics=20for=20=CE=BB=CE=B4?= MIME-Version: 1.0 Content-Type: text/plain; charset=utf8 Content-Transfer-Encoding: 8bit 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 --- .../contribs/lambdadelta/ground/arith/nat.ma | 46 +++++++ .../contribs/lambdadelta/ground/arith/nat.txt | 128 ++++++++++++++++++ .../lambdadelta/ground/arith/nat_iter.ma | 44 ++++++ .../lambdadelta/ground/arith/nat_iter_succ.ma | 24 ++++ .../lambdadelta/ground/arith/nat_le.ma | 108 +++++++++++++++ .../lambdadelta/ground/arith/nat_le_plus.ma | 70 ++++++++++ .../lambdadelta/ground/arith/nat_lt.ma | 106 +++++++++++++++ .../lambdadelta/ground/arith/nat_plus.ma | 99 ++++++++++++++ .../lambdadelta/ground/arith/nat_succ.ma | 72 ++++++++++ .../contribs/lambdadelta/ground/arith/pnat.ma | 50 +++++++ .../lambdadelta/ground/arith/pnat_iter.ma | 43 ++++++ .../lambdadelta/ground/arith/pnat_plus.ma | 51 +++++++ .../ground/notation/functions/exp_3.ma | 27 ++++ .../ground/notation/functions/one_0.ma | 19 +++ .../ground/notation/functions/zero_0.ma | 19 +++ .../lambdadelta/ground/wf_ind/wf1_ind_nlt.ma | 30 ++++ .../lambdadelta/ground/wf_ind/wf2_ind_nlt.ma | 30 ++++ .../lambdadelta/ground/wf_ind/wf3_ind_nlt.ma | 30 ++++ 18 files changed, 996 insertions(+) create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/nat.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/nat.txt create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/nat_iter.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/nat_iter_succ.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/nat_le.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/nat_le_plus.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/nat_lt.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/nat_succ.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/pnat.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/pnat_iter.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/notation/functions/exp_3.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/notation/functions/one_0.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/notation/functions/zero_0.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/wf_ind/wf1_ind_nlt.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/wf_ind/wf2_ind_nlt.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/wf_ind/wf3_ind_nlt.ma diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat.ma new file mode 100644 index 000000000..1bc7286b6 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat.ma @@ -0,0 +1,46 @@ +(**************************************************************************) +(* ___ *) +(* ||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-. diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat.txt b/matita/matita/contribs/lambdadelta/ground/arith/nat.txt new file mode 100644 index 000000000..96c8c9cc3 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat.txt @@ -0,0 +1,128 @@ +"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" diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_iter.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_iter.ma new file mode 100644 index 000000000..89c464804 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_iter.ma @@ -0,0 +1,44 @@ +(**************************************************************************) +(* ___ *) +(* ||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 (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-. diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_le_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_le_plus.ma new file mode 100644 index 000000000..513ea5257 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_le_plus.ma @@ -0,0 +1,70 @@ +(**************************************************************************) +(* ___ *) +(* ||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_assoc >nplus_assoc "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 }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/one_0.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/one_0.ma new file mode 100644 index 000000000..1a6b8474b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/one_0.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/zero_0.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/zero_0.ma new file mode 100644 index 000000000..59b76ebb0 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/zero_0.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 }. diff --git a/matita/matita/contribs/lambdadelta/ground/wf_ind/wf1_ind_nlt.ma b/matita/matita/contribs/lambdadelta/ground/wf_ind/wf1_ind_nlt.ma new file mode 100644 index 000000000..352bbfdf6 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/wf_ind/wf1_ind_nlt.ma @@ -0,0 +1,30 @@ +(**************************************************************************) +(* ___ *) +(* ||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-. diff --git a/matita/matita/contribs/lambdadelta/ground/wf_ind/wf2_ind_nlt.ma b/matita/matita/contribs/lambdadelta/ground/wf_ind/wf2_ind_nlt.ma new file mode 100644 index 000000000..492c84cdb --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/wf_ind/wf2_ind_nlt.ma @@ -0,0 +1,30 @@ +(**************************************************************************) +(* ___ *) +(* ||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-. diff --git a/matita/matita/contribs/lambdadelta/ground/wf_ind/wf3_ind_nlt.ma b/matita/matita/contribs/lambdadelta/ground/wf_ind/wf3_ind_nlt.ma new file mode 100644 index 000000000..c125183b3 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/wf_ind/wf3_ind_nlt.ma @@ -0,0 +1,30 @@ +(**************************************************************************) +(* ___ *) +(* ||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-. -- 2.39.2