(* GENERIC NOTATION *********************************************************)
+(* Note: this should go to core_notation *)
+notation "⊥"
+ non associative with precedence 90
+ for @{'false}.
+
+(* Note: this should go to core_notation *)
+notation "⊤"
+ non associative with precedence 90
+ for @{'true}.
+
(* Note: this should go to core_notation *)
notation "hvbox(a break ≺ b)"
non associative with precedence 45
include "background/xoa_notation.ma".
include "background/xoa.ma".
+include "background/notation.ma".
(* logic *)
(* Note: For some reason this cannot be in the standard library *)
interpretation "logical false" 'false = False.
-notation "⊥"
- non associative with precedence 90
- for @{'false}.
+(* booleans *)
+
+(* Note: For some reason this cannot be in the standard library *)
+interpretation "boolean false" 'false = false.
+
+(* Note: For some reason this cannot be in the standard library *)
+interpretation "boolean true" 'true = true.
(* arithmetics *)
interpretation "multiple existental quantifier (2, 3)" 'Ex P0 P1 = (ex2_3 ? ? ? P0 P1).
+(* multiple existental quantifier (3, 1) *)
+
+inductive ex3 (A0:Type[0]) (P0,P1,P2:A0→Prop) : Prop ≝
+ | ex3_intro: ∀x0. P0 x0 → P1 x0 → P2 x0 → ex3 ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (3, 1)" 'Ex P0 P1 P2 = (ex3 ? P0 P1 P2).
+
(* multiple existental quantifier (3, 2) *)
inductive ex3_2 (A0,A1:Type[0]) (P0,P1,P2:A0→A1→Prop) : Prop ≝
interpretation "multiple existental quantifier (3, 3)" 'Ex P0 P1 P2 = (ex3_3 ? ? ? P0 P1 P2).
+(* multiple existental quantifier (3, 4) *)
+
+inductive ex3_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2:A0→A1→A2→A3→Prop) : Prop ≝
+ | ex3_4_intro: ∀x0,x1,x2,x3. P0 x0 x1 x2 x3 → P1 x0 x1 x2 x3 → P2 x0 x1 x2 x3 → ex3_4 ? ? ? ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (3, 4)" 'Ex P0 P1 P2 = (ex3_4 ? ? ? ? P0 P1 P2).
+
+(* multiple existental quantifier (4, 1) *)
+
+inductive ex4 (A0:Type[0]) (P0,P1,P2,P3:A0→Prop) : Prop ≝
+ | ex4_intro: ∀x0. P0 x0 → P1 x0 → P2 x0 → P3 x0 → ex4 ? ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (4, 1)" 'Ex P0 P1 P2 P3 = (ex4 ? P0 P1 P2 P3).
+
+(* multiple existental quantifier (4, 2) *)
+
+inductive ex4_2 (A0,A1:Type[0]) (P0,P1,P2,P3:A0→A1→Prop) : Prop ≝
+ | ex4_2_intro: ∀x0,x1. P0 x0 x1 → P1 x0 x1 → P2 x0 x1 → P3 x0 x1 → ex4_2 ? ? ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (4, 2)" 'Ex P0 P1 P2 P3 = (ex4_2 ? ? P0 P1 P2 P3).
+
(* multiple existental quantifier (4, 3) *)
inductive ex4_3 (A0,A1,A2:Type[0]) (P0,P1,P2,P3:A0→A1→A2→Prop) : Prop ≝
non associative with precedence 20
for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) }.
+(* multiple existental quantifier (3, 1) *)
+
+notation > "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1 break & term 19 P2)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}.$P0) (λ${ident x0}.$P1) (λ${ident x0}.$P2) }.
+
+notation < "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1 break & term 19 P2)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}:$T0.$P0) (λ${ident x0}:$T0.$P1) (λ${ident x0}:$T0.$P2) }.
+
(* multiple existental quantifier (3, 2) *)
notation > "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1 break & term 19 P2)"
non associative with precedence 20
for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P2) }.
+(* multiple existental quantifier (3, 4) *)
+
+notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P2) }.
+
+notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P2) }.
+
+(* multiple existental quantifier (4, 1) *)
+
+notation > "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}.$P0) (λ${ident x0}.$P1) (λ${ident x0}.$P2) (λ${ident x0}.$P3) }.
+
+notation < "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}:$T0.$P0) (λ${ident x0}:$T0.$P1) (λ${ident x0}:$T0.$P2) (λ${ident x0}:$T0.$P3) }.
+
+(* multiple existental quantifier (4, 2) *)
+
+notation > "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}.λ${ident x1}.$P0) (λ${ident x0}.λ${ident x1}.$P1) (λ${ident x0}.λ${ident x1}.$P2) (λ${ident x0}.λ${ident x1}.$P3) }.
+
+notation < "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P3) }.
+
(* multiple existental quantifier (4, 3) *)
notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)"
.
interpretation "decomposed standard computation"
- 'Std M N = (dst M N).
+ 'DecomposedStd M N = (dst M N).
notation "hvbox( M break ⓢ↦* term 46 N )"
non associative with precedence 45
- for @{ 'Std $M $N }.
+ for @{ 'DecomposedStd $M $N }.
lemma dst_inv_lref: ∀M,N. M ⓢ↦* N → ∀j. #j = N →
∃∃s. is_whd s & M ↦*[s] #j.
--- /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 "subterms/delifting_substitution.ma".
+include "subterms/projections.ma".
+include "paths/standard_order.ma".
+
+(* PATH-LABELED STANDARD REDUCTION ON SUBTERMS (SINGLE STEP) ****************)
+
+(* Note: this is standard reduction on marked redexes,
+ left residuals are unmarked in the reductum
+*)
+inductive pl_st: path → relation subterms ≝
+| pl_st_beta : ∀V,T. pl_st (◊) ({⊤}@V.{⊤}𝛌.T) ([↙V]T)
+| pl_st_abst : ∀b,p,T1,T2. pl_st p T1 T2 → pl_st (rc::p) ({b}𝛌.T1) ({⊥}𝛌.T2)
+| pl_st_appl_sn: ∀b,p,V1,V2,T. pl_st p V1 V2 → pl_st (sn::p) ({b}@V1.T) ({⊥}@V2.{⊥}⇕T)
+| pl_st_appl_dx: ∀b,p,V,T1,T2. pl_st p T1 T2 → pl_st (dx::p) ({b}@V.T1) ({b}@V.T2)
+.
+
+interpretation "path-labeled standard reduction"
+ 'Std F p G = (pl_st p F G).
+
+notation "hvbox( F break Ⓡ ↦ [ term 46 p ] break term 46 G )"
+ non associative with precedence 45
+ for @{ 'Std $F $p $G }.
+(*
+lemma pl_st_inv_pl_sred: ∀p,F,G. F Ⓡ↦[p] G → ⇓F ↦[p] ⇓G.
+#p #F #G #H elim H -p -F -G // /2 width=1/
+qed-.
+
+lemma pl_st_inv_vref: ∀p,F,G. F Ⓡ↦[p] G → ∀b,i. {b}#i = F → ⊥.
+/3 width=5 by pl_st_inv_st, st_inv_vref/
+qed-.
+*)
+lemma pl_st_inv_abst: ∀p,F,G. F Ⓡ↦[p] G → ∀b0,U1. {b0}𝛌.U1 = F →
+ ∃∃q,U2. U1 Ⓡ↦[q] U2 & rc::q = p & {⊥}𝛌.U2 = G.
+#p #F #G * -p -F -G
+[ #V #T #b0 #U1 #H destruct
+| #b #p #T1 #T2 #HT12 #b0 #U1 #H destruct /2 width=5/
+| #b #p #V1 #V2 #T #_ #b0 #U1 #H destruct
+| #b #p #V #T1 #T2 #_ #b0 #U1 #H destruct
+]
+qed-.
+
+lemma pl_st_inv_appl: ∀p,F,G. F Ⓡ↦[p] G → ∀b0,W,U. {b0}@W.U = F →
+ ∨∨ (∃∃U0. ⊤ = b0 & ◊ = p & {⊤}𝛌.U0 = U & [↙W] U0 = G)
+ | (∃∃q,W0. sn::q = p & W Ⓡ↦[q] W0 & {⊥}@W0.{⊥}⇕U = G)
+ | (∃∃q,U0. dx::q = p & U Ⓡ↦[q] U0 & {b0}@W.U0 = G).
+#p #F #G * -p -F -G
+[ #V #T #b0 #W #U #H destruct /3 width=3/
+| #b #p #T1 #T2 #_ #b0 #W #U #H destruct
+| #b #p #V1 #V2 #T #HV12 #b0 #W #U #H destruct /3 width=5/
+| #b #p #V #T1 #T2 #HT12 #b0 #W #U #H destruct /3 width=5/
+]
+qed-.
+
+lemma pl_st_fwd_abst: ∀p,F,G. F Ⓡ↦[p] G → ∀b0,U2. {b0}𝛌.U2 = G →
+ ◊ = p ∨ ∃q. rc::q = p.
+#p #F #G * -p -F -G
+[ /2 width=1/
+| /3 width=2/
+| #b #p #V1 #V2 #T #_ #b0 #U2 #H destruct
+| #b #p #V #T1 #T2 #_ #b0 #U2 #H destruct
+]
+qed-.
+
+lemma pl_st_inv_nil: ∀p,F,G. F Ⓡ↦[p] G → ◊ = p →
+ ∃∃V,T. {⊤}@V.{⊤} 𝛌.T = F & [↙V] T = G.
+#p #F #G * -p -F -G
+[ #V #T #_ destruct /2 width=4/
+| #b #p #T1 #T2 #_ #H destruct
+| #b #p #V1 #V2 #T #_ #H destruct
+| #b #p #V #T1 #T2 #_ #H destruct
+]
+qed-.
+
+lemma pl_st_inv_rc: ∀p,F,G. F Ⓡ↦[p] G → ∀q. rc::q = p →
+ ∃∃b,T1,T2. T1 Ⓡ↦[q] T2 & {b}𝛌.T1 = F & {⊥}𝛌.T2 = G.
+#p #F #G * -p -F -G
+[ #V #T #q #H destruct
+| #b #p #T1 #T2 #HT12 #q #H destruct /2 width=6/
+| #b #p #V1 #V2 #T #_ #q #H destruct
+| #b #p #V #T1 #T2 #_ #q #H destruct
+]
+qed-.
+
+lemma pl_st_inv_sn: ∀p,F,G. F Ⓡ↦[p] G → ∀q. sn::q = p →
+ ∃∃b,V1,V2,T. V1 Ⓡ↦[q] V2 & {b}@V1.T = F & {⊥}@V2.{⊥}⇕T = G.
+#p #F #G * -p -F -G
+[ #V #T #q #H destruct
+| #b #p #T1 #T2 #_ #q #H destruct
+| #b #p #V1 #V2 #T #HV12 #q #H destruct /2 width=7/
+| #b #p #V #T1 #T2 #_ #q #H destruct
+]
+qed-.
+
+lemma pl_st_inv_dx: ∀p,F,G. F Ⓡ↦[p] G → ∀q. dx::q = p →
+ ∃∃b,V,T1,T2. T1 Ⓡ↦[q] T2 & {b}@V.T1 = F & {b}@V.T2 = G.
+#p #F #G * -p -F -G
+[ #V #T #q #H destruct
+| #b #p #T1 #T2 #_ #q #H destruct
+| #b #p #V1 #V2 #T #_ #q #H destruct
+| #b #p #V #T1 #T2 #HT12 #q #H destruct /2 width=7/
+]
+qed-.
+
+
+
+(*
+lemma pl_st_lift: ∀p. sliftable (pl_st p).
+#p #h #F1 #F2 #H elim H -p -F1 -F2 normalize /2 width=1/
+[ #V #T #d <sdsubst_slift_le //
+| #b #p #V1 #V2 #T #_ #IHV12 #d
+qed.
+
+lemma pl_st_inv_lift: ∀p. deliftable_sn (pl_st p).
+#p #h #G1 #G2 #H elim H -p -G1 -G2
+[ #W #U #d #F1 #H
+ elim (lift_inv_appl … H) -H #V #F #H0 #HF #H destruct
+ elim (lift_inv_abst … HF) -HF #T #H0 #H destruct /3 width=3/
+| #p #U1 #U2 #_ #IHU12 #d #F1 #H
+ elim (lift_inv_abst … H) -H #T1 #HTU1 #H
+ elim (IHU12 … HTU1) -U1 #T2 #HT12 #HTU2 destruct
+ @(ex2_intro … (𝛌.T2)) // /2 width=1/
+| #p #W1 #W2 #U1 #_ #IHW12 #d #F1 #H
+ elim (lift_inv_appl … H) -H #V1 #T #HVW1 #H1 #H2
+ elim (IHW12 … HVW1) -W1 #V2 #HV12 #HVW2 destruct
+ @(ex2_intro … (@V2.T)) // /2 width=1/
+| #p #W1 #U1 #U2 #_ #IHU12 #d #F1 #H
+ elim (lift_inv_appl … H) -H #V #T1 #H1 #HTU1 #H2
+ elim (IHU12 … HTU1) -U1 #T2 #HT12 #HTU2 destruct
+ @(ex2_intro … (@V.T2)) // /2 width=1/
+]
+qed-.
+
+lemma pl_st_dsubst: ∀p. sdsubstable_dx (pl_st p).
+#p #W1 #F1 #F2 #H elim H -p -F1 -F2 normalize /2 width=1/
+#W2 #T #d >dsubst_dsubst_ge //
+qed.
+*)
+
+lemma pl_st_inv_empty: ∀p,G1,G2. G1 Ⓡ↦[p] G2 → ∀F1. {⊥}⇕F1 = G1 → ⊥.
+#p #F1 #F2 #H elim H -p -F1 -F2
+[ #V #T #F1 #H
+ elim (mk_boolean_inv_appl … H) -H #b0 #W #U #H destruct
+| #b #p #T1 #T2 #_ #IHT12 #F1 #H
+ elim (mk_boolean_inv_abst … H) -H /2 width=2/
+| #b #p #V1 #V2 #T #_ #IHV12 #F1 #H
+ elim (mk_boolean_inv_appl … H) -H /2 width=2/
+| #b #p #V #T1 #T2 #_ #IHT12 #F1 #H
+ elim (mk_boolean_inv_appl … H) -H /2 width=2/
+]
+qed-.
+
+theorem pl_st_mono: ∀p. singlevalued … (pl_st p).
+#p #F #G1 #H elim H -p -F -G1
+[ #V #T #G2 #H elim (pl_st_inv_nil … H ?) -H //
+ #W #U #H #HG2 destruct //
+| #b #p #T1 #T2 #_ #IHT12 #G2 #H elim (pl_st_inv_rc … H ??) -H [3: // |2: skip ] (**) (* simplify line *)
+ #b0 #U1 #U2 #HU12 #H #HG2 destruct /3 width=1/
+| #b #p #V1 #V2 #T #_ #IHV12 #G2 #H elim (pl_st_inv_sn … H ??) -H [3: // |2: skip ] (**) (* simplify line *)
+ #b0 #W1 #W2 #U #HW12 #H #HG2 destruct /3 width=1/
+| #b #p #V #T1 #T2 #_ #IHT12 #G2 #H elim (pl_st_inv_dx … H ??) -H [3: // |2: skip ] (**) (* simplify line *)
+ #b0 #W #U1 #U2 #HU12 #H #HG2 destruct /3 width=1/
+]
+qed-.
+
+theorem pl_st_inv_is_standard: ∀p1,F1,F. F1 Ⓡ↦[p1] F →
+ ∀p2,F2. F Ⓡ↦[p2] F2 → p1 ≤ p2.
+#p1 #F1 #F #H elim H -p1 -F1 -F //
+[ #b #p #T1 #T #_ #IHT1 #p2 #F2 #H elim (pl_st_inv_abst … H ???) -H [3: // |2,4: skip ] (**) (* simplify line *)
+ #q #T2 #HT2 #H1 #H2 destruct /3 width=2/
+| #b #p #V1 #V #T #_ #IHV1 #p2 #F2 #H elim (pl_st_inv_appl … H ????) -H [7: // |2,3,4: skip ] * (**) (* simplify line *)
+ [ #U #H destruct
+ | #q #V2 #H1 #HV2 #H2 destruct /3 width=2/
+ | #q #U #_ #H elim (pl_st_inv_empty … H ??) [ // | skip ] (**) (* simplify line *)
+ ]
+| #b #p #V #T1 #T #HT1 #IHT1 #p2 #F2 #H elim (pl_st_inv_appl … H ????) -H [7: // |2,3,4: skip ] * (**) (* simplify line *)
+ [ #U #_ #H1 #H2 #_ -b -V -F2 -IHT1
+ elim (pl_st_fwd_abst … HT1 … H2) // -H1 * #q #H
+ elim (pl_st_inv_rc … HT1 … H) -HT1 -H #b #U1 #U2 #_ #_ #H -b -q -T1 -U1 destruct
+ | #q #V2 #H1 #_ #_ -b -F2 -T1 -T -V -V2 destruct //
+ | #q #T2 #H1 #HT2 #H2 -b -F2 -T1 -V /3 width=2/
+ ]
+]
+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 "subterms/lift.ma".
+
+(* DELIFTING SUBSTITUTION ***************************************************)
+
+(* Policy: depth (level) metavariables: d, e (as for lift) *)
+let rec sdsubst G d F on F ≝ match F with
+[ SVRef b i ⇒ tri … i d ({b}#i) (↑[i] G) ({b}#(i-1))
+| SAbst b T ⇒ {b}𝛌. (sdsubst G (d+1) T)
+| SAppl b V T ⇒ {b}@ (sdsubst G d V). (sdsubst G d T)
+].
+
+interpretation "delifting substitution for subterms"
+ 'DSubst G d F = (sdsubst G d F).
+
+lemma sdsubst_vref_lt: ∀b,i,d,G. i < d → [d ↙ G] {b}#i = {b}#i.
+normalize /2 width=1/
+qed.
+
+lemma sdsubst_vref_eq: ∀b,i,G. [i ↙ G] {b}#i = ↑[i]G.
+normalize //
+qed.
+
+lemma sdsubst_vref_gt: ∀b,i,d,G. d < i → [d ↙ G] {b}#i = {b}#(i-1).
+normalize /2 width=1/
+qed.
+
+theorem sdsubst_slift_le: ∀h,G,F,d1,d2. d2 ≤ d1 →
+ [d2 ↙ ↑[d1 - d2, h] G] ↑[d1 + 1, h] F = ↑[d1, h] [d2 ↙ G] F.
+#h #G #F elim F -F
+[ #b #i #d1 #d2 #Hd21 elim (lt_or_eq_or_gt i d2) #Hid2
+ [ lapply (lt_to_le_to_lt … Hid2 Hd21) -Hd21 #Hid1
+ >(sdsubst_vref_lt … Hid2) >(slift_vref_lt … Hid1) >slift_vref_lt /2 width=1/
+ | destruct >sdsubst_vref_eq >slift_vref_lt /2 width=1/
+ | >(sdsubst_vref_gt … Hid2) -Hd21 elim (lt_or_ge (i-1) d1) #Hi1d1
+ [ >(slift_vref_lt … Hi1d1) >slift_vref_lt /2 width=1/
+ | lapply (ltn_to_ltO … Hid2) #Hi
+ >(slift_vref_ge … Hi1d1) >slift_vref_ge /2 width=1/ -Hi1d1 >plus_minus // /3 width=1/
+ ]
+ ]
+| normalize #b #T #IHT #d1 #d2 #Hd21
+ lapply (IHT (d1+1) (d2+1) ?) -IHT /2 width=1/
+| normalize #b #V #T #IHV #IHT #d1 #d2 #Hd21
+ >IHV -IHV // >IHT -IHT //
+]
+qed.
+
+theorem sdsubst_slift_be: ∀h,G,F,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h →
+ [d2 ↙ G] ↑[d1, h + 1] F = ↑[d1, h] F.
+#h #G #F elim F -F
+[ #b #i #d1 #d2 #Hd12 #Hd21 elim (lt_or_ge i d1) #Hid1
+ [ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 -Hd21 #Hid2
+ >(slift_vref_lt … Hid1) >(slift_vref_lt … Hid1) /2 width=1/
+ | lapply (transitive_le … (i+h) Hd21 ?) -Hd12 -Hd21 /2 width=1/ #Hd2
+ >(slift_vref_ge … Hid1) >(slift_vref_ge … Hid1) -Hid1
+ >sdsubst_vref_gt // /2 width=1/
+ ]
+| normalize #b #T #IHT #d1 #d2 #Hd12 #Hd21
+ >IHT -IHT // /2 width=1/
+| normalize #b #V #T #IHV #IHT #d1 #d2 #Hd12 #Hd21
+ >IHV -IHV // >IHT -IHT //
+]
+qed.
+
+theorem sdsubst_slift_ge: ∀h,G,F,d1,d2. d1 + h ≤ d2 →
+ [d2 ↙ G] ↑[d1, h] F = ↑[d1, h] [d2 - h ↙ G] F.
+#h #G #F elim F -F
+[ #b #i #d1 #d2 #Hd12 elim (lt_or_eq_or_gt i (d2-h)) #Hid2h
+ [ >(sdsubst_vref_lt … Hid2h) elim (lt_or_ge i d1) #Hid1
+ [ lapply (lt_to_le_to_lt … (d1+h) Hid1 ?) -Hid2h // #Hid1h
+ lapply (lt_to_le_to_lt … Hid1h Hd12) -Hid1h -Hd12 #Hid2
+ >(slift_vref_lt … Hid1) -Hid1 /2 width=1/
+ | >(slift_vref_ge … Hid1) -Hid1 -Hd12 /3 width=1/
+ ]
+ | destruct elim (le_inv_plus_l … Hd12) -Hd12 #Hd12 #Hhd2
+ >sdsubst_vref_eq >slift_vref_ge // >slift_slift_be // <plus_minus_m_m //
+ | elim (le_inv_plus_l … Hd12) -Hd12 #Hd12 #_
+ lapply (le_to_lt_to_lt … Hd12 Hid2h) -Hd12 #Hid1
+ lapply (ltn_to_ltO … Hid2h) #Hi
+ >(sdsubst_vref_gt … Hid2h)
+ >slift_vref_ge /2 width=1/ >slift_vref_ge /2 width=1/ -Hid1
+ >sdsubst_vref_gt /2 width=1/ -Hid2h >plus_minus //
+ ]
+| normalize #b #T #IHT #d1 #d2 #Hd12
+ elim (le_inv_plus_l … Hd12) #_ #Hhd2
+ >IHT -IHT /2 width=1/ <plus_minus //
+| normalize #b #V #T #IHV #IHT #d1 #d2 #Hd12
+ >IHV -IHV // >IHT -IHT //
+]
+qed.
+
+theorem sdsubst_sdsubst_ge: ∀G1,G2,F,d1,d2. d1 ≤ d2 →
+ [d2 ↙ G2] [d1 ↙ G1] F = [d1 ↙ [d2 - d1 ↙ G2] G1] [d2 + 1 ↙ G2] F.
+#G1 #G2 #F elim F -F
+[ #b #i #d1 #d2 #Hd12 elim (lt_or_eq_or_gt i d1) #Hid1
+ [ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 #Hid2
+ >(sdsubst_vref_lt … Hid1) >(sdsubst_vref_lt … Hid2) >sdsubst_vref_lt /2 width=1/
+ | destruct >sdsubst_vref_eq >sdsubst_vref_lt /2 width=1/
+ | >(sdsubst_vref_gt … Hid1) elim (lt_or_eq_or_gt i (d2+1)) #Hid2
+ [ lapply (ltn_to_ltO … Hid1) #Hi
+ >(sdsubst_vref_lt … Hid2) >sdsubst_vref_lt /2 width=1/
+ | destruct /2 width=1/
+ | lapply (le_to_lt_to_lt (d1+1) … Hid2) -Hid1 /2 width=1/ -Hd12 #Hid1
+ >(sdsubst_vref_gt … Hid2) >sdsubst_vref_gt /2 width=1/
+ >sdsubst_vref_gt // /2 width=1/
+ ]
+ ]
+| normalize #b #T #IHT #d1 #d2 #Hd12
+ lapply (IHT (d1+1) (d2+1) ?) -IHT /2 width=1/
+| normalize #b #V #T #IHV #IHT #d1 #d2 #Hd12
+ >IHV -IHV // >IHT -IHT //
+]
+qed.
+
+theorem sdsubst_sdsubst_lt: ∀G1,G2,F,d1,d2. d2 < d1 →
+ [d2 ↙ [d1 - d2 -1 ↙ G1] G2] [d1 ↙ G1] F = [d1 - 1 ↙ G1] [d2 ↙ G2] F.
+#G1 #G2 #F #d1 #d2 #Hd21
+lapply (ltn_to_ltO … Hd21) #Hd1
+>sdsubst_sdsubst_ge in ⊢ (???%); /2 width=1/ <plus_minus_m_m //
+qed.
+
+definition sdsubstable_dx: predicate (relation subterms) ≝ λR.
+ ∀G,F1,F2. R F1 F2 → ∀d. R ([d ↙ G] F1) ([d ↙ G] F2).
+(*
+definition sdsubstable: predicate (relation subterms) ≝ λR.
+ ∀G1,G2. R G1 G2 → ∀F1,F2. R F1 F2 → ∀d. R ([d ↙ G1] F1) ([d ↙ G2] F2).
+
+lemma star_sdsubstable_dx: ∀R. sdsubstable_dx R → sdsubstable_dx (star … R).
+#R #HR #G #F1 #F2 #H elim H -F2 // /3 width=3/
+qed.
+
+lemma lstar_sdsubstable_dx: ∀S,R. (∀a. sdsubstable_dx (R a)) →
+ ∀l. sdsubstable_dx (lstar S … R l).
+#S #R #HR #l #G #F1 #F2 #H
+@(lstar_ind_l ????????? H) -l -F1 // /3 width=3/
+qed.
+
+lemma star_sdsubstable: ∀R. reflexive ? R →
+ sdsubstable R → sdsubstable (star … R).
+#R #H1R #H2 #G1 #G2 #H elim H -G2 /3 width=1/ /3 width=5/
+qed.
+*)
lapply (sym_eq subterms … H) -H >(plus_minus_m_m … Hh1d2) in ⊢ (???%→?); -Hh1d2 #H
elim (slift_inv_slift_le … Hd12 … H) -H -Hd12 /2 width=3/
qed-.
-(*
-definition liftable: predicate (relation term) ≝ λR.
- ∀h,M1,M2. R M1 M2 → ∀d. R (↑[d, h] M1) (↑[d, h] M2).
-definition deliftable_sn: predicate (relation term) ≝ λR.
- ∀h,N1,N2. R N1 N2 → ∀d,M1. ↑[d, h] M1 = N1 →
- ∃∃M2. R M1 M2 & ↑[d, h] M2 = N2.
+definition sliftable: predicate (relation subterms) ≝ λR.
+ ∀h,F1,F2. R F1 F2 → ∀d. R (↑[d, h] F1) (↑[d, h] F2).
-lemma star_liftable: ∀R. liftable R → liftable (star … R).
-#R #HR #h #M1 #M2 #H elim H -M2 // /3 width=3/
+definition sdeliftable_sn: predicate (relation subterms) ≝ λR.
+ ∀h,G1,G2. R G1 G2 → ∀d,F1. ↑[d, h] F1 = G1 →
+ ∃∃F2. R F1 F2 & ↑[d, h] F2 = G2.
+(*
+lemma star_sliftable: ∀R. sliftable R → sliftable (star … R).
+#R #HR #h #F1 #F2 #H elim H -F2 // /3 width=3/
qed.
-lemma star_deliftable_sn: ∀R. deliftable_sn R → deliftable_sn (star … R).
-#R #HR #h #N1 #N2 #H elim H -N2 /2 width=3/
-#N #N2 #_ #HN2 #IHN1 #d #M1 #HMN1
-elim (IHN1 … HMN1) -N1 #M #HM1 #HMN
-elim (HR … HN2 … HMN) -N /3 width=3/
+lemma star_deliftable_sn: ∀R. sdeliftable_sn R → sdeliftable_sn (star … R).
+#R #HR #h #G1 #G2 #H elim H -G2 /2 width=3/
+#G #G2 #_ #HG2 #IHG1 #d #F1 #HFG1
+elim (IHG1 … HFG1) -G1 #F #HF1 #HFG
+elim (HR … HG2 … HFG) -G /3 width=3/
qed-.
-lemma lstar_liftable: ∀S,R. (∀a. liftable (R a)) →
- ∀l. liftable (lstar S … R l).
-#S #R #HR #l #h #M1 #M2 #H
-@(lstar_ind_l ????????? H) -l -M1 // /3 width=3/
+lemma lstar_sliftable: ∀S,R. (∀a. sliftable (R a)) →
+ ∀l. sliftable (lstar S … R l).
+#S #R #HR #l #h #F1 #F2 #H
+@(lstar_ind_l ????????? H) -l -F1 // /3 width=3/
qed.
-lemma lstar_deliftable_sn: ∀S,R. (∀a. deliftable_sn (R a)) →
- ∀l. deliftable_sn (lstar S … R l).
-#S #R #HR #l #h #N1 #N2 #H
-@(lstar_ind_l ????????? H) -l -N1 /2 width=3/
-#a #l #N1 #N #HN1 #_ #IHN2 #d #M1 #HMN1
-elim (HR … HN1 … HMN1) -N1 #M #HM1 #HMN
-elim (IHN2 … HMN) -N /3 width=3/
+lemma lstar_sdeliftable_sn: ∀S,R. (∀a. sdeliftable_sn (R a)) →
+ ∀l. sdeliftable_sn (lstar S … R l).
+#S #R #HR #l #h #G1 #G2 #H
+@(lstar_ind_l ????????? H) -l -G1 /2 width=3/
+#a #l #G1 #G #HG1 #_ #IHG2 #d #F1 #HFG1
+elim (HR … HG1 … HFG1) -G1 #F #HF1 #HFG
+elim (IHG2 … HFG) -G /3 width=3/
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 "terms/term.ma".
+include "subterms/subterms.ma".
+
+(* PROJECTIONS **************************************************************)
+
+(* Note: the boolean subset of subterms *)
+let rec boolean b M on M ≝ match M with
+[ VRef i ⇒ {b}#i
+| Abst A ⇒ {b}𝛌.(boolean b A)
+| Appl B A ⇒ {b}@(boolean b B).(boolean b A)
+].
+
+interpretation "boolean subset (subterms)"
+ 'ProjectUp b M = (boolean b M).
+
+notation "hvbox( { term 46 b } ⇑ break term 46 M)"
+ non associative with precedence 46
+ for @{ 'ProjectUp $b $M }.
+
+lemma boolean_inv_vref: ∀j,b0,b,M. {b}⇑ M = {b0}#j → b = b0 ∧ M = #j.
+#j #b0 #b * normalize
+[ #i #H destruct /2 width=1/
+| #A #H destruct
+| #B #A #H destruct
+]
+qed-.
+
+lemma boolean_inv_abst: ∀U,b0,b,M. {b}⇑ M = {b0}𝛌.U →
+ ∃∃C. b = b0 & {b}⇑C = U & M = 𝛌.C.
+#U #b0 #b * normalize
+[ #i #H destruct
+| #A #H destruct /2 width=3/
+| #B #A #H destruct
+]
+qed-.
+
+lemma boolean_inv_appl: ∀W,U,b0,b,M. {b}⇑ M = {b0}@W.U →
+ ∃∃D,C. b = b0 & {b}⇑D = W & {b}⇑C = U & M = @D.C.
+#W #U #b0 #b * normalize
+[ #i #H destruct
+| #A #H destruct
+| #B #A #H destruct /2 width=5/
+]
+qed-.
+
+(* Note: the carrier (underlying term) of a subset of subterms *)
+let rec carrier F on F ≝ match F with
+[ SVRef _ i ⇒ #i
+| SAbst _ T ⇒ 𝛌.(carrier T)
+| SAppl _ V T ⇒ @(carrier V).(carrier T)
+].
+
+interpretation "carrier (subterms)"
+ 'ProjectDown F = (carrier F).
+
+notation "hvbox(⇓ term 46 F)"
+ non associative with precedence 46
+ for @{ 'ProjectDown $F }.
+
+lemma carrier_inv_vref: ∀j,F. ⇓F = #j → ∃b. F = {b}#j.
+#j * normalize
+[ #b #i #H destruct /2 width=2/
+| #b #T #H destruct
+| #b #V #T #H destruct
+]
+qed-.
+
+lemma carrier_inv_abst: ∀C,F. ⇓F = 𝛌.C → ∃∃b,U. ⇓U = C & F = {b}𝛌.U.
+#C * normalize
+[ #b #i #H destruct
+| #b #T #H destruct /2 width=4/
+| #b #V #T #H destruct
+]
+qed-.
+
+lemma carrier_inv_appl: ∀D,C,F. ⇓F = @D.C →
+ ∃∃b,W,U. ⇓W = D & ⇓U = C & F = {b}@W.U.
+#D #C * normalize
+[ #b #i #H destruct
+| #b #T #H destruct
+| #b #V #T #H destruct /2 width=6/
+]
+qed-.
+
+definition mk_boolean: bool → subterms → subterms ≝
+ λb,F. {b}⇑⇓F.
+
+interpretation "make boolean (subterms)"
+ 'ProjectSame b F = (mk_boolean b F).
+
+notation "hvbox( { term 46 b } ⇕ break term 46 F)"
+ non associative with precedence 46
+ for @{ 'ProjectSame $b $F }.
+
+lemma mk_boolean_inv_vref: ∀j,b0,b,F. {b}⇕ F = {b0}#j →
+ ∃∃b1. b = b0 & F = {b1}#j.
+#j #b0 #b #F #H
+elim (boolean_inv_vref … H) -H #H0 #H
+elim (carrier_inv_vref … H) -H /2 width=2/
+qed-.
+
+lemma mk_boolean_inv_abst: ∀U,b0,b,F. {b}⇕ F = {b0}𝛌.U →
+ ∃∃b1,T. b = b0 & {b}⇕T = U & F = {b1}𝛌.T.
+#U #b0 #b #F #H
+elim (boolean_inv_abst … H) -H #C #H0 #H1 #H
+elim (carrier_inv_abst … H) -H #b1 #U1 #H3 destruct /2 width=4/
+qed-.
+
+lemma mk_boolean_inv_appl: ∀W,U,b0,b,F. {b}⇕ F = {b0}@W.U →
+ ∃∃b1,V,T. b = b0 & {b}⇕V = W & {b}⇕T = U & F = {b1}@V.T.
+#W #U #b0 #b #F #H
+elim (boolean_inv_appl … H) -H #D #C #H0 #H1 #H2 #H
+elim (carrier_inv_appl … H) -H #b1 #W1 #U1 #H3 #H4 destruct /2 width=6/
+qed-.
(**************************************************************************)
include "background/preamble.ma".
-include "background/notation.ma".
(* SUBSETS OF SUBTERMS ******************************************************)
(* DELIFTING SUBSTITUTION ***************************************************)
(* Policy: depth (level) metavariables: d, e (as for lift) *)
-let rec dsubst D d M on M ≝ match M with
-[ VRef i ⇒ tri … i d (#i) (↑[i] D) (#(i-1))
-| Abst A ⇒ 𝛌. (dsubst D (d+1) A)
-| Appl B A ⇒ @ (dsubst D d B). (dsubst D d A)
+let rec dsubst N d M on M ≝ match M with
+[ VRef i ⇒ tri … i d (#i) (↑[i] N) (#(i-1))
+| Abst A ⇒ 𝛌. (dsubst N (d+1) A)
+| Appl B A ⇒ @ (dsubst N d B). (dsubst N d A)
].
interpretation "delifting substitution"
- 'DSubst D d M = (dsubst D d M).
+ 'DSubst N d M = (dsubst N d M).
-lemma dsubst_vref_lt: ∀i,d,D. i < d → [d ↙ D] #i = #i.
+lemma dsubst_vref_lt: ∀i,d,N. i < d → [d ↙ N] #i = #i.
normalize /2 width=1/
qed.
-lemma dsubst_vref_eq: ∀i,D. [i ↙ D] #i = ↑[i]D.
+lemma dsubst_vref_eq: ∀i,N. [i ↙ N] #i = ↑[i]N.
normalize //
qed.
-lemma dsubst_vref_gt: ∀i,d,D. d < i → [d ↙ D] #i = #(i-1).
+lemma dsubst_vref_gt: ∀i,d,N. d < i → [d ↙ N] #i = #(i-1).
normalize /2 width=1/
qed.
-theorem dsubst_lift_le: ∀h,D,M,d1,d2. d2 ≤ d1 →
- [d2 ↙ ↑[d1 - d2, h] D] ↑[d1 + 1, h] M = ↑[d1, h] [d2 ↙ D] M.
-#h #D #M elim M -M
+theorem dsubst_lift_le: ∀h,N,M,d1,d2. d2 ≤ d1 →
+ [d2 ↙ ↑[d1 - d2, h] N] ↑[d1 + 1, h] M = ↑[d1, h] [d2 ↙ N] M.
+#h #N #M elim M -M
[ #i #d1 #d2 #Hd21 elim (lt_or_eq_or_gt i d2) #Hid2
[ lapply (lt_to_le_to_lt … Hid2 Hd21) -Hd21 #Hid1
>(dsubst_vref_lt … Hid2) >(lift_vref_lt … Hid1) >lift_vref_lt /2 width=1/
]
qed.
-theorem dsubst_lift_be: ∀h,D,M,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h →
- [d2 ↙ D] ↑[d1, h + 1] M = ↑[d1, h] M.
-#h #D #M elim M -M
+theorem dsubst_lift_be: ∀h,N,M,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h →
+ [d2 ↙ N] ↑[d1, h + 1] M = ↑[d1, h] M.
+#h #N #M elim M -M
[ #i #d1 #d2 #Hd12 #Hd21 elim (lt_or_ge i d1) #Hid1
[ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 -Hd21 #Hid2
>(lift_vref_lt … Hid1) >(lift_vref_lt … Hid1) /2 width=1/
]
qed.
-theorem dsubst_lift_ge: ∀h,D,M,d1,d2. d1 + h ≤ d2 →
- [d2 ↙ D] ↑[d1, h] M = ↑[d1, h] [d2 - h ↙ D] M.
-#h #D #M elim M -M
+theorem dsubst_lift_ge: ∀h,N,M,d1,d2. d1 + h ≤ d2 →
+ [d2 ↙ N] ↑[d1, h] M = ↑[d1, h] [d2 - h ↙ N] M.
+#h #N #M elim M -M
[ #i #d1 #d2 #Hd12 elim (lt_or_eq_or_gt i (d2-h)) #Hid2h
[ >(dsubst_vref_lt … Hid2h) elim (lt_or_ge i d1) #Hid1
[ lapply (lt_to_le_to_lt … (d1+h) Hid1 ?) -Hid2h // #Hid1h
]
qed.
-theorem dsubst_dsubst_ge: ∀D1,D2,M,d1,d2. d1 ≤ d2 →
- [d2 ↙ D2] [d1 ↙ D1] M = [d1 ↙ [d2 - d1 ↙ D2] D1] [d2 + 1 ↙ D2] M.
-#D1 #D2 #M elim M -M
+theorem dsubst_dsubst_ge: ∀N1,N2,M,d1,d2. d1 ≤ d2 →
+ [d2 ↙ N2] [d1 ↙ N1] M = [d1 ↙ [d2 - d1 ↙ N2] N1] [d2 + 1 ↙ N2] M.
+#N1 #N2 #M elim M -M
[ #i #d1 #d2 #Hd12 elim (lt_or_eq_or_gt i d1) #Hid1
[ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 #Hid2
>(dsubst_vref_lt … Hid1) >(dsubst_vref_lt … Hid2) >dsubst_vref_lt /2 width=1/
]
qed.
-theorem dsubst_dsubst_lt: ∀D1,D2,M,d1,d2. d2 < d1 →
- [d2 ↙ [d1 - d2 -1 ↙ D1] D2] [d1 ↙ D1] M = [d1 - 1 ↙ D1] [d2 ↙ D2] M.
-#D1 #D2 #M #d1 #d2 #Hd21
+theorem dsubst_dsubst_lt: ∀N1,N2,M,d1,d2. d2 < d1 →
+ [d2 ↙ [d1 - d2 -1 ↙ N1] N2] [d1 ↙ N1] M = [d1 - 1 ↙ N1] [d2 ↙ N2] M.
+#N1 #N2 #M #d1 #d2 #Hd21
lapply (ltn_to_ltO … Hd21) #Hd1
>dsubst_dsubst_ge in ⊢ (???%); /2 width=1/ <plus_minus_m_m //
qed.
definition dsubstable_dx: predicate (relation term) ≝ λR.
- ∀D,M1,M2. R M1 M2 → ∀d. R ([d ↙ D] M1) ([d ↙ D] M2).
+ ∀N,M1,M2. R M1 M2 → ∀d. R ([d ↙ N] M1) ([d ↙ N] M2).
definition dsubstable: predicate (relation term) ≝ λR.
- ∀D1,D2. R D1 D2 → ∀M1,M2. R M1 M2 → ∀d. R ([d ↙ D1] M1) ([d ↙ D2] M2).
+ ∀N1,N2. R N1 N2 → ∀M1,M2. R M1 M2 → ∀d. R ([d ↙ N1] M1) ([d ↙ N2] M2).
lemma star_dsubstable_dx: ∀R. dsubstable_dx R → dsubstable_dx (star … R).
-#R #HR #D #M1 #M2 #H elim H -M2 // /3 width=3/
+#R #HR #N #M1 #M2 #H elim H -M2 // /3 width=3/
qed.
lemma lstar_dsubstable_dx: ∀S,R. (∀a. dsubstable_dx (R a)) →
∀l. dsubstable_dx (lstar S … R l).
-#S #R #HR #l #D #M1 #M2 #H
+#S #R #HR #l #N #M1 #M2 #H
@(lstar_ind_l ????????? H) -l -M1 // /3 width=3/
qed.
lemma star_dsubstable: ∀R. reflexive ? R →
dsubstable R → dsubstable (star … R).
-#R #H1R #H2 #D1 #D2 #H elim H -D2 /3 width=1/ /3 width=5/
+#R #H1R #H2 #N1 #N2 #H elim H -N2 /3 width=1/ /3 width=5/
qed.
lemma sred_inv_abst: ∀M,N. M ↦ N → ∀C1. 𝛌.C1 = M →
∃∃C2. C1 ↦ C2 & 𝛌.C2 = N.
#M #N * -M -N
-[ #B #A #C #H destruct
+[ #B #A #C1 #H destruct
| #A1 #A2 #HA12 #C1 #H destruct /2 width=3/
| #B1 #B2 #A #_ #C1 #H destruct
| #B #A1 #A2 #_ #C1 #H destruct
(* Initial invocation: - Patience on us to gain peace and perfection! - *)
include "background/preamble.ma".
-include "background/notation.ma".
(* TERM STRUCTURE ***********************************************************)
<key name="include">basics/pts.ma</key>
<key name="ex">2 2</key>
<key name="ex">2 3</key>
+ <key name="ex">3 1</key>
<key name="ex">3 2</key>
<key name="ex">3 3</key>
+ <key name="ex">3 4</key>
+ <key name="ex">4 1</key>
+ <key name="ex">4 2</key>
<key name="ex">4 3</key>
<key name="or">3</key>
</section>
projects / helm.git / commitdiff