matita/matita/lib/binding/db.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 "basics/lists/list.ma".
  16
  17 axiom alpha : Type[0].
  18 notation "𝔸" non associative with precedence 90 for @{'alphabet}.
  19 interpretation "set of names" 'alphabet = alpha.
  20
  21 inductive tp : Type[0] ≝
  22 | top : tp
  23 | arr : tp → tp → tp.
  24 inductive tm : Type[0] ≝
  25 | var : nat → tm
  26 | par :  𝔸 → tm
  27 | abs : tp → tm → tm
  28 | app : tm → tm → tm.
  29
  30 let rec Nth T n (l:list T) on n ≝
  31   match l with
  32   [ nil ⇒ None ?
  33   | cons hd tl ⇒ match n with
  34     [ O ⇒ Some ? hd
  35     | S n0 ⇒ Nth T n0 tl ] ].
  36
  37 inductive judg : list tp → tm → tp → Prop ≝
  38 | t_var : ∀g,n,t.Nth ? n g = Some ? t → judg g (var n) t
  39 | t_app : ∀g,m,n,t,u.judg g m (arr t u) → judg g n t → judg g (app m n) u
  40 | t_abs : ∀g,t,m,u.judg (t::g) m u → judg g (abs t m) (arr t u).
  41
  42 definition Env := list (𝔸 × tp).
  43
  44 axiom vclose_env : Env → list tp.
  45 axiom vclose_tm : Env → tm → tm.
  46 axiom Lam : 𝔸 → tp → tm → tm.
  47 definition Judg ≝ λG,M,T.judg (vclose_env G) (vclose_tm G M) T.
  48 definition dom ≝ λG:Env.map ?? (fst ??) G.
  49
  50 definition sctx ≝ 𝔸 × tm.
  51 axiom swap_tm : 𝔸 → 𝔸 → tm → tm.
  52 definition sctx_app : sctx → 𝔸 → tm ≝ λM0,Y.let 〈X,M〉 ≝ M0 in swap_tm X Y M.
  53
  54 axiom in_list : ∀A:Type[0].A → list A → Prop.
  55 interpretation "list membership" 'mem x l = (in_list ? x l).
  56 interpretation "list non-membership" 'notmem x l = (Not (in_list ? x l)).
  57
  58 axiom in_Env : 𝔸 × tp → Env → Prop.
  59 notation "X ◃ G" non associative with precedence 45 for @{'lefttriangle $X $G}.
  60 interpretation "Env membership" 'lefttriangle x l = (in_Env x l).
  61
  62 let rec FV M ≝ match M with
  63   [ par X ⇒ [X]
  64   | app M1 M2 ⇒ FV M1@FV M2
  65   | abs T M0 ⇒ FV M0
  66   | _ ⇒ [ ] ].
  67
  68 (* axiom Lookup : 𝔸 → Env → option tp. *)
  69
  70 (* forma alto livello del judgment
  71    t_abs* : ∀G,T,X,M,U.
  72             (∀Y ∉ supp(M).Judg (〈Y,T〉::G) (M[Y]) U) →
  73             Judg G (Lam X T (M[X])) (arr T U) *)
  74
  75 (* prima dimostrare, poi perfezionare gli assiomi, poi dimostrarli *)
  76
  77 axiom Judg_ind : ∀P:Env → tm → tp → Prop.
  78   (∀X,G,T.〈X,T〉 ◃ G → P G (par X) T) →
  79   (∀G,M,N,T,U.
  80     Judg G M (arr T U) → Judg G N T →
  81     P G M (arr T U) → P G N T → P G (app M N) U) →
  82   (∀G,T1,T2,X,M1.
  83     (∀Y.Y ∉ (FV (Lam X T1 (sctx_app M1 X))) → Judg (〈Y,T1〉::G) (sctx_app M1 Y) T2) →
  84     (∀Y.Y ∉ (FV (Lam X T1 (sctx_app M1 X))) → P (〈Y,T1〉::G) (sctx_app M1 Y) T2) →
  85     P G (Lam X T1 (sctx_app M1 X)) (arr T1 T2)) →
  86   ∀G,M,T.Judg G M T → P G M T.
  87
  88 axiom t_par : ∀X,G,T.〈X,T〉 ◃ G → Judg G (par X) T.
  89 axiom t_app2 : ∀G,M,N,T,U.Judg G M (arr T U) → Judg G N T → Judg G (app M N) U.
  90 axiom t_Lam : ∀G,X,M,T,U.Judg (〈X,T〉::G) M U → Judg G (Lam X T M) (arr T U).
  91
  92 definition subenv ≝ λG1,G2.∀x.x ◃ G1 → x ◃ G2.
  93 interpretation "subenv" 'subseteq G1 G2 = (subenv G1 G2).
  94
  95 axiom daemon : ∀P:Prop.P.
  96
  97 theorem weakening : ∀G1,G2,M,T.G1 ⊆ G2 → Judg G1 M T → Judg G2 M T.
  98 #G1 #G2 #M #T #Hsub #HJ lapply Hsub lapply G2 -G2 change with (∀G2.?)
  99 @(Judg_ind … HJ)
 100 [ #X #G #T0 #Hin #G2 #Hsub @t_par @Hsub //
 101 | #G #M0 #N #T0 #U #HM0 #HN #IH1 #IH2 #G2 #Hsub @t_app2
 102   [| @IH1 // | @IH2 // ]
 103 | #G #T1 #T2 #X #M1 #HM1 #IH #G2 #Hsub @t_Lam @IH
 104   [ (* trivial property of Lam *) @daemon
 105   | (* trivial property of subenv *) @daemon ]
 106 ]
 107 qed.
 108
 109 (* Serve un tipo Tm per i termini localmente chiusi e i suoi principi di induzione e
 110    ricorsione *)