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 (* labelled reflexive and transitive closure ********************************)
  15
  16 inductive lstar (A:Type[0]) (B:Type[0]) (R: A→relation B): list A → relation B ≝
  17 | lstar_nil : ∀b. lstar A B R ([]) b b
  18 | lstar_cons: ∀a,b1,b. R a b1 b →
  19               ∀l,b2. lstar A B R l b b2 → lstar A B R (a::l) b1 b2
  20 .
  21
  22 fact lstar_ind_l_aux: ∀A,B,R,b2. ∀P:relation2 (list A) B.
  23                       P ([]) b2 →
  24                       (∀a,l,b1,b. R a b1 b → lstar … R l b b2 → P l b → P (a::l) b1) →
  25                       ∀l,b1,b. lstar … R l b1 b → b = b2 → P l b1.
  26 #A #B #R #b2 #P #H1 #H2 #l #b1 #b #H elim H -b -b1
  27 [ #b #H destruct /2 width=1/
  28 | #a #b #b0 #Hb0 #l #b1 #Hb01 #IH #H destruct /3 width=4/
  29 ]
  30 qed-.
  31
  32 (* imporeved version of lstar_ind with "left_parameter" *)
  33 lemma lstar_ind_l: ∀A,B,R,b2. ∀P:relation2 (list A) B.
  34                    P ([]) b2 →
  35                    (∀a,l,b1,b. R a b1 b → lstar … R l b b2 → P l b → P (a::l) b1) →
  36                    ∀l,b1. lstar … R l b1 b2 → P l b1.
  37 #A #B #R #b2 #P #H1 #H2 #l #b1 #Hb12
  38 @(lstar_ind_l_aux … H1 H2 … Hb12) //
  39 qed-.
  40
  41 lemma lstar_step: ∀A,B,R,a,b1,b2. R a b1 b2 → lstar A B R ([a]) b1 b2.
  42 /2 width=3/
  43 qed.
  44
  45 lemma lstar_inv_nil: ∀A,B,R,l,b1,b2. lstar A B R l b1 b2 → [] = l → b1 = b2.
  46 #A #B #R #l #b1 #b2 * -l -b1 -b2 //
  47 #a #b1 #b #_ #l #b2 #_ #H destruct
  48 qed-.
  49
  50 lemma lstar_inv_cons: ∀A,B,R,l,b1,b2. lstar A B R l b1 b2 →
  51                       ∀a0,l0. a0::l0 = l →
  52                       ∃∃b. R a0 b1 b & lstar A B R l0 b b2.
  53 #A #B #R #l #b1 #b2 * -l -b1 -b2
  54 [ #b #a0 #l0 #H destruct
  55 | #a #b1 #b #Hb1 #l #b2 #Hb2 #a0 #l0 #H destruct /2 width=3/
  56 ]
  57 qed-.
  58
  59 lemma lstar_inv_step: ∀A,B,R,a,b1,b2. lstar A B R ([a]) b1 b2 → R a b1 b2.
  60 #A #B #R #a #b1 #b2 #H
  61 elim (lstar_inv_cons ?????? H ???) -H [4: // |2,3: skip ] #b #Hb1 #H (**) (* simplify line *)
  62 <(lstar_inv_nil ?????? H ?) -H // (**) (* simplify line *)
  63 qed-.
  64
  65 theorem lstar_singlevalued: ∀A,B,R. (∀a. singlevalued ?? (R a)) →
  66                             ∀l. singlevalued … (lstar A B R l).
  67 #A #B #R #HR #l #b #c1 #H @(lstar_ind_l ????????? H) -l -b
  68 [ /2 width=5 by lstar_inv_nil/
  69 | #a #l #b #b1 #Hb1 #_ #IHbc1 #c2 #H
  70   elim (lstar_inv_cons ?????? H ???) -H [4: // |2,3: skip ] #b2 #Hb2 #Hbc2 (**) (* simplify line *)
  71   lapply (HR … Hb1 … Hb2) -b #H destruct /2 width=1/
  72 ]
  73 qed-.
  74
  75 theorem lstar_trans: ∀A,B,R,l1,b1,b. lstar A B R l1 b1 b →
  76                      ∀l2,b2. lstar A B R l2 b b2 → lstar A B R (l1@l2) b1 b2.
  77 #A #B #R #l1 #b1 #b #H @(lstar_ind_l ????????? H) -l1 -b1 normalize // /3 width=3/
  78 qed-.