X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Frelocation%2Frtmap_sand.ma;h=5f707a57108e0977b31e20eea65d9efec3dbe870;hb=064980eacc2efe70ffee96134d75dfa37506fc36;hp=85ad506a26f5582c2b84737104f65691fdeac26c;hpb=9b8d36ee041582f876543086e7659ed9e365e861;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sand.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sand.ma
index 85ad506a2..5f707a571 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sand.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sand.ma
@@ -25,6 +25,52 @@ coinductive sand: relation3 rtmap rtmap rtmap ≝
 interpretation "intersection (rtmap)"
    'RIntersection f1 f2 f = (sand f1 f2 f).
 
+(* Basic inversion lemmas ***************************************************)
+
+lemma sand_inv_ppx: ∀g1,g2,g. g1 ⋒ g2 ≡ g → ∀f1,f2. ↑f1 = g1 → ↑f2 = g2 →
+                    ∃∃f. f1 ⋒ f2 ≡ f & ↑f = g.
+#g1 #g2 #g * -g1 -g2 -g
+#f1 #f2 #f #g1 #g2 #g #Hf #H1 #H2 #H0 #x1 #x2 #Hx1 #Hx2 destruct
+try (>(injective_push … Hx1) -x1) try (>(injective_next … Hx1) -x1)
+try elim (discr_push_next … Hx1) try elim (discr_next_push … Hx1)
+try (>(injective_push … Hx2) -x2) try (>(injective_next … Hx2) -x2)
+try elim (discr_push_next … Hx2) try elim (discr_next_push … Hx2)
+/2 width=3 by ex2_intro/
+qed-.
+
+lemma sand_inv_npx: ∀g1,g2,g. g1 ⋒ g2 ≡ g → ∀f1,f2. ⫯f1 = g1 → ↑f2 = g2 →
+                    ∃∃f. f1 ⋒ f2 ≡ f & ↑f = g.
+#g1 #g2 #g * -g1 -g2 -g
+#f1 #f2 #f #g1 #g2 #g #Hf #H1 #H2 #H0 #x1 #x2 #Hx1 #Hx2 destruct
+try (>(injective_push … Hx1) -x1) try (>(injective_next … Hx1) -x1)
+try elim (discr_push_next … Hx1) try elim (discr_next_push … Hx1)
+try (>(injective_push … Hx2) -x2) try (>(injective_next … Hx2) -x2)
+try elim (discr_push_next … Hx2) try elim (discr_next_push … Hx2)
+/2 width=3 by ex2_intro/
+qed-.
+
+lemma sand_inv_pnx: ∀g1,g2,g. g1 ⋒ g2 ≡ g → ∀f1,f2. ↑f1 = g1 → ⫯f2 = g2 →
+                    ∃∃f. f1 ⋒ f2 ≡ f & ↑f = g.
+#g1 #g2 #g * -g1 -g2 -g
+#f1 #f2 #f #g1 #g2 #g #Hf #H1 #H2 #H0 #x1 #x2 #Hx1 #Hx2 destruct
+try (>(injective_push … Hx1) -x1) try (>(injective_next … Hx1) -x1)
+try elim (discr_push_next … Hx1) try elim (discr_next_push … Hx1)
+try (>(injective_push … Hx2) -x2) try (>(injective_next … Hx2) -x2)
+try elim (discr_push_next … Hx2) try elim (discr_next_push … Hx2)
+/2 width=3 by ex2_intro/
+qed-.
+
+lemma sand_inv_nnx: ∀g1,g2,g. g1 ⋒ g2 ≡ g → ∀f1,f2. ⫯f1 = g1 → ⫯f2 = g2 →
+                    ∃∃f. f1 ⋒ f2 ≡ f & ⫯f = g.
+#g1 #g2 #g * -g1 -g2 -g
+#f1 #f2 #f #g1 #g2 #g #Hf #H1 #H2 #H0 #x1 #x2 #Hx1 #Hx2 destruct
+try (>(injective_push … Hx1) -x1) try (>(injective_next … Hx1) -x1)
+try elim (discr_push_next … Hx1) try elim (discr_next_push … Hx1)
+try (>(injective_push … Hx2) -x2) try (>(injective_next … Hx2) -x2)
+try elim (discr_push_next … Hx2) try elim (discr_next_push … Hx2)
+/2 width=3 by ex2_intro/
+qed-.
+
 (* Basic properties *********************************************************)
 
 let corec sand_refl: ∀f. f ⋒ f ≡ f ≝ ?.