MAC = mac.native
XOA_CONF = xoa.conf.xml
-XOA_TARGETS = xoa_notation.ma xoa.ma
+XOA_TARGETS = background/xoa_notation.ma background/xoa.ma
all: xoa
$(H)../../matitac.opt
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* GENERIC NOTATION *********************************************************)
+
+(* Note: this should go to core_notation *)
+notation "hvbox(a break βΊ b)"
+ non associative with precedence 45
+ for @{ 'prec $a $b }.
+
+notation "hvbox( # term 90 i )"
+ non associative with precedence 46
+ for @{ 'VariableReferenceByIndex $i }.
+
+notation "hvbox( { term 46 b } # break term 90 i )"
+ non associative with precedence 46
+ for @{ 'VariableReferenceByIndex $b $i }.
+
+notation "hvbox( π . term 46 A )"
+ non associative with precedence 46
+ for @{ 'Abstraction $A }.
+
+notation "hvbox( { term 46 b } π . break term 46 T)"
+ non associative with precedence 46
+ for @{ 'Abstraction $b $T }.
+
+notation "hvbox( @ term 46 C . break term 46 A )"
+ non associative with precedence 46
+ for @{ 'Application $C $A }.
+
+notation "hvbox( { term 46 b } @ break term 46 V . break term 46 T )"
+ non associative with precedence 46
+ for @{ 'Application $b $V $T }.
+
+notation "hvbox( β [ term 46 d , break term 46 h ] break term 46 M )"
+ non associative with precedence 46
+ for @{ 'Lift $h $d $M }.
+
+notation > "hvbox( β [ term 46 h ] break term 46 M )"
+ non associative with precedence 46
+ for @{ 'Lift $h 0 $M }.
+
+notation > "hvbox( β term 46 M )"
+ non associative with precedence 46
+ for @{ 'Lift 1 0 $M }.
+
+(* Note: the notation with "/" does not work *)
+notation "hvbox( [ term 46 d break β term 46 N ] break term 46 M )"
+ non associative with precedence 46
+ for @{ 'DSubst $N $d $M }.
+
+notation > "hvbox( [ β term 46 N ] break term 46 M )"
+ non associative with precedence 46
+ for @{ 'DSubst $N 0 $M }.
+
+(* Note: we do not use β since it is reserved by CIC *)
+notation "hvbox( M break β¦ term 46 N )"
+ non associative with precedence 45
+ for @{ 'SeqRed $M $N }.
+
+notation "hvbox( M break β¦ [ term 46 p ] break term 46 N )"
+ non associative with precedence 45
+ for @{ 'SeqRed $M $p $N }.
+
+notation "hvbox( M break β¦* term 46 N )"
+ non associative with precedence 45
+ for @{ 'SeqRedStar $M $N }.
+
+notation "hvbox( M break β¦* [ term 46 s ] break term 46 N )"
+ non associative with precedence 45
+ for @{ 'SeqRedStar $M $s $N }.
+
+notation "hvbox( M break β€ term 46 N )"
+ non associative with precedence 45
+ for @{ 'ParRed $M $N }.
+
+notation "hvbox( M break β€* term 46 N )"
+ non associative with precedence 45
+ for @{ 'ParRedStar $M $N }.
--- /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 "basics/star.ma".
+include "basics/lists/lstar.ma".
+include "arithmetics/exp.ma".
+
+include "background/xoa_notation.ma".
+include "background/xoa.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}.
+
+(* arithmetics *)
+
+lemma lt_refl_false: βn. n < n β β₯.
+#n #H elim (lt_to_not_eq β¦ H) -H /2 width=1/
+qed-.
+
+lemma lt_zero_false: βn. n < 0 β β₯.
+#n #H elim (lt_to_not_le β¦ H) -H /2 width=1/
+qed-.
+
+lemma plus_lt_false: βm,n. m + n < m β β₯.
+#m #n #H elim (lt_to_not_le β¦ H) -H /2 width=1/
+qed-.
+
+lemma lt_or_eq_or_gt: βm,n. β¨β¨ m < n | n = m | n < m.
+#m #n elim (lt_or_ge m n) /2 width=1/
+#H elim H -m /2 width=1/
+#m #Hm * #H /2 width=1/ /3 width=1/
+qed-.
+
+(* trichotomy operator *)
+
+(* Note: this is "if eqb n1 n2 then a2 else if leb n1 n2 then a1 else a3" *)
+let rec tri (A:Type[0]) n1 n2 a1 a2 a3 on n1 : A β
+ match n1 with
+ [ O β match n2 with [ O β a2 | S n2 β a1 ]
+ | S n1 β match n2 with [ O β a3 | S n2 β tri A n1 n2 a1 a2 a3 ]
+ ].
+
+lemma tri_lt: βA,a1,a2,a3,n2,n1. n1 < n2 β tri A n1 n2 a1 a2 a3 = a1.
+#A #a1 #a2 #a3 #n2 elim n2 -n2
+[ #n1 #H elim (lt_zero_false β¦ H)
+| #n2 #IH #n1 elim n1 -n1 // /3 width=1/
+]
+qed.
+
+lemma tri_eq: βA,a1,a2,a3,n. tri A n n a1 a2 a3 = a2.
+#A #a1 #a2 #a3 #n elim n -n normalize //
+qed.
+
+lemma tri_gt: βA,a1,a2,a3,n1,n2. n2 < n1 β tri A n1 n2 a1 a2 a3 = a3.
+#A #a1 #a2 #a3 #n1 elim n1 -n1
+[ #n2 #H elim (lt_zero_false β¦ H)
+| #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}.
+
+definition map_cons: βA. A β list (list A) β list (list A) β Ξ»A,a.
+ map β¦ (cons β¦ a).
+
+interpretation "map_cons" 'ho_cons a l = (map_cons ? a l).
+
+notation "hvbox(a ::: break l)"
+ right associative with precedence 47
+ for @{'ho_cons $a $l}.
+
+(* 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)
+| #a #ll #b1 #b #Hb1 #Hb2 #_ #_ /2 width=6/ (**) (* auto fail if we do not remove the inductive premise *)
+]
+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 *)
+(* *)
+(**************************************************************************)
+
+(* This file was generated by xoa.native: do not edit *********************)
+
+include "basics/pts.ma".
+
+(* multiple existental quantifier (2, 2) *)
+
+inductive ex2_2 (A0,A1:Type[0]) (P0,P1:A0βA1βProp) : Prop β
+ | ex2_2_intro: βx0,x1. P0 x0 x1 β P1 x0 x1 β ex2_2 ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (2, 2)" 'Ex P0 P1 = (ex2_2 ? ? P0 P1).
+
+(* multiple existental quantifier (2, 3) *)
+
+inductive ex2_3 (A0,A1,A2:Type[0]) (P0,P1:A0βA1βA2βProp) : Prop β
+ | ex2_3_intro: βx0,x1,x2. P0 x0 x1 x2 β P1 x0 x1 x2 β ex2_3 ? ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (2, 3)" 'Ex P0 P1 = (ex2_3 ? ? ? P0 P1).
+
+(* multiple existental quantifier (3, 2) *)
+
+inductive ex3_2 (A0,A1:Type[0]) (P0,P1,P2:A0βA1βProp) : Prop β
+ | ex3_2_intro: βx0,x1. P0 x0 x1 β P1 x0 x1 β P2 x0 x1 β ex3_2 ? ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (3, 2)" 'Ex P0 P1 P2 = (ex3_2 ? ? P0 P1 P2).
+
+(* multiple existental quantifier (3, 3) *)
+
+inductive ex3_3 (A0,A1,A2:Type[0]) (P0,P1,P2:A0βA1βA2βProp) : Prop β
+ | ex3_3_intro: βx0,x1,x2. P0 x0 x1 x2 β P1 x0 x1 x2 β P2 x0 x1 x2 β ex3_3 ? ? ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (3, 3)" 'Ex P0 P1 P2 = (ex3_3 ? ? ? 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 β
+ | or3_intro0: P0 β or3 ? ? ?
+ | or3_intro1: P1 β or3 ? ? ?
+ | or3_intro2: P2 β or3 ? ? ?
+.
+
+interpretation "multiple disjunction connective (3)" 'Or P0 P1 P2 = (or3 P0 P1 P2).
+
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* This file was generated by xoa.native: do not edit *********************)
+
+(* multiple existental quantifier (2, 2) *)
+
+notation > "hvbox(ββ ident x0 , ident x1 break . term 19 P0 break & term 19 P1)"
+ non associative with precedence 20
+ for @{ 'Ex (Ξ»${ident x0}.Ξ»${ident x1}.$P0) (Ξ»${ident x0}.Ξ»${ident x1}.$P1) }.
+
+notation < "hvbox(ββ ident x0 , ident x1 break . term 19 P0 break & term 19 P1)"
+ non associative with precedence 20
+ for @{ 'Ex (Ξ»${ident x0}:$T0.Ξ»${ident x1}:$T1.$P0) (Ξ»${ident x0}:$T0.Ξ»${ident x1}:$T1.$P1) }.
+
+(* multiple existental quantifier (2, 3) *)
+
+notation > "hvbox(ββ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1)"
+ non associative with precedence 20
+ for @{ 'Ex (Ξ»${ident x0}.Ξ»${ident x1}.Ξ»${ident x2}.$P0) (Ξ»${ident x0}.Ξ»${ident x1}.Ξ»${ident x2}.$P1) }.
+
+notation < "hvbox(ββ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1)"
+ 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, 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}.Ξ»${ident x1}.$P0) (Ξ»${ident x0}.Ξ»${ident x1}.$P1) (Ξ»${ident x0}.Ξ»${ident x1}.$P2) }.
+
+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.$P0) (Ξ»${ident x0}:$T0.Ξ»${ident x1}:$T1.$P1) (Ξ»${ident x0}:$T0.Ξ»${ident x1}:$T1.$P2) }.
+
+(* multiple existental quantifier (3, 3) *)
+
+notation > "hvbox(ββ ident x0 , ident x1 , ident x2 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}.$P0) (Ξ»${ident x0}.Ξ»${ident x1}.Ξ»${ident x2}.$P1) (Ξ»${ident x0}.Ξ»${ident x1}.Ξ»${ident x2}.$P2) }.
+
+notation < "hvbox(ββ ident x0 , ident x1 , ident x2 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 (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)"
+ non associative with precedence 30
+ for @{ 'Or $P0 $P1 $P2 }.
+
+++ /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 *)
-(* *)
-(**************************************************************************)
-
-(* GENERIC NOTATION *********************************************************)
-
-notation "hvbox( # term 90 i )"
- non associative with precedence 46
- for @{ 'VariableReferenceByIndex $i }.
-
-notation "hvbox( { term 46 b } # break term 90 i )"
- non associative with precedence 46
- for @{ 'VariableReferenceByIndex $b $i }.
-
-notation "hvbox( π . term 46 A )"
- non associative with precedence 46
- for @{ 'Abstraction $A }.
-
-notation "hvbox( { term 46 b } π . break term 46 T)"
- non associative with precedence 46
- for @{ 'Abstraction $b $T }.
-
-notation "hvbox( @ term 46 C . break term 46 A )"
- non associative with precedence 46
- for @{ 'Application $C $A }.
-
-notation "hvbox( { term 46 b } @ break term 46 V . break term 46 T )"
- non associative with precedence 46
- for @{ 'Application $b $V $T }.
-
-notation "hvbox( β [ term 46 d , break term 46 h ] break term 46 M )"
- non associative with precedence 46
- for @{ 'Lift $h $d $M }.
-
-notation > "hvbox( β [ term 46 h ] break term 46 M )"
- non associative with precedence 46
- for @{ 'Lift $h 0 $M }.
-
-notation > "hvbox( β term 46 M )"
- non associative with precedence 46
- for @{ 'Lift 1 0 $M }.
-
-(* Note: the notation with "/" does not work *)
-notation "hvbox( [ term 46 d β break term 46 N ] break term 46 M )"
- non associative with precedence 46
- for @{ 'DSubst $N $d $M }.
-
-notation > "hvbox( [ β term 46 N ] break term 46 M )"
- non associative with precedence 46
- for @{ 'DSubst $N 0 $M }.
-
\ No newline at end of file
--- /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/trace.ma".
+
+(* DECOMPOSED TRACE *********************************************************)
+
+(* Policy: decomposed trace metavariables: P, Q *)
+(* Note: this is a binary tree on traces *)
+inductive dtrace: Type[0] β
+| tree_nil : dtrace
+| tree_cons: trace β dtrace β dtrace β dtrace
+.
+
+let rec size (P:dtrace) on P β match P with
+[ tree_nil β 0
+| tree_cons s Q1 Q2 β size Q2 + size Q1 + |s|
+].
+
+interpretation "decomposed trace size" 'card P = (size P).
--- /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".
+
+(* DECOMPOSED STANDARD COMPUTATION ***********************************************)
+
+(* Note: this is the "standard" computation of:
+ R. Kashima: "A proof of the Standization Theorem in Ξ»-Calculus". (2000).
+*)
+inductive dst: relation term β
+| dst_vref: βs,M,i. is_whd s β M β¦*[s] #i β dst M (#i)
+| dst_abst: βs,M,A1,A2. is_whd s β M β¦*[s] π.A1 β dst A1 A2 β dst M (π.A2)
+| dst_appl: βs,M,B1,B2,A1,A2. is_whd s β M β¦*[s] @B1.A1 β dst B1 B2 β dst A1 A2 β dst M (@B2.A2)
+.
+
+interpretation "decomposed standard computation"
+ 'Std M N = (dst M N).
+
+notation "hvbox( M break β’β¦* term 46 N )"
+ non associative with precedence 45
+ for @{ 'Std $M $N }.
+
+lemma dst_inv_lref: βM,N. M β’β¦* N β βj. #j = N β
+ ββs. is_whd s & M β¦*[s] #j.
+#M #N * -M -N
+[ /2 width=3/
+| #s #M #A1 #A2 #_ #_ #_ #j #H destruct
+| #s #M #B1 #B2 #A1 #A2 #_ #_ #_ #_ #j #H destruct
+]
+qed-.
+
+lemma dst_inv_abst: βM,N. M β’β¦* N β βC2. π.C2 = N β
+ ββs,C1. is_whd s & M β¦*[s] π.C1 & C1 β’β¦* C2.
+#M #N * -M -N
+[ #s #M #i #_ #_ #C2 #H destruct
+| #s #M #A1 #A2 #Hs #HM #A12 #C2 #H destruct /2 width=5/
+| #s #M #B1 #B2 #A1 #A2 #_ #_ #_ #_ #C2 #H destruct
+]
+qed-.
+
+lemma dst_inv_appl: βM,N. M β’β¦* N β βD2,C2. @D2.C2 = N β
+ ββs,D1,C1. is_whd s & M β¦*[s] @D1.C1 & D1 β’β¦* D2 & C1 β’β¦* C2.
+#M #N * -M -N
+[ #s #M #i #_ #_ #D2 #C2 #H destruct
+| #s #M #A1 #A2 #_ #_ #_ #D2 #C2 #H destruct
+| #s #M #B1 #B2 #A1 #A2 #Hs #HM #HB12 #HA12 #D2 #C2 #H destruct /2 width=7/
+]
+qed-.
+
+lemma dst_refl: reflexive β¦ dst.
+#M elim M -M /2 width=3/ /2 width=5/ /2 width=7/
+qed.
+
+lemma dst_step_sn: βN1,N2. N1 β’β¦* N2 β βs,M. is_whd s β M β¦*[s] N1 β M β’β¦* N2.
+#N1 #N2 #H elim H -N1 -N2
+[ #r #N #i #Hr #HN #s #M #Hs #HMN
+ lapply (pl_sreds_trans β¦ HMN β¦ HN) -N /3 width=3/
+| #r #N #C1 #C2 #Hr #HN #_ #IHC12 #s #M #Hs #HMN
+ lapply (pl_sreds_trans β¦ HMN β¦ HN) -N /3 width=7/
+| #r #N #D1 #D2 #C1 #C2 #Hr #HN #_ #_ #IHD12 #IHC12 #s #M #Hs #HMN
+ lapply (pl_sreds_trans β¦ HMN β¦ HN) -N /3 width=9/
+]
+qed-.
+
+lemma dst_step_rc: βs,M1,M2. is_whd s β M1 β¦*[s] M2 β M1 β’β¦* M2.
+/3 width=5 by dst_step_sn/
+qed.
+
+lemma dst_lift: liftable dst.
+#h #M1 #M2 #H elim H -M1 -M2
+[ /3 width=3/
+| #s #M #A1 #A2 #Hs #HM #_ #IHA12 #d
+ @(dst_abst β¦ Hs) [2: @(pl_sreds_lift β¦ HM) | skip ] -M // (**) (* auto fails here *)
+| #s #M #B1 #B2 #A1 #A2 #Hs #HM #_ #_ #IHB12 #IHA12 #d
+ @(dst_appl β¦ Hs) [3: @(pl_sreds_lift β¦ HM) |1,2: skip ] -M // (**) (* auto fails here *)
+]
+qed.
+
+lemma dst_inv_lift: deliftable_sn dst.
+#h #N1 #N2 #H elim H -N1 -N2
+[ #s #N1 #i #Hs #HN1 #d #M1 #HMN1
+ elim (pl_sreds_inv_lift β¦ HN1 β¦ HMN1) -N1 /3 width=3/
+| #s #N1 #C1 #C2 #Hs #HN1 #_ #IHC12 #d #M1 #HMN1
+ elim (pl_sreds_inv_lift β¦ HN1 β¦ HMN1) -N1 #M2 #HM12 #HM2
+ elim (lift_inv_abst β¦ HM2) -HM2 #A1 #HAC1 #HM2 destruct
+ elim (IHC12 ???) -IHC12 [4: // |2,3: skip ] #A2 #HA12 #HAC2 destruct (**) (* simplify line *)
+ @(ex2_intro β¦ (π.A2)) // /2 width=5/
+| #s #N1 #D1 #D2 #C1 #C2 #Hs #HN1 #_ #_ #IHD12 #IHC12 #d #M1 #HMN1
+ elim (pl_sreds_inv_lift β¦ HN1 β¦ HMN1) -N1 #M2 #HM12 #HM2
+ elim (lift_inv_appl β¦ HM2) -HM2 #B1 #A1 #HBD1 #HAC1 #HM2 destruct
+ elim (IHD12 ???) -IHD12 [4: // |2,3: skip ] #B2 #HB12 #HBD2 destruct (**) (* simplify line *)
+ elim (IHC12 ???) -IHC12 [4: // |2,3: skip ] #A2 #HA12 #HAC2 destruct (**) (* simplify line *)
+ @(ex2_intro β¦ (@B2.A2)) // /2 width=7/
+]
+qed-.
+
+lemma dst_dsubst: dsubstable dst.
+#N1 #N2 #HN12 #M1 #M2 #H elim H -M1 -M2
+[ #s #M #i #Hs #HM #d elim (lt_or_eq_or_gt i d) #Hid
+ [ lapply (pl_sreds_dsubst β¦ N1 β¦ HM d) -HM
+ >(dsubst_vref_lt β¦ Hid) >(dsubst_vref_lt β¦ Hid) /2 width=3/
+ | destruct >dsubst_vref_eq
+ @(dst_step_sn (β[0,i]N1) β¦ s) /2 width=1/
+ | lapply (pl_sreds_dsubst β¦ N1 β¦ HM d) -HM
+ >(dsubst_vref_gt β¦ Hid) >(dsubst_vref_gt β¦ Hid) /2 width=3/
+ ]
+| #s #M #A1 #A2 #Hs #HM #_ #IHA12 #d
+ lapply (pl_sreds_dsubst β¦ N1 β¦ HM d) -HM /2 width=5/ (**) (* auto needs some help here *)
+| #s #M #B1 #B2 #A1 #A2 #Hs #HM #_ #_ #IHB12 #IHA12 #d
+ lapply (pl_sreds_dsubst β¦ N1 β¦ HM d) -HM /2 width=7/ (**) (* auto needs some help here *)
+]
+qed.
+
+lemma dst_step_dx: βp,M,M2. M β¦[p] M2 β βM1. M1 β’β¦* M β M1 β’β¦* M2.
+#p #M #M2 #H elim H -p -M -M2
+[ #B #A #M1 #H
+ elim (dst_inv_appl β¦ H ???) -H [4: // |2,3: skip ] #s #B1 #M #Hs #HM1 #HB1 #H (**) (* simplify line *)
+ elim (dst_inv_abst β¦ H ??) -H [3: // |2: skip ] #r #A1 #Hr #HM #HA1 (**) (* simplify line *)
+ lapply (pl_sreds_trans β¦ HM1 β¦ (dx:::r) (@B1.π.A1) ?) /2 width=1/ -M #HM1
+ lapply (pl_sreds_step_dx β¦ HM1 (β) ([βB1]A1) ?) -HM1 // #HM1
+ @(dst_step_sn β¦ HM1) /2 width=1/ /4 width=1/
+| #p #A #A2 #_ #IHA2 #M1 #H
+ elim (dst_inv_abst β¦ H ??) -H [3: // |2: skip ] /3 width=5/ (**) (* simplify line *)
+| #p #B #B2 #A #_ #IHB2 #M1 #H
+ elim (dst_inv_appl β¦ H ???) -H [4: // |2,3: skip ] /3 width=7/ (**) (* simplify line *)
+| #p #B #A #A2 #_ #IHA2 #M1 #H
+ elim (dst_inv_appl β¦ H ???) -H [4: // |2,3: skip ] /3 width=7/ (**) (* simplify line *)
+]
+qed-.
+
+lemma pl_sreds_dst: βs,M1,M2. M1 β¦*[s] M2 β M1 β’β¦* M2.
+#s #M1 #M2 #H @(lstar_ind_r ????????? H) -s -M2 // /2 width=4 by dst_step_dx/
+qed.
+
+lemma dst_inv_pl_sreds_is_standard: βM,N. M β’β¦* N β
+ ββr. M β¦*[r] N & is_standard r.
+#M #N #H elim H -M -N
+[ #s #M #i #Hs #HM
+ lapply (is_whd_is_standard β¦ Hs) -Hs /2 width=3/
+| #s #M #A1 #A2 #Hs #HM #_ * #r #HA12 #Hr
+ lapply (pl_sreds_trans β¦ HM (rc:::r) (π.A2) ?) /2 width=1/ -A1 #HM
+ @(ex2_intro β¦ HM) -M -A2 /3 width=1/
+| #s #M #B1 #B2 #A1 #A2 #Hs #HM #_ #_ * #rb #HB12 #Hrb * #ra #HA12 #Hra
+ lapply (pl_sreds_trans β¦ HM (dx:::ra) (@B1.A2) ?) /2 width=1/ -A1 #HM
+ lapply (pl_sreds_trans β¦ HM (sn:::rb) (@B2.A2) ?) /2 width=1/ -B1 #HM
+ @(ex2_intro β¦ HM) -M -B2 -A2 >associative_append /3 width=1/
+]
+qed-.
+
+theorem dst_trans: transitive β¦ dst.
+#M1 #M #M2 #HM1 #HM2
+elim (dst_inv_pl_sreds_is_standard β¦ HM1) -HM1 #s1 #HM1 #_
+elim (dst_inv_pl_sreds_is_standard β¦ HM2) -HM2 #s2 #HM2 #_
+lapply (pl_sreds_trans β¦ HM1 β¦ HM2) -M /2 width=2/
+qed-.
+
+theorem pl_sreds_standard: βs,M,N. M β¦*[s] N β ββr. M β¦*[r] N & is_standard r.
+#s #M #N #H
+@dst_inv_pl_sreds_is_standard /2 width=2/
+qed-.
+
+(* Note: we use "lapply (rewrite_r ?? is_whd β¦ Hq)" (procedural)
+ in place of "cut (is_whd (q::r)) [ >Hq ]" (declarative)
+*)
+lemma dst_in_whd_swap: βp. in_whd p β βN1,N2. N1 β¦[p] N2 β βM1. M1 β’β¦* N1 β
+ ββq,M2. in_whd q & M1 β¦[q] M2 & M2 β’β¦* N2.
+#p #H @(in_whd_ind β¦ H) -p
+[ #N1 #N2 #H1 #M1 #H2
+ elim (pl_sred_inv_nil β¦ H1 ?) -H1 // #D #C #HN1 #HN2
+ elim (dst_inv_appl β¦ H2 β¦ HN1) -N1 #s1 #D1 #N #Hs1 #HM1 #HD1 #H
+ elim (dst_inv_abst β¦ H ??) -H [3: // |2: skip ] #s2 #C1 #Hs2 #HN #HC1 (**) (* simplify line *)
+ lapply (pl_sreds_trans β¦ HM1 β¦ (dx:::s2) (@D1.π.C1) ?) /2 width=1/ -N #HM1
+ lapply (pl_sreds_step_dx β¦ HM1 (β) ([βD1]C1) ?) -HM1 // #HM1
+ elim (pl_sreds_inv_pos β¦ HM1 ?) -HM1
+ [2: >length_append normalize in β’ (??(??%)); // ]
+ #q #r #M #Hq #HM1 #HM
+ lapply (rewrite_r ?? is_whd β¦ Hq) -Hq /4 width=1/ -s1 -s2 * #Hq #Hr
+ @(ex3_2_intro β¦ HM1) -M1 // -q
+ @(dst_step_sn β¦ HM) /2 width=1/
+| #p #_ #IHp #N1 #N2 #H1 #M1 #H2
+ elim (pl_sred_inv_dx β¦ H1 ??) -H1 [3: // |2: skip ] #D #C1 #C2 #HC12 #HN1 #HN2 (**) (* simplify line *)
+ elim (dst_inv_appl β¦ H2 β¦ HN1) -N1 #s #B #A1 #Hs #HM1 #HBD #HAC1
+ elim (IHp β¦ HC12 β¦ HAC1) -p -C1 #p #C1 #Hp #HAC1 #HC12
+ lapply (pl_sreds_step_dx β¦ HM1 (dx::p) (@B.C1) ?) -HM1 /2 width=1/ -A1 #HM1
+ elim (pl_sreds_inv_pos β¦ HM1 ?) -HM1
+ [2: >length_append normalize in β’ (??(??%)); // ]
+ #q #r #M #Hq #HM1 #HM
+ lapply (rewrite_r ?? is_whd β¦ Hq) -Hq /4 width=1/ -p -s * #Hq #Hr
+ @(ex3_2_intro β¦ HM1) -M1 // -q /2 width=7/
+]
+qed-.
+
+theorem pl_sreds_in_whd_swap: βs,M1,N1. M1 β¦*[s] N1 β
+ βp,N2. in_whd p β N1 β¦[p] N2 β
+ ββq,r,M2. in_whd q & M1 β¦[q] M2 & M2 β¦*[r] N2 &
+ is_standard (q::r).
+#s #M1 #N1 #HMN1 #p #N2 #Hp #HN12
+lapply (pl_sreds_dst β¦ HMN1) -s #HMN1
+elim (dst_in_whd_swap β¦ Hp β¦ HN12 β¦ HMN1) -p -N1 #q #M2 #Hq #HM12 #HMN2
+elim (dst_inv_pl_sreds_is_standard β¦ HMN2) -HMN2 /3 width=8/
+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/labeled_sequential_computation.ma".
+include "paths/trace.ma".
+include "paths/labeled_sequential_reduction.ma".
+
+(* PATH-LABELED SEQUENTIAL COMPUTATION (MULTISTEP) *******************************)
+
+(* Note: lstar shuld be replaced by l_sreds *)
+definition pl_sreds: trace β relation term β lstar β¦ pl_sred.
+
+interpretation "path-labeled sequential computation"
+ 'SeqRedStar M s N = (pl_sreds s M N).
+
+lemma sreds_pl_sreds: βM,N. M β¦* N β βs. M β¦*[s] N.
+/3 width=1 by sreds_l_sreds, sred_pl_sred/
+qed-.
+
+lemma pl_sreds_inv_sreds: βs,M,N. M β¦*[s] N β M β¦* N.
+/3 width=5 by l_sreds_inv_sreds, pl_sred_inv_sred/
+qed-.
+
+lemma pl_sreds_refl: reflexive β¦ (pl_sreds (β)).
+//
+qed.
+
+lemma pl_sreds_step_sn: βp,M1,M. M1 β¦[p] M β βs,M2. M β¦*[s] M2 β M1 β¦*[p::s] M2.
+/2 width=3/
+qed-.
+
+lemma pl_sreds_step_dx: βs,M1,M. M1 β¦*[s] M β βp,M2. M β¦[p] M2 β M1 β¦*[s@p::β] M2.
+/2 width=3/
+qed-.
+
+lemma pl_sreds_step_rc: βp,M1,M2. M1 β¦[p] M2 β M1 β¦*[p::β] M2.
+/2 width=1/
+qed.
+
+lemma pl_sreds_inv_nil: βs,M1,M2. M1 β¦*[s] M2 β β = s β M1 = M2.
+/2 width=5 by lstar_inv_nil/
+qed-.
+
+lemma pl_sreds_inv_cons: βs,M1,M2. M1 β¦*[s] M2 β βq,r. q::r = s β
+ ββM. M1 β¦[q] M & M β¦*[r] M2.
+/2 width=3 by lstar_inv_cons/
+qed-.
+
+lemma pl_sreds_inv_step_rc: βp,M1,M2. M1 β¦*[p::β] M2 β M1 β¦[p] M2.
+/2 width=1 by lstar_inv_step/
+qed-.
+
+lemma pl_sreds_inv_pos: βs,M1,M2. M1 β¦*[s] M2 β 0 < |s| β
+ ββp,r,M. p::r = s & M1 β¦[p] M & M β¦*[r] M2.
+/2 width=1 by lstar_inv_pos/
+qed-.
+
+lemma lsred_compatible_rc: ho_compatible_rc pl_sreds.
+/3 width=1/
+qed.
+
+lemma pl_sreds_compatible_sn: ho_compatible_sn pl_sreds.
+/3 width=1/
+qed.
+
+lemma pl_sreds_compatible_dx: ho_compatible_dx pl_sreds.
+/3 width=1/
+qed.
+
+lemma pl_sreds_lift: βs. liftable (pl_sreds s).
+/2 width=1/
+qed.
+
+lemma pl_sreds_inv_lift: βs. deliftable_sn (pl_sreds s).
+/3 width=3 by lstar_deliftable_sn, pl_sred_inv_lift/
+qed-.
+
+lemma pl_sreds_dsubst: βs. dsubstable_dx (pl_sreds s).
+/2 width=1/
+qed.
+
+theorem pl_sreds_mono: βs. singlevalued β¦ (pl_sreds s).
+/3 width=7 by lstar_singlevalued, pl_sred_mono/
+qed-.
+
+theorem pl_sreds_trans: ltransitive β¦ pl_sreds.
+/2 width=3 by lstar_ltransitive/
+qed-.
+
+lemma pl_sreds_compatible_appl: βr,B1,B2. B1 β¦*[r] B2 β βs,A1,A2. A1 β¦*[s] A2 β
+ @B1.A1 β¦*[(sn:::r)@dx:::s] @B2.A2.
+#r #B1 #B2 #HB12 #s #A1 #A2 #HA12
+@(pl_sreds_trans β¦ (@B2.A1)) /2 width=1/
+qed.
+
+lemma pl_sreds_compatible_beta: βr,B1,B2. B1 β¦*[r] B2 β βs,A1,A2. A1 β¦*[s] A2 β
+ @B1.π.A1 β¦*[(sn:::r)@(dx:::rc:::s)@β::β] [βB2] A2.
+#r #B1 #B2 #HB12 #s #A1 #A2 #HA12
+@(pl_sreds_trans β¦ (@B2.π.A1)) /2 width=1/ -r -B1
+@(pl_sreds_step_dx β¦ (@B2.π.A2)) // /3 width=1/
+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 "paths/path.ma".
+include "terms/sequential_reduction.ma".
+
+(* PATH-LABELED SEQUENTIAL REDUCTION (SINGLE STEP) **************************)
+
+inductive pl_sred: path β relation term β
+| pl_sred_beta : βB,A. pl_sred (β) (@B.π.A) ([βB]A)
+| pl_sred_abst : βp,A1,A2. pl_sred p A1 A2 β pl_sred (rc::p) (π.A1) (π.A2)
+| pl_sred_appl_sn: βp,B1,B2,A. pl_sred p B1 B2 β pl_sred (sn::p) (@B1.A) (@B2.A)
+| pl_sred_appl_dx: βp,B,A1,A2. pl_sred p A1 A2 β pl_sred (dx::p) (@B.A1) (@B.A2)
+.
+
+interpretation "path-labeled sequential reduction"
+ 'SeqRed M p N = (pl_sred p M N).
+
+lemma sred_pl_sred: βM,N. M β¦ N β βp. M β¦[p] N.
+#M #N #H elim H -M -N
+[ /2 width=2/
+| #A1 #A2 #_ * /3 width=2/
+| #B1 #B2 #A #_ * /3 width=2/
+| #B #A1 #A2 #_ * /3 width=2/
+]
+qed-.
+
+lemma pl_sred_inv_sred: βp,M,N. M β¦[p] N β M β¦ N.
+#p #M #N #H elim H -p -M -N // /2 width=1/
+qed-.
+
+lemma pl_sred_inv_vref: βp,M,N. M β¦[p] N β βi. #i = M β β₯.
+/3 width=5 by pl_sred_inv_sred, sred_inv_vref/
+qed-.
+
+lemma pl_sred_inv_nil: βp,M,N. M β¦[p] N β β = p β
+ ββB,A. @B. π.A = M & [βB] A = N.
+#p #M #N * -p -M -N
+[ #B #A #_ destruct /2 width=4/
+| #p #A1 #A2 #_ #H destruct
+| #p #B1 #B2 #A #_ #H destruct
+| #p #B #A1 #A2 #_ #H destruct
+]
+qed-.
+
+lemma pl_sred_inv_rc: βp,M,N. M β¦[p] N β βq. rc::q = p β
+ ββA1,A2. A1 β¦[q] A2 & π.A1 = M & π.A2 = N.
+#p #M #N * -p -M -N
+[ #B #A #q #H destruct
+| #p #A1 #A2 #HA12 #q #H destruct /2 width=5/
+| #p #B1 #B2 #A #_ #q #H destruct
+| #p #B #A1 #A2 #_ #q #H destruct
+]
+qed-.
+
+lemma pl_sred_inv_sn: βp,M,N. M β¦[p] N β βq. sn::q = p β
+ ββB1,B2,A. B1 β¦[q] B2 & @B1.A = M & @B2.A = N.
+#p #M #N * -p -M -N
+[ #B #A #q #H destruct
+| #p #A1 #A2 #_ #q #H destruct
+| #p #B1 #B2 #A #HB12 #q #H destruct /2 width=6/
+| #p #B #A1 #A2 #_ #q #H destruct
+]
+qed-.
+
+lemma pl_sred_inv_dx: βp,M,N. M β¦[p] N β βq. dx::q = p β
+ ββB,A1,A2. A1 β¦[q] A2 & @B.A1 = M & @B.A2 = N.
+#p #M #N * -p -M -N
+[ #B #A #q #H destruct
+| #p #A1 #A2 #_ #q #H destruct
+| #p #B1 #B2 #A #_ #q #H destruct
+| #p #B #A1 #A2 #HA12 #q #H destruct /2 width=6/
+]
+qed-.
+
+lemma pl_sred_lift: βp. liftable (pl_sred p).
+#p #h #M1 #M2 #H elim H -p -M1 -M2 normalize /2 width=1/
+#B #A #d <dsubst_lift_le //
+qed.
+
+lemma pl_sred_inv_lift: βp. deliftable_sn (pl_sred p).
+#p #h #N1 #N2 #H elim H -p -N1 -N2
+[ #D #C #d #M1 #H
+ elim (lift_inv_appl β¦ H) -H #B #M #H0 #HM #H destruct
+ elim (lift_inv_abst β¦ HM) -HM #A #H0 #H destruct /3 width=3/
+| #p #C1 #C2 #_ #IHC12 #d #M1 #H
+ elim (lift_inv_abst β¦ H) -H #A1 #HAC1 #H
+ elim (IHC12 β¦ HAC1) -C1 #A2 #HA12 #HAC2 destruct
+ @(ex2_intro β¦ (π.A2)) // /2 width=1/
+| #p #D1 #D2 #C1 #_ #IHD12 #d #M1 #H
+ elim (lift_inv_appl β¦ H) -H #B1 #A #HBD1 #H1 #H2
+ elim (IHD12 β¦ HBD1) -D1 #B2 #HB12 #HBD2 destruct
+ @(ex2_intro β¦ (@B2.A)) // /2 width=1/
+| #p #D1 #C1 #C2 #_ #IHC12 #d #M1 #H
+ elim (lift_inv_appl β¦ H) -H #B #A1 #H1 #HAC1 #H2
+ elim (IHC12 β¦ HAC1) -C1 #A2 #HA12 #HAC2 destruct
+ @(ex2_intro β¦ (@B.A2)) // /2 width=1/
+]
+qed-.
+
+lemma pl_sred_dsubst: βp. dsubstable_dx (pl_sred p).
+#p #D1 #M1 #M2 #H elim H -p -M1 -M2 normalize /2 width=1/
+#D2 #A #d >dsubst_dsubst_ge //
+qed.
+
+theorem pl_sred_mono: βp. singlevalued β¦ (pl_sred p).
+#p #M #N1 #H elim H -p -M -N1
+[ #B #A #N2 #H elim (pl_sred_inv_nil β¦ H ?) -H //
+ #D #C #H #HN2 destruct //
+| #p #A1 #A2 #_ #IHA12 #N2 #H elim (pl_sred_inv_rc β¦ H ??) -H [3: // |2: skip ] (**) (* simplify line *)
+ #C1 #C2 #HC12 #H #HN2 destruct /3 width=1/
+| #p #B1 #B2 #A #_ #IHB12 #N2 #H elim (pl_sred_inv_sn β¦ H ??) -H [3: // |2: skip ] (**) (* simplify line *)
+ #D1 #D2 #C #HD12 #H #HN2 destruct /3 width=1/
+| #p #B #A1 #A2 #_ #IHA12 #N2 #H elim (pl_sred_inv_dx β¦ H ??) -H [3: // |2: skip ] (**) (* simplify line *)
+ #D #C1 #C2 #HC12 #H #HN2 destruct /3 width=1/
+]
+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".
+
+(* PATH *********************************************************************)
+
+(* Policy: path step metavariables: c *)
+(* 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 (dexter) : proceed on the right argument of an application
+*)
+inductive step: Type[0] β
+| rc: step
+| sn: step
+| dx: step
+.
+
+definition is_dx: predicate step β Ξ»c. dx = c.
+
+(* Policy: path metavariables: p, q *)
+(* Note: this is a path in the tree representation of a term, heading to a redex *)
+definition path: Type[0] β list step.
+
+(* Note: a redex is "in whd" when is not under an abstraction nor in the lefr argument of an application *)
+definition in_whd: predicate path β All β¦ is_dx.
+
+lemma in_whd_ind: βR:predicate path. R (β) β
+ (βp. in_whd p β R p β R (dx::p)) β
+ βp. in_whd p β R p.
+#R #H #IH #p elim p -p // -H *
+#p #IHp * #H1 #H2 destruct /3 width=1/
+qed-.
+
+definition compatible_rc: predicate (pathβrelation term) β Ξ»R.
+ βp,A1,A2. R p A1 A2 β R (rc::p) (π.A1) (π.A2).
+
+definition compatible_sn: predicate (pathβrelation term) β Ξ»R.
+ βp,B1,B2,A. R p B1 B2 β R (sn::p) (@B1.A) (@B2.A).
+
+definition compatible_dx: predicate (pathβrelation term) β Ξ»R.
+ βp,B,A1,A2. R p A1 A2 β R (dx::p) (@B.A1) (@B.A2).
--- /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/path.ma".
+
+(* STANDARD ORDER ************************************************************)
+
+(* 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_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_skip: sprec (dx::β) β
+.
+
+interpretation "standard 'precedes' on paths"
+ 'prec p q = (sprec p q).
+
+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
+| #p #q #p0 #H destruct
+| #p #q #p0 #H destruct
+| #c #p #q #Hpq #p0 #H destruct /2 width=3/
+| #p0 #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
+| #p #q * #H destruct
+| #c #p #q #_ #IHpq * #H destruct /3 width=1/
+]
+qed-.
+
+(* Note: this is p < q *)
+definition slt: relation path β TC β¦ sprec.
+
+interpretation "standard 'less than' on paths"
+ 'lt p q = (slt p q).
+
+lemma slt_step_rc: βp,q. p βΊ q β p < q.
+/2 width=1/
+qed.
+
+lemma slt_nil: βc,p. β < c::p.
+/2 width=1/
+qed.
+
+lemma slt_skip: dx::β < β.
+/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/
+qed.
+
+theorem slt_trans: transitive β¦ slt.
+/2 width=3/
+qed-.
+
+lemma slt_refl: βp. p < p.
+#p elim p -p /2 width=1/
+@(slt_trans β¦ (dx::β)) //
+qed.
+
+(* Note: this is p β€ q *)
+definition sle: relation path β star β¦ sprec.
+
+interpretation "standard 'less or equal to' on paths"
+ 'leq p q = (sle p q).
+
+lemma sle_step_rc: βp,q. p βΊ q β p β€ q.
+/2 width=1/
+qed.
+
+lemma sle_step_sn: βp1,p,p2. p1 βΊ p β p β€ p2 β p1 β€ p2.
+/2 width=3/
+qed-.
+
+lemma sle_rc: βp,q. dx::p β€ rc::q.
+/2 width=1/
+qed.
+
+lemma sle_sn: βp,q. rc::p β€ sn::q.
+/2 width=1/
+qed.
+
+lemma sle_skip: dx::β β€ β.
+/2 width=1/
+qed.
+
+lemma sle_nil: βp. β β€ p.
+* // /2 width=1/
+qed.
+
+lemma sle_comp: βp1,p2. p1 β€ p2 β βc. (c::p1) β€ (c::p2).
+#p1 #p2 #H elim H -p2 // /3 width=3/
+qed.
+
+lemma sle_skip_sle: βp. p β€ β β dx::p β€ β.
+#p #H @(star_ind_l ??????? H) -p //
+#p #q #Hpq #_ #H @(sle_step_sn β¦ H) -H /2 width=1/
+qed.
+
+theorem sle_trans: transitive β¦ sle.
+/2 width=3/
+qed-.
+
+lemma sle_cons: βp,q. dx::p β€ sn::q.
+#p #q
+@(sle_trans β¦ (rc::q)) /2 width=1/
+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/
+ elim (IHp1 p2) -IHp1 /3 width=1/
+]
+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/
+#q #q0 #_ #Hq0 #IHpq #p0 #H destruct
+elim (IHpq p0 ?) -IHpq // #p1 #Hp01 #H
+elim (sprec_inv_sn β¦ Hq0 β¦ H) -q /3 width=3/
+qed-.
+
+lemma in_whd_sle_nil: βp. in_whd p β p β€ β.
+#p #H @(in_whd_ind β¦ H) -p // /2 width=1/
+qed.
+
+theorem in_whd_sle: βp. in_whd p β βq. p β€ q.
+#p #H @(in_whd_ind β¦ H) -p //
+#p #_ #IHp * /3 width=1/ * #q /2 width=1/
+qed.
+
+lemma sle_nil_inv_in_whd: βp. p β€ β β in_whd p.
+#p #H @(star_ind_l ??????? H) -p // /2 width=3 by sprec_fwd_in_whd/
+qed-.
+
+lemma sle_inv_in_whd: βp. (βq. p β€ q) β in_whd p.
+/2 width=1 by sle_nil_inv_in_whd/
+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 "paths/trace.ma".
+include "paths/standard_order.ma".
+
+(* STANDARD TRACE ***********************************************************)
+
+(* 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 * //
+#q #s #IHs * /3 width=1/
+qed.
+
+lemma is_standard_cons: βp,s. is_standard s β is_standard ((dx::p)::sn:::s).
+#p #s elim s -s // #q1 * /2 width=1/
+#q2 #s #IHs * /4 width=1/
+qed.
+
+lemma is_standard_append: βr. is_standard r β βs. is_standard s β is_standard ((dx:::r)@sn:::s).
+#r elim r -r /3 width=1/ #p * /2 width=1/
+#q #r #IHr * /3 width=1/
+qed.
+
+theorem is_whd_is_standard: βs. is_whd s β is_standard s.
+#s elim s -s // #p * //
+#q #s #IHs * /3 width=1/
+qed.
+
+lemma is_standard_in_whd: βp. in_whd p β βs. is_standard s β is_standard (p::s).
+#p #Hp * // /3 width=1/
+qed.
+
+theorem is_whd_is_standard_trans: βr. is_whd r β βs. is_standard s β is_standard (r@s).
+#r elim r -r // #p *
+[ #_ * /2 width=1/
+| #q #r #IHr * /3 width=1/
+]
+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 "paths/path.ma".
+
+(* TRACE ********************************************************************)
+
+(* Policy: trace metavariables: r, s *)
+definition trace: Type[0] β list path.
+
+(* Note: a "whd" computation contracts just redexes in the whd *)
+definition is_whd: predicate trace β All β¦ in_whd.
+
+lemma is_whd_dx: βs. is_whd s β is_whd (dx:::s).
+#s elim s -s //
+#p #s #IHs * /3 width=1/
+qed.
+
+lemma is_whd_append: βr. is_whd r β βs. is_whd s β is_whd (r@s).
+#r elim r -r //
+#q #r #IHr * /3 width=1/
+qed.
+
+definition ho_compatible_rc: predicate (traceβrelation term) β Ξ»R.
+ βs,A1,A2. R s A1 A2 β R (rc:::s) (π.A1) (π.A2).
+
+definition ho_compatible_sn: predicate (traceβrelation term) β Ξ»R.
+ βs,B1,B2,A. R s B1 B2 β R (sn:::s) (@B1.A) (@B2.A).
+
+definition ho_compatible_dx: predicate (traceβrelation term) β Ξ»R.
+ βs,B,A1,A2. R s A1 A2 β R (dx:::s) (@B.A1) (@B.A2).
+
+lemma lstar_compatible_rc: βR. compatible_rc R β ho_compatible_rc (lstar β¦ R).
+#R #HR #s #A1 #A2 #H @(lstar_ind_l ????????? H) -s -A1 // /3 width=3/
+qed.
+
+lemma lstar_compatible_sn: βR. compatible_sn R β ho_compatible_sn (lstar β¦ R).
+#R #HR #s #B1 #B2 #A #H @(lstar_ind_l ????????? H) -s -B1 // /3 width=3/
+qed.
+
+lemma lstar_compatible_dx: βR. compatible_dx R β ho_compatible_dx (lstar β¦ R).
+#R #HR #s #B #A1 #A2 #H @(lstar_ind_l ????????? H) -s -A1 // /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 "basics/star.ma".
-include "basics/lists/lstar.ma".
-include "arithmetics/exp.ma".
-
-include "xoa_notation.ma".
-include "xoa.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}.
-
-(* arithmetics *)
-
-lemma lt_refl_false: βn. n < n β β₯.
-#n #H elim (lt_to_not_eq β¦ H) -H /2 width=1/
-qed-.
-
-lemma lt_zero_false: βn. n < 0 β β₯.
-#n #H elim (lt_to_not_le β¦ H) -H /2 width=1/
-qed-.
-
-lemma plus_lt_false: βm,n. m + n < m β β₯.
-#m #n #H elim (lt_to_not_le β¦ H) -H /2 width=1/
-qed-.
-
-lemma lt_or_eq_or_gt: βm,n. β¨β¨ m < n | n = m | n < m.
-#m #n elim (lt_or_ge m n) /2 width=1/
-#H elim H -m /2 width=1/
-#m #Hm * #H /2 width=1/ /3 width=1/
-qed-.
-
-(* trichotomy operator *)
-
-(* Note: this is "if eqb n1 n2 then a2 else if leb n1 n2 then a1 else a3" *)
-let rec tri (A:Type[0]) n1 n2 a1 a2 a3 on n1 : A β
- match n1 with
- [ O β match n2 with [ O β a2 | S n2 β a1 ]
- | S n1 β match n2 with [ O β a3 | S n2 β tri A n1 n2 a1 a2 a3 ]
- ].
-
-lemma tri_lt: βA,a1,a2,a3,n2,n1. n1 < n2 β tri A n1 n2 a1 a2 a3 = a1.
-#A #a1 #a2 #a3 #n2 elim n2 -n2
-[ #n1 #H elim (lt_zero_false β¦ H)
-| #n2 #IH #n1 elim n1 -n1 // /3 width=1/
-]
-qed.
-
-lemma tri_eq: βA,a1,a2,a3,n. tri A n n a1 a2 a3 = a2.
-#A #a1 #a2 #a3 #n elim n -n normalize //
-qed.
-
-lemma tri_gt: βA,a1,a2,a3,n1,n2. n2 < n1 β tri A n1 n2 a1 a2 a3 = a3.
-#A #a1 #a2 #a3 #n1 elim n1 -n1
-[ #n2 #H elim (lt_zero_false β¦ H)
-| #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}.
-
-definition map_cons: βA. A β list (list A) β list (list A) β Ξ»A,a.
- map β¦ (cons β¦ a).
-
-interpretation "map_cons" 'ho_cons a l = (map_cons ? a l).
-
-notation "hvbox(a ::: break l)"
- right associative with precedence 47
- for @{'ho_cons $a $l}.
-
-(* 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)
-| #a #ll #b1 #b #Hb1 #Hb2 #_ #_ /2 width=6/ (**) (* auto fail if we do not remove the inductive premise *)
-]
-qed-.
(* *)
(**************************************************************************)
-include "preamble.ma".
-include "notation.ma".
+include "background/preamble.ma".
+include "background/notation.ma".
(* SUBSETS OF SUBTERMS ******************************************************)
(* *)
(**************************************************************************)
-include "terms/pointer_list.ma".
-include "terms/parallel_computation.ma".
+include "terms/sequential_computation.ma".
-(* LABELED SEQUENTIAL COMPUTATION (MULTISTEP) *******************************)
+(* ABSTRACT LABELED SEQUENTIAL COMPUTATION (MULTISTEP) **********************)
-definition lsreds: ptrl β relation term β lstar β¦ lsred.
+definition l_sreds: βS. (Sβrelation term) β list S β relation term β
+ Ξ»S,R. lstar β¦ R.
-interpretation "labelled sequential computation"
- 'SeqRedStar M s N = (lsreds s M N).
-
-notation "hvbox( M break β¦* [ term 46 s ] break term 46 N )"
- non associative with precedence 45
- for @{ 'SeqRedStar $M $s $N }.
-
-lemma lsreds_refl: reflexive β¦ (lsreds (β)).
-//
-qed.
-
-lemma lsreds_step_sn: βp,M1,M. M1 β¦[p] M β βs,M2. M β¦*[s] M2 β M1 β¦*[p::s] M2.
-/2 width=3/
-qed-.
-
-lemma lsreds_step_dx: βs,M1,M. M1 β¦*[s] M β βp,M2. M β¦[p] M2 β M1 β¦*[s@p::β] M2.
-/2 width=3/
-qed-.
-
-lemma lsreds_step_rc: βp,M1,M2. M1 β¦[p] M2 β M1 β¦*[p::β] M2.
-/2 width=1/
-qed.
-
-lemma lsreds_inv_nil: βs,M1,M2. M1 β¦*[s] M2 β β = s β M1 = M2.
-/2 width=5 by lstar_inv_nil/
-qed-.
-
-lemma lsreds_inv_cons: βs,M1,M2. M1 β¦*[s] M2 β βq,r. q::r = s β
- ββM. M1 β¦[q] M & M β¦*[r] M2.
-/2 width=3 by lstar_inv_cons/
-qed-.
-
-lemma lsreds_inv_step_rc: βp,M1,M2. M1 β¦*[p::β] M2 β M1 β¦[p] M2.
-/2 width=1 by lstar_inv_step/
-qed-.
-
-lemma lsreds_inv_pos: βs,M1,M2. M1 β¦*[s] M2 β 0 < |s| β
- ββp,r,M. p::r = s & M1 β¦[p] M & M β¦*[r] M2.
-/2 width=1 by lstar_inv_pos/
-qed-.
-
-lemma lsred_compatible_rc: ho_compatible_rc lsreds.
-/3 width=1/
-qed.
-
-lemma lsreds_compatible_sn: ho_compatible_sn lsreds.
-/3 width=1/
-qed.
-
-lemma lsreds_compatible_dx: ho_compatible_dx lsreds.
-/3 width=1/
-qed.
-
-lemma lsreds_lift: βs. liftable (lsreds s).
-/2 width=1/
-qed.
-
-lemma lsreds_inv_lift: βs. deliftable_sn (lsreds s).
-/3 width=3 by lstar_deliftable_sn, lsred_inv_lift/
+lemma sreds_l_sreds: βS,R. (βM,N. M β¦ N β βa. R a M N) β
+ βM,N. M β¦* N β βl. l_sreds S R l M N.
+#S #R #HR #M #N #H elim H -N
+[ #N #N0 #_ #HN0 * #l #HMN
+ elim (HR β¦ HN0) -HR -HN0 /3 width=5/
+| /2 width=2/
+]
qed-.
-lemma lsreds_dsubst: βs. dsubstable_dx (lsreds s).
-/2 width=1/
-qed.
-
-theorem lsreds_mono: βs. singlevalued β¦ (lsreds s).
-/3 width=7 by lstar_singlevalued, lsred_mono/
-qed-.
-
-theorem lsreds_trans: ltransitive β¦ lsreds.
-/2 width=3 by lstar_ltransitive/
+lemma l_sreds_inv_sreds: βS,R. (βa,M,N. R a M N β M β¦ N) β
+ βl,M,N. l_sreds S R l M N β M β¦* N.
+#S #R #HR #l #M #N #H elim H -N // /3 by star_compl/
qed-.
-lemma lsreds_compatible_appl: βr,B1,B2. B1 β¦*[r] B2 β βs,A1,A2. A1 β¦*[s] A2 β
- @B1.A1 β¦*[(sn:::r)@dx:::s] @B2.A2.
-#r #B1 #B2 #HB12 #s #A1 #A2 #HA12
-@(lsreds_trans β¦ (@B2.A1)) /2 width=1/
-qed.
-
-lemma lsreds_compatible_beta: βr,B1,B2. B1 β¦*[r] B2 β βs,A1,A2. A1 β¦*[s] A2 β
- @B1.π.A1 β¦*[(sn:::r)@(dx:::rc:::s)@β::β] [βB2] A2.
-#r #B1 #B2 #HB12 #s #A1 #A2 #HA12
-@(lsreds_trans β¦ (@B2.π.A1)) /2 width=1/ -r -B1
-@(lsreds_step_dx β¦ (@B2.π.A2)) // /3 width=1/
-qed.
-
(* Note: "|s|" should be unparetesized *)
-lemma lsreds_fwd_mult: βs,M1,M2. M1 β¦*[s] M2 β β―{M2} β€ β―{M1} ^ (2 ^ (|s|)).
-#s #M1 #M2 #H @(lstar_ind_l ????????? H) -s -M1 normalize //
-#p #s #M1 #M #HM1 #_ #IHM2
-lapply (lsred_fwd_mult β¦ HM1) -p #HM1
+lemma l_sreds_fwd_mult: βS,R. (βa,M,N. R a M N β M β¦ N) β
+ βl,M1,M2. l_sreds S R l M1 M2 β
+ β―{M2} β€ β―{M1} ^ (2 ^ (|l|)).
+#S #R #HR #l #M1 #M2 #H @(lstar_ind_l ????????? H) -l -M1 normalize //
+#a #l #M1 #M #HM1 #_ #IHM2
+lapply (HR β¦ HM1) -HR -a #HM1
+lapply (sred_fwd_mult β¦ HM1) #HM1
@(transitive_le β¦ IHM2) -M2
/3 width=1 by le_exp1, lt_O_exp, lt_to_le/ (**) (* auto: slow without trace *)
qed-.
-
-theorem lsreds_preds: βs,M1,M2. M1 β¦*[s] M2 β M1 β€* M2.
-#s #M1 #M2 #H @(lstar_ind_l ????????? H) -s -M1 //
-#a #s #M1 #M #HM1 #_ #IHM2
-@(preds_step_sn β¦ IHM2) -M2 /2 width=2/
-qed.
-
-lemma pred_lsreds: βM1,M2. M1 β€ M2 β βr. M1 β¦*[r] M2.
-#M1 #M2 #H elim H -M1 -M2 /2 width=2/
-[ #A1 #A2 #_ * /3 width=2/
-| #B1 #B2 #A1 #A2 #_ #_ * #r #HB12 * /3 width=2/
-| #B1 #B2 #A1 #A2 #_ #_ * #r #HB12 * /3 width=2/
-qed-.
-
-theorem preds_lsreds: βM1,M2. M1 β€* M2 β βr. M1 β¦*[r] M2.
-#M1 #M2 #H elim H -M2 /2 width=2/
-#M #M2 #_ #HM2 * #r #HM1
-elim (pred_lsreds β¦ HM2) -HM2 #s #HM2
-lapply (lsreds_trans β¦ HM1 β¦ HM2) -M /2 width=2/
-qed-.
-
-theorem lsreds_conf: βs1,M0,M1. M0 β¦*[s1] M1 β βs2,M2. M0 β¦*[s2] M2 β
- ββr1,r2,M. M1 β¦*[r1] M & M2 β¦*[r2] M.
-#s1 #M0 #M1 #HM01 #s2 #M2 #HM02
-lapply (lsreds_preds β¦ HM01) -s1 #HM01
-lapply (lsreds_preds β¦ HM02) -s2 #HM02
-elim (preds_conf β¦ HM01 β¦ HM02) -M0 #M #HM1 #HM2
-elim (preds_lsreds β¦ HM1) -HM1
-elim (preds_lsreds β¦ HM2) -HM2 /2 width=5/
-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/pointer.ma".
-include "terms/multiplicity.ma".
-
-(* LABELED SEQUENTIAL REDUCTION (SINGLE STEP) *******************************)
-
-(* Note: the application "(A B)" is represented by "@B.A" following:
- F. Kamareddine and R.P. Nederpelt: "A useful Ξ»-notation".
- Theoretical Computer Science 155(1), Elsevier (1996), pp. 85-109.
-*)
-inductive lsred: ptr β relation term β
-| lsred_beta : βB,A. lsred (β) (@B.π.A) ([βB]A)
-| lsred_abst : βp,A1,A2. lsred p A1 A2 β lsred (rc::p) (π.A1) (π.A2)
-| lsred_appl_sn: βp,B1,B2,A. lsred p B1 B2 β lsred (sn::p) (@B1.A) (@B2.A)
-| lsred_appl_dx: βp,B,A1,A2. lsred p A1 A2 β lsred (dx::p) (@B.A1) (@B.A2)
-.
-
-interpretation "labelled sequential reduction"
- 'SeqRed M p N = (lsred p M N).
-
-(* Note: we do not use β since it is reserved by CIC *)
-notation "hvbox( M break β¦ [ term 46 p ] break term 46 N )"
- non associative with precedence 45
- for @{ 'SeqRed $M $p $N }.
-
-lemma lsred_inv_vref: βp,M,N. M β¦[p] N β βi. #i = M β β₯.
-#p #M #N * -p -M -N
-[ #B #A #i #H destruct
-| #p #A1 #A2 #_ #i #H destruct
-| #p #B1 #B2 #A #_ #i #H destruct
-| #p #B #A1 #A2 #_ #i #H destruct
-]
-qed-.
-
-lemma lsred_inv_nil: βp,M,N. M β¦[p] N β β = p β
- ββB,A. @B. π.A = M & [βB] A = N.
-#p #M #N * -p -M -N
-[ #B #A #_ destruct /2 width=4/
-| #p #A1 #A2 #_ #H destruct
-| #p #B1 #B2 #A #_ #H destruct
-| #p #B #A1 #A2 #_ #H destruct
-]
-qed-.
-
-lemma lsred_inv_rc: βp,M,N. M β¦[p] N β βq. rc::q = p β
- ββA1,A2. A1 β¦[q] A2 & π.A1 = M & π.A2 = N.
-#p #M #N * -p -M -N
-[ #B #A #q #H destruct
-| #p #A1 #A2 #HA12 #q #H destruct /2 width=5/
-| #p #B1 #B2 #A #_ #q #H destruct
-| #p #B #A1 #A2 #_ #q #H destruct
-]
-qed-.
-
-lemma lsred_inv_sn: βp,M,N. M β¦[p] N β βq. sn::q = p β
- ββB1,B2,A. B1 β¦[q] B2 & @B1.A = M & @B2.A = N.
-#p #M #N * -p -M -N
-[ #B #A #q #H destruct
-| #p #A1 #A2 #_ #q #H destruct
-| #p #B1 #B2 #A #HB12 #q #H destruct /2 width=6/
-| #p #B #A1 #A2 #_ #q #H destruct
-]
-qed-.
-
-lemma lsred_inv_dx: βp,M,N. M β¦[p] N β βq. dx::q = p β
- ββB,A1,A2. A1 β¦[q] A2 & @B.A1 = M & @B.A2 = N.
-#p #M #N * -p -M -N
-[ #B #A #q #H destruct
-| #p #A1 #A2 #_ #q #H destruct
-| #p #B1 #B2 #A #_ #q #H destruct
-| #p #B #A1 #A2 #HA12 #q #H destruct /2 width=6/
-]
-qed-.
-
-lemma lsred_fwd_mult: βp,M,N. M β¦[p] N β β―{N} < β―{M} * β―{M}.
-#p #M #N #H elim H -p -M -N
-[ #B #A @(le_to_lt_to_lt β¦ (β―{A}*β―{B})) //
- normalize /3 width=1 by lt_minus_to_plus_r, lt_times/ (**) (* auto: too slow without trace *)
-| //
-| #p #B #D #A #_ #IHBD
- @(lt_to_le_to_lt β¦ (β―{B}*β―{B}+β―{A})) [ /2 width=1/ ] -D -p
-| #p #B #A #C #_ #IHAC
- @(lt_to_le_to_lt β¦ (β―{B}+β―{A}*β―{A})) [ /2 width=1/ ] -C -p
-]
-@(transitive_le β¦ (β―{B}*β―{B}+β―{A}*β―{A})) [ /2 width=1/ ]
->distributive_times_plus normalize /2 width=1/
-qed-.
-
-lemma lsred_lift: βp. liftable (lsred p).
-#p #h #M1 #M2 #H elim H -p -M1 -M2 normalize /2 width=1/
-#B #A #d <dsubst_lift_le //
-qed.
-
-lemma lsred_inv_lift: βp. deliftable_sn (lsred p).
-#p #h #N1 #N2 #H elim H -p -N1 -N2
-[ #D #C #d #M1 #H
- elim (lift_inv_appl β¦ H) -H #B #M #H0 #HM #H destruct
- elim (lift_inv_abst β¦ HM) -HM #A #H0 #H destruct /3 width=3/
-| #p #C1 #C2 #_ #IHC12 #d #M1 #H
- elim (lift_inv_abst β¦ H) -H #A1 #HAC1 #H
- elim (IHC12 β¦ HAC1) -C1 #A2 #HA12 #HAC2 destruct
- @(ex2_intro β¦ (π.A2)) // /2 width=1/
-| #p #D1 #D2 #C1 #_ #IHD12 #d #M1 #H
- elim (lift_inv_appl β¦ H) -H #B1 #A #HBD1 #H1 #H2
- elim (IHD12 β¦ HBD1) -D1 #B2 #HB12 #HBD2 destruct
- @(ex2_intro β¦ (@B2.A)) // /2 width=1/
-| #p #D1 #C1 #C2 #_ #IHC12 #d #M1 #H
- elim (lift_inv_appl β¦ H) -H #B #A1 #H1 #HAC1 #H2
- elim (IHC12 β¦ HAC1) -C1 #A2 #HA12 #HAC2 destruct
- @(ex2_intro β¦ (@B.A2)) // /2 width=1/
-]
-qed-.
-
-lemma lsred_dsubst: βp. dsubstable_dx (lsred p).
-#p #D1 #M1 #M2 #H elim H -p -M1 -M2 normalize /2 width=1/
-#D2 #A #d >dsubst_dsubst_ge //
-qed.
-
-theorem lsred_mono: βp. singlevalued β¦ (lsred p).
-#p #M #N1 #H elim H -p -M -N1
-[ #B #A #N2 #H elim (lsred_inv_nil β¦ H ?) -H //
- #D #C #H #HN2 destruct //
-| #p #A1 #A2 #_ #IHA12 #N2 #H elim (lsred_inv_rc β¦ H ??) -H [3: // |2: skip ] (**) (* simplify line *)
- #C1 #C2 #HC12 #H #HN2 destruct /3 width=1/
-| #p #B1 #B2 #A #_ #IHB12 #N2 #H elim (lsred_inv_sn β¦ H ??) -H [3: // |2: skip ] (**) (* simplify line *)
- #D1 #D2 #C #HD12 #H #HN2 destruct /3 width=1/
-| #p #B #A1 #A2 #_ #IHA12 #N2 #H elim (lsred_inv_dx β¦ H ??) -H [3: // |2: skip ] (**) (* simplify line *)
- #D #C1 #C2 #HC12 #H #HN2 destruct /3 width=1/
-]
-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/lift.ma".
-
-(* LENGTH *******************************************************************)
-
-(* Note: this gives the number of abstractions and applications in M *)
-let rec length M on M β match M with
-[ VRef i β 0
-| Abst A β length A + 1
-| Appl B A β (length B) + (length A) + 1
-].
-
-interpretation "term length"
- 'card M = (length M).
-
-lemma length_lift: βh,M,d. |β[d, h] M| = |M|.
-#h #M elim M -M normalize //
-qed.
interpretation "parallel computation"
'ParRedStar M N = (preds M N).
-notation "hvbox( M β€* break term 46 N )"
- non associative with precedence 45
- for @{ 'ParRedStar $M $N }.
-
lemma preds_refl: reflexive β¦ preds.
//
qed.
(* *)
(**************************************************************************)
-include "terms/length.ma".
-include "terms/labeled_sequential_reduction.ma".
+include "terms/size.ma".
+include "terms/sequential_reduction.ma".
(* PARALLEL REDUCTION (SINGLE STEP) *****************************************)
(* Note: the application "(A B)" is represented by "@B.A"
- as for labelled sequential reduction
+ as for sequential reduction
*)
inductive pred: relation term β
| pred_vref: βi. pred (#i) (#i)
interpretation "parallel reduction"
'ParRed M N = (pred M N).
-notation "hvbox( M β€ break term 46 N )"
- non associative with precedence 45
- for @{ 'ParRed $M $N }.
-
lemma pred_refl: reflexive β¦ pred.
#M elim M -M // /2 width=1/
qed.
qed-.
theorem pred_conf: confluent β¦ pred.
-#M @(f_ind β¦ length β¦ M) -M #n #IH * normalize
+#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
]
qed-.
-lemma lsred_pred: βp,M,N. M β¦[p] N β M β€ N.
-#p #M #N #H elim H -p -M -N /2 width=1/
+lemma sred_pred: βM,N. M β¦ N β M β€ N.
+#M #N #H elim H -M -N /2 width=1/
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".
-
-(* POINTER ******************************************************************)
-
-(* Policy: pointer step metavariables: c *)
-(* 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 (dexter) : proceed on the right argument of an application
-*)
-inductive ptr_step: Type[0] β
-| rc: ptr_step
-| sn: ptr_step
-| dx: ptr_step
-.
-
-definition is_dx: predicate ptr_step β Ξ»c. dx = c.
-
-(* Policy: pointer metavariables: p, q *)
-(* Note: this is a path in the tree representation of a term, heading to a redex *)
-definition ptr: Type[0] β list ptr_step.
-
-(* Note: a redex is "in whd" when is not under an abstraction nor in the lefr argument of an application *)
-definition in_whd: predicate ptr β All β¦ is_dx.
-
-lemma in_whd_ind: βR:predicate ptr. R (β) β
- (βp. in_whd p β R p β R (dx::p)) β
- βp. in_whd p β R p.
-#R #H #IH #p elim p -p // -H *
-#p #IHp * #H1 #H2 destruct /3 width=1/
-qed-.
-
-definition compatible_rc: predicate (ptrβrelation term) β Ξ»R.
- βp,A1,A2. R p A1 A2 β R (rc::p) (π.A1) (π.A2).
-
-definition compatible_sn: predicate (ptrβrelation term) β Ξ»R.
- βp,B1,B2,A. R p B1 B2 β R (sn::p) (@B1.A) (@B2.A).
-
-definition compatible_dx: predicate (ptrβrelation term) β Ξ»R.
- βp,B,A1,A2. R p A1 A2 β R (dx::p) (@B.A1) (@B.A2).
+++ /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/pointer.ma".
-
-(* POINTER LIST *************************************************************)
-
-(* Policy: pointer list metavariables: r, s *)
-definition ptrl: Type[0] β list ptr.
-
-(* Note: a "whd" computation contracts just redexes in the whd *)
-definition is_whd: predicate ptrl β All β¦ in_whd.
-
-lemma is_whd_dx: βs. is_whd s β is_whd (dx:::s).
-#s elim s -s //
-#p #s #IHs * /3 width=1/
-qed.
-
-lemma is_whd_append: βr. is_whd r β βs. is_whd s β is_whd (r@s).
-#r elim r -r //
-#q #r #IHr * /3 width=1/
-qed.
-
-definition ho_compatible_rc: predicate (ptrlβrelation term) β Ξ»R.
- βs,A1,A2. R s A1 A2 β R (rc:::s) (π.A1) (π.A2).
-
-definition ho_compatible_sn: predicate (ptrlβrelation term) β Ξ»R.
- βs,B1,B2,A. R s B1 B2 β R (sn:::s) (@B1.A) (@B2.A).
-
-definition ho_compatible_dx: predicate (ptrlβrelation term) β Ξ»R.
- βs,B,A1,A2. R s A1 A2 β R (dx:::s) (@B.A1) (@B.A2).
-
-lemma lstar_compatible_rc: βR. compatible_rc R β ho_compatible_rc (lstar β¦ R).
-#R #HR #s #A1 #A2 #H @(lstar_ind_l ????????? H) -s -A1 // /3 width=3/
-qed.
-
-lemma lstar_compatible_sn: βR. compatible_sn R β ho_compatible_sn (lstar β¦ R).
-#R #HR #s #B1 #B2 #A #H @(lstar_ind_l ????????? H) -s -B1 // /3 width=3/
-qed.
-
-lemma lstar_compatible_dx: βR. compatible_dx R β ho_compatible_dx (lstar β¦ R).
-#R #HR #s #B #A1 #A2 #H @(lstar_ind_l ????????? H) -s -A1 // /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/pointer_list.ma".
-include "terms/pointer_order.ma".
-
-(* STANDARD POINTER LIST ****************************************************)
-
-(* Note: to us, a "normal" computation contracts redexes in non-decreasing positions *)
-definition is_standard: predicate ptrl β Allr β¦ ple.
-
-lemma is_standard_compatible: βc,s. is_standard s β is_standard (c:::s).
-#c #s elim s -s // #p * //
-#q #s #IHs * /3 width=1/
-qed.
-
-lemma is_standard_cons: βp,s. is_standard s β is_standard ((dx::p)::sn:::s).
-#p #s elim s -s // #q1 * /2 width=1/
-#q2 #s #IHs * /4 width=1/
-qed.
-
-lemma is_standard_append: βr. is_standard r β βs. is_standard s β is_standard ((dx:::r)@sn:::s).
-#r elim r -r /3 width=1/ #p * /2 width=1/
-#q #r #IHr * /3 width=1/
-qed.
-
-theorem is_whd_is_standard: βs. is_whd s β is_standard s.
-#s elim s -s // #p * //
-#q #s #IHs * /3 width=1/
-qed.
-
-lemma is_standard_in_whd: βp. in_whd p β βs. is_standard s β is_standard (p::s).
-#p #Hp * // /3 width=1/
-qed.
-
-theorem is_whd_is_standard_trans: βr. is_whd r β βs. is_standard s β is_standard (r@s).
-#r elim r -r // #p *
-[ #_ * /2 width=1/
-| #q #r #IHr * /3 width=1/
-]
-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/pointer.ma".
-
-(* POINTER ORDER ************************************************************)
-
-(* Note: precedence relation on redex pointers: p βΊ q
- to serve as base for the order relations: p < q and p β€ q *)
-inductive pprec: relation ptr β
-| pprec_nil : βc,q. pprec (β) (c::q)
-| ppprc_rc : βp,q. pprec (dx::p) (rc::q)
-| ppprc_sn : βp,q. pprec (rc::p) (sn::q)
-| pprec_comp: βc,p,q. pprec p q β pprec (c::p) (c::q)
-| pprec_skip: pprec (dx::β) β
-.
-
-interpretation "'precedes' on pointers"
- 'prec p q = (pprec p q).
-
-(* Note: this should go to core_notation *)
-notation "hvbox(a break βΊ b)"
- non associative with precedence 45
- for @{ 'prec $a $b }.
-
-lemma pprec_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
-| #p #q * #H destruct
-| #c #p #q #_ #IHpq * #H destruct /3 width=1/
-]
-qed-.
-
-(* Note: this is p < q *)
-definition plt: relation ptr β TC β¦ pprec.
-
-interpretation "'less than' on redex pointers"
- 'lt p q = (plt p q).
-
-lemma plt_step_rc: βp,q. p βΊ q β p < q.
-/2 width=1/
-qed.
-
-lemma plt_nil: βc,p. β < c::p.
-/2 width=1/
-qed.
-
-lemma plt_skip: dx::β < β.
-/2 width=1/
-qed.
-
-lemma plt_comp: βc,p,q. p < q β c::p < c::q.
-#c #p #q #H elim H -q /3 width=1/ /3 width=3/
-qed.
-
-theorem plt_trans: transitive β¦ plt.
-/2 width=3/
-qed-.
-
-lemma plt_refl: βp. p < p.
-#p elim p -p /2 width=1/
-@(plt_trans β¦ (dx::β)) //
-qed.
-
-(* Note: this is p β€ q *)
-definition ple: relation ptr β star β¦ pprec.
-
-interpretation "'less or equal to' on redex pointers"
- 'leq p q = (ple p q).
-
-lemma ple_step_rc: βp,q. p βΊ q β p β€ q.
-/2 width=1/
-qed.
-
-lemma ple_step_sn: βp1,p,p2. p1 βΊ p β p β€ p2 β p1 β€ p2.
-/2 width=3/
-qed-.
-
-lemma ple_rc: βp,q. dx::p β€ rc::q.
-/2 width=1/
-qed.
-
-lemma ple_sn: βp,q. rc::p β€ sn::q.
-/2 width=1/
-qed.
-
-lemma ple_skip: dx::β β€ β.
-/2 width=1/
-qed.
-
-lemma ple_nil: βp. β β€ p.
-* // /2 width=1/
-qed.
-
-lemma ple_comp: βp1,p2. p1 β€ p2 β βc. (c::p1) β€ (c::p2).
-#p1 #p2 #H elim H -p2 // /3 width=3/
-qed.
-
-lemma ple_skip_ple: βp. p β€ β β dx::p β€ β.
-#p #H @(star_ind_l ??????? H) -p //
-#p #q #Hpq #_ #H @(ple_step_sn β¦ H) -H /2 width=1/
-qed.
-
-theorem ple_trans: transitive β¦ ple.
-/2 width=3/
-qed-.
-
-lemma ple_cons: βp,q. dx::p β€ sn::q.
-#p #q
-@(ple_trans β¦ (rc::q)) /2 width=1/
-qed.
-
-lemma ple_dichotomy: βp1,p2:ptr. p1 β€ p2 β¨ p2 β€ p1.
-#p1 elim p1 -p1
-[ * /2 width=1/
-| #c1 #p1 #IHp1 * /2 width=1/
- * #p2 cases c1 -c1 /2 width=1/
- elim (IHp1 p2) -IHp1 /3 width=1/
-]
-qed-.
-
-lemma in_whd_ple_nil: βp. in_whd p β p β€ β.
-#p #H @(in_whd_ind β¦ H) -p // /2 width=1/
-qed.
-
-theorem in_whd_ple: βp. in_whd p β βq. p β€ q.
-#p #H @(in_whd_ind β¦ H) -p //
-#p #_ #IHp * /3 width=1/ * #q /2 width=1/
-qed.
-
-lemma ple_nil_inv_in_whd: βp. p β€ β β in_whd p.
-#p #H @(star_ind_l ??????? H) -p // /2 width=3 by pprec_fwd_in_whd/
-qed-.
-
-lemma ple_inv_in_whd: βp. (βq. p β€ q) β in_whd p.
-/2 width=1 by ple_nil_inv_in_whd/
-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/pointer_list.ma".
-
-(* POINTER TREE *************************************************************)
-
-(* Policy: pointer tree metavariables: P, Q *)
-(* Note: this is a binary tree on pointer sequences *)
-inductive ptrt: Type[0] β
-| tnil : ptrt
-| tcons: ptrl β ptrt β ptrt β ptrt
-.
-
-let rec length (P:ptrt) on P β match P with
-[ tnil β 0
-| tcons s Q1 Q2 β length Q2 + length Q1 + |s|
-].
-
-interpretation "pointer tree length" 'card P = (length P).
--- /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/parallel_computation.ma".
+
+(* SEQUENTIAL COMPUTATION (MULTISTEP) ***************************************)
+
+definition sreds: relation term β star β¦ sred.
+
+interpretation "sequential computation"
+ 'SeqRedStar M N = (sreds M N).
+
+lemma sreds_refl: reflexive β¦ sreds.
+//
+qed.
+
+lemma sreds_step_sn: βM1,M. M1 β¦ M β βM2. M β¦* M2 β M1 β¦* M2.
+/2 width=3/
+qed-.
+
+lemma sreds_step_dx: βM1,M. M1 β¦* M β βM2. M β¦ M2 β M1 β¦* M2.
+/2 width=3/
+qed-.
+
+lemma sreds_step_rc: βM1,M2. M1 β¦ M2 β M1 β¦* M2.
+/2 width=1/
+qed.
+
+lemma lsred_compatible_abst: compatible_abst sreds.
+/3 width=1/
+qed.
+
+lemma sreds_compatible_sn: compatible_sn sreds.
+/3 width=1/
+qed.
+
+lemma sreds_compatible_dx: compatible_dx sreds.
+/3 width=1/
+qed.
+
+lemma sreds_compatible_appl: compatible_appl sreds.
+/3 width=3/
+qed.
+
+lemma sreds_lift: liftable sreds.
+/2 width=1/
+qed.
+
+lemma sreds_inv_lift: deliftable_sn sreds.
+/3 width=3 by star_deliftable_sn, sred_inv_lift/
+qed-.
+
+lemma sreds_dsubst: dsubstable_dx sreds.
+/2 width=1/
+qed.
+
+theorem sreds_trans: transitive β¦ sreds.
+/2 width=3 by trans_star/
+qed-.
+
+(* Note: the substitution should be unparentesized *)
+lemma sreds_compatible_beta: βB1,B2. B1 β¦* B2 β βA1,A2. A1 β¦* A2 β
+ @B1.π.A1 β¦* ([βB2] A2).
+#B1 #B2 #HB12 #A1 #A2 #HA12
+@(sreds_trans β¦ (@B2.π.A1)) /2 width=1/ -B1
+@(sreds_step_dx β¦ (@B2.π.A2)) // /3 width=1/
+qed.
+
+theorem sreds_preds: βM1,M2. M1 β¦* M2 β M1 β€* M2.
+#M1 #M2 #H @(star_ind_l ??????? H) -M1 //
+#M1 #M #HM1 #_ #IHM2
+@(preds_step_sn β¦ IHM2) -M2 /2 width=2/
+qed.
+
+lemma pred_sreds: βM1,M2. M1 β€ M2 β M1 β¦* M2.
+#M1 #M2 #H elim H -M1 -M2 // /2 width=1/
+qed-.
+
+theorem preds_sreds: βM1,M2. M1 β€* M2 β M1 β¦* M2.
+#M1 #M2 #H elim H -M2 //
+#M #M2 #_ #HM2 #HM1
+lapply (pred_sreds β¦ HM2) -HM2 #HM2
+@(sreds_trans β¦ HM1 β¦ HM2)
+qed-.
+
+theorem sreds_conf: βM0,M1. M0 β¦* M1 β βM2. M0 β¦* M2 β
+ ββM. M1 β¦* M & M2 β¦* M.
+#M0 #M1 #HM01 #M2 #HM02
+lapply (sreds_preds β¦ HM01) #HM01
+lapply (sreds_preds β¦ HM02) #HM02
+elim (preds_conf β¦ HM01 β¦ HM02) -M0 #M #HM1 #HM2
+lapply (preds_sreds β¦ HM1) -HM1
+lapply (preds_sreds β¦ HM2) -HM2 /2 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/multiplicity.ma".
+
+(* SEQUENTIAL REDUCTION (SINGLE STEP) ***************************************)
+
+(* Note: the application "(A B)" is represented by "@B.A" following:
+ F. Kamareddine and R.P. Nederpelt: "A useful Ξ»-notation".
+ Theoretical Computer Science 155(1), Elsevier (1996), pp. 85-109.
+*)
+inductive sred: relation term β
+| sred_beta : βB,A. sred (@B.π.A) ([βB]A)
+| sred_abst : βA1,A2. sred A1 A2 β sred (π.A1) (π.A2)
+| sred_appl_sn: βB1,B2,A. sred B1 B2 β sred (@B1.A) (@B2.A)
+| sred_appl_dx: βB,A1,A2. sred A1 A2 β sred (@B.A1) (@B.A2)
+.
+
+interpretation "sequential reduction"
+ 'SeqRed M N = (sred M N).
+
+lemma sred_inv_vref: βM,N. M β¦ N β βi. #i = M β β₯.
+#M #N * -M -N
+[ #B #A #i #H destruct
+| #A1 #A2 #_ #i #H destruct
+| #B1 #B2 #A #_ #i #H destruct
+| #B #A1 #A2 #_ #i #H destruct
+]
+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
+| #A1 #A2 #HA12 #C1 #H destruct /2 width=3/
+| #B1 #B2 #A #_ #C1 #H destruct
+| #B #A1 #A2 #_ #C1 #H destruct
+]
+qed-.
+
+lemma sred_inv_appl: βM,N. M β¦ N β βD,C. @D.C = M β
+ β¨β¨ (ββC0. π.C0 = C & [βD] C0 = N)
+ | (ββD0. D β¦ D0 & @D0.C = N)
+ | (ββC0. C β¦ C0 & @D.C0 = N).
+#M #N * -M -N
+[ #B #A #D #C #H destruct /3 width=3/
+| #A1 #A2 #_ #D #C #H destruct
+| #B1 #B2 #A #HB12 #D #C #H destruct /3 width=3/
+| #B #A1 #A2 #HA12 #D #C #H destruct /3 width=3/
+]
+qed-.
+
+lemma sred_fwd_mult: βM,N. M β¦ N β β―{N} < β―{M} * β―{M}.
+#M #N #H elim H -M -N
+[ #B #A @(le_to_lt_to_lt β¦ (β―{A}*β―{B})) //
+ normalize /3 width=1 by lt_minus_to_plus_r, lt_times/ (**) (* auto: too slow without trace *)
+| //
+| #B #D #A #_ #IHBD
+ @(lt_to_le_to_lt β¦ (β―{B}*β―{B}+β―{A})) [ /2 width=1/ ] -D
+| #B #A #C #_ #IHAC
+ @(lt_to_le_to_lt β¦ (β―{B}+β―{A}*β―{A})) [ /2 width=1/ ] -C
+]
+@(transitive_le β¦ (β―{B}*β―{B}+β―{A}*β―{A})) [ /2 width=1/ ]
+>distributive_times_plus normalize /2 width=1/
+qed-.
+
+lemma sred_lift: liftable sred.
+#h #M1 #M2 #H elim H -M1 -M2 normalize /2 width=1/
+#B #A #d <dsubst_lift_le //
+qed.
+
+lemma sred_inv_lift: deliftable_sn sred.
+#h #N1 #N2 #H elim H -N1 -N2
+[ #D #C #d #M1 #H
+ elim (lift_inv_appl β¦ H) -H #B #M #H0 #HM #H destruct
+ elim (lift_inv_abst β¦ HM) -HM #A #H0 #H destruct /3 width=3/
+| #C1 #C2 #_ #IHC12 #d #M1 #H
+ elim (lift_inv_abst β¦ H) -H #A1 #HAC1 #H
+ elim (IHC12 β¦ HAC1) -C1 #A2 #HA12 #HAC2 destruct
+ @(ex2_intro β¦ (π.A2)) // /2 width=1/
+| #D1 #D2 #C1 #_ #IHD12 #d #M1 #H
+ elim (lift_inv_appl β¦ H) -H #B1 #A #HBD1 #H1 #H2
+ elim (IHD12 β¦ HBD1) -D1 #B2 #HB12 #HBD2 destruct
+ @(ex2_intro β¦ (@B2.A)) // /2 width=1/
+| #D1 #C1 #C2 #_ #IHC12 #d #M1 #H
+ elim (lift_inv_appl β¦ H) -H #B #A1 #H1 #HAC1 #H2
+ elim (IHC12 β¦ HAC1) -C1 #A2 #HA12 #HAC2 destruct
+ @(ex2_intro β¦ (@B.A2)) // /2 width=1/
+]
+qed-.
+
+lemma sred_dsubst: dsubstable_dx sred.
+#D1 #M1 #M2 #H elim H -M1 -M2 normalize /2 width=1/
+#D2 #A #d >dsubst_dsubst_ge //
+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/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.
+++ /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/labeled_sequential_computation.ma".
-include "terms/pointer_list_standard.ma".
-
-(* KASHIMA'S "ST" COMPUTATION ***********************************************)
-
-(* Note: this is the "standard" computation of:
- R. Kashima: "A proof of the Standization Theorem in Ξ»-Calculus". Typescript note, (2000).
-*)
-inductive st: relation term β
-| st_vref: βs,M,i. is_whd s β M β¦*[s] #i β st M (#i)
-| st_abst: βs,M,A1,A2. is_whd s β M β¦*[s] π.A1 β st A1 A2 β st M (π.A2)
-| st_appl: βs,M,B1,B2,A1,A2. is_whd s β M β¦*[s] @B1.A1 β st B1 B2 β st A1 A2 β st M (@B2.A2)
-.
-
-interpretation "'st' computation"
- 'Std M N = (st M N).
-
-notation "hvbox( M β’β€* break term 46 N )"
- non associative with precedence 45
- for @{ 'Std $M $N }.
-
-lemma st_inv_lref: βM,N. M β’β€* N β βj. #j = N β
- ββs. is_whd s & M β¦*[s] #j.
-#M #N * -M -N
-[ /2 width=3/
-| #s #M #A1 #A2 #_ #_ #_ #j #H destruct
-| #s #M #B1 #B2 #A1 #A2 #_ #_ #_ #_ #j #H destruct
-]
-qed-.
-
-lemma st_inv_abst: βM,N. M β’β€* N β βC2. π.C2 = N β
- ββs,C1. is_whd s & M β¦*[s] π.C1 & C1 β’β€* C2.
-#M #N * -M -N
-[ #s #M #i #_ #_ #C2 #H destruct
-| #s #M #A1 #A2 #Hs #HM #A12 #C2 #H destruct /2 width=5/
-| #s #M #B1 #B2 #A1 #A2 #_ #_ #_ #_ #C2 #H destruct
-]
-qed-.
-
-lemma st_inv_appl: βM,N. M β’β€* N β βD2,C2. @D2.C2 = N β
- ββs,D1,C1. is_whd s & M β¦*[s] @D1.C1 & D1 β’β€* D2 & C1 β’β€* C2.
-#M #N * -M -N
-[ #s #M #i #_ #_ #D2 #C2 #H destruct
-| #s #M #A1 #A2 #_ #_ #_ #D2 #C2 #H destruct
-| #s #M #B1 #B2 #A1 #A2 #Hs #HM #HB12 #HA12 #D2 #C2 #H destruct /2 width=7/
-]
-qed-.
-
-lemma st_refl: reflexive β¦ st.
-#M elim M -M /2 width=3/ /2 width=5/ /2 width=7/
-qed.
-
-lemma st_step_sn: βN1,N2. N1 β’β€* N2 β βs,M. is_whd s β M β¦*[s] N1 β M β’β€* N2.
-#N1 #N2 #H elim H -N1 -N2
-[ #r #N #i #Hr #HN #s #M #Hs #HMN
- lapply (lsreds_trans β¦ HMN β¦ HN) -N /3 width=3/
-| #r #N #C1 #C2 #Hr #HN #_ #IHC12 #s #M #Hs #HMN
- lapply (lsreds_trans β¦ HMN β¦ HN) -N /3 width=7/
-| #r #N #D1 #D2 #C1 #C2 #Hr #HN #_ #_ #IHD12 #IHC12 #s #M #Hs #HMN
- lapply (lsreds_trans β¦ HMN β¦ HN) -N /3 width=9/
-]
-qed-.
-
-lemma st_step_rc: βs,M1,M2. is_whd s β M1 β¦*[s] M2 β M1 β’β€* M2.
-/3 width=5 by st_step_sn/
-qed.
-
-lemma st_lift: liftable st.
-#h #M1 #M2 #H elim H -M1 -M2
-[ /3 width=3/
-| #s #M #A1 #A2 #Hs #HM #_ #IHA12 #d
- @(st_abst β¦ Hs) [2: @(lsreds_lift β¦ HM) | skip ] -M // (**) (* auto fails here *)
-| #s #M #B1 #B2 #A1 #A2 #Hs #HM #_ #_ #IHB12 #IHA12 #d
- @(st_appl β¦ Hs) [3: @(lsreds_lift β¦ HM) |1,2: skip ] -M // (**) (* auto fails here *)
-]
-qed.
-
-lemma st_inv_lift: deliftable_sn st.
-#h #N1 #N2 #H elim H -N1 -N2
-[ #s #N1 #i #Hs #HN1 #d #M1 #HMN1
- elim (lsreds_inv_lift β¦ HN1 β¦ HMN1) -N1 /3 width=3/
-| #s #N1 #C1 #C2 #Hs #HN1 #_ #IHC12 #d #M1 #HMN1
- elim (lsreds_inv_lift β¦ HN1 β¦ HMN1) -N1 #M2 #HM12 #HM2
- elim (lift_inv_abst β¦ HM2) -HM2 #A1 #HAC1 #HM2 destruct
- elim (IHC12 ???) -IHC12 [4: // |2,3: skip ] #A2 #HA12 #HAC2 destruct (**) (* simplify line *)
- @(ex2_intro β¦ (π.A2)) // /2 width=5/
-| #s #N1 #D1 #D2 #C1 #C2 #Hs #HN1 #_ #_ #IHD12 #IHC12 #d #M1 #HMN1
- elim (lsreds_inv_lift β¦ HN1 β¦ HMN1) -N1 #M2 #HM12 #HM2
- elim (lift_inv_appl β¦ HM2) -HM2 #B1 #A1 #HBD1 #HAC1 #HM2 destruct
- elim (IHD12 ???) -IHD12 [4: // |2,3: skip ] #B2 #HB12 #HBD2 destruct (**) (* simplify line *)
- elim (IHC12 ???) -IHC12 [4: // |2,3: skip ] #A2 #HA12 #HAC2 destruct (**) (* simplify line *)
- @(ex2_intro β¦ (@B2.A2)) // /2 width=7/
-]
-qed-.
-
-lemma st_dsubst: dsubstable st.
-#N1 #N2 #HN12 #M1 #M2 #H elim H -M1 -M2
-[ #s #M #i #Hs #HM #d elim (lt_or_eq_or_gt i d) #Hid
- [ lapply (lsreds_dsubst β¦ N1 β¦ HM d) -HM
- >(dsubst_vref_lt β¦ Hid) >(dsubst_vref_lt β¦ Hid) /2 width=3/
- | destruct >dsubst_vref_eq
- @(st_step_sn (β[0,i]N1) β¦ s) /2 width=1/
- | lapply (lsreds_dsubst β¦ N1 β¦ HM d) -HM
- >(dsubst_vref_gt β¦ Hid) >(dsubst_vref_gt β¦ Hid) /2 width=3/
- ]
-| #s #M #A1 #A2 #Hs #HM #_ #IHA12 #d
- lapply (lsreds_dsubst β¦ N1 β¦ HM d) -HM /2 width=5/ (**) (* auto needs some help here *)
-| #s #M #B1 #B2 #A1 #A2 #Hs #HM #_ #_ #IHB12 #IHA12 #d
- lapply (lsreds_dsubst β¦ N1 β¦ HM d) -HM /2 width=7/ (**) (* auto needs some help here *)
-]
-qed.
-
-lemma st_step_dx: βp,M,M2. M β¦[p] M2 β βM1. M1 β’β€* M β M1 β’β€* M2.
-#p #M #M2 #H elim H -p -M -M2
-[ #B #A #M1 #H
- elim (st_inv_appl β¦ H ???) -H [4: // |2,3: skip ] #s #B1 #M #Hs #HM1 #HB1 #H (**) (* simplify line *)
- elim (st_inv_abst β¦ H ??) -H [3: // |2: skip ] #r #A1 #Hr #HM #HA1 (**) (* simplify line *)
- lapply (lsreds_trans β¦ HM1 β¦ (dx:::r) (@B1.π.A1) ?) /2 width=1/ -M #HM1
- lapply (lsreds_step_dx β¦ HM1 (β) ([βB1]A1) ?) -HM1 // #HM1
- @(st_step_sn β¦ HM1) /2 width=1/ /4 width=1/
-| #p #A #A2 #_ #IHA2 #M1 #H
- elim (st_inv_abst β¦ H ??) -H [3: // |2: skip ] /3 width=5/ (**) (* simplify line *)
-| #p #B #B2 #A #_ #IHB2 #M1 #H
- elim (st_inv_appl β¦ H ???) -H [4: // |2,3: skip ] /3 width=7/ (**) (* simplify line *)
-| #p #B #A #A2 #_ #IHA2 #M1 #H
- elim (st_inv_appl β¦ H ???) -H [4: // |2,3: skip ] /3 width=7/ (**) (* simplify line *)
-]
-qed-.
-
-lemma st_lsreds: βs,M1,M2. M1 β¦*[s] M2 β M1 β’β€* M2.
-#s #M1 #M2 #H @(lstar_ind_r ????????? H) -s -M2 // /2 width=4 by st_step_dx/
-qed.
-
-lemma st_inv_lsreds_is_standard: βM,N. M β’β€* N β
- ββr. M β¦*[r] N & is_standard r.
-#M #N #H elim H -M -N
-[ #s #M #i #Hs #HM
- lapply (is_whd_is_standard β¦ Hs) -Hs /2 width=3/
-| #s #M #A1 #A2 #Hs #HM #_ * #r #HA12 #Hr
- lapply (lsreds_trans β¦ HM (rc:::r) (π.A2) ?) /2 width=1/ -A1 #HM
- @(ex2_intro β¦ HM) -M -A2 /3 width=1/
-| #s #M #B1 #B2 #A1 #A2 #Hs #HM #_ #_ * #rb #HB12 #Hrb * #ra #HA12 #Hra
- lapply (lsreds_trans β¦ HM (dx:::ra) (@B1.A2) ?) /2 width=1/ -A1 #HM
- lapply (lsreds_trans β¦ HM (sn:::rb) (@B2.A2) ?) /2 width=1/ -B1 #HM
- @(ex2_intro β¦ HM) -M -B2 -A2 >associative_append /3 width=1/
-]
-qed-.
-
-theorem st_trans: transitive β¦ st.
-#M1 #M #M2 #HM1 #HM2
-elim (st_inv_lsreds_is_standard β¦ HM1) -HM1 #s1 #HM1 #_
-elim (st_inv_lsreds_is_standard β¦ HM2) -HM2 #s2 #HM2 #_
-lapply (lsreds_trans β¦ HM1 β¦ HM2) -M /2 width=2/
-qed-.
-
-theorem lsreds_standard: βs,M,N. M β¦*[s] N β ββr. M β¦*[r] N & is_standard r.
-#s #M #N #H
-@st_inv_lsreds_is_standard /2 width=2/
-qed-.
-
-(* Note: we use "lapply (rewrite_r ?? is_whd β¦ Hq)" (procedural)
- in place of "cut (is_whd (q::r)) [ >Hq ]" (declarative)
-*)
-lemma st_lsred_swap: βp. in_whd p β βN1,N2. N1 β¦[p] N2 β βM1. M1 β’β€* N1 β
- ββq,M2. in_whd q & M1 β¦[q] M2 & M2 β’β€* N2.
-#p #H @(in_whd_ind β¦ H) -p
-[ #N1 #N2 #H1 #M1 #H2
- elim (lsred_inv_nil β¦ H1 ?) -H1 // #D #C #HN1 #HN2
- elim (st_inv_appl β¦ H2 β¦ HN1) -N1 #s1 #D1 #N #Hs1 #HM1 #HD1 #H
- elim (st_inv_abst β¦ H ??) -H [3: // |2: skip ] #s2 #C1 #Hs2 #HN #HC1 (**) (* simplify line *)
- lapply (lsreds_trans β¦ HM1 β¦ (dx:::s2) (@D1.π.C1) ?) /2 width=1/ -N #HM1
- lapply (lsreds_step_dx β¦ HM1 (β) ([βD1]C1) ?) -HM1 // #HM1
- elim (lsreds_inv_pos β¦ HM1 ?) -HM1
- [2: >length_append normalize in β’ (??(??%)); // ]
- #q #r #M #Hq #HM1 #HM
- lapply (rewrite_r ?? is_whd β¦ Hq) -Hq /4 width=1/ -s1 -s2 * #Hq #Hr
- @(ex3_2_intro β¦ HM1) -M1 // -q
- @(st_step_sn β¦ HM) /2 width=1/
-| #p #_ #IHp #N1 #N2 #H1 #M1 #H2
- elim (lsred_inv_dx β¦ H1 ??) -H1 [3: // |2: skip ] #D #C1 #C2 #HC12 #HN1 #HN2 (**) (* simplify line *)
- elim (st_inv_appl β¦ H2 β¦ HN1) -N1 #s #B #A1 #Hs #HM1 #HBD #HAC1
- elim (IHp β¦ HC12 β¦ HAC1) -p -C1 #p #C1 #Hp #HAC1 #HC12
- lapply (lsreds_step_dx β¦ HM1 (dx::p) (@B.C1) ?) -HM1 /2 width=1/ -A1 #HM1
- elim (lsreds_inv_pos β¦ HM1 ?) -HM1
- [2: >length_append normalize in β’ (??(??%)); // ]
- #q #r #M #Hq #HM1 #HM
- lapply (rewrite_r ?? is_whd β¦ Hq) -Hq /4 width=1/ -p -s * #Hq #Hr
- @(ex3_2_intro β¦ HM1) -M1 // -q /2 width=7/
-]
-qed-.
-
-theorem lsreds_lsred_swap: βs,M1,N1. M1 β¦*[s] N1 β
- βp,N2. in_whd p β N1 β¦[p] N2 β
- ββq,r,M2. in_whd q & M1 β¦[q] M2 & M2 β¦*[r] N2 &
- is_standard (q::r).
-#s #M1 #N1 #HMN1 #p #N2 #Hp #HN12
-lapply (st_lsreds β¦ HMN1) -s #HMN1
-elim (st_lsred_swap β¦ Hp β¦ HN12 β¦ HMN1) -p -N1 #q #M2 #Hq #HM12 #HMN2
-elim (st_inv_lsreds_is_standard β¦ HMN2) -HMN2 /3 width=8/
-qed-.
(* Initial invocation: - Patience on us to gain peace and perfection! - *)
-include "preamble.ma".
-include "notation.ma".
+include "background/preamble.ma".
+include "background/notation.ma".
(* TERM STRUCTURE ***********************************************************)
<key name="rt_base_dir">$(MATITA_RT_BASE_DIR)</key>
</section>
<section name="xoa">
- <key name="output_dir">contribs/lambda/</key>
+ <key name="output_dir">contribs/lambda/background/</key>
<key name="objects">xoa</key>
<key name="notations">xoa_notation</key>
<key name="include">basics/pts.ma</key>
+++ /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 *)
-(* *)
-(**************************************************************************)
-
-(* This file was generated by xoa.native: do not edit *********************)
-
-include "basics/pts.ma".
-
-(* multiple existental quantifier (2, 2) *)
-
-inductive ex2_2 (A0,A1:Type[0]) (P0,P1:A0βA1βProp) : Prop β
- | ex2_2_intro: βx0,x1. P0 x0 x1 β P1 x0 x1 β ex2_2 ? ? ? ?
-.
-
-interpretation "multiple existental quantifier (2, 2)" 'Ex P0 P1 = (ex2_2 ? ? P0 P1).
-
-(* multiple existental quantifier (2, 3) *)
-
-inductive ex2_3 (A0,A1,A2:Type[0]) (P0,P1:A0βA1βA2βProp) : Prop β
- | ex2_3_intro: βx0,x1,x2. P0 x0 x1 x2 β P1 x0 x1 x2 β ex2_3 ? ? ? ? ?
-.
-
-interpretation "multiple existental quantifier (2, 3)" 'Ex P0 P1 = (ex2_3 ? ? ? P0 P1).
-
-(* multiple existental quantifier (3, 2) *)
-
-inductive ex3_2 (A0,A1:Type[0]) (P0,P1,P2:A0βA1βProp) : Prop β
- | ex3_2_intro: βx0,x1. P0 x0 x1 β P1 x0 x1 β P2 x0 x1 β ex3_2 ? ? ? ? ?
-.
-
-interpretation "multiple existental quantifier (3, 2)" 'Ex P0 P1 P2 = (ex3_2 ? ? P0 P1 P2).
-
-(* multiple existental quantifier (3, 3) *)
-
-inductive ex3_3 (A0,A1,A2:Type[0]) (P0,P1,P2:A0βA1βA2βProp) : Prop β
- | ex3_3_intro: βx0,x1,x2. P0 x0 x1 x2 β P1 x0 x1 x2 β P2 x0 x1 x2 β ex3_3 ? ? ? ? ? ?
-.
-
-interpretation "multiple existental quantifier (3, 3)" 'Ex P0 P1 P2 = (ex3_3 ? ? ? 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 β
- | or3_intro0: P0 β or3 ? ? ?
- | or3_intro1: P1 β or3 ? ? ?
- | or3_intro2: P2 β or3 ? ? ?
-.
-
-interpretation "multiple disjunction connective (3)" 'Or P0 P1 P2 = (or3 P0 P1 P2).
-
+++ /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 *)
-(* *)
-(**************************************************************************)
-
-(* This file was generated by xoa.native: do not edit *********************)
-
-(* multiple existental quantifier (2, 2) *)
-
-notation > "hvbox(ββ ident x0 , ident x1 break . term 19 P0 break & term 19 P1)"
- non associative with precedence 20
- for @{ 'Ex (Ξ»${ident x0}.Ξ»${ident x1}.$P0) (Ξ»${ident x0}.Ξ»${ident x1}.$P1) }.
-
-notation < "hvbox(ββ ident x0 , ident x1 break . term 19 P0 break & term 19 P1)"
- non associative with precedence 20
- for @{ 'Ex (Ξ»${ident x0}:$T0.Ξ»${ident x1}:$T1.$P0) (Ξ»${ident x0}:$T0.Ξ»${ident x1}:$T1.$P1) }.
-
-(* multiple existental quantifier (2, 3) *)
-
-notation > "hvbox(ββ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1)"
- non associative with precedence 20
- for @{ 'Ex (Ξ»${ident x0}.Ξ»${ident x1}.Ξ»${ident x2}.$P0) (Ξ»${ident x0}.Ξ»${ident x1}.Ξ»${ident x2}.$P1) }.
-
-notation < "hvbox(ββ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1)"
- 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, 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}.Ξ»${ident x1}.$P0) (Ξ»${ident x0}.Ξ»${ident x1}.$P1) (Ξ»${ident x0}.Ξ»${ident x1}.$P2) }.
-
-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.$P0) (Ξ»${ident x0}:$T0.Ξ»${ident x1}:$T1.$P1) (Ξ»${ident x0}:$T0.Ξ»${ident x1}:$T1.$P2) }.
-
-(* multiple existental quantifier (3, 3) *)
-
-notation > "hvbox(ββ ident x0 , ident x1 , ident x2 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}.$P0) (Ξ»${ident x0}.Ξ»${ident x1}.Ξ»${ident x2}.$P1) (Ξ»${ident x0}.Ξ»${ident x1}.Ξ»${ident x2}.$P2) }.
-
-notation < "hvbox(ββ ident x0 , ident x1 , ident x2 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 (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)"
- non associative with precedence 30
- for @{ 'Or $P0 $P1 $P2 }.
-
projects / helm.git / commitdiff