matita/matita/lib/lambdaN/rc_sat.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 (* REDUCIBILITY CANDIDATES ****************************************************)
  18
  19 (* The reducibility candidate (r.c.) ******************************************)
  20
  21 (* We use saturated subsets of strongly normalizing terms [1]
  22  * rather than standard reducibility candidates [2].
  23  * The benefit is that reduction is not needed to define such subsets.
  24  * [1] Geuvers, H. 1994. A Short and Flexible Proof of Strong Normalization for the Calculus of Constructions.
  25  * [2] Barras, B. 1996. Coq en Coq. Rapport de Recherche 3026, INRIA.
  26  *)
  27 record RC : Type[0] ≝ {
  28    mem : T → Prop;
  29    cr1 : CR1 mem;
  30    sat0: SAT0 mem;
  31    sat1: SAT1 mem;
  32    sat2: SAT2 mem;
  33    sat3: SAT3 mem;  (* we add the clusure by rev dapp *)
  34    sat4: SAT4 mem   (* we add the clusure by dummies *)
  35 }.
  36
  37 (* HIDDEN BUG:
  38  * if SAT0 and SAT1 are expanded,
  39  * the projections sat0 and sat1 are not generated
  40  *)
  41
  42 interpretation "membership (reducibility candidate)" 'mem A R = (mem R A).
  43
  44 (* the r.c. of all s.n. terms *)
  45 definition snRC: RC ≝ mk_RC SN ….
  46 /2/ qed.
  47
  48 (*
  49 (* a generalization of mem on lists *)
  50 let rec memc E l on l : Prop ≝ match l with
  51    [ nil ⇒ True
  52    | cons hd tl ⇒ match E with
  53       [ nil      ⇒ hd ∈ snRC ∧ memc E tl
  54       | cons C D ⇒ hd ∈ C ∧ memc D tl
  55       ]
  56    ].
  57
  58 interpretation
  59    "componentwise membership (context of reducibility candidates)"
  60    'mem l H = (memc H l).
  61 *)
  62 (* extensional equality of r.c.'s *********************************************)
  63
  64 definition rceq: RC → RC → Prop ≝
  65                  λC1,C2. ∀M. (M ∈ C1 → M ∈ C2) ∧ (M ∈ C2 → M ∈ C1).
  66
  67 interpretation
  68    "extensional equality (reducibility candidate)"
  69    'Eq C1 C2 = (rceq C1 C2).
  70
  71 definition rceql ≝ λl1,l2. all2 … rceq l1 l2.
  72
  73 interpretation
  74    "extensional equality (context of reducibility candidates)"
  75    'Eq C1 C2 = (rceql C1 C2).
  76
  77 lemma reflexive_rceq: reflexive … rceq.
  78 /2/ qed.
  79
  80 lemma symmetric_rceq: symmetric … rceq.
  81 #x #y #H #M elim (H M) -H /3/
  82 qed.
  83
  84 lemma transitive_rceq: transitive … rceq.
  85 #x #y #z #Hxy #Hyz #M elim (Hxy M) -Hxy; elim (Hyz M) -Hyz /4/
  86 qed.
  87 (*
  88 theorem reflexive_rceql: reflexive … rceql.
  89 #l (elim l) /2/
  90 qed.
  91 *)
  92 (* HIDDEN BUG:
  93  * Without the type specification, this statement has two interpretations
  94  * but matita does not complain
  95  *)
  96 lemma mem_rceq_trans: ∀(M:T). ∀C1,C2. M ∈ C1 → C1 ≅ C2 → M ∈ C2.
  97 #M #C1 #C2 #H1 #H12 elim (H12 M) -H12 /2/
  98 qed.
  99 (*
 100 (* NOTE: hd_repl and tl_repl are proved essentially by the same script *)
 101 lemma hd_repl: ∀C1,C2. C1 ≅ C2 → ∀l1,l2. l1 ≅ l2 → hd ? l1 C1 ≅ hd ? l2 C2.
 102 #C1 #C2 #QC #l1 (elim l1) -l1 [ #l2 #Q >Q // ]
 103 #hd1 #tl1 #_ #l2 (elim l2) -l2 [ #Q elim Q ]
 104 #hd2 #tl2 #_ #Q elim Q //
 105 qed.
 106
 107 lemma tl_repl: ∀l1,l2. l1 ≅ l2 → tail ? l1 ≅ tail ? l2.
 108 #l1 (elim l1) -l1 [ #l2 #Q >Q // ]
 109 #hd1 #tl1 #_ #l2 (elim l2) -l2 [ #Q elim Q ]
 110 #hd2 #tl2 #_ #Q elim Q //
 111 qed.
 112
 113 lemma nth_repl: ∀C1,C2. C1 ≅ C2 → ∀i,l1,l2. l1 ≅ l2 →
 114                   nth i ? l1 C1 ≅ nth i ? l2 C2.
 115 #C1 #C2 #QC #i (elim i) /3/
 116 qed.
 117 *)
 118 (* the r.c. for a (dependent) product type. ***********************************)
 119
 120 definition dep_mem ≝ λB,C,M. ∀N. N ∈ B → App M N ∈ C.
 121
 122 lemma dep_cr1: ∀B,C. CR1 (dep_mem B C).
 123 #B #C #M #Hdep (lapply (Hdep (Sort 0) ?)) -Hdep /3/ @SAT0_sort //
 124 qed.
 125
 126 lemma dep_sat0: ∀B,C. SAT0 (dep_mem B C).
 127 /5/ qed.
 128
 129 lemma dep_sat1: ∀B,C. SAT1 (dep_mem B C).
 130 /5/ qed.
 131
 132 (* NOTE: @sat2 is not needed if append_cons is enabled *)
 133 lemma dep_sat2: ∀B,C. SAT2 (dep_mem B C).
 134 #B #C #N #L #M #l #HN #HL #HM #K #HK <appl_append @sat2 /2/
 135 qed.
 136
 137 lemma dep_sat3: ∀B,C. SAT3 (dep_mem B C).
 138 #B #C #M #N #l #H #L #HL <appl_append @sat3 /2/
 139 qed.
 140
 141 lemma dep_sat4: ∀B,C. SAT4 (dep_mem B C).
 142 #B #C #N #HN #M #HM @SAT3_1 /3/
 143 qed.
 144
 145 definition depRC: RC → RC → RC ≝ λB,C. mk_RC (dep_mem B C) ….
 146 /2/ qed.
 147
 148 lemma dep_repl: ∀B1,B2,C1,C2. B1 ≅ B2 → C1 ≅ C2 →
 149                 depRC B1 C1 ≅ depRC B2 C2.
 150 #B1 #B2 #C1 #C2 #QB #QC #M @conj #H1 #N #H2
 151 [ lapply (symmetric_rceq … QB) -QB | lapply (symmetric_rceq … QC) -QC ] /4/
 152 qed.
 153
 154 (* the union of two r.c.'s. ***************************************************)
 155
 156 definition lor_mem ≝ λB,C,M. M ∈ B ∨ M ∈ C.
 157
 158 lemma lor_cr1: ∀B,C. CR1 (lor_mem B C).
 159 #B #C #M #Hlor elim Hlor -Hlor #HM /2/
 160 qed.
 161
 162 lemma lor_sat0: ∀B,C. SAT0 (lor_mem B C).
 163 /3/ qed.
 164
 165 lemma lor_sat1: ∀B,C. SAT1 (lor_mem B C).
 166 /3/ qed.
 167
 168 lemma lor_sat2: ∀B,C. SAT2 (lor_mem B C).
 169 #B #C #N #L #M #l #HN #HL #HM elim HM -HM #HM /3/
 170 qed.
 171
 172 lemma lor_sat3: ∀B,C. SAT3 (lor_mem B C).
 173 #B #C #N #l1 #l2 #HN elim HN -HN #HN /3/
 174 qed.
 175
 176 lemma lor_sat4: ∀B,C. SAT4 (lor_mem B C).
 177 #B #C #N #HN elim HN -HN #HN /3/
 178 qed.
 179
 180 definition lorRC: RC → RC → RC ≝ λB,C. mk_RC (lor_mem B C) ….
 181 /2/ qed.