1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.tcs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "ground_2/notation/functions/apply_2.ma".
16 include "ground_2/relocation/nstream_eq.ma".
17 include "ground_2/relocation/rtmap_istot.ma".
19 (* RELOCATION N-STREAM ******************************************************)
21 rec definition apply (i: nat) on i: rtmap → nat ≝ ?.
24 | #i lapply (apply i f) -apply -i -f
29 interpretation "functional application (nstream)"
30 'Apply f i = (apply i f).
32 (* Specific properties on at ************************************************)
34 lemma at_O1: ∀i2,f. @⦃0, i2@f⦄ ≘ i2.
35 #i2 elim i2 -i2 /2 width=5 by at_refl, at_next/
38 lemma at_S1: ∀n,f,i1,i2. @⦃i1, f⦄ ≘ i2 → @⦃⫯i1, n@f⦄ ≘ ⫯(n+i2).
39 #n elim n -n /3 width=7 by at_push, at_next/
42 lemma at_total: ∀i1,f. @⦃i1, f⦄ ≘ f@❴i1❵.
44 [ * // | #i #IH * /3 width=1 by at_S1/ ]
47 lemma at_istot: ∀f. 𝐓⦃f⦄.
48 /2 width=2 by ex_intro/ qed.
50 lemma at_plus2: ∀f,i1,i,n,m. @⦃i1, n@f⦄ ≘ i → @⦃i1, (m+n)@f⦄ ≘ m+i.
51 #f #i1 #i #n #m #H elim m -m //
52 #m <plus_S1 /2 width=5 by at_next/ (**) (* full auto fails *)
55 (* Specific inversion lemmas on at ******************************************)
57 lemma at_inv_O1: ∀f,n,i2. @⦃0, n@f⦄ ≘ i2 → n = i2.
58 #f #n elim n -n /2 width=6 by at_inv_ppx/
59 #n #IH #i2 #H elim (at_inv_xnx … H) -H [2,3: // ]
60 #j2 #Hj * -i2 /3 width=1 by eq_f/
63 lemma at_inv_S1: ∀f,n,j1,i2. @⦃⫯j1, n@f⦄ ≘ i2 →
64 ∃∃j2. @⦃j1, f⦄ ≘ j2 & ⫯(n+j2) = i2.
65 #f #n elim n -n /2 width=5 by at_inv_npx/
66 #n #IH #j1 #i2 #H elim (at_inv_xnx … H) -H [2,3: // ]
67 #j2 #Hj * -i2 elim (IH … Hj) -IH -Hj
68 #i2 #Hi * -j2 /2 width=3 by ex2_intro/
71 lemma at_inv_total: ∀f,i1,i2. @⦃i1, f⦄ ≘ i2 → f@❴i1❵ = i2.
72 /2 width=6 by at_mono/ qed-.
74 (* Spercific forward lemmas on at *******************************************)
76 lemma at_increasing_plus: ∀f,n,i1,i2. @⦃i1, n@f⦄ ≘ i2 → i1 + n ≤ i2.
78 [ #i2 #H <(at_inv_O1 … H) -i2 //
79 | #i1 #i2 #H elim (at_inv_S1 … H) -H
80 #j1 #Ht * -i2 /4 width=2 by at_increasing, monotonic_le_plus_r, le_S_S/
84 lemma at_fwd_id: ∀f,n,i. @⦃i, n@f⦄ ≘ i → 0 = n.
85 #f #n #i #H elim (at_fwd_id_ex … H) -H
86 #g #H elim (push_inv_seq_dx … H) -H //
89 (* Basic properties *********************************************************)
91 lemma apply_eq_repl (i): eq_repl … (λf1,f2. f1@❴i❵ = f2@❴i❵).
92 #i elim i -i [2: #i #IH ] * #n1 #f1 * #n2 #f2 #H
93 elim (eq_inv_seq_aux … H) -H normalize //
94 #Hn #Hf /4 width=1 by eq_f2, eq_f/
97 lemma apply_S1: ∀f,i. (⫯f)@❴i❵ = ⫯(f@❴i❵).
101 (* Main inversion lemmas ****************************************************)
103 theorem apply_inj: ∀f,i1,i2,j. f@❴i1❵ = j → f@❴i2❵ = j → i1 = i2.
104 /2 width=4 by at_inj/ qed-.