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