right associative with precedence 47
for @{'ho_cons $a $l}.
+lemma map_cons_inv_nil: ∀A,a,l1. map_cons A a l1 = ◊ → ◊ = l1.
+#A #a * // normalize #a1 #l1 #H destruct
+qed-.
+
+lemma map_cons_inv_cons: ∀A,a,a2,l2,l1. map_cons A a l1 = a2::l2 →
+ ∃∃a1,l. a::a1 = a2 & a:::l = l2 & a1::l = l1.
+#A #a #a2 #l2 * normalize
+[ #H destruct
+| #a1 #l1 #H destruct /2 width=5/
+]
+qed-.
+
+lemma map_cons_append: ∀A,a,l1,l2. map_cons A a (l1@l2) =
+ map_cons A a l1 @ map_cons A a l2.
+#A #a #l1 elim l1 -l1 // normalize /2 width=1/
+qed.
+
(* lstar *)
(* Note: this cannot be in lib because of the missing xoa quantifier *)
lemma lstar_inv_pos: ∀A,B,R,l,b1,b2. lstar A B R l b1 b2 → 0 < |l| →
∃∃a,ll,b. a::ll = l & R a b1 b & lstar A B R ll b b2.
#A #B #R #l #b1 #b2 #H @(lstar_ind_l ????????? H) -b1
-[ #H elim (lt_refl_false … H)
+[ #H elim (lt_refl_false … H)
| #a #ll #b1 #b #Hb1 #Hb2 #_ #_ /2 width=6/ (**) (* auto fail if we do not remove the inductive premise *)
]
qed-.
include "basics/pts.ma".
+(* multiple existental quantifier (1, 2) *)
+
+inductive ex1_2 (A0,A1:Type[0]) (P0:A0→A1→Prop) : Prop ≝
+ | ex1_2_intro: ∀x0,x1. P0 x0 x1 → ex1_2 ? ? ?
+.
+
+interpretation "multiple existental quantifier (1, 2)" 'Ex P0 = (ex1_2 ? ? P0).
+
(* multiple existental quantifier (2, 2) *)
inductive ex2_2 (A0,A1:Type[0]) (P0,P1:A0→A1→Prop) : Prop ≝
(* This file was generated by xoa.native: do not edit *********************)
+(* multiple existental quantifier (1, 2) *)
+
+notation > "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}.λ${ident x1}.$P0) }.
+
+notation < "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) }.
+
(* multiple existental quantifier (2, 2) *)
notation > "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1)"
/2 width=1 by lstar_inv_pos/
qed-.
+lemma pl_sts_inv_rc_abst_dx: ∀b2,s,F1,T2. F1 Ⓡ↦*[s] {b2}𝛌.T2 → ∀r. rc:::r = s →
+ ∃∃b1,T1. T1 Ⓡ↦*[r] T2 & {b1}𝛌.T1 = F1.
+#b2 #s #F1 #T2 #H @(lstar_ind_l … s F1 H) -s -F1
+[ #r #H lapply (map_cons_inv_nil … r H) -H #H destruct /2 width=4/
+| #p #s #F1 #F #HF1 #_ #IHF2 #r #H -b2
+ elim (map_cons_inv_cons … r H) -H #q #r0 #Hp #Hs #Hr
+ elim (pl_st_inv_rc … HF1 … Hp) -HF1 -p #b1 #T1 #T #HT1 #HF1 #HF destruct
+ elim (IHF2 ??) -IHF2 [3: // |2: skip ] (**) (* simplify line *)
+ #b0 #T0 #HT02 #H destruct
+ lapply (pl_sts_step_sn … HT1 … HT02) -T /2 width=4/
+]
+qed-.
+
lemma pl_sts_lift: ∀s. sliftable (pl_sts s).
/2 width=1/
qed.
/2 width=3 by lstar_ltransitive/
qed-.
+theorem pl_sts_inv_trans: inv_ltransitive … pl_sts.
+/2 width=3 by lstar_inv_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
lapply (pl_st_fwd_sle … HF13 … HF34) -F1 -F4 /3 width=3/
qed-.
+lemma pl_sts_fwd_abst_dx: ∀b2,s,F1,T2. F1 Ⓡ↦*[s] {b2}𝛌.T2 →
+ (∃r2. rc:::r2 = s) ∨ ∃∃r1,r2. r1@◊::rc:::r2 = s.
+#b2 #s #F1 #T2 #H
+lapply (pl_sts_fwd_is_standard … H)
+@(lstar_ind_l … s F1 H) -s -F1
+[ #_ @or_introl @(ex_intro … ◊) // (**) (* auto needs some help here *)
+| * [ | * #p ] #s #F1 #F #HF1 #HF #IHF #Hs
+ lapply (is_standard_fwd_cons … Hs) #H
+ elim (IHF H) -IHF -H * [2,4,6,8: #r1 ] #r2 #H destruct
+(* case 1: ◊, @ *)
+ [ -Hs -F1 -F -T2 -b2
+ @or_intror @(ex1_2_intro … (◊::r1) r2) // (**) (* auto needs some help here *)
+(* case 2: rc, @ *)
+ | -F1 -F -T2 -b2
+ lapply (is_standard_fwd_sle … Hs) -Hs #H
+ lapply (sle_nil_inv_in_whd … H) -H * #H #_ destruct
+(* case 3: sn, @ *)
+ | -F1 -F -T2 -b2
+ lapply (is_standard_fwd_sle … Hs) -Hs #H
+ lapply (sle_nil_inv_in_whd … H) -H * #H #_ destruct
+(* case 4: dx, @ *)
+ | -Hs -F1 -F -T2 -b2
+ @or_intror @(ex1_2_intro … ((dx::p)::r1) r2) // (**) (* auto needs some help here *)
+(* case 5: ◊, no @ *)
+ | -Hs -F1 -F -T2 -b2
+ @or_intror @(ex1_2_intro … ◊ r2) // (**) (* auto needs some help here *)
+(* case 6, rc, no @ *)
+ | -Hs -F1 -F -T2 -b2
+ @or_introl @(ex_intro … (p::r2)) // (**) (* auto needs some help here *)
+(* case 7: sn, no @ *)
+ | elim (pl_sts_inv_rc_abst_dx … HF ??) -b2 [3: // |2: skip ] (**) (* simplify line *)
+ #b #T #_ #HT -Hs -T2
+ elim (pl_st_inv_sn … HF1 ??) -HF1 [3: // |2: skip ] (**) (* simplify line *)
+ #c #V1 #V #T0 #_ #_ #HT0 -c -V1 -F1 destruct
+(* case 8: dx, no @ *)
+ | elim (pl_sts_inv_rc_abst_dx … HF ??) -b2 [3: // |2: skip ] (**) (* simplify line *)
+ #b #T #_ #HT -Hs -T2
+ elim (pl_st_inv_dx … HF1 ??) -HF1 [3: // |2: skip ] (**) (* simplify line *)
+ #c #V #T1 #T0 #_ #_ #HT0 -T1 -F1 destruct
+ ]
+]
+qed-.
+
+lemma pl_sts_fwd_abst_dx_is_whd: ∀b2,s,F1,T2. F1 Ⓡ↦*[s] {b2}𝛌.T2 →
+ ∃∃r1,r2. is_whd r1 & r1@rc:::r2 = s.
+#b2 #s #F1 #T2 #H
+lapply (pl_sts_fwd_is_standard … H)
+elim (pl_sts_fwd_abst_dx … H) -b2 -F1 -T2 * [ | #r1 ] #r2 #Hs destruct
+[ #_ @(ex2_2_intro … ◊ r2) //
+| <(associative_append … r1 (◊::◊) (rc:::r2)) #Hs
+ lapply (is_standard_fwd_append_sn … Hs) -Hs #H
+ lapply (is_standard_fwd_is_whd … H) -H // /4 width=4/
+]
+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::◊)) →
>carrier_boolean in HF; #H destruct normalize /2 width=3/
| #p #A1 #A2 #_ #IHA12 #F #HF #s #M1 #HM1 #Hs
elim (carrier_inv_abst … HF) -HF #b #T #HT #HF destruct
+ elim (pl_sts_fwd_abst_dx_is_whd … HM1) #r1 #r2 #Hr1 #H destruct
+ elim (pl_sts_inv_trans … HM1) -HM1 #F0 #HM1 #HT
+ elim (pl_sts_inv_pl_sreds … HM1 ?) // #M0 #_ #H -M1 -Hr1 destruct
+ elim (pl_sts_inv_rc_abst_dx … HT ??) -HT [3: // |2: skip ] #b0 #T0 #HT02 #H (**) (* simplify line *)
+ elim (boolean_inv_abst … (sym_eq … H)) -H #A0 #_ #H #_ -b0 -M0 destruct
+ >associative_append in Hs; #Hs
+ lapply (is_standard_fwd_append_dx … Hs) -r1
+ <(map_cons_append … r2 (p::◊)) #H
+ lapply (is_standard_inv_compatible_rc … H) -H #H
+ elim (IHA12 … HT02 ?) // -r2 -A0 -IHA12 #F2 #HF2 #H
+ @(ex2_intro … ({⊥}𝛌.F2)) normalize // /2 width=1/ (**) (* auto needs some help here *)
(*
elim (carrier_inv_appl … HF) -HF #b1 #V #G #HV #HG #HF
*)
]
qed-.
+lemma sle_inv_rc: ∀p,q. p ≤ q → ∀p0. rc::p0 = p →
+ (∃∃q0. p0 ≤ q0 & rc::q0 = q) ∨
+ ∃q0. sn::q0 = q.
+#p #q #H elim H -q /3 width=3/
+#q #q0 #_ #Hq0 #IHpq #p0 #H destruct
+elim (IHpq p0 ?) -IHpq // *
+[ #p1 #Hp01 #H
+ elim (sprec_inv_rc … Hq0 … H) -q * /3 width=3/ /4 width=3/
+| #p1 #H elim (sprec_inv_sn … Hq0 … H) -q /3 width=2/
+]
+qed-.
+
lemma sle_inv_sn: ∀p,q. p ≤ q → ∀p0. sn::p0 = p →
∃∃q0. p0 ≤ q0 & sn::q0 = q.
#p #q #H elim H -q /2 width=3/
]
qed-.
+lemma sprec_inv_rc: ∀p,q. p ≺ q → ∀p0. rc::p0 = p →
+ (∃∃q0. p0 ≺ q0 & rc::q0 = q) ∨
+ ∃q0. sn::q0 = q.
+#p #q * -p -q
+[ #o #q #p0 #H destruct
+| #p #q #p0 #H destruct
+| #p #q #p0 #H destruct /3 width=2/
+| #o #p #q #Hpq #p0 #H destruct /3 width=3/
+| #p0 #H destruct
+]
+qed-.
+
+lemma sprec_inv_comp: ∀p1,p2. p1 ≺ p2 →
+ ∀o,q1,q2. o::q1 = p1 → o::q2 = p2 → q1 ≺ q2.
+#p1 #p2 * -p1 -p2
+[ #o #q #o0 #q1 #q2 #H destruct
+| #p #q #o0 #q1 #q2 #H1 #H2 destruct
+| #p #q #o0 #q1 #q2 #H1 #H2 destruct
+| #o #p #q #Hpq #o0 #q1 #q2 #H1 #H2 destruct //
+| #o0 #q1 #q2 #_ #H destruct
+]
+qed-.
+
lemma sprec_fwd_in_whd: ∀p,q. p ≺ q → in_whd q → in_whd p.
#p #q #H elim H -p -q // /2 width=1/
[ #p #q * #H destruct
/2 width=2 by Allr_fwd_cons/
qed-.
+lemma is_standard_fwd_append_dx: ∀s,r. is_standard (s@r) → is_standard r.
+/2 width=2 by Allr_fwd_append_dx/
+qed-.
+
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/
#q #r #IHr * /3 width=1/
qed.
+lemma is_standard_inv_compatible_sn: ∀s. is_standard (sn:::s) → is_standard s.
+#s elim s -s // #a1 * // #a2 #s #IHs * #H
+elim (sle_inv_sn … H ??) -H [3: // |2: skip ] (**) (* simplify line *)
+#a #Ha1 #H destruct /3 width=1/
+qed-.
+
+lemma is_standard_inv_compatible_rc: ∀s. is_standard (rc:::s) → is_standard s.
+#s elim s -s // #a1 * // #a2 #s #IHs * #H
+elim (sle_inv_rc … H ??) -H [4: // |2: skip ] * (**) (* simplify line *)
+[ #a #Ha1 #H destruct /3 width=1/
+| #a #H destruct
+]
+qed-.
+
lemma is_standard_fwd_sle: ∀s2,p2,s1,p1. is_standard ((p1::s1)@(p2::s2)) → p1 ≤ p2.
#s2 #p2 #s1 elim s1 -s1
[ #p1 * //
<key name="objects">xoa</key>
<key name="notations">xoa_notation</key>
<key name="include">basics/pts.ma</key>
+ <key name="ex">1 2</key>
<key name="ex">2 2</key>
<key name="ex">2 3</key>
<key name="ex">3 1</key>
#A #R #a * // #a0 #l * //
qed-.
+lemma Allr_fwd_append_dx: ∀A,R,l1,l2. Allr A R (l1@l2) → Allr A R l2.
+#A #R #l1 elim l1 -l1 // #a1 #l1 #IHl1 #l2 #H
+lapply (Allr_fwd_cons … (l1@l2) H) -H /2 width=1/
+qed-.
+
(**************************** Exists *******************************)
let rec Exists (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝
include "basics/lists/list.ma".
-(* labelled reflexive and transitive closure ********************************)
+(* labeled reflexive and transitive closure *********************************)
definition ltransitive: ∀A,B:Type[0]. predicate (list A → relation B) ≝ λA,B,R.
∀l1,b1,b. R l1 b1 b → ∀l2,b2. R l2 b b2 → R (l1@l2) b1 b2.
+definition inv_ltransitive: ∀A,B:Type[0]. predicate (list A → relation B) ≝
+ λA,B,R. ∀l1,l2,b1,b2. R (l1@l2) b1 b2 →
+ ∃∃b. R l1 b1 b & R l2 b b2.
+
inductive lstar (A:Type[0]) (B:Type[0]) (R: A→relation B): list A → relation B ≝
| lstar_nil : ∀b. lstar A B R ([]) b b
| lstar_cons: ∀a,b1,b. R a b1 b →
#A #B #R #l1 #b1 #b #H @(lstar_ind_l ????????? H) -l1 -b1 normalize // /3 width=3/
qed-.
+lemma lstar_inv_ltransitive: ∀A,B,R. inv_ltransitive … (lstar A B R).
+#A #B #R #l1 elim l1 -l1 normalize /2 width=3/
+#a #l1 #IHl1 #l2 #b1 #b2 #H
+elim (lstar_inv_cons … b2 H ???) -H [4: // |2,3: skip ] #b #Hb1 #Hb2 (**) (* simplify line *)
+elim (IHl1 … Hb2) -IHl1 -Hb2 /3 width=3/
+qed-.
+
lemma lstar_app: ∀A,B,R,l,b1,b. lstar A B R l b1 b → ∀a,b2. R a b b2 →
lstar A B R (l@[a]) b1 b2.
#A #B #R #l #b1 #b #H @(lstar_ind_l ????????? H) -l -b1 /2 width=1/
projects / helm.git / commitdiff