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. ∀p,f. k1 p f = k2 p f.
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, p, f❩ = ↑❨k2, p, f❩.
32 [ #k1 #k2 #f #Hk <lift_empty <lift_empty //
33 | * [ #n * [| #l0 ]] [|*: #q ] #IH #k1 #k2 #f #Hk /2 width=1 by/
37 (* Advanced constructions ***************************************************)
39 lemma lift_lcons_alt (A) (k) (f) (p) (l):
40 ↑❨λp2.k(l◗p2),p,f❩ = ↑{A}❨λp2.k((l◗𝐞)●p2),p,f❩.
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 ↑❨λp2.k(p1●l◗p2),p,f❩ = ↑{A}❨λp2.k(p1◖l●p2),p,f❩.
48 @lift_eq_repl_sn #p2 #g
49 <list_append_rcons_sn //
52 (* Basic constructions with proj_path ***************************************)
54 lemma lift_append_sn (p) (f) (q):
55 q●↑[f]p = ↑❨(λp. proj_path (q●p)), p, f❩.
58 | * [ #n * [| #l ]] [|*: #p ] #IH #f #q
59 [ <lift_d_empty_sn <lift_d_empty_sn >lift_lcons_alt >lift_append_rcons_sn
60 <IH <IH -IH <list_append_rcons_sn //
61 | <lift_d_lcons_sn <lift_d_lcons_sn <IH -IH //
62 | <lift_L_sn <lift_L_sn >lift_lcons_alt >lift_append_rcons_sn
63 <IH <IH -IH <list_append_rcons_sn //
64 | <lift_A_sn <lift_A_sn >lift_lcons_alt >lift_append_rcons_sn
65 <IH <IH -IH <list_append_rcons_sn //
66 | <lift_S_sn <lift_S_sn >lift_lcons_alt >lift_append_rcons_sn
67 <IH <IH -IH <list_append_rcons_sn //
72 lemma lift_lcons (f) (p) (l):
73 l◗↑[f]p = ↑❨(λp. proj_path (l◗p)), p, f❩.
75 >lift_lcons_alt <lift_append_sn //