matita/matita/lib/lambda/subterms/boolean.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 "lambda/subterms/carrier.ma".
  16
  17 include "lambda/notation/functions/projectup_2.ma".
  18
  19 include "lambda/xoa/ex_3_1.ma".
  20 include "lambda/xoa/ex_4_2.ma".
  21
  22 (* BOOLEAN (EMPTY OR FULL) SUBSET *******************************************)
  23
  24 let rec boolean b M on M ≝ match M with
  25 [ VRef i   ⇒ {b}#i
  26 | Abst A   ⇒ {b}𝛌.(boolean b A)
  27 | Appl B A ⇒ {b}@(boolean b B).(boolean b A)
  28 ].
  29
  30 interpretation "boolean subset (subterms)"
  31    'ProjectUp b M = (boolean b M).
  32
  33 lemma boolean_inv_vref: ∀j,c,b,M. {b}⇑ M = {c}#j → b = c ∧ M = #j.
  34 #j #c #b * normalize
  35 [ #i #H destruct /2 width=1/
  36 | #A #H destruct
  37 | #B #A #H destruct
  38 ]
  39 qed-.
  40
  41 lemma boolean_inv_abst: ∀U,c,b,M. {b}⇑ M = {c}𝛌.U →
  42                         ∃∃C. b = c & {b}⇑C = U & M = 𝛌.C.
  43 #U #c #b * normalize
  44 [ #i #H destruct
  45 | #A #H destruct /2 width=3/
  46 | #B #A #H destruct
  47 ]
  48 qed-.
  49
  50 lemma boolean_inv_appl: ∀W,U,c,b,M. {b}⇑ M = {c}@W.U →
  51                         ∃∃D,C. b = c & {b}⇑D = W & {b}⇑C = U & M = @D.C.
  52 #W #U #c #b * normalize
  53 [ #i #H destruct
  54 | #A #H destruct
  55 | #B #A #H destruct /2 width=5/
  56 ]
  57 qed-.
  58
  59 lemma boolean_lift: ∀b,h,M,d. {b}⇑ ↑[d, h] M = ↑[d, h] {b}⇑ M.
  60 #b #h #M elim M -M normalize //
  61 qed.
  62
  63 lemma boolean_dsubst: ∀b,N,M,d. {b}⇑ [d ↙ N] M = [d ↙ {b}⇑ N] {b}⇑ M.
  64 #b #N #M elim M -M [2,3: normalize // ]
  65 #i #d elim (lt_or_eq_or_gt i d) #Hid
  66 [ >(sdsubst_vref_lt … Hid) >(dsubst_vref_lt … Hid) //
  67 | destruct normalize //
  68 | >(sdsubst_vref_gt … Hid) >(dsubst_vref_gt … Hid) //
  69 ]
  70 qed.
  71
  72 lemma carrier_boolean: ∀b,M. ⇓ {b}⇑ M = M.
  73 #b #M elim M -M normalize //
  74 qed.