matita/matita/contribs/lambdadelta/basic_2/grammar/test.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 "arithmetics/nat.ma".
  16
  17 (* notations ****************************************************************)
  18
  19 include "basic_2/notation/constructors/snbind2_4.ma".
  20 include "basic_2/notation/constructors/dxbind2_3.ma".
  21 include "basic_2/notation/functions/weight_1.ma".
  22 include "basic_2/notation/functions/weight_3.ma".
  23
  24 (* definitions **************************************************************)
  25
  26 inductive list2 (A1,A2:Type[0]) : Type[0] :=
  27   | nil2 : list2 A1 A2
  28   | cons2: A1 → A2 → list2 A1 A2 → list2 A1 A2.
  29
  30
  31 inductive item0: Type[0] ≝
  32    | Sort: nat → item0
  33    | LRef: nat → item0
  34    | GRef: nat → item0
  35 .
  36
  37 inductive bind2: Type[0] ≝
  38   | Abbr: bind2
  39   | Abst: bind2
  40 .
  41
  42 inductive flat2: Type[0] ≝
  43   | Appl: flat2
  44   | Cast: flat2
  45 .
  46
  47 inductive item2: Type[0] ≝
  48   | Bind2: bool → bind2 → item2
  49   | Flat2: flat2 → item2
  50 .
  51
  52 inductive term: Type[0] ≝
  53   | TAtom: item0 → term
  54   | TPair: item2 → term → term → term
  55 .
  56
  57 let rec tw T ≝ match T with
  58 [ TAtom _     ⇒ 1
  59 | TPair _ V T ⇒ tw V + tw T + 1
  60 ].
  61
  62 inductive lenv: Type[0] ≝
  63 | LAtom: lenv
  64 | LPair: lenv → bind2 → term → lenv
  65 .
  66
  67 let rec lw L ≝ match L with
  68 [ LAtom       ⇒ 0
  69 | LPair L _ V ⇒ lw L + tw V
  70 ].
  71
  72 definition genv ≝ list2 bind2 term.
  73
  74 definition fw: genv → lenv → term → ? ≝ λG,L,T. (lw L) + (tw T).
  75
  76 (* interpretations **********************************************************)
  77
  78 interpretation "term binding construction (binary)"
  79    'SnBind2 a I T1 T2 = (TPair (Bind2 a I) T1 T2).
  80
  81 interpretation "weight (term)" 'Weight T = (tw T).
  82
  83 interpretation "weight (local environment)" 'Weight L = (lw L).
  84
  85 interpretation "weight (closure)" 'Weight G L T = (fw G L T).
  86
  87 (* first set *)
  88
  89 interpretation "environment binding construction (binary)"
  90    'DxBind2 L I T = (LPair L I T).
  91
  92 (* second set *)
  93
  94 interpretation "environment binding construction (binary)"
  95    'DxBind2 L I T = (cons2 bind2 term I T L).
  96
  97 (* statements ***************************************************************)
  98
  99 lemma fw_shift: ∀a,I,G,K,V,T. ♯{G, K.ⓑ{I}V, T} < ♯{G, K, ⓑ{a,I}V.T}.
 100 normalize //
 101 qed.