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