ā[p]f = ā[š¦āp]f.
// qed.
+(* Advanced cinstructionswith proj_rmap and tr_id ***************************)
+
+lemma lift_rmap_id (p):
+ (š¢) = ā[p]š¢.
+#p elim p -p //
+* [ #n ] #p #IH //
+qed.
+
(* Advanced constructions with proj_rmap and path_append ********************)
lemma lift_rmap_append (p2) (p1) (f):
--- /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/substitution/lift_length.ma".
+include "delayed_updating/notation/functions/black_downtriangle_1.ma".
+include "ground/relocation/tr_uni.ma".
+
+(* BASIC UNWIND FOR PATH ****************************************************)
+
+rec definition unwind1_path_pnat (n) (p) on n ā
+match n with
+[ punit ā p
+| psucc m ā
+ match p with
+ [ list_empty ā š
+ | list_lcons l q ā
+ match l with
+ [ label_d n ā
+ match q with
+ [ list_empty ā lā(unwind1_path_pnat m q)
+ | list_lcons _ _ ā unwind1_path_pnat m (ā[š®āØnā©]q)
+ ]
+ | label_m ā unwind1_path_pnat m q
+ | label_L ā šā(unwind1_path_pnat m q)
+ | label_A ā šā(unwind1_path_pnat m q)
+ | label_S ā š¦ā(unwind1_path_pnat m q)
+ ]
+ ]
+].
+
+definition unwind1_path (p) ā
+ unwind1_path_pnat (āāpā) p.
+
+interpretation
+ "basic unwind (path)"
+ 'BlackDownTriangle p = (unwind1_path p).
+
+(* Basic constructions ******************************************************)
+
+lemma unwind1_path_unfold (p):
+ unwind1_path_pnat (āāpā) p = ā¼p.
+// qed-.
+
+lemma unwind1_path_empty:
+ (š) = ā¼š.
+// qed.
+
+lemma unwind1_path_d_empty (n):
+ (š±nāš) = ā¼(š±nāš).
+// qed.
+
+lemma unwind1_path_d_lcons (p) (l) (n:pnat):
+ ā¼(ā[š®āØnā©](lāp)) = ā¼(š±nālāp).
+#p #l #n
+<unwind1_path_unfold <lift_path_length //
+qed.
+
+lemma unwind1_path_m_sn (p):
+ ā¼p = ā¼(šŗāp).
+// qed.
+
+lemma unwind1_path_L_sn (p):
+ (šāā¼p) = ā¼(šāp).
+// qed.
+
+lemma unwind1_path_A_sn (p):
+ (šāā¼p) = ā¼(šāp).
+// qed.
+
+lemma unwind1_path_S_sn (p):
+ (š¦āā¼p) = ā¼(š¦āp).
+// qed.
+
+(* Main constructions *******************************************************)
+
+fact unwind1_path_fix_aux (k) (p):
+ k = āpā ā ā¼p = ā¼ā¼p.
+#k @(nat_ind_succ ā¦ k) -k
+[ #p #H0 >(list_length_inv_zero_sn ā¦ H0) -p //
+| #k #IH *
+ [ #H0 elim (eq_inv_nsucc_zero ā¦ H0)
+ | * [ #n ] #p #H0
+ lapply (eq_inv_nsucc_bi ā¦ H0) -H0
+ [ cases p -p [ -IH | #l #p ] #H0 destruct //
+ <unwind1_path_d_lcons <IH -IH //
+ | #H0 destruct <unwind1_path_m_sn <IH -IH //
+ | #H0 destruct <unwind1_path_L_sn <unwind1_path_L_sn <IH -IH //
+ | #H0 destruct <unwind1_path_A_sn <unwind1_path_A_sn <IH -IH //
+ | #H0 destruct <unwind1_path_S_sn <unwind1_path_S_sn <IH -IH //
+ ]
+ ]
+]
+qed-.
+
+theorem unwind1_path_fix (p):
+ ā¼p = ā¼ā¼p.
+/2 width=2 by unwind1_path_fix_aux/ 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/unwind0/unwind1_rmap_eq.ma".
+include "delayed_updating/unwind0/unwind1_path.ma".
+include "delayed_updating/substitution/lift_structure.ma".
+
+(* BASIC UNWIND FOR PATH ****************************************************)
+
+(* Constructions with structure *********************************************)
+
+fact unwind1_path_d_dx_aux (k) (p) (n):
+ k = āpā ā (āp)āš±((ā¶p)@āØnā©) = ā¼(pāš±n).
+#k @(nat_ind_succ ā¦ k) -k
+[ #p #n #H0 >(list_length_inv_zero_sn ā¦ H0) -p //
+| #k #IH *
+ [ #n #H0 elim (eq_inv_nsucc_zero ā¦ H0)
+ | * [ #m ] #p #n #H0
+ lapply (eq_inv_nsucc_bi ā¦ H0) -H0
+ [ cases p -p [ -IH | #l #p ] #H0 destruct <unwind1_path_d_lcons
+ [ <lift_path_d_sn <lift_path_empty <unwind1_path_d_empty
+ <list_cons_comm <(tr_pap_eq_repl ā¦ (unwind1_rmap_d_empty ā¦)) //
+ | >list_cons_shift <lift_path_d_dx <IH -IH //
+ <structure_lift <structure_d_sn /3 width=1 by eq_f2/
+ ]
+ | #H0 destruct <unwind1_path_m_sn <IH -IH //
+ | #H0 destruct <unwind1_path_L_sn <IH -IH //
+ | #H0 destruct <unwind1_path_A_sn <IH -IH //
+ | #H0 destruct <unwind1_path_S_sn <IH -IH //
+ ]
+ ]
+]
+qed-.
+
+lemma unwind1_path_d_dx (p) (n):
+ (āp)āš±((ā¶p)@āØnā©) = ā¼(pāš±n).
+/2 width=2 by unwind1_path_d_dx_aux/ 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/substitution/lift_length.ma".
+include "delayed_updating/notation/functions/black_righttriangle_1.ma".
+include "ground/relocation/tr_uni.ma".
+include "ground/relocation/tr_compose.ma".
+
+(* BASIC UNWIND FOR RELOCATION MAP ******************************************)
+
+rec definition unwind1_rmap_pnat (n) (p) on n ā
+match n with
+[ punit ā š¢
+| psucc m ā
+ match p with
+ [ list_empty ā š¢
+ | list_lcons l q ā
+ match l with
+ [ label_d n ā (unwind1_rmap_pnat m (ā[š®āØnā©]q))ā(ā[q]š®āØnā©)
+ | label_m ā unwind1_rmap_pnat m q
+ | label_L ā unwind1_rmap_pnat m q
+ | label_A ā unwind1_rmap_pnat m q
+ | label_S ā unwind1_rmap_pnat m q
+ ]
+ ]
+].
+
+definition unwind1_rmap (p) ā
+ unwind1_rmap_pnat (āāpā) p.
+
+interpretation
+ "basic unwind (relocation map)"
+ 'BlackRightTriangle p = (unwind1_rmap p).
+
+(* Basic constructions ******************************************************)
+
+lemma unwind1_rmap_unfold (p):
+ unwind1_rmap_pnat (āāpā) p = ā¶p.
+// qed-.
+
+lemma unwind1_rmap_empty:
+ (š¢) = ā¶(š).
+// qed.
+
+lemma unwind1_rmap_d_sn (p) (n:pnat):
+ (ā¶(ā[š®āØnā©]p))ā(ā[p]š®āØnā©) = ā¶(š±nāp).
+#p #n
+<unwind1_rmap_unfold <lift_path_length //
+qed.
+
+lemma unwind1_rmap_m_sn (p):
+ ā¶p = ā¶(šŗāp).
+// qed.
+
+lemma unwind1_rmap_L_sn (p):
+ ā¶p = ā¶(šāp).
+// qed.
+
+lemma unwind1_rmap_A_sn (p):
+ ā¶p = ā¶(šāp).
+// qed.
+
+lemma unwind1_rmap_S_sn (p):
+ ā¶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/unwind0/unwind1_rmap.ma".
+include "ground/relocation/tr_id_compose.ma".
+
+(* BASIC UNWIND FOR RELOCATION MAP ******************************************)
+
+(* Constructions with stream_eq *********************************************)
+
+lemma unwind1_rmap_d_empty (n:pnat):
+ (š®āØnā©) ā ā¶(š±nāš).
+// 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/unwind0/unwind1_path.ma".
+include "delayed_updating/notation/functions/black_downtriangle_2.ma".
+
+(* EXTENDED UNWIND FOR PATH *************************************************)
+
+definition unwind2_path (f) (p) ā
+ ā¼ā[f]p.
+
+interpretation
+ "extended unwind (path)"
+ 'BlackDownTriangle f p = (unwind2_path f p).
+
+(* Basic constructions ******************************************************)
+
+lemma unwind2_path_unfold (f) (p):
+ ā¼ā[f]p = ā¼[f]p.
+// qed.
+
+lemma unwind2_path_id (p):
+ ā¼p = ā¼[š¢]p.
+// qed.
+
+lemma unwind2_path_empty (f):
+ (š) = ā¼[f]š.
+// qed.
+
+lemma unwind2_path_d_empty (f) (n):
+ (š±(f@āØnā©)āš) = ā¼[f](š±nāš).
+// qed.
+
+lemma unwind2_path_d_lcons (f) (p) (l) (n:pnat):
+ ā¼[š®āØf@āØnā©ā©](lāp) = ā¼[f](š±nālāp).
+#f #p #l #n
+<unwind2_path_unfold in ā¢ (???%);
+<lift_path_d_sn <lift_path_id <unwind1_path_d_lcons //
+qed.
+
+lemma unwind2_path_m_sn (f) (p):
+ ā¼[f]p = ā¼[f](šŗāp).
+#f #p
+<unwind2_path_unfold in ā¢ (???%);
+<lift_path_m_sn //
+qed.
+
+lemma unwind2_path_L_sn (f) (p):
+ (šāā¼[ā«Æf]p) = ā¼[f](šāp).
+#f #p
+<unwind2_path_unfold in ā¢ (???%);
+<lift_path_L_sn //
+qed.
+
+lemma unwind2_path_A_sn (f) (p):
+ (šāā¼[f]p) = ā¼[f](šāp).
+#f #p
+<unwind2_path_unfold in ā¢ (???%);
+<lift_path_A_sn //
+qed.
+
+lemma unwind2_path_S_sn (f) (p):
+ (š¦āā¼[f]p) = ā¼[f](š¦āp).
+#f #p
+<unwind2_path_unfold in ā¢ (???%);
+<lift_path_S_sn //
+qed.
+
+(* Main constructions *******************************************************)
+
+theorem unwind2_path_after_id_sn (p) (f):
+ ā¼[f]p = ā¼ā¼[f]p.
+// qed.
+
+(* Constructions with stream_eq *********************************************)
+
+lemma unwind2_path_eq_repl (p):
+ stream_eq_repl ā¦ (Ī»f1,f2. ā¼[f1]p = ā¼[f2]p).
+#p #f1 #f2 #Hf
+<unwind2_path_unfold <unwind2_path_unfold
+<(lift_path_eq_repl ā¦ Hf) -Hf //
+qed.
+
+(* Advanced eliminations with path ******************************************)
+
+lemma path_ind_unwind2 (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 (š¦āp)) ā
+ āp. Q p.
+#Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #p
+elim p -p [| * [ #n * ] ]
+/2 width=1 by/
+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/unwind0/unwind2_rmap.ma".
+include "delayed_updating/unwind0/unwind2_path.ma".
+include "delayed_updating/unwind0/unwind1_path_structure.ma".
+
+(* EXTENDED UNWIND FOR PATH *************************************************)
+
+(* Constructions with structure *********************************************)
+
+lemma unwind2_path_d_dx (f) (p) (n):
+ (āp)āš±((ā¶[f]p)@āØnā©) = ā¼[f](pāš±n).
+#f #p #n
+<unwind2_path_unfold <lift_path_d_dx <unwind1_path_d_dx
+<structure_lift >tr_compose_pap //
+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/unwind0/unwind1_rmap.ma".
+include "delayed_updating/notation/functions/black_righttriangle_2.ma".
+
+(* EXTENDED UNWIND FOR RELOCATION MAP ***************************************)
+
+definition unwind2_rmap (f) (p): tr_map ā
+ (ā¶ā[f]p)ā(ā[p]f).
+
+interpretation
+ "extended unwind (relocation map)"
+ 'BlackRightTriangle f p = (unwind2_rmap f p).
+
+(* Basic constructions ******************************************************)
+
+lemma unwind2_rmap_unfold (f) (p):
+ (ā¶ā[f]p)ā(ā[p]f) = ā¶[f]p.
+// qed.
+
+lemma unwind2_rmap_m_sn (f) (p):
+ ā¶[f]p = ā¶[f](šŗāp).
+#f #p
+<unwind2_rmap_unfold in ā¢ (???%);
+<lift_rmap_m_sn <lift_path_m_sn //
+qed.
+
+lemma unwind2_rmap_L_sn (f) (p):
+ ā¶[ā«Æf]p = ā¶[f](šāp).
+#f #p
+<unwind2_rmap_unfold in ā¢ (???%);
+<lift_rmap_L_sn <lift_path_L_sn //
+qed.
+
+lemma unwind2_rmap_A_sn (f) (p):
+ ā¶[f]p = ā¶[f](šāp).
+#f #p
+<unwind2_rmap_unfold in ā¢ (???%);
+<lift_rmap_A_sn <lift_path_A_sn //
+qed.
+
+lemma unwind2_rmap_S_sn (f) (p):
+ ā¶[f]p = ā¶[f](š¦āp).
+#f #p
+<unwind2_rmap_unfold in ā¢ (???%);
+<lift_rmap_S_sn <lift_path_S_sn //
+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/unwind0/unwind2_rmap.ma".
+include "ground/relocation/tr_id_compose.ma".
+
+(* EXTENDED UNWIND FOR RELOCATION MAP ***************************************)
+
+(* Advanced constructions ***************************************************)
+
+lemma unwind2_rmap_id (p):
+ ā¶p ā ā¶[š¢]p.
+// qed.
+
+lemma unwind2_rmap_empty (f):
+ f ā ā¶[f]š.
+// qed.
+
+lemma unwind2_rmap_d_sn (f) (p) (n):
+ ā¶[š®āØf@āØnā©ā©]p ā ā¶[f](š±nāp).
+#f #p #n
+<unwind2_rmap_unfold <unwind2_rmap_unfold
+<lift_rmap_d_sn <lift_rmap_id
+<lift_path_d_sn <lift_path_id <unwind1_rmap_d_sn //
+qed.
projects / helm.git / commitdiff