matita/matita/contribs/lambda/subterms/projections.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 "terms/term.ma".
  16 include "subterms/subterms.ma".
  17
  18 (* PROJECTIONS **************************************************************)
  19
  20 (* Note: the boolean subset of subterms *)
  21 let rec boolean b M on M ≝ match M with
  22 [ VRef i   ⇒ {b}#i
  23 | Abst A   ⇒ {b}𝛌.(boolean b A)
  24 | Appl B A ⇒ {b}@(boolean b B).(boolean b A)
  25 ].
  26
  27 interpretation "boolean subset (subterms)"
  28    'ProjectUp b M = (boolean b M).
  29
  30 notation "hvbox( { term 46 b } ⇑ break term 46 M)"
  31    non associative with precedence 46
  32    for @{ 'ProjectUp $b $M }.
  33
  34 lemma boolean_inv_vref: ∀j,b0,b,M. {b}⇑ M = {b0}#j → b = b0 ∧ M = #j.
  35 #j #b0 #b * normalize
  36 [ #i #H destruct /2 width=1/
  37 | #A #H destruct
  38 | #B #A #H destruct
  39 ]
  40 qed-.
  41
  42 lemma boolean_inv_abst: ∀U,b0,b,M. {b}⇑ M = {b0}𝛌.U →
  43                         ∃∃C. b = b0 & {b}⇑C = U & M = 𝛌.C.
  44 #U #b0 #b * normalize
  45 [ #i #H destruct
  46 | #A #H destruct /2 width=3/
  47 | #B #A #H destruct
  48 ]
  49 qed-.
  50
  51 lemma boolean_inv_appl: ∀W,U,b0,b,M. {b}⇑ M = {b0}@W.U →
  52                         ∃∃D,C. b = b0 & {b}⇑D = W & {b}⇑C = U & M = @D.C.
  53 #W #U #b0 #b * normalize
  54 [ #i #H destruct
  55 | #A #H destruct
  56 | #B #A #H destruct /2 width=5/
  57 ]
  58 qed-.
  59
  60 (* Note: the carrier (underlying term) of a subset of subterms *)
  61 let rec carrier F on F ≝ match F with
  62 [ SVRef _ i   ⇒ #i
  63 | SAbst _ T   ⇒ 𝛌.(carrier T)
  64 | SAppl _ V T ⇒ @(carrier V).(carrier T)
  65 ].
  66
  67 interpretation "carrier (subterms)"
  68    'ProjectDown F = (carrier F).
  69
  70 notation "hvbox(⇓ term 46 F)"
  71    non associative with precedence 46
  72    for @{ 'ProjectDown $F }.
  73
  74 lemma carrier_inv_vref: ∀j,F. ⇓F = #j → ∃b. F = {b}#j.
  75 #j * normalize
  76 [ #b #i #H destruct /2 width=2/
  77 | #b #T #H destruct
  78 | #b #V #T #H destruct
  79 ]
  80 qed-.
  81
  82 lemma carrier_inv_abst: ∀C,F. ⇓F = 𝛌.C → ∃∃b,U. ⇓U = C & F = {b}𝛌.U.
  83 #C * normalize
  84 [ #b #i #H destruct
  85 | #b #T #H destruct /2 width=4/
  86 | #b #V #T #H destruct
  87 ]
  88 qed-.
  89
  90 lemma carrier_inv_appl: ∀D,C,F. ⇓F = @D.C →
  91                         ∃∃b,W,U. ⇓W = D & ⇓U = C & F = {b}@W.U.
  92 #D #C * normalize
  93 [ #b #i #H destruct
  94 | #b #T #H destruct
  95 | #b #V #T #H destruct /2 width=6/
  96 ]
  97 qed-.
  98
  99 definition mk_boolean: bool → subterms → subterms ≝
 100    λb,F. {b}⇑⇓F.
 101
 102 interpretation "make boolean (subterms)"
 103    'ProjectSame b F = (mk_boolean b F).
 104
 105 notation "hvbox( { term 46 b } ⇕ break term 46 F)"
 106    non associative with precedence 46
 107    for @{ 'ProjectSame $b $F }.
 108
 109 lemma mk_boolean_inv_vref: ∀j,b0,b,F. {b}⇕ F = {b0}#j →
 110                            ∃∃b1. b = b0 & F = {b1}#j.
 111 #j #b0 #b #F #H
 112 elim (boolean_inv_vref … H) -H #H0 #H
 113 elim (carrier_inv_vref … H) -H /2 width=2/
 114 qed-.
 115
 116 lemma mk_boolean_inv_abst: ∀U,b0,b,F. {b}⇕ F = {b0}𝛌.U →
 117                            ∃∃b1,T. b = b0 & {b}⇕T = U & F = {b1}𝛌.T.
 118 #U #b0 #b #F #H
 119 elim (boolean_inv_abst … H) -H #C #H0 #H1 #H
 120 elim (carrier_inv_abst … H) -H #b1 #U1 #H3 destruct /2 width=4/
 121 qed-.
 122
 123 lemma mk_boolean_inv_appl: ∀W,U,b0,b,F. {b}⇕ F = {b0}@W.U →
 124                            ∃∃b1,V,T. b = b0 & {b}⇕V = W & {b}⇕T = U & F = {b1}@V.T.
 125 #W #U #b0 #b #F #H
 126 elim (boolean_inv_appl … H) -H #D #C #H0 #H1 #H2 #H
 127 elim (carrier_inv_appl … H) -H #b1 #W1 #U1 #H3 #H4 destruct /2 width=6/
 128 qed-.