]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/basic_2/etc/fpn/fsb_alt.etc
- ynat: some additions
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / etc / fpn / fsb_alt.etc
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "basic_2/notation/relations/btsnalt_5.ma".
16 include "basic_2/computation/fpbs_fpbs.ma".
17 include "basic_2/computation/fsb.ma".
18
19 (* "BIG TREE" STRONGLY NORMALIZING TERMS ************************************)
20
21 (* Note: alternative definition of fsb *)
22 inductive fsba (h) (g): relation3 genv lenv term ≝
23 | fsba_intro: ∀G1,L1,T1. (
24                  ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ →
25                  (⦃G1, L1, T1⦄ ⋕ ⦃G2, L2, T2⦄ → ⊥) → fsba h g G2 L2 T2
26               ) → fsba h g G1 L1 T1.
27
28 interpretation
29    "'big tree' strong normalization (closure) alternative"
30    'BTSNAlt h g G L T = (fsba h g G L T).
31
32 (* Basic eliminators ********************************************************)
33
34 theorem fsba_ind_alt: ∀h,g. ∀R: relation3 …. (
35                          ∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⦥⦥[h,g] T1 → (
36                             ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ →
37                             (⦃G1, L1, T1⦄ ⋕ ⦃G2, L2, T2⦄ → ⊥) → R G2 L2 T2
38                          ) → R G1 L1 T1
39                       ) →
40                       ∀G,L,T. ⦃G, L⦄ ⊢ ⦥⦥[h, g] T → R G L T.
41 #h #g #R #IH #G #L #T #H elim H -G -L -T
42 /5 width=1 by fsba_intro/
43 qed-.
44
45 (* Basic_properties *********************************************************)
46
47 fact fsba_intro_aux: ∀h,g,G1,L1,T1. (
48                         ∀G,G2,L,L2,T,T2. ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄ →
49                         ⦃G1, L1, T1⦄ ⋕ ⦃G, L, T⦄ →
50                         (⦃G1, L1, T1⦄ ⋕ ⦃G2, L2, T2⦄ → ⊥) → fsba h g G2 L2 T2
51                      ) → fsba h g G1 L1 T1.
52 /4 width=5 by fsba_intro/ qed-.
53
54 lemma fsba_fpbs_trans: ∀h,g,G1,L1,T1. ⦃G1, L1⦄ ⊢ ⦥⦥[h, g] T1 →
55                        ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → ⦃G2, L2⦄ ⊢ ⦥⦥[h, g] T2.
56 #h #g #G1 #L1 #T1 #H @(fsba_ind_alt … H) -G1 -L1 -T1
57 #G1 #L1 #T1 #H0 #IH0 #G #L #T #H1 @fsba_intro
58 #G2 #L2 #T2 #H2 #_ lapply (fpbs_trans … H1 … H2) -G -L -T
59 #H12 elim (bteq_dec G1 G2 L1 L2 T1 T2) /3 width=6 by fpb_fpbs/
60 -IH0 #H212 
61  
62
63  -H0 -H #H @(IH0 … H) -IH0 -H // @(fpbs_trans … H1 … H2)    
64
65 lemma fsba_intro_fpb: ∀h,g,G1,L1,T1. (
66                          ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄ →
67                          (⦃G1, L1, T1⦄ ⋕ ⦃G2, L2, T2⦄ → ⊥) → ⦃G2, L2⦄ ⊢ ⦥⦥[h, g] T2
68                       ) → ⦃G1, L1⦄ ⊢ ⦥⦥[h, g] T1.
69 #h #g #G1 #L1 #T1 #IH1 @fsba_intro_aux
70 #G #G2 #L #L2 #T #T2 #H @(fpbs_ind_dx … H) -G -L -T
71 [ #H1 #H2 -IH1 elim H2 -H2 //
72 | #G0 #G #L0 #L #T0 #T #H10 #H12 #IH2 #H210 #H212 elim (bteq_dec G1 G L1 L T1 T) 
73   [ -IH1 -H210 -H10 -H12 /3 width=1 by/
74   | -IH2 -H212 #H21 lapply (IH1 … H21) -IH1 -H21
75     [
76     | -H10 -H210 #H 
77 (*
78 (* Main inversion lemmas ****************************************************)
79
80 theorem fsba_inv_fsb: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⦥⦥[h, g] T → ⦃G, L⦄ ⊢ ⦥[h, g] T.
81 #h #g #G #L #T #H elim H -G -L -T
82 /5 width=12 by fsb_intro, fpb_fpbs, fpbc_fwd_fpb, fpbc_fwd_gen/
83 qed-.
84
85 (* Main properties **********************************************************)
86
87 theorem fsb_fsba: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⦥[h, g] T → ⦃G, L⦄ ⊢ ⦥⦥[h, g] T.
88 #h #g #G #L #T #H @(fsb_ind_alt … H) -G -L -T
89 /4 width=1 by fsba_intro_fpb/
90 qed.
91 (*
92 | fsba_intro: ∀G1,L1,T1. (
93                 ∀G2,L2,T2.  ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → fsb h g G2 L2 T2
94               ) → fsb h g G1 L1 T1
95 .
96
97
98
99 (****************************************************************************)
100
101 include "basic_2/substitution/fqup.ma".
102
103 lemma fsb_csx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → ⦃G, L⦄ ⊢ ⦥[h, g] T.
104 #h #g #G #L #T #H @(csx_ind … H) -T
105 *)*)