-nlemma eq_to_eqasttype : ∀t1,t2.t1 = t2 → eq_ast_type t1 t2 = true.
- #t1;
- napply (ast_type_index … t1);
- ##[ ##1: #b1; #t2; ncases t2;
- ##[ ##1: #b2; #H; nrewrite > (asttype_destruct_base_base … H);
- nchange with ((eq_ast_base_type b2 b2) = true);
- nrewrite > (eq_to_eqastbasetype b2 b2 (refl_eq …));
- napply refl_eq
- ##| ##2: #st2; #n2; #H; napply (asttype_destruct … H)
- ##| ##3: #nl2; #H; napply (asttype_destruct … H)
- ##]
- ##| ##2: #st1; #n1; #H; #t2; ncases t2;
- ##[ ##2: #st2; #n2; #H1; nchange with (((eq_ast_type st1 st2)⊗(eq_nat n1 n2)) = true);
- nrewrite > (H st2 (asttype_destruct_array_array_1 … H1));
- nrewrite > (eq_to_eqnat n1 n2 (asttype_destruct_array_array_2 … H1));
- nnormalize;
- napply refl_eq
- ##| ##1: #b2; #H1; napply (asttype_destruct … H1)
- ##| ##3: #nl2; #H1; napply (asttype_destruct … H1)
- ##]
- ##| ##3: #hh1; #H; #t2; ncases t2;
- ##[ ##3: #nl2; ncases nl2;
- ##[ ##1: #hh2; #H1; nchange with ((eq_ast_type hh1 hh2) = true);
- nrewrite > (H hh2 (nelist_destruct_nil_nil ? hh1 hh2 (asttype_destruct_struct_struct … H1)));
- napply refl_eq
- ##| ##2: #hh2; #ll2; #H1; nelim (nelist_destruct_nil_cons ? hh1 hh2 ll2 (asttype_destruct_struct_struct … H1))
- ##]
- ##| ##1: #b2; #H1; napply (asttype_destruct … H1)
- ##| ##2: #st2; #n2; #H1; napply (asttype_destruct … H1)
- ##]
- ##| ##4: #hh1; #ll1; #H; #H1; #t2; ncases t2;
- ##[ ##3: #nl2; ncases nl2;
- ##[ ##1: #hh2; #H2; nelim (nelist_destruct_cons_nil ? hh1 hh2 ll1 (asttype_destruct_struct_struct … H2))
- ##| ##2: #hh2; #ll2; #H2; nchange with (((eq_ast_type hh1 hh2)⊗(bfold_right_neList2 ? (λx,y.eq_ast_type x y) ll1 ll2)) = true);
- nrewrite > (H hh2 (nelist_destruct_cons_cons_1 … (asttype_destruct_struct_struct … H2)));
- nrewrite > (eq_to_eqasttype_aux1 ll1 ll2 (H1 (AST_TYPE_STRUCT ll2) ?));
- ##[ ##1: nnormalize; napply refl_eq
- ##| ##2: nrewrite > (nelist_destruct_cons_cons_2 … (asttype_destruct_struct_struct … H2));
- napply refl_eq
- ##]
- ##]
- ##| ##1: #b2; #H2; napply (asttype_destruct … H2)
- ##| ##2: #st2; #n2; #H2; napply (asttype_destruct … H2)
- ##]
+nlemma decidable_asttype : ∀x,y:ast_type.decidable (x = y).
+ #x; #y; nnormalize;
+ napply (or2_elim (eq_asttype x y = true) (eq_asttype x y = false) ? (decidable_bexpr ?));
+ ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqasttype_to_eq … H))
+ ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqasttype_to_neq … H))
+ ##]
+nqed.
+
+nlemma symmetric_eqasttype : symmetricT ast_type bool eq_asttype.
+ #n1; #n2;
+ napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_asttype n1 n2));
+ ##[ ##1: #H; nrewrite > H; napply refl_eq
+ ##| ##2: #H; nrewrite > (neq_to_neqasttype n1 n2 H);
+ napply (symmetric_eq ? (eq_asttype n2 n1) false);
+ napply (neq_to_neqasttype n2 n1 (symmetric_neq ? n1 n2 H))