definition dsubstable_dx: predicate (relation term) ≝ λR.
∀D,M1,M2. R M1 M2 → ∀d. R ([d ⬐ D] M1) ([d ⬐ D] M2).
+
+definition dsubstable_sn: predicate (relation term) ≝ λR.
+ ∀D1,D2. R D1 D2 → ∀M,d. R ([d ⬐ D1] M) ([d ⬐ D2] M).
+
+definition dsubstable: predicate (relation term) ≝ λR.
+ ∀D1,D2. R D1 D2 → ∀M1,M2. R M1 M2 → ∀d. R ([d ⬐ D1] M1) ([d ⬐ D2] M2).
| Appl B A ⇒ (mult B) + (mult A)
].
-interpretation "multiplicity"
+interpretation "term multiplicity"
'Multiplicity M = (mult M).
notation "hvbox( #{ term 46 M } )"
qed.
lemma mult_lift: ∀h,M,d. #{↑[d, h] M} = #{M}.
-#H #M elim M -M normalize //
+#h #M elim M -M normalize //
qed.
-theorem mult_dsubst: ∀C,M,d. #{[d ⬐ C] M} ≤ #{M} * #{C}.
-#C #M elim M -M
+theorem mult_dsubst: ∀D,M,d. #{[d ⬐ D] M} ≤ #{M} * #{D}.
+#D #M elim M -M
[ #i #d elim (lt_or_eq_or_gt i d) #Hid
[ >(dsubst_vref_lt … Hid) normalize //
| destruct >dsubst_vref_eq normalize //
(* *)
(**************************************************************************)
-include "multiplicity.ma".
+include "size.ma".
+include "labelled_sequential_reduction.ma".
(* PARALLEL REDUCTION (SINGLE STEP) *****************************************)
]
qed-.
+lemma pred_inv_appl: ∀M,N. M ⥤ N → ∀B,A. @B.A = M →
+ (∃∃D,C. B ⥤ D & A ⥤ C & @D.C = N) ∨
+ ∃∃A0,D,C0. B ⥤ D & A0 ⥤ C0 & 𝛌.A0 = A & [⬐D]C0 = N.
+#M #N * -M -N
+[ #i #B0 #A0 #H destruct
+| #A #C #_ #B0 #A0 #H destruct
+| #B #D #A #C #HBD #HAC #B0 #A0 #H destruct /3 width=5/
+| #B #D #A #C #HBD #HAC #B0 #A0 #H destruct /3 width=7/
+]
+qed-.
+
lemma pred_lift: liftable pred.
#h #M1 #M2 #H elim H -M1 -M2 normalize // /2 width=1/
#D #D #A #C #_ #_ #IHBD #IHAC #d <dsubst_lift_le // /2 width=1/
@(ex2_1_intro … ([⬐B2]A2)) /2 width=1/
]
qed-.
+
+lemma pred_dsubst: dsubstable pred.
+#N1 #N2 #HN12 #M1 #M2 #H elim H -M1 -M2
+[ #i #d elim (lt_or_eq_or_gt i d) #Hid
+ [ >(dsubst_vref_lt … Hid) >(dsubst_vref_lt … Hid) //
+ | destruct >dsubst_vref_eq >dsubst_vref_eq /2 width=1/
+ | >(dsubst_vref_gt … Hid) >(dsubst_vref_gt … Hid) //
+ ]
+| normalize /2 width=1/
+| normalize /2 width=1/
+| normalize #B #D #A #C #_ #_ #IHBD #IHAC #d
+ >dsubst_dsubst_ge // /2 width=1/
+]
+qed.
+
+lemma pred_conf1_vref: ∀i. confluent1 … pred (#i).
+#i #M1 #H1 #M2 #H2
+<(pred_inv_vref … H1) -H1 [3: // |2: skip ] (**) (* simplify line *)
+<(pred_inv_vref … H2) -H2 [3: // |2: skip ] (**) (* simplify line *)
+/2 width=3/
+qed-.
+
+lemma pred_conf1_abst: ∀A. confluent1 … pred A → confluent1 … pred (𝛌.A).
+#A #IH #M1 #H1 #M2 #H2
+elim (pred_inv_abst … H1 ??) -H1 [3: // |2: skip ] #A1 #HA1 #H destruct (**) (* simplify line *)
+elim (pred_inv_abst … H2 ??) -H2 [3: // |2: skip ] #A2 #HA2 #H destruct (**) (* simplify line *)
+elim (IH … HA1 … HA2) -A /3 width=3/
+qed-.
+
+lemma pred_conf1_appl_beta: ∀B,B1,B2,C,C2,M1.
+ (∀M0. |M0| < |B|+|𝛌.C|+1 → confluent1 ? pred M0) → (**) (* ? needed in place of … *)
+ B ⥤ B1 → B ⥤ B2 → 𝛌.C ⥤ M1 → C ⥤ C2 →
+ ∃∃M. @B1.M1 ⥤ M & [⬐B2]C2 ⥤ M.
+#B #B1 #B2 #C #C2 #M1 #IH #HB1 #HB2 #H1 #HC2
+elim (pred_inv_abst … H1 ??) -H1 [3: // |2: skip ] #C1 #HC1 #H destruct (**) (* simplify line *)
+elim (IH B … HB1 … HB2) -HB1 -HB2 //
+elim (IH C … HC1 … HC2) normalize // -B -C /3 width=5/
+qed-.
+
+theorem pred_conf: confluent … pred.
+#M @(f_ind … size … M) -M #n #IH * normalize
+[ /2 width=3 by pred_conf1_vref/
+| /3 width=4 by pred_conf1_abst/
+| #B #A #H #M1 #H1 #M2 #H2 destruct
+ elim (pred_inv_appl … H1 ???) -H1 [5: // |2,3: skip ] * (**) (* simplify line *)
+ elim (pred_inv_appl … H2 ???) -H2 [5,10: // |2,3,7,8: skip ] * (**) (* simplify line *)
+ [ #B2 #A2 #HB2 #HA2 #H2 #B1 #A1 #HB1 #HA1 #H1 destruct
+ elim (IH A … HA1 … HA2) -HA1 -HA2 //
+ elim (IH B … HB1 … HB2) // -A -B /3 width=5/
+ | #C #B2 #C2 #HB2 #HC2 #H2 #HM2 #B1 #N #HB1 #H #HM1 destruct
+ @(pred_conf1_appl_beta … IH) // (**) (* /2 width=7 by pred_conf1_appl_beta/ does not work *)
+ | #B2 #N #B2 #H #HM2 #C #B1 #C1 #HB1 #HC1 #H1 #HM1 destruct
+ @ex2_1_commute @(pred_conf1_appl_beta … IH) //
+ | #C #B2 #C2 #HB2 #HC2 #H2 #HM2 #C0 #B1 #C1 #HB1 #HC1 #H1 #HM1 destruct
+ elim (IH B … HB1 … HB2) -HB1 -HB2 //
+ elim (IH C … HC1 … HC2) normalize // -B -C /3 width=5/
+ ]
+]
+qed-.
+
+lemma lsred_pred: ∀p,M,N. M ⇀[p] N → M ⥤ N.
+#p #M #N #H elim H -p -M -N /2 width=1/
+qed.
include "xoa_notation.ma".
include "xoa.ma".
-(* Note: notation for nil not involving brackets *)
-notation > "◊"
- non associative with precedence 90
- for @{'nil}.
+(* logic *)
(* Note: For some reason this cannot be in the standard library *)
interpretation "logical false" 'false = False.
non associative with precedence 90
for @{'false}.
+lemma ex2_1_commute: ∀A0. ∀P0,P1:A0→Prop. (∃∃x0. P0 x0 & P1 x0) → ∃∃x0. P1 x0 & P0 x0.
+#A0 #P0 #P1 * /2 width=3/
+qed.
+
+(* relations *)
+
+definition confluent1: ∀A. relation A → predicate A ≝ λA,R,a0.
+ ∀a1. R a0 a1 → ∀a2. R a0 a2 →
+ ∃∃a. R a1 a & R a2 a.
+
+(* Note: confluent1 would be redundant if \Pi-reduction where enabled *)
+definition confluent: ∀A. predicate (relation A) ≝ λA,R.
+ ∀a0. confluent1 … R a0.
+
+(* arithmetics *)
+
lemma lt_refl_false: ∀n. n < n → ⊥.
#n #H elim (lt_to_not_eq … H) -H /2 width=1/
qed-.
| #n1 #IH #n2 elim n2 -n2 // /3 width=1/
]
qed.
+
+(* lists *)
+
+(* Note: notation for nil not involving brackets *)
+notation > "◊"
+ non associative with precedence 90
+ for @{'nil}.
--- /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 "lift.ma".
+
+(* SIZE *********************************************************************)
+
+(* Note: this gives the number of abstractions and applications in M *)
+let rec size M on M ≝ match M with
+[ VRef i ⇒ 0
+| Abst A ⇒ size A + 1
+| Appl B A ⇒ (size B) + (size A) + 1
+].
+
+interpretation "term size"
+ 'card M = (size M).
+
+lemma size_lift: ∀h,M,d. |↑[d, h] M| = |M|.
+#h #M elim M -M normalize //
+qed.
non associative with precedence 46
for @{ 'Abstraction $A }.
-notation > "hvbox( 𝛌 term 46 A )"
- non associative with precedence 46
- for @{ 'Abstraction $A }.
-
notation "hvbox( @ term 46 C . break term 46 A )"
non associative with precedence 46
for @{ 'Application $C $A }.
<key name="include">basics/pts.ma</key>
<key name="ex">2 1</key>
<key name="ex">3 2</key>
+ <key name="ex">4 3</key>
<key name="or">3</key>
</section>
</helm_registry>
interpretation "multiple existental quantifier (3, 2)" 'Ex P0 P1 P2 = (ex3_2 ? ? P0 P1 P2).
+(* multiple existental quantifier (4, 3) *)
+
+inductive ex4_3 (A0,A1,A2:Type[0]) (P0,P1,P2,P3:A0→A1→A2→Prop) : Prop ≝
+ | ex4_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → P2 x0 x1 x2 → P3 x0 x1 x2 → ex4_3 ? ? ? ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (4, 3)" 'Ex P0 P1 P2 P3 = (ex4_3 ? ? ? P0 P1 P2 P3).
+
(* multiple disjunction connective (3) *)
inductive or3 (P0,P1,P2:Prop) : Prop ≝
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) }.
+(* 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)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P3) }.
+
+notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 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.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P3) }.
+
(* multiple disjunction connective (3) *)
notation "hvbox(∨∨ term 29 P0 break | term 29 P1 break | term 29 P2)"
]
qed.
+lemma f_ind: ∀A. ∀f:A→ℕ. ∀P:predicate A.
+ (∀n. (∀a. f a < n → P a) → ∀a. f a = n → P a) → ∀a. P a.
+#A #f #P #H #a
+cut (∀n,a. f a = n → P a) /2 width=3/ -a
+#n @(nat_elim1 … n) -n #n /3 width=3/ (**) (* auto very slow (274s) without #n *)
+qed-.
+
(* More negated equalities **************************************************)
theorem lt_to_not_eq : ∀n,m:nat. n < m → n ≠ m.
projects / helm.git / commitdiff