From 750305d95b8f6bb40b5be0e9dfd05d42b256f2a1 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 13 Jan 2016 20:33:18 +0000 Subject: [PATCH] - ng_kernel: catched Invalid_argument "List.nth" in typeof of Rel i (raied when i < 1) - ground_1: relocation with streams of natural numbers begins --- .../components/ng_kernel/nCicTypeChecker.ml | 2 +- .../lambdadelta/ground_2/lib/arith.ma | 16 ++ .../lambdadelta/ground_2/lib/streams.ma | 82 ++++++ .../lambdadelta/ground_2/lib/streams_hdtl.ma | 34 +++ .../ground_2/notation/relations/exteq_3.ma | 27 ++ .../ground_2/relocation/nstream.ma | 20 ++ .../ground_2/relocation/nstream_at.ma | 244 ++++++++++++++++++ 7 files changed, 424 insertions(+), 1 deletion(-) create mode 100644 matita/matita/contribs/lambdadelta/ground_2/lib/streams.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/lib/streams_hdtl.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/notation/relations/exteq_3.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/relocation/nstream.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_at.ma diff --git a/matita/components/ng_kernel/nCicTypeChecker.ml b/matita/components/ng_kernel/nCicTypeChecker.ml index e334861cb..6871dc6ee 100644 --- a/matita/components/ng_kernel/nCicTypeChecker.ml +++ b/matita/components/ng_kernel/nCicTypeChecker.ml @@ -391,7 +391,7 @@ let rec typeof (status:#NCic.status) ~subst ~metasenv context term = match List.nth context (n - 1) with | (_,C.Decl ty) -> S.lift status n ty | (_,C.Def (_,ty)) -> S.lift status n ty - with Failure _ -> + with Failure _ | Invalid_argument _ -> raise (TypeCheckerFailure (lazy ("unbound variable " ^ string_of_int n ^" under: " ^ status#ppcontext ~metasenv ~subst context)))) | C.Sort s -> diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma index 5f8451a27..d181e88cf 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma @@ -106,6 +106,9 @@ lemma monotonic_lt_pred: ∀m,n. m < n → O < m → pred m < pred n. @le_S_S_to_le >S_pred /2 width=3 by transitive_lt/ qed. +lemma lt_S_S: ∀x,y. x < y → ⫯x < ⫯y. +/2 width=1 by le_S_S/ qed. + lemma arith_j: ∀x,y,z. x-y-1 ≤ x-(y-z)-1. /3 width=1 by monotonic_le_minus_l, monotonic_le_minus_r/ qed. @@ -174,6 +177,19 @@ lemma zero_eq_plus: ∀x,y. 0 = x + y → 0 = x ∧ 0 = y. * /2 width=1 by conj/ #x #y normalize #H destruct qed-. +lemma lt_S_S_to_lt: ∀x,y. ⫯x < ⫯y → x < y. +/2 width=1 by le_S_S_to_le/ qed-. + +lemma lt_elim: ∀R:relation nat. + (∀n2. R O (⫯n2)) → + (∀n1,n2. R n1 n2 → R (⫯n1) (⫯n2)) → + ∀n2,n1. n1 < n2 → R n1 n2. +#R #IH1 #IH2 #n2 elim n2 -n2 +[ #n1 #H elim (lt_le_false … H) -H // +| #n2 #IH * /4 width=1 by lt_S_S_to_lt/ +] +qed-. + (* Iterators ****************************************************************) (* Note: see also: lib/arithemetics/bigops.ma *) diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/streams.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/streams.ma new file mode 100644 index 000000000..30a045c54 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/streams.ma @@ -0,0 +1,82 @@ +(**************************************************************************) +(* ___ *) +(* ||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_2/notation/constructors/cons_2.ma". +include "ground_2/notation/relations/exteq_3.ma". +include "ground_2/lib/star.ma". + +(* STREAMS ******************************************************************) + +coinductive stream (A:Type[0]): Type[0] ≝ +| seq: A → stream A → stream A +. + +interpretation "cons (nstream)" 'Cons b t = (seq ? b t). + +coinductive eq_stream (A): relation (stream A) ≝ +| eq_sec: ∀t1,t2,b1,b2. b1 = b2 → eq_stream A t1 t2 → eq_stream A (b1@t1) (b2@t2) +. + +interpretation "extensional equivalence (nstream)" + 'ExtEq A t1 t2 = (eq_stream A t1 t2). + +definition eq_stream_repl_back (A) (R:predicate …) (t1,t2) ≝ + t1 ≐⦋A⦌ t2 → R t1 → R t2. + +definition eq_stream_repl_fwd (A) (R:predicate …) (t1,t2) ≝ + t2 ≐⦋A⦌ t1 → R t1 → R t2. + +(* Basic inversion lemmas ***************************************************) + +fact eq_stream_inv_seq_aux: ∀A,t1,t2. t1 ≐⦋A⦌ t2 → + ∀u1,u2,a1,a2. t1 = a1@u1 → t2 = a2@u2 → + a1 = a2 ∧ u1 ≐ u2. +#A #t1 #t2 * -t1 -t2 +#t1 #t2 #b1 #b2 #Hb #Ht #u1 #u2 #a1 #a2 #H1 #H2 destruct /2 width=1 by conj/ +qed-. + +lemma eq_stream_inv_seq: ∀A,t1,t2,b1,b2. b1@t1 ≐⦋A⦌ b2@t2 → b1 = b2 ∧ t1 ≐ t2. +/2 width=5 by eq_stream_inv_seq_aux/ qed-. + +(* Basic properties *********************************************************) + +lemma stream_expand (A) (t:stream A): t = match t with [ seq a u ⇒ a @ u ]. +#A * // +qed. + +let corec eq_stream_refl: ∀A. reflexive … (eq_stream A) ≝ ?. +#A * #b #t @eq_sec // +qed. + +let corec eq_stream_sym: ∀A. symmetric … (eq_stream A) ≝ ?. +#A #t1 #t2 * -t1 -t2 +#t1 #t2 #b1 #b2 #Hb #Ht @eq_sec /2 width=1 by/ +qed-. + +lemma eq_stream_repl_sym: ∀A,R,t1,t2. eq_stream_repl_back A R t1 t2 → eq_stream_repl_fwd A R t1 t2. +/3 width=1 by eq_stream_sym/ qed-. + +(* Main properties **********************************************************) + +let corec eq_stream_trans: ∀A. Transitive … (eq_stream A) ≝ ?. +#A #t1 #t * -t1 -t +#t1 #t #b1 #b #Hb1 #Ht1 * #b2 #t2 #H cases (eq_stream_inv_seq A … H) -H +#Hb2 #Ht2 @eq_sec /2 width=3 by/ +qed-. + +theorem eq_stream_canc_sn: ∀A,t,t1,t2. t ≐ t1 → t ≐ t2 → t1 ≐⦋A⦌ t2. +/3 width=4 by eq_stream_trans, eq_stream_repl_sym/ qed-. + +theorem eq_stream_canc_dx: ∀A,t,t1,t2. t1 ≐ t → t2 ≐ t → t1 ≐⦋A⦌ t2. +/3 width=4 by eq_stream_trans, eq_stream_repl_sym/ qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/streams_hdtl.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/streams_hdtl.ma new file mode 100644 index 000000000..90af6fd87 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/streams_hdtl.ma @@ -0,0 +1,34 @@ +(**************************************************************************) +(* ___ *) +(* ||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_2/lib/streams.ma". +include "ground_2/lib/arith.ma". + +(* STREAMS ******************************************************************) + +definition hd (A:Type[0]): stream A → A ≝ + λt. match t with [ seq a _ ⇒ a ]. + +definition tl (A:Type[0]): stream A → stream A ≝ + λt. match t with [ seq _ t ⇒ t ]. + +let rec tln (A:Type[0]) (i:nat) on i: stream A → stream A ≝ ?. +cases i -i [ #t @t | #i * #_ #t @(tln … i t) ] +qed. + +(* basic properties *********************************************************) + +lemma eq_stream_split (A) (t): (hd … t) @ (tl … t) ≐⦋A⦌ t. +#A * // +qed. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/relations/exteq_3.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/relations/exteq_3.ma new file mode 100644 index 000000000..39597d89f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/relations/exteq_3.ma @@ -0,0 +1,27 @@ +(**************************************************************************) +(* ___ *) +(* ||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( v1 ≐ break term 46 v2 )" + non associative with precedence 45 + for @{ 'ExtEq $M $v1 $v2 }. + +notation > "hvbox( v1 ≐ break term 46 v2 )" + non associative with precedence 45 + for @{ 'ExtEq ? $v1 $v2 }. + +notation > "hvbox( v1 ≐ break ⦋ term 46 M ⦌ break term 46 v2 )" + non associative with precedence 45 + for @{ 'ExtEq $M $v1 $v2 }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream.ma new file mode 100644 index 000000000..ccd8857a8 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream.ma @@ -0,0 +1,20 @@ +(**************************************************************************) +(* ___ *) +(* ||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_2/lib/arith.ma". +include "ground_2/lib/streams.ma". + +(* RELOCATION N-STREAM ******************************************************) + +definition nstream: Type[0] ≝ stream nat. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_at.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_at.ma new file mode 100644 index 000000000..60f206aab --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_at.ma @@ -0,0 +1,244 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.tcs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "ground_2/notation/functions/apply_2.ma". +include "ground_2/notation/relations/rat_3.ma". +include "ground_2/relocation/nstream.ma". + +(* RELOCATION N-STREAM ******************************************************) + +let rec apply (i: nat) on i: nstream → nat ≝ ?. +* #b #t cases i -i +[ @b +| #i lapply (apply i t) -apply -i -t + #i @(⫯(b+i)) +] +qed. + +interpretation "functional application (nstream)" + 'Apply t i = (apply i t). + +inductive at: nstream → relation nat ≝ +| at_zero: ∀t. at (0 @ t) 0 0 +| at_skip: ∀t,i1,i2. at t i1 i2 → at (0 @ t) (⫯i1) (⫯i2) +| at_lift: ∀t,b,i1,i2. at (b @ t) i1 i2 → at (⫯b @ t) i1 (⫯i2) +. + +interpretation "relational application (nstream)" + 'RAt i1 t i2 = (at t i1 i2). + +(* Basic properties on apply ************************************************) + +lemma apply_S1: ∀t,a,i. (⫯a@t)@❴i❵ = ⫯((a@t)@❴i❵). +#a #t * // +qed. + +(* Basic inversion lemmas on at *********************************************) + +fact at_inv_xOx_aux: ∀t,i1,i2. @⦃i1, t⦄ ≡ i2 → ∀u. t = 0 @ u → + (i1 = 0 ∧ i2 = 0) ∨ + ∃∃j1,j2. @⦃j1, u⦄ ≡ j2 & i1 = ⫯j1 & i2 = ⫯j2. +#t #i1 #i2 * -t -i1 -i2 +[ /3 width=1 by or_introl, conj/ +| #t #i1 #i2 #Hi #u #H destruct /3 width=5 by ex3_2_intro, or_intror/ +| #t #b #i1 #i2 #_ #u #H destruct +] +qed-. + +lemma at_inv_xOx: ∀t,i1,i2. @⦃i1, 0 @ t⦄ ≡ i2 → + (i1 = 0 ∧ i2 = 0) ∨ + ∃∃j1,j2. @⦃j1, t⦄ ≡ j2 & i1 = ⫯j1 & i2 = ⫯j2. +/2 width=3 by at_inv_xOx_aux/ qed-. + +lemma at_inv_OOx: ∀t,i. @⦃0, 0 @ t⦄ ≡ i → i = 0. +#t #i #H elim (at_inv_xOx … H) -H * // +#j1 #j2 #_ #H destruct +qed-. + +lemma at_inv_xOO: ∀t,i. @⦃i, 0 @ t⦄ ≡ 0 → i = 0. +#t #i #H elim (at_inv_xOx … H) -H * // +#j1 #j2 #_ #_ #H destruct +qed-. + +lemma at_inv_SOx: ∀t,i1,i2. @⦃⫯i1, 0 @ t⦄ ≡ i2 → + ∃∃j2. @⦃i1, t⦄ ≡ j2 & i2 = ⫯j2. +#t #i1 #i2 #H elim (at_inv_xOx … H) -H * +[ #H destruct +| #j1 #j2 #Hj #H1 #H2 destruct /2 width=3 by ex2_intro/ +] +qed-. + +lemma at_inv_xOS: ∀t,i1,i2. @⦃i1, 0 @ t⦄ ≡ ⫯i2 → + ∃∃j1. @⦃j1, t⦄ ≡ i2 & i1 = ⫯j1. +#t #i1 #i2 #H elim (at_inv_xOx … H) -H * +[ #_ #H destruct +| #j1 #j2 #Hj #H1 #H2 destruct /2 width=3 by ex2_intro/ +] +qed-. + +lemma at_inv_SOS: ∀t,i1,i2. @⦃⫯i1, 0 @ t⦄ ≡ ⫯i2 → @⦃i1, t⦄ ≡ i2. +#t #i1 #i2 #H elim (at_inv_xOx … H) -H * +[ #H destruct +| #j1 #j2 #Hj #H1 #H2 destruct // +] +qed-. + +lemma at_inv_OOS: ∀t,i. @⦃0, 0 @ t⦄ ≡ ⫯i → ⊥. +#t #i #H elim (at_inv_xOx … H) -H * +[ #_ #H destruct +| #j1 #j2 #_ #H destruct +] +qed-. + +lemma at_inv_SOO: ∀t,i. @⦃⫯i, 0 @ t⦄ ≡ 0 → ⊥. +#t #i #H elim (at_inv_xOx … H) -H * +[ #H destruct +| #j1 #j2 #_ #_ #H destruct +] +qed-. + +fact at_inv_xSx_aux: ∀t,i1,i2. @⦃i1, t⦄ ≡ i2 → ∀u,a. t = ⫯a @ u → + ∃∃j2. @⦃i1, a@u⦄ ≡ j2 & i2 = ⫯j2. +#t #i1 #i2 * -t -i1 -i2 +[ #t #u #a #H destruct +| #t #i1 #i2 #_ #u #a #H destruct +| #t #b #i1 #i2 #Hi #u #a #H destruct /2 width=3 by ex2_intro/ +] +qed-. + +lemma at_inv_xSx: ∀t,b,i1,i2. @⦃i1, ⫯b @ t⦄ ≡ i2 → + ∃∃j2. @⦃i1, b @ t⦄ ≡ j2 & i2 = ⫯j2. +/2 width=3 by at_inv_xSx_aux/ qed-. + +lemma at_inv_xSS: ∀t,b,i1,i2. @⦃i1, ⫯b @ t⦄ ≡ ⫯i2 → @⦃i1, b@t⦄ ≡ i2. +#t #b #i1 #i2 #H elim (at_inv_xSx … H) -H +#j2 #Hj #H destruct // +qed-. + +lemma at_inv_xSO: ∀t,b,i. @⦃i, ⫯b @ t⦄ ≡ 0 → ⊥. +#t #b #i #H elim (at_inv_xSx … H) -H +#j2 #_ #H destruct +qed-. + +(* alternative definition ***************************************************) + +lemma at_O1: ∀b,t. @⦃0, b @ t⦄ ≡ b. +#b elim b -b /2 width=1 by at_lift/ +qed. + +lemma at_S1: ∀b,t,i1,i2. @⦃i1, t⦄ ≡ i2 → @⦃⫯i1, b@t⦄ ≡ ⫯(b+i2). +#b elim b -b /3 width=1 by at_skip, at_lift/ +qed. + +lemma at_inv_O1: ∀t,b,i2. @⦃0, b@t⦄ ≡ i2 → i2 = b. +#t #b elim b -b /2 width=2 by at_inv_OOx/ +#b #IH #i2 #H elim (at_inv_xSx … H) -H +#j2 #Hj #H destruct /3 width=1 by eq_f/ +qed-. + +lemma at_inv_S1: ∀t,b,j1,i2. @⦃⫯j1, b@t⦄ ≡ i2 → ∃∃j2. @⦃j1, t⦄ ≡ j2 & i2 =⫯(b+j2). +#t #b elim b -b /2 width=1 by at_inv_SOx/ +#b #IH #j1 #i2 #H elim (at_inv_xSx … H) -H +#j2 #Hj #H destruct elim (IH … Hj) -IH -Hj +#i2 #Hi #H destruct /2 width=3 by ex2_intro/ +qed-. + +lemma at_total: ∀i,t. @⦃i, t⦄ ≡ t@❴i❵. +#i elim i -i +[ * // | #i #IH * /3 width=1 by at_S1/ ] +qed. + +(* Advanced forward lemmas on at ********************************************) + +lemma at_increasing: ∀t,i1,i2. @⦃i1, t⦄ ≡ i2 → i1 ≤ i2. +#t #i1 #i2 #H elim H -t -i1 -i2 /2 width=1 by le_S_S, le_S/ +qed-. + +lemma at_increasing_plus: ∀t,b,i1,i2. @⦃i1, b@t⦄ ≡ i2 → i1 + b ≤ i2. +#t #b * +[ #i2 #H >(at_inv_O1 … H) -i2 // +| #i1 #i2 #H elim (at_inv_S1 … H) -H + #j1 #Ht #H destruct + /4 width=2 by at_increasing, monotonic_le_plus_r, le_S_S/ +] +qed-. + +lemma at_increasing_strict: ∀t,b,i1,i2. @⦃i1, ⫯b @ t⦄ ≡ i2 → + i1 < i2 ∧ @⦃i1, b@t⦄ ≡ ⫰i2. +#t #b #i1 #i2 #H elim (at_inv_xSx … H) -H +#j2 #Hj #H destruct /4 width=2 by conj, at_increasing, le_S_S/ +qed-. + +(* Main properties on at ****************************************************) + +let corec at_ext: ∀t1,t2. (∀i,i1,i2. @⦃i, t1⦄ ≡ i1 → @⦃i, t2⦄ ≡ i2 → i1 = i2) → t1 ≐ t2 ≝ ?. +* #b1 #t1 * #b2 #t2 #Hi lapply (Hi 0 b1 b2 ? ?) // +#H lapply (at_ext t1 t2 ?) /2 width=1 by eq_sec/ -at_ext +#j #j1 #j2 #H1 #H2 @(injective_plus_r … b2) /4 width=5 by at_S1, injective_S/ (**) (* full auto fails *) +qed-. + +theorem at_monotonic: ∀i1,i2. i1 < i2 → ∀t,j1,j2. @⦃i1, t⦄ ≡ j1 → @⦃i2, t⦄ ≡ j2 → j1 < j2. +#i1 #i2 #H @(lt_elim … H) -i1 -i2 +[ #i2 *#b #t #j1 #j2 #H1 #H2 >(at_inv_O1 … H1) elim (at_inv_S1 … H2) -H2 -j1 // +| #i1 #i2 #IH * #b #t #j1 #j2 #H1 #H2 elim (at_inv_S1 … H2) elim (at_inv_S1 … H1) -H1 -H2 + #x1 #Hx1 #H1 #x2 #Hx2 #H2 destruct /4 width=3 by lt_S_S, monotonic_lt_plus_r/ +] +qed-. + +theorem at_inv_monotonic: ∀t,i1,j1. @⦃i1, t⦄ ≡ j1 → ∀i2,j2. @⦃i2, t⦄ ≡ j2 → j2 < j1 → i2 < i1. +#t #i1 #j1 #H elim H -t -i1 -j1 +[ #t #i2 #j2 #_ #H elim (lt_le_false … H) // +| #t #i1 #j1 #_ #IH #i2 #j2 #H #Hj elim (at_inv_xOx … H) -H * + [ #H1 #H2 destruct // + | #x2 #y2 #Hxy #H1 #H2 destruct /4 width=3 by lt_S_S_to_lt, lt_S_S/ + ] +| #t #b1 #i1 #j1 #_ #IH #i2 #j2 #H #Hj elim (at_inv_xSx … H) -H + #y2 #Hy #H destruct /3 width=3 by lt_S_S_to_lt/ +] +qed-. + +theorem at_mono: ∀t,i,i1. @⦃i, t⦄ ≡ i1 → ∀i2. @⦃i, t⦄ ≡ i2 → i2 = i1. +#t #i #i1 #H1 #i2 #H2 elim (lt_or_eq_or_gt i2 i1) // +#Hi elim (lt_le_false i i) /2 width=6 by at_inv_monotonic/ +qed-. + +theorem at_inj: ∀t,i1,i. @⦃i1, t⦄ ≡ i → ∀i2. @⦃i2, t⦄ ≡ i → i1 = i2. +#t #i1 #i #H1 #i2 #H2 elim (lt_or_eq_or_gt i2 i1) // +#Hi elim (lt_le_false i i) /2 width=6 by at_monotonic/ +qed-. + +(* Advanced properties on at ************************************************) + +(* Note: see also: trace_at/at_dec *) +lemma at_dec: ∀t,i1,i2. Decidable (@⦃i1, t⦄ ≡ i2). +#t #i1 #i2 lapply (at_total i1 t) +#Ht elim (eq_nat_dec i2 (t@❴i1❵)) +[ #H destruct /2 width=1 by or_introl/ +| /4 width=4 by at_mono, or_intror/ +] +qed-. + +lemma is_at_dec_le: ∀t,i2,i. (∀i1. i1 + i ≤ i2 → @⦃i1, t⦄ ≡ i2 → ⊥) → Decidable (∃i1. @⦃i1, t⦄ ≡ i2). +#t #i2 #i elim i -i +[ #Ht @or_intror * /3 width=3 by at_increasing/ +| #i #IH #Ht elim (at_dec t (i2-i) i2) /3 width=2 by ex_intro, or_introl/ + #Hi2 @IH -IH #i1 #H #Hi elim (le_to_or_lt_eq … H) -H /2 width=3 by/ + #H destruct -Ht /2 width=1 by/ +] +qed-. + +(* Note: see also: trace_at/is_at_dec *) +lemma is_at_dec: ∀t,i2. Decidable (∃i1. @⦃i1, t⦄ ≡ i2). +#t #i2 @(is_at_dec_le ? ? (⫯i2)) /2 width=4 by lt_le_false/ +qed-. -- 2.39.2