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
  22  * (see for instance [Cescutti 2001], but a better citation is required)
  23  * rather than standard reducibility candidates.
  24  * The benefit is that reduction is not needed to define such subsets.
  25  * Also, this approach was never tried on a system with dependent types.
  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 (* a generalization of mem on lists *)
  46 let rec memc E l on l : Prop ≝ match l with
  47    [ nil ⇒ True
  48    | cons hd tl ⇒ match E with
  49       [ nil      ⇒ hd ∈ snRC ∧ memc E tl
  50       | cons C D ⇒ hd ∈ C ∧ memc D tl
  51       ]
  52    ].
  53
  54 interpretation
  55    "componentwise membership (context of reducibility candidates)"
  56    'mem l H = (memc H l).
  57
  58 (* extensional equality of r.c.'s *********************************************)
  59
  60 definition rceq: RC → RC → Prop ≝
  61                  λC1,C2. ∀M. (M ∈ C1 → M ∈ C2) ∧ (M ∈ C2 → M ∈ C1).
  62
  63 interpretation
  64    "extensional equality (reducibility candidate)"
  65    'napart C1 C2 = (rceq C1 C2).
  66
  67 definition rceql ≝ λl1,l2. all2 ? rceq l1 l2.
  68
  69 interpretation
  70    "extensional equality (context of reducibility candidates)"
  71    'napart C1 C2 = (rceql C1 C2).
  72
  73 theorem reflexive_rceq: reflexive … rceq.
  74 /2/ qed.
  75
  76 theorem symmetric_rceq: symmetric … rceq.
  77 #x #y #H #M (elim (H M)) -H /3/
  78 qed.
  79
  80 theorem transitive_rceq: transitive … rceq.
  81 #x #y #z #Hxy #Hyz #M (elim (Hxy M)) -Hxy (elim (Hyz M)) -Hyz /4/
  82 qed.
  83
  84 theorem reflexive_rceql: reflexive … rceql.
  85 #l (elim l) /2/
  86 qed.
  87
  88 (* HIDDEN BUG:
  89  * Without the type specification, this statement has two interpretations
  90  * but matita does not complain
  91  *)
  92 theorem mem_rceq_trans: ∀(M:T). ∀C1,C2. M ∈ C1 → C1 ≈ C2 → M ∈ C2.
  93 #M #C1 #C2 #H1 #H12 (elim (H12 M)) -H12 /2/
  94 qed.
  95
  96 (* NOTE: hd_repl and tl_repl are proved essentially by the same script *)
  97 theorem hd_repl: ∀C1,C2. C1 ≈ C2 → ∀l1,l2. l1 ≈ l2 → hd ? l1 C1 ≈ hd ? l2 C2.
  98 #C1 #C2 #QC #l1 (elim l1) -l1 [ #l2 #Q >Q // ]
  99 #hd1 #tl1 #_ #l2 (elim l2) -l2 [ #Q elim Q ]
 100 #hd2 #tl2 #_ #Q elim Q //
 101 qed.
 102
 103 theorem tl_repl: ∀l1,l2. l1 ≈ l2 → tail ? l1 ≈ tail ? l2.
 104 #l1 (elim l1) -l1 [ #l2 #Q >Q // ]
 105 #hd1 #tl1 #_ #l2 (elim l2) -l2 [ #Q elim Q ]
 106 #hd2 #tl2 #_ #Q elim Q //
 107 qed.
 108
 109 theorem nth_repl: ∀C1,C2. C1 ≈ C2 → ∀i,l1,l2. l1 ≈ l2 →
 110                   nth i ? l1 C1 ≈ nth i ? l2 C2.
 111 #C1 #C2 #QC #i (elim i) /3/
 112 qed.
 113
 114 (* the r.c for a (dependent) product type. ************************************)
 115
 116 definition dep_mem ≝ λB,C,M. ∀N. N ∈ B → App M N ∈ C.
 117
 118 axiom dep_cr1: ∀B,C. CR1 (dep_mem B C).
 119
 120 axiom dep_sat0: ∀B,C. SAT0 (dep_mem B C).
 121
 122 axiom dep_sat1: ∀B,C. SAT1 (dep_mem B C).
 123
 124 axiom dep_sat2: ∀B,C. SAT2 (dep_mem B C).
 125
 126 definition depRC: RC → RC → RC ≝ λB,C. mk_RC (dep_mem B C) ….
 127 /2/ qed.
 128
 129 theorem dep_repl: ∀B1,B2,C1,C2. B1 ≈ B2 → C1 ≈ C2 →
 130                   depRC B1 C1 ≈ depRC B2 C2.
 131 #B1 #B2 #C1 #C2 #QB #QC #M @conj #H1 #N #H2
 132 [ lapply (symmetric_rceq … QB) -QB | lapply (symmetric_rceq … QC) -QC ] /4/
 133 qed.