--- /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( ๐ )"
+ non associative with precedence 70
+ for @{ 'ClassT }.
+++ /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( ฦฌ term 70 x )"
- non associative with precedence 45
- for @{ 'PredicateTHook $x }.
include "delayed_updating/syntax/path_structure.ma".
include "delayed_updating/syntax/path_balanced.ma".
include "delayed_updating/syntax/prototerm_constructors.ma".
+include "delayed_updating/syntax/prototerm_equivalence.ma".
include "delayed_updating/substitution/fsubst.ma".
include "delayed_updating/notation/relations/black_rightarrow_df_4.ma".
(* DELAYED FOCUSED REDUCTION ************************************************)
-inductive dfr (p) (q) (t): predicate prototerm โ
-| dfr_beta (b):
- let r โ pโ๐โbโ๐โq in
- rโ๐ฑ(โโqโ) ฯต t โ โ(โb) โ dfr p q t (t[โrโ๐(โโqโ).tโ(pโ๐ฆ)])
+definition dfr (p) (q): relation2 prototerm prototerm โ
+ ฮปt1,t2. โb.
+ let r โ pโ๐โbโ๐โq in
+ โงโง โ(โb) & rโ๐ฑ(โโqโ) ฯต t1 &
+ t2 โ t1[โrโ๐(โโqโ).t1โ(pโ๐ฆ)]
.
interpretation
(* DELAYED FOCUSED REDUCTION ************************************************)
-lemma dfr_lift_bi (f) (p) (q) (t1) (t2): ฦฌt1 โ
+lemma dfr_lift_bi (f) (p) (q) (t1) (t2): t1 ฯต ๐ โ
t1 โก๐๐[p,q] t2 โ โ[f]t1 โก๐[โp,โq] โ[f]t2.
-#f #p #q #t1 #t2 #Ht1
-* -t2 #b #Hr #Hb
+#f #p #q #t1 #t2 #H0t1
+* #b * #Hb #Ht1 #Ht2
+@(ex_intro โฆ (โb)) @and3_intro
+[ //
+| lapply (in_comp_lift_bi f โฆ Ht1) -Ht1 #Ht1
+
+
+
+
+
(* IMMEDIATE FOCUSED REDUCTION ************************************************)
-inductive ifr (p) (q) (t): predicate prototerm โ
-| ifr_beta (b):
- let r โ pโ๐โbโ๐โq in
- rโ๐ฑ(โโqโ) ฯต t โ โ(โb) โ ifr p q t (t[โrโโ[๐ฎโจโโqโโฉ]tโ(pโ๐ฆ)])
+definition ifr (p) (q): relation2 prototerm prototerm โ
+ ฮปt1,t2. โb.
+ let r โ pโ๐โbโ๐โq in
+ โงโง โ(โb) & rโ๐ฑ(โโqโ) ฯต t1 &
+ t2 โ t1[โrโโ[๐ฎโจโโqโโฉ]t1โ(pโ๐ฆ)]
.
interpretation
(* FOCALIZED SUBSTITUTION ***************************************************)
-lemma lift_fsubst_sn (f) (t) (u) (p): ๊u โ p โงธฯต t โ
+lemma lift_fsubst_sn (f) (t) (u) (p): ๊u โ
(โ[f]t)[โ(โp)โโ[โ[p]f]u] โ โ[f](t[โpโu]).
-#f #t #u #p #Hu #Hp #ql * *
+#f #t #u #p #Hu #ql * *
[ #rl * #r #Hr #H1 #H2 destruct
>lift_append_proper_dx
/4 width=1 by subset_in_ext_f1_dx, or_introl/
| * #q #Hq #H1 #H0
- @(ex2_intro โฆ H1) @or_intror @conj //
- #r #H2 destruct
- @H0 -H0 [| <lift_append_proper_dx /2 width=1 by/ ]
+ @(ex2_intro โฆ H1) @or_intror @conj // *
+ [ <list_append_empty_dx #H2 destruct
+ elim (lift_root f q) #r #_ #Hr /2 width=2 by/
+ | #l #r #H2 destruct
+ @H0 -H0 [| <lift_append_proper_dx /2 width=3 by ppc_lcons/ ]
+ ]
]
qed-.
-lemma lift_fsubst_dx (f) (t) (u) (p): ๊u โ p ฯต โตt โ structure_injective t โ
+lemma lift_fsubst_dx (f) (t) (u) (p): ๊u โ p ฯต โตt โ t ฯต ๐ โ
โ[f](t[โpโu]) โ (โ[f]t)[โ(โp)โโ[โ[p]f]u].
#f #t #u #p #Hu #H1p #H2p #ql * #q * *
[ #r #Hu #H1 #H2 destruct
]
qed-.
-lemma lift_fsubst (f) (t) (u) (p): ๊u โ p โงธฯต t โ p ฯต โตt โ structure_injective t โ
+lemma lift_fsubst (f) (t) (u) (p): ๊u โ p ฯต โตt โ t ฯต ๐ โ
(โ[f]t)[โ(โp)โโ[โ[p]f]u] โ โ[f](t[โpโu]).
/4 width=3 by lift_fsubst_sn, conj, lift_fsubst_dx/ qed.
interpretation
"lift (prototerm)"
'UpArrow f t = (subset_ext_f1 ? ? (lift_gen ? proj_path f) t).
+
+(* Basic constructions ******************************************************)
+
+lemma in_comp_lift_bi (f) (p) (t):
+ p ฯต t โ โ[f]p ฯต โ[f]t.
+/2 width=1 by subset_in_ext_f1_dx/ qed.
#p #f <lift_append_proper_dx //
qed.
+lemma lift_root (f) (p):
+ โโr. ๐ = โr & โpโr = โ[f]p.
+#f #p @(list_ind_rcons โฆ p) -p
+[ /2 width=3 by ex2_intro/
+| #p * [ #n ] /2 width=3 by ex2_intro/
+]
+qed-.
+
(* Advanced inversions with proj_path ***************************************)
lemma lift_path_inv_d_sn (k) (q) (p) (f):
(๐ฑkโq) = โ[f]p โ
- โโr,h. ๐ = โr & (โ[r]f)@โจhโฉ = k & ๐ = q & rโ๐ฑh = p.
+ โโr,h. ๐ = โr & (โ[r]f)@โจhโฉ = k & ๐ = q & rโ๐ฑh = p.
#k #q #p @(path_ind_lift โฆ p) -p
[| #n | #n #l #p |*: #p ] [|*: #IH ] #f
[ <lift_path_empty #H destruct
include "delayed_updating/syntax/prototerm.ma".
include "delayed_updating/syntax/path_structure.ma".
-include "delayed_updating/notation/relations/predicate_t_hook_1.ma".
+include "delayed_updating/notation/functions/class_t_0.ma".
(* PRETERM ******************************************************************)
+(* Note: a preterm is a prototerm satislying the condition below *)
(* Note: different root paths have different structure *)
definition structure_injective: predicate prototerm โ
ฮปt. โp1,p2. p1 ฯต โตt โ p2 ฯต โตt โ โp1 = โp2 โ p1 = p2
.
-(* Note: a preterm is a prototerm satislying the conditions above *)
-record is_preterm (t): Prop โ
-{
- is_pt_injective: structure_injective t
-}.
-
interpretation
- "preterm condition (prototerm)"
- 'PredicateTHook t = (is_preterm t).
+ "preterm (prototerm)"
+ 'ClassT = (structure_injective).
projects / helm.git / commitdiff