matita/matita/lib/arithmetics/lstar.ma

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department of the University of Bologna, Italy.
   5     ||I||
   6     ||T||
   7     ||A||  This file is distributed under the terms of the
   8     \   /  GNU General Public License Version 2
   9      \ /
  10       V_______________________________________________________________ *)
  11
  12 include "arithmetics/nat.ma".
  13
  14 (* nat-labeled reflexive and transitive closure *****************************)
  15
  16 definition ltransitive: ∀B:Type[0]. predicate (ℕ→relation B) ≝ λB,R.
  17                         ∀l1,b1,b. R l1 b1 b → ∀l2,b2. R l2 b b2 → R (l1+l2) b1 b2.
  18
  19 definition inv_ltransitive: ∀B:Type[0]. predicate (ℕ→relation B) ≝
  20                             λB,R. ∀l1,l2,b1,b2. R (l1+l2) b1 b2 →
  21                             ∃∃b. R l1 b1 b & R l2 b b2.
  22
  23 inductive lstar (B:Type[0]) (R: relation B): ℕ→relation B ≝
  24 | lstar_O: ∀b. lstar B R 0 b b
  25 | lstar_S: ∀b1,b. R b1 b → ∀l,b2. lstar B R l b b2 → lstar B R (l+1) b1 b2
  26 .
  27
  28 fact lstar_ind_l_aux: ∀B,R,b2. ∀P:relation2 ℕ B.
  29                       P 0 b2 →
  30                       (∀l,b1,b. R b1 b → lstar … R l b b2 → P l b → P (l+1) b1) →
  31                       ∀l,b1,b. lstar … R l b1 b → b = b2 → P l b1.
  32 #B #R #b2 #P #H1 #H2 #l #b1 #b #H elim H -b -b1
  33 [ #b #H destruct /2 width=1/
  34 | #b #b0 #Hb0 #l #b1 #Hb01 #IH #H destruct /3 width=4/
  35 ]
  36 qed-.
  37
  38 (* imporeved version of lstar_ind with "left_parameter" *)
  39 lemma lstar_ind_l: ∀B,R,b2. ∀P:relation2 ℕ B.
  40                    P 0 b2 →
  41                    (∀l,b1,b. R b1 b → lstar … R l b b2 → P l b → P (l+1) b1) →
  42                    ∀l,b1. lstar … R l b1 b2 → P l b1.
  43 #B #R #b2 #P #H1 #H2 #l #b1 #Hb12
  44 @(lstar_ind_l_aux … H1 H2 … Hb12) //
  45 qed-.
  46
  47 lemma lstar_step: ∀B,R,b1,b2. R b1 b2 → lstar B R 1 b1 b2.
  48 /2 width=3/
  49 qed.
  50
  51 lemma lstar_dx: ∀B,R,l,b1,b. lstar B R l b1 b → ∀b2. R b b2 →
  52                 lstar B R (l+1) b1 b2.
  53 #B #R #l #b1 #b #H @(lstar_ind_l … l b1 H) -l -b1 /2 width=1/ /3 width=3/
  54 qed.
  55
  56 lemma lstar_inv_O: ∀B,R,l,b1,b2. lstar B R l b1 b2 → 0 = l → b1 = b2.
  57 #B #R #l #b1 #b2 * -l -b1 -b2 //
  58 #b1 #b #_ #l #b2 #_ <plus_n_Sm #H destruct
  59 qed-.
  60
  61 lemma lstar_inv_S: ∀B,R,l,b1,b2. lstar B R l b1 b2 →
  62                    ∀l0. l0+1 = l →
  63                    ∃∃b. R b1 b & lstar B R l0 b b2.
  64 #B #R #l #b1 #b2 * -l -b1 -b2
  65 [ #b #l0 <plus_n_Sm #H destruct
  66 | #b1 #b #Hb1 #l #b2 #Hb2 #l0 #H
  67   lapply (injective_plus_l … H) -H #H destruct /2 width=3/
  68 ]
  69 qed-.
  70
  71 lemma lstar_inv_step: ∀B,R,b1,b2. lstar B R 1 b1 b2 → R b1 b2.
  72 #B #R #b1 #b2 #H
  73 elim (lstar_inv_S … 1 … H 0) -H // #b #Hb1 #H
  74 <(lstar_inv_O … R … H ?) -H //
  75 qed-.
  76
  77 theorem lstar_singlevalued: ∀B,R. singlevalued … R →
  78                             ∀l. singlevalued … (lstar B R l).
  79 #B #R #HR #l #c #c1 #H @(lstar_ind_l … l c H) -l -c
  80 [ /2 width=5 by lstar_inv_O/
  81 | #l #b #b1 #Hb1 #_ #IHbc1 #c2 #H
  82   elim (lstar_inv_S … R … H l) -H // #b2 #Hb2 #Hbc2
  83   lapply (HR … Hb1 … Hb2) -b #H destruct /2 width=1/
  84 ]
  85 qed-.
  86
  87 theorem lstar_ltransitive: ∀B,R. ltransitive … (lstar B R).
  88 #B #R #l1 #b1 #b #H @(lstar_ind_l … l1 b1 H) -l1 -b1 // /3 width=3/
  89 qed-.
  90
  91 lemma lstar_inv_ltransitive: ∀B,R. inv_ltransitive … (lstar B R).
  92 #B #R #l1 @(nat_ind_plus … l1) -l1 /2 width=3/
  93 #l1 #IHl1 #l2 #b1 #b2 <plus_plus_comm_23 #H
  94 elim (lstar_inv_S … b2 H (l1+l2)) -H // #b #Hb1 #Hb2
  95 elim (IHl1 … Hb2) -IHl1 -Hb2 /3 width=3/
  96 qed-.
  97
  98 lemma lstar_inv_S_dx: ∀B,R,l,b1,b2. lstar B R (l+1) b1 b2 →
  99                       ∃∃b. lstar B R l b1 b & R b b2.
 100 #B #R #l #b1 #b2 #H
 101 elim (lstar_inv_ltransitive B R … H) -H #b #Hb1 #H
 102 lapply (lstar_inv_step B R … H) -H /2 width=3/
 103 qed-.
 104
 105 inductive lstar_r (B:Type[0]) (R: relation B): ℕ → relation B ≝
 106 | lstar_r_O: ∀b. lstar_r B R 0 b b
 107 | lstar_r_S: ∀l,b1,b. lstar_r B R l b1 b → ∀b2. R b b2 →
 108              lstar_r B R (l+1) b1 b2
 109 .
 110
 111 lemma lstar_r_sn: ∀B,R,l,b,b2. lstar_r B R l b b2 → ∀b1. R b1 b →
 112                   lstar_r B R (l+1) b1 b2.
 113 #B #R #l #b #b2 #H elim H -l -b2 /2 width=3/
 114 #l #b1 #b #_ #b2 #Hb2 #IHb1 #b0 #Hb01
 115 @(lstar_r_S … (l+1) … Hb2) -b2 /2 width=1/
 116 qed.
 117
 118 lemma lstar_lstar_r: ∀B,R,l,b1,b2. lstar B R l b1 b2 → lstar_r B R l b1 b2.
 119 #B #R #l #b1 #b2 #H @(lstar_ind_l … l b1 H) -l -b1 // /2 width=3/
 120 qed.
 121
 122 lemma lstar_r_inv_lstar: ∀B,R,l,b1,b2. lstar_r B R l b1 b2 → lstar B R l b1 b2.
 123 #B #R #l #b1 #b2 #H elim H -l -b1 -b2 // /2 width=3/
 124 qed-.
 125
 126 fact lstar_ind_r_aux: ∀B,R,b1. ∀P:relation2 ℕ B.
 127                       P 0 b1 →
 128                       (∀l,b,b2. lstar … R l b1 b → R b b2 → P l b → P (l+1) b2) →
 129                       ∀l,b,b2. lstar … R l b b2 → b = b1 → P l b2.
 130 #B #R #b1 #P #H1 #H2 #l #b #b2 #H elim (lstar_lstar_r … l b b2 H) -l -b -b2
 131 [ #b #H destruct //
 132 | #l #b #b0 #Hb0 #b2 #Hb02 #IHb02 #H destruct /3 width=4 by lstar_r_inv_lstar/
 133 ]
 134 qed-.
 135
 136 lemma lstar_ind_r: ∀B,R,b1. ∀P:relation2 ℕ B.
 137                    P 0 b1 →
 138                    (∀l,b,b2. lstar … R l b1 b → R b b2 → P l b → P (l+1) b2) →
 139                    ∀l,b2. lstar … R l b1 b2 → P l b2.
 140 #B #R #b1 #P #H1 #H2 #l #b2 #Hb12
 141 @(lstar_ind_r_aux … H1 H2 … Hb12) //
 142 qed-.
 143
 144 lemma lstar_Conf3: ∀A,B,S,R. Conf3 A B S R → ∀l. Conf3 A B S (lstar … R l).
 145 #A #B #S #R #HSR #l #b #a1 #Ha1 #a2 #H @(lstar_ind_r … l a2 H) -l -a2 // /2 width=3/
 146 qed-.