matita/matita/lib/lambdaN/arity.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/ext.ma".
  16
  17 (* ARITIES ********************************************************************)
  18
  19 (* An arity is a normal term representing the functional structure of a term.
  20  * Arities can be freely applied as lon as the result is typable in λ→.
  21  * we encode an arity with a family of meta-linguistic functions typed by λ→
  22  * Such a family contains one member for each type of λ→
  23  *)
  24
  25 (* type of arity members ******************************************************)
  26
  27 (* the type of an arity member *)
  28 inductive MEM: Type[0] ≝
  29    | TOP: MEM
  30    | FUN: MEM → MEM → MEM
  31 .
  32
  33 definition pred ≝ λC. match C with
  34    [ TOP     ⇒ TOP
  35    | FUN _ A ⇒ A
  36    ].
  37
  38 definition decidable_MEq: ∀C1,C2:MEM. (C1 = C2) + (C1 ≠ C2).
  39 #C1 (elim C1) -C1
  40    [ #C2 elim C2 -C2
  41      [ /2/
  42      | #B2 #A2 #_ #_ @inr @nmk #false destruct
  43      ]
  44    | #B1 #A1 #IHB1 #IHA1 #C2 elim C2 -C2
  45      [ @inr @nmk #false destruct
  46      | #B2 #A2 #_ #_ elim (IHB1 B2) -IHB1 #HB
  47        [ elim (IHA1 A2) - IHA1 #HA
  48          [ /2/ | @inr @nmk #false destruct elim HA /2/ ]
  49        | @inr @nmk #false destruct elim HB /2/
  50    ]
  51 qed.
  52
  53 lemma fun_neq_sym: ∀A,C,B. pred C ≠ A → C ≠ FUN B A.
  54 #A #C #B #HA elim HA -HA #HA @nmk #H @HA -HA >H //
  55 qed.
  56
  57 (* arity members **************************************************************)
  58
  59 (* the arity members of type TOP *)
  60 inductive Top: Type[0] ≝
  61    | SORT: Top
  62 .
  63
  64 (* the arity members of type A *)
  65 let rec Mem A ≝ match A with
  66    [ TOP     ⇒ Top
  67    | FUN B A ⇒ Mem B → Mem A
  68    ].
  69
  70 (* the members of the arity "sort" *)
  71 let rec sort_mem A ≝ match A return λA. Mem A with
  72    [ TOP     ⇒ SORT
  73    | FUN B A ⇒ λ_.sort_mem A
  74    ].
  75
  76 (* arities ********************************************************************)
  77
  78 (* the type of arities *)
  79 definition Arity ≝ ∀A. Mem A.
  80
  81 (* the arity "sort" *)
  82 definition sort ≝ λA. sort_mem A.
  83
  84 (* the arity "constant" *)
  85 definition const: ∀B. Mem B → Arity.
  86 #B #x #A. elim (decidable_MEq B A) #H [ elim H @x | @(sort_mem A) ]
  87 qed.
  88
  89 (* application of arities *)
  90 definition aapp: MEM → Arity → Arity → Arity  ≝ λB,a,b,C. a (FUN B C) (b B).
  91
  92 (* abstraction of arities *)
  93 definition aabst: (Arity → Arity) → Arity ≝
  94    λf,C. match C return λC. Mem C with
  95    [ TOP     ⇒ sort_mem TOP
  96    | FUN B A ⇒ λx. f (const B x) A
  97    ].
  98
  99 (* extensional equality of arity members **************************************)
 100
 101 (* Extensional equality of arity members (extensional equalty of functions).
 102  * The functions may not respect extensional equality so reflexivity fails
 103  * in general but may hold for specific arity members.
 104  *)
 105 let rec ameq A ≝ match A return λA. Mem A → Mem A → Prop with
 106    [ TOP     ⇒ λa1,a2. a1 = a2
 107    | FUN B A ⇒ λa1,a2. ∀b1,b2. ameq B b1 b2 → ameq A (a1 b1) (a2 b2)
 108    ].
 109
 110 interpretation
 111    "extensional equality (arity member)"
 112    'Eq1 A a1 a2 = (ameq A a1 a2).
 113
 114 (* reflexivity of extensional equality for an arity member *)
 115 definition invariant_mem ≝ λA,m. m ≅^A m.
 116
 117 interpretation
 118    "invariance (arity member)"
 119    'Invariant1 a A = (invariant_mem A a).
 120
 121
 122 interpretation
 123    "invariance (arity member with implicit type)"
 124    'Invariant a = (invariant_mem ? a).
 125
 126 lemma symmetric_ameq: ∀A. symmetric ? (ameq A).
 127 #A elim A -A /4/
 128 qed.
 129
 130 lemma transitive_ameq: ∀A. transitive ? (ameq A).
 131 #A elim A -A /5/
 132 qed.
 133
 134 lemma invariant_sort_mem: ∀A. ! sort_mem A.
 135 #A elim A normalize //
 136 qed.
 137
 138 axiom const_eq: ∀A,x. const A x A ≅^A x.
 139
 140 axiom const_neq: ∀A,B,x. A ≠ B → const A x B ≅^B (sort_mem B).
 141
 142 (* extensional equality of arities ********************************************)
 143
 144 definition aeq: Arity → Arity → Prop ≝ λa1,a2. ∀A. a1 A ≅^A a2 A.
 145
 146 interpretation
 147    "extensional equality (arity)"
 148    'Eq a1 a2 = (aeq a1 a2).
 149
 150 definition invariant: Arity → Prop ≝ λa. a ≅ a.
 151
 152 interpretation
 153    "invariance (arity)"
 154    'Invariant a = (invariant a).
 155
 156 lemma symmetric_aeq: symmetric … aeq.
 157 /2/ qed.
 158
 159 lemma transitive_aeq: transitive … aeq.
 160 /2/ qed.
 161
 162 lemma const_comp: ∀A,x1,x2. x1 ≅^A x2 → const … x1 ≅ const … x2.
 163 #A #x1 #x2 #Hx #C elim (decidable_MEq A C) #H
 164    [ <H @transitive_ameq; [2: @const_eq | skip ]
 165         @transitive_ameq; [2: @Hx | skip ]
 166         @symmetric_ameq //
 167    | @transitive_ameq; [2: @(const_neq … H) | skip ]
 168      @transitive_ameq; [2: @invariant_sort_mem | skip ]
 169      @symmetric_ameq /2/
 170    ]
 171 qed.
 172
 173 lemma aapp_comp: ∀C,a1,a2,b1,b2. a1 ≅ a2 → b1 ≅ b2 → aapp C a1 b1 ≅ aapp C a2 b2.
 174 #C #a1 #a2 #b1 #b2 #Ha #Hb #D @(Ha (FUN C D)) //
 175 qed.
 176
 177 lemma aabst_comp: ∀f1,f2. (∀a1,a2. a1 ≅ a2 → f1 a1 ≅ f2 a2) →
 178                   aabst f1 ≅ aabst f2.
 179 #f1 #f2 #H #C elim C -C // #B #A #_ #_ #b1 #b2 #Hb @H /2/
 180 qed.
 181
 182 lemma invariant_sort: ! sort.
 183 normalize //
 184 qed.
 185
 186 (* "is a constant arity" *)
 187 definition isc ≝ λa,A. const ? (a A) ≅ a.
 188
 189 lemma isc_sort: ∀A. isc sort A.
 190 #A #C elim (decidable_MEq A C) #H [ <H // | /2 by const_neq/ ].
 191 qed.
 192
 193 lemma isc_aapp: ∀B,A,b,a. ! b B → isc a A → isc (aapp B a b) (pred A).
 194 #B #A #b #a #Hb #Ha #C elim (decidable_MEq (pred A) C) #H [ >H // ]
 195 @transitive_ameq; [2: @(const_neq … H) | skip ]
 196 lapply (transitive_ameq ????? (Ha (FUN B C))) -Ha [3: #Ha @Ha // |2: skip ]
 197 @symmetric_ameq @const_neq /2/
 198 qed.
 199
 200 (* extensional equality of arity contexts *************************************)
 201
 202 definition aceq ≝ λE1,E2. all2 … aeq E1 E2.
 203
 204 interpretation
 205    "extensional equality (arity context)"
 206    'Eq E1 E2 = (aceq E1 E2).
 207
 208 definition invariant_env: list Arity → Prop ≝ λE. E ≅ E.
 209
 210 interpretation
 211    "invariance (arity context)"
 212    'Invariant E = (invariant_env E).
 213
 214 lemma symmetric_aceq: symmetric … aceq.
 215 /2/ qed.
 216
 217 lemma nth_sort_comp: ∀E1,E2. E1 ≅ E2 →
 218                      ∀i. nth i ? E1 sort ≅ nth i ? E2 sort.
 219 #E1 #E2 #H #i @(all2_nth … aeq) //
 220 qed.