matita/matita/lib/lambda/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 }.
  34 (* HIDDEN BUG:
  35  * if SAT0 and SAT1 are expanded,
  36  * the projections sat0 and sat1 are not generated
  37  *)
  38
  39 interpretation "membership (reducibility candidate)" 'mem A R = (mem R A).
  40
  41 (* the r.c. of all s.n. terms *)
  42 definition snRC: RC ≝ mk_RC SN ….
  43 /2/ qed.
  44
  45 (*
  46 (* a generalization of mem on lists *)
  47 let rec memc E l on l : Prop ≝ match l with
  48    [ nil ⇒ True
  49    | cons hd tl ⇒ match E with
  50       [ nil      ⇒ hd ∈ snRC ∧ memc E tl
  51       | cons C D ⇒ hd ∈ C ∧ memc D tl
  52       ]
  53    ].
  54
  55 interpretation
  56    "componentwise membership (context of reducibility candidates)"
  57    'mem l H = (memc H l).
  58 *)
  59 (* extensional equality of r.c.'s *********************************************)
  60
  61 definition rceq: RC → RC → Prop ≝
  62                  λC1,C2. ∀M. (M ∈ C1 → M ∈ C2) ∧ (M ∈ C2 → M ∈ C1).
  63
  64 interpretation
  65    "extensional equality (reducibility candidate)"
  66    'Eq C1 C2 = (rceq C1 C2).
  67
  68 definition rceql ≝ λl1,l2. all2 ? rceq l1 l2.
  69
  70 interpretation
  71    "extensional equality (context of reducibility candidates)"
  72    'Eq C1 C2 = (rceql C1 C2).
  73
  74 theorem reflexive_rceq: reflexive … rceq.
  75 /2/ qed.
  76
  77 theorem symmetric_rceq: symmetric … rceq.
  78 #x #y #H #M (elim (H M)) -H /3/
  79 qed.
  80
  81 theorem transitive_rceq: transitive … rceq.
  82 #x #y #z #Hxy #Hyz #M (elim (Hxy M)) -Hxy (elim (Hyz M)) -Hyz /4/
  83 qed.
  84 (*
  85 theorem reflexive_rceql: reflexive … rceql.
  86 #l (elim l) /2/
  87 qed.
  88 *)
  89 (* HIDDEN BUG:
  90  * Without the type specification, this statement has two interpretations
  91  * but matita does not complain
  92  *)
  93 theorem mem_rceq_trans: ∀(M:T). ∀C1,C2. M ∈ C1 → C1 ≅ C2 → M ∈ C2.
  94 #M #C1 #C2 #H1 #H12 (elim (H12 M)) -H12 /2/
  95 qed.
  96
  97 (* NOTE: hd_repl and tl_repl are proved essentially by the same script *)
  98 theorem hd_repl: ∀C1,C2. C1 ≅ C2 → ∀l1,l2. l1 ≅ l2 → hd ? l1 C1 ≅ hd ? l2 C2.
  99 #C1 #C2 #QC #l1 (elim l1) -l1 [ #l2 #Q >Q // ]
 100 #hd1 #tl1 #_ #l2 (elim l2) -l2 [ #Q elim Q ]
 101 #hd2 #tl2 #_ #Q elim Q //
 102 qed.
 103
 104 theorem tl_repl: ∀l1,l2. l1 ≅ l2 → tail ? l1 ≅ tail ? l2.
 105 #l1 (elim l1) -l1 [ #l2 #Q >Q // ]
 106 #hd1 #tl1 #_ #l2 (elim l2) -l2 [ #Q elim Q ]
 107 #hd2 #tl2 #_ #Q elim Q //
 108 qed.
 109
 110 theorem nth_repl: ∀C1,C2. C1 ≅ C2 → ∀i,l1,l2. l1 ≅ l2 →
 111                   nth i ? l1 C1 ≅ nth i ? l2 C2.
 112 #C1 #C2 #QC #i (elim i) /3/
 113 qed.
 114
 115 (* the r.c for a (dependent) product type. ************************************)
 116
 117 definition dep_mem ≝ λB,C,M. ∀N. N ∈ B → App M N ∈ C.
 118
 119 theorem dep_cr1: ∀B,C. CR1 (dep_mem B C).
 120 #B #C #M #Hdep (lapply (Hdep (Sort 0) ?)) /2 by SAT0_sort/ /3/ (**) (* adiacent auto *)
 121 qed.
 122
 123 theorem dep_sat0: ∀B,C. SAT0 (dep_mem B C).
 124 /5/ qed.
 125
 126 theorem dep_sat1: ∀B,C. SAT1 (dep_mem B C).
 127 /5/ qed.
 128
 129 (* NOTE: @sat2 is not needed if append_cons is enabled *)
 130 theorem dep_sat2: ∀B,C. SAT2 (dep_mem B C).
 131 #B #C #N #L #M #l #HN #HL #HM #K #HK <appl_append @sat2 /2/
 132 qed.
 133
 134 definition depRC: RC → RC → RC ≝ λB,C. mk_RC (dep_mem B C) ….
 135 /2/ qed.
 136
 137 theorem dep_repl: ∀B1,B2,C1,C2. B1 ≅ B2 → C1 ≅ C2 →
 138                   depRC B1 C1 ≅ depRC B2 C2.
 139 #B1 #B2 #C1 #C2 #QB #QC #M @conj #H1 #N #H2
 140 [ lapply (symmetric_rceq … QB) -QB | lapply (symmetric_rceq … QC) -QC ] /4/
 141 qed.
 142
 143