matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_constructors.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 "delayed_updating/substitution/fsubst.ma".
  16 include "delayed_updating/syntax/prototerm_constructors.ma".
  17 include "ground/lib/subset_equivalence.ma".
  18
  19 (* FOCALIZED SUBSTITUTION ***************************************************)
  20
  21 (* Constructions with constructors for prototerm ****************************)
  22
  23 lemma fsubst_abst_hd (t) (u) (p):
  24       𝛌.(t[⋔p←u]) ⇔ (𝛌.t)[⋔𝗟◗p←u].
  25 #t #u #p @conj #r
  26 [ #Hr
  27   elim (in_comp_inv_abst … Hr) -Hr #s #H0 * *
  28   [ #q #Hq #H1 destruct
  29     /3 width=3 by ex2_intro, or_introl/
  30   | #H1s #H2s destruct
  31     @or_intror @conj
  32     [ /2 width=1 by in_comp_abst_hd/ ]
  33     #s0 <list_append_rcons_dx #Hs0
  34     elim (eq_inv_list_rcons_bi ????? Hs0) -Hs0 #H1 #H2 destruct
  35     /2 width=2 by/
  36   ]
  37 | * *
  38   [ #q #Hq #H0 destruct
  39     /4 width=3 by in_comp_abst_hd, ex2_intro, or_introl/
  40   | #H1r #H2r
  41     elim (in_comp_inv_abst … H1r) -H1r #s #H0 #Hs destruct
  42     /5 width=2 by in_comp_abst_hd, conj, or_intror/
  43   ]
  44 ]
  45 qed.
  46
  47 lemma fsubst_appl_sd (v) (t) (u) (p):
  48       ＠v[⋔p←u].t ⇔ (＠v.t)[⋔𝗦◗p←u].
  49 #v #t #u #p @conj #r
  50 [ #Hr
  51   elim (in_comp_inv_appl … Hr) -Hr * #s #H0
  52   [ * *
  53     [ #q #Hq #H1 destruct
  54       /3 width=3 by ex2_intro, or_introl/
  55     | #H1s #H2s destruct
  56       @or_intror @conj
  57       [ /2 width=1 by in_comp_appl_sd/ ]
  58       #s0 <list_append_rcons_dx #Hs0
  59       elim (eq_inv_list_rcons_bi ????? Hs0) -Hs0 #H1 #H2 destruct
  60       /2 width=2 by/
  61     ]
  62   | #Hs destruct
  63     @or_intror @conj [ /2 width=1 by in_comp_appl_hd/ ]
  64     #r <list_append_rcons_dx #H0
  65     elim (eq_inv_list_rcons_bi ????? H0) -H0 #H1 #H2 destruct
  66   ]
  67 | * *
  68   [ #q #Hq #H0 destruct
  69     /4 width=3 by in_comp_appl_sd, ex2_intro, or_introl/
  70   | #H1r #H2r
  71     elim (in_comp_inv_appl … H1r) -H1r * #s #H0 #Hs destruct
  72     /5 width=2 by in_comp_appl_hd, in_comp_appl_sd, or_intror, conj/
  73   ]
  74 ]
  75 qed.
  76
  77 lemma fsubst_appl_hd (v) (t) (u) (p):
  78       ＠v.(t[⋔p←u]) ⇔ (＠v.t)[⋔𝗔◗p←u].
  79 #v #t #u #p @conj #r
  80 [ #Hr
  81   elim (in_comp_inv_appl … Hr) -Hr * #s #H0
  82   [ #Hs destruct
  83     @or_intror @conj [ /2 width=1 by in_comp_appl_sd/ ]
  84     #r <list_append_rcons_dx #H0
  85     elim (eq_inv_list_rcons_bi ????? H0) -H0 #H1 #H2 destruct
  86   | * *
  87     [ #q #Hq #H1 destruct
  88       /3 width=3 by ex2_intro, or_introl/
  89     | #H1s #H2s destruct
  90       @or_intror @conj
  91       [ /2 width=1 by in_comp_appl_hd/ ]
  92       #s0 <list_append_rcons_dx #Hs0
  93       elim (eq_inv_list_rcons_bi ????? Hs0) -Hs0 #H1 #H2 destruct
  94       /2 width=2 by/
  95     ]
  96   ]
  97 | * *
  98   [ #q #Hq #H0 destruct
  99     /4 width=3 by in_comp_appl_hd, ex2_intro, or_introl/
 100   | #H1r #H2r
 101     elim (in_comp_inv_appl … H1r) -H1r * #s #H0 #Hs destruct
 102     /5 width=2 by in_comp_appl_hd, in_comp_appl_sd, or_intror, conj/
 103   ]
 104 ]
 105 qed.