/2 width=1/
qed.
-lemma slt_nil: ∀c,p. ◊ < c::p.
+lemma slt_nil: ∀o,p. ◊ < o::p.
/2 width=1/
qed.
/2 width=1/
qed.
-lemma slt_comp: ∀c,p,q. p < q → c::p < c::q.
-#c #p #q #H elim H -q /3 width=1/ /3 width=3/
+lemma slt_comp: ∀o,p,q. p < q → o::p < o::q.
+#o #p #q #H elim H -q /3 width=1/ /3 width=3/
qed.
theorem slt_trans: transitive … slt.
--- /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 "paths/standard_trace.ma".
+include "paths/labeled_sequential_computation.ma".
+include "paths/labeled_st_reduction.ma".
+
+(* PATH-LABELED STANDARD COMPUTATION (MULTISTEP) ****************************)
+
+(* Note: lstar shuld be replaced by l_sreds *)
+definition pl_sts: trace → relation subterms ≝ lstar … pl_st.
+
+interpretation "path-labeled standard reduction"
+ 'StdStar F p G = (pl_sts p F G).
+
+notation "hvbox( F break Ⓡ ↦* [ term 46 p ] break term 46 G )"
+ non associative with precedence 45
+ for @{ 'StdStar $F $p $G }.
+
+lemma pl_sts_fwd_pl_sreds: ∀s,F1,F2. F1 Ⓡ↦*[s] F2 → ⇓F1 ↦*[s] ⇓F2.
+#s #F1 #F2 #H @(lstar_ind_r ????????? H) -s -F2 //
+#p #s #F #F2 #_ #HF2 #IHF1
+lapply (pl_st_fwd_pl_sred … HF2) -HF2 /2 width=3/
+qed-.
+
+lemma pl_sts_refl: reflexive … (pl_sts (◊)).
+//
+qed.
+
+lemma pl_sts_step_sn: ∀p,F1,F. F1 Ⓡ↦[p] F → ∀s,F2. F Ⓡ↦*[s] F2 → F1 Ⓡ↦*[p::s] F2.
+/2 width=3/
+qed-.
+
+lemma pl_sts_step_dx: ∀s,F1,F. F1 Ⓡ↦*[s] F → ∀p,F2. F Ⓡ↦[p] F2 → F1 Ⓡ↦*[s@p::◊] F2.
+/2 width=3/
+qed-.
+
+lemma pl_sts_step_rc: ∀p,F1,F2. F1 Ⓡ↦[p] F2 → F1 Ⓡ↦*[p::◊] F2.
+/2 width=1/
+qed.
+
+lemma pl_sts_inv_nil: ∀s,F1,F2. F1 Ⓡ↦*[s] F2 → ◊ = s → F1 = F2.
+/2 width=5 by lstar_inv_nil/
+qed-.
+
+lemma pl_sts_inv_cons: ∀s,F1,F2. F1 Ⓡ↦*[s] F2 → ∀q,r. q::r = s →
+ ∃∃F. F1 Ⓡ↦[q] F & F Ⓡ↦*[r] F2.
+/2 width=3 by lstar_inv_cons/
+qed-.
+
+lemma pl_sts_inv_step_rc: ∀p,F1,F2. F1 Ⓡ↦*[p::◊] F2 → F1 Ⓡ↦[p] F2.
+/2 width=1 by lstar_inv_step/
+qed-.
+
+lemma pl_sts_inv_pos: ∀s,F1,F2. F1 Ⓡ↦*[s] F2 → 0 < |s| →
+ ∃∃p,r,F. p::r = s & F1 Ⓡ↦[p] F & F Ⓡ↦*[r] F2.
+/2 width=1 by lstar_inv_pos/
+qed-.
+
+lemma pl_sts_lift: ∀s. sliftable (pl_sts s).
+/2 width=1/
+qed.
+
+lemma pl_sts_inv_lift: ∀s. sdeliftable_sn (pl_sts s).
+/3 width=3 by lstar_sdeliftable_sn, pl_st_inv_lift/
+qed-.
+
+lemma pl_sts_dsubst: ∀s. sdsubstable_f_dx … (booleanized ⊥) (pl_sts s).
+/2 width=1/
+qed.
+
+theorem pl_sts_mono: ∀s. singlevalued … (pl_sts s).
+/3 width=7 by lstar_singlevalued, pl_st_mono/
+qed-.
+
+theorem pl_sts_trans: ltransitive … pl_sts.
+/2 width=3 by lstar_ltransitive/
+qed-.
+
+theorem pl_sts_fwd_is_standard: ∀s,F1,F2. F1 Ⓡ↦*[s] F2 → is_standard s.
+#s elim s -s // #p1 * //
+#p2 #s #IHs #F1 #F2 #H
+elim (pl_sts_inv_cons … H ???) -H [4: // |2,3: skip ] #F3 #HF13 #H (**) (* simplify line *)
+elim (pl_sts_inv_cons … H ???) [2: // |3,4: skip ] #F4 #HF34 #_ (**) (* simplify line *)
+lapply (pl_st_fwd_sle … HF13 … HF34) -F1 -F4 /3 width=3/
+qed-.
+
+axiom pl_sred_is_standard_pl_st: ∀p,M,M2. M ↦[p] M2 → ∀F. ⇓F = M →
+ ∀s,M1.{⊤}⇑ M1 Ⓡ↦*[s] F →
+ is_standard (s@(p::◊)) →
+ ∃∃F2. F Ⓡ↦[p] F2 & ⇓F2 = M2.
+
+theorem pl_sreds_is_standard_pl_sts: ∀s,M1,M2. M1 ↦*[s] M2 → is_standard s →
+ ∃∃F2. {⊤}⇑ M1 Ⓡ↦*[s] F2 & ⇓F2 = M2.
+#s #M1 #M2 #H @(lstar_ind_r ????????? H) -s -M2 /2 width=3/
+#p #s #M #M2 #_ #HM2 #IHM1 #Hsp
+lapply (is_standard_fwd_append_sn … Hsp) #Hs
+elim (IHM1 Hs) -IHM1 -Hs #F #HM1 #H
+elim (pl_sred_is_standard_pl_st … HM2 … HM1 ?) -HM2 // -M -Hsp #F2 #HF2 #HFM2
+lapply (pl_sts_step_dx … HM1 … HF2) -F
+#H @(ex2_intro … F2) // (**) (* auto needs some help here *)
+qed-.
(* *)
(**************************************************************************)
-include "subterms/booleanize.ma".
+include "subterms/booleanized.ma".
+include "paths/labeled_sequential_reduction.ma".
include "paths/standard_order.ma".
(* PATH-LABELED STANDARD REDUCTION ON SUBTERMS (SINGLE STEP) ****************)
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/
+
+lemma pl_st_fwd_pl_sred: ∀p,F1,F2. F1 Ⓡ↦[p] F2 → ⇓F1 ↦[p] ⇓F2.
+#p #F1 #F2 #H elim H -p -F1 -F2 normalize /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/
+#p #F #G #HFG #b #i #H
+lapply (pl_st_fwd_pl_sred … HFG) -HFG #HFG
+lapply (eq_f … carrier … H) -H normalize #H
+/2 width=6 by pl_sred_inv_vref/
qed-.
-*)
-lemma pl_st_inv_abst: ∀p,F,G. F Ⓡ↦[p] G → ∀b0,U1. {b0}𝛌.U1 = F →
+
+lemma pl_st_inv_abst: ∀p,F,G. F Ⓡ↦[p] G → ∀c,U1. {c}𝛌.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
+[ #V #T #c #U1 #H destruct
+| #b #p #T1 #T2 #HT12 #c #U1 #H destruct /2 width=5/
+| #b #p #V1 #V2 #T #_ #c #U1 #H destruct
+| #b #p #V #T1 #T2 #_ #c #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)
+lemma pl_st_inv_appl: ∀p,F,G. F Ⓡ↦[p] G → ∀c,W,U. {c}@W.U = F →
+ ∨∨ (∃∃U0. ⊤ = c & ◊ = 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).
+ | (∃∃q,U0. dx::q = p & U Ⓡ↦[q] U0 & {c}@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/
+[ #V #T #c #W #U #H destruct /3 width=3/
+| #b #p #T1 #T2 #_ #c #W #U #H destruct
+| #b #p #V1 #V2 #T #HV12 #c #W #U #H destruct /3 width=5/
+| #b #p #V #T1 #T2 #HT12 #c #W #U #H destruct /3 width=5/
]
qed-.
-lemma pl_st_fwd_abst: ∀p,F,G. F Ⓡ↦[p] G → ∀b0,U2. {b0}𝛌.U2 = G →
+lemma pl_st_fwd_abst: ∀p,F,G. F Ⓡ↦[p] G → ∀c,U2. {c}𝛌.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
+| #b #p #V1 #V2 #T #_ #c #U2 #H destruct
+| #b #p #V #T1 #T2 #_ #c #U2 #H destruct
]
qed-.
]
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 //
+#p #h #F1 #F2 #H elim H -p -F1 -F2 /2 width=1/
+[ #V #T #d normalize <sdsubst_slift_le //
| #b #p #V1 #V2 #T #_ #IHV12 #d
+ whd in ⊢ (??%%); <booleanized_lift /2 width=1/ (**) (* auto needs some help here *)
+]
qed.
-lemma pl_st_inv_lift: ∀p. deliftable_sn (pl_st p).
+lemma pl_st_inv_lift: ∀p. sdeliftable_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 (slift_inv_appl … H) -H #V #F #H0 #HF #H destruct
+ elim (slift_inv_abst … HF) -HF #T #H0 #H destruct /3 width=3/
+| #b #p #U1 #U2 #_ #IHU12 #d #F1 #H
+ elim (slift_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
+ @(ex2_intro … ({⊥}𝛌.T2)) // /2 width=1/
+| #b #p #W1 #W2 #U1 #_ #IHW12 #d #F1 #H
+ elim (slift_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
+ @(ex2_intro … ({⊥}@V2.{⊥}⇕T)) [ /2 width=1/ ]
+ whd in ⊢ (??%%); // (**) (* auto needs some help here *)
+| #b #p #W1 #U1 #U2 #_ #IHU12 #d #F1 #H
+ elim (slift_inv_appl … H) -H #V #T1 #H1 #HTU1 #H2
elim (IHU12 … HTU1) -U1 #T2 #HT12 #HTU2 destruct
- @(ex2_intro … (@V.T2)) // /2 width=1/
+ @(ex2_intro … ({b}@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 //
+lemma pl_st_dsubst: ∀p. sdsubstable_f_dx … (booleanized ⊥) (pl_st p).
+#p #W1 #F1 #F2 #H elim H -p -F1 -F2 /2 width=1/
+[ #W2 #T #d normalize >sdsubst_sdsubst_ge //
+| #b #p #V1 #V2 #T #_ #IHV12 #d
+ whd in ⊢ (??%%); <(booleanized_booleanized ⊥) in ⊢ (???(???%)); <booleanized_dsubst /2 width=1/ (**) (* auto needs some help here *)
+]
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
+ elim (booleanized_inv_appl … H) -H #c #W #U #H destruct
| #b #p #T1 #T2 #_ #IHT12 #F1 #H
- elim (mk_boolean_inv_abst … H) -H /2 width=2/
+ elim (booleanized_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/
+ elim (booleanized_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/
+ elim (booleanized_inv_appl … H) -H /2 width=2/
]
qed-.
[ #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/
+ #c #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/
+ #c #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/
+ #c #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.
+theorem pl_st_fwd_sle: ∀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/
(* PATH *********************************************************************)
-(* Policy: path step metavariables: c *)
+(* Policy: path step metavariables: o *)
(* Note: this is a step of a path in the tree representation of a term:
rc (rectus) : proceed on the argument of an abstraction
sn (sinister): proceed on the left argument of an application
| dx: step
.
-definition is_dx: predicate step ≝ λc. dx = c.
+definition is_dx: predicate step ≝ λo. dx = o.
(* Policy: path metavariables: p, q *)
(* Note: this is a path in the tree representation of a term, heading to a redex *)
* // /2 width=1/
qed.
-lemma sle_comp: ∀p1,p2. p1 ≤ p2 → ∀c. (c::p1) ≤ (c::p2).
+lemma sle_comp: ∀p1,p2. p1 ≤ p2 → ∀o. (o::p1) ≤ (o::p2).
#p1 #p2 #H elim H -p2 // /3 width=3/
qed.
lemma sle_dichotomy: ∀p1,p2:path. p1 ≤ p2 ∨ p2 ≤ p1.
#p1 elim p1 -p1
[ * /2 width=1/
-| #c1 #p1 #IHp1 * /2 width=1/
- * #p2 cases c1 -c1 /2 width=1/
+| #o1 #p1 #IHp1 * /2 width=1/
+ * #p2 cases o1 -o1 /2 width=1/
elim (IHp1 p2) -IHp1 /3 width=1/
]
qed-.
(* Note: standard precedence relation on paths: p ≺ q
to serve as base for the order relations: p < q and p ≤ q *)
inductive sprec: relation path ≝
-| sprec_nil : ∀c,q. sprec (◊) (c::q)
+| sprec_nil : ∀o,q. sprec (◊) (o::q)
| sprec_rc : ∀p,q. sprec (dx::p) (rc::q)
| sprec_sn : ∀p,q. sprec (rc::p) (sn::q)
-| sprec_comp: ∀c,p,q. sprec p q → sprec (c::p) (c::q)
+| sprec_comp: ∀o,p,q. sprec p q → sprec (o::p) (o::q)
| sprec_skip: sprec (dx::◊) ◊
.
lemma sprec_inv_sn: ∀p,q. p ≺ q → ∀p0. sn::p0 = p →
∃∃q0. p0 ≺ q0 & sn::q0 = q.
#p #q * -p -q
-[ #c #q #p0 #H destruct
+[ #o #q #p0 #H destruct
| #p #q #p0 #H destruct
| #p #q #p0 #H destruct
-| #c #p #q #Hpq #p0 #H destruct /2 width=3/
+| #o #p #q #Hpq #p0 #H destruct /2 width=3/
| #p0 #H destruct
]
qed-.
#p #q #H elim H -p -q // /2 width=1/
[ #p #q * #H destruct
| #p #q * #H destruct
-| #c #p #q #_ #IHpq * #H destruct /3 width=1/
+| #o #p #q #_ #IHpq * #H destruct /3 width=1/
]
qed-.
(* Note: to us, a "standard" computation contracts redexes in non-decreasing positions *)
definition is_standard: predicate trace ≝ Allr … sle.
-lemma is_standard_compatible: ∀c,s. is_standard s → is_standard (c:::s).
-#c #s elim s -s // #p * //
+lemma is_standard_compatible: ∀o,s. is_standard s → is_standard (o:::s).
+#o #s elim s -s // #p * //
#q #s #IHs * /3 width=1/
qed.
| #q #r #IHr * /3 width=1/
]
qed.
+
+lemma is_standard_fwd_append_sn: ∀s,r. is_standard (s@r) → is_standard s.
+/2 width=2 by Allr_fwd_append_sn/
+qed-.
T, U, V, W: subset of subterms
a : arbitrary element
-b : boolean mark
-c : pointer step
+b,c : boolean mark
d, e : variable reference level
+f : arbitrary function
h : relocation height
i, j : variable reference depth (de Bruijn index)
k : relocation height
l : arbitrary list
m, n : measures on terms
+o : pointer step
p, q : pointer
r, s : pointer sequence
-
(* *)
(**************************************************************************)
-include "terms/relocating_substitution.ma".
-include "subterms/relocating_substitution.ma".
+include "subterms/carrier.ma".
(* BOOLEAN (EMPTY OR FULL) SUBSET *******************************************)
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
+lemma boolean_inv_vref: ∀j,c,b,M. {b}⇑ M = {c}#j → b = c ∧ M = #j.
+#j #c #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
+lemma boolean_inv_abst: ∀U,c,b,M. {b}⇑ M = {c}𝛌.U →
+ ∃∃C. b = c & {b}⇑C = U & M = 𝛌.C.
+#U #c #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
+lemma boolean_inv_appl: ∀W,U,c,b,M. {b}⇑ M = {c}@W.U →
+ ∃∃D,C. b = c & {b}⇑D = W & {b}⇑C = U & M = @D.C.
+#W #U #c #b * normalize
[ #i #H destruct
| #A #H destruct
| #B #A #H destruct /2 width=5/
| >(sdsubst_vref_gt … Hid) >(dsubst_vref_gt … Hid) //
]
qed.
+
+lemma carrier_boolean: ∀b,M. ⇓ {b}⇑ M = M.
+#b #M elim M -M normalize //
+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/carrier.ma".
-include "subterms/boolean.ma".
-
-(* BOOLEANIZE (EMPTY OR FILL) **********************************************)
-
-definition booleanize: bool → subterms → subterms ≝
- λb,F. {b}⇑⇓F.
-
-interpretation "make boolean (subterms)"
- 'ProjectSame b F = (booleanize b F).
-
-notation "hvbox( { term 46 b } ⇕ break term 46 F)"
- non associative with precedence 46
- for @{ 'ProjectSame $b $F }.
-
-lemma booleanize_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 booleanize_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 booleanize_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-.
-(*
-lemma booleanize_lift: ∀b,h,F,d. {b}⇕ ↑[d, h] F = ↑[d, h] {b}⇕ F.
-#b #h #M elim M -M normalize //
-qed.
-
-lemma booleanize_dsubst: ∀b,G,F,d. {b}⇕ [d ↙ G] F = [d ↙ {b}⇕ G] {b}⇕ F.
-#b #N #M elim M -M [2,3: normalize // ]
-*)
--- /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/carrier.ma".
+include "subterms/boolean.ma".
+
+(* BOOLEANIZED SUBSET (EMPTY OR FULL) **************************************)
+
+definition booleanized: bool → subterms → subterms ≝
+ λb,F. {b}⇑⇓F.
+
+interpretation "make boolean (subterms)"
+ 'ProjectSame b F = (booleanized b F).
+
+notation "hvbox( { term 46 b } ⇕ break term 46 F)"
+ non associative with precedence 46
+ for @{ 'ProjectSame $b $F }.
+
+lemma booleanized_inv_vref: ∀j,c,b,F. {b}⇕ F = {c}#j →
+ ∃∃b1. b = c & F = {b1}#j.
+#j #c #b #F #H
+elim (boolean_inv_vref … H) -H #H0 #H
+elim (carrier_inv_vref … H) -H /2 width=2/
+qed-.
+
+lemma booleanized_inv_abst: ∀U,c,b,F. {b}⇕ F = {c}𝛌.U →
+ ∃∃b1,T. b = c & {b}⇕T = U & F = {b1}𝛌.T.
+#U #c #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 booleanized_inv_appl: ∀W,U,c,b,F. {b}⇕ F = {c}@W.U →
+ ∃∃b1,V,T. b = c & {b}⇕V = W & {b}⇕T = U & F = {b1}@V.T.
+#W #U #c #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-.
+
+lemma booleanized_booleanized: ∀c,b,F. {b}⇕ {c}⇕ F = {b}⇕ F.
+normalize //
+qed.
+
+lemma booleanized_lift: ∀b,h,F,d. {b}⇕ ↑[d, h] F = ↑[d, h] {b}⇕ F.
+normalize //
+qed.
+
+lemma booleanized_dsubst: ∀b,G,F,d. {b}⇕ [d ↙ G] F = [d ↙ {b}⇕ G] {b}⇕ F.
+normalize //
+qed.
>sdsubst_sdsubst_ge in ⊢ (???%); /2 width=1/ <plus_minus_m_m //
qed.
+definition sdsubstable_f_dx: ∀S:Type[0]. (S → ?) → predicate (relation subterms) ≝ λS,f,R.
+ ∀G,F1,F2. R F1 F2 → ∀d. R ([d ↙ (f G)] F1) ([d ↙ (f G)] F2).
+
+lemma lstar_sdsubstable_f_dx: ∀S1,f,S2,R. (∀a. sdsubstable_f_dx S1 f (R a)) →
+ ∀l. sdsubstable_f_dx S1 f (lstar S2 … R l).
+#S1 #f #S2 #R #HR #l #G #F1 #F2 #H
+@(lstar_ind_l ????????? H) -l -F1 // /3 width=3/
+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.
-lemma slift_inv_vref_lt: ∀b0,j,d. j < d → ∀h,E. ↑[d, h] E = {b0}#j → E = {b0}#j.
-#b0 #j #d #Hjd #h * normalize
+lemma slift_inv_vref_lt: ∀c,j,d. j < d → ∀h,E. ↑[d, h] E = {c}#j → E = {c}#j.
+#c #j #d #Hjd #h * normalize
[ #b #i elim (lt_or_eq_or_gt i d) #Hid
[ >(tri_lt ???? … Hid) -Hid -Hjd //
| #H destruct >tri_eq in Hjd; #H
]
qed.
-lemma slift_inv_vref_ge: ∀b0,j,d. d ≤ j → ∀h,E. ↑[d, h] E = {b0}#j →
- d + h ≤ j ∧ E = {b0}#(j-h).
-#b0 #j #d #Hdj #h * normalize
+lemma slift_inv_vref_ge: ∀c,j,d. d ≤ j → ∀h,E. ↑[d, h] E = {c}#j →
+ d + h ≤ j ∧ E = {c}#(j-h).
+#c #j #d #Hdj #h * normalize
[ #b #i elim (lt_or_eq_or_gt i d) #Hid
[ >(tri_lt ???? … Hid) #H destruct
lapply (le_to_lt_to_lt … Hdj Hid) -Hdj -Hid #H
]
qed-.
-lemma slift_inv_vref_be: ∀b0,j,d,h. d ≤ j → j < d + h → ∀E. ↑[d, h] E = {b0}#j → ⊥.
-#b0 #j #d #h #Hdj #Hjdh #E #H elim (slift_inv_vref_ge … H) -H // -Hdj #Hdhj #_ -E
+lemma slift_inv_vref_be: ∀c,j,d,h. d ≤ j → j < d + h → ∀E. ↑[d, h] E = {c}#j → ⊥.
+#c #j #d #h #Hdj #Hjdh #E #H elim (slift_inv_vref_ge … H) -H // -Hdj #Hdhj #_ -E
lapply (lt_to_le_to_lt … Hjdh Hdhj) -d -h #H
elim (lt_refl_false … H)
qed-.
-lemma slift_inv_vref_ge_plus: ∀b0,j,d,h. d + h ≤ j →
- ∀E. ↑[d, h] E = {b0}#j → E = {b0}#(j-h).
-#b0 #j #d #h #Hdhj #E #H elim (slift_inv_vref_ge … H) -H // -E /2 width=2/
+lemma slift_inv_vref_ge_plus: ∀c,j,d,h. d + h ≤ j →
+ ∀E. ↑[d, h] E = {c}#j → E = {c}#(j-h).
+#c #j #d #h #Hdhj #E #H elim (slift_inv_vref_ge … H) -H // -E /2 width=2/
qed.
-lemma slift_inv_abst: ∀b0,U,d,h,E. ↑[d, h] E = {b0}𝛌.U →
- ∃∃T. ↑[d+1, h] T = U & E = {b0}𝛌.T.
-#b0 #U #d #h * normalize
+lemma slift_inv_abst: ∀c,U,d,h,E. ↑[d, h] E = {c}𝛌.U →
+ ∃∃T. ↑[d+1, h] T = U & E = {c}𝛌.T.
+#c #U #d #h * normalize
[ #b #i #H destruct
| #b #T #H destruct /2 width=3/
| #b #V #T #H destruct
]
qed-.
-lemma slift_inv_appl: ∀b0,W,U,d,h,E. ↑[d, h] E = {b0}@W.U →
- ∃∃V,T. ↑[d, h] V = W & ↑[d, h] T = U & E = {b0}@V.T.
-#b0 #W #U #d #h * normalize
+lemma slift_inv_appl: ∀c,W,U,d,h,E. ↑[d, h] E = {c}@W.U →
+ ∃∃V,T. ↑[d, h] V = W & ↑[d, h] T = U & E = {c}@V.T.
+#c #W #U #d #h * normalize
[ #b #i #H destruct
| #b #T #H destruct
| #b #V #T #H destruct /2 width=5/
(* SUBSETS OF SUBTERMS ******************************************************)
-(* Policy: boolean marks metavariables: b
+(* Policy: boolean marks metavariables: b,c
subterms metavariables: F,G,T,U,V,W
*)
(* Note: each subterm is marked with true if it belongs to the subset *)
]
] qed.
+(**************************** Allr ******************************)
+
let rec Allr (A:Type[0]) (R:relation A) (l:list A) on l : Prop ≝
match l with
[ nil ⇒ True
| cons a1 l ⇒ match l with [ nil ⇒ True | cons a2 _ ⇒ R a1 a2 ∧ Allr A R l ]
].
+lemma Allr_fwd_append_sn: ∀A,R,l1,l2. Allr A R (l1@l2) → Allr A R l1.
+#A #R #l1 elim l1 -l1 // #a1 * // #a2 #l1 #IHl1 #l2 * /3 width=2/
+qed-.
+
(**************************** Exists *******************************)
let rec Exists (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝
projects / helm.git / commitdiff