1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "ground/lib/bool.ma".
16 include "ground/lib/arith.ma".
18 (* ITEMS ********************************************************************)
21 inductive item0: Type[0] ≝
22 | Sort: nat → item0 (* sort: starting at 0 *)
23 | LRef: nat → item0 (* reference by index: starting at 0 *)
24 | GRef: nat → item0 (* reference by position: starting at 0 *)
27 (* binary binding items *)
28 inductive bind2: Type[0] ≝
29 | Abbr: bind2 (* abbreviation *)
30 | Abst: bind2 (* abstraction *)
33 (* binary non-binding items *)
34 inductive flat2: Type[0] ≝
35 | Appl: flat2 (* application *)
36 | Cast: flat2 (* explicit type annotation *)
40 inductive item2: Type[0] ≝
41 | Bind2: bool → bind2 → item2 (* polarized binding item *)
42 | Flat2: flat2 → item2 (* non-binding item *)
45 (* Basic inversion lemmas ***************************************************)
47 fact destruct_sort_sort_aux: ∀k1,k2. Sort k1 = Sort k2 → k1 = k2.
48 #k1 #k2 #H destruct //
51 (* Basic properties *********************************************************)
53 lemma eq_item0_dec: ∀I1,I2:item0. Decidable (I1 = I2).
54 * #i1 * #i2 [2,3,4,6,7,8: @or_intror #H destruct ]
55 elim (eq_nat_dec i1 i2) /2 width=1 by or_introl/
56 #Hni12 @or_intror #H destruct /2 width=1 by/
59 lemma eq_bind2_dec: ∀I1,I2:bind2. Decidable (I1 = I2).
60 * * /2 width=1 by or_introl/
61 @or_intror #H destruct
64 lemma eq_flat2_dec: ∀I1,I2:flat2. Decidable (I1 = I2).
65 * * /2 width=1 by or_introl/
66 @or_intror #H destruct
69 lemma eq_item2_dec: ∀I1,I2:item2. Decidable (I1 = I2).
70 * [ #a1 ] #I1 * [1,3: #a2 ] #I2
71 [2,3: @or_intror #H destruct
72 | elim (eq_bool_dec a1 a2) #Ha
73 [ elim (eq_bind2_dec I1 I2) /2 width=1 by or_introl/ #HI ]
74 @or_intror #H destruct /2 width=1 by/
75 | elim (eq_flat2_dec I1 I2) /2 width=1 by or_introl/ #HI
76 @or_intror #H destruct /2 width=1 by/