+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR DELAYED UPDATING ********************************************)
-
-notation "hvbox( t1 โก'd''f'[ break term 46 p, break term 46 q ] break term 46 t2 )"
- non associative with precedence 45
- for @{ 'BlackRightArrow $t1 $p $q $t2 }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR DELAYED UPDATING ********************************************)
+
+notation "hvbox( t1 โก๐๐[ break term 46 p, break term 46 q ] break term 46 t2 )"
+ non associative with precedence 45
+ for @{ 'BlackRightArrowDF $t1 $p $q $t2 }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR DELAYED UPDATING ********************************************)
+
+notation "hvbox( t1 โก๐[ break term 46 p, break term 46 q ] break term 46 t2 )"
+ non associative with precedence 45
+ for @{ 'BlackRightArrowF $t1 $p $q $t2 }.
include "delayed_updating/syntax/path_structure.ma".
include "delayed_updating/syntax/path_balanced.ma".
include "delayed_updating/substitution/fsubst.ma".
-include "delayed_updating/notation/relations/black_rightarrow_4.ma".
+include "delayed_updating/notation/relations/black_rightarrow_df_4.ma".
-(* DELAYED FOCALIZED REDUCTION **********************************************)
+(* DELAYED FOCUSED REDUCTION ************************************************)
inductive dfr (p) (q) (t): predicate preterm โ
| dfr_beta (b) (n):
.
interpretation
- "delayed focalized reduction (preterm)"
- 'BlackRightArrow t1 p q t2 = (dfr p q t1 t2).
+ "focused balanced reduction with delayed updating (preterm)"
+ 'BlackRightArrowDF t1 p q t2 = (dfr p q t1 t2).
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 "delayed_updating/reduction/ifr.ma".
+include "delayed_updating/reduction/dfr.ma".
+
+(* DELAYED FOCUSED REDUCTION ************************************************)
+
+lemma dfr_lift_bi (f) (p) (q) (t1) (t2):
+ t1 โก๐๐[p,q] t2 โ โ[f]t1 โก๐[โp,โq] โ[f]t2.
+#f #p #q #t1 #t2
+* #b #n #Hr #Hb
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 "delayed_updating/syntax/path_structure.ma".
+include "delayed_updating/syntax/path_balanced.ma".
+include "delayed_updating/substitution/fsubst.ma".
+include "delayed_updating/substitution/lift_preterm.ma".
+include "delayed_updating/notation/relations/black_rightarrow_f_4.ma".
+
+(* IMMEDIATE FOCUSED REDUCTION ************************************************)
+
+inductive ifr (p) (q) (t): predicate preterm โ
+| ifr_beta (b) (n):
+ let r โ pโ๐โbโ๐โq in
+ rโ๐ฑโจnโฉ ฯต t โ โโb โ ifr p q t (t[โrโโ[๐ฎโจnโฉ]tโ(pโ๐ฆ)])
+.
+
+interpretation
+ "focused balanced reduction with immediate updating (preterm)"
+ 'BlackRightArrowF t1 p q t2 = (ifr p q t1 t2).
lemma lift_S_sn (A) (k) (p) (f):
โโจ(ฮปp. k (๐ฆโp)), p, fโฉ = โ{A}โจk, ๐ฆโp, fโฉ.
// qed.
+
+(* Basic constructions with proj_path ***************************************)
+
+lemma lift_path_d_empty_sn (f) (n):
+ ๐ฑโจf@โจnโฉโฉโ๐ = โ[f](๐ฑโจnโฉโ๐).
+// qed.
+
+lemma lift_path_d_lcons_sn (f) (p) (l) (n):
+ โ[fโ๐ฎโจninj nโฉ](lโp) = โ[f](๐ฑโจnโฉโlโp).
+// qed.
+
+(* Basic constructions with proj_rmap ***************************************)
+
+lemma lift_rmap_d_empty_sn (f) (n):
+ f = โ[๐ฑโจnโฉโ๐]f.
+// qed.
+
+lemma lift_rmap_d_lcons_sn (f) (p) (l) (n):
+ โ[lโp](fโ๐ฎโจninj nโฉ) = โ[๐ฑโจnโฉโlโp]f.
+// qed.
+
+lemma lift_rmap_L_sn (f) (p):
+ โ[p](โซฏf) = โ[๐โp]f.
+// qed.
+
+lemma lift_rmap_A_sn (f) (p):
+ โ[p]f = โ[๐โp]f.
+// qed.
+
+lemma lift_rmap_S_sn (f) (p):
+ โ[p]f = โ[๐ฆโp]f.
+// qed.
+
+(* Advanced eliminations with path ******************************************)
+
+lemma path_ind_lift (Q:predicate โฆ):
+ Q ๐ โ
+ (โn. Q ๐ โ Q (๐ฑโจnโฉโ๐)) โ
+ (โn,l,p. Q (lโp) โ Q (๐ฑโจnโฉโlโp)) โ
+ (โp. Q p โ Q (๐โp)) โ
+ (โp. Q p โ Q (๐โp)) โ
+ (โp. Q p โ Q (๐ฆโp)) โ
+ โp. Q p.
+#Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #p
+elim p -p [| * [ #n * ] ]
+/2 width=1 by/
+qed-.
lemma lift_eq_repl_sn (A) (p) (k1) (k2) (f):
k1 โ{A} k2 โ โโจk1, p, fโฉ = โโจk2, p, fโฉ.
-#A #p elim p -p
+#A #p @(path_ind_lift โฆ p) -p [| #n | #n #l0 #q ]
[ #k1 #k2 #f #Hk <lift_empty <lift_empty //
-| * [ #n * [| #l0 ]] [|*: #q ] #IH #k1 #k2 #f #Hk /2 width=1 by/
+|*: #IH #k1 #k2 #f #Hk /2 width=1 by/
]
qed-.
<list_append_rcons_sn //
qed.
-(* Basic constructions with proj_path ***************************************)
+(* Advanced constructions with proj_path ************************************)
-lemma lift_append_sn (p) (f) (q):
+lemma lift_path_append_sn (p) (f) (q):
qโโ[f]p = โโจ(ฮปp. proj_path (qโp)), p, fโฉ.
-#p elim p -p
-[ //
-| * [ #n * [| #l ]] [|*: #p ] #IH #f #q
- [ <lift_d_empty_sn <lift_d_empty_sn >lift_lcons_alt >lift_append_rcons_sn
- <IH <IH -IH <list_append_rcons_sn //
- | <lift_d_lcons_sn <lift_d_lcons_sn <IH -IH //
- | <lift_L_sn <lift_L_sn >lift_lcons_alt >lift_append_rcons_sn
- <IH <IH -IH <list_append_rcons_sn //
- | <lift_A_sn <lift_A_sn >lift_lcons_alt >lift_append_rcons_sn
- <IH <IH -IH <list_append_rcons_sn //
- | <lift_S_sn <lift_S_sn >lift_lcons_alt >lift_append_rcons_sn
- <IH <IH -IH <list_append_rcons_sn //
- ]
+#p @(path_ind_lift โฆ p) -p // [ #n #l #p |*: #p ] #IH #f #q
+[ <lift_d_lcons_sn <lift_d_lcons_sn <IH -IH //
+| <lift_L_sn <lift_L_sn >lift_lcons_alt >lift_append_rcons_sn
+ <IH <IH -IH <list_append_rcons_sn //
+| <lift_A_sn <lift_A_sn >lift_lcons_alt >lift_append_rcons_sn
+ <IH <IH -IH <list_append_rcons_sn //
+| <lift_S_sn <lift_S_sn >lift_lcons_alt >lift_append_rcons_sn
+ <IH <IH -IH <list_append_rcons_sn //
]
qed.
-lemma lift_lcons (f) (p) (l):
+lemma lift_path_lcons (f) (p) (l):
lโโ[f]p = โโจ(ฮปp. proj_path (lโp)), p, fโฉ.
#f #p #l
->lift_lcons_alt <lift_append_sn //
+>lift_lcons_alt <lift_path_append_sn //
qed.
+
+lemma lift_path_L_sn (f) (p):
+ ๐โโ[โซฏf]p = โ[f](๐โp).
+// qed.
+
+lemma lift_path_A_sn (f) (p):
+ ๐โโ[f]p = โ[f](๐โp).
+// qed.
+
+lemma lift_path_S_sn (f) (p):
+ ๐ฆโโ[f]p = โ[f](๐ฆโp).
+// qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 "delayed_updating/syntax/preterm.ma".
+include "delayed_updating/substitution/lift.ma".
+
+(* LIFT FOR PRETERM ***********************************************************)
+
+definition lift_preterm (f) (t): preterm โ
+ ฮปp. โโr. r ฯต t & p = โ[f]r.
+
+interpretation
+ "lift (preterm)"
+ 'UpArrow f t = (lift_preterm f t).
lemma lift_d_empty_dx (n) (p) (f):
(โp)โ๐ฑโจ(โ[pโ๐ฑโจnโฉ]f)@โจnโฉโฉ = โ[f](pโ๐ฑโจnโฉ).
-#n #p elim p -p
-[| * [ #m * [| #l ]] [|*: #p ] #IH ] #f
-[ //
-| <list_cons_shift <list_cons_comm <list_cons_comm //
-| <lift_d_lcons_sn <lift_d_lcons_sn //
-| <lift_L_sn <lift_L_sn <lift_lcons <IH //
-| <lift_A_sn <lift_A_sn <lift_lcons <IH //
-| <lift_S_sn <lift_S_sn <lift_lcons <IH //
+#n #p @(path_ind_lift โฆ p) -p // [ #m #l #p |*: #p ] #IH #f
+[ <lift_rmap_d_lcons_sn <lift_path_d_lcons_sn //
+| <lift_rmap_L_sn <lift_path_L_sn <IH //
+| <lift_rmap_A_sn <lift_path_A_sn <IH //
+| <lift_rmap_S_sn <lift_path_S_sn <IH //
]
qed.
lemma lift_L_dx (p) (f):
(โp)โ๐ = โ[f](pโ๐).
-#p elim p -p
-[| * [ #m * [| #l ]] [|*: #p ] #IH ] #f
-[ //
-| //
-| <lift_d_lcons_sn //
-| <lift_L_sn <lift_lcons //
-| <lift_A_sn <lift_lcons //
-| <lift_S_sn <lift_lcons //
-]
+#p @(path_ind_lift โฆ p) -p // #m #l #p #IH #f
+<lift_path_d_lcons_sn //
qed.
lemma lift_A_dx (p) (f):
(โp)โ๐ = โ[f](pโ๐).
-#p elim p -p
-[| * [ #m * [| #l ]] [|*: #p ] #IH ] #f
-[ //
-| //
-| <lift_d_lcons_sn //
-| <lift_L_sn <lift_lcons //
-| <lift_A_sn <lift_lcons //
-| <lift_S_sn <lift_lcons //
-]
+#p @(path_ind_lift โฆ p) -p // #m #l #p #IH #f
+<lift_path_d_lcons_sn //
qed.
lemma lift_S_dx (p) (f):
(โp)โ๐ฆ = โ[f](pโ๐ฆ).
-#p elim p -p
-[| * [ #m * [| #l ]] [|*: #p ] #IH ] #f
-[ //
-| //
-| <lift_d_lcons_sn //
-| <lift_L_sn <lift_lcons //
-| <lift_A_sn <lift_lcons //
-| <lift_S_sn <lift_lcons //
-]
+#p @(path_ind_lift โฆ p) -p // #m #l #p #IH #f
+<lift_path_d_lcons_sn //
qed.
lemma structure_lift (p) (f):
โp = โโ[f]p.
-#p elim p -p
-[| * [ #m * [| #l ]] [|*: #p ] #IH ] #f
-[ //
-| //
-| //
-| <lift_L_sn <lift_lcons //
-| <lift_A_sn <lift_lcons //
-| <lift_S_sn <lift_lcons //
-]
+#p @(path_ind_lift โฆ p) -p // #p #IH #f
+<lift_path_L_sn //
qed.
lemma lift_structure (p) (f):
โp = โ[f]โp.
-#p elim p -p
-[| * [ #m * [| #l ]] [|*: #p ] #IH ] #f
-[ //
-| //
-| //
-| <structure_L_sn <lift_L_sn <lift_lcons //
-| <structure_A_sn <lift_A_sn <lift_lcons //
-| <structure_S_sn <lift_S_sn <lift_lcons //
-]
+#p @(path_ind_lift โฆ p) -p //
qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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 "delayed_updating/syntax/path_dephi.ma".
-include "delayed_updating/syntax/preterm_constructors.ma".
-
-(* DEPHI FOR PRETERM ********************************************************)
-
-definition preterm_dephi (f) (t): preterm โ
- ฮปp. โโq. q ฯต t & p = path_dephi f q.
projects / helm.git / commitdiff