]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/static_2/s_computation/fqup.ma
d01ca0882d22dee39109c1f211c3a80ba4b29ac0
[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/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 *)