(**************************************************************************)
include "basic_2/notation/relations/supterm_6.ma".
-include "basic_2/grammar/lenv.ma".
-include "basic_2/grammar/genv.ma".
+include "basic_2/notation/relations/supterm_7.ma".
+include "basic_2/syntax/lenv.ma".
+include "basic_2/syntax/genv.ma".
include "basic_2/relocation/lifts.ma".
(* SUPCLOSURE ***************************************************************)
(* activate genv *)
-(* Note: frees_total requires fqu_drop for all atoms *)
-inductive fqu: tri_relation genv lenv term ≝
-| fqu_lref_O : ∀I,G,L,V. fqu G (L.ⓑ{I}V) (#0) G L V
-| fqu_pair_sn: ∀I,G,L,V,T. fqu G L (②{I}V.T) G L V
-| fqu_bind_dx: ∀p,I,G,L,V,T. fqu G L (ⓑ{p,I}V.T) G (L.ⓑ{I}V) T
-| fqu_flat_dx: ∀I,G,L,V,T. fqu G L (ⓕ{I}V.T) G L T
-| fqu_drop : ∀I,I1,I2,G,L,V. ⬆*[1] ⓪{I2} ≡ ⓪{I1} →
- fqu G (L.ⓑ{I}V) (⓪{I1}) G L (⓪{I2})
+(* Note: frees_total requires fqu_drop for all atoms
+ fqu_cpx_trans requires fqu_drop for all terms
+ frees_fqus_drops requires fqu_drop restricted on atoms
+*)
+inductive fqu (b:bool): tri_relation genv lenv term ≝
+| fqu_lref_O : ∀I,G,L,V. fqu b G (L.ⓑ{I}V) (#0) G L V
+| fqu_pair_sn: ∀I,G,L,V,T. fqu b G L (②{I}V.T) G L V
+| fqu_bind_dx: ∀p,I,G,L,V,T. fqu b G L (ⓑ{p,I}V.T) G (L.ⓑ{I}V) T
+| fqu_clear : ∀p,I,G,L,V,T. b = Ⓕ → fqu b G L (ⓑ{p,I}V.T) G (L.ⓧ) T
+| fqu_flat_dx: ∀I,G,L,V,T. fqu b G L (ⓕ{I}V.T) G L T
+| fqu_drop : ∀I,G,L,T,U. ⬆*[1] T ≘ U → fqu b G (L.ⓘ{I}) U G L T
.
+interpretation
+ "extended structural successor (closure)"
+ 'SupTerm b G1 L1 T1 G2 L2 T2 = (fqu b G1 L1 T1 G2 L2 T2).
+
interpretation
"structural successor (closure)"
- 'SupTerm G1 L1 T1 G2 L2 T2 = (fqu G1 L1 T1 G2 L2 T2).
+ 'SupTerm G1 L1 T1 G2 L2 T2 = (fqu true G1 L1 T1 G2 L2 T2).
(* Basic properties *********************************************************)
-lemma fqu_lref_S: ∀I,G,L,V,i. ⦃G, L.ⓑ{I}V, #(⫯i)⦄ ⊐ ⦃G, L, #(i)⦄.
+lemma fqu_sort: ∀b,I,G,L,s. ⦃G, L.ⓘ{I}, ⋆s⦄ ⊐[b] ⦃G, L, ⋆s⦄.
/2 width=1 by fqu_drop/ qed.
-(* Basic inversion lemmas ***************************************************)
+lemma fqu_lref_S: ∀b,I,G,L,i. ⦃G, L.ⓘ{I}, #↑i⦄ ⊐[b] ⦃G, L, #i⦄.
+/2 width=1 by fqu_drop/ qed.
-fact fqu_inv_atom1_aux: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
- ∀I. L1 = ⋆ → T1 = ⓪{I} → ⊥.
-#G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2
-[ #I #G #L #T #J #H destruct
-| #I #G #L #V #T #J #_ #H destruct
-| #p #I #G #L #V #T #J #_ #H destruct
-| #I #G #L #V #T #J #_ #H destruct
-| #I #I1 #I2 #G #L #V #_ #J #H destruct
-]
-qed-.
+lemma fqu_gref: ∀b,I,G,L,l. ⦃G, L.ⓘ{I}, §l⦄ ⊐[b] ⦃G, L, §l⦄.
+/2 width=1 by fqu_drop/ qed.
-lemma fqu_inv_atom1: ∀I,G1,G2,L2,T2. ⦃G1, ⋆, ⓪{I}⦄ ⊐ ⦃G2, L2, T2⦄ → ⊥.
-/2 width=10 by fqu_inv_atom1_aux/ qed-.
-
-fact fqu_inv_sort1_aux: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
- ∀I,K,V,s. L1 = K.ⓑ{I}V → T1 = ⋆s →
- ∧∧ G1 = G2 & L2 = K & T2 = ⋆s.
-#G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2
-[ #I #G #L #T #J #K #W #s #_ #H destruct
-| #I #G #L #V #T #J #K #W #s #_ #H destruct
-| #p #I #G #L #V #T #J #K #W #s #_ #H destruct
-| #I #G #L #V #T #J #K #W #s #_ #H destruct
-| #I #I1 #I2 #G #L #V #HI12 #J #K #W #s #H1 #H2 destruct
- lapply (lifts_inv_sort2 … HI12) -HI12 /2 width=1 by and3_intro/
-]
-qed-.
+(* Basic inversion lemmas ***************************************************)
-lemma fqu_inv_sort1: ∀I,G1,G2,K,L2,V,T2,s. ⦃G1, K.ⓑ{I}V, ⋆s⦄ ⊐ ⦃G2, L2, T2⦄ →
- ∧∧ G1 = G2 & L2 = K & T2 = ⋆s.
-/2 width=7 by fqu_inv_sort1_aux/ qed-.
-
-fact fqu_inv_zero1_aux: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
- ∀I,K,V. L1 = K.ⓑ{I}V → T1 = #0 →
- ∧∧ G1 = G2 & L2 = K & T2 = V.
-#G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2
-[ #I #G #L #T #J #K #W #H1 #H2 destruct /2 width=1 by and3_intro/
-| #I #G #L #V #T #J #K #W #_ #H destruct
-| #p #I #G #L #V #T #J #K #W #_ #H destruct
-| #I #G #L #V #T #J #K #W #_ #H destruct
-| #I #I1 #I2 #G #L #V #HI12 #J #K #W #H1 #H2 destruct
- elim (lifts_inv_lref2_uni_lt … HI12) -HI12 //
+fact fqu_inv_sort1_aux: ∀b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ →
+ ∀s. T1 = ⋆s →
+ ∃∃J. G1 = G2 & L1 = L2.ⓘ{J} & T2 = ⋆s.
+#b #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2
+[ #I #G #L #T #s #H destruct
+| #I #G #L #V #T #s #H destruct
+| #p #I #G #L #V #T #s #H destruct
+| #p #I #G #L #V #T #_ #s #H destruct
+| #I #G #L #V #T #s #H destruct
+| #I #G #L #T #U #HI12 #s #H destruct
+ lapply (lifts_inv_sort2 … HI12) -HI12 /2 width=2 by ex3_intro/
]
qed-.
-lemma fqu_inv_zero1: ∀I,G1,G2,K,L2,V,T2. ⦃G1, K.ⓑ{I}V, #0⦄ ⊐ ⦃G2, L2, T2⦄ →
- ∧∧ G1 = G2 & L2 = K & T2 = V.
-/2 width=9 by fqu_inv_zero1_aux/ qed-.
-
-fact fqu_inv_lref1_aux: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
- ∀I,K,V,i. L1 = K.ⓑ{I}V → T1 = #(⫯i) →
- ∧∧ G1 = G2 & L2 = K & T2 = #i.
-#G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2
-[ #I #G #L #T #J #K #W #i #_ #H destruct
-| #I #G #L #V #T #J #K #W #i #_ #H destruct
-| #p #I #G #L #V #T #J #K #W #i #_ #H destruct
-| #I #G #L #V #T #J #K #W #i #_ #H destruct
-| #I #I1 #I2 #G #L #V #HI12 #J #K #W #i #H1 #H2 destruct
- lapply (lifts_inv_lref2_uni_ge … HI12) -HI12 /2 width=1 by and3_intro/
+lemma fqu_inv_sort1: ∀b,G1,G2,L1,L2,T2,s. ⦃G1, L1, ⋆s⦄ ⊐[b] ⦃G2, L2, T2⦄ →
+ ∃∃J. G1 = G2 & L1 = L2.ⓘ{J} & T2 = ⋆s.
+/2 width=4 by fqu_inv_sort1_aux/ qed-.
+
+fact fqu_inv_lref1_aux: ∀b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ →
+ ∀i. T1 = #i →
+ (∃∃J,V. G1 = G2 & L1 = L2.ⓑ{J}V & T2 = V & i = 0) ∨
+ ∃∃J,j. G1 = G2 & L1 = L2.ⓘ{J} & T2 = #j & i = ↑j.
+#b #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2
+[ #I #G #L #T #i #H destruct /3 width=4 by ex4_2_intro, or_introl/
+| #I #G #L #V #T #i #H destruct
+| #p #I #G #L #V #T #i #H destruct
+| #p #I #G #L #V #T #_ #i #H destruct
+| #I #G #L #V #T #i #H destruct
+| #I #G #L #T #U #HI12 #i #H destruct
+ elim (lifts_inv_lref2_uni … HI12) -HI12 /3 width=3 by ex4_2_intro, or_intror/
]
qed-.
-lemma fqu_inv_lref1: ∀I,G1,G2,K,L2,V,T2,i. ⦃G1, K.ⓑ{I}V, #(⫯i)⦄ ⊐ ⦃G2, L2, T2⦄ →
- ∧∧ G1 = G2 & L2 = K & T2 = #i.
-/2 width=9 by fqu_inv_lref1_aux/ qed-.
-
-fact fqu_inv_gref1_aux: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
- ∀I,K,V,l. L1 = K.ⓑ{I}V → T1 = §l →
- ∧∧ G1 = G2 & L2 = K & T2 = §l.
-#G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2
-[ #I #G #L #T #J #K #W #l #_ #H destruct
-| #I #G #L #V #T #J #K #W #l #_ #H destruct
-| #p #I #G #L #V #T #J #K #W #l #_ #H destruct
-| #I #G #L #V #T #J #K #W #l #_ #H destruct
-| #I #I1 #I2 #G #L #V #HI12 #J #K #W #l #H1 #H2 destruct
- lapply (lifts_inv_gref2 … HI12) -HI12 /2 width=1 by and3_intro/
+lemma fqu_inv_lref1: ∀b,G1,G2,L1,L2,T2,i. ⦃G1, L1, #i⦄ ⊐[b] ⦃G2, L2, T2⦄ →
+ (∃∃J,V. G1 = G2 & L1 = L2.ⓑ{J}V & T2 = V & i = 0) ∨
+ ∃∃J,j. G1 = G2 & L1 = L2.ⓘ{J} & T2 = #j & i = ↑j.
+/2 width=4 by fqu_inv_lref1_aux/ qed-.
+
+fact fqu_inv_gref1_aux: ∀b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ →
+ ∀l. T1 = §l →
+ ∃∃J. G1 = G2 & L1 = L2.ⓘ{J} & T2 = §l.
+#b #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2
+[ #I #G #L #T #l #H destruct
+| #I #G #L #V #T #l #H destruct
+| #p #I #G #L #V #T #l #H destruct
+| #p #I #G #L #V #T #_ #l #H destruct
+| #I #G #L #V #T #s #H destruct
+| #I #G #L #T #U #HI12 #l #H destruct
+ lapply (lifts_inv_gref2 … HI12) -HI12 /2 width=3 by ex3_intro/
]
qed-.
-lemma fqu_inv_gref1: ∀I,G1,G2,K,L2,V,T2,l. ⦃G1, K.ⓑ{I}V, §l⦄ ⊐ ⦃G2, L2, T2⦄ →
- â\88§â\88§ G1 = G2 & L2 = K & T2 = §l.
-/2 width=7 by fqu_inv_gref1_aux/ qed-.
+lemma fqu_inv_gref1: ∀b,G1,G2,L1,L2,T2,l. ⦃G1, L1, §l⦄ ⊐[b] ⦃G2, L2, T2⦄ →
+ â\88\83â\88\83J. G1 = G2 & L1 = L2.â\93\98{J} & T2 = §l.
+/2 width=4 by fqu_inv_gref1_aux/ qed-.
-fact fqu_inv_bind1_aux: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
+fact fqu_inv_bind1_aux: ∀b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ →
∀p,I,V1,U1. T1 = ⓑ{p,I}V1.U1 →
- (∧∧ G1 = G2 & L1 = L2 & V1 = T2) ∨
- (∧∧ G1 = G2 & L1.ⓑ{I}V1 = L2 & U1 = T2).
-#G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2
-[ #I #G #L #T #q #J #W #U #H destruct
-| #I #G #L #V #T #q #J #W #U #H destruct /3 width=1 by and3_intro, or_introl/
-| #p #I #G #L #V #T #q #J #W #U #H destruct /3 width=1 by and3_intro, or_intror/
-| #I #G #L #V #T #q #J #W #U #H destruct
-| #I #I1 #I2 #G #L #V #_ #q #J #W #U #H destruct
+ ∨∨ ∧∧ G1 = G2 & L1 = L2 & V1 = T2
+ | ∧∧ G1 = G2 & L1.ⓑ{I}V1 = L2 & U1 = T2
+ | ∧∧ G1 = G2 & L1.ⓧ = L2 & U1 = T2 & b = Ⓕ
+ | ∃∃J. G1 = G2 & L1 = L2.ⓘ{J} & ⬆*[1] T2 ≘ ⓑ{p,I}V1.U1.
+#b #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2
+[ #I #G #L #T #q #J #V0 #U0 #H destruct
+| #I #G #L #V #T #q #J #V0 #U0 #H destruct /3 width=1 by and3_intro, or4_intro0/
+| #p #I #G #L #V #T #q #J #V0 #U0 #H destruct /3 width=1 by and3_intro, or4_intro1/
+| #p #I #G #L #V #T #Hb #q #J #V0 #U0 #H destruct /3 width=1 by and4_intro, or4_intro2/
+| #I #G #L #V #T #q #J #V0 #U0 #H destruct
+| #I #G #L #T #U #HTU #q #J #V0 #U0 #H destruct /3 width=2 by or4_intro3, ex3_intro/
]
qed-.
-lemma fqu_inv_bind1: ∀p,I,G1,G2,L1,L2,V1,U1,T2. ⦃G1, L1, ⓑ{p,I}V1.U1⦄ ⊐ ⦃G2, L2, T2⦄ →
- (∧∧ G1 = G2 & L1 = L2 & V1 = T2) ∨
- (∧∧ G1 = G2 & L1.ⓑ{I}V1 = L2 & U1 = T2).
+lemma fqu_inv_bind1: ∀b,p,I,G1,G2,L1,L2,V1,U1,T2. ⦃G1, L1, ⓑ{p,I}V1.U1⦄ ⊐[b] ⦃G2, L2, T2⦄ →
+ ∨∨ ∧∧ G1 = G2 & L1 = L2 & V1 = T2
+ | ∧∧ G1 = G2 & L1.ⓑ{I}V1 = L2 & U1 = T2
+ | ∧∧ G1 = G2 & L1.ⓧ = L2 & U1 = T2 & b = Ⓕ
+ | ∃∃J. G1 = G2 & L1 = L2.ⓘ{J} & ⬆*[1] T2 ≘ ⓑ{p,I}V1.U1.
/2 width=4 by fqu_inv_bind1_aux/ qed-.
-fact fqu_inv_flat1_aux: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
+lemma fqu_inv_bind1_true: ∀p,I,G1,G2,L1,L2,V1,U1,T2. ⦃G1, L1, ⓑ{p,I}V1.U1⦄ ⊐ ⦃G2, L2, T2⦄ →
+ ∨∨ ∧∧ G1 = G2 & L1 = L2 & V1 = T2
+ | ∧∧ G1 = G2 & L1.ⓑ{I}V1 = L2 & U1 = T2
+ | ∃∃J. G1 = G2 & L1 = L2.ⓘ{J} & ⬆*[1] T2 ≘ ⓑ{p,I}V1.U1.
+#p #I #G1 #G2 #L1 #L2 #V1 #U1 #T2 #H elim (fqu_inv_bind1 … H) -H
+/3 width=1 by or3_intro0, or3_intro1, or3_intro2/
+* #_ #_ #_ #H destruct
+qed-.
+
+fact fqu_inv_flat1_aux: ∀b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ →
∀I,V1,U1. T1 = ⓕ{I}V1.U1 →
- (∧∧ G1 = G2 & L1 = L2 & V1 = T2) ∨
- (∧∧ G1 = G2 & L1 = L2 & U1 = T2).
-#G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2
-[ #I #G #L #T #J #W #U #H destruct
-| #I #G #L #V #T #J #W #U #H destruct /3 width=1 by and3_intro, or_introl/
-| #p #I #G #L #V #T #J #W #U #H destruct
-| #I #G #L #V #T #J #W #U #H destruct /3 width=1 by and3_intro, or_intror/
-| #I #I1 #I2 #G #L #V #_ #J #W #U #H destruct
+ ∨∨ ∧∧ G1 = G2 & L1 = L2 & V1 = T2
+ | ∧∧ G1 = G2 & L1 = L2 & U1 = T2
+ | ∃∃J. G1 = G2 & L1 = L2.ⓘ{J} & ⬆*[1] T2 ≘ ⓕ{I}V1.U1.
+#b #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2
+[ #I #G #L #T #J #V0 #U0 #H destruct
+| #I #G #L #V #T #J #V0 #U0 #H destruct /3 width=1 by and3_intro, or3_intro0/
+| #p #I #G #L #V #T #J #V0 #U0 #H destruct
+| #p #I #G #L #V #T #_ #J #V0 #U0 #H destruct
+| #I #G #L #V #T #J #V0 #U0 #H destruct /3 width=1 by and3_intro, or3_intro1/
+| #I #G #L #T #U #HTU #J #V0 #U0 #H destruct /3 width=2 by or3_intro2, ex3_intro/
]
qed-.
-lemma fqu_inv_flat1: ∀I,G1,G2,L1,L2,V1,U1,T2. ⦃G1, L1, ⓕ{I}V1.U1⦄ ⊐ ⦃G2, L2, T2⦄ →
- (∧∧ G1 = G2 & L1 = L2 & V1 = T2) ∨
- (∧∧ G1 = G2 & L1 = L2 & U1 = T2).
+lemma fqu_inv_flat1: ∀b,I,G1,G2,L1,L2,V1,U1,T2. ⦃G1, L1, ⓕ{I}V1.U1⦄ ⊐[b] ⦃G2, L2, T2⦄ →
+ ∨∨ ∧∧ G1 = G2 & L1 = L2 & V1 = T2
+ | ∧∧ G1 = G2 & L1 = L2 & U1 = T2
+ | ∃∃J. G1 = G2 & L1 = L2.ⓘ{J} & ⬆*[1] T2 ≘ ⓕ{I}V1.U1.
/2 width=4 by fqu_inv_flat1_aux/ qed-.
+(* Advanced inversion lemmas ************************************************)
+
+lemma fqu_inv_atom1: ∀b,I,G1,G2,L2,T2. ⦃G1, ⋆, ⓪{I}⦄ ⊐[b] ⦃G2, L2, T2⦄ → ⊥.
+#b * #x #G1 #G2 #L2 #T2 #H
+[ elim (fqu_inv_sort1 … H) | elim (fqu_inv_lref1 … H) * | elim (fqu_inv_gref1 … H) ] -H
+#I [2: #V |3: #i ] #_ #H destruct
+qed-.
+
+lemma fqu_inv_sort1_bind: ∀b,I,G1,G2,K,L2,T2,s. ⦃G1, K.ⓘ{I}, ⋆s⦄ ⊐[b] ⦃G2, L2, T2⦄ →
+ ∧∧ G1 = G2 & L2 = K & T2 = ⋆s.
+#b #I #G1 #G2 #K #L2 #T2 #s #H elim (fqu_inv_sort1 … H) -H
+#Z #X #H1 #H2 destruct /2 width=1 by and3_intro/
+qed-.
+
+lemma fqu_inv_zero1_pair: ∀b,I,G1,G2,K,L2,V,T2. ⦃G1, K.ⓑ{I}V, #0⦄ ⊐[b] ⦃G2, L2, T2⦄ →
+ ∧∧ G1 = G2 & L2 = K & T2 = V.
+#b #I #G1 #G2 #K #L2 #V #T2 #H elim (fqu_inv_lref1 … H) -H *
+#Z #X #H1 #H2 #H3 #H4 destruct /2 width=1 by and3_intro/
+qed-.
+
+lemma fqu_inv_lref1_bind: ∀b,I,G1,G2,K,L2,T2,i. ⦃G1, K.ⓘ{I}, #(↑i)⦄ ⊐[b] ⦃G2, L2, T2⦄ →
+ ∧∧ G1 = G2 & L2 = K & T2 = #i.
+#b #I #G1 #G2 #K #L2 #T2 #i #H elim (fqu_inv_lref1 … H) -H *
+#Z #X #H1 #H2 #H3 #H4 destruct /2 width=1 by and3_intro/
+qed-.
+
+lemma fqu_inv_gref1_bind: ∀b,I,G1,G2,K,L2,T2,l. ⦃G1, K.ⓘ{I}, §l⦄ ⊐[b] ⦃G2, L2, T2⦄ →
+ ∧∧ G1 = G2 & L2 = K & T2 = §l.
+#b #I #G1 #G2 #K #L2 #T2 #l #H elim (fqu_inv_gref1 … H) -H
+#Z #H1 #H2 #H3 destruct /2 width=1 by and3_intro/
+qed-.
+
(* Basic_2A1: removed theorems 3:
fqu_drop fqu_drop_lt fqu_lref_S_lt
*)
projects / helm.git / blobdiff