From adc2a5bba9b4b907fdc1eb8ad443c97e3fdc7bd0 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 2 Mar 2011 21:02:38 +0000
Subject: [PATCH] we started the implementation of higher order saturated sets

---
 matita/matita/lib/lambda/ext.ma             | 44 ++++++++------
 matita/matita/lib/lambda/lambda_notation.ma |  4 ++
 matita/matita/lib/lambda/rc_hsat.ma         | 67 +++++++++++++++++++++
 3 files changed, 96 insertions(+), 19 deletions(-)
 create mode 100644 matita/matita/lib/lambda/rc_hsat.ma

diff --git a/matita/matita/lib/lambda/ext.ma b/matita/matita/lib/lambda/ext.ma
index ee674a9cd..ebbd051f7 100644
--- a/matita/matita/lib/lambda/ext.ma
+++ b/matita/matita/lib/lambda/ext.ma
@@ -32,6 +32,14 @@ theorem arith3: ∀x,y,z. x ≰ y → x + z ≰ y + z.
 #x #y #z #H @nmk (elim H) -H /3/
 qed.
 
+theorem arith4: ∀x,y. S x ≰ y → x≠y → y < x.
+#x #y #H1 #H2 lapply (not_le_to_lt … H1) -H1 #H1 @not_eq_to_le_to_lt /2/
+qed.
+
+theorem arith5: ∀x,y. x < y → S (y - 1) ≰ x.
+#x #y #H @lt_to_not_le <minus_Sn_m /2/
+qed.
+
 (* lists **********************************************************************)
 
 (* all(P,l) holds when P holds for all members of l *)
@@ -111,31 +119,29 @@ theorem lift_prod: ∀N,M,k,p.
                    lift (Prod N M) k p = Prod (lift N k p) (lift M (k + 1) p).
 // qed.
 
-(* telescopic non-delifting substitution of l in M.
- * [this is the telescoping delifting substitution lifted by |l|]
+theorem subst_app: ∀M,N,k,L. (App M N)[k≝L] = App M[k≝L] N[k≝L].
+// qed.
+
+theorem subst_lambda: ∀N,M,k,L. (Lambda N M)[k≝L] = Lambda N[k≝L] M[k+1≝L].
+// qed.
+
+theorem subst_prod: ∀N,M,k,L. (Prod N M)[k≝L] = Prod N[k≝L] M[k+1≝L].
+// qed.
+
+(* telescopic delifting substitution of l in M.
  * Rel 0 is replaced with the head of l
  *)
-let rec substc M l on l ≝ match l with
-   [ nil ⇒ M
-   | cons A D ⇒ (lift (substc M[0≝A] D) 0 1)
+let rec tsubst M l on l ≝ match l with
+   [ nil      ⇒ M
+   | cons A D ⇒ (tsubst M[0≝A] D)
    ]. 
 
-interpretation "Substc" 'Subst1 M l = (substc M l).
-
-(* this is just to test that substitution works as expected
-theorem test1: ∀A,B,C. (App (App (Rel 0) (Rel 1)) (Rel 2))[A::B::C::nil ?] = 
-                       App (App (lift A 0 1) (lift B 0 2)) (lift C 0 3).
-#A #B #C normalize 
->lift_0 >lift_0 >lift_0
->lift_lift1>lift_lift1>lift_lift1>lift_lift1>lift_lift1>lift_lift1
-normalize
-qed.
-*)
+interpretation "telescopic substitution" 'Subst1 M l = (tsubst M l).
 
-theorem substc_refl: ∀l,t. (lift t 0 (|l|))[l] = (lift t 0 (|l|)).
-#l (elim l) -l (normalize) // #A #D #IHl #t cut (S (|D|) = |D| + 1) // (**) (* eliminate cut *)
+theorem tsubst_refl: ∀l,t. (lift t 0 (|l|))[l] = t.
+#l (elim l) -l (normalize) // #hd #tl #IHl #t cut (S (|tl|) = |tl| + 1) // (**) (* eliminate cut *)
 qed.
 
-theorem substc_sort: ∀n,l. (Sort n)[l] = Sort n.
+theorem tsubst_sort: ∀n,l. (Sort n)[l] = Sort n.
 //
 qed.
diff --git a/matita/matita/lib/lambda/lambda_notation.ma b/matita/matita/lib/lambda/lambda_notation.ma
index 42f3eb2aa..f7f8d9d8f 100644
--- a/matita/matita/lib/lambda/lambda_notation.ma
+++ b/matita/matita/lib/lambda/lambda_notation.ma
@@ -20,6 +20,10 @@ notation "hvbox(a break ≅ b)"
   non associative with precedence 45
   for @{'Eq $a $b}.
 
+notation "hvbox(a break (≅ ^ term 90 c) b)"
+  non associative with precedence 45
+  for @{'Eq1 $c $a $b}.
+
 (* lifting, substitution *)
 
 notation "hvbox(M break [ l ])"
diff --git a/matita/matita/lib/lambda/rc_hsat.ma b/matita/matita/lib/lambda/rc_hsat.ma
new file mode 100644
index 000000000..55f8cba43
--- /dev/null
+++ b/matita/matita/lib/lambda/rc_hsat.ma
@@ -0,0 +1,67 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "lambda/rc_sat.ma".
+
+(* HIGHER ORDER REDUCIBILITY CANDIDATES ***************************************)
+
+(* An arity is a type of λ→ to be used as carrier for a h.o. r.c. *)
+inductive ARITY: Type[0] ≝
+   | SORT: ARITY
+   | IMPL: ARITY → ARITY → ARITY
+.
+
+(* The type of the higher order r.c.'s having a given carrier.
+ * a h.o. r.c is implemented as an inductively defined metalinguistic function
+ * [ a CIC function in the present case ]. 
+ *)
+let rec HRC P ≝ match P with
+   [ SORT     ⇒ RC
+   | IMPL Q P ⇒ HRC Q → HRC P
+   ].
+
+(* The default h.o r.c.
+ * This is needed to complete the partial interpretation of types.
+ *)
+let rec defHRC P ≝ match P return λP. HRC P with
+   [ SORT     ⇒ snRC
+   | IMPL Q P ⇒ λ_. defHRC P
+   ].
+
+(* extensional equality *******************************************************)
+
+(* This is the extensional equalty of functions
+ * modulo the extensional equality on the domain.
+ * The functions may not respect extensional equality so reflexivity fails.
+ *)
+let rec hrceq P ≝ match P return λP. HRC P → HRC P → Prop with
+   [ SORT     ⇒ λC1,C2. C1 ≅ C2
+   | IMPL Q P ⇒ λC1,C2. ∀B1,B2. hrceq Q B1 B2 → hrceq P (C1 B1) (C2 B2)
+   ].
+
+interpretation
+   "extensional equality (h.o. reducibility candidate)"
+   'Eq1 P C1 C2 = (hrceq P C1 C2).
+
+lemma symmetric_hrceq: ∀P. symmetric ? (hrceq P).
+#P (elim P) -P /4/
+qed.
+
+lemma transitive_hrceq: ∀P. transitive ? (hrceq P).
+#P (elim P) -P /5/
+qed.
+
+lemma reflexive_defHRC: ∀P. defHRC P ≅^P defHRC P.
+#P (elim P) -P (normalize) /2/
+qed.
-- 
2.39.2