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_lift.ma".
  18 include "ground_2/relocation/nstream_after.ma".
  19
  20 (* RELOCATION N-STREAM ******************************************************)
  21
  22 let corec id: nstream ≝ ↑id.
  23
  24 interpretation "identity (nstream)"
  25    'Identity = (id).
  26
  27 definition isid: predicate nstream ≝ λt. t ≐ 𝐈𝐝.
  28
  29 interpretation "test for identity (trace)"
  30    'IsIdentity t = (isid t).
  31
  32 (* Basic properties on id ***************************************************)
  33
  34 lemma id_unfold: 𝐈𝐝 = ↑𝐈𝐝.
  35 >(stream_expand … (𝐈𝐝)) in ⊢ (??%?); normalize //
  36 qed.
  37
  38 (* Basic properties on isid *************************************************)
  39
  40 lemma isid_id: 𝐈⦃𝐈𝐝⦄.
  41 // qed.
  42
  43 lemma isid_push: ∀t. 𝐈⦃t⦄ → 𝐈⦃↑t⦄.
  44 #t #H normalize >id_unfold /2 width=1 by eq_seq/
  45 qed.
  46
  47 (* Basic inversion lemmas on isid *******************************************)
  48
  49 lemma isid_inv_seq: ∀t,a.  𝐈⦃a@t⦄ → 𝐈⦃t⦄ ∧ a = 0.
  50 #t #a normalize >id_unfold in ⊢ (???%→?);
  51 #H elim (eq_stream_inv_seq ????? H) -H /2 width=1 by conj/
  52 qed-.
  53
  54 lemma isid_inv_push: ∀t. 𝐈⦃↑t⦄ → 𝐈⦃t⦄.
  55 * #a #t #H elim (isid_inv_seq … H) -H //
  56 qed-.
  57
  58 lemma isid_inv_next: ∀t. 𝐈⦃⫯t⦄ → ⊥.
  59 * #a #t #H elim (isid_inv_seq … H) -H
  60 #_ #H destruct
  61 qed-.
  62
  63 (* inversion lemmas on at ***************************************************)
  64
  65 let corec id_inv_at: ∀t. (∀i. @⦃i, t⦄ ≡ i) → t ≐ 𝐈𝐝 ≝ ?.
  66 * #a #t #Ht lapply (Ht 0)
  67 #H lapply (at_inv_O1 … H) -H
  68 #H0 >id_unfold @eq_seq
  69 [ cases H0 -a //
  70 | @id_inv_at -id_inv_at
  71   #i lapply (Ht (⫯i)) -Ht cases H0 -a
  72   #H elim (at_inv_SOx … H) -H //
  73 ]
  74 qed-.
  75
  76 lemma isid_inv_at: ∀i,t. 𝐈⦃t⦄ → @⦃i, t⦄ ≡ i.
  77 #i elim i -i
  78 [ * #a #t #H elim (isid_inv_seq … H) -H //
  79 | #i #IH * #a #t #H elim (isid_inv_seq … H) -H
  80   /3 width=1 by at_S1/
  81 ]
  82 qed-.
  83
  84 lemma isid_inv_at_mono: ∀t,i1,i2. 𝐈⦃t⦄ → @⦃i1, t⦄ ≡ i2 → i1 = i2.
  85 /3 width=6 by isid_inv_at, at_mono/ qed-.
  86
  87 (* Properties on at *********************************************************)
  88
  89 lemma id_at: ∀i. @⦃i, 𝐈𝐝⦄ ≡ i.
  90 /2 width=1 by isid_inv_at/ qed.
  91
  92 lemma isid_at: ∀t. (∀i. @⦃i, t⦄ ≡ i) → 𝐈⦃t⦄.
  93 /2 width=1 by id_inv_at/ qed.
  94
  95 lemma isid_at_total: ∀t. (∀i1,i2. @⦃i1, t⦄ ≡ i2 → i1 = i2) → 𝐈⦃t⦄.
  96 #t #Ht @isid_at
  97 #i lapply (at_total i t)
  98 #H >(Ht … H) in ⊢ (???%); -Ht //
  99 qed.
 100
 101 (* Properties on after ******************************************************)
 102
 103 lemma after_isid_dx: ∀t2,t1,t. t2 ⊚ t1 ≡ t → t2 ≐ t → 𝐈⦃t1⦄.
 104 #t2 #t1 #t #Ht #H2 @isid_at_total
 105 #i1 #i2 #Hi12 elim (after_at1_fwd … Hi12 … Ht) -t1
 106 /3 width=6 by at_inj, eq_stream_sym/
 107 qed.
 108
 109 lemma after_isid_sn: ∀t2,t1,t. t2 ⊚ t1 ≡ t → t1 ≐ t → 𝐈⦃t2⦄.
 110 #t2 #t1 #t #Ht #H1 @isid_at_total
 111 #i2 #i #Hi2 lapply (at_total i2 t1)
 112 #H0 lapply (at_increasing … H0)
 113 #Ht1 lapply (after_fwd_at2 … (t1@❴i2❵) … H0 … Ht)
 114 /3 width=7 by at_repl_back, at_mono, at_id_le/
 115 qed.
 116
 117 (* Inversion lemmas on after ************************************************)
 118
 119 let corec isid_after_sn: ∀t1,t2. 𝐈⦃t1⦄ → t1 ⊚ t2 ≡ t2 ≝ ?.
 120 * #a1 #t1 * * [ | #a2 ] #t2 #H cases (isid_inv_seq … H) -H
 121 #Ht1 #H1
 122 [ @(after_zero … H1) -H1 /2 width=1 by/
 123 | @(after_skip … H1) -H1 /2 width=5 by/
 124 ]
 125 qed-.
 126
 127 let corec isid_after_dx: ∀t2,t1. 𝐈⦃t2⦄ → t1 ⊚ t2 ≡ t1 ≝ ?.
 128 * #a2 #t2 * *
 129 [ #t1 #H cases (isid_inv_seq … H) -H
 130   #Ht2 #H2 @(after_zero … H2) -H2 /2 width=1 by/
 131 | #a1 #t1 #H @(after_drop … a1 a1) /2 width=5 by/
 132 ]
 133 qed-.
 134
 135 lemma after_isid_inv_sn: ∀t1,t2,t. t1 ⊚ t2 ≡ t →  𝐈⦃t1⦄ → t2 ≐ t.
 136 /3 width=4 by isid_after_sn, after_mono/
 137 qed-.
 138
 139 lemma after_isid_inv_dx: ∀t1,t2,t. t1 ⊚ t2 ≡ t →  𝐈⦃t2⦄ → t1 ≐ t.
 140 /3 width=4 by isid_after_dx, after_mono/
 141 qed-.
 142 (*
 143 lemma after_inv_isid3: ∀t1,t2,t. t1 ⊚ t2 ≡ t → 𝐈⦃t⦄ → 𝐈⦃t1⦄ ∧ 𝐈⦃t2⦄.
 144 qed-.
 145 *)