matita/matita/contribs/lambdadelta/ground_2/lib/ltc.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/insert_eq/insert_eq_0.ma".
  16 include "ground_2/lib/functions.ma".
  17
  18 (* LABELLED TRANSITIVE CLOSURE **********************************************)
  19
  20 inductive ltc (A:Type[0]) (f) (B) (R:relation3 A B B): relation3 A B B ≝
  21 | ltc_rc   : ∀a,b1,b2. R a b1 b2 → ltc … a b1 b2
  22 | ltc_trans: ∀a1,a2,b1,b,b2. ltc … a1 b1 b → ltc … a2 b b2 → ltc … (f a1 a2) b1 b2
  23 .
  24
  25 (* Basic properties *********************************************************)
  26
  27 lemma ltc_sn (A) (f) (B) (R): ∀a1,b1,b. R a1 b1 b →
  28                               ∀a2,b2. ltc A f B R a2 b b2 → ltc … f … R (f a1 a2) b1 b2.
  29 /3 width=3 by ltc_rc, ltc_trans/ qed.
  30
  31 lemma ltc_dx (A) (f) (B) (R): ∀a1,b1,b. ltc A f B R a1 b1 b →
  32                               ∀a2,b2. R a2 b b2 → ltc … f … R (f a1 a2) b1 b2.
  33 /3 width=3 by ltc_rc, ltc_trans/ qed.
  34
  35 (* Basic eliminators ********************************************************)
  36
  37 lemma ltc_ind_sn (A) (f) (B) (R) (Q:relation2 A B) (b2): associative … f →
  38                  (∀a,b1. R a b1 b2 → Q a b1) →
  39                  (∀a1,a2,b1,b. R a1 b1 b → ltc … f … R a2 b b2 → Q a2 b → Q (f a1 a2) b1) →
  40                  ∀a,b1. ltc … f … R a b1 b2 → Q a b1.
  41 #A #f #B #R #Q #b2 #Hf #IH1 #IH2 #a #b1 @(insert_eq_0 … b2)
  42 #b0 #H elim H -a -b1 -b0 /2 width=2 by/
  43 #a1 #a2 #b1 #b #b0 #H #Hb2 #_
  44 generalize in match Hb2; generalize in match a2; -Hb2 -a2
  45 elim H -a1 -b1 -b /4 width=4 by ltc_trans/
  46 qed-.
  47
  48 lemma ltc_ind_dx (A) (f) (B) (R) (Q:A→predicate B) (b1): associative … f →
  49                  (∀a,b2. R a b1 b2 → Q a b2) →
  50                  (∀a1,a2,b,b2. ltc … f … R a1 b1 b → Q a1 b → R a2 b b2 → Q (f a1 a2) b2) →
  51                  ∀a,b2. ltc … f … R a b1 b2 → Q a b2.
  52 #A #f #B #R #Q #b1 #Hf #IH1 #IH2 #a #b2 @(insert_eq_0 … b1)
  53 #b0 #H elim H -a -b0 -b2 /2 width=2 by/
  54 #a1 #a2 #b0 #b #b2 #Hb0 #H #IHb0 #_
  55 generalize in match IHb0; generalize in match Hb0; generalize in match a1; -IHb0 -Hb0 -a1
  56 elim H -a2 -b -b2 /4 width=4 by ltc_trans/
  57 qed-.
  58
  59 (* Advanced elimiators with reflexivity *************************************)
  60
  61 lemma ltc_ind_sn_refl (A) (i) (f) (B) (R) (Q:relation2 A B) (b2):
  62                       associative … f → right_identity … f i → reflexive B (R i) →
  63                       Q i b2 →
  64                       (∀a1,a2,b1,b. R a1 b1 b → ltc … f … R a2 b b2 → Q a2 b → Q (f a1 a2) b1) →
  65                       ∀a,b1. ltc … f … R a b1 b2 → Q a b1.
  66 #A #i #f #B #R #Q #b2 #H1f #H2f #HR #IH1 #IH2 #a #b1 #H
  67 @(ltc_ind_sn … R … H1f … IH2 … H) -a -b1 -H1f #a #b1 #Hb12
  68 >(H2f a) -H2f /3 width=4 by ltc_rc/
  69 qed-.
  70
  71 lemma ltc_ind_dx_refl (A) (i) (f) (B) (R) (Q:A→predicate B) (b1):
  72                       associative … f → left_identity … f i → reflexive B (R i) →
  73                       Q i b1 →
  74                       (∀a1,a2,b,b2. ltc … f … R a1 b1 b → Q a1 b → R a2 b b2 → Q (f a1 a2) b2) →
  75                       ∀a,b2. ltc … f … R a b1 b2 → Q a b2.
  76 #A #i #f #B #R #Q #b1 #H1f #H2f #HR #IH1 #IH2 #a #b2 #H
  77 @(ltc_ind_dx … R … H1f … IH2 … H) -a -b2 -H1f #a #b2 #Hb12
  78 >(H2f a) -H2f /3 width=4 by ltc_rc/
  79 qed-.