matita/matita/lib/basics/lists/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||
   8     \   /  This file is distributed under the terms of the
   9      \ /   GNU General Public License Version 2
  10       V_______________________________________________________________ *)
  11
  12 include "basics/lists/list.ma".
  13
  14 (* list-labeled reflexive and transitive closure ****************************)
  15
  16 definition ltransitive: ∀A,B:Type[0]. predicate (list A → relation B) ≝ λA,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: ∀A,B:Type[0]. predicate (list A → relation B) ≝
  20                             λA,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 (A:Type[0]) (B:Type[0]) (R: A→relation B): list A → relation B ≝
  24 | lstar_nil : ∀b. lstar A B R ([]) b b
  25 | lstar_cons: ∀a,b1,b. R a b1 b →
  26               ∀l,b2. lstar A B R l b b2 → lstar A B R (a::l) b1 b2
  27 .
  28
  29 fact lstar_ind_l_aux: ∀A,B,R,b2. ∀P:relation2 (list A) B.
  30                       P ([]) b2 →
  31                       (∀a,l,b1,b. R a b1 b → lstar … R l b b2 → P l b → P (a::l) b1) →
  32                       ∀l,b1,b. lstar … R l b1 b → b = b2 → P l b1.
  33 #A #B #R #b2 #P #H1 #H2 #l #b1 #b #H elim H -b -b1
  34 [ #b #H destruct /2 width=1/
  35 | #a #b #b0 #Hb0 #l #b1 #Hb01 #IH #H destruct /3 width=4/
  36 ]
  37 qed-.
  38
  39 (* imporeved version of lstar_ind with "left_parameter" *)
  40 lemma lstar_ind_l: ∀A,B,R,b2. ∀P:relation2 (list A) B.
  41                    P ([]) b2 →
  42                    (∀a,l,b1,b. R a b1 b → lstar … R l b b2 → P l b → P (a::l) b1) →
  43                    ∀l,b1. lstar … R l b1 b2 → P l b1.
  44 #A #B #R #b2 #P #H1 #H2 #l #b1 #Hb12
  45 @(lstar_ind_l_aux … H1 H2 … Hb12) //
  46 qed-.
  47
  48 lemma lstar_step: ∀A,B,R,a,b1,b2. R a b1 b2 → lstar A B R ([a]) b1 b2.
  49 /2 width=3/
  50 qed.
  51
  52 lemma lstar_inv_nil: ∀A,B,R,l,b1,b2. lstar A B R l b1 b2 → [] = l → b1 = b2.
  53 #A #B #R #l #b1 #b2 * -l -b1 -b2 //
  54 #a #b1 #b #_ #l #b2 #_ #H destruct
  55 qed-.
  56
  57 lemma lstar_inv_cons: ∀A,B,R,l,b1,b2. lstar A B R l b1 b2 →
  58                       ∀a0,l0. a0::l0 = l →
  59                       ∃∃b. R a0 b1 b & lstar A B R l0 b b2.
  60 #A #B #R #l #b1 #b2 * -l -b1 -b2
  61 [ #b #a0 #l0 #H destruct
  62 | #a #b1 #b #Hb1 #l #b2 #Hb2 #a0 #l0 #H destruct /2 width=3/
  63 ]
  64 qed-.
  65
  66 lemma lstar_inv_step: ∀A,B,R,a,b1,b2. lstar A B R ([a]) b1 b2 → R a b1 b2.
  67 #A #B #R #a #b1 #b2 #H
  68 elim (lstar_inv_cons ?????? H) -H [4: // |2,3: skip ] #b #Hb1 #H (**) (* simplify line *)
  69 <(lstar_inv_nil ?????? H ?) -H // (**) (* simplify line *)
  70 qed-.
  71
  72 theorem lstar_singlevalued: ∀A,B,R. (∀a. singlevalued ?? (R a)) →
  73                             ∀l. singlevalued … (lstar A B R l).
  74 #A #B #R #HR #l #b #c1 #H @(lstar_ind_l … l b H) -l -b
  75 [ /2 width=5 by lstar_inv_nil/
  76 | #a #l #b #b1 #Hb1 #_ #IHbc1 #c2 #H
  77   elim (lstar_inv_cons ?????? H) -H [4: // |2,3: skip ] #b2 #Hb2 #Hbc2 (**) (* simplify line *)
  78   lapply (HR … Hb1 … Hb2) -b #H destruct /2 width=1/
  79 ]
  80 qed-.
  81
  82 theorem lstar_ltransitive: ∀A,B,R. ltransitive … (lstar A B R).
  83 #A #B #R #l1 #b1 #b #H @(lstar_ind_l … l1 b1 H) -l1 -b1 normalize // /3 width=3/
  84 qed-.
  85
  86 lemma lstar_inv_ltransitive: ∀A,B,R. inv_ltransitive … (lstar A B R).
  87 #A #B #R #l1 elim l1 -l1 normalize /2 width=3/
  88 #a #l1 #IHl1 #l2 #b1 #b2 #H
  89 elim (lstar_inv_cons … b2 H) -H [4: // |2,3: skip ] #b #Hb1 #Hb2 (**) (* simplify line *)
  90 elim (IHl1 … Hb2) -IHl1 -Hb2 /3 width=3/
  91 qed-.
  92
  93 lemma lstar_app: ∀A,B,R,l,b1,b. lstar A B R l b1 b → ∀a,b2. R a b b2 →
  94                  lstar A B R (l@[a]) b1 b2.
  95 #A #B #R #l #b1 #b #H @(lstar_ind_l … l b1 H) -l -b1 /2 width=1/
  96 normalize /3 width=3/
  97 qed.
  98
  99 inductive lstar_r (A:Type[0]) (B:Type[0]) (R: A→relation B): list A → relation B ≝
 100 | lstar_r_nil: ∀b. lstar_r A B R ([]) b b
 101 | lstar_r_app: ∀l,b1,b. lstar_r A B R l b1 b → ∀a,b2. R a b b2 →
 102                lstar_r A B R (l@[a]) b1 b2
 103 .
 104
 105 lemma lstar_r_cons: ∀A,B,R,l,b,b2. lstar_r A B R l b b2 → ∀a,b1. R a b1 b →
 106                     lstar_r A B R (a::l) b1 b2.
 107 #A #B #R #l #b #b2 #H elim H -l -b2 /2 width=3/
 108 #l #b1 #b #_ #a #b2 #Hb2 #IHb1 #a0 #b0 #Hb01
 109 @(lstar_r_app … (a0::l) … Hb2) -b2 /2 width=1/
 110 qed.
 111
 112 lemma lstar_lstar_r: ∀A,B,R,l,b1,b2. lstar A B R l b1 b2 → lstar_r A B R l b1 b2.
 113 #A #B #R #l #b1 #b2 #H @(lstar_ind_l … l b1 H) -l -b1 // /2 width=3/
 114 qed.
 115
 116 lemma lstar_r_inv_lstar: ∀A,B,R,l,b1,b2. lstar_r A B R l b1 b2 → lstar A B R l b1 b2.
 117 #A #B #R #l #b1 #b2 #H elim H -l -b1 -b2 // /2 width=3/
 118 qed-.
 119
 120 fact lstar_ind_r_aux: ∀A,B,R,b1. ∀P:relation2 (list A) B.
 121                       P ([]) b1 →
 122                       (∀a,l,b,b2. lstar … R l b1 b → R a b b2 → P l b → P (l@[a]) b2) →
 123                       ∀l,b,b2. lstar … R l b b2 → b = b1 → P l b2.
 124 #A #B #R #b1 #P #H1 #H2 #l #b #b2 #H elim (lstar_lstar_r … l b b2 H) -l -b -b2
 125 [ #b #H destruct //
 126 | #l #b #b0 #Hb0 #a #b2 #Hb02 #IH #H destruct /3 width=4 by lstar_r_inv_lstar/
 127 ]
 128 qed-.
 129
 130 lemma lstar_ind_r: ∀A,B,R,b1. ∀P:relation2 (list A) B.
 131                    P ([]) b1 →
 132                    (∀a,l,b,b2. lstar … R l b1 b → R a b b2 → P l b → P (l@[a]) b2) →
 133                    ∀l,b2. lstar … R l b1 b2 → P l b2.
 134 #A #B #R #b1 #P #H1 #H2 #l #b2 #Hb12
 135 @(lstar_ind_r_aux … H1 H2 … Hb12) //
 136 qed-.