1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "delayed_updating/substitution/lift.ma".
16 include "ground/notation/relations/ringeq_3.ma".
18 (* LIFT FOR PATH ***********************************************************)
20 definition lift_exteq (A): relation2 (lift_continuation A) (lift_continuation A) ≝
21 λk1,k2. ∀f,p. k1 f p = k2 f p.
24 "extensional equivalence (lift continuation)"
25 'RingEq A k1 k2 = (lift_exteq A k1 k2).
27 (* Constructions with lift_exteq ********************************************)
29 lemma lift_eq_repl_sn (A) (p) (k1) (k2) (f):
30 k1 ≗{A} k2 → ↑❨k1, f, p❩ = ↑❨k2, f, p❩.
31 #A #p @(path_ind_lift … p) -p [| #n | #n #l0 #q ]
32 [ #k1 #k2 #f #Hk <lift_empty <lift_empty //
33 |*: #IH #k1 #k2 #f #Hk /2 width=1 by/
37 (* Advanced constructions ***************************************************)
39 lemma lift_lcons_alt (A) (k) (f) (p) (l):
40 ↑❨λg,p2. k g (l◗p2), f, p❩ = ↑{A}❨λg,p2. k g ((l◗𝐞)●p2), f, p❩.
42 @lift_eq_repl_sn #p2 #g // (**) (* auto fails with typechecker failure *)
45 lemma lift_append_rcons_sn (A) (k) (f) (p1) (p) (l):
46 ↑❨λg,p2. k g (p1●l◗p2), f, p❩ = ↑{A}❨λg,p2. k g (p1◖l●p2), f, p❩.
48 @lift_eq_repl_sn #p2 #g
49 <list_append_rcons_sn //
52 (* Advanced constructions with proj_path ************************************)
54 lemma lift_path_append_sn (p) (f) (q):
55 q●↑[f]p = ↑❨(λg,p. proj_path g (q●p)), f, p❩.
56 #p @(path_ind_lift … p) -p // [ #n #l #p |*: #p ] #IH #f #q
57 [ <lift_d_lcons_sn <lift_d_lcons_sn <IH -IH //
58 | <lift_L_sn <lift_L_sn >lift_lcons_alt >lift_append_rcons_sn
59 <IH <IH -IH <list_append_rcons_sn //
60 | <lift_A_sn <lift_A_sn >lift_lcons_alt >lift_append_rcons_sn
61 <IH <IH -IH <list_append_rcons_sn //
62 | <lift_S_sn <lift_S_sn >lift_lcons_alt >lift_append_rcons_sn
63 <IH <IH -IH <list_append_rcons_sn //
67 lemma lift_path_lcons (f) (p) (l):
68 l◗↑[f]p = ↑❨(λg,p. proj_path g (l◗p)), f, p❩.
70 >lift_lcons_alt <lift_path_append_sn //
73 lemma lift_path_L_sn (f) (p):
74 (𝗟◗↑[⫯f]p) = ↑[f](𝗟◗p).
77 lemma lift_path_A_sn (f) (p):
78 (𝗔◗↑[f]p) = ↑[f](𝗔◗p).
81 lemma lift_path_S_sn (f) (p):
82 (𝗦◗↑[f]p) = ↑[f](𝗦◗p).