matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_id.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "ground_2/notation/functions/identity_0.ma".
  16 include "ground_2/notation/relations/isidentity_1.ma".
  17 include "ground_2/relocation/nstream_after.ma".
  18
  19 (* RELOCATION N-STREAM ******************************************************)
  20
  21 let corec id: rtmap ≝ ↑id.
  22
  23 interpretation "identity (nstream)"
  24    'Identity = (id).
  25
  26 definition isid: predicate rtmap ≝ λf. f ≐ 𝐈𝐝.
  27
  28 interpretation "test for identity (trace)"
  29    'IsIdentity f = (isid f).
  30
  31 (* Basic properties on id ***************************************************)
  32
  33 lemma id_unfold: 𝐈𝐝 = ↑𝐈𝐝.
  34 >(stream_expand … (𝐈𝐝)) in ⊢ (??%?); normalize //
  35 qed.
  36
  37 (* Basic properties on isid *************************************************)
  38
  39 lemma isid_id: 𝐈⦃𝐈𝐝⦄.
  40 // qed.
  41
  42 lemma isid_push: ∀f. 𝐈⦃f⦄ → 𝐈⦃↑f⦄.
  43 #f #H normalize >id_unfold /2 width=1 by eq_seq/
  44 qed.
  45
  46 (* Basic inversion lemmas on isid *******************************************)
  47
  48 lemma isid_inv_seq: ∀f,n.  𝐈⦃n@f⦄ → 𝐈⦃f⦄ ∧ n = 0.
  49 #f #n normalize >id_unfold in ⊢ (???%→?);
  50 #H elim (eq_stream_inv_seq ????? H) -H /2 width=1 by conj/
  51 qed-.
  52
  53 lemma isid_inv_push: ∀f. 𝐈⦃↑f⦄ → 𝐈⦃f⦄.
  54 * #n #f #H elim (isid_inv_seq … H) -H //
  55 qed-.
  56
  57 lemma isid_inv_next: ∀f. 𝐈⦃⫯f⦄ → ⊥.
  58 * #n #f #H elim (isid_inv_seq … H) -H
  59 #_ #H destruct
  60 qed-.
  61
  62 (* inversion lemmas on at ***************************************************)
  63
  64 let corec id_inv_at: ∀f. (∀i. @⦃i, f⦄ ≡ i) → f ≐ 𝐈𝐝 ≝ ?.
  65 * #n #f #Ht lapply (Ht 0)
  66 #H lapply (at_inv_O1 … H) -H
  67 #H0 >id_unfold @eq_seq
  68 [ cases H0 -n //
  69 | @id_inv_at -id_inv_at
  70   #i lapply (Ht (⫯i)) -Ht cases H0 -n
  71   #H elim (at_inv_SOx … H) -H //
  72 ]
  73 qed-.
  74
  75 lemma isid_inv_at: ∀i,f. 𝐈⦃f⦄ → @⦃i, f⦄ ≡ i.
  76 #i elim i -i
  77 [ * #n #f #H elim (isid_inv_seq … H) -H //
  78 | #i #IH * #n #f #H elim (isid_inv_seq … H) -H
  79   /3 width=1 by at_S1/
  80 ]
  81 qed-.
  82
  83 lemma isid_inv_at_mono: ∀f,i1,i2. 𝐈⦃f⦄ → @⦃i1, f⦄ ≡ i2 → i1 = i2.
  84 /3 width=6 by isid_inv_at, at_mono/ qed-.
  85
  86 (* Properties on at *********************************************************)
  87
  88 lemma id_at: ∀i. @⦃i, 𝐈𝐝⦄ ≡ i.
  89 /2 width=1 by isid_inv_at/ qed.
  90
  91 lemma isid_at: ∀f. (∀i. @⦃i, f⦄ ≡ i) → 𝐈⦃f⦄.
  92 /2 width=1 by id_inv_at/ qed.
  93
  94 lemma isid_at_total: ∀f. (∀i1,i2. @⦃i1, f⦄ ≡ i2 → i1 = i2) → 𝐈⦃f⦄.
  95 #f #Ht @isid_at
  96 #i lapply (at_total i f)
  97 #H >(Ht … H) in ⊢ (???%); -Ht //
  98 qed.
  99
 100 (* Properties on after ******************************************************)
 101
 102 lemma after_isid_dx: ∀f2,f1,f. f2 ⊚ f1 ≡ f → f2 ≐ f → 𝐈⦃f1⦄.
 103 #f2 #f1 #f #Ht #H2 @isid_at_total
 104 #i1 #i2 #Hi12 elim (after_at1_fwd … Hi12 … Ht) -f1
 105 /3 width=6 by at_inj, eq_stream_sym/
 106 qed.
 107
 108 lemma after_isid_sn: ∀f2,f1,f. f2 ⊚ f1 ≡ f → f1 ≐ f → 𝐈⦃f2⦄.
 109 #f2 #f1 #f #Ht #H1 @isid_at_total
 110 #i2 #i #Hi2 lapply (at_total i2 f1)
 111 #H0 lapply (at_increasing … H0)
 112 #Ht1 lapply (after_fwd_at2 … (f1@❴i2❵) … H0 … Ht)
 113 /3 width=7 by at_repl_back, at_mono, at_id_le/
 114 qed.
 115
 116 (* Inversion lemmas on after ************************************************)
 117
 118 let corec isid_after_sn: ∀f1,f2. 𝐈⦃f1⦄ → f1 ⊚ f2 ≡ f2 ≝ ?.
 119 * #n1 #f1 * * [ | #n2 ] #f2 #H cases (isid_inv_seq … H) -H
 120 /3 width=7 by after_push, after_refl/
 121 qed-.
 122
 123 let corec isid_after_dx: ∀f2,f1. 𝐈⦃f2⦄ → f1 ⊚ f2 ≡ f1 ≝ ?.
 124 * #n2 #f2 * *
 125 [ #f1 #H cases (isid_inv_seq … H) -H
 126   /3 width=7 by after_refl/
 127 | #n1 #f1 #H @after_next [4,5: // |1,2: skip ] /2 width=1 by/
 128 ]
 129 qed-.
 130
 131 lemma after_isid_inv_sn: ∀f1,f2,f. f1 ⊚ f2 ≡ f →  𝐈⦃f1⦄ → f2 ≐ f.
 132 /3 width=4 by isid_after_sn, after_mono/
 133 qed-.
 134
 135 lemma after_isid_inv_dx: ∀f1,f2,f. f1 ⊚ f2 ≡ f →  𝐈⦃f2⦄ → f1 ≐ f.
 136 /3 width=4 by isid_after_dx, after_mono/
 137 qed-.
 138 (*
 139 lemma after_inv_isid3: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃t⦄ → 𝐈⦃t1⦄ ∧ 𝐈⦃t2⦄.
 140 qed-.
 141 *)