matita/matita/lib/pts_dummy/rc_hsat.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 "pts_dummy/rc_sat.ma".
  16 (*
  17 (* HIGHER ORDER REDUCIBILITY CANDIDATES ***************************************)
  18
  19 (* An arity is a type of λ→ to be used as carrier for a h.o. r.c. *)
  20
  21 (* The type of the higher order r.c.'s having a given carrier.
  22  * a h.o. r.c is implemented as an inductively defined metalinguistic function
  23  * [ a CIC function in the present case ].
  24  *)
  25 let rec HRC P ≝ match P with
  26    [ SORT     ⇒ RC
  27    | ABST Q P ⇒ HRC Q → HRC P
  28    ].
  29
  30 (* The default h.o r.c.
  31  * This is needed to complete the partial interpretation of types.
  32  *)
  33 let rec defHRC P ≝ match P return λP. HRC P with
  34    [ SORT     ⇒ snRC
  35    | ABST Q P ⇒ λ_. defHRC P
  36    ].
  37
  38 (* extensional equality *******************************************************)
  39
  40 (* This is the extensional equalty of functions
  41  * modulo the extensional equality on the domain.
  42  * The functions may not respect extensional equality so reflexivity fails.
  43  *)
  44 let rec hrceq P ≝ match P return λP. HRC P → HRC P → Prop with
  45    [ SORT     ⇒ λC1,C2. C1 ≅ C2
  46    | ABST Q P ⇒ λC1,C2. ∀B1,B2. hrceq Q B1 B2 → hrceq P (C1 B1) (C2 B2)
  47    ].
  48
  49 interpretation
  50    "extensional equality (h.o. reducibility candidate)"
  51    'Eq1 P C1 C2 = (hrceq P C1 C2).
  52
  53 lemma symmetric_hrceq: ∀P. symmetric ? (hrceq P).
  54 #P (elim P) -P /4/
  55 qed.
  56
  57 lemma transitive_hrceq: ∀P. transitive ? (hrceq P).
  58 #P (elim P) -P /5/
  59 qed.
  60
  61 lemma reflexive_defHRC: ∀P. defHRC P ≅^P defHRC P.
  62 #P (elim P) -P (normalize) /2/
  63 qed.
  64 *)