REGISTRY = $(RT_BASE_DIR)/matita.conf.xml
OBJS = cic:/matita/lambdadelta/basic_1/pr0/pr0/pr0_confluence.con\
- cic:/matita/lambdadelta/basic_1/pr0/defs/pr0_ind.con
+ cic:/matita/lambdadelta/basic_1/pr0/defs/pr0_ind.con\
+ cic:/matita/lambdadelta/basic_1/pr0/defs/pr0.ind
test:
- @echo MaTeX: $(OBJS:cic:/matita/lambdadelta/basic_1/pr0/%.con=%)
+ @echo MaTeX: $(OBJS:cic:/matita/lambdadelta/basic_1/pr0/%=%)
$(H)./matex.native -O test -t -p $(REGISTRY) $(OBJS)
.PHONY: test
with
| T.TypeCheckerFailure s
| T.AssertFailure s -> malformed (Lazy.force s)
- | Invalid_argument "List.nth" -> malformed "4" (* to be removed *)
let proc_fun c =
let r, s, i, u, t = c in
let malformed s =
X.error ("engine: malformed term: " ^ s)
-let not_supported () =
- X.error "engine: object not supported"
-
(* generic term processing *)
let proc_sort = function
let proc_fun ss (r, s, i, u, t) =
proc_pair s (s :: ss) u (Some t)
+let proc_constructor ss (r, s, u) =
+ proc_pair s (s :: ss) u None
+
+let proc_type ss (r, s, u, cs) =
+ proc_pair s (s :: ss) u None;
+ L.iter (proc_constructor ss) cs
+
let proc_obj u =
let ss = K.segments_of_uri u in
let _, _, _, _, obj = E.get_checked_obj G.status u in
match obj with
| C.Constant (_, s, xt, u, _) -> proc_pair s ss u xt
| C.Fixpoint (_, fs, _) -> L.iter (proc_fun ss) fs
- | C.Inductive (_, _, _, _) -> not_supported ()
+ | C.Inductive (_, _, ts, _) -> L.iter (proc_type ss) ts
(* interface functions ******************************************************)
\begin{document}
-\input{matita.lambdadelta.basic_1.pr0.defs.pr0_ind.pr0_ind.type.tex}
+\input{matita.lambdadelta.basic_1.pr0.defs.pr0.pr0_beta.type}
\bigskip
-\input{matita.lambdadelta.basic_1.pr0.defs.pr0_ind.pr0_ind.body.tex}
+\input{matita.lambdadelta.basic_1.pr0.defs.pr0.pr0_comp.type}
+
+\bigskip
+
+\input{matita.lambdadelta.basic_1.pr0.defs.pr0.pr0_delta.type}
+
+\bigskip
+
+\input{matita.lambdadelta.basic_1.pr0.defs.pr0.pr0_refl.type}
+
+\bigskip
+
+\input{matita.lambdadelta.basic_1.pr0.defs.pr0.pr0_tau.type}
+
+\bigskip
+
+\input{matita.lambdadelta.basic_1.pr0.defs.pr0.pr0.type}
+
+\bigskip
+
+\input{matita.lambdadelta.basic_1.pr0.defs.pr0.pr0_upsilon.type}
+
+\bigskip
+
+\input{matita.lambdadelta.basic_1.pr0.defs.pr0.pr0_zeta.type}
+
+\bigskip
+
+\input{matita.lambdadelta.basic_1.pr0.defs.pr0_ind.pr0_ind.type}
+
+\bigskip
+
+\input{matita.lambdadelta.basic_1.pr0.defs.pr0_ind.pr0_ind.body}
\bigskip
\input{matita.lambdadelta.basic_1.pr0.pr0.pr0_confluence.body}
+\bigskip
+
+\ObjRef{pr0}
\ObjRef{pr0_ind}
\ObjRef{pr0_confluence}
(* *)
(**************************************************************************)
-include "ground_2/relocation/trace_isid.ma".
+include "ground_2/relocation/nstream_id.ma".
include "basic_2/notation/relations/rliftstar_3.ma".
include "basic_2/grammar/term.ma".
lift_sort lift_lref_lt lift_lref_ge lift_bind lift_flat
lifts_nil lifts_cons
*)
-inductive lifts: trace → relation term ≝
-| lifts_sort: ∀k,t. lifts t (⋆k) (⋆k)
-| lifts_lref: ∀i1,i2,t. @⦃i1, t⦄ ≡ i2 → lifts t (#i1) (#i2)
-| lifts_gref: ∀p,t. lifts t (§p) (§p)
-| lifts_bind: ∀a,I,V1,V2,T1,T2,t.
- lifts t V1 V2 → lifts (Ⓣ@t) T1 T2 →
- lifts t (ⓑ{a,I}V1.T1) (ⓑ{a,I}V2.T2)
-| lifts_flat: ∀I,V1,V2,T1,T2,t.
- lifts t V1 V2 → lifts t T1 T2 →
- lifts t (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
+inductive lifts: rtmap → relation term ≝
+| lifts_sort: ∀s,f. lifts f (⋆s) (⋆s)
+| lifts_lref: ∀i1,i2,f. @⦃i1, f⦄ ≡ i2 → lifts f (#i1) (#i2)
+| lifts_gref: ∀l,f. lifts f (§l) (§l)
+| lifts_bind: ∀p,I,V1,V2,T1,T2,f.
+ lifts f V1 V2 → lifts (↑f) T1 T2 →
+ lifts f (ⓑ{p,I}V1.T1) (ⓑ{p,I}V2.T2)
+| lifts_flat: ∀I,V1,V2,T1,T2,f.
+ lifts f V1 V2 → lifts f T1 T2 →
+ lifts f (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
.
interpretation "generic relocation (term)"
(* Basic inversion lemmas ***************************************************)
-fact lifts_inv_sort1_aux: ∀X,Y,t. ⬆*[t] X ≡ Y → ∀k. X = ⋆k → Y = ⋆k.
-#X #Y #t * -X -Y -t //
-[ #i1 #i2 #t #_ #x #H destruct
-| #a #I #V1 #V2 #T1 #T2 #t #_ #_ #x #H destruct
-| #I #V1 #V2 #T1 #T2 #t #_ #_ #x #H destruct
+fact lifts_inv_sort1_aux: ∀X,Y,f. ⬆*[f] X ≡ Y → ∀s. X = ⋆s → Y = ⋆s.
+#X #Y #f * -X -Y -f //
+[ #i1 #i2 #f #_ #x #H destruct
+| #p #I #V1 #V2 #T1 #T2 #f #_ #_ #x #H destruct
+| #I #V1 #V2 #T1 #T2 #f #_ #_ #x #H destruct
]
qed-.
(* Basic_1: was: lift1_sort *)
(* Basic_2A1: includes: lift_inv_sort1 *)
-lemma lifts_inv_sort1: ∀Y,k,t. ⬆*[t] ⋆k ≡ Y → Y = ⋆k.
+lemma lifts_inv_sort1: ∀Y,s,f. ⬆*[f] ⋆s ≡ Y → Y = ⋆s.
/2 width=4 by lifts_inv_sort1_aux/ qed-.
-fact lifts_inv_lref1_aux: ∀X,Y,t. ⬆*[t] X ≡ Y → ∀i1. X = #i1 →
- ∃∃i2. @⦃i1, t⦄ ≡ i2 & Y = #i2.
-#X #Y #t * -X -Y -t
-[ #k #t #x #H destruct
-| #i1 #i2 #t #Hi12 #x #H destruct /2 width=3 by ex2_intro/
-| #p #t #x #H destruct
-| #a #I #V1 #V2 #T1 #T2 #t #_ #_ #x #H destruct
-| #I #V1 #V2 #T1 #T2 #t #_ #_ #x #H destruct
+fact lifts_inv_lref1_aux: ∀X,Y,f. ⬆*[f] X ≡ Y → ∀i1. X = #i1 →
+ ∃∃i2. @⦃i1, f⦄ ≡ i2 & Y = #i2.
+#X #Y #f * -X -Y -f
+[ #s #f #x #H destruct
+| #i1 #i2 #f #Hi12 #x #H destruct /2 width=3 by ex2_intro/
+| #l #f #x #H destruct
+| #p #I #V1 #V2 #T1 #T2 #f #_ #_ #x #H destruct
+| #I #V1 #V2 #T1 #T2 #f #_ #_ #x #H destruct
]
qed-.
(* Basic_1: was: lift1_lref *)
(* Basic_2A1: includes: lift_inv_lref1 lift_inv_lref1_lt lift_inv_lref1_ge *)
-lemma lifts_inv_lref1: ∀Y,i1,t. ⬆*[t] #i1 ≡ Y →
- ∃∃i2. @⦃i1, t⦄ ≡ i2 & Y = #i2.
+lemma lifts_inv_lref1: ∀Y,i1,f. ⬆*[f] #i1 ≡ Y →
+ ∃∃i2. @⦃i1, f⦄ ≡ i2 & Y = #i2.
/2 width=3 by lifts_inv_lref1_aux/ qed-.
-fact lifts_inv_gref1_aux: ∀X,Y,t. ⬆*[t] X ≡ Y → ∀p. X = §p → Y = §p.
-#X #Y #t * -X -Y -t //
-[ #i1 #i2 #t #_ #x #H destruct
-| #a #I #V1 #V2 #T1 #T2 #t #_ #_ #x #H destruct
-| #I #V1 #V2 #T1 #T2 #t #_ #_ #x #H destruct
+fact lifts_inv_gref1_aux: ∀X,Y,f. ⬆*[f] X ≡ Y → ∀l. X = §l → Y = §l.
+#X #Y #f * -X -Y -f //
+[ #i1 #i2 #f #_ #x #H destruct
+| #p #I #V1 #V2 #T1 #T2 #f #_ #_ #x #H destruct
+| #I #V1 #V2 #T1 #T2 #f #_ #_ #x #H destruct
]
qed-.
(* Basic_2A1: includes: lift_inv_gref1 *)
-lemma lifts_inv_gref1: ∀Y,p,t. ⬆*[t] §p ≡ Y → Y = §p.
+lemma lifts_inv_gref1: ∀Y,l,f. ⬆*[f] §l ≡ Y → Y = §l.
/2 width=4 by lifts_inv_gref1_aux/ qed-.
-fact lifts_inv_bind1_aux: ∀X,Y,t. ⬆*[t] X ≡ Y →
- ∀a,I,V1,T1. X = ⓑ{a,I}V1.T1 →
- ∃∃V2,T2. ⬆*[t] V1 ≡ V2 & ⬆*[Ⓣ@t] T1 ≡ T2 &
- Y = ⓑ{a,I}V2.T2.
-#X #Y #t * -X -Y -t
-[ #k #t #b #J #W1 #U1 #H destruct
-| #i1 #i2 #t #_ #b #J #W1 #U1 #H destruct
-| #p #t #b #J #W1 #U1 #H destruct
-| #a #I #V1 #V2 #T1 #T2 #t #HV12 #HT12 #b #J #W1 #U1 #H destruct /2 width=5 by ex3_2_intro/
-| #I #V1 #V2 #T1 #T2 #t #_ #_ #b #J #W1 #U1 #H destruct
+fact lifts_inv_bind1_aux: ∀X,Y,f. ⬆*[f] X ≡ Y →
+ ∀p,I,V1,T1. X = ⓑ{p,I}V1.T1 →
+ ∃∃V2,T2. ⬆*[f] V1 ≡ V2 & ⬆*[↑f] T1 ≡ T2 &
+ Y = ⓑ{p,I}V2.T2.
+#X #Y #f * -X -Y -f
+[ #s #f #q #J #W1 #U1 #H destruct
+| #i1 #i2 #f #_ #q #J #W1 #U1 #H destruct
+| #l #f #b #J #W1 #U1 #H destruct
+| #p #I #V1 #V2 #T1 #T2 #f #HV12 #HT12 #q #J #W1 #U1 #H destruct /2 width=5 by ex3_2_intro/
+| #I #V1 #V2 #T1 #T2 #f #_ #_ #q #J #W1 #U1 #H destruct
]
qed-.
(* Basic_1: was: lift1_bind *)
(* Basic_2A1: includes: lift_inv_bind1 *)
-lemma lifts_inv_bind1: ∀a,I,V1,T1,Y,t. ⬆*[t] ⓑ{a,I}V1.T1 ≡ Y →
- ∃∃V2,T2. ⬆*[t] V1 ≡ V2 & ⬆*[Ⓣ@t] T1 ≡ T2 &
- Y = ⓑ{a,I}V2.T2.
+lemma lifts_inv_bind1: ∀p,I,V1,T1,Y,f. ⬆*[f] ⓑ{p,I}V1.T1 ≡ Y →
+ ∃∃V2,T2. ⬆*[f] V1 ≡ V2 & ⬆*[↑f] T1 ≡ T2 &
+ Y = ⓑ{p,I}V2.T2.
/2 width=3 by lifts_inv_bind1_aux/ qed-.
-fact lifts_inv_flat1_aux: ∀X,Y,t. ⬆*[t] X ≡ Y →
+fact lifts_inv_flat1_aux: ∀X,Y,f. ⬆*[f] X ≡ Y →
∀I,V1,T1. X = ⓕ{I}V1.T1 →
- ∃∃V2,T2. ⬆*[t] V1 ≡ V2 & ⬆*[t] T1 ≡ T2 &
+ ∃∃V2,T2. ⬆*[f] V1 ≡ V2 & ⬆*[f] T1 ≡ T2 &
Y = ⓕ{I}V2.T2.
-#X #Y #t * -X -Y -t
-[ #k #t #J #W1 #U1 #H destruct
-| #i1 #i2 #t #_ #J #W1 #U1 #H destruct
-| #p #t #J #W1 #U1 #H destruct
-| #a #I #V1 #V2 #T1 #T2 #t #_ #_ #J #W1 #U1 #H destruct
-| #I #V1 #V2 #T1 #T2 #t #HV12 #HT12 #J #W1 #U1 #H destruct /2 width=5 by ex3_2_intro/
+#X #Y #f * -X -Y -f
+[ #s #f #J #W1 #U1 #H destruct
+| #i1 #i2 #f #_ #J #W1 #U1 #H destruct
+| #l #f #J #W1 #U1 #H destruct
+| #p #I #V1 #V2 #T1 #T2 #f #_ #_ #J #W1 #U1 #H destruct
+| #I #V1 #V2 #T1 #T2 #f #HV12 #HT12 #J #W1 #U1 #H destruct /2 width=5 by ex3_2_intro/
]
qed-.
(* Basic_1: was: lift1_flat *)
(* Basic_2A1: includes: lift_inv_flat1 *)
-lemma lifts_inv_flat1: ∀I,V1,T1,Y,t. ⬆*[t] ⓕ{I}V1.T1 ≡ Y →
- ∃∃V2,T2. ⬆*[t] V1 ≡ V2 & ⬆*[t] T1 ≡ T2 &
+lemma lifts_inv_flat1: ∀I,V1,T1,Y,f. ⬆*[f] ⓕ{I}V1.T1 ≡ Y →
+ ∃∃V2,T2. ⬆*[f] V1 ≡ V2 & ⬆*[f] T1 ≡ T2 &
Y = ⓕ{I}V2.T2.
/2 width=3 by lifts_inv_flat1_aux/ qed-.
-fact lifts_inv_sort2_aux: ∀X,Y,t. ⬆*[t] X ≡ Y → ∀k. Y = ⋆k → X = ⋆k.
-#X #Y #t * -X -Y -t //
-[ #i1 #i2 #t #_ #x #H destruct
-| #a #I #V1 #V2 #T1 #T2 #t #_ #_ #x #H destruct
-| #I #V1 #V2 #T1 #T2 #t #_ #_ #x #H destruct
+fact lifts_inv_sort2_aux: ∀X,Y,f. ⬆*[f] X ≡ Y → ∀s. Y = ⋆s → X = ⋆s.
+#X #Y #f * -X -Y -f //
+[ #i1 #i2 #f #_ #x #H destruct
+| #p #I #V1 #V2 #T1 #T2 #f #_ #_ #x #H destruct
+| #I #V1 #V2 #T1 #T2 #f #_ #_ #x #H destruct
]
qed-.
(* Basic_1: includes: lift_gen_sort *)
(* Basic_2A1: includes: lift_inv_sort2 *)
-lemma lifts_inv_sort2: ∀X,k,t. ⬆*[t] X ≡ ⋆k → X = ⋆k.
+lemma lifts_inv_sort2: ∀X,s,f. ⬆*[f] X ≡ ⋆s → X = ⋆s.
/2 width=4 by lifts_inv_sort2_aux/ qed-.
-fact lifts_inv_lref2_aux: ∀X,Y,t. ⬆*[t] X ≡ Y → ∀i2. Y = #i2 →
- ∃∃i1. @⦃i1, t⦄ ≡ i2 & X = #i1.
-#X #Y #t * -X -Y -t
-[ #k #t #x #H destruct
-| #i1 #i2 #t #Hi12 #x #H destruct /2 width=3 by ex2_intro/
-| #p #t #x #H destruct
-| #a #I #V1 #V2 #T1 #T2 #t #_ #_ #x #H destruct
-| #I #V1 #V2 #T1 #T2 #t #_ #_ #x #H destruct
+fact lifts_inv_lref2_aux: ∀X,Y,f. ⬆*[f] X ≡ Y → ∀i2. Y = #i2 →
+ ∃∃i1. @⦃i1, f⦄ ≡ i2 & X = #i1.
+#X #Y #f * -X -Y -f
+[ #s #f #x #H destruct
+| #i1 #i2 #f #Hi12 #x #H destruct /2 width=3 by ex2_intro/
+| #l #f #x #H destruct
+| #p #I #V1 #V2 #T1 #T2 #f #_ #_ #x #H destruct
+| #I #V1 #V2 #T1 #T2 #f #_ #_ #x #H destruct
]
qed-.
(* Basic_1: includes: lift_gen_lref lift_gen_lref_lt lift_gen_lref_false lift_gen_lref_ge *)
(* Basic_2A1: includes: lift_inv_lref2 lift_inv_lref2_lt lift_inv_lref2_be lift_inv_lref2_ge lift_inv_lref2_plus *)
-lemma lifts_inv_lref2: ∀X,i2,t. ⬆*[t] X ≡ #i2 →
- ∃∃i1. @⦃i1, t⦄ ≡ i2 & X = #i1.
+lemma lifts_inv_lref2: ∀X,i2,f. ⬆*[f] X ≡ #i2 →
+ ∃∃i1. @⦃i1, f⦄ ≡ i2 & X = #i1.
/2 width=3 by lifts_inv_lref2_aux/ qed-.
-fact lifts_inv_gref2_aux: ∀X,Y,t. ⬆*[t] X ≡ Y → ∀p. Y = §p → X = §p.
-#X #Y #t * -X -Y -t //
-[ #i1 #i2 #t #_ #x #H destruct
-| #a #I #V1 #V2 #T1 #T2 #t #_ #_ #x #H destruct
-| #I #V1 #V2 #T1 #T2 #t #_ #_ #x #H destruct
+fact lifts_inv_gref2_aux: ∀X,Y,f. ⬆*[f] X ≡ Y → ∀l. Y = §l → X = §l.
+#X #Y #f * -X -Y -f //
+[ #i1 #i2 #f #_ #x #H destruct
+| #p #I #V1 #V2 #T1 #T2 #f #_ #_ #x #H destruct
+| #I #V1 #V2 #T1 #T2 #f #_ #_ #x #H destruct
]
qed-.
(* Basic_2A1: includes: lift_inv_gref1 *)
-lemma lifts_inv_gref2: ∀X,p,t. ⬆*[t] X ≡ §p → X = §p.
+lemma lifts_inv_gref2: ∀X,l,f. ⬆*[f] X ≡ §l → X = §l.
/2 width=4 by lifts_inv_gref2_aux/ qed-.
-fact lifts_inv_bind2_aux: ∀X,Y,t. ⬆*[t] X ≡ Y →
- ∀a,I,V2,T2. Y = ⓑ{a,I}V2.T2 →
- ∃∃V1,T1. ⬆*[t] V1 ≡ V2 & ⬆*[Ⓣ@t] T1 ≡ T2 &
- X = ⓑ{a,I}V1.T1.
-#X #Y #t * -X -Y -t
-[ #k #t #b #J #W2 #U2 #H destruct
-| #i1 #i2 #t #_ #b #J #W2 #U2 #H destruct
-| #p #t #b #J #W2 #U2 #H destruct
-| #a #I #V1 #V2 #T1 #T2 #t #HV12 #HT12 #b #J #W2 #U2 #H destruct /2 width=5 by ex3_2_intro/
-| #I #V1 #V2 #T1 #T2 #t #_ #_ #b #J #W2 #U2 #H destruct
+fact lifts_inv_bind2_aux: ∀X,Y,f. ⬆*[f] X ≡ Y →
+ ∀p,I,V2,T2. Y = ⓑ{p,I}V2.T2 →
+ ∃∃V1,T1. ⬆*[f] V1 ≡ V2 & ⬆*[↑f] T1 ≡ T2 &
+ X = ⓑ{p,I}V1.T1.
+#X #Y #f * -X -Y -f
+[ #s #f #q #J #W2 #U2 #H destruct
+| #i1 #i2 #f #_ #q #J #W2 #U2 #H destruct
+| #l #f #q #J #W2 #U2 #H destruct
+| #p #I #V1 #V2 #T1 #T2 #f #HV12 #HT12 #q #J #W2 #U2 #H destruct /2 width=5 by ex3_2_intro/
+| #I #V1 #V2 #T1 #T2 #f #_ #_ #q #J #W2 #U2 #H destruct
]
qed-.
(* Basic_1: includes: lift_gen_bind *)
(* Basic_2A1: includes: lift_inv_bind2 *)
-lemma lifts_inv_bind2: ∀a,I,V2,T2,X,t. ⬆*[t] X ≡ ⓑ{a,I}V2.T2 →
- ∃∃V1,T1. ⬆*[t] V1 ≡ V2 & ⬆*[Ⓣ@t] T1 ≡ T2 &
- X = ⓑ{a,I}V1.T1.
+lemma lifts_inv_bind2: ∀p,I,V2,T2,X,f. ⬆*[f] X ≡ ⓑ{p,I}V2.T2 →
+ ∃∃V1,T1. ⬆*[f] V1 ≡ V2 & ⬆*[↑f] T1 ≡ T2 &
+ X = ⓑ{p,I}V1.T1.
/2 width=3 by lifts_inv_bind2_aux/ qed-.
-fact lifts_inv_flat2_aux: ∀X,Y,t. ⬆*[t] X ≡ Y →
+fact lifts_inv_flat2_aux: ∀X,Y,f. ⬆*[f] X ≡ Y →
∀I,V2,T2. Y = ⓕ{I}V2.T2 →
- ∃∃V1,T1. ⬆*[t] V1 ≡ V2 & ⬆*[t] T1 ≡ T2 &
+ ∃∃V1,T1. ⬆*[f] V1 ≡ V2 & ⬆*[f] T1 ≡ T2 &
X = ⓕ{I}V1.T1.
-#X #Y #t * -X -Y -t
-[ #k #t #J #W2 #U2 #H destruct
-| #i1 #i2 #t #_ #J #W2 #U2 #H destruct
-| #p #t #J #W2 #U2 #H destruct
-| #a #I #V1 #V2 #T1 #T2 #t #_ #_ #J #W2 #U2 #H destruct
-| #I #V1 #V2 #T1 #T2 #t #HV12 #HT12 #J #W2 #U2 #H destruct /2 width=5 by ex3_2_intro/
+#X #Y #f * -X -Y -f
+[ #s #f #J #W2 #U2 #H destruct
+| #i1 #i2 #f #_ #J #W2 #U2 #H destruct
+| #l #f #J #W2 #U2 #H destruct
+| #p #I #V1 #V2 #T1 #T2 #f #_ #_ #J #W2 #U2 #H destruct
+| #I #V1 #V2 #T1 #T2 #f #HV12 #HT12 #J #W2 #U2 #H destruct /2 width=5 by ex3_2_intro/
]
qed-.
(* Basic_1: includes: lift_gen_flat *)
(* Basic_2A1: includes: lift_inv_flat2 *)
-lemma lifts_inv_flat2: ∀I,V2,T2,X,t. ⬆*[t] X ≡ ⓕ{I}V2.T2 →
- ∃∃V1,T1. ⬆*[t] V1 ≡ V2 & ⬆*[t] T1 ≡ T2 &
+lemma lifts_inv_flat2: ∀I,V2,T2,X,f. ⬆*[f] X ≡ ⓕ{I}V2.T2 →
+ ∃∃V1,T1. ⬆*[f] V1 ≡ V2 & ⬆*[f] T1 ≡ T2 &
X = ⓕ{I}V1.T1.
/2 width=3 by lifts_inv_flat2_aux/ qed-.
(* Basic_2A1: includes: lift_inv_pair_xy_x *)
-lemma lifts_inv_pair_xy_x: ∀I,V,T,t. ⬆*[t] ②{I}V.T ≡ V → ⊥.
+lemma lifts_inv_pair_xy_x: ∀I,V,T,f. ⬆*[f] ②{I}V.T ≡ V → ⊥.
#J #V elim V -V
-[ * #i #U #t #H
+[ * #i #U #f #H
[ lapply (lifts_inv_sort2 … H) -H #H destruct
| elim (lifts_inv_lref2 … H) -H
#x #_ #H destruct
| lapply (lifts_inv_gref2 … H) -H #H destruct
]
-| * [ #a ] #I #V2 #T2 #IHV2 #_ #U #t #H
+| * [ #p ] #I #V2 #T2 #IHV2 #_ #U #f #H
[ elim (lifts_inv_bind2 … H) -H #V1 #T1 #HV12 #_ #H destruct /2 width=3 by/
| elim (lifts_inv_flat2 … H) -H #V1 #T1 #HV12 #_ #H destruct /2 width=3 by/
]
(* Basic_1: includes: thead_x_lift_y_y *)
(* Basic_2A1: includes: lift_inv_pair_xy_y *)
-lemma lifts_inv_pair_xy_y: ∀I,T,V,t. ⬆*[t] ②{I}V.T ≡ T → ⊥.
+lemma lifts_inv_pair_xy_y: ∀I,T,V,f. ⬆*[f] ②{I}V.T ≡ T → ⊥.
#J #T elim T -T
-[ * #i #W #t #H
+[ * #i #W #f #H
[ lapply (lifts_inv_sort2 … H) -H #H destruct
| elim (lifts_inv_lref2 … H) -H
#x #_ #H destruct
| lapply (lifts_inv_gref2 … H) -H #H destruct
]
-| * [ #a ] #I #V2 #T2 #_ #IHT2 #W #t #H
+| * [ #p ] #I #V2 #T2 #_ #IHT2 #W #f #H
[ elim (lifts_inv_bind2 … H) -H #V1 #T1 #_ #HT12 #H destruct /2 width=4 by/
| elim (lifts_inv_flat2 … H) -H #V1 #T1 #_ #HT12 #H destruct /2 width=4 by/
]
(* Basic forward lemmas *****************************************************)
(* Basic_2A1: includes: lift_inv_O2 *)
-lemma lifts_fwd_isid: ∀T1,T2,t. ⬆*[t] T1 ≡ T2 → 𝐈⦃t⦄ → T1 = T2.
-#T1 #T2 #t #H elim H -T1 -T2 -t /4 width=3 by isid_inv_at, eq_f2, eq_f/
+lemma lifts_fwd_isid: ∀T1,T2,f. ⬆*[f] T1 ≡ T2 → 𝐈⦃f⦄ → T1 = T2.
+#T1 #T2 #f #H elim H -T1 -T2 -f
+/4 width=3 by isid_inv_at_mono, isid_push, eq_f2, eq_f/
qed-.
(* Basic_2A1: includes: lift_fwd_pair1 *)
-lemma lifts_fwd_pair1: ∀I,V1,T1,Y,t. ⬆*[t] ②{I}V1.T1 ≡ Y →
- ∃∃V2,T2. ⬆*[t] V1 ≡ V2 & Y = ②{I}V2.T2.
-* [ #a ] #I #V1 #T1 #Y #t #H
+lemma lifts_fwd_pair1: ∀I,V1,T1,Y,f. ⬆*[f] ②{I}V1.T1 ≡ Y →
+ ∃∃V2,T2. ⬆*[f] V1 ≡ V2 & Y = ②{I}V2.T2.
+* [ #p ] #I #V1 #T1 #Y #f #H
[ elim (lifts_inv_bind1 … H) -H /2 width=4 by ex2_2_intro/
| elim (lifts_inv_flat1 … H) -H /2 width=4 by ex2_2_intro/
]
qed-.
(* Basic_2A1: includes: lift_fwd_pair2 *)
-lemma lifts_fwd_pair2: ∀I,V2,T2,X,t. ⬆*[t] X ≡ ②{I}V2.T2 →
- ∃∃V1,T1. ⬆*[t] V1 ≡ V2 & X = ②{I}V1.T1.
-* [ #a ] #I #V2 #T2 #X #t #H
+lemma lifts_fwd_pair2: ∀I,V2,T2,X,f. ⬆*[f] X ≡ ②{I}V2.T2 →
+ ∃∃V1,T1. ⬆*[f] V1 ≡ V2 & X = ②{I}V1.T1.
+* [ #p ] #I #V2 #T2 #X #f #H
[ elim (lifts_inv_bind2 … H) -H /2 width=4 by ex2_2_intro/
| elim (lifts_inv_flat2 … H) -H /2 width=4 by ex2_2_intro/
]
(* Basic properties *********************************************************)
+lemma lifts_eq_repl_back: ∀T1,T2. eq_stream_repl_back … (λf. ⬆*[f] T1 ≡ T2).
+#T1 #T2 #f1 #H elim H -T1 -T2 -f1
+/4 width=3 by lifts_flat, lifts_bind, lifts_lref, at_eq_repl_back, push_eq_repl/
+qed-.
+
+lemma lifts_eq_repl_fwd: ∀T1,T2. eq_stream_repl_fwd … (λf. ⬆*[f] T1 ≡ T2).
+#T1 #T2 @eq_stream_repl_sym /2 width=3 by lifts_eq_repl_back/ (**) (* full auto fails *)
+qed-.
+
+(* Basic_1: includes: lift_r *)
+(* Basic_2A1: includes: lift_refl *)
+lemma lifts_refl: ∀T,f. 𝐈⦃f⦄ → ⬆*[f] T ≡ T.
+#T elim T -T *
+/4 width=1 by lifts_flat, lifts_bind, lifts_lref, isid_inv_at, isid_push/
+qed.
+
+(* Basic_2A1: includes: lift_total *)
+lemma lifts_total: ∀T1,f. ∃T2. ⬆*[f] T1 ≡ T2.
+#T1 elim T1 -T1 *
+/3 width=2 by lifts_lref, lifts_sort, lifts_gref, ex_intro/
+[ #p ] #I #V1 #T1 #IHV1 #IHT1 #f
+elim (IHV1 f) -IHV1 #V2 #HV12
+[ elim (IHT1 (↑f)) -IHT1 /3 width=2 by lifts_bind, ex_intro/
+| elim (IHT1 f) -IHT1 /3 width=2 by lifts_flat, ex_intro/
+]
+qed-.
+
(* Basic_1: includes: lift_free (right to left) *)
(* Basic_2A1: includes: lift_split *)
-lemma lifts_split_trans: ∀T1,T2,t. ⬆*[t] T1 ≡ T2 →
- ∀t1,t2. t2 ⊚ t1 ≡ t →
- ∃∃T. ⬆*[t1] T1 ≡ T & ⬆*[t2] T ≡ T2.
-#T1 #T2 #t #H elim H -T1 -T2 -t
+lemma lifts_split_trans: ∀T1,T2,f. ⬆*[f] T1 ≡ T2 →
+ ∀f1,f2. f2 ⊚ f1 ≡ f →
+ ∃∃T. ⬆*[f1] T1 ≡ T & ⬆*[f2] T ≡ T2.
+#T1 #T2 #f #H elim H -T1 -T2 -f
[ /3 width=3 by lifts_sort, ex2_intro/
-| #i1 #i2 #t #Hi #t1 #t2 #Ht elim (after_at_fwd … Ht … Hi) -Ht -Hi
+| #i1 #i2 #f #Hi #f1 #f2 #Ht elim (after_at_fwd … Hi … Ht) -Hi -Ht
/3 width=3 by lifts_lref, ex2_intro/
| /3 width=3 by lifts_gref, ex2_intro/
-| #a #I #V1 #V2 #T1 #T2 #t #_ #_ #IHV #IHT #t1 #t2 #Ht
- elim (IHV â\80¦ Ht) elim (IHT (â\93\89@t1) (â\93\89@t2)) -IHV -IHT
- /3 width=5 by lifts_bind, after_true, ex2_intro/
-| #I #V1 #V2 #T1 #T2 #t #_ #_ #IHV #IHT #t1 #t2 #Ht
+| #p #I #V1 #V2 #T1 #T2 #f #_ #_ #IHV #IHT #f1 #f2 #Ht
+ elim (IHV â\80¦ Ht) elim (IHT (â\86\91f1) (â\86\91f2)) -IHV -IHT
+ /3 width=5 by lifts_bind, after_O2, ex2_intro/
+| #I #V1 #V2 #T1 #T2 #f #_ #_ #IHV #IHT #f1 #f2 #Ht
elim (IHV … Ht) elim (IHT … Ht) -IHV -IHT -Ht
/3 width=5 by lifts_flat, ex2_intro/
]
qed-.
(* Note: apparently, this was missing in Basic_2A1 *)
-lemma lifts_split_div: ∀T1,T2,t1. ⬆*[t1] T1 ≡ T2 →
- ∀t2,t. t2 ⊚ t1 ≡ t →
- ∃∃T. ⬆*[t2] T2 ≡ T & ⬆*[t] T1 ≡ T.
-#T1 #T2 #t1 #H elim H -T1 -T2 -t1
+lemma lifts_split_div: ∀T1,T2,f1. ⬆*[f1] T1 ≡ T2 →
+ ∀f2,f. f2 ⊚ f1 ≡ f →
+ ∃∃T. ⬆*[f2] T2 ≡ T & ⬆*[f] T1 ≡ T.
+#T1 #T2 #f1 #H elim H -T1 -T2 -f1
[ /3 width=3 by lifts_sort, ex2_intro/
-| #i1 #i2 #t1 #Hi #t2 #t #Ht elim (after_at1_fwd … Ht … Hi) -Ht -Hi
+| #i1 #i2 #f1 #Hi #f2 #f #Ht elim (after_at1_fwd … Hi … Ht) -Hi -Ht
/3 width=3 by lifts_lref, ex2_intro/
| /3 width=3 by lifts_gref, ex2_intro/
-| #a #I #V1 #V2 #T1 #T2 #t1 #_ #_ #IHV #IHT #t2 #t #Ht
- elim (IHV â\80¦ Ht) elim (IHT (â\93\89@t2) (â\93\89@t)) -IHV -IHT
- /3 width=5 by lifts_bind, after_true, ex2_intro/
-| #I #V1 #V2 #T1 #T2 #t1 #_ #_ #IHV #IHT #t2 #t #Ht
+| #p #I #V1 #V2 #T1 #T2 #f1 #_ #_ #IHV #IHT #f2 #f #Ht
+ elim (IHV â\80¦ Ht) elim (IHT (â\86\91f2) (â\86\91f)) -IHV -IHT
+ /3 width=5 by lifts_bind, after_O2, ex2_intro/
+| #I #V1 #V2 #T1 #T2 #f1 #_ #_ #IHV #IHT #f2 #f #Ht
elim (IHV … Ht) elim (IHT … Ht) -IHV -IHT -Ht
/3 width=5 by lifts_flat, ex2_intro/
]
(* Basic_1: includes: dnf_dec2 dnf_dec *)
(* Basic_2A1: includes: is_lift_dec *)
-lemma is_lifts_dec: ∀T2,t. Decidable (∃T1. ⬆*[t] T1 ≡ T2).
+lemma is_lifts_dec: ∀T2,f. Decidable (∃T1. ⬆*[f] T1 ≡ T2).
#T1 elim T1 -T1
[ * [1,3: /3 width=2 by lifts_sort, lifts_gref, ex_intro, or_introl/ ]
- #i2 #t elim (is_at_dec t i2)
+ #i2 #f elim (is_at_dec f i2)
[ * /4 width=3 by lifts_lref, ex_intro, or_introl/
| #H @or_intror *
#X #HX elim (lifts_inv_lref2 … HX) -HX
/3 width=2 by ex_intro/
]
-| * [ #a ] #I #V2 #T2 #IHV2 #IHT2 #t
- [ elim (IHV2 t) -IHV2
- [ * #V1 #HV12 elim (IHT2 (â\93\89@t)) -IHT2
+| * [ #p ] #I #V2 #T2 #IHV2 #IHT2 #f
+ [ elim (IHV2 f) -IHV2
+ [ * #V1 #HV12 elim (IHT2 (â\86\91f)) -IHT2
[ * #T1 #HT12 @or_introl /3 width=2 by lifts_bind, ex_intro/
| -V1 #HT2 @or_intror * #X #H
elim (lifts_inv_bind2 … H) -H /3 width=2 by ex_intro/
| -IHT2 #HV2 @or_intror * #X #H
elim (lifts_inv_bind2 … H) -H /3 width=2 by ex_intro/
]
- | elim (IHV2 t) -IHV2
- [ * #V1 #HV12 elim (IHT2 t) -IHT2
+ | elim (IHV2 f) -IHV2
+ [ * #V1 #HV12 elim (IHT2 f) -IHT2
[ * #T1 #HT12 /4 width=2 by lifts_flat, ex_intro, or_introl/
| -V1 #HT2 @or_intror * #X #H
elim (lifts_inv_flat2 … H) -H /3 width=2 by ex_intro/
(* Main properties **********************************************************)
-(* Basic_2A1: includes: lift_inj *)
-theorem lifts_inj: ∀t,T1,U. ⬆*[t] T1 ≡ U → ∀T2. ⬆*[t] T2 ≡ U → T1 = T2.
-#t #T1 #U #H elim H -t -T1 -U
-[ /2 width=2 by lifts_inv_sort2/
-| #i1 #j #t #Hi1j #X #HX elim (lifts_inv_lref2 … HX) -HX
- /4 width=4 by at_inj, eq_f/
-| /2 width=2 by lifts_inv_gref2/
-| #a #I #V1 #V2 #T1 #T2 #t #_ #_ #IHV12 #IHT12 #X #HX elim (lifts_inv_bind2 … HX) -HX
- #V #T #HV1 #HT1 #HX destruct /3 width=1 by eq_f2/
-| #I #V1 #V2 #T1 #T2 #t #_ #_ #IHV12 #IHT12 #X #HX elim (lifts_inv_flat2 … HX) -HX
- #V #T #HV1 #HT1 #HX destruct /3 width=1 by eq_f2/
-]
-qed-.
-
(* Basic_1: includes: lift_gen_lift *)
(* Basic_2A1: includes: lift_div_le lift_div_be *)
-theorem lifts_div: ∀T,T2,t2. ⬆*[t2] T2 ≡ T → ∀T1,t. ⬆*[t] T1 ≡ T →
- ∀t1. t2 ⊚ t1 ≡ t → ⬆*[t1] T1 ≡ T2.
-#T #T2 #t2 #H elim H -T -T2 -t2
-[ #k #t2 #T1 #t #H >(lifts_inv_sort2 … H) -T1 //
-| #i2 #i #t2 #Hi2 #T1 #t #H #t1 #Ht21 elim (lifts_inv_lref2 … H) -H
+theorem lifts_div: ∀T,T2,f2. ⬆*[f2] T2 ≡ T → ∀T1,f. ⬆*[f] T1 ≡ T →
+ ∀f1. f2 ⊚ f1 ≡ f → ⬆*[f1] T1 ≡ T2.
+#T #T2 #f2 #H elim H -T -T2 -f2
+[ #s #f2 #T1 #f #H >(lifts_inv_sort2 … H) -T1 //
+| #i2 #i #f2 #Hi2 #T1 #f #H #f1 #Ht21 elim (lifts_inv_lref2 … H) -H
#i1 #Hi1 #H destruct /3 width=6 by lifts_lref, after_fwd_at1/
-| #p #t2 #T1 #t #H >(lifts_inv_gref2 … H) -T1 //
-| #a #I #W2 #W #U2 #U #t2 #_ #_ #IHW #IHU #T1 #t #H
+| #l #f2 #T1 #f #H >(lifts_inv_gref2 … H) -T1 //
+| #p #I #W2 #W #U2 #U #f2 #_ #_ #IHW #IHU #T1 #f #H
elim (lifts_inv_bind2 … H) -H #W1 #U1 #HW1 #HU1 #H destruct
- /4 width=3 by lifts_bind, after_true/
-| #I #W2 #W #U2 #U #t2 #_ #_ #IHW #IHU #T1 #t #H
+ /4 width=3 by lifts_bind, after_O2/
+| #I #W2 #W #U2 #U #f2 #_ #_ #IHW #IHU #T1 #f #H
elim (lifts_inv_flat2 … H) -H #W1 #U1 #HW1 #HU1 #H destruct
/3 width=3 by lifts_flat/
]
qed-.
-(* Basic_2A1: includes: lift_mono *)
-theorem lifts_mono: ∀t,T,U1. ⬆*[t] T ≡ U1 → ∀U2. ⬆*[t] T ≡ U2 → U1 = U2.
-#t #T #U1 #H elim H -t -T -U1
-[ /2 width=2 by lifts_inv_sort1/
-| #i1 #j #t #Hi1j #X #HX elim (lifts_inv_lref1 … HX) -HX
- /4 width=4 by at_mono, eq_f/
-| /2 width=2 by lifts_inv_gref1/
-| #a #I #V1 #V2 #T1 #T2 #t #_ #_ #IHV12 #IHT12 #X #HX elim (lifts_inv_bind1 … HX) -HX
- #V #T #HV1 #HT1 #HX destruct /3 width=1 by eq_f2/
-| #I #V1 #V2 #T1 #T2 #t #_ #_ #IHV12 #IHT12 #X #HX elim (lifts_inv_flat1 … HX) -HX
- #V #T #HV1 #HT1 #HX destruct /3 width=1 by eq_f2/
-]
-qed-.
-
(* Basic_1: was: lift1_lift1 (left to right) *)
(* Basic_1: includes: lift_free (left to right) lift_d lift1_xhg (right to left) lift1_free (right to left) *)
(* Basic_2A1: includes: lift_trans_be lift_trans_le lift_trans_ge lifts_lift_trans_le lifts_lift_trans *)
-theorem lifts_trans: ∀T1,T,t1. ⬆*[t1] T1 ≡ T → ∀T2,t2. ⬆*[t2] T ≡ T2 →
- ∀t. t2 ⊚ t1 ≡ t → ⬆*[t] T1 ≡ T2.
-#T1 #T #t1 #H elim H -T1 -T -t1
-[ #k #t1 #T2 #t2 #H >(lifts_inv_sort1 … H) -T2 //
-| #i1 #i #t1 #Hi1 #T2 #t2 #H #t #Ht21 elim (lifts_inv_lref1 … H) -H
+theorem lifts_trans: ∀T1,T,f1. ⬆*[f1] T1 ≡ T → ∀T2,f2. ⬆*[f2] T ≡ T2 →
+ ∀f. f2 ⊚ f1 ≡ f → ⬆*[f] T1 ≡ T2.
+#T1 #T #f1 #H elim H -T1 -T -f1
+[ #s #f1 #T2 #f2 #H >(lifts_inv_sort1 … H) -T2 //
+| #i1 #i #f1 #Hi1 #T2 #f2 #H #f #Ht21 elim (lifts_inv_lref1 … H) -H
#i2 #Hi2 #H destruct /3 width=6 by lifts_lref, after_fwd_at/
-| #p #t1 #T2 #t2 #H >(lifts_inv_gref1 … H) -T2 //
-| #a #I #W1 #W #U1 #U #t1 #_ #_ #IHW #IHU #T2 #t2 #H
+| #l #f1 #T2 #f2 #H >(lifts_inv_gref1 … H) -T2 //
+| #p #I #W1 #W #U1 #U #f1 #_ #_ #IHW #IHU #T2 #f2 #H
elim (lifts_inv_bind1 … H) -H #W2 #U2 #HW2 #HU2 #H destruct
- /4 width=3 by lifts_bind, after_true/
-| #I #W1 #W #U1 #U #t1 #_ #_ #IHW #IHU #T2 #t2 #H
+ /4 width=3 by lifts_bind, after_O2/
+| #I #W1 #W #U1 #U #f1 #_ #_ #IHW #IHU #T2 #f2 #H
elim (lifts_inv_flat1 … H) -H #W2 #U2 #HW2 #HU2 #H destruct
/3 width=3 by lifts_flat/
]
qed-.
(* Basic_2A1: includes: lift_conf_O1 lift_conf_be *)
-theorem lifts_conf: ∀T,T1,t1. ⬆*[t1] T ≡ T1 → ∀T2,t. ⬆*[t] T ≡ T2 →
- ∀t2. t2 ⊚ t1 ≡ t → ⬆*[t2] T1 ≡ T2.
-#T #T1 #t1 #H elim H -T -T1 -t1
-[ #k #t1 #T2 #t #H >(lifts_inv_sort1 … H) -T2 //
-| #i #i1 #t1 #Hi1 #T2 #t #H #t2 #Ht21 elim (lifts_inv_lref1 … H) -H
+theorem lifts_conf: ∀T,T1,f1. ⬆*[f1] T ≡ T1 → ∀T2,f. ⬆*[f] T ≡ T2 →
+ ∀f2. f2 ⊚ f1 ≡ f → ⬆*[f2] T1 ≡ T2.
+#T #T1 #f1 #H elim H -T -T1 -f1
+[ #s #f1 #T2 #f #H >(lifts_inv_sort1 … H) -T2 //
+| #i #i1 #f1 #Hi1 #T2 #f #H #f2 #Ht21 elim (lifts_inv_lref1 … H) -H
#i2 #Hi2 #H destruct /3 width=6 by lifts_lref, after_fwd_at2/
-| #p #t1 #T2 #t #H >(lifts_inv_gref1 … H) -T2 //
-| #a #I #W #W1 #U #U1 #t1 #_ #_ #IHW #IHU #T2 #t #H
+| #l #f1 #T2 #f #H >(lifts_inv_gref1 … H) -T2 //
+| #p #I #W #W1 #U #U1 #f1 #_ #_ #IHW #IHU #T2 #f #H
elim (lifts_inv_bind1 … H) -H #W2 #U2 #HW2 #HU2 #H destruct
- /4 width=3 by lifts_bind, after_true/
-| #I #W #W1 #U #U1 #t1 #_ #_ #IHW #IHU #T2 #t #H
+ /4 width=3 by lifts_bind, after_O2/
+| #I #W #W1 #U #U1 #f1 #_ #_ #IHW #IHU #T2 #f #H
elim (lifts_inv_flat1 … H) -H #W2 #U2 #HW2 #HU2 #H destruct
/3 width=3 by lifts_flat/
]
qed-.
+
+(* Advanced proprerties *****************************************************)
+
+(* Basic_2A1: includes: lift_inj *)
+lemma lifts_inj: ∀T1,U,f. ⬆*[f] T1 ≡ U → ∀T2. ⬆*[f] T2 ≡ U → T1 = T2.
+#T1 #U #f #H1 #T2 #H2 lapply (isid_after_dx 𝐈𝐝 f ?)
+/3 width=6 by lifts_div, lifts_fwd_isid/
+qed-.
+
+(* Basic_2A1: includes: lift_mono *)
+lemma lifts_mono: ∀T,U1,f. ⬆*[f] T ≡ U1 → ∀U2. ⬆*[f] T ≡ U2 → U1 = U2.
+#T #U1 #f #H1 #U2 #H2 lapply (isid_after_sn 𝐈𝐝 f ?)
+/3 width=6 by lifts_conf, lifts_fwd_isid/
+qed-.
(* Main properties **********************************************************)
(* Basic_1: includes: lifts_inj *)
-theorem liftsv_inj: ∀T1s,Us,t. ⬆*[t] T1s ≡ Us →
- ∀T2s. ⬆*[t] T2s ≡ Us → T1s = T2s.
-#T1s #Us #t #H elim H -T1s -Us
-[ #T2s #H >(liftsv_inv_nil2 … H) -H //
-| #T1s #Us #T1 #U #HT1U #_ #IHT1Us #X #H destruct
- elim (liftsv_inv_cons2 … H) -H #T2 #T2s #HT2U #HT2Us #H destruct
+theorem liftsv_inj: ∀T1c,Us,f. ⬆*[f] T1c ≡ Us →
+ ∀T2c. ⬆*[f] T2c ≡ Us → T1c = T2c.
+#T1c #Us #f #H elim H -T1c -Us
+[ #T2c #H >(liftsv_inv_nil2 … H) -H //
+| #T1c #Us #T1 #U #HT1U #_ #IHT1Us #X #H destruct
+ elim (liftsv_inv_cons2 … H) -H #T2 #T2c #HT2U #HT2Us #H destruct
>(lifts_inj … HT1U … HT2U) -U /3 width=1 by eq_f/
]
qed-.
(* Basic_2A1: includes: liftv_mono *)
-theorem liftsv_mono: ∀Ts,U1s,t. ⬆*[t] Ts ≡ U1s →
- ∀U2s. ⬆*[t] Ts ≡ U2s → U1s = U2s.
-#Ts #U1s #t #H elim H -Ts -U1s
-[ #U2s #H >(liftsv_inv_nil1 … H) -H //
-| #Ts #U1s #T #U1 #HTU1 #_ #IHTU1s #X #H destruct
- elim (liftsv_inv_cons1 … H) -H #U2 #U2s #HTU2 #HTU2s #H destruct
+theorem liftsv_mono: ∀Ts,U1c,f. ⬆*[f] Ts ≡ U1c →
+ ∀U2c. ⬆*[f] Ts ≡ U2c → U1c = U2c.
+#Ts #U1c #f #H elim H -Ts -U1c
+[ #U2c #H >(liftsv_inv_nil1 … H) -H //
+| #Ts #U1c #T #U1 #HTU1 #_ #IHTU1c #X #H destruct
+ elim (liftsv_inv_cons1 … H) -H #U2 #U2c #HTU2 #HTU2c #H destruct
>(lifts_mono … HTU1 … HTU2) -T /3 width=1 by eq_f/
]
qed-.
(* Basic_1: includes: lifts1_xhg (right to left) *)
(* Basic_2A1: includes: liftsv_liftv_trans_le *)
-theorem liftsv_trans: ∀T1s,Ts,t1. ⬆*[t1] T1s ≡ Ts → ∀T2s,t2. ⬆*[t2] Ts ≡ T2s →
- ∀t. t2 ⊚ t1 ≡ t → ⬆*[t] T1s ≡ T2s.
-#T1s #Ts #t1 #H elim H -T1s -Ts
-[ #T2s #t2 #H >(liftsv_inv_nil1 … H) -T2s /2 width=3 by liftsv_nil/
-| #T1s #Ts #T1 #T #HT1 #_ #IHT1s #X #t2 #H elim (liftsv_inv_cons1 … H) -H
- #T2 #T2s #HT2 #HT2s #H destruct /3 width=6 by lifts_trans, liftsv_cons/
+theorem liftsv_trans: ∀T1c,Ts,f1. ⬆*[f1] T1c ≡ Ts → ∀T2c,f2. ⬆*[f2] Ts ≡ T2c →
+ ∀f. f2 ⊚ f1 ≡ f → ⬆*[f] T1c ≡ T2c.
+#T1c #Ts #f1 #H elim H -T1c -Ts
+[ #T2c #f2 #H >(liftsv_inv_nil1 … H) -T2c /2 width=3 by liftsv_nil/
+| #T1c #Ts #T1 #T #HT1 #_ #IHT1c #X #f2 #H elim (liftsv_inv_cons1 … H) -H
+ #T2 #T2c #HT2 #HT2c #H destruct /3 width=6 by lifts_trans, liftsv_cons/
]
qed-.
(* Forward lemmas on simple terms *******************************************)
(* Basic_2A1: includes: lift_simple_dx *)
-lemma lifts_simple_dx: ∀T1,T2,t. ⬆*[t] T1 ≡ T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄.
-#T1 #T2 #t #H elim H -T1 -T2 -t //
-#a #I #V1 #V2 #T1 #T2 #t #_ #_ #_ #_ #H elim (simple_inv_bind … H)
+lemma lifts_simple_dx: ∀T1,T2,f. ⬆*[f] T1 ≡ T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄.
+#T1 #T2 #f #H elim H -T1 -T2 -f //
+#p #I #V1 #V2 #T1 #T2 #f #_ #_ #_ #_ #H elim (simple_inv_bind … H)
qed-.
(* Basic_2A1: includes: lift_simple_sn *)
-lemma lifts_simple_sn: ∀T1,T2,t. ⬆*[t] T1 ≡ T2 → 𝐒⦃T2⦄ → 𝐒⦃T1⦄.
-#T1 #T2 #t #H elim H -T1 -T2 -t //
-#a #I #V1 #V2 #T1 #T2 #t #_ #_ #_ #_ #H elim (simple_inv_bind … H)
+lemma lifts_simple_sn: ∀T1,T2,f. ⬆*[f] T1 ≡ T2 → 𝐒⦃T2⦄ → 𝐒⦃T1⦄.
+#T1 #T2 #f #H elim H -T1 -T2 -f //
+#p #I #V1 #V2 #T1 #T2 #f #_ #_ #_ #_ #H elim (simple_inv_bind … H)
qed-.
(* GENERIC RELOCATION FOR TERM VECTORS *************************************)
(* Basic_2A1: includes: liftv_nil liftv_cons *)
-inductive liftsv (t:trace) : relation (list term) ≝
-| liftsv_nil : liftsv t (◊) (◊)
-| liftsv_cons: ∀T1s,T2s,T1,T2.
- ⬆*[t] T1 ≡ T2 → liftsv t T1s T2s →
- liftsv t (T1 @ T1s) (T2 @ T2s)
+inductive liftsv (f): relation (list term) ≝
+| liftsv_nil : liftsv f (◊) (◊)
+| liftsv_cons: ∀T1c,T2c,T1,T2.
+ ⬆*[f] T1 ≡ T2 → liftsv f T1c T2c →
+ liftsv f (T1 @ T1c) (T2 @ T2c)
.
interpretation "generic relocation (vector)"
- 'RLiftStar t T1s T2s = (liftsv t T1s T2s).
+ 'RLiftStar f T1c T2c = (liftsv f T1c T2c).
(* Basic inversion lemmas ***************************************************)
-fact liftsv_inv_nil1_aux: ∀X,Y,t. ⬆*[t] X ≡ Y → X = ◊ → Y = ◊.
-#X #Y #t * -X -Y //
-#T1s #T2s #T1 #T2 #_ #_ #H destruct
+fact liftsv_inv_nil1_aux: ∀X,Y,f. ⬆*[f] X ≡ Y → X = ◊ → Y = ◊.
+#X #Y #f * -X -Y //
+#T1c #T2c #T1 #T2 #_ #_ #H destruct
qed-.
(* Basic_2A1: includes: liftv_inv_nil1 *)
-lemma liftsv_inv_nil1: ∀Y,t. ⬆*[t] ◊ ≡ Y → Y = ◊.
+lemma liftsv_inv_nil1: ∀Y,f. ⬆*[f] ◊ ≡ Y → Y = ◊.
/2 width=5 by liftsv_inv_nil1_aux/ qed-.
-fact liftsv_inv_cons1_aux: ∀X,Y,t. ⬆*[t] X ≡ Y →
- ∀T1,T1s. X = T1 @ T1s →
- ∃∃T2,T2s. ⬆*[t] T1 ≡ T2 & ⬆*[t] T1s ≡ T2s &
- Y = T2 @ T2s.
-#X #Y #t * -X -Y
-[ #U1 #U1s #H destruct
-| #T1s #T2s #T1 #T2 #HT12 #HT12s #U1 #U1s #H destruct /2 width=5 by ex3_2_intro/
+fact liftsv_inv_cons1_aux: ∀X,Y,f. ⬆*[f] X ≡ Y →
+ ∀T1,T1c. X = T1 @ T1c →
+ ∃∃T2,T2c. ⬆*[f] T1 ≡ T2 & ⬆*[f] T1c ≡ T2c &
+ Y = T2 @ T2c.
+#X #Y #f * -X -Y
+[ #U1 #U1c #H destruct
+| #T1c #T2c #T1 #T2 #HT12 #HT12c #U1 #U1c #H destruct /2 width=5 by ex3_2_intro/
]
qed-.
(* Basic_2A1: includes: liftv_inv_cons1 *)
-lemma liftsv_inv_cons1: ∀T1,T1s,Y,t. ⬆*[t] T1 @ T1s ≡ Y →
- ∃∃T2,T2s. ⬆*[t] T1 ≡ T2 & ⬆*[t] T1s ≡ T2s &
- Y = T2 @ T2s.
+lemma liftsv_inv_cons1: ∀T1,T1c,Y,f. ⬆*[f] T1 @ T1c ≡ Y →
+ ∃∃T2,T2c. ⬆*[f] T1 ≡ T2 & ⬆*[f] T1c ≡ T2c &
+ Y = T2 @ T2c.
/2 width=3 by liftsv_inv_cons1_aux/ qed-.
-fact liftsv_inv_nil2_aux: ∀X,Y,t. ⬆*[t] X ≡ Y → Y = ◊ → X = ◊.
-#X #Y #t * -X -Y //
-#T1s #T2s #T1 #T2 #_ #_ #H destruct
+fact liftsv_inv_nil2_aux: ∀X,Y,f. ⬆*[f] X ≡ Y → Y = ◊ → X = ◊.
+#X #Y #f * -X -Y //
+#T1c #T2c #T1 #T2 #_ #_ #H destruct
qed-.
-lemma liftsv_inv_nil2: ∀X,t. ⬆*[t] X ≡ ◊ → X = ◊.
+lemma liftsv_inv_nil2: ∀X,f. ⬆*[f] X ≡ ◊ → X = ◊.
/2 width=5 by liftsv_inv_nil2_aux/ qed-.
-fact liftsv_inv_cons2_aux: ∀X,Y,t. ⬆*[t] X ≡ Y →
- ∀T2,T2s. Y = T2 @ T2s →
- ∃∃T1,T1s. ⬆*[t] T1 ≡ T2 & ⬆*[t] T1s ≡ T2s &
- X = T1 @ T1s.
-#X #Y #t * -X -Y
-[ #U2 #U2s #H destruct
-| #T1s #T2s #T1 #T2 #HT12 #HT12s #U2 #U2s #H destruct /2 width=5 by ex3_2_intro/
+fact liftsv_inv_cons2_aux: ∀X,Y,f. ⬆*[f] X ≡ Y →
+ ∀T2,T2c. Y = T2 @ T2c →
+ ∃∃T1,T1c. ⬆*[f] T1 ≡ T2 & ⬆*[f] T1c ≡ T2c &
+ X = T1 @ T1c.
+#X #Y #f * -X -Y
+[ #U2 #U2c #H destruct
+| #T1c #T2c #T1 #T2 #HT12 #HT12c #U2 #U2c #H destruct /2 width=5 by ex3_2_intro/
]
qed-.
-lemma liftsv_inv_cons2: ∀X,T2,T2s,t. ⬆*[t] X ≡ T2 @ T2s →
- ∃∃T1,T1s. ⬆*[t] T1 ≡ T2 & ⬆*[t] T1s ≡ T2s &
- X = T1 @ T1s.
+lemma liftsv_inv_cons2: ∀X,T2,T2c,f. ⬆*[f] X ≡ T2 @ T2c →
+ ∃∃T1,T1c. ⬆*[f] T1 ≡ T2 & ⬆*[f] T1c ≡ T2c &
+ X = T1 @ T1c.
/2 width=3 by liftsv_inv_cons2_aux/ qed-.
(* Basic_1: was: lifts1_flat (left to right) *)
-lemma lifts_inv_applv1: ∀V1s,U1,T2,t. ⬆*[t] Ⓐ V1s.U1 ≡ T2 →
- ∃∃V2s,U2. ⬆*[t] V1s ≡ V2s & ⬆*[t] U1 ≡ U2 &
- T2 = Ⓐ V2s.U2.
-#V1s elim V1s -V1s
+lemma lifts_inv_applv1: ∀V1c,U1,T2,f. ⬆*[f] Ⓐ V1c.U1 ≡ T2 →
+ ∃∃V2c,U2. ⬆*[f] V1c ≡ V2c & ⬆*[f] U1 ≡ U2 &
+ T2 = Ⓐ V2c.U2.
+#V1c elim V1c -V1c
[ /3 width=5 by ex3_2_intro, liftsv_nil/
-| #V1 #V1s #IHV1s #T1 #X #t #H elim (lifts_inv_flat1 … H) -H
- #V2 #Y #HV12 #HY #H destruct elim (IHV1s … HY) -IHV1s -HY
- #V2s #T2 #HV12s #HT12 #H destruct /3 width=5 by ex3_2_intro, liftsv_cons/
+| #V1 #V1c #IHV1c #T1 #X #f #H elim (lifts_inv_flat1 … H) -H
+ #V2 #Y #HV12 #HY #H destruct elim (IHV1c … HY) -IHV1c -HY
+ #V2c #T2 #HV12c #HT12 #H destruct /3 width=5 by ex3_2_intro, liftsv_cons/
]
qed-.
-lemma lifts_inv_applv2: ∀V2s,U2,T1,t. ⬆*[t] T1 ≡ Ⓐ V2s.U2 →
- ∃∃V1s,U1. ⬆*[t] V1s ≡ V2s & ⬆*[t] U1 ≡ U2 &
- T1 = Ⓐ V1s.U1.
-#V2s elim V2s -V2s
+lemma lifts_inv_applv2: ∀V2c,U2,T1,f. ⬆*[f] T1 ≡ Ⓐ V2c.U2 →
+ ∃∃V1c,U1. ⬆*[f] V1c ≡ V2c & ⬆*[f] U1 ≡ U2 &
+ T1 = Ⓐ V1c.U1.
+#V2c elim V2c -V2c
[ /3 width=5 by ex3_2_intro, liftsv_nil/
-| #V2 #V2s #IHV2s #T2 #X #t #H elim (lifts_inv_flat2 … H) -H
- #V1 #Y #HV12 #HY #H destruct elim (IHV2s … HY) -IHV2s -HY
- #V1s #T1 #HV12s #HT12 #H destruct /3 width=5 by ex3_2_intro, liftsv_cons/
+| #V2 #V2c #IHV2c #T2 #X #f #H elim (lifts_inv_flat2 … H) -H
+ #V1 #Y #HV12 #HY #H destruct elim (IHV2c … HY) -IHV2c -HY
+ #V1c #T1 #HV12c #HT12 #H destruct /3 width=5 by ex3_2_intro, liftsv_cons/
]
qed-.
(* Basic properties *********************************************************)
+(* Basic_2A1: includes: liftv_total *)
+lemma liftsv_total: ∀f. ∀T1c:list term. ∃T2c. ⬆*[f] T1c ≡ T2c.
+#f #T1c elim T1c -T1c
+[ /2 width=2 by liftsv_nil, ex_intro/
+| #T1 #T1c * #T2c #HT12c
+ elim (lifts_total T1 f) /3 width=2 by liftsv_cons, ex_intro/
+]
+qed-.
+
(* Basic_1: was: lifts1_flat (right to left) *)
-lemma lifts_applv: ∀V1s,V2s,t. ⬆*[t] V1s ≡ V2s →
- ∀T1,T2. ⬆*[t] T1 ≡ T2 →
- ⬆*[t] Ⓐ V1s. T1 ≡ Ⓐ V2s. T2.
-#V1s #V2s #t #H elim H -V1s -V2s /3 width=1 by lifts_flat/
+lemma lifts_applv: ∀V1c,V2c,f. ⬆*[f] V1c ≡ V2c →
+ ∀T1,T2. ⬆*[f] T1 ≡ T2 →
+ ⬆*[f] Ⓐ V1c. T1 ≡ Ⓐ V2c. T2.
+#V1c #V2c #f #H elim H -V1c -V2c /3 width=1 by lifts_flat/
qed.
-(* Basic_2A1: removed theorems 1: liftv_total *)
(* Basic_1: removed theorems 2: lifts1_nil lifts1_cons *)
(* Forward lemmas on weight for terms ***************************************)
(* Basic_2A1: includes: lift_fwd_tw *)
-lemma lifts_fwd_tw: ∀T1,T2,t. ⬆*[t] T1 ≡ T2 → ♯{T1} = ♯{T2}.
-#T1 #T2 #t #H elim H -T1 -T2 -t normalize //
+lemma lifts_fwd_tw: ∀T1,T2,f. ⬆*[f] T1 ≡ T2 → ♯{T1} = ♯{T2}.
+#T1 #T2 #f #H elim H -T1 -T2 -f normalize //
qed-.
interpretation "extensional equivalence (nstream)"
'ExtEq A t1 t2 = (eq_stream A t1 t2).
+definition eq_stream_repl (A) (R:relation …) ≝
+ ∀t1,t2. t1 ≐⦋A⦌ t2 → R t1 t2.
+
definition eq_stream_repl_back (A) (R:predicate …) ≝
- ∀t1,t2. t1 ≐⦋A⦌ t2 → R t1 → R t2.
+ ∀t1. R t1 → ∀t2. t1 ≐⦋A⦌ t2 → R t2.
definition eq_stream_repl_fwd (A) (R:predicate …) ≝
- ∀t1,t2. t2 ≐⦋A⦌ t1 → R t1 → R t2.
+ ∀t1. R t1 → ∀t2. t2 ≐⦋A⦌ t1 → R t2.
(* Basic inversion lemmas ***************************************************)
lemma eq_stream_split (A) (t): (hd … t) @ (tl … t) ≐⦋A⦌ t.
#A * //
qed.
+
+lemma tln_eq_repl (A) (i): eq_stream_repl A (λt1,t2. tln … i t1 ≐ tln … i t2).
+#A #i elim i -i //
+#i #IH * #n1 #t1 * #n2 #t2 #H elim (eq_stream_inv_seq ????? H) -H
+/2 width=1 by/
+qed.
(* Main inversion lemmas on after *******************************************)
-let corec after_mono: ∀f1,f2,x. f1 ⊚ f2 ≡ x → ∀y. f1 ⊚ f2 ≡ y → x ≐ y ≝ ?.
-* #n1 #f1 * #n2 #f2 * #n #x #Hx * #m #y #Hy
-cases (after_inv_apply … Hx) -Hx #Hn #Hx
-cases (after_inv_apply … Hy) -Hy #Hm #Hy
-/3 width=4 by eq_seq/
-qed-.
-
-let corec after_inj: ∀f1,x,f. f1 ⊚ x ≡ f → ∀y. f1 ⊚ y ≡ f → x ≐ y ≝ ?.
-* #n1 #f1 * #n2 #x * #n #f #Hx * #m2 #y #Hy
-cases (after_inv_apply … Hx) -Hx #Hn2 #Hx
-cases (after_inv_apply … Hy) -Hy #Hm2
-cases (apply_inj_aux … Hn2 Hm2) -n -m2 /3 width=4 by eq_seq/
+let corec after_mono: ∀f1,f2,f,g1,g2,g. f1 ⊚ f2 ≡ f → g1 ⊚ g2 ≡ g →
+ f1 ≐ g1 → f2 ≐ g2 → f ≐ g ≝ ?.
+* #n1 #f1 * #n2 #f2 * #n #f * #m1 #g1 * #m2 #g2 * #m #g #Hf #Hg #H1 #H2
+cases (after_inv_apply … Hf) -Hf #Hn #Hf
+cases (after_inv_apply … Hg) -Hg #Hm #Hg
+cases (eq_stream_inv_seq ????? H1) -H1
+cases (eq_stream_inv_seq ????? H2) -H2
+/4 width=8 by apply_eq_repl, tln_eq_repl, eq_seq/
+qed-.
+
+let corec after_inj: ∀f1,f2,f,g1,g2,g. f1 ⊚ f2 ≡ f → g1 ⊚ g2 ≡ g →
+ f1 ≐ g1 → f ≐ g → f2 ≐ g2 ≝ ?.
+* #n1 #f1 * #n2 #f2 * #n #f * #m1 #g1 * #m2 #g2 * #m #g #Hf #Hg #H1 #H2
+cases (after_inv_apply … Hf) -Hf #Hn #Hf
+cases (after_inv_apply … Hg) -Hg #Hm #Hg
+cases (eq_stream_inv_seq ????? H1) -H1 #Hnm1 #Hfg1
+cases (eq_stream_inv_seq ????? H2) -H2 #Hnm #Hfg
+lapply (apply_inj_aux … Hn Hm Hnm ?) -n -m
+/4 width=8 by tln_eq_repl, eq_seq/
qed-.
theorem after_inv_total: ∀f1,f2,f. f1 ⊚ f2 ≡ f → f1 ∘ f2 ≐ f.
-/2 width=4 by after_mono/ qed-.
+/2 width=8 by after_mono/ qed-.
(* Basic properties on apply ************************************************)
+lemma apply_eq_repl (i): eq_stream_repl … (λf1,f2. f1@❴i❵ = f2@❴i❵).
+#i elim i -i [2: #i #IH ] * #n1 #f1 * #n2 #f2 #H
+elim (eq_stream_inv_seq ????? H) -H normalize //
+#Hn #Hf /4 width=1 by eq_f2, eq_f/
+qed.
+
lemma apply_S1: ∀f,n,i. (⫯n@f)@❴i❵ = ⫯((n@f)@❴i❵).
#n #f * //
qed.
lemma at_inv_total: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → i2 = f@❴i1❵.
/2 width=6 by at_mono/ qed-.
-lemma at_repl_back: ∀i1,i2. eq_stream_repl_back ? (λf. @⦃i1, f⦄ ≡ i2).
-#i1 #i2 #f1 #f2 #Ht #H1 lapply (at_total i1 f2)
-#H2 <(at_mono … Ht … H1 … H2) -f1 -i2 //
+lemma at_eq_repl_back: ∀i1,i2. eq_stream_repl_back ? (λf. @⦃i1, f⦄ ≡ i2).
+#i1 #i2 #f1 #H1 #f2 #Hf lapply (at_total i1 f2)
+#H2 <(at_mono … Hf … H1 … H2) -f1 -i2 //
qed-.
-lemma at_repl_fwd: ∀i1,i2. eq_stream_repl_fwd ? (λf. @⦃i1, f⦄ ≡ i2).
-#i1 #i2 @eq_stream_repl_sym /2 width=3 by at_repl_back/
+lemma at_eq_repl_fwd: ∀i1,i2. eq_stream_repl_fwd ? (λf. @⦃i1, f⦄ ≡ i2).
+#i1 #i2 @eq_stream_repl_sym /2 width=3 by at_eq_repl_back/
qed-.
(* Advanced properties on at ************************************************)
(* Advanced properties on apply *********************************************)
-fact apply_inj_aux: ∀f1,f2. f1 ≐ f2 → ∀i,i1,i2. i = f1@❴i1❵ → i = f2@❴i2❵ → i1 = i2.
+fact apply_inj_aux: ∀f1,f2,j1,j2,i1,i2. j1 = f1@❴i1❵ → j2 = f2@❴i2❵ →
+ j1 = j2 → f1 ≐ f2 → i1 = i2.
/2 width=6 by at_inj/ qed-.
(* Basic properties on isid *************************************************)
+lemma isid_eq_repl_back: eq_stream_repl_back … isid.
+/2 width=3 by eq_stream_canc_sn/ qed-.
+
+lemma isid_eq_repl_fwd: eq_stream_repl_fwd … isid.
+/3 width=3 by isid_eq_repl_back, eq_stream_repl_sym/ qed-.
+
lemma isid_id: 𝐈⦃𝐈𝐝⦄.
// qed.
#_ #H destruct
qed-.
+lemma isid_inv_gen: ∀f. 𝐈⦃f⦄ → ∃∃g. 𝐈⦃g⦄ & f = ↑g.
+* #n #f #H elim (isid_inv_seq … H) -H
+#Hf #H destruct /2 width=3 by ex2_intro/
+qed-.
+
+lemma isid_inv_eq_repl: ∀f1,f2. 𝐈⦃f1⦄ → 𝐈⦃f2⦄ → f1 ≐ f2.
+/2 width=3 by eq_stream_canc_dx/ qed-.
+
(* inversion lemmas on at ***************************************************)
let corec id_inv_at: ∀f. (∀i. @⦃i, f⦄ ≡ i) → f ≐ 𝐈𝐝 ≝ ?.
#i2 #i #Hi2 lapply (at_total i2 f1)
#H0 lapply (at_increasing … H0)
#Ht1 lapply (after_fwd_at2 … (f1@❴i2❵) … H0 … Ht)
-/3 width=7 by at_repl_back, at_mono, at_id_le/
+/3 width=7 by at_eq_repl_back, at_mono, at_id_le/
qed.
(* Inversion lemmas on after ************************************************)
qed-.
lemma after_isid_inv_sn: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f1⦄ → f2 ≐ f.
-/3 width=4 by isid_after_sn, after_mono/
+/3 width=8 by isid_after_sn, after_mono/
qed-.
lemma after_isid_inv_dx: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f2⦄ → f1 ≐ f.
-/3 width=4 by isid_after_dx, after_mono/
+/3 width=8 by isid_after_dx, after_mono/
qed-.
(*
lemma after_inv_isid3: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃t⦄ → 𝐈⦃t1⦄ ∧ 𝐈⦃t2⦄.
(* Basic properties *********************************************************)
+lemma push_eq_repl: eq_stream_repl … (λf1,f2. ↑f1 ≐ ↑f2).
+/2 width=1 by eq_seq/ qed.
+
+lemma next_eq_repl: eq_stream_repl … (λf1,f2. ⫯f1 ≐ ⫯f2).
+* #n1 #f1 * #n2 #f2 #H elim (eq_stream_inv_seq ????? H) -H
+/2 width=1 by eq_seq/
+qed.
+
lemma push_rew: ∀f. ↑f = 0@f.
// qed.
lemma next_inv_seq_dx: ∀f,g,n. ⫯f = n@g → ∃∃m. n = ⫯m & f = m@g.
* #m #f #g #n >next_rew #H destruct /2 width=3 by ex2_intro/
qed-.
+
+lemma push_inv_dx: ∀x,f. x ≐ ↑f → ∃∃g. x = ↑g & g ≐ f.
+* #m #x #f #H elim (eq_stream_inv_seq ????? H) -H
+/2 width=3 by ex2_intro/
+qed-.
+
+lemma push_inv_sn: ∀f,x. ↑f ≐ x → ∃∃g. x = ↑g & f ≐ g.
+#f #x #H lapply (eq_stream_sym … H) -H
+#H elim (push_inv_dx … H) -H
+/3 width=3 by eq_stream_sym, ex2_intro/
+qed-.
+
+lemma push_inv_bi: ∀f,g. ↑f ≐ ↑g → f ≐ g.
+#f #g #H elim (push_inv_dx … H) -H
+#x #H #Hg lapply (injective_push … H) -H //
+qed-.
+
+lemma next_inv_dx: ∀x,f. x ≐ ⫯f → ∃∃g. x = ⫯g & g ≐ f.
+* #m #x * #n #f #H elim (eq_stream_inv_seq ????? H) -H
+/3 width=5 by eq_seq, ex2_intro/
+qed-.
+
+lemma next_inv_sn: ∀f,x. ⫯f ≐ x → ∃∃g. x = ⫯g & f ≐ g.
+#f #x #H lapply (eq_stream_sym … H) -H
+#H elim (next_inv_dx … H) -H
+/3 width=3 by eq_stream_sym, ex2_intro/
+qed-.
+
+lemma next_inv_bi: ∀f,g. ⫯f ≐ ⫯g → f ≐ g.
+#f #g #H elim (next_inv_dx … H) -H
+#x #H #Hg lapply (injective_next … H) -H //
+qed-.
}
]
class "green"
- [ { "multiple relocation" * } {
+ [ { "natural numbers with infinity" * } {
[ { "" * } {
- [ "nstream" "nstream_lift ( ↑? ) ( ⫯? )" "nstream_at ( ?@❴?❵ ) ( @⦃?,?⦄ ≡ ? )" "nstream_after ( ? ∘ ? ) ( ? ⊚ ? ≡ ? )" "nstream_id ( 𝐈𝐝 ) ( 𝐈⦃?⦄ )" * ]
- [ "trace ( ∥?∥ )" "trace_at ( @⦃?,?⦄ ≡ ? )" "trace_after ( ? ⊚ ? ≡ ? )" "trace_isid ( 𝐈⦃?⦄ )" "trace_isun ( 𝐔⦃?⦄ )"
- "trace_sle ( ? ⊆ ? )" "trace_sor ( ? ⋓ ? ≡ ? )" "trace_snot ( ∁ ? )" * ]
- [ "mr2" "mr2_at ( @⦃?,?⦄ ≡ ? )" "mr2_plus ( ? + ? )" "mr2_minus ( ? ▭ ? ≡ ? )" * ]
+ [ "ynat ( ∞ )" "ynat_pred ( ⫰? )" "ynat_succ ( ⫯? )"
+ "ynat_le ( ? ≤ ? )" "ynat_lt ( ? < ? )"
+ "ynat_plus ( ? + ? )" *
+ ]
}
]
}
]
class "grass"
- [ { "natural numbers with infinity" * } {
+ [ { "multiple relocation" * } {
[ { "" * } {
- [ "ynat ( ∞ )" "ynat_pred ( ⫰? )" "ynat_succ ( ⫯? )"
- "ynat_le ( ? ≤ ? )" "ynat_lt ( ? < ? )"
- "ynat_plus ( ? + ? )" *
- ]
+ [ "nstream" "nstream_lift ( ↑? ) ( ⫯? )" "nstream_at ( ?@❴?❵ ) ( @⦃?,?⦄ ≡ ? )" "nstream_after ( ? ∘ ? ) ( ? ⊚ ? ≡ ? )" "nstream_id ( 𝐈𝐝 ) ( 𝐈⦃?⦄ )" * ]
+ [ "trace ( ∥?∥ )" "trace_at ( @⦃?,?⦄ ≡ ? )" "trace_after ( ? ⊚ ? ≡ ? )" "trace_isid ( 𝐈⦃?⦄ )" "trace_isun ( 𝐔⦃?⦄ )"
+ "trace_sle ( ? ⊆ ? )" "trace_sor ( ? ⋓ ? ≡ ? )" "trace_snot ( ∁ ? )" * ]
+ [ "mr2" "mr2_at ( @⦃?,?⦄ ≡ ? )" "mr2_plus ( ? + ? )" "mr2_minus ( ? ▭ ? ≡ ? )" * ]
}
]
}
projects / helm.git / commitdiff