1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "ground/notation/functions/apply_2.ma".
16 include "ground/relocation/tr_map.ma".
18 include "ground/arith/pnat_le_plus.ma".
19 include "ground/relocation/pstream_eq.ma".
20 include "ground/relocation/rtmap_istot.ma".
22 (* POSITIVE APPLICATION FOR TOTAL RELOCATION MAPS ***************************)
24 rec definition tr_pat (i: pnat) on i: tr_map → pnat.
27 | #i lapply (tr_pat i f) -tr_pat -i -f
33 "functional positive application (total relocation maps)"
34 'apply f i = (tr_pat i f).
36 (* Properties on at (specific) ************************************************)
38 lemma at_O1: ∀i2,f. @❪𝟏, i2⨮f❫ ≘ i2.
39 #i2 elim i2 -i2 /2 width=5 by gr_pat_refl, gr_pat_next/
42 lemma at_S1: ∀p,f,i1,i2. @❪i1, f❫ ≘ i2 → @❪↑i1, p⨮f❫ ≘ i2+p.
43 #p elim p -p /3 width=7 by gr_pat_push, gr_pat_next/
46 lemma at_total: ∀i1,f. @❪i1, f❫ ≘ f@❨i1❩.
48 [ * // | #i #IH * /3 width=1 by at_S1/ ]
51 lemma at_istot: ∀f. 𝐓❪f❫.
52 /2 width=2 by ex_intro/ qed.
54 lemma at_plus2: ∀f,i1,i,p,q. @❪i1, p⨮f❫ ≘ i → @❪i1, (p+q)⨮f❫ ≘ i+q.
55 #f #i1 #i #p #q #H elim q -q
56 /2 width=5 by gr_pat_next/
59 (* Inversion lemmas on at (specific) ******************************************)
61 lemma at_inv_O1: ∀f,p,i2. @❪𝟏, p⨮f❫ ≘ i2 → p = i2.
62 #f #p elim p -p /2 width=6 by gr_pat_inv_unit_push/
63 #p #IH #i2 #H elim (gr_pat_inv_next … H) -H [|*: // ]
64 #j2 #Hj * -i2 /3 width=1 by eq_f/
67 lemma at_inv_S1: ∀f,p,j1,i2. @❪↑j1, p⨮f❫ ≘ i2 →
68 ∃∃j2. @❪j1, f❫ ≘ j2 & j2+p = i2.
69 #f #p elim p -p /2 width=5 by gr_pat_inv_succ_push/
70 #p #IH #j1 #i2 #H elim (gr_pat_inv_next … H) -H [|*: // ]
71 #j2 #Hj * -i2 elim (IH … Hj) -IH -Hj
72 #i2 #Hi * -j2 /2 width=3 by ex2_intro/
75 lemma at_inv_total: ∀f,i1,i2. @❪i1, f❫ ≘ i2 → f@❨i1❩ = i2.
76 /2 width=6 by fr2_nat_mono/ qed-.
78 (* Forward lemmas on at (specific) *******************************************)
80 lemma at_increasing_plus: ∀f,p,i1,i2. @❪i1, p⨮f❫ ≘ i2 → i1 + p ≤ ↑i2.
82 [ #i2 #H <(at_inv_O1 … H) -i2 //
83 | #i1 #i2 #H elim (at_inv_S1 … H) -H
84 #j1 #Ht * -i2 <pplus_succ_sn
85 /4 width=2 by gr_pat_increasing, ple_plus_bi_dx, ple_succ_bi/
89 lemma at_fwd_id: ∀f,p,i. @❪i, p⨮f❫ ≘ i → 𝟏 = p.
90 #f #p #i #H elim (gr_pat_des_id … H) -H
91 #g #H elim (push_inv_seq_dx … H) -H //
94 (* Basic properties *********************************************************)
96 lemma tr_pat_O1: ∀p,f. (p⨮f)@❨𝟏❩ = p.
99 lemma tr_pat_S1: ∀p,f,i. (p⨮f)@❨↑i❩ = f@❨i❩+p.
102 lemma tr_pat_eq_repl (i): gr_eq_repl … (λf1,f2. f1@❨i❩ = f2@❨i❩).
103 #i elim i -i [2: #i #IH ] * #p1 #f1 * #p2 #f2 #H
104 elim (eq_inv_seq_aux … H) -H #Hp #Hf //
105 >tr_pat_S1 >tr_pat_S1 /3 width=1 by eq_f2/
108 lemma tr_pat_S2: ∀f,i. (↑f)@❨i❩ = ↑(f@❨i❩).
112 (* Main inversion lemmas ****************************************************)
114 theorem tr_pat_inj: ∀f,i1,i2,j. f@❨i1❩ = j → f@❨i2❩ = j → i1 = i2.
115 /2 width=4 by gr_pat_inj/ qed-.
117 corec theorem nstream_eq_inv_ext: ∀f1,f2. (∀i. f1@❨i❩ = f2@❨i❩) → f1 ≗ f2.
118 * #p1 #f1 * #p2 #f2 #Hf @stream_eq_cons
120 | @nstream_eq_inv_ext -nstream_eq_inv_ext #i
121 ltr_pat (Hf (𝟏)) >tr_pat_O1 >tr_pat_O1 #H destruct
122 ltr_pat (Hf (↑i)) >tr_pat_S1 >tr_pat_S1 #H
123 /3 width=2 by eq_inv_pplus_bi_dx, eq_inv_psucc_bi/