- more background for the exclusion binder

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / syntax / bind.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/bind.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/bind.ma
index ca474406d499dc2650ecdcab1aa3fc83da92e092..8787d709b1b4d873f889b5945e1af6bdf454fa89 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/syntax/bind.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/bind.ma
@@ -21,16 +21,69 @@ inductive bind: Type[0] ≝
 | BPair: bind2 → term → bind
 .
 
+inductive ext2 (R:relation term): relation bind ≝
+| ext2_unit: ∀I. ext2 R (BUnit I) (BUnit I)
+| ext2_pair: ∀I,V1,V2. R V1 V2 → ext2 R (BPair I V1) (BPair I V2)
+.
+
+(* Basic_inversion lemmas **************************************************)
+
+fact ext2_inv_unit_sn_aux: ∀R,Z1,Z2. ext2 R Z1 Z2 →
+                           ∀I. Z1 = BUnit I → Z2 = BUnit I.
+#R #Z1 #Z2 * -Z1 -Z2 #I [2: #V1 #V2 #_ ]
+#J #H destruct //
+qed-.
+
+lemma ext2_inv_unit_sn: ∀R,I,Z2. ext2 R (BUnit I) Z2 → Z2 = BUnit I.
+/2 width=4 by ext2_inv_unit_sn_aux/ qed-.
+
+fact ext2_inv_pair_sn_aux: ∀R,Z1,Z2. ext2 R Z1 Z2 →
+                           ∀I,V1. Z1 = BPair I V1 →
+                           ∃∃V2. R V1 V2 & Z2 = BPair I V2.
+#R #Z1 #Z2 * -Z1 -Z2 #I [2: #V1 #V2 #HV12 ]
+#J #W1 #H destruct /2 width=3 by ex2_intro/
+qed-.
+
+lemma ext2_inv_pair_sn: ∀R,Z2,I,V1. ext2 R (BPair I V1) Z2 →
+                        ∃∃V2. R V1 V2 & Z2 = BPair I V2.
+/2 width=3 by ext2_inv_pair_sn_aux/ qed-.
+
+fact ext2_inv_unit_dx_aux: ∀R,Z1,Z2. ext2 R Z1 Z2 →
+                           ∀I. Z2 = BUnit I → Z1 = BUnit I.
+#R #Z1 #Z2 * -Z1 -Z2 #I [2: #V1 #V2 #_ ]
+#J #H destruct //
+qed-.
+
+lemma ext2_inv_unit_dx: ∀R,I,Z1. ext2 R Z1 (BUnit I) → Z1 = BUnit I.
+/2 width=4 by ext2_inv_unit_dx_aux/ qed-.
+
+fact ext2_inv_pair_dx_aux: ∀R,Z1,Z2. ext2 R Z1 Z2 →
+                           ∀I,V2. Z2 = BPair I V2 →
+                           ∃∃V1. R V1 V2 & Z1 = BPair I V1.
+#R #Z1 #Z2 * -Z1 -Z2 #I [2: #V1 #V2 #HV12 ]
+#J #W2 #H destruct /2 width=3 by ex2_intro/
+qed-.
+
+lemma ext2_inv_pair_dx: ∀R,Z1,I,V2. ext2 R Z1 (BPair I V2) →
+                        ∃∃V1. R V1 V2 & Z1 = BPair I V1.
+/2 width=3 by ext2_inv_pair_dx_aux/ qed-.
+
 (* Basic properties ********************************************************)
 
 lemma eq_bind_dec: ∀I1,I2:bind. Decidable (I1 = I2).
 * #I1 [2: #V1 ] * #I2 [2,4: #V2 ]
-[ elim (eq_bind2_dec I1 I2) #HI
-  [ elim (eq_term_dec V1 V2) #HV /2 width=1 by or_introl/ ]
-  @or_intror #H destruct /2 width=1 by/
-| @or_intror #H destruct
-| @or_intror #H destruct
-| elim (eq_bind1_dec I1 I2) #HI /2 width=1 by or_introl/
-  @or_intror #H destruct /2 width=1 by/
+[1: elim (eq_bind2_dec I1 I2) #HI
+    [ elim (eq_term_dec V1 V2) #HV ]
+|4: elim (eq_bind1_dec I1 I2) #HI
 ]
+/2 width=1 by or_introl/
+@or_intror #H destruct /2 width=1 by/
+qed-.
+
+lemma ext2_refl: ∀R. reflexive … R → reflexive … (ext2 R).
+#R #HR * /2 width=1 by ext2_pair/
+qed.
+
+lemma ext2_sym: ∀R. symmetric … R → symmetric … (ext2 R).
+#R #HR #T1 #T2 * /3 width=1 by ext2_unit, ext2_pair/
 qed-.