]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/static_2/s_computation/fqup.ma
Merge remote-tracking branch 'origin/matita-lablgtk3'
[helm.git] / matita / matita / contribs / lambdadelta / static_2 / s_computation / fqup.ma
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 "ground_2/lib/star.ma".
16 include "static_2/notation/relations/suptermplus_6.ma".
17 include "static_2/notation/relations/suptermplus_7.ma".
18 include "static_2/s_transition/fqu.ma".
19
20 (* PLUS-ITERATED SUPCLOSURE *************************************************)
21
22 definition fqup: bool → tri_relation genv lenv term ≝
23                  λb. tri_TC … (fqu b).
24
25 interpretation "extended plus-iterated structural successor (closure)"
26    'SupTermPlus b G1 L1 T1 G2 L2 T2 = (fqup b G1 L1 T1 G2 L2 T2).
27
28 interpretation "plus-iterated structural successor (closure)"
29    'SupTermPlus G1 L1 T1 G2 L2 T2 = (fqup true G1 L1 T1 G2 L2 T2).
30
31 (* Basic properties *********************************************************)
32
33 lemma fqu_fqup: ∀b,G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⬂[b] ⦃G2,L2,T2⦄ →
34                 ⦃G1,L1,T1⦄ ⬂+[b] ⦃G2,L2,T2⦄.
35 /2 width=1 by tri_inj/ qed.
36
37 lemma fqup_strap1: ∀b,G1,G,G2,L1,L,L2,T1,T,T2.
38                    ⦃G1,L1,T1⦄ ⬂+[b] ⦃G,L,T⦄ → ⦃G,L,T⦄ ⬂[b] ⦃G2,L2,T2⦄ →
39                    ⦃G1,L1,T1⦄ ⬂+[b] ⦃G2,L2,T2⦄.
40 /2 width=5 by tri_step/ qed.
41
42 lemma fqup_strap2: ∀b,G1,G,G2,L1,L,L2,T1,T,T2.
43                    ⦃G1,L1,T1⦄ ⬂[b] ⦃G,L,T⦄ → ⦃G,L,T⦄ ⬂+[b] ⦃G2,L2,T2⦄ →
44                    ⦃G1,L1,T1⦄ ⬂+[b] ⦃G2,L2,T2⦄.
45 /2 width=5 by tri_TC_strap/ qed.
46
47 lemma fqup_pair_sn: ∀b,I,G,L,V,T. ⦃G,L,②{I}V.T⦄ ⬂+[b] ⦃G,L,V⦄.
48 /2 width=1 by fqu_pair_sn, fqu_fqup/ qed.
49
50 lemma fqup_bind_dx: ∀p,I,G,L,V,T. ⦃G,L,ⓑ{p,I}V.T⦄ ⬂+[Ⓣ] ⦃G,L.ⓑ{I}V,T⦄.
51 /3 width=1 by fqu_bind_dx, fqu_fqup/ qed.
52
53 lemma fqup_clear: ∀p,I,G,L,V,T. ⦃G,L,ⓑ{p,I}V.T⦄ ⬂+[Ⓕ] ⦃G,L.ⓧ,T⦄.
54 /3 width=1 by fqu_clear, fqu_fqup/ qed.
55
56 lemma fqup_flat_dx: ∀b,I,G,L,V,T. ⦃G,L,ⓕ{I}V.T⦄ ⬂+[b] ⦃G,L,T⦄.
57 /2 width=1 by fqu_flat_dx, fqu_fqup/ qed.
58
59 lemma fqup_flat_dx_pair_sn: ∀b,I1,I2,G,L,V1,V2,T. ⦃G,L,ⓕ{I1}V1.②{I2}V2.T⦄ ⬂+[b] ⦃G,L,V2⦄.
60 /2 width=5 by fqu_pair_sn, fqup_strap1/ qed.
61
62 lemma fqup_bind_dx_flat_dx: ∀p,G,I1,I2,L,V1,V2,T. ⦃G,L,ⓑ{p,I1}V1.ⓕ{I2}V2.T⦄ ⬂+[Ⓣ] ⦃G,L.ⓑ{I1}V1,T⦄.
63 /2 width=5 by fqu_flat_dx, fqup_strap1/ qed.
64
65 lemma fqup_flat_dx_bind_dx: ∀p,I1,I2,G,L,V1,V2,T. ⦃G,L,ⓕ{I1}V1.ⓑ{p,I2}V2.T⦄ ⬂+[Ⓣ] ⦃G,L.ⓑ{I2}V2,T⦄.
66 /3 width=5 by fqu_bind_dx, fqup_strap1/ qed.
67
68 (* Basic eliminators ********************************************************)
69
70 lemma fqup_ind: ∀b,G1,L1,T1. ∀Q:relation3 ….
71                 (∀G2,L2,T2. ⦃G1,L1,T1⦄ ⬂[b] ⦃G2,L2,T2⦄ → Q G2 L2 T2) →
72                 (∀G,G2,L,L2,T,T2. ⦃G1,L1,T1⦄ ⬂+[b] ⦃G,L,T⦄ → ⦃G,L,T⦄ ⬂[b] ⦃G2,L2,T2⦄ → Q G L T → Q G2 L2 T2) →
73                 ∀G2,L2,T2. ⦃G1,L1,T1⦄ ⬂+[b] ⦃G2,L2,T2⦄ → Q G2 L2 T2.
74 #b #G1 #L1 #T1 #Q #IH1 #IH2 #G2 #L2 #T2 #H
75 @(tri_TC_ind … IH1 IH2 G2 L2 T2 H)
76 qed-.
77
78 lemma fqup_ind_dx: ∀b,G2,L2,T2. ∀Q:relation3 ….
79                    (∀G1,L1,T1. ⦃G1,L1,T1⦄ ⬂[b] ⦃G2,L2,T2⦄ → Q G1 L1 T1) →
80                    (∀G1,G,L1,L,T1,T. ⦃G1,L1,T1⦄ ⬂[b] ⦃G,L,T⦄ → ⦃G,L,T⦄ ⬂+[b] ⦃G2,L2,T2⦄ → Q G L T → Q G1 L1 T1) →
81                    ∀G1,L1,T1. ⦃G1,L1,T1⦄ ⬂+[b] ⦃G2,L2,T2⦄ → Q G1 L1 T1.
82 #b #G2 #L2 #T2 #Q #IH1 #IH2 #G1 #L1 #T1 #H
83 @(tri_TC_ind_dx … IH1 IH2 G1 L1 T1 H)
84 qed-.
85
86 (* Advanced properties ******************************************************)
87
88 lemma fqup_zeta (b) (p) (I) (G) (K) (V):
89                 ∀T1,T2. ⇧*[1]T2 ≘ T1 → ⦃G,K,ⓑ{p,I}V.T1⦄ ⬂+[b] ⦃G,K,T2⦄.
90 * /4 width=5 by fqup_strap2, fqu_fqup, fqu_drop, fqu_clear, fqu_bind_dx/ qed.
91
92 (* Basic_2A1: removed theorems 1: fqup_drop *)