]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/static_2/syntax/ext2.ma
update in delayed_updating
[helm.git] / matita / matita / contribs / lambdadelta / static_2 / syntax / ext2.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "static_2/syntax/bind.ma".
16
17 (* EXTENSION TO BINDERS OF A RELATION FOR TERMS *****************************)
18
19 inductive ext2 (R:relation term): relation bind ≝
20 | ext2_unit: ∀I. ext2 R (BUnit I) (BUnit I)
21 | ext2_pair: ∀I,V1,V2. R V1 V2 → ext2 R (BPair I V1) (BPair I V2)
22 .
23
24 (* Basic_inversion lemmas **************************************************)
25
26 fact ext2_inv_unit_sn_aux: ∀R,Z1,Z2. ext2 R Z1 Z2 →
27                            ∀I. Z1 = BUnit I → Z2 = BUnit I.
28 #R #Z1 #Z2 * -Z1 -Z2 #I [2: #V1 #V2 #_ ]
29 #J #H destruct //
30 qed-.
31
32 lemma ext2_inv_unit_sn: ∀R,I,Z2. ext2 R (BUnit I) Z2 → Z2 = BUnit I.
33 /2 width=4 by ext2_inv_unit_sn_aux/ qed-.
34
35 fact ext2_inv_pair_sn_aux: ∀R,Z1,Z2. ext2 R Z1 Z2 →
36                            ∀I,V1. Z1 = BPair I V1 →
37                            ∃∃V2. R V1 V2 & Z2 = BPair I V2.
38 #R #Z1 #Z2 * -Z1 -Z2 #I [2: #V1 #V2 #HV12 ]
39 #J #W1 #H destruct /2 width=3 by ex2_intro/
40 qed-.
41
42 lemma ext2_inv_pair_sn: ∀R,Z2,I,V1. ext2 R (BPair I V1) Z2 →
43                         ∃∃V2. R V1 V2 & Z2 = BPair I V2.
44 /2 width=3 by ext2_inv_pair_sn_aux/ qed-.
45
46 fact ext2_inv_unit_dx_aux: ∀R,Z1,Z2. ext2 R Z1 Z2 →
47                            ∀I. Z2 = BUnit I → Z1 = BUnit I.
48 #R #Z1 #Z2 * -Z1 -Z2 #I [2: #V1 #V2 #_ ]
49 #J #H destruct //
50 qed-.
51
52 lemma ext2_inv_unit_dx: ∀R,I,Z1. ext2 R Z1 (BUnit I) → Z1 = BUnit I.
53 /2 width=4 by ext2_inv_unit_dx_aux/ qed-.
54
55 fact ext2_inv_pair_dx_aux: ∀R,Z1,Z2. ext2 R Z1 Z2 →
56                            ∀I,V2. Z2 = BPair I V2 →
57                            ∃∃V1. R V1 V2 & Z1 = BPair I V1.
58 #R #Z1 #Z2 * -Z1 -Z2 #I [2: #V1 #V2 #HV12 ]
59 #J #W2 #H destruct /2 width=3 by ex2_intro/
60 qed-.
61
62 lemma ext2_inv_pair_dx: ∀R,Z1,I,V2. ext2 R Z1 (BPair I V2) →
63                         ∃∃V1. R V1 V2 & Z1 = BPair I V1.
64 /2 width=3 by ext2_inv_pair_dx_aux/ qed-.
65
66 (* Advanced inversion lemmas ***********************************************)
67
68 lemma ext2_inv_unit: ∀R,I1,I2. ext2 R (BUnit I1) (BUnit I2) → I1 = I2.
69 #R #I1 #I2 #H lapply (ext2_inv_unit_sn … H) -H
70 #H destruct //
71 qed-.
72
73 lemma ext2_inv_pair: ∀R,I1,I2,V1,V2. ext2 R (BPair I1 V1) (BPair I2 V2) →
74                      I1 = I2 ∧ R V1 V2.
75 #R #I1 #I2 #V1 #V2 #H elim (ext2_inv_pair_sn … H) -H
76 #V #HV #H destruct /2 width=1 by conj/
77 qed-.
78
79 (* Basic properties ********************************************************)
80
81 lemma ext2_refl: ∀R. reflexive … R → reflexive … (ext2 R).
82 #R #HR * /2 width=1 by ext2_pair/
83 qed.
84
85 lemma ext2_sym: ∀R. symmetric … R → symmetric … (ext2 R).
86 #R #HR #T1 #T2 * /3 width=1 by ext2_unit, ext2_pair/
87 qed-.
88
89 lemma ext2_dec: ∀R. (∀T1,T2. Decidable (R T1 T2)) →
90                 ∀I1,I2. Decidable (ext2 R I1 I2).
91 #R #HR * #I1 [2: #T1 ] * #I2 [2,4: #T2 ]
92 [ elim (eq_bind2_dec I1 I2) #HI12 destruct
93   [ elim (HR T1 T2) -HR #HT12 /3 width=1 by ext2_pair, or_introl/ ]
94   @or_intror #H elim (ext2_inv_pair … H) -H /2 width=1 by/
95 | @or_intror #H lapply (ext2_inv_unit_sn … H) -H
96   #H destruct
97 | @or_intror #H lapply (ext2_inv_unit_dx … H) -H
98   #H destruct
99 | elim (eq_bind1_dec I1 I2) #HI12 destruct
100   /4 width=2 by ext2_inv_unit, ext2_unit, or_intror, or_introl/
101 ]
102 qed-.