update in ground_2 static_2 basic_2

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / syntax / tueq.ma

diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/tueq.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/tueq.ma
deleted file mode 100644 (file)
index 49a6b2f..0000000
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/tueq.ma
+++ /dev/null
@@ -1,143 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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 "static_2/notation/relations/approxeq_2.ma".
-include "static_2/syntax/term.ma".
-
-(* TAIL SORT-IRRELEVANT EQUIVALENCE ON TERMS ********************************)
-
-inductive tueq: relation term ≝
-| tueq_sort: ∀s1,s2. tueq (⋆s1) (⋆s2)
-| tueq_lref: ∀i. tueq (#i) (#i)
-| tueq_gref: ∀l. tueq (§l) (§l)
-| tueq_bind: ∀p,I,V,T1,T2. tueq T1 T2 → tueq (ⓑ{p,I}V.T1) (ⓑ{p,I}V.T2)
-| tueq_appl: ∀V,T1,T2. tueq T1 T2 → tueq (ⓐV.T1) (ⓐV.T2)
-| tueq_cast: ∀V1,V2,T1,T2. tueq V1 V2 → tueq T1 T2 → tueq (ⓝV1.T1) (ⓝV2.T2)
-.
-
-interpretation
-   "context-free tail sort-irrelevant equivalence (term)"
-   'ApproxEq T1 T2 = (tueq T1 T2).
-
-(* Basic properties *********************************************************)
-
-lemma tueq_refl: reflexive … tueq.
-#T elim T -T * [|||| * ] 
-/2 width=1 by tueq_sort, tueq_lref, tueq_gref, tueq_bind, tueq_appl, tueq_cast/
-qed.
-
-lemma tueq_sym: symmetric … tueq.
-#T1 #T2 #H elim H -T1 -T2
-/2 width=3 by tueq_sort, tueq_bind, tueq_appl, tueq_cast/
-qed-.
-
-(* Left basic inversion lemmas **********************************************)
-
-fact tueq_inv_sort1_aux: ∀X,Y. X ≅ Y → ∀s1. X = ⋆s1 →
-                         ∃s2. Y = ⋆s2.
-#X #Y * -X -Y
-[ #s1 #s2 #s #H destruct /2 width=2 by ex_intro/
-| #i #s #H destruct
-| #l #s #H destruct
-| #p #I #V #T1 #T2 #_ #s #H destruct
-| #V #T1 #T2 #_ #s #H destruct
-| #V1 #V2 #T1 #T2 #_ #_ #s #H destruct
-]
-qed-.
-
-lemma tueq_inv_sort1: ∀Y,s1. ⋆s1 ≅ Y →
-                      ∃s2. Y = ⋆s2.
-/2 width=4 by tueq_inv_sort1_aux/ qed-.
-
-fact tueq_inv_lref1_aux: ∀X,Y. X ≅ Y → ∀i. X = #i → Y = #i.
-#X #Y * -X -Y //
-[ #s1 #s2 #j #H destruct
-| #p #I #V #T1 #T2 #_ #j #H destruct
-| #V #T1 #T2 #_ #j #H destruct
-| #V1 #V2 #T1 #T2 #_ #_ #j #H destruct
-]
-qed-.
-
-lemma tueq_inv_lref1: ∀Y,i. #i ≅ Y → Y = #i.
-/2 width=5 by tueq_inv_lref1_aux/ qed-.
-
-fact tueq_inv_gref1_aux: ∀X,Y. X ≅ Y → ∀l. X = §l → Y = §l.
-#X #Y * -X -Y //
-[ #s1 #s2 #k #H destruct
-| #p #I #V #T1 #T2 #_ #k #H destruct
-| #V #T1 #T2 #_ #k #H destruct
-| #V1 #V2 #T1 #T2 #_ #_ #k #H destruct
-]
-qed-.
-
-lemma tueq_inv_gref1: ∀Y,l. §l ≅ Y → Y = §l.
-/2 width=5 by tueq_inv_gref1_aux/ qed-.
-
-fact tueq_inv_bind1_aux: ∀X,Y. X ≅ Y → ∀p,I,V,T1. X = ⓑ{p,I}V.T1 →
-                         ∃∃T2. T1 ≅ T2 & Y = ⓑ{p,I}V.T2.
-#X #Y * -X -Y
-[ #s1 #s2 #q #J #W #U1 #H destruct
-| #i #q #J #W #U1 #H destruct
-| #l #q #J #W #U1 #H destruct
-| #p #I #V #T1 #T2 #HT #q #J #W #U1 #H destruct /2 width=3 by ex2_intro/
-| #V #T1 #T2 #_ #q #J #W #U1 #H destruct
-| #V1 #V2 #T1 #T2 #_ #_ #q #J #W #U1 #H destruct
-]
-qed-.
-
-lemma tueq_inv_bind1: ∀p,I,V,T1,Y. ⓑ{p,I}V.T1 ≅ Y →
-                      ∃∃T2. T1 ≅ T2 & Y = ⓑ{p,I}V.T2.
-/2 width=3 by tueq_inv_bind1_aux/ qed-.
-
-fact tueq_inv_appl1_aux: ∀X,Y. X ≅ Y → ∀V,T1. X = ⓐV.T1 →
-                         ∃∃T2. T1 ≅ T2 & Y = ⓐV.T2.
-#X #Y * -X -Y
-[ #s1 #s2 #W #U1 #H destruct
-| #i #W #U1 #H destruct
-| #l #W #U1 #H destruct
-| #p #I #V #T1 #T2 #_ #W #U1 #H destruct
-| #V #T1 #T2 #HT #W #U1 #H destruct /2 width=3 by ex2_intro/
-| #V1 #V2 #T1 #T2 #_ #_ #W #U1 #H destruct
-]
-qed-.
-
-lemma tueq_inv_appl1: ∀V,T1,Y. ⓐV.T1 ≅ Y →
-                      ∃∃T2. T1 ≅ T2 & Y = ⓐV.T2.
-/2 width=3 by tueq_inv_appl1_aux/ qed-.
-
-fact tueq_inv_cast1_aux: ∀X,Y. X ≅ Y → ∀V1,T1. X = ⓝV1.T1 →
-                         ∃∃V2,T2. V1 ≅ V2 & T1 ≅ T2 & Y = ⓝV2.T2.
-#X #Y * -X -Y
-[ #s1 #s2 #W1 #U1 #H destruct
-| #i #W1 #U1 #H destruct
-| #l #W1 #U1 #H destruct
-| #p #I #V #T1 #T2 #_ #W1 #U1 #H destruct
-| #V #T1 #T2 #_ #W1 #U1 #H destruct
-| #V1 #V2 #T1 #T2 #HV #HT #W1 #U1 #H destruct /2 width=5 by ex3_2_intro/
-]
-qed-.
-
-lemma tueq_inv_cast1: ∀V1,T1,Y. ⓝV1.T1 ≅ Y →
-                      ∃∃V2,T2. V1 ≅ V2 & T1 ≅ T2 & Y = ⓝV2.T2.
-/2 width=3 by tueq_inv_cast1_aux/ qed-.
-
-(* Right basic inversion lemmas *********************************************)
-
-lemma tueq_inv_bind2: ∀p,I,V,T2,X1. X1 ≅ ⓑ{p,I}V.T2 →
-                      ∃∃T1. T1 ≅ T2 & X1 = ⓑ{p,I}V.T1.
-#p #I #V #T2 #X1 #H
-elim (tueq_inv_bind1 p I V T2 X1)
-[ #T1 #HT #H destruct ]
-/3 width=3 by tueq_sym, ex2_intro/
-qed-.