matita/matita/contribs/lambdadelta/ground/lib/star.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 "basics/star1.ma".
  16 include "ground/lib/relations.ma".
  17
  18 (* TRANSITIVE CLOSURE FOR RELATIONS *****************************************)
  19
  20 definition CTC (A:Type[0]) (B):
  21            (A→relation B) → (A→relation B) ≝
  22            λR,a. TC … (R a).
  23
  24 definition s_r_transitive (A) (B):
  25            relation2 (A→relation B) (B→relation A) ≝
  26            λR1,R2.
  27            ∀L2,T1,T2. R1 L2 T1 T2 → ∀L1. R2 T1 L1 L2 → CTC … R1 L1 T1 T2.
  28
  29 definition s_rs_transitive (A) (B):
  30            relation2 (A→relation B) (B→relation A) ≝
  31            λR1,R2.
  32            ∀L2,T1,T2. CTC … R1 L2 T1 T2 → ∀L1. R2 T1 L1 L2 → CTC … R1 L1 T1 T2.
  33
  34 lemma TC_strip (A) (R1) (R2):
  35       confluent2 A R1 R2 →
  36       ∀a0,a1. TC … R1 a0 a1 → ∀a2. R2 a0 a2 →
  37       ∃∃a. R2 a1 a & TC … R1 a2 a.
  38 #A #R1 #R2 #HR12 #a0 #a1 #H elim H -a1
  39 [ #a1 #Ha01 #a2 #Ha02
  40   elim (HR12 … Ha01 … Ha02) -HR12 -a0 /3 width=3 by inj, ex2_intro/
  41 | #a #a1 #_ #Ha1 #IHa0 #a2 #Ha02
  42   elim (IHa0 … Ha02) -a0 #a0 #Ha0 #Ha20
  43   elim (HR12 … Ha1 … Ha0) -HR12 -a /4 width=5 by step, ex2_intro/
  44 ]
  45 qed.
  46
  47 lemma TC_strip2 (A) (R1) (R2):
  48       confluent2 A R1 R2 →
  49       ∀a0,a2. TC … R2 a0 a2 → ∀a1. R1 a0 a1 →
  50       ∃∃a. TC … R2 a1 a & R1 a2 a.
  51 #A #R1 #R2 #HR12 #a0 #a2 #H elim H -a2
  52 [ #a2 #Ha02 #a1 #Ha01
  53   elim (HR12 … Ha01 … Ha02) -HR12 -a0 /3 width=3 by inj, ex2_intro/
  54 | #a #a2 #_ #Ha2 #IHa0 #a1 #Ha01
  55   elim (IHa0 … Ha01) -a0 #a0 #Ha10 #Ha0
  56   elim (HR12 … Ha0 … Ha2) -HR12 -a /4 width=3 by step, ex2_intro/
  57 ]
  58 qed.
  59
  60 lemma TC_confluent2 (A) (R1) (R2):
  61       confluent2 A R1 R2 → confluent2 A (TC … R1) (TC … R2).
  62 #A #R1 #R2 #HR12 #a0 #a1 #H elim H -a1
  63 [ #a1 #Ha01 #a2 #Ha02
  64   elim (TC_strip2 … HR12 … Ha02 … Ha01) -HR12 -a0 /3 width=3 by inj, ex2_intro/
  65 | #a #a1 #_ #Ha1 #IHa0 #a2 #Ha02
  66   elim (IHa0 … Ha02) -a0 #a0 #Ha0 #Ha20
  67   elim (TC_strip2 … HR12 … Ha0 … Ha1) -HR12 -a /4 width=5 by step, ex2_intro/
  68 ]
  69 qed.
  70
  71 lemma TC_strap1 (A) (R1) (R2):
  72       transitive2 A R1 R2 →
  73       ∀a1,a0. TC … R1 a1 a0 → ∀a2. R2 a0 a2 →
  74       ∃∃a. R2 a1 a & TC … R1 a a2.
  75 #A #R1 #R2 #HR12 #a1 #a0 #H elim H -a0
  76 [ #a0 #Ha10 #a2 #Ha02
  77   elim (HR12 … Ha10 … Ha02) -HR12 -a0 /3 width=3 by inj, ex2_intro/
  78 | #a #a0 #_ #Ha0 #IHa #a2 #Ha02
  79   elim (HR12 … Ha0 … Ha02) -HR12 -a0 #a0 #Ha0 #Ha02
  80   elim (IHa … Ha0) -a /4 width=5 by step, ex2_intro/
  81 ]
  82 qed.
  83
  84 lemma TC_strap2 (A) (R1) (R2):
  85       transitive2 A R1 R2 →
  86       ∀a0,a2. TC … R2 a0 a2 → ∀a1. R1 a1 a0 →
  87       ∃∃a. TC … R2 a1 a & R1 a a2.
  88 #A #R1 #R2 #HR12 #a0 #a2 #H elim H -a2
  89 [ #a2 #Ha02 #a1 #Ha10
  90   elim (HR12 … Ha10 … Ha02) -HR12 -a0 /3 width=3 by inj, ex2_intro/
  91 | #a #a2 #_ #Ha02 #IHa #a1 #Ha10
  92   elim (IHa … Ha10) -a0 #a0 #Ha10 #Ha0
  93   elim (HR12 … Ha0 … Ha02) -HR12 -a /4 width=3 by step, ex2_intro/
  94 ]
  95 qed.
  96
  97 lemma TC_transitive2 (A) (R1) (R2):
  98       transitive2 A R1 R2 → transitive2 A (TC … R1) (TC … R2).
  99 #A #R1 #R2 #HR12 #a1 #a0 #H elim H -a0
 100 [ #a0 #Ha10 #a2 #Ha02
 101   elim (TC_strap2 … HR12 … Ha02 … Ha10) -HR12 -a0 /3 width=3 by inj, ex2_intro/
 102 | #a #a0 #_ #Ha0 #IHa #a2 #Ha02
 103   elim (TC_strap2 … HR12 … Ha02 … Ha0) -HR12 -a0 #a0 #Ha0 #Ha02
 104   elim (IHa … Ha0) -a /4 width=5 by step, ex2_intro/
 105 ]
 106 qed.
 107
 108 lemma CTC_lsub_trans (A) (B) (R) (S):
 109       lsub_trans A B R S → lsub_trans A B (CTC … R) S.
 110 #A #B #R #S #HRS #L2 #T1 #T2 #H elim H -T2 /3 width=3 by inj/
 111 #T #T2 #_ #HT2 #IHT1 #L1 #HL12
 112 lapply (HRS … HT2 … HL12) -HRS -HT2 /3 width=3 by step/
 113 qed-.
 114
 115 lemma s_r_conf1_CTC1 (A) (B) (S) (R):
 116       s_r_confluent1 A B S R → s_r_confluent1 A B (CTC … S) R.
 117 #A #B #S #R #HSR #L1 #T1 #T2 #H @(TC_ind_dx … T1 H) -T1 /3 width=3 by/
 118 qed-.
 119
 120 lemma s_r_trans_CTC1 (A) (B) (S) (R):
 121       s_r_confluent1 A B S R →
 122       s_r_transitive A B S R → s_rs_transitive A B S R.
 123 #A #B #S #R #H1SR #H2SR #L2 #T1 #T2 #H @(TC_ind_dx … T1 H) -T1 /2 width=3 by/
 124 #T1 #T #HT1 #_ #IHT2 #L1 #HL12 lapply (H2SR … HT1 … HL12) -H2SR -HT1
 125 /4 width=5 by s_r_conf1_CTC1, trans_TC/
 126 qed-.
 127
 128 lemma s_r_trans_CTC2 (A) (B) (S) (R):
 129       s_rs_transitive A B S R → s_r_transitive A B S (CTC … R).
 130 #A #B #S #R #HSR #L2 #T1 #T2 #HT12 #L1 #H @(TC_ind_dx … L1 H) -L1 /3 width=3 by inj/
 131 qed-.
 132
 133 lemma s_r_to_s_rs_trans (A) (B) (S) (R):
 134       s_r_transitive A B (CTC … S) R → s_rs_transitive A B S R.
 135 #A #B #S #R #HSR #L2 #T1 #T2 #HL2 #L1 #HT1
 136 elim (TC_idem … (S L1) …  T1 T2)
 137 #_ #H @H @HSR //
 138 qed-.
 139
 140 lemma s_rs_to_s_r_trans (A) (B) (S) (R):
 141       s_rs_transitive A B S R → s_r_transitive A B (CTC … S) R.
 142 #A #B #S #R #HSR #L2 #T1 #T2 #HL2 #L1 #HT1
 143 elim (TC_idem … (S L1) …  T1 T2)
 144 #H #_ @H @HSR //
 145 qed-.
 146
 147 lemma s_rs_trans_TC1 (A) (B) (S) (R):
 148       s_rs_transitive A B S R → s_rs_transitive A B (CTC … S) R.
 149 #A #B #S #R #HSR #L2 #T1 #T2 #HL2 #L1 #HT1
 150 elim (TC_idem … (S L1) …  T1 T2)
 151 elim (TC_idem … (S L2) …  T1 T2)
 152 #_ #H1 #H2 #_ @H2 @HSR /3 width=3 by/
 153 qed-.
 154
 155 (* NOTE: Normal form and strong normalization *******************************)
 156
 157 lemma SN_to_NF (A) (R) (S):
 158       NF_dec A R S →
 159       ∀a1. SN A R S a1 →
 160       ∃∃a2. star … R a1 a2 & NF A R S a2.
 161 #A #R #S #HRS #a1 #H elim H -a1
 162 #a1 #_ #IHa1 elim (HRS a1) -HRS /2 width=3 by srefl, ex2_intro/
 163 * #a0 #Ha10 #Ha01 elim (IHa1 … Ha10 Ha01) -IHa1 -Ha01 /3 width=3 by star_compl, ex2_intro/
 164 qed-.
 165
 166 (* NOTE: Relations with unboxed pairs ***************************************)
 167
 168 lemma bi_TC_strip (A) (B) (R):
 169       bi_confluent A B R →
 170       ∀a0,a1,b0,b1. R a0 b0 a1 b1 → ∀a2,b2. bi_TC … R a0 b0 a2 b2 →
 171       ∃∃a,b. bi_TC … R a1 b1 a b & R a2 b2 a b.
 172 #A #B #R #HR #a0 #a1 #b0 #b1 #H01 #a2 #b2 #H elim H -a2 -b2
 173 [ #a2 #b2 #H02
 174   elim (HR … H01 … H02) -HR -a0 -b0 /3 width=4 by ex2_2_intro, bi_inj/
 175 | #a2 #b2 #a3 #b3 #_ #H23 * #a #b #H1 #H2
 176   elim (HR … H23 … H2) -HR -a0 -b0 -a2 -b2 /3 width=4 by ex2_2_intro, bi_step/
 177 ]
 178 qed.
 179
 180 lemma bi_TC_confluent (A) (B) (R):
 181       bi_confluent A B R → bi_confluent A B (bi_TC … R).
 182 #A #B #R #HR #a0 #a1 #b0 #b1 #H elim H -a1 -b1
 183 [ #a1 #b1 #H01 #a2 #b2 #H02
 184   elim (bi_TC_strip … HR … H01 … H02) -a0 -b0 /3 width=4 by ex2_2_intro, bi_inj/
 185 | #a1 #b1 #a3 #b3 #_ #H13 #IH #a2 #b2 #H02
 186   elim (IH … H02) -a0 -b0 #a0 #b0 #H10 #H20
 187   elim (bi_TC_strip … HR … H13 … H10) -a1 -b1 /3 width=7 by ex2_2_intro, bi_step/
 188 ]
 189 qed.
 190
 191 lemma bi_TC_decomp_r (A) (B) (R:bi_relation A B):
 192       ∀a1,a2,b1,b2. bi_TC … R a1 b1 a2 b2 →
 193       ∨∨ R a1 b1 a2 b2
 194        | ∃∃a,b. bi_TC … R a1 b1 a b & R a b a2 b2.
 195 #A #B #R #a1 #a2 #b1 #b2 * -a2 -b2 /2 width=1/ /3 width=4 by ex2_2_intro, or_intror/
 196 qed-.
 197
 198 lemma bi_TC_decomp_l (A) (B) (R:bi_relation A B):
 199       ∀a1,a2,b1,b2. bi_TC … R a1 b1 a2 b2 →
 200       ∨∨ R a1 b1 a2 b2
 201        | ∃∃a,b. R a1 b1 a b & bi_TC … R a b a2 b2.
 202 #A #B #R #a1 #a2 #b1 #b2 #H @(bi_TC_ind_dx … a1 b1 H) -a1 -b1
 203 [ /2 width=1 by or_introl/
 204 | #a1 #a #b1 #b #Hab1 #Hab2 #_ /3 width=4 by ex2_2_intro, or_intror/ (* * auto fails without #_ *)
 205 ]
 206 qed-.
 207
 208 (* NOTE: Relations with unboxed triples *************************************)
 209
 210 definition tri_star (A) (B) (C) (R):
 211            tri_relation A B C ≝
 212            tri_RC A B C (tri_TC … R).
 213
 214 lemma tri_star_tri_reflexive (A) (B) (C) (R):
 215       tri_reflexive A B C (tri_star … R).
 216 /2 width=1 by/ qed.
 217
 218 lemma tri_TC_to_tri_star (A) (B) (C) (R):
 219       ∀a1,b1,c1,a2,b2,c2.
 220       tri_TC A B C R a1 b1 c1 a2 b2 c2 → tri_star A B C R a1 b1 c1 a2 b2 c2.
 221 /2 width=1 by or_introl/ qed.
 222
 223 lemma tri_R_to_tri_star (A) (B) (C) (R):
 224       ∀a1,b1,c1,a2,b2,c2.
 225       R a1 b1 c1 a2 b2 c2 → tri_star A B C R a1 b1 c1 a2 b2 c2.
 226 /3 width=1 by tri_TC_to_tri_star, tri_inj/ qed.
 227
 228 lemma tri_star_strap1 (A) (B) (C) (R):
 229       ∀a1,a,a2,b1,b,b2,c1,c,c2.
 230       tri_star A B C R a1 b1 c1 a b c →
 231       R a b c a2 b2 c2 → tri_star A B C R a1 b1 c1 a2 b2 c2.
 232 #A #B #C #R #a1 #a #a2 #b1 #b #b2 #c1 #c #c2 *
 233 [ /3 width=5 by tri_TC_to_tri_star, tri_step/
 234 | * #H1 #H2 #H3 destruct /2 width=1 by tri_R_to_tri_star/
 235 ]
 236 qed.
 237
 238 lemma tri_star_strap2 (A) (B) (C) (R):
 239       ∀a1,a,a2,b1,b,b2,c1,c,c2.
 240       R a1 b1 c1 a b c → tri_star A B C R a b c a2 b2 c2 →
 241       tri_star A B C R a1 b1 c1 a2 b2 c2.
 242 #A #B #C #R #a1 #a #a2 #b1 #b #b2 #c1 #c #c2 #H *
 243 [ /3 width=5 by tri_TC_to_tri_star, tri_TC_strap/
 244 | * #H1 #H2 #H3 destruct /2 width=1 by tri_R_to_tri_star/
 245 ]
 246 qed.
 247
 248 lemma tri_star_to_tri_TC_to_tri_TC (A) (B) (C) (R):
 249       ∀a1,a,a2,b1,b,b2,c1,c,c2.
 250       tri_star A B C R a1 b1 c1 a b c →
 251       tri_TC A B C R a b c a2 b2 c2 → tri_TC A B C R a1 b1 c1 a2 b2 c2.
 252 #A #B #C #R #a1 #a #a2 #b1 #b #b2 #c1 #c #c2 *
 253 [ /2 width=5 by tri_TC_transitive/
 254 | * #H1 #H2 #H3 destruct /2 width=1 by/
 255 ]
 256 qed.
 257
 258 lemma tri_TC_to_tri_star_to_tri_TC (A) (B) (C) (R):
 259       ∀a1,a,a2,b1,b,b2,c1,c,c2.
 260       tri_TC A B C R a1 b1 c1 a b c →
 261       tri_star A B C R a b c a2 b2 c2 → tri_TC A B C R a1 b1 c1 a2 b2 c2.
 262 #A #B #C #R #a1 #a #a2 #b1 #b #b2 #c1 #c #c2 #H *
 263 [ /2 width=5 by tri_TC_transitive/
 264 | * #H1 #H2 #H3 destruct /2 width=1 by/
 265 ]
 266 qed.
 267
 268 lemma tri_tansitive_tri_star (A) (B) (C) (R):
 269       tri_transitive A B C (tri_star … R).
 270 #A #B #C #R #a1 #a #b1 #b #c1 #c #H #a2 #b2 #c2 *
 271 [ /3 width=5 by tri_star_to_tri_TC_to_tri_TC, tri_TC_to_tri_star/
 272 | * #H1 #H2 #H3 destruct /2 width=1 by/
 273 ]
 274 qed.
 275
 276 lemma tri_star_ind (A) (B) (C) (R):
 277       ∀a1,b1,c1. ∀Q:relation3 A B C. Q a1 b1 c1 →
 278       (∀a,a2,b,b2,c,c2. tri_star … R a1 b1 c1 a b c → R a b c a2 b2 c2 → Q a b c → Q a2 b2 c2) →
 279       ∀a2,b2,c2. tri_star … R a1 b1 c1 a2 b2 c2 → Q a2 b2 c2.
 280 #A #B #C #R #a1 #b1 #c1 #Q #H #IH #a2 #b2 #c2 *
 281 [ #H12 elim H12 -a2 -b2 -c2 /3 width=6 by tri_TC_to_tri_star/
 282 | * #H1 #H2 #H3 destruct //
 283 ]
 284 qed-.
 285
 286 lemma tri_star_ind_dx (A) (B) (C) (R):
 287       ∀a2,b2,c2. ∀Q:relation3 A B C. Q a2 b2 c2 →
 288       (∀a1,a,b1,b,c1,c. R a1 b1 c1 a b c → tri_star … R a b c a2 b2 c2 → Q a b c → Q a1 b1 c1) →
 289       ∀a1,b1,c1. tri_star … R a1 b1 c1 a2 b2 c2 → Q a1 b1 c1.
 290 #A #B #C #R #a2 #b2 #c2 #Q #H #IH #a1 #b1 #c1 *
 291 [ #H12 @(tri_TC_ind_dx … a1 b1 c1 H12) -a1 -b1 -c1 /3 width=6 by tri_TC_to_tri_star/
 292 | * #H1 #H2 #H3 destruct //
 293 ]
 294 qed-.