(* *)
(**************************************************************************)
-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/
projects / helm.git / blobdiff