matita/matita/lib/lambda/rc.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/sn.ma".
  16
  17 let rec substc M l on l ≝ match l with
  18    [ nil ⇒ M
  19    | cons A D ⇒ lift (substc M D)[0≝A] 0 1
  20    ].
  21
  22 notation "M [ l ]" non associative with precedence 90 for @{'Substc $M $l}.
  23
  24 interpretation "Substc" 'Substc M l = (substc M l).
  25
  26 theorem substc_sort: ∀n,l. (Sort n)[l] = Sort n.
  27 #n #l (elim l) -l // #A #D #IH normalize >IH -IH. normalize //
  28 qed.
  29
  30 (* REDUCIBILITY CANDIDATES ****************************************************)
  31
  32 (* nautral terms *)
  33 inductive neutral: T → Prop ≝
  34    | neutral_sort: ∀n.neutral (Sort n)
  35    | neutral_rel: ∀i.neutral (Rel i)
  36    | neutral_app: ∀M,N.neutral (App M N)
  37 .
  38
  39 (* the reducibility candidates (r.c.) *)
  40 record RC : Type[0] ≝ {
  41    mem : T → Prop;
  42    cr1 : ∀t. mem t → SN t;
  43    sat0: ∀l,n. all mem l → mem (Appl (Sort n) l);
  44    sat1: ∀l,i. all mem l → mem (Appl (Rel i) l);
  45    sat2: ∀F,A,B,l. mem B → mem A →
  46          mem (Appl F[0:=A] l) → mem (Appl (Lambda B F) (A::l))
  47 }.
  48
  49 interpretation "membership (reducibility candidate)" 'mem A R = (mem R A).
  50
  51 (* the r.c. of all s.n. terms *)
  52 definition snRC: RC ≝ mk_RC SN ….
  53 /2/ qed.
  54
  55 (* the carrier of the r.c. of a (dependent) product type *)
  56 definition dep_mem ≝ λRA,RB,M. ∀N. N ∈ RA → App M N ∈ RB.
  57
  58 (* the r.c. of a (dependent) product type *)
  59 axiom depRC: RC → RC → RC.
  60 (* FG
  61  * ≝ λRA,RB. mk_RC (dev_mem RA RB) ?.
  62  *)
  63
  64 (* a generalization of mem on lists *)
  65 let rec memc H l on l : Prop ≝ match l with
  66    [ nil ⇒ True
  67    | cons A D ⇒ match H with
  68       [ nil      ⇒ A ∈ snRC ∧ memc H D
  69       | cons R K ⇒ A ∈ R ∧ memc K D
  70       ]
  71    ].
  72
  73 interpretation "componentwise membership (context of reducibility candidates)" 'mem l H = (memc H l).
  74
  75 (* the r.c. associated to a type *)
  76 let rec trc H t on t : RC ≝ match t with
  77    [ Sort _     ⇒ snRC
  78    | Rel i      ⇒ nth i … H snRC
  79    | App _ _    ⇒ snRC (* FG ??? *)
  80    | Lambda _ _ ⇒ snRC
  81    | Prod A B   ⇒ depRC (trc H A) (trc (trc H A :: H) B)
  82    | D _        ⇒ snRC (* FG ??? *)
  83    ].
  84
  85 notation "hvbox(〚T〛 _ term 90 E)" non associative with precedence 50 for @{'InterpE $T $E}.
  86
  87 interpretation "interpretation of a type" 'InterpE t H = (trc H t).
  88
  89 (* the r.c. context associated to a context *)
  90 let rec trcc H G on G : list RC ≝ match G with
  91    [ nil      ⇒ H
  92    | cons A D ⇒ 〚A〛_(trcc H D) :: trcc H D
  93    ].
  94
  95 interpretation "interpretation of a context" 'InterpE G H = (trcc H G).
  96
  97 theorem tj_trc: ∀G,A,B. G ⊢A:B → ∀H,l. l ∈ 〚G〛_(H) →
  98                 A[l] ∈ 〚B[l]〛_〚G〛_(H).
  99 #G #A #B #tjAB (elim tjAB) -G A B tjAB
 100    [ #i #j #_ #H #l #_ >substc_sort >substc_sort @(sn_sort (nil ?)) //
 101    | #G #B #n #tjB #IH #H #l (elim l) -l (normalize)
 102      [ #_
 103      | #C #D #IHl #mem (elim mem) -mem #mem #memc
 104 (*
 105 theorem tj_sn: ∀G,A,B. G ⊢A:B → SN A.
 106 #G #A #B #tjAB lapply (tj_trc … tjAB (nil ?) (nil ?)) -tjAB (normalize) /3/
 107 qed.
 108 *)