- delift started ...
- nnAuto: we removed an optimization that breaks lambda_delta
with Error _ ->
smart_apply_auto ("",0,t) eq_cache status
in
+(* FG: this optimization rules out some applications of
+ * lift_bind (from contribs/lambda_delta/Basic_2/substitution/lift.ma)
+ *
(* we compare the expected branching with the actual one and
prune the candidate when the latter is larger. The optimization
is meant to rule out stange applications of flexible terms,
^ (string_of_int res) ^ " vs. " ^ (string_of_int og_no)));
debug_print ~depth (lazy "strange application"); None)
else
- (incr candidate_no; Some ((!candidate_no,t),status))
+*) (incr candidate_no; Some ((!candidate_no,t),status))
with Error (msg,exn) -> debug_print ~depth (lazy "failed"); None
;;
(* Basic inversion lemmas ***************************************************)
+fact thom_inv_bind1_aux: βT1,T2. T1 β T2 β βI,W1,U1. T1 = π{I}W1.U1 β
+ ββW2,U2. I = Abst & T2 = π{Abst} W2. U2.
+#T1 #T2 * -T1 T2
+[ #J #I #W1 #U1 #H destruct
+| #V1 #V2 #T1 #T2 #I #W1 #U1 #H destruct -V1 T1 /2/
+| #V1 #V2 #T1 #T2 #H_ #_ #_ #I #W1 #U1 #H destruct
+]
+qed.
+
+lemma thom_inv_bind1: βI,W1,U1,T2. π{I}W1.U1 β T2 β
+ ββW2,U2. I = Abst & T2 = π{Abst} W2. U2.
+/2 width=5/ qed-.
+
+fact thom_inv_flat1_aux: βT1,T2. T1 β T2 β βI,W1,U1. T1 = π{I}W1.U1 β
+ ββW2,U2. U1 β U2 & π[U1] & π[U2] &
+ I = Appl & T2 = π{Appl} W2. U2.
+#T1 #T2 * -T1 T2
+[ #J #I #W1 #U1 #H destruct
+| #V1 #V2 #T1 #T2 #I #W1 #U1 #H destruct
+| #V1 #V2 #T1 #T2 #HT12 #HT1 #HT2 #I #W1 #U1 #H destruct -V1 T1 /2 width=5/
+]
+qed.
+
+lemma thom_inv_flat1: βI,W1,U1,T2. π{I}W1.U1 β T2 β
+ ββW2,U2. U1 β U2 & π[U1] & π[U2] &
+ I = Appl & T2 = π{Appl} W2. U2.
+/2/ qed-.
(* Basic_1: removed theorems 7:
iso_gen_sort iso_gen_lref iso_gen_head iso_refl iso_trans
+(**************************************************************************)
+(* ___ *)
+(* ||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 "Basic_2/grammar/thom.ma".
include "Basic_2/reducibility/tpr.ma".
(* CONTEXT-FREE WEAK HEAD NORMAL TERMS **************************************)
definition twhnf: term β Prop β
- NF β¦ tpr (thom β¦).
+ NF β¦ tpr thom.
interpretation
"context-free weak head normality (term)"
'WHdNormal T = (twhnf T).
+(* Basic inversion lemmas ***************************************************)
+
+lemma twhnf_inv_thom: βT. πββ[T] β T β T.
+normalize /2 depth=1/
+qed-.
+
(* Basic properties *********************************************************)
+
+lemma tpr_thom: βT1,T2. T1 β T2 β T1 β T1 β T1 β T2.
+#T1 #T2 #H elim H -T1 T2 //
+[ #I #V1 #V2 #T1 #T2 #_ #_ #_ #IHT12 #H
+ elim (thom_inv_flat1 β¦ H) -H #W2 #U2 #HT1U2 #HT1 #_ #H1 #H2 destruct -I T1 V1;
+ lapply (IHT12 HT1U2) -IHT12 HT1U2 #HUT2
+ lapply (simple_thom_repl_dx β¦ HUT2 HT1) /2 width=1/
+| #V1 #V2 #W #T1 #T2 #_ #_ #_ #_ #H
+ elim (thom_inv_flat1 β¦ H) -H #W2 #U2 #_ #H
+ elim (simple_inv_bind β¦ H)
+| #I #V1 #V2 #T1 #T #T2 #_ #_ #_ #_ #_ #H
+ elim (thom_inv_bind1 β¦ H) -H #W2 #U2 #H destruct -I //
+| #V2 #V1 #V #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #H
+ elim (thom_inv_flat1 β¦ H) -H #U1 #U2 #_ #H
+ elim (simple_inv_bind β¦ H)
+| #V #T #T1 #T2 #_ #_ #_ #H
+ elim (thom_inv_bind1 β¦ H) -H #W2 #U2 #H destruct
+| #V #T1 #T2 #_ #_ #H
+ elim (thom_inv_flat1 β¦ H) -H #W2 #U2 #_ #_ #_ #H destruct
+]
+qed.
+
+lemma twhnf_thom: βT. T β T β πββ[T].
+/2/ qed.
lemma tps_fwd_tw: βL,T1,T2,d,e. L β’ T1 [d, e] β« T2 β #[T1] β€ #[T2].
#L #T1 #T2 #d #e #H elim H normalize -H L T1 T2 d e
-[ //
-| /2/
-| /3 by monotonic_le_plus_l, le_plus/ (**) (* just /3/ is too slow *)
-| /3 by monotonic_le_plus_l, le_plus/ (**) (* just /3/ is too slow *)
-]
+/3 by monotonic_le_plus_l, le_plus/ (**) (* just /3/ is too slow *)
qed-.
(* Basic_1: removed theorems 25:
--- /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 "Basic_2/unfold/tpss.ma".
+
+(* DELIFT ON TERMS **********************************************************)
+
+definition delift: nat β nat β lenv β relation term β
+ Ξ»d,e,L,T1,T2. ββT. L β’ T1 [d, e] β«* T & β[d, e] T2 β‘ T.
+
+interpretation "delift (term)"
+ 'TSubst L T1 d e T2 = (delift d e L T1 T2).
+++ /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 "Basic_2/unfold/tpss.ma".
-
-(* SUBSTITUTION ON TERMS ****************************************************)
-
-definition tsubst: nat β nat β lenv β relation term β
- Ξ»d,e,L,T1,T2. ββT. L β’ T1 [d, e] β«* T & β[d, e] T2 β‘ T.
-
-interpretation "substitution (term)"
- 'TSubst L T1 d e T2 = (tsubst d e L T1 T2).
<key name="ex">4 2</key>
<key name="ex">4 3</key>
<key name="ex">4 4</key>
+ <key name="ex">5 2</key>
<key name="ex">5 3</key>
<key name="ex">5 4</key>
<key name="ex">6 4</key>
interpretation "multiple existental quantifier (4, 4)" 'Ex P0 P1 P2 P3 = (ex4_4 ? ? ? ? P0 P1 P2 P3).
+(* multiple existental quantifier (5, 2) *)
+
+inductive ex5_2 (A0,A1:Type[0]) (P0,P1,P2,P3,P4:A0βA1βProp) : Prop β
+ | ex5_2_intro: βx0,x1. P0 x0 x1 β P1 x0 x1 β P2 x0 x1 β P3 x0 x1 β P4 x0 x1 β ex5_2 ? ? ? ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (5, 2)" 'Ex P0 P1 P2 P3 P4 = (ex5_2 ? ? P0 P1 P2 P3 P4).
+
(* multiple existental quantifier (5, 3) *)
inductive ex5_3 (A0,A1,A2:Type[0]) (P0,P1,P2,P3,P4:A0βA1βA2βProp) : Prop β
non associative with precedence 20
for @{ 'Ex (Ξ»${ident x0}:$T0.Ξ»${ident x1}:$T1.Ξ»${ident x2}:$T2.Ξ»${ident x3}:$T3.$P0) (Ξ»${ident x0}:$T0.Ξ»${ident x1}:$T1.Ξ»${ident x2}:$T2.Ξ»${ident x3}:$T3.$P1) (Ξ»${ident x0}:$T0.Ξ»${ident x1}:$T1.Ξ»${ident x2}:$T2.Ξ»${ident x3}:$T3.$P2) (Ξ»${ident x0}:$T0.Ξ»${ident x1}:$T1.Ξ»${ident x2}:$T2.Ξ»${ident x3}:$T3.$P3) }.
+(* multiple existental quantifier (5, 2) *)
+
+notation > "hvbox(ββ ident x0 , ident x1 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)"
+ non associative with precedence 20
+ for @{ 'Ex (Ξ»${ident x0}.Ξ»${ident x1}.$P0) (Ξ»${ident x0}.Ξ»${ident x1}.$P1) (Ξ»${ident x0}.Ξ»${ident x1}.$P2) (Ξ»${ident x0}.Ξ»${ident x1}.$P3) (Ξ»${ident x0}.Ξ»${ident x1}.$P4) }.
+
+notation < "hvbox(ββ ident x0 , ident x1 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)"
+ 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) (Ξ»${ident x0}:$T0.Ξ»${ident x1}:$T1.$P3) (Ξ»${ident x0}:$T0.Ξ»${ident x1}:$T1.$P4) }.
+
(* multiple existental quantifier (5, 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 break & term 19 P4)"
projects / helm.git / commitdiff