interpretation
"balanced focused reduction with delayed updating (prototerm)"
'BlackRightArrowDBF t1 r t2 = (dbfr r t1 t2).
+
+(* Constructions with subset_equivalence ************************************)
+
+lemma dbfr_eq_trans (t) (t1) (t2) (r):
+ t1 ➡𝐝𝐛𝐟[r] t → t ⇔ t2 → t1 ➡𝐝𝐛𝐟[r] t2.
+#t #t1 #t2 #r
+* #p #b #q #m #n #Hr #Hb #Hm #Hn #Ht1 #Ht #Ht2
+/3 width=13 by subset_eq_trans, ex6_5_intro/
+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/reduction/dbfr.ma".
+include "delayed_updating/substitution/fsubst_constructors.ma".
+include "delayed_updating/substitution/fsubst_eq.ma".
+include "delayed_updating/syntax/prototerm_constructors_eq.ma".
+
+(* DELAYED BALANCED FOCUSED REDUCTION ***************************************)
+
+(* Constructions with constructors for prototerm ****************************)
+
+lemma dbfr_abst_hd (t1) (t2) (r):
+ t1 ➡𝐝𝐛𝐟[r] t2 → 𝛌.t1 ➡𝐝𝐛𝐟[𝗟◗r] 𝛌.t2.
+#t1 #t2 #r *
+#p #b #q #m #n #Hr #Hb #Hm #Hn #Ht1 #Ht2 destruct
+@(ex6_5_intro … (𝗟◗p) … Hb Hm Hn) -Hb -Hm -Hn
+[ -Ht2 //
+| -Ht2 /2 width=1 by in_comp_abst_hd/
+| @(subset_eq_trans … (abst_eq_repl … Ht2)) -Ht1 -Ht2
+ @(subset_eq_canc_sn … (fsubst_abst_hd …)) @abst_eq_repl
+ @fsubst_eq_repl // @iref_eq_repl
+ >list_cons_shift @(subset_eq_canc_sn … (grafted_abst_hd … )) //
+]
+qed.
+
+lemma dbfr_appl_hd (v) (t1) (t2) (r):
+ t1 ➡𝐝𝐛𝐟[r] t2 → ＠v.t1 ➡𝐝𝐛𝐟[𝗔◗r] ＠v.t2.
+#v #t1 #t2 #r *
+#p #b #q #m #n #Hr #Hb #Hm #Hn #Ht1 #Ht2 destruct
+@(ex6_5_intro … (𝗔◗p) … Hb Hm Hn) -Hb -Hm -Hn
+[ -Ht2 //
+| -Ht2 /2 width=1 by in_comp_appl_hd/
+| @(subset_eq_trans … (appl_eq_repl … Ht2)) -Ht1 -Ht2 [|*: // ]
+ @(subset_eq_canc_sn … (fsubst_appl_hd …)) @appl_eq_repl [ // ]
+ @fsubst_eq_repl // @iref_eq_repl
+ >list_cons_shift @(subset_eq_canc_sn … (grafted_appl_hd … )) //
+]
+qed.
+
+lemma dbfr_appl_sd (v1) (v2) (t) (r):
+ v1 ➡𝐝𝐛𝐟[r] v2 → ＠v1.t ➡𝐝𝐛𝐟[𝗦◗r] ＠v2.t.
+#v1 #v2 #t #r *
+#p #b #q #m #n #Hr #Hb #Hm #Hn #Hv1 #Hv2 destruct
+@(ex6_5_intro … (𝗦◗p) … Hb Hm Hn) -Hb -Hm -Hn
+[ -Hv2 //
+| -Hv2 /2 width=1 by in_comp_appl_sd/
+| @(subset_eq_trans ????? (appl_eq_repl …)) [3: @Hv2 |2,4: // |5: skip ]
+ @(subset_eq_canc_sn … (fsubst_appl_sd …)) @appl_eq_repl [| // ]
+ @fsubst_eq_repl // @iref_eq_repl
+ >list_cons_shift @(subset_eq_canc_sn … (grafted_appl_sd … )) //
+]
+qed.
+
+lemma dbfr_beta_0 (v) (t) (q) (n):
+ q ϵ 𝐂❨Ⓕ,n❩ → q◖𝗱↑n ϵ t →
+ ＠v.𝛌.t ➡𝐝𝐛𝐟[𝗔◗𝗟◗q] ＠v.𝛌.(t[⋔q←𝛕↑n.v]).
+#v #t #q #n #Hn #Ht
+@(ex6_5_intro … (𝐞) (𝐞) q (𝟎) … Hn) -Hn
+[ //
+| //
+| //
+| /3 width=1 by in_comp_appl_hd, in_comp_abst_hd/
+| @(subset_eq_canc_sn … (fsubst_appl_hd …)) @appl_eq_repl [ // ]
+ @(subset_eq_canc_sn … (fsubst_abst_hd …)) @abst_eq_repl
+ @fsubst_eq_repl // <nplus_zero_sn @iref_eq_repl
+ >list_cons_comm @(subset_eq_canc_sn … (grafted_appl_sd … ))
+ @(subset_eq_canc_sn … (grafted_empty_dx … )) //
+]
+qed.
+(*
+lemma dbfr_beta_1 (v) (v1) (t) (q) (n):
+ q ϵ 𝐂❨Ⓕ,n❩ → q◖𝗱↑n ϵ t →
+ ＠v.＠v1.𝛌.𝛌.t ➡𝐝𝐛𝐟[𝗔◗𝗔◗𝗟◗𝗟◗q] ＠v.＠v1.𝛌.𝛌.(t[⋔q←🠡[𝐮❨↑↑n❩]v]).
+#v #v1 #t #q #n #Hn #Ht
+@(ex6_5_intro … (𝐞) (𝗔◗𝗟◗𝐞) q (𝟏) … Hn) -Hn
+[ //
+| /2 width=1 by pbc_empty, pbc_redex/
+| /3 width=1 by pcc_A_sn, pcc_L_sn, pcc_empty/
+| /5 width=1 by in_comp_appl_hd, in_comp_abst_hd/
+| @(subset_eq_canc_sn … (fsubst_appl_hd …)) @appl_eq_repl [ // ]
+ @(subset_eq_canc_sn … (fsubst_appl_hd …)) @appl_eq_repl [ // ]
+ @(subset_eq_canc_sn … (fsubst_abst_hd …)) @abst_eq_repl
+ @(subset_eq_canc_sn … (fsubst_abst_hd …)) @abst_eq_repl
+ @fsubst_eq_repl // <nplus_unit_sn @lift_term_eq_repl_dx
+ >list_cons_comm @(subset_eq_canc_sn … (grafted_appl_sd … ))
+ @(subset_eq_canc_sn … (grafted_empty_dx … )) //
+]
+qed.
+*)
(* *)
(**************************************************************************)
+include "delayed_updating/reduction/dbfr_constructors.ma".
include "delayed_updating/reduction/ibfr_constructors.ma".
+include "delayed_updating/unwind/unwind2_prototerm_constructors.ma".
include "delayed_updating/substitution/lift_prototerm_constructors.ma".
include "ground/arith/pnat_two.ma".
(* DELAYED BALANCED FOCUSED REDUCTION ***************************************)
-(* Prerequisites ************************************************************)
+(* Example of unprotected balanced β-reduction ******************************)
-lemma list_rcons_prop_1 (A) (a1) (a2):
- ⓔ ⨭ a1 ⨭{A} a2 = a1 ⨮ (ⓔ ⨭ a2).
-// qed.
+definition l3_t: prototerm ≝
+ (＠(⧣𝟏).＠(𝛌.⧣𝟏).𝛌.⧣𝟏).
-(* Example of unprotected balanced β-reduction ******************************)
+definition l3_i1: prototerm ≝
+ (＠(⧣𝟏).＠(𝛌.⧣𝟏).𝛌.𝛌.⧣𝟏).
-definition l3_t0: prototerm ≝
- (𝛌.＠(⧣𝟏).＠(𝛌.＠(⧣𝟐).⧣𝟏).𝛌.⧣𝟏).
+definition l3_i2: prototerm ≝
+ (＠(⧣𝟏).＠(𝛌.⧣𝟏).𝛌.𝛌.⧣↑𝟐).
-definition l3_t1: prototerm ≝
- (𝛌.＠(⧣𝟏).＠(𝛌.＠(⧣𝟐).⧣𝟏).𝛌.(𝛌.＠(⧣↑𝟐).⧣𝟏)).
+definition l3_d1: prototerm ≝
+ (＠(⧣𝟏).＠(𝛌.⧣𝟏).𝛌.𝛕𝟏.𝛌.⧣𝟏).
-definition l3_t2: prototerm ≝
- (𝛌.＠(⧣𝟏).＠(𝛌.＠(⧣𝟐).⧣𝟏).𝛌.(𝛌.＠(⧣↑𝟐).⧣↑𝟐)).
+definition l3_d2: prototerm ≝
+ (＠(⧣𝟏).＠(𝛌.⧣𝟏).𝛌.𝛕𝟏.𝛌.𝛕𝟏.⧣𝟏).
-lemma l3_t01:
- l3_t0 ➡𝐢𝐛𝐟[𝗟◗𝗔◗𝗔◗𝗟◗𝐞] l3_t1.
-@ibfr_abst_hd
+lemma l3_ti1:
+ l3_t ➡𝐢𝐛𝐟[𝗔◗𝗔◗𝗟◗𝐞] l3_i1.
@ibfr_appl_hd
@ibfr_eq_trans [| @ibfr_beta_0 // ]
@appl_eq_repl [ // ]
@(subset_eq_canc_sn … (fsubst_empty_rc …))
@(subset_eq_canc_sn … (lift_term_abst …))
@abst_eq_repl
-@(subset_eq_canc_sn … (lift_term_appl … ))
-@appl_eq_repl
@(subset_eq_canc_sn … (lift_term_oref_pap … )) //
qed.
-lemma l3_t12:
- l3_t1 ➡𝐢𝐛𝐟[𝗟◗𝗔◗𝗔◗𝗟◗𝗟◗𝗔◗𝐞] l3_t2.
-@ibfr_abst_hd
-@ibfr_eq_trans
-[| @(ibfr_beta_1 … (𝟎)) [| <list_rcons_prop_1 ]
- /2 width=3 by pcc_A_sn, in_comp_appl_hd/
-]
+lemma l3_i12:
+ l3_i1 ➡𝐢𝐛𝐟[𝗔◗𝗔◗𝗟◗𝗟◗𝐞] l3_i2.
+@ibfr_eq_trans [| @ibfr_beta_1 // ]
@appl_eq_repl [ // ]
@appl_eq_repl [ // ]
@abst_eq_repl
@abst_eq_repl
-@(subset_eq_canc_sn … (fsubst_appl_hd …))
-@appl_eq_repl [ // ]
@(subset_eq_canc_sn … (fsubst_empty_rc …))
@(subset_eq_canc_sn … (lift_term_oref_pap … )) //
qed.
+
+lemma l3_td1:
+ l3_t ➡𝐝𝐛𝐟[𝗔◗𝗔◗𝗟◗𝐞] l3_d1.
+@dbfr_appl_hd
+@dbfr_eq_trans [| @dbfr_beta_0 // ]
+@appl_eq_repl [ // ]
+@abst_eq_repl
+@(subset_eq_canc_sn … (fsubst_empty_rc …)) //
+qed.
+
+lemma ld_di2:
+ l3_i2 ⇔ ▼[𝐢]l3_d2.
+@(subset_eq_canc_sn … (unwind2_term_appl …)) @appl_eq_repl
+[ @(subset_eq_canc_sn … (unwind2_term_oref_pap …)) // ]
+@(subset_eq_canc_sn … (unwind2_term_appl …)) @appl_eq_repl
+[ @(subset_eq_canc_sn … (unwind2_term_abst …)) @abst_eq_repl
+ @(subset_eq_canc_sn … (unwind2_term_oref_pap …)) //
+]
+@(subset_eq_canc_sn … (unwind2_term_abst …)) @abst_eq_repl
+@(subset_eq_canc_sn … (unwind2_term_iref …))
+@(subset_eq_canc_sn … (unwind2_term_abst …)) @abst_eq_repl
+@(subset_eq_canc_sn … (unwind2_term_iref …))
+@(subset_eq_canc_sn … (unwind2_term_oref_pap …)) //
+qed.
(* Constructions with constructors for prototerm ****************************)
-lemma unwind2_term_iref_sn (f) (t) (k:pnat):
- ▼[f∘𝐮❨k❩]t ⊆ ▼[f](𝛕k.t).
-#f #t #k #p * #q #Hq #H0 destruct
-@(ex2_intro … (𝗱k◗𝗺◗q))
-/2 width=1 by in_comp_iref_hd/
-qed-.
-
-lemma unwind2_term_iref_dx (f) (t) (k:pnat):
- ▼[f](𝛕k.t) ⊆ ▼[f∘𝐮❨k❩]t.
-#f #t #k #p * #q #Hq #H0 destruct
-elim (in_comp_inv_iref … Hq) -Hq #p #Hp #Ht destruct
-/2 width=1 by in_comp_unwind2_path_term/
-qed-.
+lemma unwind2_term_oref_pap (f) (k):
+ (⧣(f＠⧣❨k❩)) ⇔ ▼[f]⧣k.
+#f #k @conj #p *
+[ /2 width=1 by in_comp_unwind2_path_term/
+| #q * #H0 destruct //
+]
+qed.
lemma unwind2_term_iref (f) (t) (k:pnat):
▼[f∘𝐮❨k❩]t ⇔ ▼[f](𝛕k.t).
-/3 width=2 by conj, unwind2_term_iref_sn, unwind2_term_iref_dx/
+#f #t #k @conj
+#p * #q #Hq #H0 destruct
+[ @(ex2_intro … (𝗱k◗𝗺◗q))
+ /2 width=1 by in_comp_iref_hd/
+| elim (in_comp_inv_iref … Hq) -Hq #p #Hp #Ht destruct
+ /2 width=1 by in_comp_unwind2_path_term/
+]
+qed.
+
+lemma unwind2_term_abst (f) (t):
+ (𝛌.▼[⫯f]t) ⇔ ▼[f]𝛌.t.
+#f #t @conj #p #Hp
+[ elim (in_comp_inv_abst … Hp) -Hp #q #H1 * #r #Hr #H2 destruct
+ /3 width=1 by in_comp_unwind2_path_term, in_comp_abst_hd/
+| elim Hp -Hp #q #Hq #H0 destruct
+ elim (in_comp_inv_abst … Hq) -Hq #r #H0 #Hr destruct
+ /3 width=1 by in_comp_unwind2_path_term, in_comp_abst_hd/
+]
+qed.
+
+lemma unwind2_term_appl (f) (v) (t):
+ ＠▼[f]v.▼[f]t ⇔ ▼[f]＠v.t.
+#f #v #t @conj #p #Hp
+[ elim (in_comp_inv_appl … Hp) -Hp * #q #H1 * #r #Hr #H2 destruct
+ /3 width=1 by in_comp_unwind2_path_term, in_comp_appl_sd, in_comp_appl_hd/
+| elim Hp -Hp #q #Hq #H0 destruct
+ elim (in_comp_inv_appl … Hq) -Hq * #r #H0 #Hr destruct
+ /3 width=1 by in_comp_unwind2_path_term, in_comp_appl_sd, in_comp_appl_hd/
+]
qed.
--- /dev/null
+lemma list_rcons_prop_1 (A) (a1) (a2):
+ ⓔ ⨭ a1 ⨭{A} a2 = a1 ⨮ (ⓔ ⨭ a2).
+// qed.
projects / helm.git / commitdiff