X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fsyntax%2Ftdeq.ma;h=60c1e4d13750ced7ac2d026d2b350cf89e4b762f;hp=358533f04015ed2016350694c14d6e480475e8d7;hb=4173283e148199871d787c53c0301891deb90713;hpb=a67fc50ccfda64377e2c94c18c3a0d9265f651db

diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/tdeq.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/tdeq.ma
index 358533f04..60c1e4d13 100644
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/tdeq.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/tdeq.ma
@@ -12,132 +12,116 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "static_2/notation/relations/stareq_4.ma".
-include "static_2/syntax/item_sd.ma".
+include "static_2/notation/relations/stareq_2.ma".
 include "static_2/syntax/term.ma".
 
-(* DEGREE-BASED EQUIVALENCE ON TERMS ****************************************)
+(* SORT-IRRELEVANT EQUIVALENCE ON TERMS *************************************)
 
-inductive tdeq (h) (o): relation term ≝
-| tdeq_sort: ∀s1,s2,d. deg h o s1 d → deg h o s2 d → tdeq h o (⋆s1) (⋆s2)
-| tdeq_lref: ∀i. tdeq h o (#i) (#i)
-| tdeq_gref: ∀l. tdeq h o (§l) (§l)
-| tdeq_pair: ∀I,V1,V2,T1,T2. tdeq h o V1 V2 → tdeq h o T1 T2 → tdeq h o (②{I}V1.T1) (②{I}V2.T2)
+inductive tdeq: relation term ≝
+| tdeq_sort: ∀s1,s2. tdeq (⋆s1) (⋆s2)
+| tdeq_lref: ∀i. tdeq (#i) (#i)
+| tdeq_gref: ∀l. tdeq (§l) (§l)
+| tdeq_pair: ∀I,V1,V2,T1,T2. tdeq V1 V2 → tdeq T1 T2 → tdeq (②{I}V1.T1) (②{I}V2.T2)
 .
 
 interpretation
-   "context-free degree-based equivalence (term)"
-   'StarEq h o T1 T2 = (tdeq h o T1 T2).
+   "context-free sort-irrelevant equivalence (term)"
+   'StarEq T1 T2 = (tdeq T1 T2).
 
 (* Basic properties *********************************************************)
 
-lemma tdeq_refl: ∀h,o. reflexive … (tdeq h o).
-#h #o #T elim T -T /2 width=1 by tdeq_pair/
+lemma tdeq_refl: reflexive … tdeq.
+#T elim T -T /2 width=1 by tdeq_pair/
 * /2 width=1 by tdeq_lref, tdeq_gref/
-#s elim (deg_total h o s) /2 width=3 by tdeq_sort/
 qed.
 
-lemma tdeq_sym: ∀h,o. symmetric … (tdeq h o).
-#h #o #T1 #T2 #H elim H -T1 -T2
+lemma tdeq_sym: symmetric … tdeq.
+#T1 #T2 #H elim H -T1 -T2
 /2 width=3 by tdeq_sort, tdeq_lref, tdeq_gref, tdeq_pair/
 qed-.
 
 (* Basic inversion lemmas ***************************************************)
 
-fact tdeq_inv_sort1_aux: ∀h,o,X,Y. X ≛[h, o] Y → ∀s1. X = ⋆s1 →
-                         ∃∃s2,d. deg h o s1 d & deg h o s2 d & Y = ⋆s2.
-#h #o #X #Y * -X -Y
-[ #s1 #s2 #d #Hs1 #Hs2 #s #H destruct /2 width=5 by ex3_2_intro/
+fact tdeq_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
 | #I #V1 #V2 #T1 #T2 #_ #_ #s #H destruct
 ]
 qed-.
 
-lemma tdeq_inv_sort1: ∀h,o,Y,s1. ⋆s1 ≛[h, o] Y →
-                      ∃∃s2,d. deg h o s1 d & deg h o s2 d & Y = ⋆s2.
-/2 width=3 by tdeq_inv_sort1_aux/ qed-.
+lemma tdeq_inv_sort1: ∀Y,s1. ⋆s1 ≛ Y →
+                      ∃s2. Y = ⋆s2.
+/2 width=4 by tdeq_inv_sort1_aux/ qed-.
 
-fact tdeq_inv_lref1_aux: ∀h,o,X,Y. X ≛[h, o] Y → ∀i. X = #i → Y = #i.
-#h #o #X #Y * -X -Y //
-[ #s1 #s2 #d #_ #_ #j #H destruct
+fact tdeq_inv_lref1_aux: ∀X,Y. X ≛ Y → ∀i. X = #i → Y = #i.
+#X #Y * -X -Y //
+[ #s1 #s2 #j #H destruct
 | #I #V1 #V2 #T1 #T2 #_ #_ #j #H destruct
 ]
 qed-.
 
-lemma tdeq_inv_lref1: ∀h,o,Y,i. #i ≛[h, o] Y → Y = #i.
+lemma tdeq_inv_lref1: ∀Y,i. #i ≛ Y → Y = #i.
 /2 width=5 by tdeq_inv_lref1_aux/ qed-.
 
-fact tdeq_inv_gref1_aux: ∀h,o,X,Y. X ≛[h, o] Y → ∀l. X = §l → Y = §l.
-#h #o #X #Y * -X -Y //
-[ #s1 #s2 #d #_ #_ #k #H destruct
+fact tdeq_inv_gref1_aux: ∀X,Y. X ≛ Y → ∀l. X = §l → Y = §l.
+#X #Y * -X -Y //
+[ #s1 #s2 #k #H destruct
 | #I #V1 #V2 #T1 #T2 #_ #_ #k #H destruct
 ]
 qed-.
 
-lemma tdeq_inv_gref1: ∀h,o,Y,l. §l ≛[h, o] Y → Y = §l.
+lemma tdeq_inv_gref1: ∀Y,l. §l ≛ Y → Y = §l.
 /2 width=5 by tdeq_inv_gref1_aux/ qed-.
 
-fact tdeq_inv_pair1_aux: ∀h,o,X,Y. X ≛[h, o] Y → ∀I,V1,T1. X = ②{I}V1.T1 →
-                         ∃∃V2,T2. V1 ≛[h, o] V2 & T1 ≛[h, o] T2 & Y = ②{I}V2.T2.
-#h #o #X #Y * -X -Y
-[ #s1 #s2 #d #_ #_ #J #W1 #U1 #H destruct
+fact tdeq_inv_pair1_aux: ∀X,Y. X ≛ Y → ∀I,V1,T1. X = ②{I}V1.T1 →
+                         ∃∃V2,T2. V1 ≛ V2 & T1 ≛ T2 & Y = ②{I}V2.T2.
+#X #Y * -X -Y
+[ #s1 #s2 #J #W1 #U1 #H destruct
 | #i #J #W1 #U1 #H destruct
 | #l #J #W1 #U1 #H destruct
 | #I #V1 #V2 #T1 #T2 #HV #HT #J #W1 #U1 #H destruct /2 width=5 by ex3_2_intro/
 ]
 qed-.
 
-lemma tdeq_inv_pair1: ∀h,o,I,V1,T1,Y. ②{I}V1.T1 ≛[h, o] Y →
-                      ∃∃V2,T2. V1 ≛[h, o] V2 & T1 ≛[h, o] T2 & Y = ②{I}V2.T2.
+lemma tdeq_inv_pair1: ∀I,V1,T1,Y. ②{I}V1.T1 ≛ Y →
+                      ∃∃V2,T2. V1 ≛ V2 & T1 ≛ T2 & Y = ②{I}V2.T2.
 /2 width=3 by tdeq_inv_pair1_aux/ qed-.
 
-lemma tdeq_inv_sort2: ∀h,o,X1,s2. X1 ≛[h, o] ⋆s2 →
-                      ∃∃s1,d. deg h o s1 d & deg h o s2 d & X1 = ⋆s1.
-#h #o #X1 #s2 #H
-elim (tdeq_inv_sort1 h o X1 s2)
-/2 width=5 by tdeq_sym, ex3_2_intro/
+lemma tdeq_inv_sort2: ∀X1,s2. X1 ≛ ⋆s2 →
+                      ∃s1. X1 = ⋆s1.
+#X1 #s2 #H
+elim (tdeq_inv_sort1 X1 s2)
+/2 width=2 by tdeq_sym, ex_intro/
 qed-.
 
-lemma tdeq_inv_pair2: ∀h,o,I,X1,V2,T2. X1 ≛[h, o] ②{I}V2.T2 →
-                      ∃∃V1,T1. V1 ≛[h, o] V2 & T1 ≛[h, o] T2 & X1 = ②{I}V1.T1.
-#h #o #I #X1 #V2 #T2 #H
-elim (tdeq_inv_pair1 h o I V2 T2 X1)
+lemma tdeq_inv_pair2: ∀I,X1,V2,T2. X1 ≛ ②{I}V2.T2 →
+                      ∃∃V1,T1. V1 ≛ V2 & T1 ≛ T2 & X1 = ②{I}V1.T1.
+#I #X1 #V2 #T2 #H
+elim (tdeq_inv_pair1 I V2 T2 X1)
 [ #V1 #T1 #HV #HT #H destruct ]
 /3 width=5 by tdeq_sym, ex3_2_intro/
 qed-.
 
 (* Advanced inversion lemmas ************************************************)
 
-lemma tdeq_inv_sort1_deg: ∀h,o,Y,s1. ⋆s1 ≛[h, o] Y → ∀d. deg h o s1 d →
-                          ∃∃s2. deg h o s2 d & Y = ⋆s2.
-#h #o #Y #s1 #H #d #Hs1 elim (tdeq_inv_sort1 … H) -H
-#s2 #x #Hx <(deg_mono h o … Hx … Hs1) -s1 -d /2 width=3 by ex2_intro/
-qed-.
-
-lemma tdeq_inv_sort_deg: ∀h,o,s1,s2. ⋆s1 ≛[h, o] ⋆s2 →
-                         ∀d1,d2. deg h o s1 d1 → deg h o s2 d2 →
-                         d1 = d2.
-#h #o #s1 #y #H #d1 #d2 #Hs1 #Hy
-elim (tdeq_inv_sort1_deg … H … Hs1) -s1 #s2 #Hs2 #H destruct
-<(deg_mono h o … Hy … Hs2) -s2 -d1 //
-qed-.
-
-lemma tdeq_inv_pair: ∀h,o,I1,I2,V1,V2,T1,T2. ②{I1}V1.T1 ≛[h, o] ②{I2}V2.T2 →
-                     ∧∧ I1 = I2 & V1 ≛[h, o] V2 & T1 ≛[h, o] T2.
-#h #o #I1 #I2 #V1 #V2 #T1 #T2 #H elim (tdeq_inv_pair1 … H) -H
+lemma tdeq_inv_pair: ∀I1,I2,V1,V2,T1,T2. ②{I1}V1.T1 ≛ ②{I2}V2.T2 →
+                     ∧∧ I1 = I2 & V1 ≛ V2 & T1 ≛ T2.
+#I1 #I2 #V1 #V2 #T1 #T2 #H elim (tdeq_inv_pair1 … H) -H
 #V0 #T0 #HV #HT #H destruct /2 width=1 by and3_intro/
 qed-.
 
-lemma tdeq_inv_pair_xy_x: ∀h,o,I,V,T. ②{I}V.T ≛[h, o] V → ⊥.
-#h #o #I #V elim V -V
+lemma tdeq_inv_pair_xy_x: ∀I,V,T. ②{I}V.T ≛ V → ⊥.
+#I #V elim V -V
 [ #J #T #H elim (tdeq_inv_pair1 … H) -H #X #Y #_ #_ #H destruct
 | #J #X #Y #IHX #_ #T #H elim (tdeq_inv_pair … H) -H #H #HY #_ destruct /2 width=2 by/
 ]
 qed-.
 
-lemma tdeq_inv_pair_xy_y: ∀h,o,I,T,V. ②{I}V.T ≛[h, o] T → ⊥.
-#h #o #I #T elim T -T
+lemma tdeq_inv_pair_xy_y: ∀I,T,V. ②{I}V.T ≛ T → ⊥.
+#I #T elim T -T
 [ #J #V #H elim (tdeq_inv_pair1 … H) -H #X #Y #_ #_ #H destruct
 | #J #X #Y #_ #IHY #V #H elim (tdeq_inv_pair … H) -H #H #_ #HY destruct /2 width=2 by/
 ]
@@ -145,23 +129,19 @@ qed-.
 
 (* Basic forward lemmas *****************************************************)
 
-lemma tdeq_fwd_atom1: ∀h,o,I,Y. ⓪{I} ≛[h, o] Y → ∃J. Y = ⓪{J}.
-#h #o * #x #Y #H [ elim (tdeq_inv_sort1 … H) -H ]
+lemma tdeq_fwd_atom1: ∀I,Y. ⓪{I} ≛ Y → ∃J. Y = ⓪{J}.
+* #x #Y #H [ elim (tdeq_inv_sort1 … H) -H ]
 /3 width=4 by tdeq_inv_gref1, tdeq_inv_lref1, ex_intro/
 qed-.
 
 (* Advanced properties ******************************************************)
 
-lemma tdeq_dec: ∀h,o,T1,T2. Decidable (T1 ≛[h, o] T2).
-#h #o #T1 elim T1 -T1 [ * #s1 | #I1 #V1 #T1 #IHV #IHT ] * [1,3,5,7: * #s2 |*: #I2 #V2 #T2 ]
-[ elim (deg_total h o s1) #d1 #H1
-  elim (deg_total h o s2) #d2 #H2
-  elim (eq_nat_dec d1 d2) #Hd12 destruct /3 width=3 by tdeq_sort, or_introl/
-  @or_intror #H
-  lapply (tdeq_inv_sort_deg … H … H1 H2) -H -H1 -H2 /2 width=1 by/
+lemma tdeq_dec: ∀T1,T2. Decidable (T1 ≛ T2).
+#T1 elim T1 -T1 [ * #s1 | #I1 #V1 #T1 #IHV #IHT ] * [1,3,5,7: * #s2 |*: #I2 #V2 #T2 ]
+[ /3 width=1 by tdeq_sort, or_introl/
 |2,3,13:
   @or_intror #H
-  elim (tdeq_inv_sort1 … H) -H #x1 #x2 #_ #_ #H destruct
+  elim (tdeq_inv_sort1 … H) -H #x #H destruct
 |4,6,14:
   @or_intror #H
   lapply (tdeq_inv_lref1 … H) -H #H destruct
@@ -192,13 +172,13 @@ qed-.
 
 (* Negated inversion lemmas *************************************************)
 
-lemma tdneq_inv_pair: ∀h,o,I1,I2,V1,V2,T1,T2.
-                      (②{I1}V1.T1 ≛[h, o] ②{I2}V2.T2 → ⊥) → 
+lemma tdneq_inv_pair: ∀I1,I2,V1,V2,T1,T2.
+                      (②{I1}V1.T1 ≛ ②{I2}V2.T2 → ⊥) → 
                       ∨∨ I1 = I2 → ⊥
-                      |  (V1 ≛[h, o] V2 → ⊥)
-                      |  (T1 ≛[h, o] T2 → ⊥).
-#h #o #I1 #I2 #V1 #V2 #T1 #T2 #H12
+                      |  (V1 ≛ V2 → ⊥)
+                      |  (T1 ≛ T2 → ⊥).
+#I1 #I2 #V1 #V2 #T1 #T2 #H12
 elim (eq_item2_dec I1 I2) /3 width=1 by or3_intro0/ #H destruct
-elim (tdeq_dec h o V1 V2) /3 width=1 by or3_intro1/
-elim (tdeq_dec h o T1 T2) /4 width=1 by tdeq_pair, or3_intro2/
+elim (tdeq_dec V1 V2) /3 width=1 by or3_intro1/
+elim (tdeq_dec T1 T2) /4 width=1 by tdeq_pair, or3_intro2/
 qed-.